diff options
Diffstat (limited to 'src/prop/minisat/minisat.h')
| -rw-r--r-- | src/prop/minisat/minisat.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 42588080d..74b7ab749 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -58,6 +58,8 @@ class MinisatSatSolver : public CDCLTSatSolverInterface SatValue solve() override; SatValue solve(long unsigned int&) override; + SatValue solve(const std::vector<SatLiteral>& assumptions) override; + void getUnsatAssumptions(std::vector<SatLiteral>& unsat_assumptions) override; bool ok() const override; @@ -100,6 +102,14 @@ class MinisatSatSolver : public CDCLTSatSolverInterface /** Context we will be using to synchronize the sat solver */ context::Context* d_context; + /** + * Stores assumptions passed via last solve() call. + * + * It is used in getUnsatAssumptions() to determine which of the literals in + * the final conflict clause are assumptions. + */ + std::unordered_set<SatLiteral, SatLiteralHashFunction> d_assumptions; + void setupOptions(); class Statistics { |