diff options
Diffstat (limited to 'src/prop/sat_solver.h')
-rw-r--r-- | src/prop/sat_solver.h | 41 |
1 files changed, 21 insertions, 20 deletions
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index d2e967393..567f897a1 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PROP__SAT_MODULE_H -#define __CVC4__PROP__SAT_MODULE_H +#ifndef __CVC4__PROP__SAT_SOLVER_H +#define __CVC4__PROP__SAT_SOLVER_H #include <string> #include <stdint.h> @@ -30,21 +30,21 @@ namespace CVC4 { namespace prop { -class TheoryProxy; +class TheoryProxy; class SatSolver { -public: +public: /** Virtual destructor */ virtual ~SatSolver() { } - + /** Assert a clause in the solver. */ virtual void addClause(SatClause& clause, bool removable) = 0; /** Create a new boolean variable in the solver. */ virtual SatVariable newVar(bool theoryAtom = false) = 0; - + /** Create a new (or return an existing) boolean variable representing the constant true */ virtual SatVariable trueVar() = 0; @@ -56,7 +56,7 @@ public: /** Check the satisfiability of the added clauses */ virtual SatValue solve(long unsigned int&) = 0; - + /** Interrupt the solver */ virtual void interrupt() = 0; @@ -67,12 +67,12 @@ public: virtual SatValue modelValue(SatLiteral l) = 0; virtual void unregisterVar(SatLiteral lit) = 0; - + virtual void renewVar(SatLiteral lit, int level = -1) = 0; virtual unsigned getAssertionLevel() const = 0; -}; +};/* class SatSolver */ class BVSatSolverInterface: public SatSolver { @@ -94,30 +94,31 @@ public: * Notify about a learnt clause. */ virtual void notify(SatClause& clause) = 0; - }; + };/* class BVSatSolverInterface::Notify */ + + virtual void setNotify(Notify* notify) = 0; - virtual void setNotify(Notify* notify) = 0; - virtual void markUnremovable(SatLiteral lit) = 0; - virtual void getUnsatCore(SatClause& unsatCore) = 0; + virtual void getUnsatCore(SatClause& unsatCore) = 0; - virtual void addMarkerLiteral(SatLiteral lit) = 0; + virtual void addMarkerLiteral(SatLiteral lit) = 0; virtual SatValue propagate() = 0; virtual void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0; - virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0; + virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0; virtual void popAssumption() = 0; -}; + +};/* class BVSatSolverInterface */ class DPLLSatSolverInterface: public SatSolver { public: - virtual void initialize(context::Context* context, prop::TheoryProxy* theoryProxy) = 0; - + virtual void initialize(context::Context* context, prop::TheoryProxy* theoryProxy) = 0; + virtual void push() = 0; virtual void pop() = 0; @@ -130,9 +131,9 @@ public: virtual bool isDecision(SatVariable decn) const = 0; -}; +};/* class DPLLSatSolverInterface */ -}/* prop namespace */ +}/* CVC4::prop namespace */ inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { out << lit.toString(); |