Version abc80130

14 files changed, 56 insertions, 215 deletions

diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
index d11fd793..46f7ca1a 100644
--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@@ -17,6 +17,7 @@
 ***********************************************************************/
 
 #include "fxuInt.h" 
+//#include "mvc.h"
 #include "fxu.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -31,7 +32,7 @@ static int s_MemoryTotal;
 static int s_MemoryPeak;
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -58,7 +59,6 @@ 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( "Div %5d : Best single = %5d.\r", Counter++, Weight1 );
+                printf( "Best single = %3d.\n", 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( "Div %5d : Best double = %5d.\r", Counter++, Weight2 );
+                printf( "Best double = %3d.\n", 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( "Div %5d : Best double = %5d. Best single = %5d.\r", Counter++, Weight2, Weight1 );
+                printf( "Best double = %3d. Best single = %3d.\n", 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( "Div %5d : Best double = %5d. Best single = %5d. Best complement = %5d.\r", 
-                    Counter++, Weight2, Weight1, Weight3 );
+                printf( "Best double = %3d. Best single = %3d. Best complement = %3d.\n", 
+                    Weight2, Weight1, Weight3 );
 
             if ( Weight3 > 0 || Weight3 == 0 && pData->fUse0 )
                 Fxu_Update( p, pSingle, pDouble );
@@ -153,14 +153,13 @@ 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 deallocation:   Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
+//    printf( "Memory usage after delocation:   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 e6d0b69e..e9f63ea3 100644
--- a/src/opt/fxu/fxu.h
+++ b/src/opt/fxu/fxu.h
@@ -19,10 +19,6 @@
 #ifndef __FXU_H__
 #define __FXU_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -37,11 +33,9 @@ extern "C" {
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifndef __cplusplus
 #ifndef bool
 #define bool int
 #endif
-#endif
 
 typedef struct FxuDataStruct   Fxu_Data_t;
 
@@ -55,8 +49,7 @@ 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               nSingleMax;       // the max number of single-cube divisors to consider
-    int               nPairsMax;        // the max number of double-cube divisors to consider
+    int               nPairsMax;        // the maximum number of cube pairs 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
@@ -71,23 +64,19 @@ struct FxuDataStruct
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
+///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /*===== 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 55026b27..b061f53d 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_Int_t * vFanins, int * pOrder );
+static void        Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Fan_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 int * s_pLits;
+static Abc_Fan_t * s_pLits;
 
 extern int         Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**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_Int_t * vFanins;
+    Vec_Fan_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 > 50000000 )
+    if ( nPairsStore > 10000000 )
     {
         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] ] < s_pLits[ pOrder[nFanins-1] ] );
+        assert( s_pLits[ pOrder[0] ].iFan < s_pLits[ pOrder[nFanins-1] ].iFan );
         // create the corresponding cubes in the matrix
         pCubeFirst = NULL;
         c = 0;
@@ -178,26 +178,11 @@ 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 );
+        Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax );
 
     // add the var pairs to the heap
-    Fxu_MatrixComputeSingles( p, pData->fUse0, pData->nSingleMax );
+    Fxu_MatrixComputeSingles( p );
 
     // print stats
     if ( pData->fVerbose )
@@ -208,8 +193,9 @@ 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 divs = %6d. (Total = %6d)  ",  p->lSingles.nItems, p->nSingleTotal );
-        fprintf( stdout, "2-cube divs = %6d. (Total = %6d)",  p->nDivsTotal, nPairsTotal );
+        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, "\n" );
     }
 //    Fxu_MatrixPrint( stdout, p );
@@ -228,7 +214,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
   SeeAlso     []
 
 ***********************************************************************/
-void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder )
+void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Fan_t * vFanins, int * pOrder )
 {
     Fxu_Var * pVar;
     int Value, i;
@@ -238,12 +224,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]] + 1 ];  // CST
+            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]].iFan + 1 ];  // CST
             Fxu_MatrixAddLiteral( p, pCube, pVar );
         }
         else if ( Value == '1' )
         {
-            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] ];  // CST
+            pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]].iFan ];  // CST
             Fxu_MatrixAddLiteral( p, pCube, pVar );
         }
     }
@@ -423,7 +409,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] - s_pLits[*ptrY];
+    return s_pLits[*ptrX].iFan - s_pLits[*ptrY].iFan;
 } 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/fxu/fxuHeapD.c b/src/opt/fxu/fxuHeapD.c
index c81ad818..7c123249 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/fxu/fxuHeapS.c b/src/opt/fxu/fxuHeapS.c
index eaca8363..dbd66055 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h
index ea85cb79..59b2df6d 100644
--- a/src/opt/fxu/fxuInt.h
+++ b/src/opt/fxu/fxuInt.h
@@ -23,6 +23,7 @@
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
+#include "util.h"
 #include "extra.h"
 #include "vec.h"
 
@@ -172,8 +173,6 @@ 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;
@@ -273,7 +272,7 @@ struct FxuSingle // 7 words
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
+///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
 // minimum/maximum
@@ -431,7 +430,7 @@ extern void Fxu_MatrixRingVarsUnmark( Fxu_Matrix * p );
 #endif
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /*===== fxu.c ====================================================*/
@@ -461,7 +460,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, int fUse0, int nSingleMax );
+extern void         Fxu_MatrixComputeSingles( Fxu_Matrix * p );
 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 ====================================================*/
@@ -531,9 +530,8 @@ 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 52995804..bb081d80 100644
--- a/src/opt/fxu/fxuList.c
+++ b/src/opt/fxu/fxuList.c
@@ -23,7 +23,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 // matrix -> var
diff --git a/src/opt/fxu/fxuMatrix.c b/src/opt/fxu/fxuMatrix.c
index 93ec7b90..503ba2f1 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -130,7 +130,7 @@ void Fxu_MatrixDelete( Fxu_Matrix * p )
             MEM_FREE_FXU( p, Fxu_Var, 1, pVar );
     }
 #else
-    Extra_MmFixedStop( p->pMemMan );
+    Extra_MmFixedStop( p->pMemMan, 0 );
 #endif
 
     Vec_PtrFree( p->vPairs );
diff --git a/src/opt/fxu/fxuPair.c b/src/opt/fxu/fxuPair.c
index 3c031ce8..be6be5e9 100644
--- a/src/opt/fxu/fxuPair.c
+++ b/src/opt/fxu/fxuPair.c
@@ -55,7 +55,7 @@ static s_Primes[MAX_PRIMES] =
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/fxu/fxuPrint.c b/src/opt/fxu/fxuPrint.c
index 232b109a..2d25c0e9 100644
--- a/src/opt/fxu/fxuPrint.c
+++ b/src/opt/fxu/fxuPrint.c
@@ -23,7 +23,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/fxu/fxuReduce.c b/src/opt/fxu/fxuReduce.c
index 0ab8a157..652d807b 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -90,16 +90,6 @@ 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 b9265487..b56407a9 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/fxu/fxuSingle.c b/src/opt/fxu/fxuSingle.c
index 73d9a76c..5af5c341 100644
--- a/src/opt/fxu/fxuSingle.c
+++ b/src/opt/fxu/fxuSingle.c
@@ -17,16 +17,13 @@
 ***********************************************************************/
 
 #include "fxuInt.h"
-#include "vec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles );
-
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -41,130 +38,12 @@ static void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar,
   SeeAlso     []
 
 ***********************************************************************/
-void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax )
+void Fxu_MatrixComputeSingles( Fxu_Matrix * p )
 {
     Fxu_Var * pVar;
-    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 );
+    // iterate through the columns in the matrix
     Fxu_MatrixForEachVariable( 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 );
+        Fxu_MatrixComputeSinglesOne( p, pVar );
 }
 
 /**Function*************************************************************
@@ -180,9 +59,12 @@ void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr
 ***********************************************************************/
 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
@@ -194,6 +76,7 @@ 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;
@@ -209,17 +92,16 @@ 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;
-        // peformance fix (August 24, 2007)
-//        if ( WeightCur >= 0 )
-//        Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
-        if ( WeightCur >= p->nWeightLimit )
+        if ( WeightCur >= 0 )
             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 274f79f6..4006bc76 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -757,14 +757,12 @@ 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 )
@@ -780,7 +778,6 @@ void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p )
             }
         }
     }
-//    printf( "Called procedure %d times.\n", Counter );
 }
 
 /**Function*************************************************************