diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-25 20:45:45 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-25 20:45:45 +0000 |
commit | 70c23e23c3bfc8aa3fdf285fc643b0438359d22a (patch) | |
tree | 3f8f1797e0f8dd3d977f983c1ab823c682f51551 /src/prop/minisat | |
parent | 0d080430206880ffc19050acfa01aae1475f1978 (diff) |
moving minisat implementation into their respective directories (regular and bv)
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/Makefile.am | 4 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 2 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 228 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 101 |
4 files changed, 333 insertions, 2 deletions
diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am index 6e003c248..045cc3616 100644 --- a/src/prop/minisat/Makefile.am +++ b/src/prop/minisat/Makefile.am @@ -22,7 +22,9 @@ libminisat_la_SOURCES = \ mtl/Sort.h \ mtl/Vec.h \ mtl/XAlloc.h \ - utils/Options.h + utils/Options.h \ + minisat.cpp \ + minisat.h EXTRA_DIST = \ core/Main.cc \ diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index e5a6d32e1..d75421e25 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_solver.h" +#include "prop/minisat/minisat.h" #include "util/output.h" #include "expr/command.h" #include "proof/proof_manager.h" diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp new file mode 100644 index 000000000..bc611a097 --- /dev/null +++ b/src/prop/minisat/minisat.cpp @@ -0,0 +1,228 @@ +/********************* */ +/*! \file minisat.cpp + ** \verbatim + ** Original author: dejan + ** 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. + ** + ** Implementation of the minisat for cvc4. + **/ + +#include "prop/minisat/minisat.h" +#include "prop/minisat/simp/SimpSolver.h" + +using namespace CVC4; +using namespace CVC4::prop; + +//// 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::Lit>& 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<Minisat::Lit>& 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::Lit> 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<Minisat::Lit> 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); +} diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h new file mode 100644 index 000000000..81a12c491 --- /dev/null +++ b/src/prop/minisat/minisat.h @@ -0,0 +1,101 @@ +/********************* */ +/*! \file minisat.h + ** \verbatim + ** Original author: dejan + ** 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. + ** + ** Implementation of the minisat for cvc4. + **/ + +#pragma once + +#include "prop/sat_solver.h" +#include "prop/minisat/simp/SimpSolver.h" + +namespace CVC4 { +namespace prop { + +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); + + 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; + + friend class SatSolverFactory; +}; + +} // prop namespace +} // cvc4 namespace + |