diff options
Diffstat (limited to 'src/prop/sat_solver.h')
-rw-r--r-- | src/prop/sat_solver.h | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 1c1dae410..1383308a3 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -30,10 +30,15 @@ #include "util/statistics_registry.h" namespace CVC4 { + +class BitVectorProof; + namespace prop { class TheoryProxy; +typedef unsigned ClauseId; + class SatSolver { public: @@ -42,7 +47,8 @@ public: virtual ~SatSolver() throw(AssertionException) { } /** Assert a clause in the solver. */ - virtual void addClause(SatClause& clause, bool removable, uint64_t proof_id) = 0; + virtual ClauseId addClause(SatClause& clause, + bool removable) = 0; /** * Create a new boolean variable in the solver. @@ -77,6 +83,10 @@ public: /** Get the current assertion level */ virtual unsigned getAssertionLevel() const = 0; + /** Check if the solver is in an inconsistent state */ + virtual bool ok() const = 0; + + };/* class SatSolver */ @@ -121,6 +131,10 @@ public: virtual void popAssumption() = 0; + virtual bool ok() const = 0; + + virtual void setProofLog( BitVectorProof * bvp ) {} + };/* class BVSatSolverInterface */ @@ -139,7 +153,8 @@ public: virtual bool flipDecision() = 0; virtual bool isDecision(SatVariable decn) const = 0; - + + virtual bool ok() const = 0; };/* class DPLLSatSolverInterface */ inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { |