theory_proxy.cpp \
cnf_stream.h \
cnf_stream.cpp \
- sat_module.h \
- sat_module.cpp
+ sat_solver.h \
+ sat_solver.cpp
SUBDIRS = minisat bvminisat
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) {
}
}
-TseitinCnfStream::TseitinCnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap) :
+TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap) :
CnfStream(satSolver, registrar, fullLitToNodeMap) {
}
protected:
/** The SAT solver we will be using */
- SatSolverInterface *d_satSolver;
+ SatSolver *d_satSolver;
TranslationCache d_translationCache;
NodeCache d_nodeCache;
* @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
* @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:
#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"
#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"
+++ /dev/null
-/********************* */
-/*! \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<BVMinisat::Lit> 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<BVMinisat::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") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl;
- return result;
-}
-
-SatLiteralValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions){
- Debug("sat::minisat") << "Solve with assumptions ";
- context::CDList<SatLiteral>::const_iterator it = assumptions.begin();
- BVMinisat::vec<BVMinisat::Lit> 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<BVMinisat::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 MinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::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());
-}
-
-
-// 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::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);
-}
-
-
-/*
-
- SatSolverFactory
-
- */
-
-MinisatSatSolver* SatSolverFactory::createMinisat() {
- return new MinisatSatSolver();
-}
-
-DPLLMinisatSatSolver* SatSolverFactory::createDPLLMinisat(){
- return new DPLLMinisatSatSolver();
-}
-
-
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \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 <stdint.h>
-#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<SatLiteral> 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<SatLiteral> & 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<SatLiteral> & assumptions);
- void getUnsatCore(SatClause& unsatCore);
-
- SatLiteralValue value(SatLiteral l);
- SatLiteralValue modelValue(SatLiteral l);
-
- void unregisterVar(SatLiteral lit);
- void renewVar(SatLiteral lit, int level = -1);
- int getAssertionLevel() const;
-
-
- // helper methods for converting from the internal Minisat representation
-
- static SatVariable toSatVariable(BVMinisat::Var var);
- static BVMinisat::Lit toMinisatLit(SatLiteral lit);
- static SatLiteral toSatLiteral(BVMinisat::Lit lit);
- static SatLiteralValue toSatLiteralValue(bool res);
- static SatLiteralValue toSatLiteralValue(BVMinisat::lbool res);
-
- static void toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause);
- static void toSatClause (BVMinisat::vec<BVMinisat::Lit>& clause, SatClause& sat_clause);
-
- class Statistics {
- public:
- ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
- ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
- ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
- ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals;
- ReferenceStat<uint64_t> d_statTotLiterals;
- ReferenceStat<int> d_statEliminatedVars;
- Statistics();
- ~Statistics();
- void init(BVMinisat::SimpSolver* minisat);
- };
-
- Statistics d_statistics;
- friend class SatSolverFactory;
-};
-
-
-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;
-};
-
-class SatSolverFactory {
-public:
- static MinisatSatSolver* createMinisat();
- static DPLLMinisatSatSolver* createDPLLMinisat();
-};
-
-}/* prop namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PROP__SAT_MODULE_H */
--- /dev/null
+/********************* */
+/*! \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<BVMinisat::Lit> 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<BVMinisat::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") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl;
+ return result;
+}
+
+SatLiteralValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions){
+ Debug("sat::minisat") << "Solve with assumptions ";
+ context::CDList<SatLiteral>::const_iterator it = assumptions.begin();
+ BVMinisat::vec<BVMinisat::Lit> 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<BVMinisat::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 MinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::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());
+}
+
+
+// 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::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);
+}
+
+
+/*
+
+ SatSolverFactory
+
+ */
+
+MinisatSatSolver* SatSolverFactory::createMinisat() {
+ return new MinisatSatSolver();
+}
+
+DPLLMinisatSatSolver* SatSolverFactory::createDPLLMinisat(){
+ return new DPLLMinisatSatSolver();
+}
+
+
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \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 <stdint.h>
+#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<SatLiteral> 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<SatLiteral> & 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<SatLiteral> & assumptions);
+ void getUnsatCore(SatClause& unsatCore);
+
+ SatLiteralValue value(SatLiteral l);
+ SatLiteralValue modelValue(SatLiteral l);
+
+ void unregisterVar(SatLiteral lit);
+ void renewVar(SatLiteral lit, int level = -1);
+ int getAssertionLevel() const;
+
+
+ // helper methods for converting from the internal Minisat representation
+
+ static SatVariable toSatVariable(BVMinisat::Var var);
+ static BVMinisat::Lit toMinisatLit(SatLiteral lit);
+ static SatLiteral toSatLiteral(BVMinisat::Lit lit);
+ static SatLiteralValue toSatLiteralValue(bool res);
+ static SatLiteralValue toSatLiteralValue(BVMinisat::lbool res);
+
+ static void toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause);
+ static void toSatClause (BVMinisat::vec<BVMinisat::Lit>& clause, SatClause& sat_clause);
+
+ class Statistics {
+ public:
+ ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
+ ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
+ ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
+ ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals;
+ ReferenceStat<uint64_t> d_statTotLiterals;
+ ReferenceStat<int> d_statEliminatedVars;
+ Statistics();
+ ~Statistics();
+ void init(BVMinisat::SimpSolver* minisat);
+ };
+
+ Statistics d_statistics;
+ friend class SatSolverFactory;
+};
+
+
+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;
+};
+
+class SatSolverFactory {
+public:
+ static MinisatSatSolver* createMinisat();
+ static DPLLMinisatSatSolver* createDPLLMinisat();
+};
+
+}/* prop namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PROP__SAT_MODULE_H */
#include "util/options.h"
#include "util/stats.h"
-#include "prop/sat_module.h"
+#include "prop/sat_solver.h"
namespace CVC4 {
#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;
#include "expr/node.h"
-#include "prop/sat_module.h"
+#include "prop/sat_solver.h"
namespace CVC4 {
#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;
#include "util/stats.h"
#include "bitblast_strategies.h"
-#include "prop/sat_module.h"
+#include "prop/sat_solver.h"
namespace CVC4 {
projects / cvc5.git / commitdiff