Version abc51126

6 files changed, 278 insertions, 8 deletions

diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index f518e8c4..5c9b2e8e 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -69,6 +69,8 @@ struct Cut_CutStruct_t_
     unsigned           nVarsMax   :  4;   // the max number of vars [4-6]
     unsigned           nLeaves    :  4;   // the number of leaves [4-6]
     unsigned           uSign;             // the signature
+    unsigned           uCanon0;           // the canonical form 
+    unsigned           uCanon1;           // the canonical form 
     Cut_Cut_t *        pNext;             // the next cut in the list
     int                pLeaves[0];        // the array of leaves
 };
@@ -113,6 +115,7 @@ extern int              Cut_ManReadVarsMax( Cut_Man_t * p );
 /*=== cutNode.c ==========================================================*/
 extern Cut_Cut_t *      Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv ); 
 extern Cut_Cut_t *      Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes );
+extern Cut_Cut_t *      Cut_NodeUnionCutsSeq( Cut_Man_t * p, Vec_Int_t * vNodes, int CutSetNum, int fFirst );
 /*=== cutSeq.c ==========================================================*/
 extern void             Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int nLat0, int nLat1, int fTriv, int CutSetNum );
 extern void             Cut_NodeNewMergeWithOld( Cut_Man_t * p, int Node );
@@ -126,6 +129,8 @@ extern int              Cut_OracleReadDrop( Cut_Oracle_t * p );
 extern void             Cut_OracleNodeSetTriv( Cut_Oracle_t * p, int Node );
 extern Cut_Cut_t *      Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 );
 extern void             Cut_OracleTryDroppingCuts( Cut_Oracle_t * p, int Node );
+/*=== cutTruth.c ==========================================================*/
+extern void             Cut_TruthCanonicize( Cut_Cut_t * pCut );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index 80568d71..0268ba19 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -376,6 +376,7 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
     // start with the elementary cut
     if ( fTriv ) 
     {
+//        printf( "Creating trivial cut %d.\n", Node );
         pTemp0 = Cut_CutCreateTriv( p, Node );
         Cut_ListAdd( pSuper, pTemp0 );
         p->nNodeCuts++;
@@ -542,6 +543,189 @@ p->timeUnion += clock() - clk;
     return pList;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts by unioning cuts at a choice node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Cut_t * Cut_NodeUnionCutsSeq( Cut_Man_t * p, Vec_Int_t * vNodes, int CutSetNum, int fFirst )
+{
+    Cut_List_t Super, * pSuper = &Super;
+    Cut_Cut_t * pList, * pListStart, * pCut, * pCut2, * pTop;
+    int i, k, Node, Root, Limit = p->pParams->nVarsMax;
+    int clk = clock();
+
+    // start the new list
+    Cut_ListStart( pSuper );
+
+    // remember the root node to save the resulting cuts
+    Root = Vec_IntEntry( vNodes, 0 );
+    p->nNodeCuts = 1;
+
+    // store the original lists for comparison
+    p->pCompareOld = Cut_NodeReadCutsOld( p, Root );
+    p->pCompareNew = (CutSetNum >= 0)? Cut_NodeReadCutsNew( p, Root ) : NULL;
+
+    // get the topmost cut
+    pTop = NULL;
+    if ( (pTop = Cut_NodeReadCutsOld( p, Root )) == NULL )
+        pTop = Cut_NodeReadCutsNew( p, Root );
+    assert( pTop != NULL );
+
+    // collect small cuts first
+    Vec_PtrClear( p->vTemp );
+    Vec_IntForEachEntry( vNodes, Node, i )
+    {
+        // get the cuts of this node
+        if ( i == 0 && CutSetNum >= 0 )
+        {
+            pList = Cut_NodeReadCutsTemp( p, CutSetNum );
+            Cut_NodeWriteCutsTemp( p, CutSetNum, NULL );
+        }
+        else
+        {
+            pList = Cut_NodeReadCutsNew( p, Node );
+            Cut_NodeWriteCutsNew( p, Node, NULL );
+        }
+        if ( pList == NULL )
+            continue;
+
+        // process the cuts
+        if ( fFirst )
+        {
+            // remember the starting point
+            pListStart = pList->pNext;
+            pList->pNext = NULL;
+            // save or recycle the elementary cut
+            if ( i == 0 )
+                Cut_ListAdd( pSuper, pList );
+            else
+                Cut_CutRecycle( p, pList );
+        }
+        else
+            pListStart = pList;
+
+        // save all the cuts that are smaller than the limit
+        Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
+        {
+            if ( pCut->nLeaves == (unsigned)Limit )
+            {
+                Vec_PtrPush( p->vTemp, pCut );
+                break;
+            }
+            // check containment
+//            if ( p->pParams->fFilter && Cut_CutFilterOne( p, pSuper, pCut ) )
+//                continue;
+            if ( p->pParams->fFilter )
+            {
+                if ( Cut_CutFilterOne(p, pSuper, pCut) )
+                    continue;
+                if ( p->pParams->fSeq )
+                {
+                    if ( p->pCompareOld && Cut_CutFilterOld(p, p->pCompareOld, pCut) )
+                        continue;
+                    if ( p->pCompareNew && Cut_CutFilterOld(p, p->pCompareNew, pCut) )
+                        continue;
+                }
+            }
+
+            // set the complemented bit by comparing the first cut with the current cut
+            pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
+            pListStart = pCut->pNext;
+            pCut->pNext = NULL;
+            // add to the list
+            Cut_ListAdd( pSuper, pCut );
+            if ( ++p->nNodeCuts == p->pParams->nKeepMax )
+            {
+                // recycle the rest of the cuts of this node
+                Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
+                    Cut_CutRecycle( p, pCut );
+                // recycle all cuts of other nodes
+                Vec_IntForEachEntryStart( vNodes, Node, k, i+1 )
+                    Cut_NodeFreeCuts( p, Node );
+                // recycle the saved cuts of other nodes
+                Vec_PtrForEachEntry( p->vTemp, pList, k )
+                    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+                        Cut_CutRecycle( p, pCut );
+                goto finish;
+            }
+        }
+    } 
+    // collect larger cuts next
+    Vec_PtrForEachEntry( p->vTemp, pList, i )
+    {
+        Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+        {
+            // check containment
+//            if ( p->pParams->fFilter && Cut_CutFilterOne( p, pSuper, pCut ) )
+//                continue;
+            if ( p->pParams->fFilter )
+            {
+                if ( Cut_CutFilterOne(p, pSuper, pCut) )
+                    continue;
+                if ( p->pParams->fSeq )
+                {
+                    if ( p->pCompareOld && Cut_CutFilterOld(p, p->pCompareOld, pCut) )
+                        continue;
+                    if ( p->pCompareNew && Cut_CutFilterOld(p, p->pCompareNew, pCut) )
+                        continue;
+                }
+            }
+
+            // set the complemented bit
+            pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
+            pListStart   = pCut->pNext;
+            pCut->pNext  = NULL;
+            // add to the list
+            Cut_ListAdd( pSuper, pCut );
+            if ( ++p->nNodeCuts == p->pParams->nKeepMax )
+            {
+                // recycle the rest of the cuts
+                Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
+                    Cut_CutRecycle( p, pCut );
+                // recycle the saved cuts of other nodes
+                Vec_PtrForEachEntryStart( p->vTemp, pList, k, i+1 )
+                    Cut_ListForEachCutSafe( pList, pCut, pCut2 )
+                        Cut_CutRecycle( p, pCut );
+                goto finish;
+            }
+        }
+    }
+finish :
+    // set the cuts at the node
+    pList = Cut_ListFinish( pSuper );
+
+    // set the lists at the node
+//    assert( Cut_NodeReadCutsNew(p, Root) == NULL );
+//    Cut_NodeWriteCutsNew( p, Root, pList );
+    if ( CutSetNum >= 0 )
+    {
+        assert( Cut_NodeReadCutsTemp(p, CutSetNum) == NULL );
+        Cut_NodeWriteCutsTemp( p, CutSetNum, pList );
+    }
+    else
+    {
+        assert( Cut_NodeReadCutsNew(p, Root) == NULL );
+        Cut_NodeWriteCutsNew( p, Root, pList );
+    }
+
+p->timeUnion += clock() - clk;
+    // filter the cuts
+//clk = clock();
+//    if ( p->pParams->fFilter )
+//        Cut_CutFilter( p, pList );
+//p->timeFilter += clock() - clk;
+//    if ( fFirst )
+//        p->nNodes -= vNodes->nSize - 1;
+    return pList;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/opt/cut/cutTruth.c b/src/opt/cut/cutTruth.c
index 28984e5a..b65e5eff 100644
--- a/src/opt/cut/cutTruth.c
+++ b/src/opt/cut/cutTruth.c
@@ -107,6 +107,48 @@ void Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, i
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table computation.]
+
+  Description [This procedure cannot be used while recording oracle
+  because it will overwrite Num0 and Num1.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_TruthCanonicize( Cut_Cut_t * pCut )
+{
+    unsigned uTruth;
+    unsigned * uCanon2;
+    char * pPhases2;
+    assert( pCut->nVarsMax < 6 );
+
+    // get the direct truth table
+    uTruth = *Cut_CutReadTruth(pCut);
+
+    // compute the direct truth table
+    Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
+//    uCanon[0] = uCanon2[0];
+//    uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
+//    uPhases[0] = pPhases2[0];
+    pCut->uCanon0 = uCanon2[0];
+    pCut->Num0    = pPhases2[0];
+
+    // get the complemented truth table
+    uTruth = ~*Cut_CutReadTruth(pCut);
+
+    // compute the direct truth table
+    Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 );
+//    uCanon[0] = uCanon2[0];
+//    uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
+//    uPhases[0] = pPhases2[0];
+    pCut->uCanon1 = uCanon2[0];
+    pCut->Num1    = pPhases2[0];
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h
index aa2a7039..b6b2524b 100644
--- a/src/opt/dec/dec.h
+++ b/src/opt/dec/dec.h
@@ -96,6 +96,7 @@ struct Dec_Man_t_
 
 /*=== decAbc.c ========================================================*/
 extern Abc_Obj_t *    Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
+extern Abc_Obj_t *    Dec_GraphToNetworkNoStrash( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
 extern int            Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
 extern void           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
 /*=== decFactor.c ========================================================*/
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
index 6782a02f..1416cf0d 100644
--- a/src/opt/dec/decAbc.c
+++ b/src/opt/dec/decAbc.c
@@ -63,6 +63,44 @@ Abc_Obj_t * Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph )
 
 /**Function*************************************************************
 
+  Synopsis    [Transforms the decomposition graph into the AIG.]
+
+  Description [AIG nodes for the fanins should be assigned to pNode->pFunc
+  of the leaves of the graph before calling this procedure.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Dec_GraphToNetworkNoStrash( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph )
+{
+    Abc_Obj_t * pAnd, * pAnd0, * pAnd1;
+    Dec_Node_t * pNode;
+    int i;
+    // check for constant function
+    if ( Dec_GraphIsConst(pGraph) )
+        return Abc_ObjNotCond( Abc_NtkConst1(pNtk), Dec_GraphIsComplement(pGraph) );
+    // check for a literal
+    if ( Dec_GraphIsVar(pGraph) )
+        return Abc_ObjNotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
+    // build the AIG nodes corresponding to the AND gates of the graph
+    Dec_GraphForEachNode( pGraph, pNode, i )
+    {
+        pAnd0 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
+        pAnd1 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
+//        pNode->pFunc = Abc_AigAnd( pNtk->pManFunc, pAnd0, pAnd1 );
+        pAnd = Abc_NtkCreateNode( pNtk );
+        Abc_ObjAddFanin( pAnd, pAnd0 );
+        Abc_ObjAddFanin( pAnd, pAnd1 );
+        pNode->pFunc = pAnd;
+    }
+    // complement the result if necessary
+    return Abc_ObjNotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of new nodes added when using this graph.]
 
   Description [AIG nodes for the fanins should be assigned to pNode->pFunc 
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index 24b86c95..02b7605c 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -24,11 +24,11 @@
 ///                        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 );
 
@@ -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;
@@ -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;
@@ -214,7 +214,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 +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]].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 +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].iFan - s_pLits[*ptrY].iFan;
+    return s_pLits[*ptrX] - s_pLits[*ptrY];
 } 
 
 ////////////////////////////////////////////////////////////////////////