diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/sat/satoko/satoko.h | 12 | ||||
| -rw-r--r-- | src/sat/satoko/solver.c | 5 | ||||
| -rw-r--r-- | src/sat/satoko/solver.h | 13 | ||||
| -rw-r--r-- | src/sat/satoko/solver_api.c | 36 |
4 files changed, 44 insertions, 22 deletions
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h index 2095a650..537cc394 100644 --- a/src/sat/satoko/satoko.h +++ b/src/sat/satoko/satoko.h @@ -86,13 +86,15 @@ extern void satoko_reset(satoko_t *); extern void satoko_default_opts(satoko_opts_t *); extern void satoko_configure(satoko_t *, satoko_opts_t *); extern int satoko_parse_dimacs(char *, satoko_t **); +extern void satoko_setnvars(satoko_t *, int); extern int satoko_add_variable(satoko_t *, char); extern int satoko_add_clause(satoko_t *, int *, int); extern void satoko_assump_push(satoko_t *s, int); extern void satoko_assump_pop(satoko_t *s); extern int satoko_simplify(satoko_t *); extern int satoko_solve(satoko_t *); -extern int satoko_solve_with_assumptions(satoko_t *s, int * plits, int nlits); +extern int satoko_solve_assumptions(satoko_t *s, int * plits, int nlits); +extern int satoko_solve_assumptions_limit(satoko_t *s, int * plits, int nlits, int nconflim); extern void satoko_mark_cone(satoko_t *, int *, int); extern void satoko_unmark_cone(satoko_t *, int *, int); @@ -101,14 +103,12 @@ extern void satoko_bookmark(satoko_t *); extern void satoko_unbookmark(satoko_t *); /* If problem is unsatisfiable under assumptions, this function is used to * obtain the final conflict clause expressed in the assumptions. - * - * - It receives as inputs the solver and a pointer to a array where clause - * will be copied. The memory is allocated by the solver, but must be freed by - * the caller. + * - It receives as inputs the solver and a pointer to an array where clause + * is stored. The memory for the clause is managed by the solver. * - The return value is either the size of the array or -1 in case the final * conflict cluase was not generated. */ -extern int satoko_final_conflict(satoko_t *, unsigned *); +extern int satoko_final_conflict(satoko_t *, int **); /* Procedure to dump a DIMACS file. * - It receives as input the solver, a file name string and two integers. diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index 3cf7bb5f..51befd16 100644 --- a/src/sat/satoko/solver.c +++ b/src/sat/satoko/solver.c @@ -639,7 +639,8 @@ char solver_search(solver_t *s) /* No conflict */ unsigned next_lit; - if (solver_rst(s) || solver_check_limits(s) == 0 || solver_stop(s)) { + if (solver_rst(s) || solver_check_limits(s) == 0 || solver_stop(s) || + (s->nRuntimeLimit && (s->stats.n_conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)) { b_queue_clean(s->bq_lbd); solver_cancel_until(s, 0); return SATOKO_UNDEC; @@ -648,7 +649,7 @@ char solver_search(solver_t *s) satoko_simplify(s); /* Reduce the set of learnt clauses */ - if (s->opts.learnt_ratio && + if (s->opts.learnt_ratio && vec_uint_size(s->learnts) > 100 && s->stats.n_conflicts >= s->n_confl_bfr_reduce) { s->RC1 = (s->stats.n_conflicts / s->RC2) + 1; solver_reduce_cdb(s); diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h index 4abf9979..d6f7d75e 100644 --- a/src/sat/satoko/solver.h +++ b/src/sat/satoko/solver.h @@ -103,8 +103,11 @@ struct solver_t_ { /* Temporary data used for solving cones */ vec_char_t *marks; - /* Callback to stop the solver */ - int * pstop; + /* Callbacks to stop the solver */ + abctime nRuntimeLimit; + int *pstop; + int RunId; + int (*pFuncStop)(int); struct satoko_stats stats; struct satoko_opts opts; @@ -251,6 +254,12 @@ static inline int solver_read_cex_varvalue(solver_t *s, int ivar) { return var_polarity(s, ivar) == LIT_TRUE; } +static abctime solver_set_runtime_limit(solver_t* s, abctime Limit) +{ + abctime nRuntimeLimit = s->nRuntimeLimit; + s->nRuntimeLimit = Limit; + return nRuntimeLimit; +} //===------------------------------------------------------------------------=== // Inline clause functions diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index 54987007..8784a761 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -218,6 +218,13 @@ int satoko_simplify(solver_t * s) return SATOKO_OK; } +void satoko_setnvars(solver_t *s, int nvars) +{ + int i; + for (i = solver_varnum(s); i < nvars; i++) + satoko_add_variable(s, 0); +} + int satoko_add_variable(solver_t *s, char sign) { unsigned var = vec_act_size(s->activity); @@ -305,6 +312,10 @@ int satoko_solve(solver_t *s) status = solver_search(s); if (solver_check_limits(s) == 0 || solver_stop(s)) break; + if (s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit) + break; + if (s->pFuncStop && s->pFuncStop(s->RunId)) + break; } if (s->opts.verbose) print_stats(s); @@ -313,7 +324,7 @@ int satoko_solve(solver_t *s) return status; } -int satoko_solve_with_assumptions(solver_t *s, int * plits, int nlits) +int satoko_solve_assumptions(solver_t *s, int * plits, int nlits) { int i, status; for ( i = 0; i < nlits; i++ ) @@ -321,20 +332,21 @@ int satoko_solve_with_assumptions(solver_t *s, int * plits, int nlits) status = satoko_solve( s ); for ( i = 0; i < nlits; i++ ) satoko_assump_pop( s ); - if ( status == SATOKO_UNSAT ) - return 1; - if ( status == SATOKO_SAT ) - return 0; - return -1; + return status; +} + +int satoko_solve_assumptions_limit(satoko_t *s, int * plits, int nlits, int nconflim) +{ + int temp = s->opts.conf_limit, status; + s->opts.conf_limit = nconflim; + status = satoko_solve_assumptions(s, plits, nlits); + s->opts.conf_limit = temp; + return status; } -int satoko_final_conflict(solver_t *s, unsigned *out) +int satoko_final_conflict(solver_t *s, int **out) { - if (vec_uint_size(s->final_conflict) == 0) - return -1; - out = satoko_alloc(unsigned, vec_uint_size(s->final_conflict)); - memcpy(out, vec_uint_data(s->final_conflict), - sizeof(unsigned) * vec_uint_size(s->final_conflict)); + *out = (int *)vec_uint_data(s->final_conflict); return vec_uint_size(s->final_conflict); } |