From: Dejan Jovanović Date: Sun, 25 Mar 2012 20:12:07 +0000 (+0000) Subject: sat_module.h,cpp -> sat_solver.h,cpp (as intended) X-Git-Tag: cvc5-1.0.0~8267 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0d080430206880ffc19050acfa01aae1475f1978;p=cvc5.git sat_module.h,cpp -> sat_solver.h,cpp (as intended) --- diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 02a6a4714..832255621 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -15,8 +15,8 @@ libprop_la_SOURCES = \ theory_proxy.cpp \ cnf_stream.h \ cnf_stream.cpp \ - sat_module.h \ - sat_module.cpp + sat_solver.h \ + sat_solver.cpp SUBDIRS = minisat bvminisat diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 676cc4c49..3a4fa781a 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -44,7 +44,7 @@ namespace CVC4 { namespace prop { -CnfStream::CnfStream(SatSolverInterface *satSolver, Registrar* registrar, bool fullLitToNodeMap) : +CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, bool fullLitToNodeMap) : d_satSolver(satSolver), d_fullLitToNodeMap(fullLitToNodeMap), d_registrar(registrar) { @@ -66,7 +66,7 @@ void CnfStream::recordTranslation(TNode node, bool alwaysRecord) { } } -TseitinCnfStream::TseitinCnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap) : +TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap) : CnfStream(satSolver, registrar, fullLitToNodeMap) { } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index af2ff2fcd..f75e74d63 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -65,7 +65,7 @@ public: protected: /** The SAT solver we will be using */ - SatSolverInterface *d_satSolver; + SatSolver *d_satSolver; TranslationCache d_translationCache; NodeCache d_nodeCache; @@ -190,7 +190,7 @@ public: * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - CnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap = false); + CnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap = false); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -290,7 +290,7 @@ public: * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - TseitinCnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap = false); + TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap = false); private: diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 65ec025b1..e5a6d32e1 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/core/Solver.h" #include "prop/theory_proxy.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" #include "util/output.h" #include "expr/command.h" #include "proof/proof_manager.h" diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 9d6a2c8f6..0fa13dc04 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -19,7 +19,7 @@ #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/theory_proxy.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" diff --git a/src/prop/sat_module.cpp b/src/prop/sat_module.cpp deleted file mode 100644 index 5e5b78b44..000000000 --- a/src/prop/sat_module.cpp +++ /dev/null @@ -1,478 +0,0 @@ -/********************* */ -/*! \file sat.cpp - ** \verbatim - ** Original author: cconway - ** Major contributors: dejan, taking, mdeters, lianah - ** Minor contributors (to current version): none - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "prop/prop_engine.h" -#include "prop/sat_module.h" -#include "context/context.h" -#include "theory/theory_engine.h" -#include "expr/expr_stream.h" -#include "prop/theory_proxy.h" - -// DPLLT Minisat -#include "prop/minisat/simp/SimpSolver.h" - -// BV Minisat -#include "prop/bvminisat/simp/SimpSolver.h" - - -using namespace std; - -namespace CVC4 { -namespace prop { - -string SatLiteral::toString() { - ostringstream os; - os << (isNegated()? "~" : "") << getSatVariable() << " "; - return os.str(); -} - -MinisatSatSolver::MinisatSatSolver() : - d_minisat(new BVMinisat::SimpSolver()) -{ - d_statistics.init(d_minisat); -} - -MinisatSatSolver::~MinisatSatSolver() { - delete d_minisat; -} - -void MinisatSatSolver::addClause(SatClause& clause, bool removable) { - Debug("sat::minisat") << "Add clause " << clause <<"\n"; - BVMinisat::vec minisat_clause; - toMinisatClause(clause, minisat_clause); - // for(unsigned i = 0; i < minisat_clause.size(); ++i) { - // d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true); - // } - d_minisat->addClause(minisat_clause); -} - -SatVariable MinisatSatSolver::newVar(bool freeze){ - return d_minisat->newVar(true, true, freeze); -} - -void MinisatSatSolver::markUnremovable(SatLiteral lit){ - d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true); -} - -void MinisatSatSolver::interrupt(){ - d_minisat->interrupt(); -} - -SatLiteralValue MinisatSatSolver::solve(){ - return toSatLiteralValue(d_minisat->solve()); -} - -SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){ - Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; - if(resource == 0) { - d_minisat->budgetOff(); - } else { - d_minisat->setConfBudget(resource); - } - BVMinisat::vec empty; - unsigned long conflictsBefore = d_minisat->conflicts; - SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); - d_minisat->clearInterrupt(); - resource = d_minisat->conflicts - conflictsBefore; - Trace("limit") << " & assumptions){ - Debug("sat::minisat") << "Solve with assumptions "; - context::CDList::const_iterator it = assumptions.begin(); - BVMinisat::vec assump; - for(; it!= assumptions.end(); ++it) { - SatLiteral lit = *it; - Debug("sat::minisat") << lit <<" "; - assump.push(toMinisatLit(lit)); - } - Debug("sat::minisat") <<"\n"; - - SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump)); - return result; -} - - -void MinisatSatSolver::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])); - } -} - -SatLiteralValue MinisatSatSolver::value(SatLiteral l){ - Unimplemented(); - return SatValUnknown; -} - -SatLiteralValue MinisatSatSolver::modelValue(SatLiteral l){ - Unimplemented(); - return SatValUnknown; -} - -void MinisatSatSolver::unregisterVar(SatLiteral lit) { - // this should only be called when user context is implemented - // in the BVSatSolver - Unreachable(); -} - -void MinisatSatSolver::renewVar(SatLiteral lit, int level) { - // this should only be called when user context is implemented - // in the BVSatSolver - - Unreachable(); -} - -int MinisatSatSolver::getAssertionLevel() const { - // we have no user context implemented so far - return 0; -} - -// converting from internal Minisat representation - -SatVariable MinisatSatSolver::toSatVariable(BVMinisat::Var var) { - if (var == var_Undef) { - return undefSatVariable; - } - return SatVariable(var); -} - -BVMinisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) { - if (lit == undefSatLiteral) { - return BVMinisat::lit_Undef; - } - return BVMinisat::mkLit(lit.getSatVariable(), lit.isNegated()); -} - -SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) { - if (lit == BVMinisat::lit_Undef) { - return undefSatLiteral; - } - - return SatLiteral(SatVariable(BVMinisat::var(lit)), - BVMinisat::sign(lit)); -} - -SatLiteralValue MinisatSatSolver::toSatLiteralValue(bool res) { - if(res) return SatValTrue; - else return SatValFalse; -} - -SatLiteralValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) { - if(res == (BVMinisat::lbool((uint8_t)0))) return SatValTrue; - if(res == (BVMinisat::lbool((uint8_t)2))) return SatValUnknown; - Assert(res == (BVMinisat::lbool((uint8_t)1))); - return SatValFalse; -} - -void MinisatSatSolver::toMinisatClause(SatClause& clause, - BVMinisat::vec& minisat_clause) { - for (unsigned i = 0; i < clause.size(); ++i) { - minisat_clause.push(toMinisatLit(clause[i])); - } - Assert(clause.size() == (unsigned)minisat_clause.size()); -} - -void MinisatSatSolver::toSatClause(BVMinisat::vec& clause, - SatClause& sat_clause) { - for (int i = 0; i < clause.size(); ++i) { - sat_clause.push_back(toSatLiteral(clause[i])); - } - Assert((unsigned)clause.size() == sat_clause.size()); -} - - -// Satistics for MinisatSatSolver - -MinisatSatSolver::Statistics::Statistics() : - d_statStarts("theory::bv::bvminisat::starts"), - d_statDecisions("theory::bv::bvminisat::decisions"), - d_statRndDecisions("theory::bv::bvminisat::rnd_decisions"), - d_statPropagations("theory::bv::bvminisat::propagations"), - d_statConflicts("theory::bv::bvminisat::conflicts"), - d_statClausesLiterals("theory::bv::bvminisat::clauses_literals"), - d_statLearntsLiterals("theory::bv::bvminisat::learnts_literals"), - d_statMaxLiterals("theory::bv::bvminisat::max_literals"), - d_statTotLiterals("theory::bv::bvminisat::tot_literals"), - d_statEliminatedVars("theory::bv::bvminisat::eliminated_vars") -{ - StatisticsRegistry::registerStat(&d_statStarts); - StatisticsRegistry::registerStat(&d_statDecisions); - StatisticsRegistry::registerStat(&d_statRndDecisions); - StatisticsRegistry::registerStat(&d_statPropagations); - StatisticsRegistry::registerStat(&d_statConflicts); - StatisticsRegistry::registerStat(&d_statClausesLiterals); - StatisticsRegistry::registerStat(&d_statLearntsLiterals); - StatisticsRegistry::registerStat(&d_statMaxLiterals); - StatisticsRegistry::registerStat(&d_statTotLiterals); - StatisticsRegistry::registerStat(&d_statEliminatedVars); -} - -MinisatSatSolver::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_statStarts); - StatisticsRegistry::unregisterStat(&d_statDecisions); - StatisticsRegistry::unregisterStat(&d_statRndDecisions); - StatisticsRegistry::unregisterStat(&d_statPropagations); - StatisticsRegistry::unregisterStat(&d_statConflicts); - StatisticsRegistry::unregisterStat(&d_statClausesLiterals); - StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); - StatisticsRegistry::unregisterStat(&d_statMaxLiterals); - StatisticsRegistry::unregisterStat(&d_statTotLiterals); - StatisticsRegistry::unregisterStat(&d_statEliminatedVars); -} - -void MinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ - d_statStarts.setData(minisat->starts); - d_statDecisions.setData(minisat->decisions); - d_statRndDecisions.setData(minisat->rnd_decisions); - d_statPropagations.setData(minisat->propagations); - d_statConflicts.setData(minisat->conflicts); - d_statClausesLiterals.setData(minisat->clauses_literals); - d_statLearntsLiterals.setData(minisat->learnts_literals); - d_statMaxLiterals.setData(minisat->max_literals); - d_statTotLiterals.setData(minisat->tot_literals); - d_statEliminatedVars.setData(minisat->eliminated_vars); -} - - - -//// DPllMinisatSatSolver - -DPLLMinisatSatSolver::DPLLMinisatSatSolver() : - d_minisat(NULL), - d_theoryProxy(NULL), - d_context(NULL) -{} - -DPLLMinisatSatSolver::~DPLLMinisatSatSolver() { - delete d_minisat; -} - -SatVariable DPLLMinisatSatSolver::toSatVariable(Minisat::Var var) { - if (var == var_Undef) { - return undefSatVariable; - } - return SatVariable(var); -} - -Minisat::Lit DPLLMinisatSatSolver::toMinisatLit(SatLiteral lit) { - if (lit == undefSatLiteral) { - return Minisat::lit_Undef; - } - return Minisat::mkLit(lit.getSatVariable(), lit.isNegated()); -} - -SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) { - if (lit == Minisat::lit_Undef) { - return undefSatLiteral; - } - - return SatLiteral(SatVariable(Minisat::var(lit)), - Minisat::sign(lit)); -} - -SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) { - if(res) return SatValTrue; - else return SatValFalse; -} - -SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { - if(res == (Minisat::lbool((uint8_t)0))) return SatValTrue; - if(res == (Minisat::lbool((uint8_t)2))) return SatValUnknown; - Assert(res == (Minisat::lbool((uint8_t)1))); - return SatValFalse; -} - - -void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause, - Minisat::vec& minisat_clause) { - for (unsigned i = 0; i < clause.size(); ++i) { - minisat_clause.push(toMinisatLit(clause[i])); - } - Assert(clause.size() == (unsigned)minisat_clause.size()); -} - -void DPLLMinisatSatSolver::toSatClause(Minisat::vec& clause, - SatClause& sat_clause) { - for (int i = 0; i < clause.size(); ++i) { - sat_clause.push_back(toSatLiteral(clause[i])); - } - Assert((unsigned)clause.size() == sat_clause.size()); -} - - -void DPLLMinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) -{ - - d_context = context; - - // Create the solver - d_minisat = new Minisat::SimpSolver(theoryProxy, d_context, - Options::current()->incrementalSolving); - // Setup the verbosity - d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1; - - // Setup the random decision parameters - d_minisat->random_var_freq = Options::current()->satRandomFreq; - d_minisat->random_seed = Options::current()->satRandomSeed; - // Give access to all possible options in the sat solver - d_minisat->var_decay = Options::current()->satVarDecay; - d_minisat->clause_decay = Options::current()->satClauseDecay; - d_minisat->restart_first = Options::current()->satRestartFirst; - d_minisat->restart_inc = Options::current()->satRestartInc; - - d_statistics.init(d_minisat); -} - -void DPLLMinisatSatSolver::addClause(SatClause& clause, bool removable) { - Minisat::vec minisat_clause; - toMinisatClause(clause, minisat_clause); - d_minisat->addClause(minisat_clause, removable); -} - -SatVariable DPLLMinisatSatSolver::newVar(bool theoryAtom) { - return d_minisat->newVar(true, true, theoryAtom); -} - - -SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) { - Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; - if(resource == 0) { - d_minisat->budgetOff(); - } else { - d_minisat->setConfBudget(resource); - } - Minisat::vec empty; - unsigned long conflictsBefore = d_minisat->conflicts; - SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); - d_minisat->clearInterrupt(); - resource = d_minisat->conflicts - conflictsBefore; - Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl; - return result; -} - -SatLiteralValue DPLLMinisatSatSolver::solve() { - d_minisat->budgetOff(); - return toSatLiteralValue(d_minisat->solve()); -} - - -void DPLLMinisatSatSolver::interrupt() { - d_minisat->interrupt(); -} - -SatLiteralValue DPLLMinisatSatSolver::value(SatLiteral l) { - return toSatLiteralValue(d_minisat->value(toMinisatLit(l))); -} - -SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){ - return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l))); -} - -bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const { - return true; -} - -/** Incremental interface */ - -int DPLLMinisatSatSolver::getAssertionLevel() const { - return d_minisat->getAssertionLevel(); -} - -void DPLLMinisatSatSolver::push() { - d_minisat->push(); -} - -void DPLLMinisatSatSolver::pop(){ - d_minisat->pop(); -} - -void DPLLMinisatSatSolver::unregisterVar(SatLiteral lit) { - d_minisat->unregisterVar(toMinisatLit(lit)); -} - -void DPLLMinisatSatSolver::renewVar(SatLiteral lit, int level) { - d_minisat->renewVar(toMinisatLit(lit), level); -} - -/// Statistics for DPLLMinisatSatSolver - -DPLLMinisatSatSolver::Statistics::Statistics() : - d_statStarts("sat::starts"), - d_statDecisions("sat::decisions"), - d_statRndDecisions("sat::rnd_decisions"), - d_statPropagations("sat::propagations"), - d_statConflicts("sat::conflicts"), - d_statClausesLiterals("sat::clauses_literals"), - d_statLearntsLiterals("sat::learnts_literals"), - d_statMaxLiterals("sat::max_literals"), - d_statTotLiterals("sat::tot_literals") -{ - StatisticsRegistry::registerStat(&d_statStarts); - StatisticsRegistry::registerStat(&d_statDecisions); - StatisticsRegistry::registerStat(&d_statRndDecisions); - StatisticsRegistry::registerStat(&d_statPropagations); - StatisticsRegistry::registerStat(&d_statConflicts); - StatisticsRegistry::registerStat(&d_statClausesLiterals); - StatisticsRegistry::registerStat(&d_statLearntsLiterals); - StatisticsRegistry::registerStat(&d_statMaxLiterals); - StatisticsRegistry::registerStat(&d_statTotLiterals); -} -DPLLMinisatSatSolver::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_statStarts); - StatisticsRegistry::unregisterStat(&d_statDecisions); - StatisticsRegistry::unregisterStat(&d_statRndDecisions); - StatisticsRegistry::unregisterStat(&d_statPropagations); - StatisticsRegistry::unregisterStat(&d_statConflicts); - StatisticsRegistry::unregisterStat(&d_statClausesLiterals); - StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); - StatisticsRegistry::unregisterStat(&d_statMaxLiterals); - StatisticsRegistry::unregisterStat(&d_statTotLiterals); -} -void DPLLMinisatSatSolver::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); - d_statPropagations.setData(d_minisat->propagations); - d_statConflicts.setData(d_minisat->conflicts); - d_statClausesLiterals.setData(d_minisat->clauses_literals); - d_statLearntsLiterals.setData(d_minisat->learnts_literals); - d_statMaxLiterals.setData(d_minisat->max_literals); - d_statTotLiterals.setData(d_minisat->tot_literals); -} - - -/* - - SatSolverFactory - - */ - -MinisatSatSolver* SatSolverFactory::createMinisat() { - return new MinisatSatSolver(); -} - -DPLLMinisatSatSolver* SatSolverFactory::createDPLLMinisat(){ - return new DPLLMinisatSatSolver(); -} - - -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ diff --git a/src/prop/sat_module.h b/src/prop/sat_module.h deleted file mode 100644 index 9c49c7d67..000000000 --- a/src/prop/sat_module.h +++ /dev/null @@ -1,299 +0,0 @@ -/********************* */ -/*! \file sat_module.h - ** \verbatim - ** Original author: lianah - ** Major contributors: - ** Minor contributors (to current version): - ** 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 SAT Solver. - ** - ** SAT Solver. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__PROP__SAT_MODULE_H -#define __CVC4__PROP__SAT_MODULE_H - -#include -#include "util/options.h" -#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 { - -class TheoryProxy; - -enum SatLiteralValue { - SatValUnknown, - SatValTrue, - SatValFalse -}; - - -typedef uint64_t SatVariable; -// special constant -const SatVariable undefSatVariable = SatVariable(-1); - -class SatLiteral { - uint64_t d_value; -public: - SatLiteral() : - d_value(undefSatVariable) - {} - - SatLiteral(SatVariable var, bool negated = false) { d_value = var + var + (int)negated; } - SatLiteral operator~() { - return SatLiteral(getSatVariable(), !isNegated()); - } - bool operator==(const SatLiteral& other) const { - return d_value == other.d_value; - } - bool operator!=(const SatLiteral& other) const { - return !(*this == other); - } - std::string toString(); - bool isNegated() const { return d_value & 1; } - size_t toHash() const {return (size_t)d_value; } - bool isNull() const { return d_value == (uint64_t)-1; } - SatVariable getSatVariable() const {return d_value >> 1; } -}; - -// special constant -const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable); - - -struct SatLiteralHashFunction { - inline size_t operator() (const SatLiteral& literal) const { - return literal.toHash(); - } -}; - -typedef std::vector SatClause; - - - -class SatSolverInterface { -public: - /** Virtual destructor to make g++ happy */ - virtual ~SatSolverInterface() { } - - /** 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; - - - /** Check the satisfiability of the added clauses */ - virtual SatLiteralValue solve() = 0; - - /** Check the satisfiability of the added clauses */ - virtual SatLiteralValue solve(long unsigned int&) = 0; - - /** Interrupt the solver */ - virtual void interrupt() = 0; - - /** Call value() during the search.*/ - virtual SatLiteralValue value(SatLiteral l) = 0; - - /** Call modelValue() when the search is done.*/ - virtual SatLiteralValue modelValue(SatLiteral l) = 0; - - virtual void unregisterVar(SatLiteral lit) = 0; - - virtual void renewVar(SatLiteral lit, int level = -1) = 0; - - virtual int getAssertionLevel() const = 0; - -}; - - -class BVSatSolverInterface: public SatSolverInterface { -public: - virtual SatLiteralValue solve(const context::CDList & assumptions) = 0; - - virtual void markUnremovable(SatLiteral lit) = 0; - - virtual void getUnsatCore(SatClause& unsatCore) = 0; -}; - - -class DPLLSatSolverInterface: public SatSolverInterface { -public: - virtual void initialize(context::Context* context, prop::TheoryProxy* theoryProxy) = 0; - - virtual void push() = 0; - - virtual void pop() = 0; - - virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0; - -}; - -// toodo add ifdef - - -class MinisatSatSolver: public BVSatSolverInterface { - BVMinisat::SimpSolver* d_minisat; - - MinisatSatSolver(); -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 & 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& minisat_clause); - static void toSatClause (BVMinisat::vec& clause, SatClause& sat_clause); - - class Statistics { - public: - ReferenceStat d_statStarts, d_statDecisions; - ReferenceStat d_statRndDecisions, d_statPropagations; - ReferenceStat d_statConflicts, d_statClausesLiterals; - ReferenceStat d_statLearntsLiterals, d_statMaxLiterals; - ReferenceStat d_statTotLiterals; - ReferenceStat d_statEliminatedVars; - Statistics(); - ~Statistics(); - void init(BVMinisat::SimpSolver* minisat); - }; - - Statistics d_statistics; - friend class SatSolverFactory; -}; - - -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_clause); - static void toSatClause (Minisat::vec& 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); - - class Statistics { - private: - ReferenceStat d_statStarts, d_statDecisions; - ReferenceStat d_statRndDecisions, d_statPropagations; - ReferenceStat d_statConflicts, d_statClausesLiterals; - ReferenceStat d_statLearntsLiterals, d_statMaxLiterals; - ReferenceStat d_statTotLiterals; - public: - Statistics(); - ~Statistics(); - void init(Minisat::SimpSolver* d_minisat); - }; - Statistics d_statistics; - - friend class SatSolverFactory; -}; - -class SatSolverFactory { -public: - static MinisatSatSolver* createMinisat(); - static DPLLMinisatSatSolver* createDPLLMinisat(); -}; - -}/* prop namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PROP__SAT_MODULE_H */ diff --git a/src/prop/sat_solver.cpp b/src/prop/sat_solver.cpp new file mode 100644 index 000000000..13f2498f2 --- /dev/null +++ b/src/prop/sat_solver.cpp @@ -0,0 +1,478 @@ +/********************* */ +/*! \file sat.cpp + ** \verbatim + ** Original author: cconway + ** Major contributors: dejan, taking, mdeters, lianah + ** Minor contributors (to current version): none + ** 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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "prop/prop_engine.h" +#include "prop/sat_solver.h" +#include "context/context.h" +#include "theory/theory_engine.h" +#include "expr/expr_stream.h" +#include "prop/theory_proxy.h" + +// DPLLT Minisat +#include "prop/minisat/simp/SimpSolver.h" + +// BV Minisat +#include "prop/bvminisat/simp/SimpSolver.h" + + +using namespace std; + +namespace CVC4 { +namespace prop { + +string SatLiteral::toString() { + ostringstream os; + os << (isNegated()? "~" : "") << getSatVariable() << " "; + return os.str(); +} + +MinisatSatSolver::MinisatSatSolver() : + d_minisat(new BVMinisat::SimpSolver()) +{ + d_statistics.init(d_minisat); +} + +MinisatSatSolver::~MinisatSatSolver() { + delete d_minisat; +} + +void MinisatSatSolver::addClause(SatClause& clause, bool removable) { + Debug("sat::minisat") << "Add clause " << clause <<"\n"; + BVMinisat::vec minisat_clause; + toMinisatClause(clause, minisat_clause); + // for(unsigned i = 0; i < minisat_clause.size(); ++i) { + // d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true); + // } + d_minisat->addClause(minisat_clause); +} + +SatVariable MinisatSatSolver::newVar(bool freeze){ + return d_minisat->newVar(true, true, freeze); +} + +void MinisatSatSolver::markUnremovable(SatLiteral lit){ + d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true); +} + +void MinisatSatSolver::interrupt(){ + d_minisat->interrupt(); +} + +SatLiteralValue MinisatSatSolver::solve(){ + return toSatLiteralValue(d_minisat->solve()); +} + +SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){ + Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; + if(resource == 0) { + d_minisat->budgetOff(); + } else { + d_minisat->setConfBudget(resource); + } + BVMinisat::vec empty; + unsigned long conflictsBefore = d_minisat->conflicts; + SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); + d_minisat->clearInterrupt(); + resource = d_minisat->conflicts - conflictsBefore; + Trace("limit") << " & assumptions){ + Debug("sat::minisat") << "Solve with assumptions "; + context::CDList::const_iterator it = assumptions.begin(); + BVMinisat::vec assump; + for(; it!= assumptions.end(); ++it) { + SatLiteral lit = *it; + Debug("sat::minisat") << lit <<" "; + assump.push(toMinisatLit(lit)); + } + Debug("sat::minisat") <<"\n"; + + SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump)); + return result; +} + + +void MinisatSatSolver::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])); + } +} + +SatLiteralValue MinisatSatSolver::value(SatLiteral l){ + Unimplemented(); + return SatValUnknown; +} + +SatLiteralValue MinisatSatSolver::modelValue(SatLiteral l){ + Unimplemented(); + return SatValUnknown; +} + +void MinisatSatSolver::unregisterVar(SatLiteral lit) { + // this should only be called when user context is implemented + // in the BVSatSolver + Unreachable(); +} + +void MinisatSatSolver::renewVar(SatLiteral lit, int level) { + // this should only be called when user context is implemented + // in the BVSatSolver + + Unreachable(); +} + +int MinisatSatSolver::getAssertionLevel() const { + // we have no user context implemented so far + return 0; +} + +// converting from internal Minisat representation + +SatVariable MinisatSatSolver::toSatVariable(BVMinisat::Var var) { + if (var == var_Undef) { + return undefSatVariable; + } + return SatVariable(var); +} + +BVMinisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) { + if (lit == undefSatLiteral) { + return BVMinisat::lit_Undef; + } + return BVMinisat::mkLit(lit.getSatVariable(), lit.isNegated()); +} + +SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) { + if (lit == BVMinisat::lit_Undef) { + return undefSatLiteral; + } + + return SatLiteral(SatVariable(BVMinisat::var(lit)), + BVMinisat::sign(lit)); +} + +SatLiteralValue MinisatSatSolver::toSatLiteralValue(bool res) { + if(res) return SatValTrue; + else return SatValFalse; +} + +SatLiteralValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) { + if(res == (BVMinisat::lbool((uint8_t)0))) return SatValTrue; + if(res == (BVMinisat::lbool((uint8_t)2))) return SatValUnknown; + Assert(res == (BVMinisat::lbool((uint8_t)1))); + return SatValFalse; +} + +void MinisatSatSolver::toMinisatClause(SatClause& clause, + BVMinisat::vec& minisat_clause) { + for (unsigned i = 0; i < clause.size(); ++i) { + minisat_clause.push(toMinisatLit(clause[i])); + } + Assert(clause.size() == (unsigned)minisat_clause.size()); +} + +void MinisatSatSolver::toSatClause(BVMinisat::vec& clause, + SatClause& sat_clause) { + for (int i = 0; i < clause.size(); ++i) { + sat_clause.push_back(toSatLiteral(clause[i])); + } + Assert((unsigned)clause.size() == sat_clause.size()); +} + + +// Satistics for MinisatSatSolver + +MinisatSatSolver::Statistics::Statistics() : + d_statStarts("theory::bv::bvminisat::starts"), + d_statDecisions("theory::bv::bvminisat::decisions"), + d_statRndDecisions("theory::bv::bvminisat::rnd_decisions"), + d_statPropagations("theory::bv::bvminisat::propagations"), + d_statConflicts("theory::bv::bvminisat::conflicts"), + d_statClausesLiterals("theory::bv::bvminisat::clauses_literals"), + d_statLearntsLiterals("theory::bv::bvminisat::learnts_literals"), + d_statMaxLiterals("theory::bv::bvminisat::max_literals"), + d_statTotLiterals("theory::bv::bvminisat::tot_literals"), + d_statEliminatedVars("theory::bv::bvminisat::eliminated_vars") +{ + StatisticsRegistry::registerStat(&d_statStarts); + StatisticsRegistry::registerStat(&d_statDecisions); + StatisticsRegistry::registerStat(&d_statRndDecisions); + StatisticsRegistry::registerStat(&d_statPropagations); + StatisticsRegistry::registerStat(&d_statConflicts); + StatisticsRegistry::registerStat(&d_statClausesLiterals); + StatisticsRegistry::registerStat(&d_statLearntsLiterals); + StatisticsRegistry::registerStat(&d_statMaxLiterals); + StatisticsRegistry::registerStat(&d_statTotLiterals); + StatisticsRegistry::registerStat(&d_statEliminatedVars); +} + +MinisatSatSolver::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_statStarts); + StatisticsRegistry::unregisterStat(&d_statDecisions); + StatisticsRegistry::unregisterStat(&d_statRndDecisions); + StatisticsRegistry::unregisterStat(&d_statPropagations); + StatisticsRegistry::unregisterStat(&d_statConflicts); + StatisticsRegistry::unregisterStat(&d_statClausesLiterals); + StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); + StatisticsRegistry::unregisterStat(&d_statMaxLiterals); + StatisticsRegistry::unregisterStat(&d_statTotLiterals); + StatisticsRegistry::unregisterStat(&d_statEliminatedVars); +} + +void MinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ + d_statStarts.setData(minisat->starts); + d_statDecisions.setData(minisat->decisions); + d_statRndDecisions.setData(minisat->rnd_decisions); + d_statPropagations.setData(minisat->propagations); + d_statConflicts.setData(minisat->conflicts); + d_statClausesLiterals.setData(minisat->clauses_literals); + d_statLearntsLiterals.setData(minisat->learnts_literals); + d_statMaxLiterals.setData(minisat->max_literals); + d_statTotLiterals.setData(minisat->tot_literals); + d_statEliminatedVars.setData(minisat->eliminated_vars); +} + + + +//// DPllMinisatSatSolver + +DPLLMinisatSatSolver::DPLLMinisatSatSolver() : + d_minisat(NULL), + d_theoryProxy(NULL), + d_context(NULL) +{} + +DPLLMinisatSatSolver::~DPLLMinisatSatSolver() { + delete d_minisat; +} + +SatVariable DPLLMinisatSatSolver::toSatVariable(Minisat::Var var) { + if (var == var_Undef) { + return undefSatVariable; + } + return SatVariable(var); +} + +Minisat::Lit DPLLMinisatSatSolver::toMinisatLit(SatLiteral lit) { + if (lit == undefSatLiteral) { + return Minisat::lit_Undef; + } + return Minisat::mkLit(lit.getSatVariable(), lit.isNegated()); +} + +SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) { + if (lit == Minisat::lit_Undef) { + return undefSatLiteral; + } + + return SatLiteral(SatVariable(Minisat::var(lit)), + Minisat::sign(lit)); +} + +SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) { + if(res) return SatValTrue; + else return SatValFalse; +} + +SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { + if(res == (Minisat::lbool((uint8_t)0))) return SatValTrue; + if(res == (Minisat::lbool((uint8_t)2))) return SatValUnknown; + Assert(res == (Minisat::lbool((uint8_t)1))); + return SatValFalse; +} + + +void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause, + Minisat::vec& minisat_clause) { + for (unsigned i = 0; i < clause.size(); ++i) { + minisat_clause.push(toMinisatLit(clause[i])); + } + Assert(clause.size() == (unsigned)minisat_clause.size()); +} + +void DPLLMinisatSatSolver::toSatClause(Minisat::vec& clause, + SatClause& sat_clause) { + for (int i = 0; i < clause.size(); ++i) { + sat_clause.push_back(toSatLiteral(clause[i])); + } + Assert((unsigned)clause.size() == sat_clause.size()); +} + + +void DPLLMinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) +{ + + d_context = context; + + // Create the solver + d_minisat = new Minisat::SimpSolver(theoryProxy, d_context, + Options::current()->incrementalSolving); + // Setup the verbosity + d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1; + + // Setup the random decision parameters + d_minisat->random_var_freq = Options::current()->satRandomFreq; + d_minisat->random_seed = Options::current()->satRandomSeed; + // Give access to all possible options in the sat solver + d_minisat->var_decay = Options::current()->satVarDecay; + d_minisat->clause_decay = Options::current()->satClauseDecay; + d_minisat->restart_first = Options::current()->satRestartFirst; + d_minisat->restart_inc = Options::current()->satRestartInc; + + d_statistics.init(d_minisat); +} + +void DPLLMinisatSatSolver::addClause(SatClause& clause, bool removable) { + Minisat::vec minisat_clause; + toMinisatClause(clause, minisat_clause); + d_minisat->addClause(minisat_clause, removable); +} + +SatVariable DPLLMinisatSatSolver::newVar(bool theoryAtom) { + return d_minisat->newVar(true, true, theoryAtom); +} + + +SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) { + Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; + if(resource == 0) { + d_minisat->budgetOff(); + } else { + d_minisat->setConfBudget(resource); + } + Minisat::vec empty; + unsigned long conflictsBefore = d_minisat->conflicts; + SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); + d_minisat->clearInterrupt(); + resource = d_minisat->conflicts - conflictsBefore; + Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl; + return result; +} + +SatLiteralValue DPLLMinisatSatSolver::solve() { + d_minisat->budgetOff(); + return toSatLiteralValue(d_minisat->solve()); +} + + +void DPLLMinisatSatSolver::interrupt() { + d_minisat->interrupt(); +} + +SatLiteralValue DPLLMinisatSatSolver::value(SatLiteral l) { + return toSatLiteralValue(d_minisat->value(toMinisatLit(l))); +} + +SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){ + return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l))); +} + +bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const { + return true; +} + +/** Incremental interface */ + +int DPLLMinisatSatSolver::getAssertionLevel() const { + return d_minisat->getAssertionLevel(); +} + +void DPLLMinisatSatSolver::push() { + d_minisat->push(); +} + +void DPLLMinisatSatSolver::pop(){ + d_minisat->pop(); +} + +void DPLLMinisatSatSolver::unregisterVar(SatLiteral lit) { + d_minisat->unregisterVar(toMinisatLit(lit)); +} + +void DPLLMinisatSatSolver::renewVar(SatLiteral lit, int level) { + d_minisat->renewVar(toMinisatLit(lit), level); +} + +/// Statistics for DPLLMinisatSatSolver + +DPLLMinisatSatSolver::Statistics::Statistics() : + d_statStarts("sat::starts"), + d_statDecisions("sat::decisions"), + d_statRndDecisions("sat::rnd_decisions"), + d_statPropagations("sat::propagations"), + d_statConflicts("sat::conflicts"), + d_statClausesLiterals("sat::clauses_literals"), + d_statLearntsLiterals("sat::learnts_literals"), + d_statMaxLiterals("sat::max_literals"), + d_statTotLiterals("sat::tot_literals") +{ + StatisticsRegistry::registerStat(&d_statStarts); + StatisticsRegistry::registerStat(&d_statDecisions); + StatisticsRegistry::registerStat(&d_statRndDecisions); + StatisticsRegistry::registerStat(&d_statPropagations); + StatisticsRegistry::registerStat(&d_statConflicts); + StatisticsRegistry::registerStat(&d_statClausesLiterals); + StatisticsRegistry::registerStat(&d_statLearntsLiterals); + StatisticsRegistry::registerStat(&d_statMaxLiterals); + StatisticsRegistry::registerStat(&d_statTotLiterals); +} +DPLLMinisatSatSolver::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_statStarts); + StatisticsRegistry::unregisterStat(&d_statDecisions); + StatisticsRegistry::unregisterStat(&d_statRndDecisions); + StatisticsRegistry::unregisterStat(&d_statPropagations); + StatisticsRegistry::unregisterStat(&d_statConflicts); + StatisticsRegistry::unregisterStat(&d_statClausesLiterals); + StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); + StatisticsRegistry::unregisterStat(&d_statMaxLiterals); + StatisticsRegistry::unregisterStat(&d_statTotLiterals); +} +void DPLLMinisatSatSolver::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); + d_statPropagations.setData(d_minisat->propagations); + d_statConflicts.setData(d_minisat->conflicts); + d_statClausesLiterals.setData(d_minisat->clauses_literals); + d_statLearntsLiterals.setData(d_minisat->learnts_literals); + d_statMaxLiterals.setData(d_minisat->max_literals); + d_statTotLiterals.setData(d_minisat->tot_literals); +} + + +/* + + SatSolverFactory + + */ + +MinisatSatSolver* SatSolverFactory::createMinisat() { + return new MinisatSatSolver(); +} + +DPLLMinisatSatSolver* SatSolverFactory::createDPLLMinisat(){ + return new DPLLMinisatSatSolver(); +} + + +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h new file mode 100644 index 000000000..56c6c2783 --- /dev/null +++ b/src/prop/sat_solver.h @@ -0,0 +1,297 @@ +/********************* */ +/*! \file sat_module.h + ** \verbatim + ** Original author: lianah + ** Major contributors: + ** Minor contributors (to current version): + ** 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 SAT Solver. + ** + ** SAT Solver. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROP__SAT_MODULE_H +#define __CVC4__PROP__SAT_MODULE_H + +#include +#include "util/options.h" +#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 { + +class TheoryProxy; + +enum SatLiteralValue { + SatValUnknown, + SatValTrue, + SatValFalse +}; + + +typedef uint64_t SatVariable; +// special constant +const SatVariable undefSatVariable = SatVariable(-1); + +class SatLiteral { + uint64_t d_value; +public: + SatLiteral() : + d_value(undefSatVariable) + {} + + SatLiteral(SatVariable var, bool negated = false) { d_value = var + var + (int)negated; } + SatLiteral operator~() { + return SatLiteral(getSatVariable(), !isNegated()); + } + bool operator==(const SatLiteral& other) const { + return d_value == other.d_value; + } + bool operator!=(const SatLiteral& other) const { + return !(*this == other); + } + std::string toString(); + bool isNegated() const { return d_value & 1; } + size_t toHash() const {return (size_t)d_value; } + bool isNull() const { return d_value == (uint64_t)-1; } + SatVariable getSatVariable() const {return d_value >> 1; } +}; + +// special constant +const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable); + + +struct SatLiteralHashFunction { + inline size_t operator() (const SatLiteral& literal) const { + return literal.toHash(); + } +}; + +typedef std::vector SatClause; + +class SatSolver { +public: + /** Virtual destructor to make g++ happy */ + 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; + + + /** Check the satisfiability of the added clauses */ + virtual SatLiteralValue solve() = 0; + + /** Check the satisfiability of the added clauses */ + virtual SatLiteralValue solve(long unsigned int&) = 0; + + /** Interrupt the solver */ + virtual void interrupt() = 0; + + /** Call value() during the search.*/ + virtual SatLiteralValue value(SatLiteral l) = 0; + + /** Call modelValue() when the search is done.*/ + virtual SatLiteralValue modelValue(SatLiteral l) = 0; + + virtual void unregisterVar(SatLiteral lit) = 0; + + virtual void renewVar(SatLiteral lit, int level = -1) = 0; + + virtual int getAssertionLevel() const = 0; + +}; + + +class BVSatSolverInterface: public SatSolver { +public: + virtual SatLiteralValue solve(const context::CDList & assumptions) = 0; + + virtual void markUnremovable(SatLiteral lit) = 0; + + virtual void getUnsatCore(SatClause& unsatCore) = 0; +}; + + +class DPLLSatSolverInterface: public SatSolver { +public: + virtual void initialize(context::Context* context, prop::TheoryProxy* theoryProxy) = 0; + + virtual void push() = 0; + + virtual void pop() = 0; + + virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0; + +}; + +// toodo add ifdef + + +class MinisatSatSolver: public BVSatSolverInterface { + BVMinisat::SimpSolver* d_minisat; + + MinisatSatSolver(); +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 & 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& minisat_clause); + static void toSatClause (BVMinisat::vec& clause, SatClause& sat_clause); + + class Statistics { + public: + ReferenceStat d_statStarts, d_statDecisions; + ReferenceStat d_statRndDecisions, d_statPropagations; + ReferenceStat d_statConflicts, d_statClausesLiterals; + ReferenceStat d_statLearntsLiterals, d_statMaxLiterals; + ReferenceStat d_statTotLiterals; + ReferenceStat d_statEliminatedVars; + Statistics(); + ~Statistics(); + void init(BVMinisat::SimpSolver* minisat); + }; + + Statistics d_statistics; + friend class SatSolverFactory; +}; + + +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_clause); + static void toSatClause (Minisat::vec& 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); + + class Statistics { + private: + ReferenceStat d_statStarts, d_statDecisions; + ReferenceStat d_statRndDecisions, d_statPropagations; + ReferenceStat d_statConflicts, d_statClausesLiterals; + ReferenceStat d_statLearntsLiterals, d_statMaxLiterals; + ReferenceStat d_statTotLiterals; + public: + Statistics(); + ~Statistics(); + void init(Minisat::SimpSolver* d_minisat); + }; + Statistics d_statistics; + + friend class SatSolverFactory; +}; + +class SatSolverFactory { +public: + static MinisatSatSolver* createMinisat(); + static DPLLMinisatSatSolver* createDPLLMinisat(); +}; + +}/* prop namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PROP__SAT_MODULE_H */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 85dcae68b..2934bcad9 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -29,7 +29,7 @@ #include "util/options.h" #include "util/stats.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" namespace CVC4 { diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index 6cbec732c..c0855122e 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -18,7 +18,7 @@ #include "bitblast_strategies.h" #include "bv_sat.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" #include "theory/booleans/theory_bool_rewriter.h" using namespace CVC4::prop; diff --git a/src/theory/bv/bitblast_strategies.h b/src/theory/bv/bitblast_strategies.h index c445af626..826b61d4f 100644 --- a/src/theory/bv/bitblast_strategies.h +++ b/src/theory/bv/bitblast_strategies.h @@ -23,7 +23,7 @@ #include "expr/node.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" namespace CVC4 { diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp index d386fd4db..f580aee44 100644 --- a/src/theory/bv/bv_sat.cpp +++ b/src/theory/bv/bv_sat.cpp @@ -21,7 +21,7 @@ #include "theory_bv_utils.h" #include "theory/rewriter.h" #include "prop/cnf_stream.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" using namespace std; diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h index 3ffc79b7a..c0f3b75ed 100644 --- a/src/theory/bv/bv_sat.h +++ b/src/theory/bv/bv_sat.h @@ -37,7 +37,7 @@ #include "util/stats.h" #include "bitblast_strategies.h" -#include "prop/sat_module.h" +#include "prop/sat_solver.h" namespace CVC4 {