Enables FXCH to handle Distance-1 cubes (D1C) and Single Cube Containment (SCC) as by product of extraction.

D1C: Whenever they appear a constant divisor (x! + x)  will be created and handle as any other divisor.
SCC: Will be taken care of as soon as they appear.

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