diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-03-01 13:59:23 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-03-01 13:59:23 -0800 |
| commit | bd9b7d64e1131f45699a5a4b20b4bf44795da857 (patch) | |
| tree | 3e6a6b9f243519bf31635e3efb9bf85bf450b201 /src/sat/bsat/satSolver.h | |
| parent | b71d2ab2ba4dd1da265845a94439c36a38e9d8d3 (diff) | |
| download | abc-bd9b7d64e1131f45699a5a4b20b4bf44795da857.tar.gz abc-bd9b7d64e1131f45699a5a4b20b4bf44795da857.tar.bz2 abc-bd9b7d64e1131f45699a5a4b20b4bf44795da857.zip | |
Adding efficient procedure to minimize the set of assumptions.
Diffstat (limited to 'src/sat/bsat/satSolver.h')
| -rw-r--r-- | src/sat/bsat/satSolver.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 5a8483c1..ac0b6e8d 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -50,6 +50,7 @@ extern int sat_solver_simplify(sat_solver* s); extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); extern int sat_solver_solve_internal(sat_solver* s); extern int sat_solver_solve_lexsat(sat_solver* s, int * pLits, int nLits); +extern int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int nConfLimit ); extern int sat_solver_push(sat_solver* s, int p); extern void sat_solver_pop(sat_solver* s); extern void sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); |