Version abc60220

4 files changed, 26 insertions, 13 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++;
     }
 }