summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/opt/fxch/Fxch.h28
-rw-r--r--src/opt/fxch/FxchDiv.c11
-rw-r--r--src/opt/fxch/FxchMan.c258
-rw-r--r--src/opt/fxch/FxchSCHashTable.c20
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;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-30 00:17:10 +0000