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

3 files changed, 25 insertions, 11 deletions

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