Version abc60220

9 files changed, 101 insertions, 33 deletions

diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index 5c9b2e8e..b724c976 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -30,7 +30,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #define CUT_SIZE_MIN    3      // the min K of the K-feasible cut computation
-#define CUT_SIZE_MAX    8      // the max K of the K-feasible cut computation
+#define CUT_SIZE_MAX   12      // the max K of the K-feasible cut computation
 
 #define CUT_SHIFT       8      // the number of bits for storing latch number in the cut leaves
 #define CUT_MASK        0xFF   // the mask to get the stored latch number
@@ -55,7 +55,7 @@ struct Cut_ParamsStruct_t_
     int                fFilter;           // filter dominated cuts
     int                fSeq;              // compute sequential cuts
     int                fDrop;             // drop cuts on the fly
-    int                fMulti;            // compute cuts in multi-input AND gate graph
+    int                fMulti;            // compute factor-cuts
     int                fRecord;           // record the cut computation flow
     int                fVerbose;          // the verbosiness flag
 };
@@ -105,6 +105,7 @@ extern void             Cut_NodeFreeCuts( Cut_Man_t * p, int Node );
 /*=== cutCut.c ==========================================================*/
 extern void             Cut_CutPrint( Cut_Cut_t * pCut, int fSeq );
 extern void             Cut_CutPrintList( Cut_Cut_t * pList, int fSeq );
+extern int              Cut_CutCountList( Cut_Cut_t * pList );
 /*=== cutMan.c ==========================================================*/
 extern Cut_Man_t *      Cut_ManStart( Cut_Params_t * pParams );
 extern void             Cut_ManStop( Cut_Man_t * p );
diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h
index 51ff07f9..eca2fcd5 100644
--- a/src/opt/cut/cutInt.h
+++ b/src/opt/cut/cutInt.h
@@ -80,6 +80,7 @@ struct Cut_ManStruct_t_
     int                nCutsLimit;
     int                nNodes;
     int                nNodesMulti;
+    int                nNodesMulti0;
     // runtime
     int                timeMerge;
     int                timeUnion;
@@ -122,7 +123,6 @@ extern void                Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut );
 extern int                 Cut_CutCompare( Cut_Cut_t * pCut1, Cut_Cut_t * pCut2 );
 extern Cut_Cut_t *         Cut_CutDupList( Cut_Man_t * p, Cut_Cut_t * pList );
 extern void                Cut_CutRecycleList( Cut_Man_t * p, Cut_Cut_t * pList );
-extern int                 Cut_CutCountList( Cut_Cut_t * pList );
 extern Cut_Cut_t *         Cut_CutMergeLists( Cut_Cut_t * pList1, Cut_Cut_t * pList2 ); 
 extern void                Cut_CutNumberList( Cut_Cut_t * pList );
 extern Cut_Cut_t *         Cut_CutCreateTriv( Cut_Man_t * p, int Node );
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index b2d62fce..8269da06 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -153,6 +153,15 @@ void Cut_ManPrintStats( Cut_Man_t * p )
     printf( "Cuts per node     = %8.1f\n", ((float)(p->nCutsCur-p->nCutsTriv))/p->nNodes );
     printf( "The cut size      = %8d bytes.\n", p->EntrySize );
     printf( "Peak memory       = %8.2f Mb.\n", (float)p->nCutsPeak * p->EntrySize / (1<<20) );
+    if ( p->pParams->fMulti )
+    {
+    printf( "Factor-cut computation statistics:\n" );
+    printf( "Total nodes       = %8d.\n", p->nNodes );
+    printf( "Factor nodes      = %8d.\n", p->nNodesMulti );
+    printf( "Factor nodes 0    = %8d.\n", p->nNodesMulti0 );
+    printf( "Factor cuts       = %8d.\n", p->nCutsMulti );
+    printf( "Cuts per node     = %8.1f\n", ((float)(p->nCutsMulti))/(p->nNodesMulti-p->nNodesMulti0) );
+    }
     PRT( "Merge ", p->timeMerge );
     PRT( "Union ", p->timeUnion );
     PRT( "Filter", p->timeFilter );
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index 0268ba19..cace83bd 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -355,10 +355,19 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
 {
     Cut_Cut_t * pStop0, * pStop1, * pTemp0, * pTemp1;
     int i, nCutsOld, Limit;
+    // 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++;
+    }
     // get the cut lists of children
     if ( pList0 == NULL || pList1 == NULL )
         return;
-    // start the new list
+
+    // remember the old number of cuts
     nCutsOld = p->nCutsCur;
     Limit = p->pParams->nVarsMax;
     // get the simultation bit of the node
@@ -373,15 +382,7 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
     Cut_ListForEachCut( pList1, pStop1 )
         if ( pStop1->nLeaves == (unsigned)Limit )
             break;
-    // 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++;
-        nCutsOld++;
-    }
+
     // small by small
     Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
     Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
@@ -424,6 +425,8 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
     {
         p->nCutsMulti += p->nCutsCur - nCutsOld;         
         p->nNodesMulti++;
+        if ( p->nCutsCur == nCutsOld )
+            p->nNodesMulti0++;
     }
 }
 
diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h
index b6b2524b..7b8b2e94 100644
--- a/src/opt/dec/dec.h
+++ b/src/opt/dec/dec.h
@@ -628,19 +628,75 @@ static inline Dec_Edge_t Dec_GraphAddNodeOr( Dec_Graph_t * pGraph, Dec_Edge_t eE
   SeeAlso     []
 
 ***********************************************************************/
-static inline Dec_Edge_t Dec_GraphAddNodeXor( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 )
-{
-    Dec_Edge_t eNode0, eNode1;
-    // derive the first AND
-    eEdge0.fCompl = !eEdge0.fCompl;
-    eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
-    eEdge0.fCompl = !eEdge0.fCompl;
-    // derive the second AND
-    eEdge1.fCompl = !eEdge1.fCompl;
-    eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
-    eEdge1.fCompl = !eEdge1.fCompl;
-    // derive the final OR
-    return Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
+static inline Dec_Edge_t Dec_GraphAddNodeXor( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1, int Type )
+{
+    Dec_Edge_t eNode0, eNode1, eNode;
+    if ( Type == 0 )
+    {
+        // derive the first AND
+        eEdge0.fCompl ^= 1;
+        eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
+        eEdge0.fCompl ^= 1;
+        // derive the second AND
+        eEdge1.fCompl ^= 1;
+        eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
+        // derive the final OR
+        eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
+    }
+    else
+    {
+        // derive the first AND
+        eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
+        // derive the second AND
+        eEdge0.fCompl ^= 1;
+        eEdge1.fCompl ^= 1;
+        eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
+        // derive the final OR
+        eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
+        eNode.fCompl ^= 1;
+    }
+    return eNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates an XOR node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Dec_Edge_t Dec_GraphAddNodeMux( Dec_Graph_t * pGraph, Dec_Edge_t eEdgeC, Dec_Edge_t eEdgeT, Dec_Edge_t eEdgeE, int Type )
+{
+    Dec_Edge_t eNode0, eNode1, eNode;
+    if ( Type == 0 )
+    {
+        // derive the first AND
+        eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
+        // derive the second AND
+        eEdgeC.fCompl ^= 1;
+        eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
+        // derive the final OR
+        eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
+    }
+    else
+    {
+        // complement the arguments
+        eEdgeT.fCompl ^= 1;
+        eEdgeE.fCompl ^= 1;
+        // derive the first AND
+        eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
+        // derive the second AND
+        eEdgeC.fCompl ^= 1;
+        eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
+        // derive the final OR
+        eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
+        eNode.fCompl ^= 1;
+    }
+    return eNode;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
index af76cd84..066b3bb2 100644
--- a/src/opt/dec/decAbc.c
+++ b/src/opt/dec/decAbc.c
@@ -18,7 +18,7 @@
 
 #include "abc.h"
 #include "dec.h"
-//#include "aig.h"
+#include "aig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -214,7 +214,6 @@ void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpda
   SeeAlso     []
 
 ***********************************************************************/
-/*
 Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
 {
     Dec_Node_t * pNode;
@@ -236,7 +235,7 @@ Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
     // complement the result if necessary
     return Aig_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
 }
-*/
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h
index 385cccef..d82a68db 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"
 
diff --git a/src/opt/rwr/rwrDec.c b/src/opt/rwr/rwrDec.c
index 45fcb02c..ef7af34f 100644
--- a/src/opt/rwr/rwrDec.c
+++ b/src/opt/rwr/rwrDec.c
@@ -135,7 +135,7 @@ Dec_Edge_t Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Dec_Graph_t *
         eNode1.fCompl = !eNode1.fCompl;
     // create the decomposition node(s)
     if ( pNode->fExor )
-        eNode = Dec_GraphAddNodeXor( pGraph, eNode0, eNode1 );
+        eNode = Dec_GraphAddNodeXor( pGraph, eNode0, eNode1, 0 );
     else
         eNode = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 );
     // save the result
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index 3f3163f1..71d0b24d 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -66,7 +66,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
     Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY;
     // get the node's cuts
 clk = clock();
-    pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode );
+    pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode, 0 );
     assert( pCut != NULL );
 p->timeCut += clock() - clk;
 
@@ -140,8 +140,9 @@ p->timeRes += clock() - clk;
         Dec_GraphNode(p->pGraph, i)->pFunc = pFanin;
 
     p->nScores[p->pMap[uTruthBest]]++;
-    p->nNodesRewritten++;
     p->nNodesGained += GainBest;
+    if ( fUseZeros || GainBest > 0 )
+        p->nNodesRewritten++;
 
     // report the progress
     if ( fVeryVerbose )