Version abc50807

6 files changed, 46 insertions, 98 deletions

diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
index 4b95b5a5..46f7ca1a 100644
--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@@ -39,21 +39,14 @@ static int s_MemoryPeak;
 
   Synopsis    [Performs fast_extract on a set of covers.]
 
-  Description [All the covers are given in the array p->ppCovers. 
-  The resulting covers are returned in the array p->ppCoversNew.
-  The number of entries in both cover arrays is equal to the number
-  of all values in the current nodes plus the max expected number 
-  of extracted nodes (p->nValuesCi + p->nValuesInt + p->nValuesExtMax). 
-  The first p->nValuesCi entries, corresponding to the CI nodes, are NULL.
-  The next p->nValuesInt entries, corresponding to the int nodes, are covers
-  from which the divisors are extracted. The last p->nValuesExtMax entries  
-  are reserved for the new covers to be extracted. The number of extracted 
-  covers is returned. This number does not exceed the given number (p->nNodesExt). 
+  Description [All the covers are given in the array p->vSops. 
+  The resulting covers are returned in the array p->vSopsNew.
+  The entries in these arrays correspond to objects in the network.
+  The entries corresponding to the PI and objects with trivial covers are NULL.
+  The number of extracted covers (not exceeding p->nNodesExt) is returned. 
   Two other things are important for the correct operation of this procedure:
-  (1) The input covers should be SCC-free. (2) The literal array (pCover->pLits) 
-  is allocated in each cover. The i-th entry in the literal array of a cover
-  is the number of the cover in the array p->ppCovers, which represents this
-  literal (variable value) in the given cover.]
+  (1) The input covers do not have duplicated fanins and are SCC-free. 
+  (2) The fanins array contains the numbers of the fanin objects.]
                
   SideEffects []
 
diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h
index 5bc1e75f..e9f63ea3 100644
--- a/src/opt/fxu/fxu.h
+++ b/src/opt/fxu/fxu.h
@@ -48,37 +48,8 @@ struct FxuDataStruct
     bool              fUse0;            // set to 1 to have 0-weight also extracted
     bool              fUseCompl;        // set to 1 to have complement taken into account
     bool              fVerbose;         // set to 1 to have verbose output
-    int               nPairsMax;        // the maximum number of cube pairs to consider
-/*
-    // parameters of the network
-    int               fMvNetwork;       // the network has some MV nodes
-    // the information about nodes
-    int               nNodesCi;         // the number of CI nodes of the network
-    int               nNodesInt;        // the number of internal nodes of the network
-    int               nNodesOld;        // the number of CI and int nodes
-    int               nNodesNew;        // the number of added nodes
-    int               nNodesExt;        // the max number of (binary) nodes to be added by FX
-    int               nNodesAlloc;      // the total number of all nodes
-    int *             pNode2Value;      // for each node, the number of its first value
-    // the information about values
-    int               nValuesCi;        // the total number of values of CI nodes
-    int               nValuesInt;       // the total number of values of int nodes
-    int               nValuesOld;       // the number of CI and int values
-    int               nValuesNew;       // the number of values added nodes
-    int               nValuesExt;       // the total number of values of the added nodes
-    int               nValuesAlloc;     // the total number of all values of all nodes
-    int *             pValue2Node;      // for each value, the number of its node
-    // the information about covers
-    Mvc_Cover_t **    ppCovers;         // for each value, the corresponding cover
-    Mvc_Cover_t **    ppCoversNew;      // for each value, the corresponding cover after FX
-    // the MVC manager
-    Mvc_Manager_t *   pManMvc;
-*/
-    // statistics   
-    int               nNodesOld;        // the old number of nodes
     int               nNodesExt;        // the number of divisors to extract
-    int               nNodesNew;        // the number of divisors extracted
-
+    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
@@ -87,6 +58,9 @@ struct FxuDataStruct
     Vec_Ptr_t *       vFaninsNew;       // the fanins of each node in the network after extraction
     // the SOP manager
     Extra_MmFlex_t *  pManSop;
+    // statistics   
+    int               nNodesOld;        // the old number of nodes
+    int               nNodesNew;        // the number of divisors actually extracted
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index 04b23fce..b061f53d 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -24,21 +24,21 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern int         Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax );
-
 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 Abc_Fan_t * s_pLits;
 
+extern int         Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Creates the sparse matrix from the array of Sop covers.]
+  Synopsis    [Creates the sparse matrix from the array of SOPs.]
 
   Description []
                
@@ -53,6 +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;
     char * pSopCover;
     char * pSopCube;
     int * pOrder, nBitsMax;
@@ -63,12 +64,11 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
     int nCubes;
     int iCube, iPair;
     int nFanins;
-    Vec_Fan_t * vFanins;
 
     // collect all sorts of statistics
-    nCubesTotal = 0;
-    nPairsTotal = 0;
-    nPairsStore = 0;
+    nCubesTotal =  0;
+    nPairsTotal =  0;
+    nPairsStore =  0;
     nBitsMax    = -1;
     for ( i = 0; i < pData->nNodesOld; i++ )
         if ( pSopCover = pData->vSops->pArray[i] )
@@ -158,12 +158,11 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
         Abc_SopForEachCube( pSopCover, nFanins, pSopCube )
         {
             // create the cube
-            pCubeNew = Fxu_MatrixAddCube( p, pVar, c );
+            pCubeNew = Fxu_MatrixAddCube( p, pVar, c++ );
             Fxu_CreateMatrixAddCube( p, pCubeNew, pSopCube, vFanins, pOrder );
             if ( pCubeFirst == NULL )
                 pCubeFirst = pCubeNew;
             pCubeNew->pFirst = pCubeFirst;
-            c++;
         }
         // set the first cube of this var
         pVar->pFirst = pCubeFirst;
@@ -185,10 +184,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
     // add the var pairs to the heap
     Fxu_MatrixComputeSingles( p );
 
-    // allocate temporary storage for pairs
-    if ( pData->nPairsMax < 1000 )
-        pData->nPairsMax = 1000;
-    p->pPairsTemp = ALLOC( Fxu_Pair *, pData->nPairsMax * 10 + 100 );
+    // print stats
     if ( pData->fVerbose )
     {
         double Density;
@@ -254,8 +250,8 @@ void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube,
 void Fxu_CreateCovers( Fxu_Matrix * p, Fxu_Data_t * pData )
 {
     Fxu_Cube * pCube, * pCubeFirst, * pCubeNext;
-    int iNode, n;
     char * pSopCover;
+    int iNode, n;
 
     // get the first cube of the first internal node 
     pCubeFirst = Fxu_CreateCoversFirstCube( p, pData, 0 );
@@ -306,13 +302,11 @@ void Fxu_CreateCovers( Fxu_Matrix * p, Fxu_Data_t * pData )
 void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext )
 {
     Vec_Int_t * vInputsNew;
-    char * pSopCover;
-    char * pSopCube;
+    char * pSopCover, * pSopCube;
     Fxu_Var * pVar;
     Fxu_Cube * pCube;
     Fxu_Lit * pLit;
     int iNum, nCubes, v;
-    int fEmptyCube;
 
     // collect positive polarity variable in the cubes between pCubeFirst and pCubeNext
     Fxu_MatrixRingVarsStart( p );
@@ -362,7 +356,6 @@ void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cu
         // get hold of the SOP cube
         pSopCube = pSopCover + nCubes * (vInputsNew->nSize + 3);
         // insert literals
-        fEmptyCube = 1;
         for ( pLit = pCube->lLits.pHead; pLit; pLit = pLit->pHNext )
         {
             iNum = pLit->pVar->lLits.nItems; // hack - reuse lLits.nItems
@@ -371,14 +364,13 @@ void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cu
                 pSopCube[iNum] = (pLit->pVar->iVar & 1)? '0' : '1';   // reverse CST
             else
                 pSopCube[iNum] = (pLit->pVar->iVar & 1)? '1' : '0';   // no CST
-            fEmptyCube = 0;
         }
-        assert( !fEmptyCube );
         // count the cube
         nCubes++;
     }
     assert( nCubes == Abc_SopGetCubeNum(pSopCover) );
 
+    // set the new cover and the array of fanins
     pData->vSopsNew->pArray[iNode]   = pSopCover;
     pData->vFaninsNew->pArray[iNode] = vInputsNew;
 }
diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h
index 1f5a19b8..59b2df6d 100644
--- a/src/opt/fxu/fxuInt.h
+++ b/src/opt/fxu/fxuInt.h
@@ -25,6 +25,7 @@
 
 #include "util.h"
 #include "extra.h"
+#include "vec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -158,9 +159,6 @@ struct FxuHeapSingle
 // sparse matrix
 struct FxuMatrix // ~ 30 words
 {
-    // information about the network
-//    int              fMvNetwork;  // set to 1 if the network has MV nodes
-//    int *            pValue2Node; // the mapping of values into nodes
     // the cubes
     Fxu_ListCube     lCubes;      // the double linked list of cubes
     // the values (binary literals)
@@ -185,9 +183,7 @@ struct FxuMatrix // ~ 30 words
     Fxu_Var *        pOrderVars;
     Fxu_Var **       ppTailVars;
     // temporary storage for pairs
-    Fxu_Pair **      pPairsTemp;
-    int              nPairsTemp;
-//    int              nPairsMax;
+    Vec_Ptr_t *      vPairs;
     // statistics
     int              nEntries;    // the total number of entries in the sparse matrix
     int              nDivs1;      // the single cube divisors taken
diff --git a/src/opt/fxu/fxuMatrix.c b/src/opt/fxu/fxuMatrix.c
index 0b732aef..503ba2f1 100644
--- a/src/opt/fxu/fxuMatrix.c
+++ b/src/opt/fxu/fxuMatrix.c
@@ -77,6 +77,7 @@ Fxu_Matrix * Fxu_MatrixAllocate()
 #endif
     p->pHeapDouble = Fxu_HeapDoubleStart();
     p->pHeapSingle = Fxu_HeapSingleStart();
+    p->vPairs = Vec_PtrAlloc( 100 );
     return p;
 }
 
@@ -132,9 +133,10 @@ void Fxu_MatrixDelete( Fxu_Matrix * p )
     Extra_MmFixedStop( p->pMemMan, 0 );
 #endif
 
+    Vec_PtrFree( p->vPairs );
     FREE( p->pppPairs );
     FREE( p->ppPairs );
-    FREE( p->pPairsTemp );
+//    FREE( p->pPairsTemp );
     FREE( p->pTable );
     FREE( p->ppVars );
     FREE( p );
@@ -305,20 +307,8 @@ void Fxu_MatrixAddDivisor( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2
 
     // canonicize the pair
     Fxu_PairCanonicize( &pCube1, &pCube2 );
-
-/*
     // compute the hash key
-    if ( p->fMvNetwork )
-//    if ( 0 )
-    {   // in case of MV network, if all the values in the cube-free divisor
-        // belong to the same MV variable, this cube pair is not a divisor
-        Key = Fxu_PairHashKeyMv( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );
-        if ( Key == 0 )
-            return;
-    }
-    else
-*/
-        Key = Fxu_PairHashKey( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );
+    Key = Fxu_PairHashKey( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );
 
     // create the cube pair
     pPair = Fxu_PairAlloc( p, pCube1, pCube2 );
@@ -330,11 +320,13 @@ void Fxu_MatrixAddDivisor( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2
     fFound = 0;
     Key %= p->nTableSize;
     Fxu_TableForEachDouble( p, Key, pDiv )
+    {
         if ( Fxu_PairCompare( pPair, pDiv->lPairs.pTail ) ) // they are equal
         {
             fFound = 1;
             break;
         }
+    }
 
     if ( !fFound )
     {   // create the new divisor
diff --git a/src/opt/fxu/fxuUpdate.c b/src/opt/fxu/fxuUpdate.c
index b781e0b1..4006bc76 100644
--- a/src/opt/fxu/fxuUpdate.c
+++ b/src/opt/fxu/fxuUpdate.c
@@ -287,10 +287,12 @@ void Fxu_UpdateDoublePairs( Fxu_Matrix * p, Fxu_Double * pDouble, Fxu_Var * pVar
 
     // collect and sort the pairs
     Fxu_UpdatePairsSort( p, pDouble );
-    for ( i = 0; i < p->nPairsTemp; i++ )
+//    for ( i = 0; i < p->nPairsTemp; i++ )
+    for ( i = 0; i < p->vPairs->nSize; i++ )
     {
         // get the pair
-        pPair = p->pPairsTemp[i];
+//        pPair = p->pPairsTemp[i];
+        pPair = p->vPairs->pArray[i];
         // out of the two cubes, select the one which comes earlier
         pCubeUse = Fxu_PairMinCube( pPair );
         pCubeRem = Fxu_PairMaxCube( pPair );
@@ -312,7 +314,7 @@ void Fxu_UpdateDoublePairs( Fxu_Matrix * p, Fxu_Double * pDouble, Fxu_Var * pVar
         // remove the pair
         MEM_FREE_FXU( p, Fxu_Pair, 1, pPair );
     }
-    p->nPairsTemp = 0;
+    p->vPairs->nSize = 0;
 }
 
 /**Function*************************************************************
@@ -575,18 +577,17 @@ void Fxu_UpdateMatrixSingleClean( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVa
 void Fxu_UpdatePairsSort( Fxu_Matrix * p, Fxu_Double * pDouble )
 {
     Fxu_Pair * pPair;
-    // order the pairs by the first cube to ensure that 
-    // new literals are added to the matrix from top to bottom
-    // collect pairs into the array
-    p->nPairsTemp = 0;
+    // order the pairs by the first cube to ensure that new literals are added 
+    // to the matrix from top to bottom - collect pairs into the array
+    p->vPairs->nSize = 0;
     Fxu_DoubleForEachPair( pDouble, pPair )
-        p->pPairsTemp[ p->nPairsTemp++ ] = pPair;
-    if ( p->nPairsTemp > 1 )
-    {   // sort
-        qsort( (void *)p->pPairsTemp, p->nPairsTemp, sizeof(Fxu_Pair *), 
-            (int (*)(const void *, const void *)) Fxu_UpdatePairCompare );
-        assert( Fxu_UpdatePairCompare( p->pPairsTemp, p->pPairsTemp + p->nPairsTemp - 1 ) < 0 );
-    }
+        Vec_PtrPush( p->vPairs, pPair );
+    if ( p->vPairs->nSize < 2 )
+        return;
+    // sort
+    qsort( (void *)p->vPairs->pArray, p->vPairs->nSize, sizeof(Fxu_Pair *), 
+        (int (*)(const void *, const void *)) Fxu_UpdatePairCompare );
+    assert( Fxu_UpdatePairCompare( (Fxu_Pair**)p->vPairs->pArray, (Fxu_Pair**)p->vPairs->pArray + p->vPairs->nSize - 1 ) < 0 );
 }
 
 /**Function*************************************************************