Experiments with SAT sweeping.

3 files changed, 235 insertions, 74 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 403c8e19..2ed1f5ef 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -36287,15 +36287,19 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     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;
+    Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp;
     int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoG2 = 0;
     Cec_ManFraSetDefaultParams( pPars );
-    pPars->fSatSweeping = 1;
-    pPars->nItersMax = 1000000;
-    pPars->nBTLimit  = 1000000;
+    pPars->fSatSweeping   =       1;    // conflict limit at a node
+    pPars->nWords         =       4;    // simulation words
+    pPars->nRounds        =     250;    // simulation rounds
+    pPars->nItersMax      = 1000000;    // 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      =       5;    // pattern generation iterations
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdckngxwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCPrmdckngxwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -36365,6 +36369,17 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nBTLimit < 0 )
                 goto usage;
             break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nGenIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nGenIters < 0 )
+                goto usage;
+            break;
         case 'r':
             pPars->fRewriting ^= 1;
             break;
@@ -36416,7 +36431,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdckngwvh]\n" );
+    Abc_Print( -2, "usage: &fraig [-WRILDCP <num>] [-rmdckngwvh]\n" );
     Abc_Print( -2, "\t         performs combinational SAT sweeping\n" );
     Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
     Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds );
@@ -36424,6 +36439,7 @@ usage:
     Abc_Print( -2, "\t-L num : the max number of levels of nodes to consider [default = %d]\n", pPars->nLevelMax );
     Abc_Print( -2, "\t-D num : the max number of steps of speculative reduction [default = %d]\n", pPars->nDepthMax );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+    Abc_Print( -2, "\t-P num : the number of pattern generation iterations [default = %d]\n", pPars->nGenIters );
     Abc_Print( -2, "\t-r     : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
     Abc_Print( -2, "\t-d     : toggle using double output miters [default = %s]\n", pPars->fDualOut? "yes": "no" );
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index 757d9fd3..c5c5dbb7 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -102,6 +102,9 @@ struct Cec_ParFra_t_
     int              TimeLimit;     // the runtime limit in seconds
     int              nLevelMax;     // restriction on the level nodes to be swept
     int              nDepthMax;     // the depth in terms of steps of speculative reduction
+    int              nCallsRecycle; // calls to perform before recycling SAT solver
+    int              nSatVarMax;    // the max number of SAT variables
+    int              nGenIters;     // pattern generation iterations
     int              fRewriting;    // enables AIG rewriting
     int              fCheckMiter;   // the circuit is the miter
 //    int              fFirstStop;    // stop on the first sat output
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index 2890a364..d01b7bd5 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -29,27 +29,11 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-// sweeping manager
-typedef struct Cec4_Par_t_ Cec4_Par_t;
-struct Cec4_Par_t_
-{
-    int              nSimWords;     // simulation words
-    int              nSimRounds;    // simulation rounds
-    int              nItersMax;     // max number of iterations
-    int              nConfLimit;    // SAT solver conflict limit
-    int              nSatVarMax;    // the max number of SAT variables
-    int              nCallsRecycle; // calls to perform before recycling SAT solver
-    int              fIsMiter;      // this is a miter
-    int              fUseCones;     // use logic cones
-    int              fVeryVerbose;  // verbose stats
-    int              fVerbose;      // verbose stats
-};
-
 // SAT solving manager
 typedef struct Cec4_Man_t_ Cec4_Man_t;
 struct Cec4_Man_t_
 {
-    Cec4_Par_t *     pPars;          // parameters
+    Cec_ParFra_t *   pPars;          // parameters
     Gia_Man_t *      pAig;           // user's AIG
     Gia_Man_t *      pNew;           // internal AIG
     // SAT solving
@@ -60,6 +44,9 @@ struct Cec4_Man_t_
     Vec_Int_t *      vCexMin;        // minimized CEX
     Vec_Int_t *      vClassUpdates;  // updated equiv classes
     Vec_Int_t *      vCexStamps;     // time stamps
+    Vec_Int_t *      vCands;
+    Vec_Int_t *      vVisit;
+    Vec_Int_t *      vPat;
     int              iLastConst;     // last const node proved
     // statistics
     int              nPatterns;
@@ -70,6 +57,8 @@ struct Cec4_Man_t_
     int              nSimulates;
     int              nRecycles;
     int              nConflicts[2][3];
+    abctime          timeCnf;
+    abctime          timeGenPats;
     abctime          timeSatSat0;
     abctime          timeSatUnsat0;
     abctime          timeSatSat;
@@ -92,32 +81,6 @@ static inline void   Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Sets parameter defaults.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec4_SetDefaultParams( Cec4_Par_t * p )
-{
-    memset( p, 0, sizeof(Cec4_Par_t) );
-    p->nSimWords      =       4;    // simulation words
-    p->nSimRounds     =     250;    // simulation rounds
-    p->nItersMax      =      10;    // max number of iterations
-    p->nConfLimit     =    1000;    // conflict limit at a node
-    p->nSatVarMax     =    1000;    // the max number of SAT variables before recycling SAT solver
-    p->nCallsRecycle  =     200;    // calls to perform before recycling SAT solver
-    p->fIsMiter       =       0;    // this is a miter
-    p->fUseCones      =       0;    // use logic cones
-    p->fVeryVerbose   =       0;    // verbose stats
-    p->fVerbose       =       0;    // verbose stats
-}  
-
-/**Function*************************************************************
-
   Synopsis    []
 
   Description []
@@ -127,7 +90,7 @@ void Cec4_SetDefaultParams( Cec4_Par_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec4_Par_t * pPars )
+Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
 {
     Cec4_Man_t * p;
     Gia_Obj_t * pObj; int i;
@@ -153,6 +116,9 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec4_Par_t * pPars )
     p->vCexMin       = Vec_IntAlloc( 100 );
     p->vClassUpdates = Vec_IntAlloc( 100 );
     p->vCexStamps    = Vec_IntStart( Gia_ManObjNum(pAig) );
+    p->vCands        = Vec_IntAlloc( 100 );
+    p->vVisit        = Vec_IntAlloc( 100 );
+    p->vPat          = Vec_IntAlloc( 100 );
     return p;
 }
 void Cec4_ManDestroy( Cec4_Man_t * p )
@@ -161,13 +127,15 @@ void Cec4_ManDestroy( Cec4_Man_t * p )
     {
         abctime timeTotal = Abc_Clock() - p->timeStart;
         abctime timeSat   = p->timeSatSat0 + p->timeSatSat + p->timeSatUnsat0 + p->timeSatUnsat + p->timeSatUndec;
-        abctime timeOther = timeTotal - timeSat - p->timeSim - p->timeRefine - p->timeResimLoc;// - p->timeResimGlo;
+        abctime timeOther = timeTotal - timeSat - p->timeSim - p->timeRefine - p->timeResimLoc - p->timeGenPats;// - p->timeResimGlo;
         ABC_PRTP( "SAT solving  ", timeSat,          timeTotal );
         ABC_PRTP( "  sat(easy)  ", p->timeSatSat0,   timeTotal );
         ABC_PRTP( "  sat        ", p->timeSatSat,    timeTotal );
         ABC_PRTP( "  unsat(easy)", p->timeSatUnsat0, timeTotal );
         ABC_PRTP( "  unsat      ", p->timeSatUnsat,  timeTotal );
         ABC_PRTP( "  fail       ", p->timeSatUndec,  timeTotal );
+        ABC_PRTP( "Generate CNF ", p->timeCnf,       timeTotal );
+        ABC_PRTP( "Generate pats", p->timeGenPats,   timeTotal );
         ABC_PRTP( "Simulation   ", p->timeSim,       timeTotal );
         ABC_PRTP( "Refinement   ", p->timeRefine,    timeTotal );
         ABC_PRTP( "Resim global ", p->timeResimGlo,  timeTotal );
@@ -185,6 +153,9 @@ void Cec4_ManDestroy( Cec4_Man_t * p )
     Vec_IntFreeP( &p->vCexMin );
     Vec_IntFreeP( &p->vClassUpdates );
     Vec_IntFreeP( &p->vCexStamps );
+    Vec_IntFreeP( &p->vCands );
+    Vec_IntFreeP( &p->vVisit );
+    Vec_IntFreeP( &p->vPat );
     ABC_FREE( p );
 }
 
@@ -471,6 +442,11 @@ static inline void Cec4_ObjSimSetInputBit( Gia_Man_t * p, int iObj, int Bit )
     if ( Abc_InfoHasBit( (unsigned*)pSim, p->iPatsPi ) != Bit )
         Abc_InfoXorBit( (unsigned*)pSim, p->iPatsPi );
 }
+static inline int Cec4_ObjSimGetInputBit( Gia_Man_t * p, int iObj )
+{
+    word * pSim = Cec4_ObjSim( p, iObj );
+    return Abc_InfoHasBit( (unsigned*)pSim, p->iPatsPi );
+}
 static inline void Cec4_ObjSimRo( Gia_Man_t * p, int iObj )
 {
     int w;
@@ -661,7 +637,7 @@ void Cec4_ManPrintTfiConeStats( Gia_Man_t * p )
     Vec_IntFree( vNodes );
     Vec_IntFree( vLeaves );
 }
-void Cec4_ManPrintStats( Gia_Man_t * p, Cec4_Par_t * pPars, Cec4_Man_t * pMan )
+void Cec4_ManPrintStats( Gia_Man_t * p, Cec_ParFra_t * pPars, Cec4_Man_t * pMan )
 {
     if ( !pPars->fVerbose )
         return;
@@ -806,7 +782,6 @@ int Cec4_ManVerify_rec( Gia_Man_t * p, int iObj, bmcg_sat_solver * pSat )
         return pObj->fMark1;
     Gia_ObjSetTravIdCurrentId(p, iObj);
     if ( Gia_ObjIsCi(pObj) )
-//        return pObj->fMark1 = satoko_var_polarity(pSat, Cec4_ObjSatId(p, pObj)) == SATOKO_LIT_TRUE;
         return pObj->fMark1 = bmcg_sat_solver_read_cex_varvalue(pSat, Cec4_ObjSatId(p, pObj));
     assert( Gia_ObjIsAnd(pObj) );
     Value0 = Cec4_ManVerify_rec( p, Gia_ObjFaninId0(pObj, iObj), pSat ) ^ Gia_ObjFaninC0(pObj);
@@ -828,6 +803,174 @@ void Cec4_ManVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase, bmcg_sat_s
 
 /**Function*************************************************************
 
+  Synopsis    [Verify counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec4_ManCexVerify_rec( Gia_Man_t * p, int iObj )
+{
+    int Value0, Value1;
+    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+    if ( iObj == 0 ) return 0;
+    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+        return pObj->fMark1;
+    Gia_ObjSetTravIdCurrentId(p, iObj);
+    if ( Gia_ObjIsCi(pObj) )
+        return pObj->fMark1 = Cec4_ObjSimGetInputBit(p, iObj);
+    assert( Gia_ObjIsAnd(pObj) );
+    Value0 = Cec4_ManCexVerify_rec( p, Gia_ObjFaninId0(pObj, iObj) ) ^ Gia_ObjFaninC0(pObj);
+    Value1 = Cec4_ManCexVerify_rec( p, Gia_ObjFaninId1(pObj, iObj) ) ^ Gia_ObjFaninC1(pObj);
+    return pObj->fMark1 = Value0 & Value1;
+}
+void Cec4_ManCexVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase )
+{
+    int Value0, Value1;
+    Gia_ManIncrementTravId( p );
+    Value0 = Cec4_ManCexVerify_rec( p, iObj0 );
+    Value1 = Cec4_ManCexVerify_rec( p, iObj1 );
+    if ( (Value0 ^ Value1) == fPhase )
+        printf( "CEX verification FAILED for obj %d and obj %d.\n", iObj0, iObj1 );
+//    else
+//        printf( "CEX verification succeeded for obj %d and obj %d.\n", iObj0, iObj1 );;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Generates counter-examples to refine the candidate equivalences.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cec4_ObjFan0HasValue( Gia_Obj_t * pObj, int v )
+{
+    return (v ^ Gia_ObjFaninC0(pObj)) ? Gia_ObjFanin0(pObj)->fMark1 : Gia_ObjFanin0(pObj)->fMark0;
+}
+static inline int Cec4_ObjFan1HasValue( Gia_Obj_t * pObj, int v )
+{
+    return (v ^ Gia_ObjFaninC1(pObj)) ? Gia_ObjFanin1(pObj)->fMark1 : Gia_ObjFanin1(pObj)->fMark0;
+}
+int Cec4_ManGeneratePatterns_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int Value, Vec_Int_t * vPat, Vec_Int_t * vVisit )
+{
+    Gia_Obj_t * pFan0, * pFan1;
+    assert( !pObj->fMark0 && !pObj->fMark1 ); // not visited
+    if ( Value ) pObj->fMark1 = 1; else pObj->fMark0 = 1;
+    Vec_IntPush( vVisit, Gia_ObjId(p, pObj) );
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        Vec_IntPush( vPat, Abc_Var2Lit(Gia_ObjId(p, pObj), Value) );
+        return 1;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    pFan0 = Gia_ObjFanin0(pObj);
+    pFan1 = Gia_ObjFanin1(pObj);
+    if ( Value )
+    {
+        if ( Cec4_ObjFan0HasValue(pObj, 0) || Cec4_ObjFan1HasValue(pObj, 0) )
+            return 0;
+        if ( !Cec4_ObjFan0HasValue(pObj, 1) && !Cec4_ManGeneratePatterns_rec(p, pFan0, !Gia_ObjFaninC0(pObj), vPat, vVisit) )
+            return 0;
+        if ( !Cec4_ObjFan1HasValue(pObj, 1) && !Cec4_ManGeneratePatterns_rec(p, pFan1, !Gia_ObjFaninC1(pObj), vPat, vVisit) )
+            return 0;
+        assert( Cec4_ObjFan0HasValue(pObj, 1) && Cec4_ObjFan1HasValue(pObj, 1) );
+        return 1;
+    }
+    else
+    {
+        if ( Cec4_ObjFan0HasValue(pObj, 1) && Cec4_ObjFan1HasValue(pObj, 1) )
+            return 0;
+        if ( Cec4_ObjFan0HasValue(pObj, 0) || Cec4_ObjFan1HasValue(pObj, 0) )
+            return 1;
+        if ( Cec4_ObjFan0HasValue(pObj, 1) )
+        {
+            if ( !Cec4_ManGeneratePatterns_rec(p, pFan1, Gia_ObjFaninC1(pObj), vPat, vVisit) )
+                return 0;
+        }
+        else if ( Cec4_ObjFan1HasValue(pObj, 1) )
+        {
+            if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, Gia_ObjFaninC0(pObj), vPat, vVisit) )
+                return 0;
+        }
+        else if ( Abc_Random(0) & 1 )
+        {
+            if ( !Cec4_ManGeneratePatterns_rec(p, pFan1, Gia_ObjFaninC1(pObj), vPat, vVisit) )
+                return 0;
+        }
+        else
+        {
+            if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, Gia_ObjFaninC0(pObj), vPat, vVisit) )
+                return 0;
+        }
+        assert( Cec4_ObjFan0HasValue(pObj, 0) || Cec4_ObjFan1HasValue(pObj, 0) );
+        return 1;
+    }
+}
+int Cec4_ManGeneratePatternOne( Gia_Man_t * p, int iRepr, int iReprVal, int iCand, int iCandVal, Vec_Int_t * vPat, Vec_Int_t * vVisit )
+{
+    int Res, k;
+    Gia_Obj_t * pObj;
+    assert( iCand > 0 );
+    if ( !iRepr && iReprVal )
+        return 0;
+    Vec_IntClear( vPat );
+    Vec_IntClear( vVisit );
+    //Gia_ManForEachObj( p, pObj, k )
+    //    assert( !pObj->fMark0 && !pObj->fMark1 );
+    Res = (!iRepr || Cec4_ManGeneratePatterns_rec(p, Gia_ManObj(p, iRepr), iReprVal, vPat, vVisit)) && Cec4_ManGeneratePatterns_rec(p, Gia_ManObj(p, iCand), iCandVal, vPat, vVisit);
+    Gia_ManForEachObjVec( vVisit, p, pObj, k )
+        pObj->fMark0 = pObj->fMark1 = 0;
+    return Res;
+}
+void Cec4_ManGeneratePatterns( Cec4_Man_t * p )
+{
+    abctime clk = Abc_Clock();
+    int i, k, iLit, nPats = 64 * p->pAig->nSimWords;
+    Gia_Obj_t * pObj;
+    // collect candidate nodes
+    Vec_IntClear( p->vCands );
+    Gia_ManForEachObj( p->pAig, pObj, i )
+    {
+        pObj->fMark0 = pObj->fMark1 = 0;
+        if ( !Gia_ObjIsHead(p->pAig, i) )
+            continue;
+        Gia_ClassForEachObj1( p->pAig, i, k )
+            Vec_IntPush( p->vCands, k );
+    }
+    // generate the given number of patterns
+    for ( i = 0, p->pAig->iPatsPi = 1; i < p->pPars->nGenIters * nPats && p->pAig->iPatsPi < nPats; p->pAig->iPatsPi++, i++ )
+    {
+        int iCand    = Vec_IntEntry( p->vCands, Abc_Random(0) % Vec_IntSize(p->vCands) );
+        int iRepr    = Gia_ObjRepr( p->pAig, iCand );
+        int iCandVal = Gia_ManObj(p->pAig, iCand)->fPhase;
+        int iReprVal = Gia_ManObj(p->pAig, iRepr)->fPhase;
+        int Res = Cec4_ManGeneratePatternOne( p->pAig, iRepr,  iReprVal, iCand, !iCandVal, p->vPat, p->vVisit );
+        if ( !Res )
+            Res = Cec4_ManGeneratePatternOne( p->pAig, iRepr, !iReprVal, iCand,  iCandVal, p->vPat, p->vVisit );
+        if ( !Res )
+            p->pAig->iPatsPi--;
+        else
+        {
+            // record this pattern
+            Vec_IntForEachEntry( p->vPat, iLit, k )
+                Cec4_ObjSimSetInputBit( p->pAig, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) );
+            //Cec4_ManCexVerify( p->pAig, iRepr, iCand, iReprVal ^ iCandVal );
+            //Gia_ManCleanMark01( p->pAig );
+        }
+    }
+    //printf( "Generated %d CEXs after trying %d candidate equivalence pairs.\n", p->pAig->iPatsPi-1, i );
+    p->timeGenPats += Abc_Clock() - clk;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Internal simulation APIs.]
 
   Description []
@@ -841,6 +984,7 @@ void Cec4_ManSatSolverRecycle( Cec4_Man_t * p )
 {
     Gia_Obj_t * pObj;
     int i;
+    //printf( "Solver size = %d.\n", bmcg_sat_solver_varnum(p->pSat) );
     p->nRecycles++;
     p->nCallsSince = 0;
     bmcg_sat_solver_reset( p->pSat );
@@ -852,6 +996,7 @@ void Cec4_ManSatSolverRecycle( Cec4_Man_t * p )
 }
 int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pfEasy, int fVerbose )
 {
+    abctime clk;
     int nConfEnd, nConfBeg;
     int status, iVar0, iVar1, Lits[2];
     int UnsatConflicts[3] = {0};
@@ -867,12 +1012,14 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
     // add more logic to the solver
     if ( !iObj0 && Cec4_ObjSatId(p->pNew, Gia_ManConst0(p->pNew)) == -1 )
         Cec4_ObjSetSatId( p->pNew, Gia_ManConst0(p->pNew), bmcg_sat_solver_addvar(p->pSat) );
+    clk = Abc_Clock();
     iVar0 = Cec4_ObjGetCnfVar( p, iObj0 );
     iVar1 = Cec4_ObjGetCnfVar( p, iObj1 );
+    p->timeCnf += Abc_Clock() - clk;
     // perform solving
     Lits[0] = Abc_Var2Lit(iVar0, 1);
     Lits[1] = Abc_Var2Lit(iVar1, fPhase);
-    bmcg_sat_solver_set_conflict_budget( p->pSat, p->pPars->nConfLimit );
+    bmcg_sat_solver_set_conflict_budget( p->pSat, p->pPars->nBTLimit );
     nConfBeg = bmcg_sat_solver_conflictnum( p->pSat );
     status = bmcg_sat_solver_solve( p->pSat, Lits, 2 );
     nConfEnd = bmcg_sat_solver_conflictnum( p->pSat );
@@ -907,7 +1054,7 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
     {
         Lits[0] = Abc_Var2Lit(iVar0, 0);
         Lits[1] = Abc_Var2Lit(iVar1, !fPhase);
-        bmcg_sat_solver_set_conflict_budget( p->pSat, p->pPars->nConfLimit );
+        bmcg_sat_solver_set_conflict_budget( p->pSat, p->pPars->nBTLimit );
         nConfBeg = bmcg_sat_solver_conflictnum( p->pSat );
         status = bmcg_sat_solver_solve( p->pSat, Lits, 2 );
         nConfEnd = bmcg_sat_solver_conflictnum( p->pSat );
@@ -1028,20 +1175,19 @@ Gia_Obj_t * Cec4_ManFindRepr( Gia_Man_t * p, Cec4_Man_t * pMan, int iObj )
     pMan->timeResimLoc += Abc_Clock() - clk;
     return NULL;
 }
-int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec4_Par_t * pPars, Gia_Man_t ** ppNew )
+int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew )
 {
     Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars ); 
     Gia_Obj_t * pObj, * pRepr; int i;
-    //Gia_Obj_t * pObjNew; 
     if ( pPars->fVerbose )
-        printf( "Simulating %d words for %d rounds. SAT solving with %d conflicts. Recycle after %d SAT calls.\n", 
-            pPars->nSimWords, pPars->nSimRounds, pPars->nConfLimit, pPars->nCallsRecycle );
+        printf( "Simulate %d words in %d rounds. Easy SAT with %d tries. SAT with %d confs. Recycle after %d SAT calls.\n", 
+            pPars->nWords, pPars->nRounds, pPars->nGenIters, pPars->nBTLimit, pPars->nCallsRecycle );
 
     // check if any output trivially fails under all-0 pattern
     Gia_ManRandomW( 1 );
     Gia_ManSetPhase( p );
     Gia_ManStaticFanoutStart( p );
-    if ( pPars->fIsMiter ) 
+    if ( pPars->fCheckMiter ) 
     {
         Gia_ManForEachCo( p, pObj, i )
             if ( pObj->fPhase )
@@ -1052,28 +1198,31 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec4_Par_t * pPars, Gia_Man_t ** ppN
     }
 
     // simulate one round and create classes
-    Cec4_ManSimAlloc( p, pPars->nSimWords );
+    Cec4_ManSimAlloc( p, pPars->nWords );
     Cec4_ManSimulateCis( p );
     Cec4_ManSimulate( p, pMan, 0 );
-    if ( pPars->fIsMiter && !Cec4_ManSimulateCos(p) ) // cex detected
+    if ( pPars->fCheckMiter && !Cec4_ManSimulateCos(p) ) // cex detected
         goto finalize;
     Cec4_ManCreateClasses( p, pMan );
     if ( pPars->fVerbose )
         Cec4_ManPrintStats( p, pPars, pMan );
 
     // perform additional simulation
-    for ( i = 0; i < pPars->nSimRounds; i++ )
+    for ( i = 0; i < pPars->nRounds; i++ )
     {
         Cec4_ManSimulateCis( p );
+        if ( i >= pPars->nRounds/3 )
+            Cec4_ManGeneratePatterns( pMan );
         Cec4_ManSimulate( p, pMan, 1 );
-        if ( pPars->fIsMiter && !Cec4_ManSimulateCos(p) ) // cex detected
+        if ( pPars->fCheckMiter && !Cec4_ManSimulateCos(p) ) // cex detected
             goto finalize;
-        if ( i % (pPars->nSimRounds / 5) == 0 && pPars->fVerbose )
+        if ( i % (pPars->nRounds / 5) == 0 && pPars->fVerbose )
             Cec4_ManPrintStats( p, pPars, pMan );
     }
     p->iPatsPi = 0;
     Gia_ManForEachAnd( p, pObj, i )
     {
+        //Gia_Obj_t * pObjNew; 
         pObj->Value = Gia_ManHashAnd( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         //pObjNew = Gia_ManObj( pMan->pNew, Abc_Lit2Var(pObj->Value) );
         //if ( Gia_ObjIsAnd(pObjNew) )
@@ -1130,17 +1279,10 @@ finalize:
     //Gia_ManEquivPrintClasses( p, 1, 0 );
     return p->pCexSeq ? 0 : 1;
 }
-Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars0 )
+Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
 {
     Gia_Man_t * pNew = NULL;
-    //abctime clk = Abc_Clock();
-    Cec4_Par_t Pars, * pPars = &Pars;
-    Cec4_SetDefaultParams( pPars );
-    pPars->nConfLimit = pPars0->nBTLimit;   // conflict limit at a node
-    pPars->fUseCones  = pPars0->fUseCones;
-    pPars->fVerbose   = pPars0->fVerbose;
     Cec4_ManPerformSweeping( p, pPars, &pNew );
-    //Abc_PrintTime( 1, "SAT sweeping time", Abc_Clock() - clk );
     return pNew;
 }