2 files changed, 30 insertions, 10 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 45510e62..5e65d636 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -5860,7 +5860,7 @@ int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: muxes [-h]\n" );
-    fprintf( pErr, "\t        converts the current network by a network derived by\n" );
+    fprintf( pErr, "\t        converts the current network into a network derived by\n" );
     fprintf( pErr, "\t        replacing all nodes by DAGs isomorphic to the local BDDs\n" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
@@ -7683,7 +7683,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nLevels;
     int fVerbose;
     int fVeryVerbose;
-    char * pFileName;
+//    char * pFileName;
 
 //    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
@@ -7703,6 +7703,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib );
     extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose );
     extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
+    extern void Aig_ProcedureTest();
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -7902,11 +7903,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
+*//*
+
     if ( argc != globalUtilOptind + 1 )
         goto usage;
     pFileName = argv[globalUtilOptind];
     Nwk_ManLutMergeGraphTest( pFileName );
+*/
+    Aig_ProcedureTest();
+
     return 0;
 usage:
     fprintf( pErr, "usage: test [-h] <file_name>\n" );
@@ -8962,7 +8967,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Dch_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -8999,6 +9004,9 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nSatVarMax < 0 ) 
                 goto usage;
             break;
+        case 's':
+            pPars->fSynthesis ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -9029,11 +9037,12 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dch [-WCS num] [-vh]\n" );
+    fprintf( pErr, "usage: dch [-WCS num] [-svh]\n" );
     fprintf( pErr, "\t         performs computation of structural choices\n" );
     fprintf( pErr, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     fprintf( pErr, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
+    fprintf( pErr, "\t-s     : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index c7e0df30..16215a64 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -834,16 +834,27 @@ Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
     Vec_Ptr_t * vAigs;
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
-    int i;
+    int i, clk;
     assert( Abc_NtkIsStrash(pNtk) );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
-    vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fVerbose );
-    Aig_ManStop( pMan );
+clk = clock();
+    if ( pPars->fSynthesis )
+    {
+//        vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fVerbose );
+        vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, 0 );
+        Aig_ManStop( pMan );
+    }
+    else
+    {
+        vAigs = Vec_PtrAlloc( 1 );
+        Vec_PtrPush( vAigs, pMan );
+    }
+pPars->timeSynth = clock() - clk;
     pMan = Dch_ComputeChoices( vAigs, pPars );
-//    pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
-    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
+//    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
     Aig_ManStop( pMan );
     // cleanup
     Vec_PtrForEachEntry( vAigs, pTemp, i )