Version abc70828

6 files changed, 161 insertions, 22 deletions

diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
index a92ef934..d11fd793 100644
--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@@ -58,6 +58,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
     Fxu_Single * pSingle;
     Fxu_Double * pDouble;
     int Weight1, Weight2, Weight3;
+    int Counter = 0;
 
     s_MemoryTotal = 0;
     s_MemoryPeak  = 0;
@@ -77,7 +78,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
         {
             Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
             if ( pData->fVerbose )
-                printf( "Best single = %3d.\n", Weight1 );
+                printf( "Div %5d : Best single = %5d.\r", Counter++, Weight1 );
             if ( Weight1 > 0 || Weight1 == 0 && pData->fUse0 )
                 Fxu_UpdateSingle( p );
             else
@@ -92,7 +93,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
         {
             Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
             if ( pData->fVerbose )
-                printf( "Best double = %3d.\n", Weight2 );
+                printf( "Div %5d : Best double = %5d.\r", Counter++, Weight2 );
             if ( Weight2 > 0 || Weight2 == 0 && pData->fUse0 )
                 Fxu_UpdateDouble( p );
             else
@@ -109,7 +110,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
             Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
 
             if ( pData->fVerbose )
-                printf( "Best double = %3d. Best single = %3d.\n", Weight2, Weight1 );
+                printf( "Div %5d : Best double = %5d. Best single = %5d.\r", Counter++, Weight2, Weight1 );
 //Fxu_Select( p, &pSingle, &pDouble );
 
             if ( Weight1 >= Weight2 )
@@ -140,8 +141,8 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
             // select the best single and double
             Weight3 = Fxu_Select( p, &pSingle, &pDouble );
             if ( pData->fVerbose )
-                printf( "Best double = %3d. Best single = %3d. Best complement = %3d.\n", 
-                    Weight2, Weight1, Weight3 );
+                printf( "Div %5d : Best double = %5d. Best single = %5d. Best complement = %5d.\r", 
+                    Counter++, Weight2, Weight1, Weight3 );
 
             if ( Weight3 > 0 || Weight3 == 0 && pData->fUse0 )
                 Fxu_Update( p, pSingle, pDouble );
@@ -152,7 +153,8 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
     }
 
     if ( pData->fVerbose )
-        printf( "Total single = %3d. Total double = %3d. Total compl = %3d.\n", p->nDivs1, p->nDivs2, p->nDivs3 );
+        printf( "Total single = %3d. Total double = %3d. Total compl = %3d.                    \n", 
+        p->nDivs1, p->nDivs2, p->nDivs3 );
 
     // create the new covers
     if ( pData->nNodesNew )
diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h
index 7025d019..e6d0b69e 100644
--- a/src/opt/fxu/fxu.h
+++ b/src/opt/fxu/fxu.h
@@ -55,7 +55,8 @@ struct FxuDataStruct
     bool              fUseCompl;        // set to 1 to have complement taken into account
     bool              fVerbose;         // set to 1 to have verbose output
     int               nNodesExt;        // the number of divisors to extract
-    int               nPairsMax;        // the maximum number of cube pairs to consider
+    int               nSingleMax;       // the max number of single-cube divisors to consider
+    int               nPairsMax;        // the max number of double-cube divisors 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
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index 99942a88..e3300df9 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -178,12 +178,26 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
 
     // consider the case when cube pairs should be preprocessed
     // before adding them to the set of divisors
+//    if ( pData->fVerbose )
+//        printf( "The total number of cube pairs is %d.\n", nPairsTotal );
+    if ( nPairsTotal > 10000000 )
+    {
+        printf( "The total number of cube pairs of the network is more than 10,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( "One way to achieve this is to run the commands \"st; multi -m -F <num>\"\n" );
+        printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
+        return NULL;
+    }
     if ( nPairsTotal > pData->nPairsMax )
         if ( !Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax ) )
             return NULL;
+//    if ( pData->fVerbose )
+//        printf( "Only %d best cube pairs will be used by the fast extract command.\n", pData->nPairsMax );
 
     // add the var pairs to the heap
-    Fxu_MatrixComputeSingles( p );
+    Fxu_MatrixComputeSingles( p, pData->fUse0, pData->nSingleMax );
 
     // print stats
     if ( pData->fVerbose )
@@ -194,9 +208,8 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
             p->lVars.nItems, p->lCubes.nItems );
         fprintf( stdout, "Lits = %d  Density = %.5f%%\n", 
             p->nEntries, Density );
-        fprintf( stdout, "1-cube divisors = %6d.  ",  p->lSingles.nItems );
-        fprintf( stdout, "2-cube divisors = %6d.  ",  p->nDivsTotal );
-        fprintf( stdout, "Cube pairs = %6d.",    nPairsTotal );
+        fprintf( stdout, "1-cube divs = %6d. (Total = %6d)  ",  p->lSingles.nItems, p->nSingleTotal );
+        fprintf( stdout, "2-cube divs = %6d. (Total = %6d)",  p->nDivsTotal, nPairsTotal );
         fprintf( stdout, "\n" );
     }
 //    Fxu_MatrixPrint( stdout, p );
diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h
index 0ae1d79e..ea85cb79 100644
--- a/src/opt/fxu/fxuInt.h
+++ b/src/opt/fxu/fxuInt.h
@@ -172,6 +172,8 @@ struct FxuMatrix // ~ 30 words
     // the single cube divisors
     Fxu_ListSingle   lSingles;    // the linked list of single cube divisors  
     Fxu_HeapSingle * pHeapSingle; // the heap of variables by the number of literals in the matrix
+    int              nWeightLimit;// the limit on weight of single cube divisors collected
+    int              nSingleTotal;// the total number of single cube divisors
     // storage for cube pairs
     Fxu_Pair ***     pppPairs;
     Fxu_Pair **      ppPairs;
@@ -459,7 +461,7 @@ extern void         Fxu_PairClearStorage( Fxu_Cube * pCube );
 extern Fxu_Pair *   Fxu_PairAlloc( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 );
 extern void         Fxu_PairAdd( Fxu_Pair * pPair );
 /*===== fxuSingle.c ====================================================*/
-extern void         Fxu_MatrixComputeSingles( Fxu_Matrix * p );
+extern void         Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax );
 extern void         Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar );
 extern int          Fxu_SingleCountCoincidence( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2 );
 /*===== fxuMatrix.c ====================================================*/
diff --git a/src/opt/fxu/fxuSingle.c b/src/opt/fxu/fxuSingle.c
index be90e159..73d9a76c 100644
--- a/src/opt/fxu/fxuSingle.c
+++ b/src/opt/fxu/fxuSingle.c
@@ -17,11 +17,14 @@
 ***********************************************************************/
 
 #include "fxuInt.h"
+#include "vec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -38,12 +41,130 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Fxu_MatrixComputeSingles( Fxu_Matrix * p )
+void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax )
 {
     Fxu_Var * pVar;
-    // iterate through the columns in the matrix
+    Vec_Ptr_t * vSingles;
+    int i, k;
+    // set the weight limit
+    p->nWeightLimit = 1 - fUse0;
+    // iterate through columns in the matrix and collect single-cube divisors
+    vSingles = Vec_PtrAlloc( 10000 );
     Fxu_MatrixForEachVariable( p, pVar )
-        Fxu_MatrixComputeSinglesOne( p, pVar );
+        Fxu_MatrixComputeSinglesOneCollect( p, pVar, vSingles );
+    p->nSingleTotal = Vec_PtrSize(vSingles) / 3;
+    // check if divisors should be filtered
+    if ( Vec_PtrSize(vSingles) > nSingleMax )
+    {
+        int * pWeigtCounts, nDivCount, Weight, i, c;;
+        assert( Vec_PtrSize(vSingles) % 3 == 0 );
+        // count how many divisors have the given weight
+        pWeigtCounts = ALLOC( int, 1000 );
+        memset( pWeigtCounts, 0, sizeof(int) * 1000 );
+        for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
+        {
+            Weight = (int)Vec_PtrEntry(vSingles, i);
+            if ( Weight >= 999 )
+                pWeigtCounts[999]++;
+            else
+                pWeigtCounts[Weight]++;
+        }
+        // select the bound on the weight (above this bound, singles will be included)
+        nDivCount = 0;
+        for ( c = 999; c >= 0; c-- )
+        {
+            nDivCount += pWeigtCounts[c];
+            if ( nDivCount >= nSingleMax )
+                break;
+        }
+        free( pWeigtCounts );
+        // collect singles with the given costs
+        k = 0;
+        for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
+        {
+            Weight = (int)Vec_PtrEntry(vSingles, i);
+            if ( Weight < c )
+                continue;
+            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-2) );
+            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-1) );
+            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i) );
+            if ( k/3 == nSingleMax )
+                break;
+        }
+        Vec_PtrShrink( vSingles, k );
+        // adjust the weight limit
+        p->nWeightLimit = c;
+    }
+    // collect the selected divisors
+    assert( Vec_PtrSize(vSingles) % 3 == 0 );
+    for ( i = 0; i < Vec_PtrSize(vSingles); i += 3 )
+    {
+        Fxu_MatrixAddSingle( p, 
+            Vec_PtrEntry(vSingles,i), 
+            Vec_PtrEntry(vSingles,i+1), 
+            (int)Vec_PtrEntry(vSingles,i+2) );
+    }
+    Vec_PtrFree( vSingles );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the single-cube divisors associated with a new column.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles )
+{
+    Fxu_Lit * pLitV, * pLitH;
+    Fxu_Var * pVar2;
+    int Coin;
+    int WeightCur;
+
+    // start collecting the affected vars
+    Fxu_MatrixRingVarsStart( p );
+    // go through all the literals of this variable
+    for ( pLitV = pVar->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
+        // for this literal, go through all the horizontal literals
+        for ( pLitH = pLitV->pHPrev; pLitH; pLitH = pLitH->pHPrev )
+        {
+            // get another variable
+            pVar2 = pLitH->pVar;
+            // skip the var if it is already used
+            if ( pVar2->pOrder )
+                continue;
+            // skip the var if it belongs to the same node
+//            if ( pValue2Node[pVar->iVar] == pValue2Node[pVar2->iVar] )
+//                continue;
+            // collect the var
+            Fxu_MatrixRingVarsAdd( p, pVar2 );
+        }
+    // stop collecting the selected vars
+    Fxu_MatrixRingVarsStop( p );
+
+    // iterate through the selected vars
+    Fxu_MatrixForEachVarInRing( p, pVar2 )
+    {
+        // count the coincidence
+        Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
+        assert( Coin > 0 );
+        // get the new weight
+        WeightCur = Coin - 2;
+        // peformance fix (August 24, 2007)
+        if ( WeightCur >= p->nWeightLimit )
+        {
+            Vec_PtrPush( vSingles, pVar2 );
+            Vec_PtrPush( vSingles, pVar );
+            Vec_PtrPush( vSingles, (void *)WeightCur );
+        }
+    }
+
+    // unmark the vars
+    Fxu_MatrixRingVarsUnmark( p );
 }
 
 /**Function*************************************************************
@@ -59,12 +180,9 @@ void Fxu_MatrixComputeSingles( Fxu_Matrix * p )
 ***********************************************************************/
 void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
 {
-//    int * pValue2Node = p->pValue2Node;
     Fxu_Lit * pLitV, * pLitH;
     Fxu_Var * pVar2;
     int Coin;
-//    int CounterAll;
-//    int CounterTest;
     int WeightCur;
 
     // start collecting the affected vars
@@ -76,7 +194,6 @@ void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
         {
             // get another variable
             pVar2 = pLitH->pVar;
-//            CounterAll++;
             // skip the var if it is already used
             if ( pVar2->pOrder )
                 continue;
@@ -92,16 +209,17 @@ void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
     // iterate through the selected vars
     Fxu_MatrixForEachVarInRing( p, pVar2 )
     {
-//        CounterTest++;
         // count the coincidence
         Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
         assert( Coin > 0 );
         // get the new weight
         WeightCur = Coin - 2;
-        if ( WeightCur >= 0 )
+        // peformance fix (August 24, 2007)
+//        if ( WeightCur >= 0 )
+//        Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
+        if ( WeightCur >= p->nWeightLimit )
             Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
     }
-
     // unmark the vars
     Fxu_MatrixRingVarsUnmark( p );
 }
diff --git a/src/opt/fxu/fxuUpdate.c b/src/opt/fxu/fxuUpdate.c
index a430b9c1..274f79f6 100644
--- a/src/opt/fxu/fxuUpdate.c
+++ b/src/opt/fxu/fxuUpdate.c
@@ -757,12 +757,14 @@ void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p )
 { 
     Fxu_Single * pSingle, * pSingle2;
     int WeightNew;
+    int Counter = 0;
 
     Fxu_MatrixForEachSingleSafe( p, pSingle, pSingle2 )
     {
         // if at least one of the variables is marked, recalculate
         if ( pSingle->pVar1->pOrder || pSingle->pVar2->pOrder )
         {
+            Counter++;
             // get the new weight
             WeightNew = -2 + Fxu_SingleCountCoincidence( p, pSingle->pVar1, pSingle->pVar2 );
             if ( WeightNew >= 0 )
@@ -778,6 +780,7 @@ void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p )
             }
         }
     }
+//    printf( "Called procedure %d times.\n", Counter );
 }
 
 /**Function*************************************************************