Upgrading choice computation.

5 files changed, 38 insertions, 27 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 83c98e10..06a7c877 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -15125,7 +15125,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, "WCSsptgcfrvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcfrxvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -15183,6 +15183,9 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             pPars->fSkipRedSupp ^= 1;
             break;
+        case 'x':
+            pPars->fUseNew ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -15213,7 +15216,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: dch [-WCS num] [-sptgcfrvh]\n" );
+    Abc_Print( -2, "usage: dch [-WCS num] [-sptgcfrxvh]\n" );
     Abc_Print( -2, "\t         computes structural choices using a new approach\n" );
     Abc_Print( -2, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
@@ -15225,6 +15228,7 @@ usage:
     Abc_Print( -2, "\t-c     : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" );
     Abc_Print( -2, "\t-f     : toggle using faster logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle skipping choices with redundant support [default = %s]\n", pPars->fSkipRedSupp? "yes": "no" );
+    Abc_Print( -2, "\t-x     : toggle using new choice computation [default = %s]\n", pPars->fUseNew? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -30654,7 +30658,7 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
     else
     {
         Abc_Ntk_t * pNtkNoCh;
-//        Abc_Print( -1, "Transforming AIG with %d choice nodes.\n", Gia_ManEquivCountClasses(pAbc->pGia) );
+        Abc_Print( -1, "Transforming AIG with %d choice nodes.\n", Gia_ManEquivCountClasses(pAbc->pGia) );
         // create network without choices
         pMan = Gia_ManToAig( pAbc->pGia, 0 );
         pNtkNoCh = Abc_NtkFromAigPhase( pMan );
@@ -32565,19 +32569,19 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( nVars )
     {
-        Abc_Print( -1, "Cofactoring the last %d inputs.\n", nVars );
+        Abc_Print( 0, "Cofactoring the last %d inputs.\n", nVars );
         pTemp = Gia_ManComputeCofs( pAbc->pGia, nVars );
         Abc_FrameUpdateGia( pAbc, pTemp );
     }
     else if ( nLimFan )
     {
-        Abc_Print( -1, "Cofactoring all variables whose fanout count is higher than %d.\n", nLimFan );
+        Abc_Print( 0, "Cofactoring all variables whose fanout count is higher than %d.\n", nLimFan );
         pTemp = Gia_ManDupCofAll( pAbc->pGia, nLimFan, fVerbose );
         Abc_FrameUpdateGia( pAbc, pTemp );
     }
     else if ( iVar )
     {
-        Abc_Print( -1, "Cofactoring one variable with object ID %d.\n", iVar );
+        Abc_Print( 0, "Cofactoring one variable with object ID %d.\n", iVar );
         pTemp = Gia_ManDupCof( pAbc->pGia, iVar );
         Abc_FrameUpdateGia( pAbc, pTemp );
     }
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ae2d9835..95c9200d 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1651,6 +1651,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
 {
+    extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
     extern Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose );
     extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
 
@@ -1662,23 +1663,28 @@ Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
-clk = Abc_Clock();
-    if ( pPars->fSynthesis )
-        pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
-    else
+    if ( pPars->fUseNew )
+        pMan = Dar_ManChoiceNew( pMan, pPars );
+    else 
     {
-        pGia = Gia_ManFromAig( pMan );
-        Aig_ManStop( pMan );
-    }
+clk = Abc_Clock();
+        if ( pPars->fSynthesis )
+            pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
+        else
+        {
+            pGia = Gia_ManFromAig( pMan );
+            Aig_ManStop( pMan );
+        }
 pPars->timeSynth = Abc_Clock() - clk;
-    if ( pPars->fUseGia )
-        pMan = Cec_ComputeChoices( pGia, pPars );
-    else
-    {
-        pMan = Gia_ManToAigSkip( pGia, 3 );
-        Gia_ManStop( pGia );
-        pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
-        Aig_ManStop( pTemp );
+        if ( pPars->fUseGia )
+            pMan = Cec_ComputeChoices( pGia, pPars );
+        else
+        {
+            pMan = Gia_ManToAigSkip( pGia, 3 );
+            Gia_ManStop( pGia );
+            pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
+            Aig_ManStop( pTemp );
+        }
     }
     pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
     Aig_ManStop( pMan );
diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c
index 684e85e6..d95c23d7 100644
--- a/src/opt/dar/darScript.c
+++ b/src/opt/dar/darScript.c
@@ -848,7 +848,7 @@ pPars->timeSynth = Abc_Clock() - clk;
 ***********************************************************************/
 Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
-    extern Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int fVerbose );
+    extern Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose );
     extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
 //    extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
     extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
@@ -872,7 +872,7 @@ pPars->timeSynth = Abc_Clock() - clk;
 
     // perform choice computation
     if ( pPars->fUseNew )
-        pMan = Cec_ComputeChoicesNew( pGia, pPars->fVerbose );
+        pMan = Cec_ComputeChoicesNew( pGia, pPars->nBTLimit, pPars->fVerbose );
     else if ( pPars->fUseGia )
         pMan = Cec_ComputeChoices( pGia, pPars );
     else
diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c
index 780a1196..db0059fd 100644
--- a/src/proof/cec/cecChoice.c
+++ b/src/proof/cec/cecChoice.c
@@ -412,11 +412,11 @@ Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int fVerbose )
+Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose )
 {
-    extern void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose );
+    extern void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose );
     Aig_Man_t * pAig;
-    Cec4_ManSimulateTest2( pGia, fVerbose );
+    Cec4_ManSimulateTest2( pGia, nConfs, fVerbose );
     pGia = Gia_ManEquivToChoices( pGia, 3 );
     Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) );
     pAig = Gia_ManToAig( pGia, 1 );
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index 19349986..ae90e7fc 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -1794,13 +1794,14 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
     Cec4_ManPerformSweeping( p, pPars, &pNew, 0 );
     return pNew;
 }
-void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose )
+void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )
 {
     abctime clk = Abc_Clock();
     Cec_ParFra_t ParsFra, * pPars = &ParsFra;
     Cec4_ManSetParams( pPars );
     Cec4_ManPerformSweeping( p, pPars, NULL, 0 );
     pPars->fVerbose = fVerbose;
+    pPars->nBTLimit = nConfs;
     if ( fVerbose )
         Abc_PrintTime( 1, "New choice computation time", Abc_Clock() - clk );
 }