diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-06-17 21:53:04 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-06-17 21:53:04 -0700 |
commit | 22406e71014007e662f20402035eed258fe0169c (patch) | |
tree | 62216122006033839389d74d7c85f0611e7c8b7a | |
parent | c912875261ae9da7e6ffeeb3466b7d467ee4b010 (diff) | |
parent | 85428a60ccea5de48d4507501e420efb082f3201 (diff) | |
download | abc-22406e71014007e662f20402035eed258fe0169c.tar.gz abc-22406e71014007e662f20402035eed258fe0169c.tar.bz2 abc-22406e71014007e662f20402035eed258fe0169c.zip |
Merged in boschmitt/abc (pull request #28)
Handling D1C and SCC in FXCH
-rw-r--r-- | src/opt/fxch/Fxch.h | 28 | ||||
-rw-r--r-- | src/opt/fxch/FxchDiv.c | 11 | ||||
-rw-r--r-- | src/opt/fxch/FxchMan.c | 258 | ||||
-rw-r--r-- | src/opt/fxch/FxchSCHashTable.c | 20 |
4 files changed, 189 insertions, 128 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 ); diff --git a/src/opt/fxch/FxchDiv.c b/src/opt/fxch/FxchDiv.c index 68fd569d..18c8bbfb 100644 --- a/src/opt/fxch/FxchDiv.c +++ b/src/opt/fxch/FxchDiv.c @@ -457,6 +457,17 @@ void Fxch_DivPrint( Fxch_Man_t* pFxchMan, printf( "Divs =%8d \n", Hsh_VecSize( pFxchMan->pDivHash ) ); } +int Fxch_DivIsNotConstant1( Vec_Int_t* vDiv ) +{ + int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ), + Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) ); + + if ( ( Vec_IntSize( vDiv ) == 2 ) && ( Lit0 == Abc_LitNot( Lit1 ) ) ) + return 0; + + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/fxch/FxchMan.c b/src/opt/fxch/FxchMan.c index 83794ea9..19886ea5 100644 --- a/src/opt/fxch/FxchMan.c +++ b/src/opt/fxch/FxchMan.c @@ -24,13 +24,13 @@ ABC_NAMESPACE_IMPL_START /// LOCAL FUNCTIONS DEFINITIONS /// //////////////////////////////////////////////////////////////////////// static inline int Fxch_ManSCAddRemove( Fxch_Man_t* pFxchMan, - 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 fAdd, - char fUpdate ) + char fUpdate ) { int ret = 0; @@ -170,6 +170,7 @@ Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes ) pFxchMan->vDivCubePairs = Vec_WecAlloc( 1000 ); pFxchMan->vCubeFree = Vec_IntAlloc( 100 ); pFxchMan->vDiv = Vec_IntAlloc( 100 ); + pFxchMan->vSCC = Vec_IntAlloc( 64 ); pFxchMan->vCubesS = Vec_IntAlloc( 100 ); pFxchMan->vPairs = Vec_IntAlloc( 100 ); @@ -188,6 +189,7 @@ void Fxch_ManFree( Fxch_Man_t* pFxchMan ) Vec_IntFree( pFxchMan->vLevels ); Vec_IntFree( pFxchMan->vCubeFree ); Vec_IntFree( pFxchMan->vDiv ); + Vec_IntFree( pFxchMan->vSCC ); Vec_IntFree( pFxchMan->vCubesS ); Vec_IntFree( pFxchMan->vPairs ); ABC_FREE( pFxchMan ); @@ -341,86 +343,88 @@ void Fxch_ManComputeLevel( Fxch_Man_t* pFxchMan ) } } -void Fxch_ManUpdate( Fxch_Man_t* pFxchMan, - int iDiv ) +/* Extract divisor from single-cubes */ +static inline void Fxch_ManExtractDivFromCube( Fxch_Man_t* pFxchMan, + const int Lit0, + const int Lit1, + const int iVarNew ) { - int i, - k, - iCube0, - iCube1, - Lit0 = -1, - Lit1 = -1, - iVarNew, - Level, - nCompls; + int i, iCube0; + Vec_Int_t* vLitP = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 2 ); - Vec_Int_t* vCube0, - * vCube1, - * vLitP, - * vLitN, - * vDivCubePairs; + Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i ) + { + int RetValue; + Vec_Int_t* vCube0; - /* Get the selected candidate (divisor) */ - Vec_IntClear( pFxchMan->vDiv ); - Vec_IntAppend( pFxchMan->vDiv, Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv ) ); + vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 ); + RetValue = Vec_IntRemove1( vCube0, Abc_LitNot( Lit0 ) ); + RetValue += Vec_IntRemove1( vCube0, Abc_LitNot( Lit1 ) ); + assert( RetValue == 2 ); - /* Find cubes associated with the single divisor */ - Vec_IntClear( pFxchMan->vCubesS ); - if ( Vec_IntSize( pFxchMan->vDiv ) == 2 ) - { - Lit0 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 0 ) ); - Lit1 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 1 ) ); - assert( Lit0 >= 0 && Lit1 >= 0 ); + Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) ); + Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); - Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit0 ) ) ); - Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ) ); - Vec_IntTwoRemoveCommon( Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit0 ) ), - Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ), - pFxchMan->vCubesS ); + pFxchMan->nLits--; } +} +/* Extract divisor from cube pairs */ +static inline int Fxch_ManExtractDivFromCubePairs( Fxch_Man_t* pFxchMan, + const int iVarNew ) +{ + /* For each pair (Ci, Cj) */ + int k = 0, + iCube0, iCube1, i; - /* Find pairs associated with the divisor */ - Vec_IntClear( pFxchMan->vPairs ); - vDivCubePairs = Vec_WecEntry( pFxchMan->vDivCubePairs, iDiv ); - Vec_IntAppend( pFxchMan->vPairs, vDivCubePairs ); - Vec_IntErase( vDivCubePairs ); + Vec_Int_t* vLitP = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 2 ), + * vLitN = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 1 ); Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i ) { - assert( Fxch_ManGetLit( pFxchMan, iCube0, 0) == Fxch_ManGetLit( pFxchMan, iCube1, 0) ); - if (iCube0 > iCube1) - { - Vec_IntSetEntry( pFxchMan->vPairs, i, iCube1); - Vec_IntSetEntry( pFxchMan->vPairs, i+1, iCube0); - } - } + int RetValue, + fCompl = 0; - Vec_IntUniqifyPairs( pFxchMan->vPairs ); - assert( Vec_IntSize( pFxchMan->vPairs ) % 2 == 0 ); + Vec_Int_t* vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 ), + * vCube1 = Fxch_ManGetCube( pFxchMan, iCube1 ); - /* subtract cost of single-cube divisors */ - Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i ) - Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1); /* remove (fAdd = 0) - fUpdate = 1 */ + RetValue = Fxch_DivRemoveLits( vCube0, vCube1, pFxchMan->vDiv, &fCompl ); - Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i ) - Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1), /* remove (fAdd = 0) - fUpdate = 1 */ - Fxch_ManDivSingleCube( pFxchMan, iCube1, 0, 1); /* remove (fAdd = 0) - fUpdate = 1 */ + assert( RetValue == Vec_IntSize( pFxchMan->vDiv ) ); - /* subtract cost of double-cube divisors */ - Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i ) - { - if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) ) - Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */ - } + pFxchMan->nLits -= Vec_IntSize( pFxchMan->vDiv ) + Vec_IntSize( vCube1 ) - 2; - Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i ) - { - if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) ) - Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */ + /* Remove second cube */ + Vec_IntClear( vCube1 ); + Vec_IntWriteEntry( pFxchMan->vPairs, k++, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + if ( iVarNew ) + { + if ( Vec_IntSize( pFxchMan->vDiv ) == 2 || fCompl ) + { + Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 1 ) ); + Vec_IntPush( vLitN, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + } + else + { + Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) ); + Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + } + } } + return k; +} + +static inline int Fxch_ManCreateCube( Fxch_Man_t* pFxchMan, + int Lit0, + int Lit1 ) +{ + int Level, + iVarNew; + Vec_Int_t* vCube0, + * vCube1; + /* Create a new variable */ iVarNew = pFxchMan->nVars; pFxchMan->nVars++; @@ -457,58 +461,89 @@ void Fxch_ManUpdate( Fxch_Man_t* pFxchMan, pFxchMan->nLits += Vec_IntSize( pFxchMan->vDiv ); /* Create new literals */ - vLitP = Vec_WecPushLevel( pFxchMan->vLits ); - vLitN = Vec_WecPushLevel( pFxchMan->vLits ); - vLitP = Vec_WecEntry( pFxchMan->vLits, Vec_WecSize( pFxchMan->vLits ) - 2 ); + Vec_WecPushLevel( pFxchMan->vLits ); + Vec_WecPushLevel( pFxchMan->vLits ); - /* Extract divisor from single-cubes */ - Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i ) - { - int RetValue; + return iVarNew; +} - vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 ); - RetValue = Vec_IntRemove1( vCube0, Abc_LitNot( Lit0 ) ); - RetValue += Vec_IntRemove1( vCube0, Abc_LitNot( Lit1 ) ); - assert( RetValue == 2 ); +void Fxch_ManUpdate( Fxch_Man_t* pFxchMan, + int iDiv ) +{ + int i, iCube0, iCube1, + Lit0 = -1, + Lit1 = -1, + iVarNew; - Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) ); - Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + Vec_Int_t* vCube0, + * vCube1, + * vDivCubePairs; - pFxchMan->nLits--; + /* Get the selected candidate (divisor) */ + Vec_IntClear( pFxchMan->vDiv ); + Vec_IntAppend( pFxchMan->vDiv, Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv ) ); + + /* Find cubes associated with the divisor */ + Vec_IntClear( pFxchMan->vCubesS ); + if ( Vec_IntSize( pFxchMan->vDiv ) == 2 ) + { + Lit0 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 0 ) ); + Lit1 = Abc_Lit2Var( Vec_IntEntry( pFxchMan->vDiv, 1 ) ); + assert( Lit0 >= 0 && Lit1 >= 0 ); + + Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit0 ) ) ); + Fxch_ManCompressCubes( pFxchMan->vCubes, Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ) ); + Vec_IntTwoRemoveCommon( Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit0 ) ), + Vec_WecEntry( pFxchMan->vLits, Abc_LitNot( Lit1 ) ), + pFxchMan->vCubesS ); } - /* For each pair (Ci, Cj) */ - /* Extract divisor from cube pairs */ - k = 0; - nCompls = 0; + /* Find pairs associated with the divisor */ + Vec_IntClear( pFxchMan->vPairs ); + vDivCubePairs = Vec_WecEntry( pFxchMan->vDivCubePairs, iDiv ); + Vec_IntAppend( pFxchMan->vPairs, vDivCubePairs ); + Vec_IntErase( vDivCubePairs ); + Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i ) { - int RetValue, fCompl = 0; + assert( Fxch_ManGetLit( pFxchMan, iCube0, 0) == Fxch_ManGetLit( pFxchMan, iCube1, 0) ); + if (iCube0 > iCube1) + { + Vec_IntSetEntry( pFxchMan->vPairs, i, iCube1); + Vec_IntSetEntry( pFxchMan->vPairs, i+1, iCube0); + } + } - vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 ); - vCube1 = Fxch_ManGetCube( pFxchMan, iCube1 ); + Vec_IntUniqifyPairs( pFxchMan->vPairs ); + assert( Vec_IntSize( pFxchMan->vPairs ) % 2 == 0 ); - RetValue = Fxch_DivRemoveLits( vCube0, vCube1, pFxchMan->vDiv, &fCompl ); - nCompls += fCompl; + /* subtract cost of single-cube divisors */ + Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i ) + Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1); /* remove (fAdd = 0) - fUpdate = 1 */ - assert( RetValue == Vec_IntSize( pFxchMan->vDiv ) ); + Vec_IntForEachEntryDouble( pFxchMan->vPairs, iCube0, iCube1, i ) + Fxch_ManDivSingleCube( pFxchMan, iCube0, 0, 1), /* remove (fAdd = 0) - fUpdate = 1 */ + Fxch_ManDivSingleCube( pFxchMan, iCube1, 0, 1); /* remove (fAdd = 0) - fUpdate = 1 */ - if ( Vec_IntSize( pFxchMan->vDiv ) == 2 || fCompl ) - { - Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 1 ) ); - Vec_IntPush( vLitN, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); - } - else - { - Vec_IntPush( vCube0, Abc_Var2Lit( iVarNew, 0 ) ); - Vec_IntPush( vLitP, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); - } - pFxchMan->nLits -= Vec_IntSize( pFxchMan->vDiv ) + Vec_IntSize( vCube1 ) - 2; + /* subtract cost of double-cube divisors */ + Vec_IntForEachEntry( pFxchMan->vCubesS, iCube0, i ) + if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) ) + Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */ - /* Remove second cube */ - Vec_IntClear( vCube1 ); - Vec_IntWriteEntry( pFxchMan->vPairs, k++, Vec_WecLevelId( pFxchMan->vCubes, vCube0 ) ); + Vec_IntForEachEntry( pFxchMan->vPairs, iCube0, i ) + if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) ) + Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */ + + int k = 0; + if ( Fxch_DivIsNotConstant1( pFxchMan->vDiv ) ) + { + iVarNew = Fxch_ManCreateCube( pFxchMan, Lit0, Lit1 ); + Fxch_ManExtractDivFromCube( pFxchMan, Lit0, Lit1, iVarNew ); + k = Fxch_ManExtractDivFromCubePairs( pFxchMan, iVarNew ); } + else + k = Fxch_ManExtractDivFromCubePairs( pFxchMan, 0 ); + assert( k == Vec_IntSize( pFxchMan->vPairs ) / 2 ); Vec_IntShrink( pFxchMan->vPairs, k ); @@ -528,6 +563,22 @@ void Fxch_ManUpdate( Fxch_Man_t* pFxchMan, if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) ) Fxch_ManDivDoubleCube( pFxchMan, iCube0, 1, 1 ); /* fAdd = 1 - fUpdate = 1 */ + /* Deal with SCC */ + if ( Vec_IntSize( pFxchMan->vSCC ) ) + { + Vec_IntUniqify( pFxchMan->vSCC ); + Vec_IntForEachEntry( pFxchMan->vSCC, iCube0, i ) + if ( iCube0 < Vec_IntSize(pFxchMan->pSCHashTable->vCubeLinks) ) + { + Fxch_ManDivDoubleCube( pFxchMan, iCube0, 0, 1 ); /* remove (fAdd = 0) - fUpdate = 1 */ + vCube0 = Fxch_ManGetCube( pFxchMan, iCube0 ), + Vec_IntClear( vCube0 ); + } + + Vec_IntClear( pFxchMan->vSCC ); + } + + /* If it's a double-cube devisor add its cost */ if ( Vec_IntSize( pFxchMan->vDiv ) > 2 ) { @@ -567,7 +618,6 @@ void Fxch_ManPrintDivs( Fxch_Man_t* pFxchMan ) void Fxch_ManPrintStats( Fxch_Man_t* pFxchMan ) { - printf( "[FXCH] "); printf( "Cubes =%8d ", Vec_WecSizeUsed( pFxchMan->vCubes ) ); printf( "Lits =%8d ", Vec_WecSizeUsed( pFxchMan->vLits ) ); printf( "Divs =%8d ", Hsh_VecSize( pFxchMan->pDivHash ) ); diff --git a/src/opt/fxch/FxchSCHashTable.c b/src/opt/fxch/FxchSCHashTable.c index 1bf7e8b3..a37009eb 100644 --- a/src/opt/fxch/FxchSCHashTable.c +++ b/src/opt/fxch/FxchSCHashTable.c @@ -182,10 +182,6 @@ static inline int Fxch_SCHashTableEntryCompare( Fxch_SCHashTable_t* pSCHashTable Vec_IntClear( &pSCHashTable->vSubCube0 ); Vec_IntClear( &pSCHashTable->vSubCube1 ); - if ( pSCData0->iLit1 == 0 && pSCData1->iLit1 == 0 && - Vec_IntEntry( vCube0, pSCData0->iLit0 ) == Abc_LitNot( Vec_IntEntry( vCube1, pSCData1->iLit0 ) ) ) - return 0; - if ( pSCData0->iLit1 > 0 && pSCData1->iLit1 > 0 && ( Vec_IntEntry( vCube0, pSCData0->iLit0 ) == Vec_IntEntry( vCube1, pSCData1->iLit0 ) || Vec_IntEntry( vCube0, pSCData0->iLit0 ) == Vec_IntEntry( vCube1, pSCData1->iLit1 ) || @@ -270,14 +266,16 @@ int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable, if ( !Fxch_SCHashTableEntryCompare( pSCHashTable, vCubes, &( pEntry->SCData ), &( pNewEntry->SCData ) ) ) continue; - if ( pEntry->SCData.iLit0 == 0 ) - { - printf("[FXCH] SCC detected\n"); - continue; - } - if ( pNewEntry->SCData.iLit0 == 0 ) + if ( ( pEntry->SCData.iLit0 == 0 ) || ( pNewEntry->SCData.iLit0 == 0 ) ) { - printf("[FXCH] SCC detected\n"); + Vec_Int_t* vCube0 = Fxch_ManGetCube( pSCHashTable->pFxchMan, pEntry->SCData.iCube ), + * vCube1 = Fxch_ManGetCube( pSCHashTable->pFxchMan, pEntry->SCData.iCube ); + + if ( Vec_IntSize( vCube0 ) > Vec_IntSize( vCube1 ) ) + Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pEntry->SCData.iCube ); + else + Vec_IntPush( pSCHashTable->pFxchMan->vSCC, pNewEntry->SCData.iCube ); + continue; } |