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

Adding a callback feature to Satoko.

This commit is contained in:
Alan Mishchenko 2017-08-13 13:37:36 +07:00
parent cf427690a5
commit b39b55e885
3 changed files with 13 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/sat/satoko/solver.c
View File

@ -639,7 +639,7 @@ char solver_search(solver_t *s)
/* No conflict */
unsigned next_lit;
if (solver_rst(s) || solver_check_limits(s) == 0) {
if (solver_rst(s) || solver_check_limits(s) == 0 || solver_stop(s)) {
b_queue_clean(s->bq_lbd);
solver_cancel_until(s, 0);
return SATOKO_UNDEC;

11
src/sat/satoko/solver.h
View File

@ -102,6 +102,9 @@ struct solver_t_ {
/* Temporary data used for solving cones */
vec_char_t *marks;
/* Callback to stop the solver */
int * pstop;
struct satoko_stats stats;
struct satoko_opts opts;
@ -223,6 +226,14 @@ static inline int solver_has_marks(solver_t *s)
{
return (int)(s->marks != NULL);
}
static inline int solver_stop(solver_t *s)
{
return s->pstop && *s->pstop;
}
static inline void solver_set_stop(solver_t *s, int * pstop)
{
s->pstop = pstop;
}
//===------------------------------------------------------------------------===
// Inline clause functions

2
src/sat/satoko/solver_api.c
View File

@ -303,7 +303,7 @@ int satoko_solve(solver_t *s)
while (status == SATOKO_UNDEC) {
status = solver_search(s);
if (solver_check_limits(s) == 0)
if (solver_check_limits(s) == 0 || solver_stop(s))
break;
}
if (s->opts.verbose)