diff options
| author | Mathias Soeken <mathias.soeken@gmail.com> | 2017-03-03 10:33:59 +0100 |
|---|---|---|
| committer | Mathias Soeken <mathias.soeken@gmail.com> | 2017-03-03 10:33:59 +0100 |
| commit | f03871ab22b6c8a487e8fce19ab6b8a540b849f8 (patch) | |
| tree | b2c4c1fad6f8b5ce111e0545ed34c89d38397fc9 /src/sat/bsat/satSolver.h | |
| parent | 28e8e7f3e79d1391a2f3a31cefe3afe234aa3b8e (diff) | |
| parent | b1907e909d92d1147937b26b5e97fb344647f719 (diff) | |
| download | abc-f03871ab22b6c8a487e8fce19ab6b8a540b849f8.tar.gz abc-f03871ab22b6c8a487e8fce19ab6b8a540b849f8.tar.bz2 abc-f03871ab22b6c8a487e8fce19ab6b8a540b849f8.zip | |
Merged alanmi/abc into default
Diffstat (limited to 'src/sat/bsat/satSolver.h')
| -rw-r--r-- | src/sat/bsat/satSolver.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 5a8483c1..5191b2cd 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -50,6 +50,8 @@ 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_minimize_assumptions2( 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); |