1 files changed, 54 insertions, 19 deletions

diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index 31e003cf..c9dccb6a 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -24,6 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern void Npn_StartTruth8( uint8 uTruths[][32] );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -43,32 +45,32 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
 {
     Cut_Man_t * p;
     int clk = clock();
-    assert( pParams->nVarsMax >= 4 && pParams->nVarsMax <= 6 );
+    assert( pParams->nVarsMax >= 4 && pParams->nVarsMax <= CUT_SIZE_MAX );
     p = ALLOC( Cut_Man_t, 1 );
     memset( p, 0, sizeof(Cut_Man_t) );
     // set and correct parameters
     p->pParams = pParams;
-    if ( p->pParams->fSeq )
-        p->pParams->fFilter = 1;
-    // space for cuts
-    p->vCuts = Vec_PtrAlloc( pParams->nIdsMax );
-    Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL );
+    // prepare storage for cuts
+    p->vCutsNew = Vec_PtrAlloc( pParams->nIdsMax );
+    Vec_PtrFill( p->vCutsNew, pParams->nIdsMax, NULL );
+    // prepare storage for sequential cuts
     if ( pParams->fSeq )
     {
-        p->vCutsNew = Vec_PtrAlloc( pParams->nIdsMax );
-        Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL );
+        p->pParams->fFilter = 1;
+        p->vCutsOld = Vec_PtrAlloc( pParams->nIdsMax );
+        Vec_PtrFill( p->vCutsOld, pParams->nIdsMax, NULL );
+        p->vCutsTemp = Vec_PtrAlloc( pParams->nCutSet );
+        Vec_PtrFill( p->vCutsTemp, pParams->nCutSet, NULL );
     }
+    assert( !pParams->fTruth || pParams->nVarsMax <= 5 );
     // entry size
-    p->EntrySize = sizeof(Cut_Cut_t) + (pParams->nVarsMax + pParams->fSeq) * sizeof(int);
-    if ( pParams->fTruth )
-    {
-        if ( pParams->nVarsMax == 5 )
-            p->EntrySize += sizeof(unsigned);
-        else if ( pParams->nVarsMax == 6 )
-            p->EntrySize += 2 * sizeof(unsigned);
-    }
+    p->EntrySize = sizeof(Cut_Cut_t) + pParams->nVarsMax * sizeof(int);
+    if ( pParams->fTruth && pParams->nVarsMax >= 5 && pParams->nVarsMax <= 8 )
+        p->EntrySize += (1 << (pParams->nVarsMax - 5)) * sizeof(unsigned);
     // memory for cuts
     p->pMmCuts = Extra_MmFixedStart( p->EntrySize );
+    // elementary truth tables
+    Npn_StartTruth8( p->uTruths );
     p->uTruthVars[0][1] = p->uTruthVars[0][0] = 0xAAAAAAAA;    // 1010 1010 1010 1010 1010 1010 1010 1010
     p->uTruthVars[1][1] = p->uTruthVars[1][0] = 0xCCCCCCCC;    // 1010 1010 1010 1010 1010 1010 1010 1010
     p->uTruthVars[2][1] = p->uTruthVars[2][0] = 0xF0F0F0F0;    // 1111 0000 1111 0000 1111 0000 1111 0000
@@ -95,13 +97,14 @@ void Cut_ManStop( Cut_Man_t * p )
 {
     Cut_Cut_t * pCut;
     int i;
-    Vec_PtrForEachEntry( p->vCuts, pCut, i )
+    Vec_PtrForEachEntry( p->vCutsNew, pCut, i )
         if ( pCut != NULL )
         {
             int k = 0;
         }
     if ( p->vCutsNew )   Vec_PtrFree( p->vCutsNew );
-    if ( p->vCuts )      Vec_PtrFree( p->vCuts );
+    if ( p->vCutsOld )   Vec_PtrFree( p->vCutsOld );
+    if ( p->vCutsTemp )  Vec_PtrFree( p->vCutsTemp );
     if ( p->vFanCounts ) Vec_IntFree( p->vFanCounts );
     if ( p->pPerms43 )   free( p->pPerms43 );
     if ( p->pPerms53 )   free( p->pPerms53 );
@@ -124,13 +127,18 @@ void Cut_ManStop( Cut_Man_t * p )
 ***********************************************************************/
 void Cut_ManPrintStats( Cut_Man_t * p )
 {
+    if ( p->pReady )
+    {
+        Cut_CutRecycle( p, p->pReady );
+        p->pReady = NULL;
+    }
     printf( "Cut computation statistics:\n" );
     printf( "Current cuts      = %8d. (Trivial = %d.)\n", p->nCutsCur-p->nCutsTriv, p->nCutsTriv );
     printf( "Peak cuts         = %8d.\n", p->nCutsPeak );
     printf( "Total allocated   = %8d.\n", p->nCutsAlloc );
     printf( "Total deallocated = %8d.\n", p->nCutsDealloc );
     printf( "Cuts filtered     = %8d.\n", p->nCutsFilter );
-    printf( "Nodes with limit  = %8d.\n", p->nCutsLimit );
+    printf( "Nodes saturated   = %8d. (Max cuts = %d.)\n", p->nCutsLimit, p->pParams->nKeepMax );
     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) );
@@ -138,8 +146,35 @@ void Cut_ManPrintStats( Cut_Man_t * p )
     PRT( "Union ", p->timeUnion );
     PRT( "Filter", p->timeFilter );
     PRT( "Truth ", p->timeTruth );
+    printf( "Nodes = %d. Multi = %d.  Cuts = %d. Multi = %d.\n", 
+        p->nNodes, p->nNodesMulti, p->nCutsCur-p->nCutsTriv, p->nCutsMulti );
 }
 
+    
+/**Function*************************************************************
+
+  Synopsis    [Prints some interesting stats.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, int TimeTotal )
+{
+    FILE * pTable;
+    pTable = fopen( "cut_stats.txt", "a+" );
+    fprintf( pTable, "%-20s ", pFileName );
+    fprintf( pTable, "%8d ", p->nNodes );
+    fprintf( pTable, "%6.1f ", ((float)(p->nCutsCur))/p->nNodes );
+    fprintf( pTable, "%6.2f ", ((float)(100.0 * p->nCutsLimit))/p->nNodes );
+    fprintf( pTable, "%6.2f ", (float)p->nCutsPeak * p->EntrySize / (1<<20) );
+    fprintf( pTable, "%6.2f ", (float)(TimeTotal)/(float)(CLOCKS_PER_SEC) );
+    fprintf( pTable, "\n" );
+    fclose( pTable );
+}
 
 /**Function*************************************************************