Adding switch '-W' to fx to control the quality of extracted divisors.

4 files changed, 41 insertions, 15 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 862288fd..f935506d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3426,19 +3426,19 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Abc_NtkFxuFreeInfo( Fxu_Data_t * p );
 
     // allocate the structure
-    p = ABC_ALLOC( Fxu_Data_t, 1 );
-    memset( p, 0, sizeof(Fxu_Data_t) );
+    p = ABC_CALLOC( Fxu_Data_t, 1 );
     // set the defaults
     p->nSingleMax = 20000;
     p->nPairsMax  = 30000;
     p->nNodesExt  = 10000;
+    p->WeightMax  = 0;
     p->fOnlyS     = 0;
     p->fOnlyD     = 0;
     p->fUse0      = 0;
     p->fUseCompl  = 1;
     p->fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "SDNsdzcvh")) != EOF ) 
+    while ( (c = Extra_UtilGetopt(argc, argv, "SDNWsdzcvh")) != EOF ) 
     {
         switch (c) 
         {
@@ -3475,6 +3475,17 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
                 if ( p->nNodesExt < 0 ) 
                     goto usage;
                 break;
+            case 'W':
+                if ( globalUtilOptind >= argc )
+                {
+                    Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                    goto usage;
+                }
+                p->WeightMax = atoi(argv[globalUtilOptind]);
+                globalUtilOptind++;
+                if ( p->WeightMax < 0 ) 
+                    goto usage;
+                break;
             case 's':
                 p->fOnlyS ^= 1;
                 break;
@@ -3526,11 +3537,12 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: fx [-SDN <num>] [-sdzcvh]\n");
+    Abc_Print( -2, "usage: fx [-SDNW <num>] [-sdzcvh]\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> : the maximum number of divisors to extract [default = %d]\n", p->nNodesExt );  
+    Abc_Print( -2, "\t-W <num> : only extract divisors with weight more than this [default = %d]\n", p->nSingleMax );  
     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/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
index 264a7898..95f1c99d 100644
--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@@ -57,6 +57,7 @@ static int s_MemoryPeak;
 ***********************************************************************/
 int Fxu_FastExtract( Fxu_Data_t * pData )
 {
+    int fScrollLines = 1;
     Fxu_Matrix * p;
     Fxu_Single * pSingle;
     Fxu_Double * pDouble;
@@ -81,8 +82,8 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
         {
             Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
             if ( pData->fVerbose )
-                printf( "Div %5d : Best single = %5d.\r", Counter++, Weight1 );
-            if ( Weight1 > 0 || (Weight1 == 0 && pData->fUse0) )
+                printf( "Div %5d : Best single = %5d.%s", Counter++, Weight1, fScrollLines?"\n":"\r" );
+            if ( Weight1 > pData->WeightMax || (Weight1 == 0 && pData->fUse0) )
                 Fxu_UpdateSingle( p );
             else
                 break;
@@ -96,8 +97,8 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
         {
             Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
             if ( pData->fVerbose )
-                printf( "Div %5d : Best double = %5d.\r", Counter++, Weight2 );
-            if ( Weight2 > 0 || (Weight2 == 0 && pData->fUse0) )
+                printf( "Div %5d : Best double = %5d.%s", Counter++, Weight2, fScrollLines?"\n":"\r" );
+            if ( Weight2 > pData->WeightMax || (Weight2 == 0 && pData->fUse0) )
                 Fxu_UpdateDouble( p );
             else
                 break;
@@ -113,19 +114,19 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
             Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
 
             if ( pData->fVerbose )
-                printf( "Div %5d : Best double = %5d. Best single = %5d.\r", Counter++, Weight2, Weight1 );
+                printf( "Div %5d : Best double = %5d. Best single = %5d.%s", Counter++, Weight2, Weight1, fScrollLines?"\n":"\r" );
 //Fxu_Select( p, &pSingle, &pDouble );
 
             if ( Weight1 >= Weight2 )
             {
-                if ( Weight1 > 0 || (Weight1 == 0 && pData->fUse0) )
+                if ( Weight1 > pData->WeightMax || (Weight1 == 0 && pData->fUse0) )
                     Fxu_UpdateSingle( p );
                 else
                     break;
             }
             else
             {
-                if ( Weight2 > 0 || (Weight2 == 0 && pData->fUse0) )
+                if ( Weight2 > pData->WeightMax || (Weight2 == 0 && pData->fUse0) )
                     Fxu_UpdateDouble( p );
                 else
                     break;
@@ -144,10 +145,10 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
             // select the best single and double
             Weight3 = Fxu_Select( p, &pSingle, &pDouble );
             if ( pData->fVerbose )
-                printf( "Div %5d : Best double = %5d. Best single = %5d. Best complement = %5d.\r", 
-                    Counter++, Weight2, Weight1, Weight3 );
+                printf( "Div %5d : Best double = %5d. Best single = %5d. Best complement = %5d.%s", 
+                    Counter++, Weight2, Weight1, Weight3, fScrollLines?"\n":"\r" );
 
-            if ( Weight3 > 0 || (Weight3 == 0 && pData->fUse0) )
+            if ( Weight3 > pData->WeightMax || (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 282b1d2b..d42bf873 100644
--- a/src/opt/fxu/fxu.h
+++ b/src/opt/fxu/fxu.h
@@ -53,6 +53,7 @@ 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
     // 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
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index 76c534e3..31228dfd 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -188,7 +188,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
         printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
         printf( "that the user changes the network by reducing the size of logic node and\n" );
         printf( "consequently the number of cube pairs to be processed by this command.\n" );
-        printf( "One way to achieve this is to run the commands \"st; multi -m -F <num>\"\n" );
+        printf( "It can be achieved as follows: \"st; if -K <num>\" or \"st; renode -s -K <num>\"\n" );
         printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
         return NULL;
     }
@@ -198,6 +198,18 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
 //    if ( pData->fVerbose )
 //        printf( "Only %d best cube pairs will be used by the fast extract command.\n", pData->nPairsMax );
 
+    if ( p->lVars.nItems > 1000000 )
+    {
+        printf( "The total number of variables is more than 1,000,000.\n" );
+        printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
+        printf( "that the user changes the network by reducing the size of logic node and\n" );
+        printf( "consequently the number of cube pairs to be processed by this command.\n" );
+        printf( "It can be achieved as follows: \"st; if -K <num>\" or \"st; renode -s -K <num>\"\n" );
+        printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
+        return NULL;
+    }
+
+
     // add the var pairs to the heap
     Fxu_MatrixComputeSingles( p, pData->fUse0, pData->nSingleMax );