Integration with several commands.

8 files changed, 119 insertions, 23 deletions

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 4f448c40..ed4b7109 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1327,7 +1327,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
     {
         Gia_Obj_t * pRepr;
         pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) );
-        for ( i = 0; i < Gia_ManObjNum(p); i++ )
+        for ( i = 0; i < Gia_ManObjNum(pNew); i++ )
             Gia_ObjSetRepr( pNew, i, GIA_VOID );
         Gia_ManForEachObj1( p, pObj, i )
         {
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index f7f873cd..c987453f 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1988,7 +1988,7 @@ Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
     pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
     pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
     for ( i = 0; i < Gia_ManObjNum(p); i++ )
-        Gia_ObjSetRepr( pNew, i, GIA_VOID );
+        pNew->pReprs[i].iRepr = GIA_VOID;
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7bf97aa6..2819195f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -36284,21 +36284,13 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    extern void Cec4_ManSetParams( Cec_ParFra_t * pPars );
     extern Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
     extern Gia_Man_t * Cec3_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
     extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
     Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp;
     int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoG2 = 0;
-    Cec_ManFraSetDefaultParams( pPars );
-    pPars->jType          =       2;    // solver type
-    pPars->fSatSweeping   =       1;    // conflict limit at a node
-    pPars->nWords         =       4;    // simulation words
-    pPars->nRounds        =      10;    // simulation rounds
-    pPars->nItersMax      =    2000;    // this is a miter
-    pPars->nBTLimit       = 1000000;    // use logic cones
-    pPars->nSatVarMax     =    1000;    // the max number of SAT variables before recycling SAT solver
-    pPars->nCallsRecycle  =     500;    // calls to perform before recycling SAT solver
-    pPars->nGenIters      =     100;    // pattern generation iterations
+    Cec4_ManSetParams( pPars );
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxwvh" ) ) != EOF )
     {
@@ -37034,10 +37026,10 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pFile;
     Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter;
     char ** pArgvNew;
-    int c, nArgcNew, fMiter = 0, fDualOutput = 0, fDumpMiter = 0;
+    int c, nArgcNew, fUseNew = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0;
     Cec_ManCecSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdasvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdasxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -37078,6 +37070,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             pPars->fSilent ^= 1;
             break;
+        case 'x':
+            fUseNew ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -37216,7 +37211,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
     // compute the miter
-    pMiter = Gia_ManMiter( pGias[0], pGias[1], 0, 1, 0, 0, pPars->fVerbose );
+    pMiter = Gia_ManMiter( pGias[0], pGias[1], 0, !fUseNew, 0, 0, pPars->fVerbose );
     if ( pMiter )
     {
         if ( fDumpMiter )
@@ -37229,8 +37224,23 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
             pMiter->vSimsPi = Vec_WrdDup(pGias[0]->vSimsPi); 
             pMiter->nSimWords = pGias[0]->nSimWords;
         }
-        pAbc->Status = Cec_ManVerify( pMiter, pPars );
-        Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb );
+        if ( fUseNew )
+        {
+            abctime clk = Abc_Clock();
+            extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int fVerbose );
+            Gia_Man_t * pNew = Cec4_ManSimulateTest3( pMiter, pPars->fVerbose );
+            if ( Gia_ManAndNum(pNew) == 0 )
+                Abc_Print( 1, "Networks are equivalent.  " );
+            else
+                Abc_Print( 1, "Networks are NOT EQUIVALENT.  " );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+            Gia_ManStop( pNew );
+        }
+        else
+        {
+            pAbc->Status = Cec_ManVerify( pMiter, pPars );
+            Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb );
+        }
         Gia_ManStop( pMiter );
     }
     if ( pGias[0] != pAbc->pGia )
@@ -37239,7 +37249,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &cec [-CT num] [-nmdasvwh]\n" );
+    Abc_Print( -2, "usage: &cec [-CT num] [-nmdasxvwh]\n" );
     Abc_Print( -2, "\t         new combinational equivalence checker\n" );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
@@ -37248,6 +37258,7 @@ usage:
     Abc_Print( -2, "\t-d     : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no");
     Abc_Print( -2, "\t-a     : toggle writing dual-output miter [default = %s]\n", fDumpMiter? "yes":"no");
     Abc_Print( -2, "\t-s     : toggle silent operation [default = %s]\n", pPars->fSilent ? "yes":"no");
+    Abc_Print( -2, "\t-x     : toggle using new solver [default = %s]\n", fUseNew? "yes":"no");
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
     Abc_Print( -2, "\t-w     : toggle printing SAT solver statistics [default = %s]\n", pPars->fVeryVerbose? "yes":"no");
     Abc_Print( -2, "\t-h     : print the command usage\n");
@@ -40970,7 +40981,7 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Dch_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremgcxvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -41028,6 +41039,15 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'm':
             fMinLevel ^= 1;
             break;
+        case 'g':
+            pPars->fUseGia ^= 1;
+            break;
+        case 'c':
+            pPars->fUseCSat ^= 1;
+            break;
+        case 'x':
+            pPars->fUseNew ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -41067,7 +41087,7 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremvh]\n" );
+    Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremgcxvh]\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 );
@@ -41079,6 +41099,9 @@ usage:
     Abc_Print( -2, "\t-r     : toggle skipping choices with redundant support [default = %s]\n", pPars->fSkipRedSupp? "yes": "no" );
     Abc_Print( -2, "\t-e     : toggle computing and merging equivalences [default = %s]\n", fEquiv? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle minimizing logic level after merging equivalences [default = %s]\n", fMinLevel? "yes": "no" );
+    Abc_Print( -2, "\t-g     : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" );
+    Abc_Print( -2, "\t-c     : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "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;
diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c
index f8fa3788..684e85e6 100644
--- a/src/opt/dar/darScript.c
+++ b/src/opt/dar/darScript.c
@@ -848,6 +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_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 );
@@ -870,15 +871,17 @@ clk = Abc_Clock();
 pPars->timeSynth = Abc_Clock() - clk;
 
     // perform choice computation
-    if ( pPars->fUseGia )
+    if ( pPars->fUseNew )
+        pMan = Cec_ComputeChoicesNew( pGia, pPars->fVerbose );
+    else 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 );
     }
+    Gia_ManStop( pGia );
 
     // create guidence
     vPios = Aig_ManOrderPios( pMan, pAig ); 
diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c
index 49025630..47d6a478 100644
--- a/src/proof/cec/cecChoice.c
+++ b/src/proof/cec/cecChoice.c
@@ -401,6 +401,29 @@ Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )
     return pAig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs computation of AIGs with choices.]
+
+  Description [Takes several AIGs and performs choicing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int fVerbose )
+{
+    extern void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose );
+    Aig_Man_t * pAig;
+    Cec4_ManSimulateTest2( pGia, fVerbose );
+    pGia = Gia_ManEquivToChoices( pGia, 3 );
+    Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) );
+    pAig = Gia_ManToAig( pGia, 1 );
+    Gia_ManStop( pGia );
+    return pAig;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index 51654cba..122f33d0 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -145,6 +145,30 @@ static inline void   Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj )
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/**Function*************************************************************
+
+  Synopsis    [Default parameter settings.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec4_ManSetParams( Cec_ParFra_t * pPars )
+{
+    memset( pPars, 0, sizeof(Cec_ParFra_t) );
+    pPars->jType          =       2;    // solver type
+    pPars->fSatSweeping   =       1;    // conflict limit at a node
+    pPars->nWords         =       4;    // simulation words
+    pPars->nRounds        =      10;    // simulation rounds
+    pPars->nItersMax      =    2000;    // this is a miter
+    pPars->nBTLimit       = 1000000;    // use logic cones
+    pPars->nSatVarMax     =    1000;    // the max number of SAT variables before recycling SAT solver
+    pPars->nCallsRecycle  =     500;    // calls to perform before recycling SAT solver
+    pPars->nGenIters      =     100;    // pattern generation iterations
+}
 
 /**Function*************************************************************
 
@@ -1768,6 +1792,26 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
     Cec4_ManPerformSweeping( p, pPars, &pNew );
     return pNew;
 }
+void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Cec_ParFra_t ParsFra, * pPars = &ParsFra;
+    Cec4_ManSetParams( pPars );
+    Cec4_ManPerformSweeping( p, pPars, NULL );
+    pPars->fVerbose = fVerbose;
+    //if ( fVerbose )
+        Abc_PrintTime( 1, "New choice computation time", Abc_Clock() - clk );
+}
+Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Gia_Man_t * pNew = NULL;
+    Cec_ParFra_t ParsFra, * pPars = &ParsFra;
+    Cec4_ManSetParams( pPars );
+    pPars->fVerbose = fVerbose;
+    Cec4_ManPerformSweeping( p, pPars, &pNew );
+    return pNew;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/proof/dch/dch.h b/src/proof/dch/dch.h
index 5d644643..07f6a1d2 100644
--- a/src/proof/dch/dch.h
+++ b/src/proof/dch/dch.h
@@ -52,6 +52,7 @@ struct Dch_Pars_t_
     int              fPower;        // uses power-aware rewriting
     int              fUseGia;       // uses GIA package 
     int              fUseCSat;      // uses circuit-based solver
+    int              fUseNew;       // uses new implementation
     int              fLightSynth;   // uses lighter version of synthesis
     int              fSkipRedSupp;  // skip choices with redundant support vars
     int              fVerbose;      // verbose stats
diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c
index 0da65bee..eef53e73 100644
--- a/src/proof/dch/dchCore.c
+++ b/src/proof/dch/dchCore.c
@@ -90,7 +90,7 @@ Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     Dch_Man_t * p;
     Aig_Man_t * pResult;
-    abctime clk, clkTotal = Abc_Clock();
+    abctime clk, clk2 = Abc_Clock(), clkTotal = Abc_Clock();
     // reset random numbers
     Aig_ManRandom(1);
     // start the choicing manager
@@ -106,6 +106,8 @@ p->timeSimInit = Abc_Clock() - clk;
     // free memory ahead of time
 p->timeTotal = Abc_Clock() - clkTotal;
     Dch_ManStop( p );
+    //if ( pPars->fVerbose ) 
+        Abc_PrintTime( 1, "Old choice computation time", Abc_Clock() - clk2 );
     // create choices
     ABC_FREE( pAig->pTable );
     pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );