Merged in boschmitt/abc (pull request #28)

Handling D1C and SCC in FXCH

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 );
 

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                                ///
 ////////////////////////////////////////////////////////////////////////

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;
         }