Integration with several commands.

4 files changed, 71 insertions, 1 deletions

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 );