From: Dejan Jovanović Date: Wed, 28 Mar 2012 15:44:30 +0000 (+0000) Subject: Some renaming and refactoring in SAT X-Git-Tag: cvc5-1.0.0~8257 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4d5d28e59c6338876e8436a5fc2b9e2dd6058e30;p=cvc5.git Some renaming and refactoring in SAT --- diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index e505c168e..730df70aa 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -16,6 +16,7 @@ libprop_la_SOURCES = \ cnf_stream.h \ cnf_stream.cpp \ sat_solver.h \ + sat_solver_types.h \ sat_solver_factory.h \ sat_solver_factory.cpp \ sat_solver_registry.h \ diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index c4c21e126..b32483cbe 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -22,17 +22,17 @@ using namespace CVC4; using namespace prop; -MinisatSatSolver::MinisatSatSolver() : +BVMinisatSatSolver::BVMinisatSatSolver() : d_minisat(new BVMinisat::SimpSolver()) { d_statistics.init(d_minisat); } -MinisatSatSolver::~MinisatSatSolver() { +BVMinisatSatSolver::~BVMinisatSatSolver() { delete d_minisat; } -void MinisatSatSolver::addClause(SatClause& clause, bool removable) { +void BVMinisatSatSolver::addClause(SatClause& clause, bool removable) { Debug("sat::minisat") << "Add clause " << clause <<"\n"; BVMinisat::vec minisat_clause; toMinisatClause(clause, minisat_clause); @@ -42,23 +42,23 @@ void MinisatSatSolver::addClause(SatClause& clause, bool removable) { d_minisat->addClause(minisat_clause); } -SatVariable MinisatSatSolver::newVar(bool freeze){ +SatVariable BVMinisatSatSolver::newVar(bool freeze){ return d_minisat->newVar(true, true, freeze); } -void MinisatSatSolver::markUnremovable(SatLiteral lit){ +void BVMinisatSatSolver::markUnremovable(SatLiteral lit){ d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true); } -void MinisatSatSolver::interrupt(){ +void BVMinisatSatSolver::interrupt(){ d_minisat->interrupt(); } -SatValue MinisatSatSolver::solve(){ +SatValue BVMinisatSatSolver::solve(){ return toSatLiteralValue(d_minisat->solve()); } -SatValue MinisatSatSolver::solve(long unsigned int& resource){ +SatValue BVMinisatSatSolver::solve(long unsigned int& resource){ Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; if(resource == 0) { d_minisat->budgetOff(); @@ -74,7 +74,7 @@ SatValue MinisatSatSolver::solve(long unsigned int& resource){ return result; } -SatValue MinisatSatSolver::solve(const context::CDList & assumptions){ +SatValue BVMinisatSatSolver::solve(const context::CDList & assumptions){ Debug("sat::minisat") << "Solve with assumptions "; context::CDList::const_iterator it = assumptions.begin(); BVMinisat::vec assump; @@ -90,58 +90,58 @@ SatValue MinisatSatSolver::solve(const context::CDList & assumptions } -void MinisatSatSolver::getUnsatCore(SatClause& unsatCore) { +void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) { // TODO add assertion to check the call was after an unsat call for (int i = 0; i < d_minisat->conflict.size(); ++i) { unsatCore.push_back(toSatLiteral(d_minisat->conflict[i])); } } -SatValue MinisatSatSolver::value(SatLiteral l){ +SatValue BVMinisatSatSolver::value(SatLiteral l){ Unimplemented(); return SAT_VALUE_UNKNOWN; } -SatValue MinisatSatSolver::modelValue(SatLiteral l){ +SatValue BVMinisatSatSolver::modelValue(SatLiteral l){ Unimplemented(); return SAT_VALUE_UNKNOWN; } -void MinisatSatSolver::unregisterVar(SatLiteral lit) { +void BVMinisatSatSolver::unregisterVar(SatLiteral lit) { // this should only be called when user context is implemented // in the BVSatSolver Unreachable(); } -void MinisatSatSolver::renewVar(SatLiteral lit, int level) { +void BVMinisatSatSolver::renewVar(SatLiteral lit, int level) { // this should only be called when user context is implemented // in the BVSatSolver Unreachable(); } -unsigned MinisatSatSolver::getAssertionLevel() const { +unsigned BVMinisatSatSolver::getAssertionLevel() const { // we have no user context implemented so far return 0; } // converting from internal Minisat representation -SatVariable MinisatSatSolver::toSatVariable(BVMinisat::Var var) { +SatVariable BVMinisatSatSolver::toSatVariable(BVMinisat::Var var) { if (var == var_Undef) { return undefSatVariable; } return SatVariable(var); } -BVMinisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) { +BVMinisat::Lit BVMinisatSatSolver::toMinisatLit(SatLiteral lit) { if (lit == undefSatLiteral) { return BVMinisat::lit_Undef; } return BVMinisat::mkLit(lit.getSatVariable(), lit.isNegated()); } -SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) { +SatLiteral BVMinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) { if (lit == BVMinisat::lit_Undef) { return undefSatLiteral; } @@ -150,19 +150,19 @@ SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) { BVMinisat::sign(lit)); } -SatValue MinisatSatSolver::toSatLiteralValue(bool res) { +SatValue BVMinisatSatSolver::toSatLiteralValue(bool res) { if(res) return SAT_VALUE_TRUE; else return SAT_VALUE_FALSE; } -SatValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) { +SatValue BVMinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) { if(res == (BVMinisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE; if(res == (BVMinisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN; Assert(res == (BVMinisat::lbool((uint8_t)1))); return SAT_VALUE_FALSE; } -void MinisatSatSolver::toMinisatClause(SatClause& clause, +void BVMinisatSatSolver::toMinisatClause(SatClause& clause, BVMinisat::vec& minisat_clause) { for (unsigned i = 0; i < clause.size(); ++i) { minisat_clause.push(toMinisatLit(clause[i])); @@ -170,7 +170,7 @@ void MinisatSatSolver::toMinisatClause(SatClause& clause, Assert(clause.size() == (unsigned)minisat_clause.size()); } -void MinisatSatSolver::toSatClause(BVMinisat::vec& clause, +void BVMinisatSatSolver::toSatClause(BVMinisat::vec& clause, SatClause& sat_clause) { for (int i = 0; i < clause.size(); ++i) { sat_clause.push_back(toSatLiteral(clause[i])); @@ -179,9 +179,9 @@ void MinisatSatSolver::toSatClause(BVMinisat::vec& clause, } -// Satistics for MinisatSatSolver +// Satistics for BVMinisatSatSolver -MinisatSatSolver::Statistics::Statistics() : +BVMinisatSatSolver::Statistics::Statistics() : d_statStarts("theory::bv::bvminisat::starts"), d_statDecisions("theory::bv::bvminisat::decisions"), d_statRndDecisions("theory::bv::bvminisat::rnd_decisions"), @@ -205,7 +205,7 @@ MinisatSatSolver::Statistics::Statistics() : StatisticsRegistry::registerStat(&d_statEliminatedVars); } -MinisatSatSolver::Statistics::~Statistics() { +BVMinisatSatSolver::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_statStarts); StatisticsRegistry::unregisterStat(&d_statDecisions); StatisticsRegistry::unregisterStat(&d_statRndDecisions); @@ -218,7 +218,7 @@ MinisatSatSolver::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_statEliminatedVars); } -void MinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ +void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ d_statStarts.setData(minisat->starts); d_statDecisions.setData(minisat->decisions); d_statRndDecisions.setData(minisat->rnd_decisions); diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 86fbe4433..d192b34b7 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -25,12 +25,12 @@ namespace CVC4 { namespace prop { -class MinisatSatSolver: public BVSatSolverInterface { +class BVMinisatSatSolver: public BVSatSolverInterface { BVMinisat::SimpSolver* d_minisat; public: - MinisatSatSolver(); - ~MinisatSatSolver(); + BVMinisatSatSolver(); + ~BVMinisatSatSolver(); void addClause(SatClause& clause, bool removable); SatVariable newVar(bool theoryAtom = false); @@ -79,7 +79,7 @@ public: Statistics d_statistics; }; -template class SatSolverConstructor; +template class SatSolverConstructor; } } diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index d75421e25..3a16b0d19 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -179,9 +179,9 @@ CRef Solver::reason(Var x) { // Get the explanation from the theory SatClause explanation_cl; - proxy->explainPropagation(DPLLMinisatSatSolver::toSatLiteral(l), explanation_cl); + proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl); vec explanation; - DPLLMinisatSatSolver::toMinisatClause(explanation_cl, explanation); + MinisatSatSolver::toMinisatClause(explanation_cl, explanation); // Sort the literals by trail index level lemma_lt lt(*this); @@ -343,7 +343,7 @@ void Solver::cancelUntil(int level) { int currentLevel = decisionLevel(); for(int i = variables_to_register.size() - 1; i >= 0 && variables_to_register[i].level > currentLevel; --i) { variables_to_register[i].level = currentLevel; - proxy->variableNotify(DPLLMinisatSatSolver::toSatVariable(variables_to_register[i].var)); + proxy->variableNotify(MinisatSatSolver::toSatVariable(variables_to_register[i].var)); } } } @@ -361,7 +361,7 @@ Lit Solver::pickBranchLit() Lit nextLit; #ifdef CVC4_REPLAY - nextLit = DPLLMinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision()); + nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision()); if (nextLit != lit_Undef) { return nextLit; @@ -369,7 +369,7 @@ Lit Solver::pickBranchLit() #endif /* CVC4_REPLAY */ // Theory requests - nextLit = DPLLMinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest()); + nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest()); while (nextLit != lit_Undef) { if(value(var(nextLit)) == l_Undef) { Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl; @@ -377,7 +377,7 @@ Lit Solver::pickBranchLit() } else { Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl; } - nextLit = DPLLMinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest()); + nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest()); } Var next = var_Undef; @@ -642,7 +642,7 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) } if (theory[var(p)]) { // Enqueue to the theory - proxy->enqueueTheoryLiteral(DPLLMinisatSatSolver::toSatLiteral(p)); + proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p)); } } @@ -708,7 +708,7 @@ void Solver::propagateTheory() { proxy->theoryPropagate(propagatedLiteralsClause); vec propagatedLiterals; - DPLLMinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals); + MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals); int oldTrailSize = trail.size(); Debug("minisat") << "old trail size is " << oldTrailSize << ", propagating " << propagatedLiterals.size() << " lits..." << std::endl; @@ -1079,7 +1079,7 @@ lbool Solver::search(int nof_conflicts) } #ifdef CVC4_REPLAY - proxy->logDecision(DPLLMinisatSatSolver::toSatLiteral(next)); + proxy->logDecision(MinisatSatSolver::toSatLiteral(next)); #endif /* CVC4_REPLAY */ } diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 1ec81a4f6..c8d310992 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -24,31 +24,31 @@ using namespace CVC4::prop; //// DPllMinisatSatSolver -DPLLMinisatSatSolver::DPLLMinisatSatSolver() : +MinisatSatSolver::MinisatSatSolver() : d_minisat(NULL), d_theoryProxy(NULL), d_context(NULL) {} -DPLLMinisatSatSolver::~DPLLMinisatSatSolver() { +MinisatSatSolver::~MinisatSatSolver() { delete d_minisat; } -SatVariable DPLLMinisatSatSolver::toSatVariable(Minisat::Var var) { +SatVariable MinisatSatSolver::toSatVariable(Minisat::Var var) { if (var == var_Undef) { return undefSatVariable; } return SatVariable(var); } -Minisat::Lit DPLLMinisatSatSolver::toMinisatLit(SatLiteral lit) { +Minisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) { if (lit == undefSatLiteral) { return Minisat::lit_Undef; } return Minisat::mkLit(lit.getSatVariable(), lit.isNegated()); } -SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) { +SatLiteral MinisatSatSolver::toSatLiteral(Minisat::Lit lit) { if (lit == Minisat::lit_Undef) { return undefSatLiteral; } @@ -57,12 +57,12 @@ SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) { Minisat::sign(lit)); } -SatValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) { +SatValue MinisatSatSolver::toSatLiteralValue(bool res) { if(res) return SAT_VALUE_TRUE; else return SAT_VALUE_FALSE; } -SatValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { +SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE; if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN; Assert(res == (Minisat::lbool((uint8_t)1))); @@ -70,7 +70,7 @@ SatValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { } -void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause, +void MinisatSatSolver::toMinisatClause(SatClause& clause, Minisat::vec& minisat_clause) { for (unsigned i = 0; i < clause.size(); ++i) { minisat_clause.push(toMinisatLit(clause[i])); @@ -78,7 +78,7 @@ void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause, Assert(clause.size() == (unsigned)minisat_clause.size()); } -void DPLLMinisatSatSolver::toSatClause(Minisat::vec& clause, +void MinisatSatSolver::toSatClause(Minisat::vec& clause, SatClause& sat_clause) { for (int i = 0; i < clause.size(); ++i) { sat_clause.push_back(toSatLiteral(clause[i])); @@ -87,7 +87,7 @@ void DPLLMinisatSatSolver::toSatClause(Minisat::vec& clause, } -void DPLLMinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) +void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) { d_context = context; @@ -110,18 +110,18 @@ void DPLLMinisatSatSolver::initialize(context::Context* context, TheoryProxy* th d_statistics.init(d_minisat); } -void DPLLMinisatSatSolver::addClause(SatClause& clause, bool removable) { +void MinisatSatSolver::addClause(SatClause& clause, bool removable) { Minisat::vec minisat_clause; toMinisatClause(clause, minisat_clause); d_minisat->addClause(minisat_clause, removable); } -SatVariable DPLLMinisatSatSolver::newVar(bool theoryAtom) { +SatVariable MinisatSatSolver::newVar(bool theoryAtom) { return d_minisat->newVar(true, true, theoryAtom); } -SatValue DPLLMinisatSatSolver::solve(unsigned long& resource) { +SatValue MinisatSatSolver::solve(unsigned long& resource) { Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; if(resource == 0) { d_minisat->budgetOff(); @@ -137,53 +137,53 @@ SatValue DPLLMinisatSatSolver::solve(unsigned long& resource) { return result; } -SatValue DPLLMinisatSatSolver::solve() { +SatValue MinisatSatSolver::solve() { d_minisat->budgetOff(); return toSatLiteralValue(d_minisat->solve()); } -void DPLLMinisatSatSolver::interrupt() { +void MinisatSatSolver::interrupt() { d_minisat->interrupt(); } -SatValue DPLLMinisatSatSolver::value(SatLiteral l) { +SatValue MinisatSatSolver::value(SatLiteral l) { return toSatLiteralValue(d_minisat->value(toMinisatLit(l))); } -SatValue DPLLMinisatSatSolver::modelValue(SatLiteral l){ +SatValue MinisatSatSolver::modelValue(SatLiteral l){ return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l))); } -bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const { +bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const { return true; } /** Incremental interface */ -unsigned DPLLMinisatSatSolver::getAssertionLevel() const { +unsigned MinisatSatSolver::getAssertionLevel() const { return d_minisat->getAssertionLevel(); } -void DPLLMinisatSatSolver::push() { +void MinisatSatSolver::push() { d_minisat->push(); } -void DPLLMinisatSatSolver::pop(){ +void MinisatSatSolver::pop(){ d_minisat->pop(); } -void DPLLMinisatSatSolver::unregisterVar(SatLiteral lit) { +void MinisatSatSolver::unregisterVar(SatLiteral lit) { d_minisat->unregisterVar(toMinisatLit(lit)); } -void DPLLMinisatSatSolver::renewVar(SatLiteral lit, int level) { +void MinisatSatSolver::renewVar(SatLiteral lit, int level) { d_minisat->renewVar(toMinisatLit(lit), level); } -/// Statistics for DPLLMinisatSatSolver +/// Statistics for MinisatSatSolver -DPLLMinisatSatSolver::Statistics::Statistics() : +MinisatSatSolver::Statistics::Statistics() : d_statStarts("sat::starts"), d_statDecisions("sat::decisions"), d_statRndDecisions("sat::rnd_decisions"), @@ -204,7 +204,7 @@ DPLLMinisatSatSolver::Statistics::Statistics() : StatisticsRegistry::registerStat(&d_statMaxLiterals); StatisticsRegistry::registerStat(&d_statTotLiterals); } -DPLLMinisatSatSolver::Statistics::~Statistics() { +MinisatSatSolver::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_statStarts); StatisticsRegistry::unregisterStat(&d_statDecisions); StatisticsRegistry::unregisterStat(&d_statRndDecisions); @@ -215,7 +215,7 @@ DPLLMinisatSatSolver::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_statMaxLiterals); StatisticsRegistry::unregisterStat(&d_statTotLiterals); } -void DPLLMinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ +void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ d_statStarts.setData(d_minisat->starts); d_statDecisions.setData(d_minisat->decisions); d_statRndDecisions.setData(d_minisat->rnd_decisions); diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 66aca717d..3bd690cc7 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -25,7 +25,7 @@ namespace CVC4 { namespace prop { -class DPLLMinisatSatSolver : public DPLLSatSolverInterface { +class MinisatSatSolver : public DPLLSatSolverInterface { /** The SatSolver used */ Minisat::SimpSolver* d_minisat; @@ -39,8 +39,8 @@ class DPLLMinisatSatSolver : public DPLLSatSolverInterface { public: - DPLLMinisatSatSolver (); - ~DPLLMinisatSatSolver(); + MinisatSatSolver (); + ~MinisatSatSolver(); static SatVariable toSatVariable(Minisat::Var var); static Minisat::Lit toMinisatLit(SatLiteral lit); @@ -96,7 +96,7 @@ public: }; -template class SatSolverConstructor; +template class SatSolverConstructor; } // prop namespace } // cvc4 namespace diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 61c67ed5f..f18335048 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -26,135 +26,13 @@ #include "util/options.h" #include "util/stats.h" #include "context/cdlist.h" +#include "prop/sat_solver_types.h" namespace CVC4 { namespace prop { class TheoryProxy; -/** - * Boolean values of the SAT solver. - */ -enum SatValue { - SAT_VALUE_UNKNOWN, - SAT_VALUE_TRUE, - SAT_VALUE_FALSE -}; - -/** - * A variable of the SAT solver. - */ -typedef uint64_t SatVariable; - -/** - * Undefined SAT solver variable. - */ -const SatVariable undefSatVariable = SatVariable(-1); - -/** - * A SAT literal is a variable or an negated variable. - */ -class SatLiteral { - - /** - * The value holds the variable and a bit noting if the variable is negated. - */ - uint64_t d_value; - -public: - - /** - * Construct an undefined SAT literal. - */ - SatLiteral() - : d_value(undefSatVariable) - {} - - /** - * Construct a literal given a possible negated variable. - */ - SatLiteral(SatVariable var, bool negated = false) { - d_value = var + var + (int)negated; - } - - /** - * Returns the variable of the literal. - */ - SatVariable getSatVariable() const { - return d_value >> 1; - } - - /** - * Returns true if the literal is a negated variable. - */ - bool isNegated() const { - return d_value & 1; - } - - /** - * Negate the given literal. - */ - SatLiteral operator ~ () const { - return SatLiteral(getSatVariable(), !isNegated()); - } - - /** - * Compare two literals for equality. - */ - bool operator == (const SatLiteral& other) const { - return d_value == other.d_value; - } - - /** - * Compare two literals for dis-equality. - */ - bool operator != (const SatLiteral& other) const { - return !(*this == other); - } - - /** - * Returns a string representation of the literal. - */ - std::string toString() const { - std::ostringstream os; - os << (isNegated()? "~" : "") << getSatVariable() << " "; - return os.str(); - } - - /** - * Returns the hash value of a literal. - */ - size_t hash() const { - return (size_t)d_value; - } - - /** - * Returns true if the literal is undefined. - */ - bool isNull() const { - return getSatVariable() == undefSatVariable; - } -}; - -/** - * A constant representing a undefined literal. - */ -const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable); - -/** - * Helper for hashing the literals. - */ -struct SatLiteralHashFunction { - inline size_t operator() (const SatLiteral& literal) const { - return literal.hash(); - } -}; - -/** - * A SAT clause is a vector of literals. - */ -typedef std::vector SatClause; - class SatSolver { public: diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index c5972d7bb..fa787451d 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -25,11 +25,11 @@ using namespace CVC4; using namespace prop; BVSatSolverInterface* SatSolverFactory::createMinisat() { - return new MinisatSatSolver(); + return new BVMinisatSatSolver(); } DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() { - return new DPLLMinisatSatSolver(); + return new MinisatSatSolver(); } SatSolver* SatSolverFactory::create(const char* name) { diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h new file mode 100644 index 000000000..406782468 --- /dev/null +++ b/src/prop/sat_solver_types.h @@ -0,0 +1,194 @@ +/********************* */ +/*! \file cnf_stream.h + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters, dejan + ** Minor contributors (to current version): barrett, cconway + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This class transforms a sequence of formulas into clauses. + ** + ** This class takes a sequence of formulas. + ** It outputs a stream of clauses that is propositionally + ** equi-satisfiable with the conjunction of the formulas. + ** This stream is maintained in an online fashion. + ** + ** Unlike other parts of the system it is aware of the PropEngine's + ** internals such as the representation and translation of [??? -Chris] + **/ + +#pragma once + +#include "cvc4_private.h" + +namespace CVC4 { +namespace prop { + +/** + * Boolean values of the SAT solver. + */ +enum SatValue { + SAT_VALUE_UNKNOWN, + SAT_VALUE_TRUE, + SAT_VALUE_FALSE +}; + +/** + * A variable of the SAT solver. + */ +typedef uint64_t SatVariable; + +/** + * Undefined SAT solver variable. + */ +const SatVariable undefSatVariable = SatVariable(-1); + +/** + * A SAT literal is a variable or an negated variable. + */ +class SatLiteral { + + /** + * The value holds the variable and a bit noting if the variable is negated. + */ + uint64_t d_value; + +public: + + /** + * Construct an undefined SAT literal. + */ + SatLiteral() + : d_value(undefSatVariable) + {} + + /** + * Construct a literal given a possible negated variable. + */ + SatLiteral(SatVariable var, bool negated = false) { + d_value = var + var + (int)negated; + } + + /** + * Returns the variable of the literal. + */ + SatVariable getSatVariable() const { + return d_value >> 1; + } + + /** + * Returns true if the literal is a negated variable. + */ + bool isNegated() const { + return d_value & 1; + } + + /** + * Negate the given literal. + */ + SatLiteral operator ~ () const { + return SatLiteral(getSatVariable(), !isNegated()); + } + + /** + * Compare two literals for equality. + */ + bool operator == (const SatLiteral& other) const { + return d_value == other.d_value; + } + + /** + * Compare two literals for dis-equality. + */ + bool operator != (const SatLiteral& other) const { + return !(*this == other); + } + + /** + * Returns a string representation of the literal. + */ + std::string toString() const { + std::ostringstream os; + os << (isNegated()? "~" : "") << getSatVariable() << " "; + return os.str(); + } + + /** + * Returns the hash value of a literal. + */ + size_t hash() const { + return (size_t)d_value; + } + + /** + * Returns true if the literal is undefined. + */ + bool isNull() const { + return getSatVariable() == undefSatVariable; + } +}; + +/** + * A constant representing a undefined literal. + */ +const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable); + +/** + * Helper for hashing the literals. + */ +struct SatLiteralHashFunction { + inline size_t operator() (const SatLiteral& literal) const { + return literal.hash(); + } +}; + +/** + * A SAT clause is a vector of literals. + */ +typedef std::vector SatClause; + +/** + * Each object in the SAT solver, such as as variables and clauses, can be assigned a life span, + * so that the SAT solver can (or should) remove them when the lifespan is over. + */ +enum SatSolverLifespan +{ + /** + * The object should stay forever and never be removed + */ + SAT_LIFESPAN_PERMANENT, + /** + * The object can be removed at any point when it becomes unnecessary. + */ + SAT_LIFESPAN_REMOVABLE, + /** + * The object must be removed as soon as the SAT solver exits the search context + * where the object got introduced. + */ + SAT_LIFESPAN_SEARCH_CONTEXT_STRICT, + /** + * The object can be removed when SAT solver exits the search context where the object + * got introduced, but can be kept at the solver discretion. + */ + SAT_LIFESPAN_SEARCH_CONTEXT_LENIENT, + /** + * The object must be removed as soon as the SAT solver exits the user-level context where + * the object got introduced. + */ + SAT_LIFESPAN_USER_CONTEXT_STRICT, + /** + * The object can be removed when the SAT solver exits the user-level context where + * the object got introduced. + */ + SAT_LIFESPAN_USER_CONTEXT_LENIENT +}; + +} +} + +