diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
commit | 52d6dc20c61007a5c066590aa1fd0b95ed3c2527 (patch) | |
tree | 040efec36cde7775b5c19eb43fcdd60cbeb61f9e /src/prop/sat_solver.h | |
parent | 4fa8c7d1a0654e7780fd485c51463c06b34379b5 (diff) |
* added propagation as lemmas to TheoryBV:
* modified BVMinisat to work incrementally
* added more bv regressions
Diffstat (limited to 'src/prop/sat_solver.h')
-rw-r--r-- | src/prop/sat_solver.h | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index f18335048..4fe24fc60 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -72,11 +72,20 @@ public: class BVSatSolverInterface: public SatSolver { public: - virtual SatValue solve(const context::CDList<SatLiteral> & assumptions) = 0; virtual void markUnremovable(SatLiteral lit) = 0; virtual void getUnsatCore(SatClause& unsatCore) = 0; + + virtual void addMarkerLiteral(SatLiteral lit) = 0; + + virtual bool getPropagations(std::vector<SatLiteral>& propagations) = 0; + + virtual void explainPropagation(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0; + + virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0; + + virtual void popAssumption() = 0; }; |