summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c30
-rw-r--r--src/proof/cec/cec.h3
-rw-r--r--src/proof/cec/cecSatG2.c276
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;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-15 02:05:30 +0000