From: Dejan Jovanović Date: Sun, 25 Mar 2012 20:45:45 +0000 (+0000) Subject: moving minisat implementation into their respective directories (regular and bv) X-Git-Tag: cvc5-1.0.0~8266 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=70c23e23c3bfc8aa3fdf285fc643b0438359d22a;p=cvc5.git moving minisat implementation into their respective directories (regular and bv) --- diff --git a/src/prop/bvminisat/Makefile.am b/src/prop/bvminisat/Makefile.am index 480e4e83c..685dfac7d 100644 --- a/src/prop/bvminisat/Makefile.am +++ b/src/prop/bvminisat/Makefile.am @@ -22,7 +22,9 @@ libbvminisat_la_SOURCES = \ mtl/Sort.h \ mtl/Vec.h \ mtl/XAlloc.h \ - utils/Options.h + utils/Options.h \ + bvminisat.h \ + bvminisat.cpp EXTRA_DIST = \ core/Main.cc \ diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp new file mode 100644 index 000000000..d4e123489 --- /dev/null +++ b/src/prop/bvminisat/bvminisat.cpp @@ -0,0 +1,232 @@ +/********************* */ +/*! \file bvminisat.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 (bitvectors). + **/ + +#include "prop/bvminisat/bvminisat.h" +#include "prop/bvminisat/simp/SimpSolver.h" + +using namespace CVC4; +using namespace prop; + +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); +} diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h new file mode 100644 index 000000000..7c12fcbd0 --- /dev/null +++ b/src/prop/bvminisat/bvminisat.h @@ -0,0 +1,87 @@ +/********************* */ +/*! \file bvminisat.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 (bitvectors). + **/ + +#pragma once + +#include "prop/sat_solver.h" +#include "prop/bvminisat/simp/SimpSolver.h" + +namespace CVC4 { +namespace prop { + +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; +}; + +} +} + + + + 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_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); +} 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_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; +}; + +} // prop namespace +} // cvc4 namespace + diff --git a/src/prop/sat_solver.cpp b/src/prop/sat_solver.cpp index 13f2498f2..d3710b617 100644 --- a/src/prop/sat_solver.cpp +++ b/src/prop/sat_solver.cpp @@ -24,12 +24,8 @@ #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" - +#include "prop/minisat/minisat.h" +#include "prop/bvminisat/bvminisat.h" using namespace std; @@ -42,434 +38,11 @@ string SatLiteral::toString() { 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() { +BVSatSolverInterface* SatSolverFactory::createMinisat() { return new MinisatSatSolver(); } -DPLLMinisatSatSolver* SatSolverFactory::createDPLLMinisat(){ +DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(){ return new DPLLMinisatSatSolver(); } 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 & 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; + 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_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); +inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { + out << lit.toString(); + return out; +} - 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; +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 */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 2934bcad9..8b585710f 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -123,41 +123,6 @@ inline TheoryProxy::TheoryProxy(PropEngine* propEngine, }/* CVC4::prop namespace */ -inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { - out << lit.toString(); - return out; -} - -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; -} - -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; - } - - out << str; - return out; -} - }/* CVC4 namespace */ #endif /* __CVC4__PROP__SAT_H */