Version abc80130_2

14 files changed, 215 insertions, 56 deletions

diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
index 46f7ca1a..d11fd793 100644
--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@@ -17,7 +17,6 @@
 ***********************************************************************/
 
 #include "fxuInt.h" 
-//#include "mvc.h"
 #include "fxu.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -32,7 +31,7 @@ static int s_MemoryTotal;
 static int s_MemoryPeak;
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -59,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;
@@ -78,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
@@ -93,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
@@ -110,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 )
@@ -141,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 );
@@ -153,13 +153,14 @@ 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 )
         Fxu_CreateCovers( p, pData );
     Fxu_MatrixDelete( p );
-//    printf( "Memory usage after delocation:   Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
+//    printf( "Memory usage after deallocation:   Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
     if ( pData->nNodesNew == pData->nNodesExt )
         printf( "Warning: The limit on the number of extracted divisors has been reached.\n" );
     return pData->nNodesNew;
diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h
index e9f63ea3..e6d0b69e 100644
--- a/src/opt/fxu/fxu.h
+++ b/src/opt/fxu/fxu.h
@@ -19,6 +19,10 @@
 #ifndef __FXU_H__
 #define __FXU_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -33,9 +37,11 @@
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifndef __cplusplus
 #ifndef bool
 #define bool int
 #endif
+#endif
 
 typedef struct FxuDataStruct   Fxu_Data_t;
 
@@ -49,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
@@ -64,19 +71,23 @@ struct FxuDataStruct
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFITIONS                            ///
+///                       MACRO DEFINITIONS                          ///
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /*===== fxu.c ==========================================================*/
 extern int          Fxu_FastExtract( Fxu_Data_t * pData );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index b061f53d..55026b27 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -24,16 +24,16 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void        Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Fan_t * vFanins, int * pOrder );
+static void        Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder );
 static int         Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY );
 static void        Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext );
 static Fxu_Cube *  Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode );
-static Abc_Fan_t * s_pLits;
+static int * s_pLits;
 
 extern int         Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -53,7 +53,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
     Fxu_Var * pVar;
     Fxu_Cube * pCubeFirst, * pCubeNew;
     Fxu_Cube * pCube1, * pCube2;
-    Vec_Fan_t * vFanins;
+    Vec_Int_t * vFanins;
     char * pSopCover;
     char * pSopCube;
     int * pOrder, nBitsMax;
@@ -69,7 +69,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
     nCubesTotal =  0;
     nPairsTotal =  0;
     nPairsStore =  0;
-    nBitsMax    = -1;
+    nBitsMax    = -1; 
     for ( i = 0; i < pData->nNodesOld; i++ )
         if ( pSopCover = pData->vSops->pArray[i] )
         {
@@ -89,7 +89,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
         return NULL;
     }
 
-    if ( nPairsStore > 10000000 )
+    if ( nPairsStore > 50000000 )
     {
         printf( "The problem is too large to be solved by \"fxu\" (%d cubes and %d cube pairs)\n", nCubesTotal, nPairsStore );
         return NULL;
@@ -151,7 +151,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
             pOrder[v] = v;
         // reorder the fanins
         qsort( (void *)pOrder, nFanins, sizeof(int),(int (*)(const void *, const void *))Fxu_CreateMatrixLitCompare);
-        assert( s_pLits[ pOrder[0] ].iFan < s_pLits[ pOrder[nFanins-1] ].iFan );
+        assert( s_pLits[ pOrder[0] ] < s_pLits[ pOrder[nFanins-1] ] );
         // create the corresponding cubes in the matrix
         pCubeFirst = NULL;
         c = 0;
@@ -178,11 +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 )
-        Fxu_PreprocessCubePairs( p, pData->vSops, 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 )
@@ -193,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 );
@@ -214,7 +228,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
   SeeAlso     []
 
 ***********************************************************************/
-void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Fan_t * vFanins, int * pOrder )
+void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder )
 {
     Fxu_Var * pVar;
     int Value, i;
@@ -224,12 +238,12 @@ void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube,
         Value = pSopCube[pOrder[i]];
         if ( Value == '0' )
         {
-            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]].iFan + 1 ];  // CST
+            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] + 1 ];  // CST
             Fxu_MatrixAddLiteral( p, pCube, pVar );
         }
         else if ( Value == '1' )
         {
-            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]].iFan ];  // CST
+            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] ];  // CST
             Fxu_MatrixAddLiteral( p, pCube, pVar );
         }
     }
@@ -409,7 +423,7 @@ Fxu_Cube * Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iV
 ***********************************************************************/
 int Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY )
 {
-    return s_pLits[*ptrX].iFan - s_pLits[*ptrY].iFan;
+    return s_pLits[*ptrX] - s_pLits[*ptrY];
 } 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/fxu/fxuHeapD.c b/src/opt/fxu/fxuHeapD.c
index 7c123249..c81ad818 100644
--- a/src/opt/fxu/fxuHeapD.c
+++ b/src/opt/fxu/fxuHeapD.c
@@ -38,7 +38,7 @@ static void Fxu_HeapDoubleMoveUp( Fxu_HeapDouble * p, Fxu_Double * pDiv );
 static void Fxu_HeapDoubleMoveDn( Fxu_HeapDouble * p, Fxu_Double * pDiv );  
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/fxu/fxuHeapS.c b/src/opt/fxu/fxuHeapS.c
index dbd66055..eaca8363 100644
--- a/src/opt/fxu/fxuHeapS.c
+++ b/src/opt/fxu/fxuHeapS.c
@@ -38,7 +38,7 @@ static void Fxu_HeapSingleMoveUp( Fxu_HeapSingle * p, Fxu_Single * pSingle );
 static void Fxu_HeapSingleMoveDn( Fxu_HeapSingle * p, Fxu_Single * pSingle );  
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h
index 59b2df6d..ea85cb79 100644
--- a/src/opt/fxu/fxuInt.h
+++ b/src/opt/fxu/fxuInt.h
@@ -23,7 +23,6 @@
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#include "util.h"
 #include "extra.h"
 #include "vec.h"
 
@@ -173,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;
@@ -272,7 +273,7 @@ struct FxuSingle // 7 words
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFITIONS                            ///
+///                       MACRO DEFINITIONS                          ///
 ////////////////////////////////////////////////////////////////////////
 
 // minimum/maximum
@@ -430,7 +431,7 @@ extern void Fxu_MatrixRingVarsUnmark( Fxu_Matrix * p );
 #endif
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /*===== fxu.c ====================================================*/
@@ -460,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 ====================================================*/
@@ -530,8 +531,9 @@ extern int          Fxu_HeapSingleReadMaxWeight( Fxu_HeapSingle * p );
 extern Fxu_Single * Fxu_HeapSingleReadMax( Fxu_HeapSingle * p );
 extern Fxu_Single * Fxu_HeapSingleGetMax( Fxu_HeapSingle * p );  
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         END OF FILE                              ///
 ////////////////////////////////////////////////////////////////////////
-#endif
 
diff --git a/src/opt/fxu/fxuList.c b/src/opt/fxu/fxuList.c
index bb081d80..52995804 100644
--- a/src/opt/fxu/fxuList.c
+++ b/src/opt/fxu/fxuList.c
@@ -23,7 +23,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 // matrix -> var
diff --git a/src/opt/fxu/fxuMatrix.c b/src/opt/fxu/fxuMatrix.c
index 503ba2f1..93ec7b90 100644
--- a/src/opt/fxu/fxuMatrix.c
+++ b/src/opt/fxu/fxuMatrix.c
@@ -25,7 +25,7 @@
 extern unsigned int Cudd_Prime( unsigned int p );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -130,7 +130,7 @@ void Fxu_MatrixDelete( Fxu_Matrix * p )
             MEM_FREE_FXU( p, Fxu_Var, 1, pVar );
     }
 #else
-    Extra_MmFixedStop( p->pMemMan, 0 );
+    Extra_MmFixedStop( p->pMemMan );
 #endif
 
     Vec_PtrFree( p->vPairs );
diff --git a/src/opt/fxu/fxuPair.c b/src/opt/fxu/fxuPair.c
index be6be5e9..3c031ce8 100644
--- a/src/opt/fxu/fxuPair.c
+++ b/src/opt/fxu/fxuPair.c
@@ -55,7 +55,7 @@ static s_Primes[MAX_PRIMES] =
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/fxu/fxuPrint.c b/src/opt/fxu/fxuPrint.c
index 2d25c0e9..232b109a 100644
--- a/src/opt/fxu/fxuPrint.c
+++ b/src/opt/fxu/fxuPrint.c
@@ -23,7 +23,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/fxu/fxuReduce.c b/src/opt/fxu/fxuReduce.c
index 652d807b..0ab8a157 100644
--- a/src/opt/fxu/fxuReduce.c
+++ b/src/opt/fxu/fxuReduce.c
@@ -27,7 +27,7 @@
 static int Fxu_CountPairDiffs( char * pCover, unsigned char pDiffs[] );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -90,6 +90,16 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
         pnPairCounters[ pnLitsDiff[k] ]++;
     // determine what pairs to take starting from the lower
     // so that there would be exactly pPairsMax pairs
+    if ( pnPairCounters[0] != 0 )
+    {
+        printf( "The SOPs of the nodes are not cube-free. Run \"bdd; sop\" before \"fx\".\n" );
+        return 0;
+    }
+    if ( pnPairCounters[1] != 0 )
+    {
+        printf( "The SOPs of the nodes are not SCC-free. Run \"bdd; sop\" before \"fx\".\n" );
+        return 0;
+    }
     assert( pnPairCounters[0] == 0 ); // otherwise, covers are not dup-free
     assert( pnPairCounters[1] == 0 ); // otherwise, covers are not SCC-free
     nSum = 0;
diff --git a/src/opt/fxu/fxuSelect.c b/src/opt/fxu/fxuSelect.c
index b56407a9..b9265487 100644
--- a/src/opt/fxu/fxuSelect.c
+++ b/src/opt/fxu/fxuSelect.c
@@ -37,7 +37,7 @@ void Fxu_MatrixGetDoubleVars( Fxu_Matrix * p, Fxu_Double * pDouble,
 
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/fxu/fxuSingle.c b/src/opt/fxu/fxuSingle.c
index 5af5c341..73d9a76c 100644
--- a/src/opt/fxu/fxuSingle.c
+++ b/src/opt/fxu/fxuSingle.c
@@ -17,13 +17,16 @@
 ***********************************************************************/
 
 #include "fxuInt.h"
+#include "vec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles );
+
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -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 4006bc76..274f79f6 100644
--- a/src/opt/fxu/fxuUpdate.c
+++ b/src/opt/fxu/fxuUpdate.c
@@ -37,7 +37,7 @@ static void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p );
 static void Fxu_UpdateAddNewSingles( Fxu_Matrix * p, Fxu_Var * pVar );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -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*************************************************************