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

added callbacks to bmc3 and sat solver

This commit is contained in:
Yen-Sheng Ho 2017-03-20 19:13:40 -07:00
parent 245532cad1
commit bacc1bc12c
3 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/sat/bmc/bmcBmc3.c
View File

@ -1416,6 +1416,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
p->pSat->nLearntMax = p->pSat->nLearntStart;
p->pSat->fNoRestarts = p->pPars->fNoRestarts;
p->pSat->RunId = p->pPars->RunId;
p->pSat->pFuncStop = p->pPars->pFuncStop;
if ( pPars->fSolveAll && p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
if ( pPars->fVerbose )

2
src/sat/bsat/satSolver.c
View File

@ -1956,6 +1956,8 @@ int sat_solver_solve_internal(sat_solver* s)
break;
if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
break;
if ( s->pFuncStop && s->pFuncStop(s->RunId) )
break;
}
if (s->verbosity >= 1)
printf("==============================================================================\n");

4
src/sat/bsat/satSolver.h
View File

@ -196,6 +196,10 @@ struct sat_solver_t
// CNF loading
void * pCnfMan; // external CNF manager
int(*pCnfFunc)(void * p, int); // external callback
// termination callback
int RunId; // SAT id in this run
int(*pFuncStop)(int); // callback to terminate
};
static inline clause * clause_read( sat_solver * s, cla h )