diff options
Diffstat (limited to 'src/opt/fxch/Fxch.h')
| -rw-r--r-- | src/opt/fxch/Fxch.h | 28 |
1 files changed, 15 insertions, 13 deletions
diff --git a/src/opt/fxch/Fxch.h b/src/opt/fxch/Fxch.h index d9f9dc7e..5781846c 100644 --- a/src/opt/fxch/Fxch.h +++ b/src/opt/fxch/Fxch.h @@ -40,22 +40,22 @@ typedef struct Fxch_SCHashTable_Entry_t_ Fxch_SCHashTable_Entry_t; //////////////////////////////////////////////////////////////////////// /* Sub-Cube Structure * - * In the context of this program, a sub-cube is a cube derived from + * In the context of this program, a sub-cube is a cube derived from * another cube by removing one or two literals. Since a cube is represented - * as a vector of literals, one might think that a sub-cube would also be - * represented in the same way. However, in order to same memory, we only + * as a vector of literals, one might think that a sub-cube would also be + * represented in the same way. However, in order to same memory, we only * store a sub-cube identifier and the data necessary to generate the sub-cube: * - The index number of the orignal cube in the cover. (iCube) * - Identifiers of which literal(s) was(were) removed. (iLit0, iLit1) * - * The sub-cube identifier is generated by adding the unique identifiers of - * its literals. + * The sub-cube identifier is generated by adding the unique identifiers of + * its literals. * */ struct Fxch_SubCube_t_ { - unsigned int Id, - iCube; + unsigned int Id, + iCube; unsigned int iLit0 : 16, iLit1 : 16; }; @@ -112,6 +112,7 @@ struct Fxch_Man_t_ Vec_Int_t* vPairs; /* cube pairs for the given double cube divisor */ Vec_Int_t* vCubeFree; // cube-free divisor Vec_Int_t* vDiv; // selected divisor + Vec_Int_t* vSCC; /* Statistics */ abctime timeInit; /* Initialization time */ @@ -145,6 +146,7 @@ int Fxch_DivRemove( Fxch_Man_t* pFxchMan, int fUpdate, int fSingleCube, int fBa void Fxch_DivSepareteCubes( Vec_Int_t* vDiv, Vec_Int_t* vCube0, Vec_Int_t* vCube1 ); int Fxch_DivRemoveLits( Vec_Int_t* vCube0, Vec_Int_t* vCube1, Vec_Int_t* vDiv, int *fCompl ); void Fxch_DivPrint( Fxch_Man_t* pFxchMan, int iDiv ); +int Fxch_DivIsNotConstant1( Vec_Int_t* vDiv ); /*===== FxchMan.c ====================================================================================================*/ Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes ); @@ -181,19 +183,19 @@ void Fxch_SCHashTableDelete( Fxch_SCHashTable_t* ); int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable, Vec_Wec_t* vCubes, - unsigned int SubCubeID, + unsigned int SubCubeID, unsigned int iSubCube, - unsigned int iCube, - unsigned int iLit0, + unsigned int iCube, + unsigned int iLit0, unsigned int iLit1, char fUpdate ); int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable, Vec_Wec_t* vCubes, - unsigned int SubCubeID, + unsigned int SubCubeID, unsigned int iSubCube, - unsigned int iCube, - unsigned int iLit0, + unsigned int iCube, + unsigned int iLit0, unsigned int iLit1, char fUpdate ); |