Added switch -M to set max size of two-cube divisors to extract (often helps both runtime and quality).

5 files changed, 38 insertions, 19 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c51c53c5..4493c361 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3582,14 +3582,14 @@ usage:
 ***********************************************************************/
 int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int fVerbose );
+    extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int nLitCountMax, int fVerbose );
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     Fxu_Data_t Params, * p = &Params;
     int c, fNewAlgo = 1;
     // set the defaults
     Abc_NtkSetDefaultParams( p );
     Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "SDNWsdzcnvh")) != EOF )
+    while ( (c = Extra_UtilGetopt(argc, argv, "SDNWMsdzcnvh")) != EOF )
     {
         switch (c)
         {
@@ -3632,9 +3632,20 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
                     Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
                     goto usage;
                 }
-                p->WeightMax = atoi(argv[globalUtilOptind]);
+                p->WeightMin = atoi(argv[globalUtilOptind]);
                 globalUtilOptind++;
-                if ( p->WeightMax < 0 )
+                if ( p->WeightMin < 0 )
+                    goto usage;
+                break;
+            case 'M':
+                if ( globalUtilOptind >= argc )
+                {
+                    Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                    goto usage;
+                }
+                p->LitCountMax = atoi(argv[globalUtilOptind]);
+                globalUtilOptind++;
+                if ( p->LitCountMax < 0 )
                     goto usage;
                 break;
             case 's':
@@ -3685,19 +3696,20 @@ 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->fVerbose );
+        Abc_NtkFxPerform( pNtk, p->nNodesExt, p->LitCountMax, p->fVerbose );
     else
         Abc_NtkFastExtract( pNtk, p );
     Abc_NtkFxuFreeInfo( p );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: fx [-SDNW <num>] [-sdzcnvh]\n");
+    Abc_Print( -2, "usage: fx [-SDNWM <num>] [-sdzcnvh]\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 );
     Abc_Print( -2, "\t-N <num> : max number of divisors to extract during this run [default = %d]\n", p->nNodesExt );
-    Abc_Print( -2, "\t-W <num> : only extract divisors with weight more than this [default = %d]\n", p->WeightMax );
+    Abc_Print( -2, "\t-W <num> : lower bound on the weight of divisors to extract [default = %d]\n", p->WeightMin );
+    Abc_Print( -2, "\t-M <num> : upper bound on literal count of divisors to extract [default = %d]\n", p->LitCountMax );
     Abc_Print( -2, "\t-s       : use only single-cube divisors [default = %s]\n", p->fOnlyS? "yes": "no" );
     Abc_Print( -2, "\t-d       : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" );
     Abc_Print( -2, "\t-z       : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" );
diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c
index 953f87f3..83136118 100644
--- a/src/base/abci/abcFx.c
+++ b/src/base/abci/abcFx.c
@@ -87,6 +87,7 @@ struct Fx_Man_t_
 {
     // user's data
     Vec_Wec_t *     vCubes;     // cube -> lit
+    int             LitCountMax;// max size of divisor to extract
     // internal data
     Vec_Wec_t *     vLits;      // lit -> cube
     Vec_Int_t *     vCounts;    // literal counts (currently not used)
@@ -141,7 +142,6 @@ Vec_Wec_t * Abc_NtkFxRetrieve( Abc_Ntk_t * pNtk )
     char * pCube, * pSop;
     int nVars, i, v, Lit;
     assert( Abc_NtkIsSopLogic(pNtk) );
-    Abc_NtkMakeLegit( pNtk );
     vCubes = Vec_WecAlloc( 1000 );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
@@ -300,9 +300,9 @@ int Abc_NtkFxCheck( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int fVerbose )
+int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int LitCountMax, int fVerbose )
 {
-    extern int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int fVerbose );
+    extern int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fVerbose );
     Vec_Wec_t * vCubes;
     assert( Abc_NtkIsSopLogic(pNtk) );
     // check unique fanins
@@ -314,10 +314,12 @@ int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int fVerbose )
     // sweep removes useless nodes
     Abc_NtkCleanup( pNtk, 0 );
 //    Abc_NtkOrderFanins( pNtk );
+    // makes sure the SOPs are SCC-free and D1C-free
+    Abc_NtkMakeLegit( pNtk );
     // collect information about the covers
     vCubes = Abc_NtkFxRetrieve( pNtk );
     // call the fast extract procedure
-    if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), nNewNodesMax, fVerbose ) > 0 )
+    if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), nNewNodesMax, LitCountMax, fVerbose ) > 0 )
     {
         // update the network
         Abc_NtkFxInsert( pNtk, vCubes );
@@ -792,6 +794,8 @@ void Fx_ManCubeDoubleCubeDivisors( Fx_Man_t * p, int iFirst, Vec_Int_t * vPivot,
             else
                 p->nDivMux[2]++;
         }
+        if ( p->LitCountMax && p->LitCountMax < Vec_IntSize(p->vCubeFree) )
+            continue;
         iDiv = Hsh_VecManAdd( p->pHash, p->vCubeFree );
         if ( !fRemove )
         {
@@ -1107,7 +1111,7 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv )
   SeeAlso     []
 
 ***********************************************************************/
-int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int fVerbose )
+int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fVerbose )
 {
     int fVeryVerbose = 0;
     int i, iDiv;
@@ -1115,6 +1119,7 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int fVer
     clock_t clk = clock();
     // initialize the data-structure
     p = Fx_ManStart( vCubes );
+    p->LitCountMax = LitCountMax;
     Fx_ManCreateLiterals( p, ObjIdMax );
     Fx_ManCreateDivisors( p );
     if ( fVeryVerbose )
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index b2a56a7d..b0106636 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -55,7 +55,8 @@ void Abc_NtkSetDefaultParams( Fxu_Data_t * p )
     p->nSingleMax =  20000;
     p->nPairsMax  =  30000;
     p->nNodesExt  = 100000;
-    p->WeightMax  =      0;
+    p->WeightMin  =      0;
+    p->LitCountMax=      0;
     p->fOnlyS     =      0;
     p->fOnlyD     =      0;
     p->fUse0      =      0;
diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
index 0095abf9..2b078120 100644
--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@@ -83,7 +83,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
             Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
             if ( pData->fVerbose )
                 printf( "Div %5d : Best single = %5d.%s", Counter++, Weight1, fScrollLines?"\n":"\r" );
-            if ( Weight1 > pData->WeightMax || (Weight1 == 0 && pData->fUse0) )
+            if ( Weight1 > pData->WeightMin || (Weight1 == 0 && pData->fUse0) )
                 Fxu_UpdateSingle( p );
             else
                 break;
@@ -98,7 +98,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
             Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
             if ( pData->fVerbose )
                 printf( "Div %5d : Best double = %5d.%s", Counter++, Weight2, fScrollLines?"\n":"\r" );
-            if ( Weight2 > pData->WeightMax || (Weight2 == 0 && pData->fUse0) )
+            if ( Weight2 > pData->WeightMin || (Weight2 == 0 && pData->fUse0) )
                 Fxu_UpdateDouble( p );
             else
                 break;
@@ -119,14 +119,14 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
 
             if ( Weight1 >= Weight2 )
             {
-                if ( Weight1 > pData->WeightMax || (Weight1 == 0 && pData->fUse0) )
+                if ( Weight1 > pData->WeightMin || (Weight1 == 0 && pData->fUse0) )
                     Fxu_UpdateSingle( p );
                 else
                     break;
             }
             else
             {
-                if ( Weight2 > pData->WeightMax || (Weight2 == 0 && pData->fUse0) )
+                if ( Weight2 > pData->WeightMin || (Weight2 == 0 && pData->fUse0) )
                     Fxu_UpdateDouble( p );
                 else
                     break;
@@ -148,7 +148,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
                 printf( "Div %5d : Best double = %5d. Best single = %5d. Best complement = %5d.%s", 
                     Counter++, Weight2, Weight1, Weight3, fScrollLines?"\n":"\r" );
 
-            if ( Weight3 > pData->WeightMax || (Weight3 == 0 && pData->fUse0) )
+            if ( Weight3 > pData->WeightMin || (Weight3 == 0 && pData->fUse0) )
                 Fxu_Update( p, pSingle, pDouble );
             else
                 break;
diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h
index 3c6384dc..e8ef6586 100644
--- a/src/opt/fxu/fxu.h
+++ b/src/opt/fxu/fxu.h
@@ -53,7 +53,8 @@ struct FxuDataStruct
     int               nNodesExt;        // the number of divisors to extract
     int               nSingleMax;       // the max number of single-cube divisors to consider
     int               nPairsMax;        // the max number of double-cube divisors to consider
-    int               WeightMax;        // the max weight of a divisor to extract
+    int               WeightMin;        // the min weight of a divisor to extract
+    int               LitCountMax;      // the max literal count of a divisor to consider
     // 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