summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorYen-Sheng Ho <ysho@berkeley.edu>2017-03-20 19:13:40 -0700
committerYen-Sheng Ho <ysho@berkeley.edu>2017-03-20 19:13:40 -0700
commitbacc1bc12c946442c6709614093ad188282ffcfc (patch)
tree8a79ff3f764323e1340332fa2f8d966cedbf677e /src
parent245532cad1d93f1347dec39035d6db7f8eebc2c6 (diff)
downloadabc-bacc1bc12c946442c6709614093ad188282ffcfc.tar.gz
abc-bacc1bc12c946442c6709614093ad188282ffcfc.tar.bz2
abc-bacc1bc12c946442c6709614093ad188282ffcfc.zip
added callbacks to bmc3 and sat solver
Diffstat (limited to 'src')
-rw-r--r--src/sat/bmc/bmcBmc3.c2
-rw-r--r--src/sat/bsat/satSolver.c2
-rw-r--r--src/sat/bsat/satSolver.h4
3 files changed, 8 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 34fdf45f..a1011ae1 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -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 )
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index fe7e65fe..787626d6 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -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");
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 5191b2cd..e8a350ca 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -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 )