4 files changed, 90 insertions, 3 deletions

diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 2a4fcaf3..72e7d3d1 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -83,7 +83,7 @@ extern Aig_Man_t *     Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
 /*=== darCore.c ========================================================*/
 extern void            Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars );
 extern int             Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
-extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax );
+extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose );
 /*=== darRefact.c ========================================================*/
 extern void            Dar_ManDefaultRefParams( Dar_RefPar_t * pPars );
 extern int             Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars );
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index f4041dd1..141d9b79 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -195,6 +195,34 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the total number of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_ManCutCount( Aig_Man_t * pAig, int * pnCutsK )
+{
+    Dar_Cut_t * pCut;
+    Aig_Obj_t * pObj;
+    int i, k, nCuts = 0, nCutsK = 0;
+    Aig_ManForEachNode( pAig, pObj, i )
+        Dar_ObjForEachCut( pObj, pCut, k )
+        {
+            nCuts++;
+            if ( pCut->nLeaves == 4 )
+                nCutsK++;
+        }
+    if ( pnCutsK )
+        *pnCutsK = nCutsK;
+    return nCuts;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -204,13 +232,13 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
   SeeAlso     []
 
 ***********************************************************************/
-Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax )
+Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose )
 {
     Dar_Man_t * p;
     Dar_RwrPar_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
     Aig_MmFixed_t * pMemCuts;
-    int i, nNodes;
+    int i, nNodes, clk = clock();
     // remove dangling nodes
     if ( (nNodes = Aig_ManCleanup( pAig )) )
     {
@@ -226,6 +254,23 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax )
     // compute cuts for each nodes in the topological order
     Aig_ManForEachNode( pAig, pObj, i )
         Dar_ObjComputeCuts( p, pObj );
+    // print verbose stats
+    if ( fVerbose )
+    {
+//        Aig_Obj_t * pObj;
+        int nCuts, nCutsK;//, i;
+        nCuts = Dar_ManCutCount( pAig, &nCutsK );
+        printf( "Nodes = %6d. Total cuts = %6d. 4-input cuts = %6d.\n",
+            Aig_ManObjNum(pAig), nCuts, nCutsK );
+        printf( "Cut size = %2d. Truth size = %2d. Total mem = %5.2f Mb  ",
+            sizeof(Dar_Cut_t), 4, 1.0*Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) );
+        PRT( "Runtime", clock() - clk );
+/*
+        Aig_ManForEachNode( pAig, pObj, i )
+            if ( i % 300 == 0 )
+                Dar_ObjCutPrint( pAig, pObj );
+*/
+    }
     // free the cuts
     pMemCuts = p->pMemCuts;
     p->pMemCuts = NULL;
diff --git a/src/aig/dar/darCut.c b/src/aig/dar/darCut.c
index b0aff095..79e4dcc4 100644
--- a/src/aig/dar/darCut.c
+++ b/src/aig/dar/darCut.c
@@ -30,6 +30,47 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_CutPrint( Dar_Cut_t * pCut )
+{
+    unsigned i;
+    printf( "{" );
+    for ( i = 0; i < pCut->nLeaves; i++ )
+        printf( " %d", pCut->pLeaves[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ObjCutPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Dar_Cut_t * pCut;
+    int i;
+    printf( "Cuts for node %d:\n", pObj->Id );
+    Dar_ObjForEachCut( pObj, pCut, i )
+        Dar_CutPrint( pCut );
+//    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the number of 1s in the machine word.]
 
   Description []
diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h
index 4da793f5..afa3bd07 100644
--- a/src/aig/dar/darInt.h
+++ b/src/aig/dar/darInt.h
@@ -134,6 +134,7 @@ extern void            Dar_ManCutsStart( Dar_Man_t * p );
 extern void            Dar_ManCutsFree( Dar_Man_t * p );
 extern Dar_Cut_t *     Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj );
 extern Dar_Cut_t *     Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
+extern void            Dar_ObjCutPrint( Aig_Man_t * p, Aig_Obj_t * pObj );
 /*=== darData.c ===========================================================*/
 extern Vec_Int_t *     Dar_LibReadNodes();
 extern Vec_Int_t *     Dar_LibReadOuts();