Version abc70110

11 files changed, 190 insertions, 12 deletions

diff --git a/src/opt/cut/abcCut.c b/src/opt/cut/abcCut.c
index 3b70e9c1..9bbd5790 100644
--- a/src/opt/cut/abcCut.c
+++ b/src/opt/cut/abcCut.c
@@ -20,7 +20,6 @@
 
 #include "abc.h"
 #include "cut.h"
-#include "seqInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index ca829471..8593ef93 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -145,7 +145,7 @@ void Cut_ManStop( Cut_Man_t * p )
     if ( p->vCutPairs )   Vec_IntFree( p->vCutPairs );
     if ( p->puTemp[0] )   free( p->puTemp[0] );
 
-    Extra_MmFixedStop( p->pMmCuts, 0 );
+    Extra_MmFixedStop( p->pMmCuts );
     free( p );
 }
 
diff --git a/src/opt/cut/cutOracle.c b/src/opt/cut/cutOracle.c
index 8e1ad3da..3eb4462b 100644
--- a/src/opt/cut/cutOracle.c
+++ b/src/opt/cut/cutOracle.c
@@ -148,7 +148,7 @@ void Cut_OracleStop( Cut_Oracle_t * p )
     if ( p->vNodeStarts ) Vec_IntFree( p->vNodeStarts );
     if ( p->vCutPairs )   Vec_IntFree( p->vCutPairs );
 
-    Extra_MmFixedStop( p->pMmCuts, 0 );
+    Extra_MmFixedStop( p->pMmCuts );
     free( p ); 
 }
 
diff --git a/src/opt/cut/cutPre22.c b/src/opt/cut/cutPre22.c
index 20c93c5f..5cb87a9c 100644
--- a/src/opt/cut/cutPre22.c
+++ b/src/opt/cut/cutPre22.c
@@ -798,7 +798,7 @@ Cut_CMan_t * Cut_CManStart()
 void Cut_CManStop( Cut_CMan_t * p )
 {
     st_free_table( p->tTable );
-    Extra_MmFixedStop( p->pMem, 0 );
+    Extra_MmFixedStop( p->pMem );
     free( p );
 }
 /**Function*************************************************************
diff --git a/src/opt/dec/decPrint.c b/src/opt/dec/decPrint.c
index b9185509..2d8f09b3 100644
--- a/src/opt/dec/decPrint.c
+++ b/src/opt/dec/decPrint.c
@@ -101,7 +101,7 @@ void Dec_GraphPrint( FILE * pFile, Dec_Graph_t * pGraph, char * pNamesIn[], char
   SeeAlso     []
 
 ***********************************************************************/
-void Dec_GraphPrint_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax )
+void Dec_GraphPrint2_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax )
 {
     Dec_Node_t * pNode0, * pNode1;
     pNode0 = Dec_GraphNode(pGraph, pNode->eEdge0.Node);
@@ -165,6 +165,69 @@ void Dec_GraphPrint_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode,
   SeeAlso     []
 
 ***********************************************************************/
+void Dec_GraphPrint_rec( FILE * pFile, Dec_Graph_t * pGraph, Dec_Node_t * pNode, int fCompl, char * pNamesIn[], int * pPos, int LitSizeMax )
+{
+    Dec_Node_t * pNode0, * pNode1;
+    Dec_Node_t * pNode00, * pNode01, * pNode10, * pNode11;
+    pNode0 = Dec_GraphNode(pGraph, pNode->eEdge0.Node);
+    pNode1 = Dec_GraphNode(pGraph, pNode->eEdge1.Node);
+    if ( Dec_GraphNodeIsVar(pGraph, pNode) ) // FT_NODE_LEAF )
+    {
+        (*pPos) += Dec_GraphPrintGetLeafName( pFile, Dec_GraphNodeInt(pGraph,pNode), fCompl, pNamesIn );
+        return;
+    }
+    if ( !Dec_GraphNodeIsVar(pGraph, pNode0) && !Dec_GraphNodeIsVar(pGraph, pNode1) )
+    {
+        pNode00 = Dec_GraphNode(pGraph, pNode0->eEdge0.Node);
+        pNode01 = Dec_GraphNode(pGraph, pNode0->eEdge1.Node);
+        pNode10 = Dec_GraphNode(pGraph, pNode1->eEdge0.Node);
+        pNode11 = Dec_GraphNode(pGraph, pNode1->eEdge1.Node);
+        if ( (pNode00 == pNode10 || pNode00 == pNode11) && (pNode01 == pNode10 || pNode01 == pNode11) )
+        {
+            fprintf( pFile, "(" );
+            (*pPos)++;
+            Dec_GraphPrint_rec( pFile, pGraph, pNode00, pNode00->fCompl0, pNamesIn, pPos, LitSizeMax );
+            fprintf( pFile, " # " );
+            (*pPos) += 3;
+            Dec_GraphPrint_rec( pFile, pGraph, pNode01, pNode01->fCompl1, pNamesIn, pPos, LitSizeMax );
+            fprintf( pFile, ")" );
+            (*pPos)++;
+            return;
+        }
+    }
+    if ( fCompl )
+    {
+        fprintf( pFile, "(" );
+        (*pPos)++;
+        Dec_GraphPrint_rec( pFile, pGraph, pNode0, !pNode->fCompl0, pNamesIn, pPos, LitSizeMax );
+        fprintf( pFile, " + " );
+        (*pPos) += 3;
+        Dec_GraphPrint_rec( pFile, pGraph, pNode1, !pNode->fCompl1, pNamesIn, pPos, LitSizeMax );
+        fprintf( pFile, ")" );
+        (*pPos)++;
+    }
+    else
+    {
+        fprintf( pFile, "(" );
+        (*pPos)++;
+        Dec_GraphPrint_rec( pFile, pGraph, pNode0, pNode->fCompl0, pNamesIn, pPos, LitSizeMax );
+        Dec_GraphPrint_rec( pFile, pGraph, pNode1, pNode->fCompl1, pNamesIn, pPos, LitSizeMax );
+        fprintf( pFile, ")" );
+        (*pPos)++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Dec_GraphPrintGetLeafName( FILE * pFile, int iLeaf, int fCompl, char * pNamesIn[] )
 {
     static char Buffer[100];
diff --git a/src/opt/fxu/fxuMatrix.c b/src/opt/fxu/fxuMatrix.c
index a0d4f0cb..93ec7b90 100644
--- a/src/opt/fxu/fxuMatrix.c
+++ b/src/opt/fxu/fxuMatrix.c
@@ -130,7 +130,7 @@ void Fxu_MatrixDelete( Fxu_Matrix * p )
             MEM_FREE_FXU( p, Fxu_Var, 1, pVar );
     }
 #else
-    Extra_MmFixedStop( p->pMemMan, 0 );
+    Extra_MmFixedStop( p->pMemMan );
 #endif
 
     Vec_PtrFree( p->vPairs );
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index eda2b85f..03d0b637 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -95,6 +95,9 @@ struct Rwr_Node_t_ // 24 bytes
 {
     int                Id;               // ID 
     int                TravId;           // traversal ID
+    short              nScore;
+    short              nGain;
+    short              nAdded;
     unsigned           uTruth : 16;      // truth table
     unsigned           Volume :  8;      // volume
     unsigned           Level  :  6;      // level
@@ -123,6 +126,8 @@ static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c )  { return (Rwr_N
 extern void              Rwr_ManPreprocess( Rwr_Man_t * p );
 /*=== rwrEva.c ========================================================*/
 extern int               Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros );
+extern void              Rwr_ScoresClean( Rwr_Man_t * p );
+extern void              Rwr_ScoresReport( Rwr_Man_t * p );
 /*=== rwrLib.c ========================================================*/
 extern void              Rwr_ManPrecompute( Rwr_Man_t * p );
 extern Rwr_Node_t *      Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, int fPrecompute );
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index 4ce71a9b..0cac4af8 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -198,7 +198,9 @@ p->timeRes += clock() - clk;
     p->nScores[p->pMap[uTruthBest]]++;
     p->nNodesGained += GainBest;
     if ( fUseZeros || GainBest > 0 )
+    {
         p->nNodesRewritten++;
+    }
 
     // report the progress
     if ( fVeryVerbose && GainBest > 0 )
@@ -257,6 +259,14 @@ Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCu
             GainBest   = nNodesSaved - nNodesAdded;
             pGraphBest = pGraphCur;
 
+            // score the graph
+            if ( GainBest > 0 )
+            {
+                pNode->nScore++;
+                pNode->nGain += GainBest;
+                pNode->nAdded += nNodesAdded;
+            }
+
 //            if ( GainBest > 0 )
 //            printf( "%d %d  ", nNodesSaved, nNodesAdded );
         }
@@ -267,7 +277,6 @@ Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCu
     return pGraphBest;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Checks the type of the cut.]
@@ -418,6 +427,107 @@ int Rwr_NodeGetDepth_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves )
     return 1 + ABC_MAX( Depth0, Depth1 );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ScoresClean( Rwr_Man_t * p )
+{
+    Vec_Ptr_t * vSubgraphs;
+    Rwr_Node_t * pNode;
+    int i, k;
+    for ( i = 0; i < p->vClasses->nSize; i++ )
+    {
+        vSubgraphs = Vec_VecEntry( p->vClasses, i );
+        Vec_PtrForEachEntry( vSubgraphs, pNode, k )
+            pNode->nScore = pNode->nGain = pNode->nAdded = 0;
+    }
+}
+
+static int Gains[222];
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rwr_ScoresCompare( int * pNum1, int * pNum2 )
+{
+    if ( Gains[*pNum1] > Gains[*pNum2] )
+        return -1;
+    if ( Gains[*pNum1] < Gains[*pNum2] )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ScoresReport( Rwr_Man_t * p )
+{
+    extern void Ivy_TruthDsdComputePrint( unsigned uTruth );
+    int Perm[222];
+    Vec_Ptr_t * vSubgraphs;
+    Rwr_Node_t * pNode;
+    int i, iNew, k;
+    unsigned uTruth;
+    // collect total gains
+    assert( p->vClasses->nSize == 222 );
+    for ( i = 0; i < p->vClasses->nSize; i++ )
+    {
+        Perm[i] = i;
+        Gains[i] = 0;
+        vSubgraphs = Vec_VecEntry( p->vClasses, i );
+        Vec_PtrForEachEntry( vSubgraphs, pNode, k )
+            Gains[i] += pNode->nGain;
+    }
+    // sort the gains
+    qsort( Perm, 222, sizeof(int), (int (*)(const void *, const void *))Rwr_ScoresCompare );
+
+    // print classes
+    for ( i = 0; i < p->vClasses->nSize; i++ )
+    {
+        iNew = Perm[i];
+        if ( Gains[iNew] == 0 )
+            break;
+        vSubgraphs = Vec_VecEntry( p->vClasses, iNew );
+        printf( "CLASS %3d: Subgr = %3d. Total gain = %6d.  ", iNew, Vec_PtrSize(vSubgraphs), Gains[iNew] );
+        uTruth = (unsigned)p->pMapInv[iNew];
+        Extra_PrintBinary( stdout, &uTruth, 16 );
+        printf( "  " );
+        Ivy_TruthDsdComputePrint( (unsigned)p->pMapInv[iNew] | ((unsigned)p->pMapInv[iNew] << 16) );
+        Vec_PtrForEachEntry( vSubgraphs, pNode, k )
+        {
+            if ( pNode->nScore == 0 )
+                continue;
+            printf( "    %2d: S=%5d. A=%5d. G=%6d. ", k, pNode->nScore, pNode->nAdded, pNode->nGain );
+            Dec_GraphPrint( stdout, (Dec_Graph_t *)pNode->pNext, NULL, NULL );
+        }
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index b6d58d99..1863f38f 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -118,7 +118,7 @@ void Rwr_ManStop( Rwr_Man_t * p )
     Vec_IntFree( p->vLevNums );
     Vec_PtrFree( p->vFanins );
     Vec_PtrFree( p->vFaninsCur );
-    Extra_MmFixedStop( p->pMmNode, 0 );
+    Extra_MmFixedStop( p->pMmNode );
     FREE( p->pMapInv );
     free( p->pTable );
     free( p->pPractical );
@@ -159,7 +159,7 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
     PRT( "Update      ", p->timeUpdate );
     PRT( "TOTAL       ", p->timeTotal );
 
-
+/*
     printf( "The scores are:\n" );
     for ( i = 0; i < 222; i++ )
         if ( p->nScores[i] > 0 )
@@ -168,6 +168,7 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
             printf( "%3d = %8d  canon = %5d  ", i, p->nScores[i], p->pMapInv[i] );
             Ivy_TruthDsdComputePrint( (unsigned)p->pMapInv[i] | ((unsigned)p->pMapInv[i] << 16) );
         }
+*/
     printf( "\n" );
 
 }
diff --git a/src/opt/sim/simMan.c b/src/opt/sim/simMan.c
index a7d8251c..3b50ad84 100644
--- a/src/opt/sim/simMan.c
+++ b/src/opt/sim/simMan.c
@@ -210,7 +210,7 @@ void Sim_ManStop( Sim_Man_t * p )
     if ( p->vSuppStr )     Sim_UtilInfoFree( p->vSuppStr );    
 //    if ( p->vSuppFun )     Sim_UtilInfoFree( p->vSuppFun );    
     if ( p->vSuppTargs )   Vec_VecFree( p->vSuppTargs );
-    if ( p->pMmPat )       Extra_MmFixedStop( p->pMmPat, 0 );
+    if ( p->pMmPat )       Extra_MmFixedStop( p->pMmPat );
     if ( p->vFifo )        Vec_PtrFree( p->vFifo );
     if ( p->vDiffs )       Vec_IntFree( p->vDiffs );
     free( p );
diff --git a/src/opt/sim/simSymSim.c b/src/opt/sim/simSymSim.c
index ff0cafed..2282825b 100644
--- a/src/opt/sim/simSymSim.c
+++ b/src/opt/sim/simSymSim.c
@@ -65,8 +65,8 @@ clk = clock();
     Abc_NtkForEachCo( p->pNtk, pNode, i )
     {
         pNode = Abc_ObjFanin0(pNode);
-        if ( Abc_ObjIsCi(pNode) || Abc_AigNodeIsConst(pNode) )
-            continue;
+//        if ( Abc_ObjIsCi(pNode) || Abc_AigNodeIsConst(pNode) )
+//            continue;
         nPairsTotal  = Vec_IntEntry(p->vPairsTotal, i);
         nPairsSym    = Vec_IntEntry(p->vPairsSym,   i);
         nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i);