Switch 'fx -x' to use only canonical divisors in 'fx'.

src/base/abci/abc.c

@@ -3980,7 +3980,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int nLitCountMax, int fVerbose, int fVeryVerbose );
+    extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int nLitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose );
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     Fxu_Data_t Params, * p = &Params;
     int c, fNewAlgo = 1;
@@ -3988,7 +3988,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set the defaults
     Abc_NtkSetDefaultFxParams( p );
     Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "SDNWMPsdzcnvwh")) != EOF )
+    while ( (c = Extra_UtilGetopt(argc, argv, "SDNWMPsdzcnxvwh")) != EOF )
     {
         switch (c)
         {
@@ -4073,6 +4073,9 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
             case 'n':
                 fNewAlgo ^= 1;
                 break;
+            case 'x':
+                p->fCanonDivs ^= 1;
+                break;
             case 'v':
                 p->fVerbose ^= 1;
                 break;
@@ -4114,14 +4117,14 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // the nodes to be merged are linked into the special linked list
     if ( fNewAlgo )
-        Abc_NtkFxPerform( pNtk, p->nNodesExt, p->LitCountMax, p->fVerbose, p->fVeryVerbose );
+        Abc_NtkFxPerform( pNtk, p->nNodesExt, p->LitCountMax, p->fCanonDivs, p->fVerbose, p->fVeryVerbose );
     else
         Abc_NtkFastExtract( pNtk, p );
     Abc_NtkFxuFreeInfo( p );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: fx [-SDNWMP <num>] [-sdzcnvwh]\n");
+    Abc_Print( -2, "usage: fx [-SDNWMP <num>] [-sdzcnxvwh]\n");
     Abc_Print( -2, "\t           performs unate fast extract on the current network\n");
     Abc_Print( -2, "\t-S <num> : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax );
     Abc_Print( -2, "\t-D <num> : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax );
@@ -4134,6 +4137,7 @@ usage:
     Abc_Print( -2, "\t-z       : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" );
     Abc_Print( -2, "\t-c       : use complement in the binary case [default = %s]\n", p->fUseCompl? "yes": "no" );
     Abc_Print( -2, "\t-n       : use new implementation of fast extract [default = %s]\n", fNewAlgo? "yes": "no" );
+    Abc_Print( -2, "\t-x       : use only canonical divisors (AND, XOR, MUX) [default = %s]\n", p->fCanonDivs? "yes": "no" );
     Abc_Print( -2, "\t-v       : print verbose information [default = %s]\n", p->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w       : print additional information [default = %s]\n", p->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");

src/base/abci/abcFx.c

@@ -88,6 +88,7 @@ struct Fx_Man_t_
     // user's data
     Vec_Wec_t *     vCubes;     // cube -> lit
     int             LitCountMax;// max size of divisor to extract
+    int             fCanonDivs; // use only AND/XOR/MUX
     // internal data
     Vec_Wec_t *     vLits;      // lit -> cube
     Vec_Int_t *     vCounts;    // literal counts (currently not used)
@@ -300,9 +301,9 @@ int Abc_NtkFxCheck( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int LitCountMax, int fVerbose, int fVeryVerbose )
+int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int LitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose )
 {
-    extern int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fVerbose, int fVeryVerbose );
+    extern int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose );
     Vec_Wec_t * vCubes;
     assert( Abc_NtkIsSopLogic(pNtk) );
     // check unique fanins
@@ -319,7 +320,7 @@ int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int LitCountMax, int f
     // collect information about the covers
     vCubes = Abc_NtkFxRetrieve( pNtk );
     // call the fast extract procedure
-    if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), nNewNodesMax, LitCountMax, fVerbose, fVeryVerbose ) > 0 )
+    if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), nNewNodesMax, LitCountMax, fCanonDivs, fVerbose, fVeryVerbose ) > 0 )
     {
         // update the network
         Abc_NtkFxInsert( pNtk, vCubes );
@@ -841,9 +842,13 @@ void Fx_ManCubeDoubleCubeDivisors( Fx_Man_t * p, int iFirst, Vec_Int_t * vPivot,
                 p->nDivMux[1]++;
             else
                 p->nDivMux[2]++;
+            if ( p->fCanonDivs && Value < 0 )
+                continue;
         }
         if ( p->LitCountMax && p->LitCountMax < Vec_IntSize(p->vCubeFree) )
             continue;
+        if ( p->fCanonDivs && Vec_IntSize(p->vCubeFree) == 3 )
+            continue;
         iDiv = Hsh_VecManAdd( p->pHash, p->vCubeFree );
         if ( !fRemove )
         {
@@ -1167,7 +1172,7 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv, int * fWarning )
   SeeAlso     []
 
 ***********************************************************************/
-int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fVerbose, int fVeryVerbose )
+int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose )
 {
     int fVeryVeryVerbose = 0;
     int i, iDiv, fWarning = 0;
@@ -1176,6 +1181,7 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitC
     // initialize the data-structure
     p = Fx_ManStart( vCubes );
     p->LitCountMax = LitCountMax;
+    p->fCanonDivs = fCanonDivs;
     Fx_ManCreateLiterals( p, ObjIdMax );
     Fx_ManComputeLevel( p );
     Fx_ManCreateDivisors( p );

src/opt/fxu/fxu.h

@@ -56,6 +56,7 @@ struct FxuDataStruct
     int               nPairsMax;        // the max number of double-cube divisors to consider
     int               WeightMin;        // the min weight of a divisor to extract
     int               LitCountMax;      // the max literal count of a divisor to consider
+    int               fCanonDivs;       // use only canonical divisors (AND/XOR/MUX) 
     // the input information
     Vec_Ptr_t *       vSops;            // the SOPs for each node in the network
     Vec_Ptr_t *       vFanins;          // the fanins of each node in the network