4 files changed, 40 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c2a6214d..3a6874ca 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2569,6 +2569,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     Res_Par_t Pars, * pPars = &Pars;
     int c;
 
+//    printf( "Implementation of this command is not finished.\n" );
+//    return 1;
+
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
@@ -2641,8 +2644,8 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: mfs [-W <NM>] [-S <num>] [-vwh]\n" );
     fprintf( pErr, "\t           performs resubstitution-based resynthesis with don't-cares\n" );
-    fprintf( pErr, "\t-W <NM>  : specifies the windowing paramters (00 < NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
-    fprintf( pErr, "\t-S <num> : specifies the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
+    fprintf( pErr, "\t-W <NM>  : Fanin/Fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
+    fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
     fprintf( pErr, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w       : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : print the command usage\n");
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 243067ce..00f8c183 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -187,18 +187,44 @@ Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int
 {
     Abc_Ntk_t * pNtkAig;
     Ivy_Man_t * pMan;
+    int clk;
 //    int i;
-
+/*
+extern int nMoves;
+extern int nMovesS;
+extern int nClauses;
+extern int timeInv;
+
+nMoves = 0;
+nMovesS = 0;
+nClauses = 0;
+timeInv = 0;
+*/
     pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
     if ( pMan == NULL )
         return NULL;
 //timeRetime = clock();
 
+clk = clock();
     Ivy_ManHaigStart( pMan, fVerbose );
 //    Ivy_ManRewriteSeq( pMan, 0, 0 );
 //    for ( i = 0; i < nIters; i++ )
 //        Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
+
+//printf( "%d ", Ivy_ManNodeNum(pMan) );
     Ivy_ManRewriteSeq( pMan, 0, 0 );
+    Ivy_ManRewriteSeq( pMan, 0, 0 );
+    Ivy_ManRewriteSeq( pMan, 1, 0 );
+//printf( "%d ", Ivy_ManNodeNum(pMan) );
+//printf( "%d ", Ivy_ManNodeNum(pMan->pHaig) );
+//PRT( " ", clock() - clk );
+//printf( "\n" );
+/*
+    printf( "Moves = %d.  ", nMoves );
+    printf( "MovesS = %d.  ", nMovesS );
+    printf( "Clauses = %d.  ", nClauses );
+    PRT( "Time", timeInv );
+*/
 //    Ivy_ManRewriteSeq( pMan, 1, 0 );
 //printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) );
 //    Ivy_ManHaigPostprocess( pMan, fVerbose );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index e66ce018..177c269b 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -77,7 +77,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 //            fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 );
     }
     else 
+    {
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
+        fprintf( pFile, "  net = %5d", Abc_NtkGetTotalFanins(pNtk) );
+    }
 
     if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsNetlist(pNtk) )
     {
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 96540269..d9cae254 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -65,6 +65,10 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
     pSat = Abc_NtkMiterSatCreate( pNtk, 0 );
     if ( pSat == NULL )
         return 1;
+//printf( "%d \n", pSat->clauses.size );
+//sat_solver_delete( pSat );
+//return 1;
+
 //    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
 //    PRT( "Time", clock() - clk );
 
@@ -619,7 +623,7 @@ void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes )
 
     nMuxes = 0;
     pSat = sat_solver_new();
-sat_solver_store_alloc( pSat );
+//sat_solver_store_alloc( pSat );
     RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk );
 sat_solver_store_mark_roots( pSat );