luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Experiments with SAT sweeping.

This commit is contained in:
Alan Mishchenko 2020-11-10 23:15:42 -08:00
parent 3da87edbb4
commit c0bb4bb047
3 changed files with 235 additions and 74 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
src/base/abci/abc.c
View File

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

3
src/proof/cec/cec.h
View File

@ -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

276
src/proof/cec/cecSatG2.c
View File

@ -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;
@ -90,32 +79,6 @@ static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj )
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**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 []
@ -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);
@ -826,6 +801,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.]
@ -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;
}