diff options
Diffstat (limited to 'src/prop/sat_solver.h')
-rw-r--r-- | src/prop/sat_solver.h | 184 |
1 files changed, 35 insertions, 149 deletions
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 56c6c2783..3b8e1ccbf 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -26,24 +26,6 @@ #include "util/stats.h" #include "context/cdlist.h" -// DPLLT Minisat -#include "prop/minisat/core/SolverTypes.h" - -// BV Minisat -#include "prop/bvminisat/core/SolverTypes.h" - - -namespace Minisat{ -class Solver; -class SimpSolver; -} - -namespace BVMinisat{ -class Solver; -class SimpSolver; -} - - namespace CVC4 { namespace prop { @@ -55,7 +37,6 @@ enum SatLiteralValue { SatValFalse }; - typedef uint64_t SatVariable; // special constant const SatVariable undefSatVariable = SatVariable(-1); @@ -154,144 +135,49 @@ public: }; -// toodo add ifdef - - -class MinisatSatSolver: public BVSatSolverInterface { - BVMinisat::SimpSolver* d_minisat; - - MinisatSatSolver(); +class SatSolverFactory { public: - ~MinisatSatSolver(); - void addClause(SatClause& clause, bool removable); - - SatVariable newVar(bool theoryAtom = false); - - void markUnremovable(SatLiteral lit); - - void interrupt(); - - SatLiteralValue solve(); - SatLiteralValue solve(long unsigned int&); - SatLiteralValue solve(const context::CDList<SatLiteral> & assumptions); - void getUnsatCore(SatClause& unsatCore); - - SatLiteralValue value(SatLiteral l); - SatLiteralValue modelValue(SatLiteral l); - - void unregisterVar(SatLiteral lit); - void renewVar(SatLiteral lit, int level = -1); - int getAssertionLevel() const; - - - // helper methods for converting from the internal Minisat representation - - static SatVariable toSatVariable(BVMinisat::Var var); - static BVMinisat::Lit toMinisatLit(SatLiteral lit); - static SatLiteral toSatLiteral(BVMinisat::Lit lit); - static SatLiteralValue toSatLiteralValue(bool res); - static SatLiteralValue toSatLiteralValue(BVMinisat::lbool res); - - static void toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause); - static void toSatClause (BVMinisat::vec<BVMinisat::Lit>& clause, SatClause& sat_clause); - - class Statistics { - public: - ReferenceStat<uint64_t> d_statStarts, d_statDecisions; - ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations; - ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals; - ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals; - ReferenceStat<uint64_t> d_statTotLiterals; - ReferenceStat<int> d_statEliminatedVars; - Statistics(); - ~Statistics(); - void init(BVMinisat::SimpSolver* minisat); - }; - - Statistics d_statistics; - friend class SatSolverFactory; + static BVSatSolverInterface* createMinisat(); + static DPLLSatSolverInterface* createDPLLMinisat(); }; +}/* prop namespace */ -class DPLLMinisatSatSolver : public DPLLSatSolverInterface { - - /** The SatSolver used */ - Minisat::SimpSolver* d_minisat; - - - /** The SatSolver uses this to communicate with the theories */ - TheoryProxy* d_theoryProxy; - - /** Context we will be using to synchronzie the sat solver */ - context::Context* d_context; - - DPLLMinisatSatSolver (); - -public: - - ~DPLLMinisatSatSolver(); - static SatVariable toSatVariable(Minisat::Var var); - static Minisat::Lit toMinisatLit(SatLiteral lit); - static SatLiteral toSatLiteral(Minisat::Lit lit); - static SatLiteralValue toSatLiteralValue(bool res); - static SatLiteralValue toSatLiteralValue(Minisat::lbool res); - - static void toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause); - static void toSatClause (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause); - - void initialize(context::Context* context, TheoryProxy* theoryProxy); - - void addClause(SatClause& clause, bool removable); - - SatVariable newVar(bool theoryAtom = false); - - SatLiteralValue solve(); - SatLiteralValue solve(long unsigned int&); - - void interrupt(); - - SatLiteralValue value(SatLiteral l); - - SatLiteralValue modelValue(SatLiteral l); - - bool properExplanation(SatLiteral lit, SatLiteral expl) const; - - /** Incremental interface */ - - int getAssertionLevel() const; - - void push(); - - void pop(); - - void unregisterVar(SatLiteral lit); - - void renewVar(SatLiteral lit, int level = -1); +inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { + out << lit.toString(); + return out; +} - class Statistics { - private: - ReferenceStat<uint64_t> d_statStarts, d_statDecisions; - ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations; - ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals; - ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals; - ReferenceStat<uint64_t> d_statTotLiterals; - public: - Statistics(); - ~Statistics(); - void init(Minisat::SimpSolver* d_minisat); - }; - Statistics d_statistics; +inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) { + out << "clause:"; + for(unsigned i = 0; i < clause.size(); ++i) { + out << " " << clause[i]; + } + out << ";"; + return out; +} - friend class SatSolverFactory; -}; +inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) { + std::string str; + switch(val) { + case prop::SatValUnknown: + str = "_"; + break; + case prop::SatValTrue: + str = "1"; + break; + case prop::SatValFalse: + str = "0"; + break; + default: + str = "Error"; + break; + } -class SatSolverFactory { -public: - static MinisatSatSolver* createMinisat(); - static DPLLMinisatSatSolver* createDPLLMinisat(); -}; + out << str; + return out; +} -}/* prop namespace */ }/* CVC4 namespace */ #endif /* __CVC4__PROP__SAT_MODULE_H */ |