diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/Makefile.am | 3 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 5 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 2 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 3 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 23 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 9 | ||||
-rw-r--r-- | src/prop/options | 31 | ||||
-rw-r--r-- | src/prop/options_handlers.h | 49 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 10 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 2 | ||||
-rw-r--r-- | src/prop/sat_module.cpp | 478 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 1 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 23 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 1 |
14 files changed, 607 insertions, 33 deletions
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 5e6b18c19..f109e0ed2 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -22,5 +22,8 @@ libprop_la_SOURCES = \ sat_solver_registry.h \ sat_solver_registry.cpp +EXTRA_DIST = \ + options_handlers.h + SUBDIRS = minisat bvminisat diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 94f3a6b74..293ddd657 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -27,7 +27,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "util/output.h" #include "util/utility.h" -#include "util/options.h" + +#include "theory/bv/options.h" using namespace BVMinisat; @@ -423,7 +424,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip out_btlevel = level(var(p)); } - if (out_learnt.size() > 0 && clause_all_marker && CVC4::Options::current()->bitvectorShareLemmas) { + if (out_learnt.size() > 0 && clause_all_marker && CVC4::options::bitvectorShareLemmas()) { notify->notify(out_learnt); } diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 485ddbb55..b498f1e40 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -202,7 +202,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { // If it's a theory literal, need to store it for back queries if ( theoryLiteral || d_fullLitToNodeMap || - ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) || + ( CVC4_USE_REPLAY && options::replayLog() != NULL ) || (Dump.isOn("clauses")) ) { d_nodeCache[lit] = node; d_nodeCache[~lit] = node.notNode(); diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 4c5743c7c..675bc8f4e 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/theory_proxy.h" #include "prop/minisat/minisat.h" +#include "prop/options.h" #include "util/output.h" #include "expr/command.h" #include "proof/proof_manager.h" @@ -1079,7 +1080,7 @@ lbool Solver::search(int nof_conflicts) (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); } - if (theoryConflict && Options::current()->sat_refine_conflicts) { + if (theoryConflict && options::sat_refine_conflicts()) { check_type = CHECK_FINAL_FAKE; } else { check_type = CHECK_WITH_THEORY; diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 6fa698bd0..464a41d74 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -18,6 +18,9 @@ #include "prop/minisat/minisat.h" #include "prop/minisat/simp/SimpSolver.h" +#include "prop/options.h" +#include "smt/options.h" +#include "decision/options.h" using namespace CVC4; using namespace CVC4::prop; @@ -106,26 +109,26 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory d_context = context; - if( Options::current()->decisionMode != Options::DECISION_STRATEGY_INTERNAL ) { + if( options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL ) { Notice() << "minisat: Incremental solving is disabled" << " unless using internal decision strategy." << std::endl; } // Create the solver d_minisat = new Minisat::SimpSolver(theoryProxy, d_context, - Options::current()->incrementalSolving || - Options::current()->decisionMode != Options::DECISION_STRATEGY_INTERNAL ); + options::incrementalSolving() || + options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL ); // Setup the verbosity - d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1; + d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1; // Setup the random decision parameters - d_minisat->random_var_freq = Options::current()->satRandomFreq; - d_minisat->random_seed = Options::current()->satRandomSeed; + d_minisat->random_var_freq = options::satRandomFreq(); + d_minisat->random_seed = options::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_minisat->var_decay = options::satVarDecay(); + d_minisat->clause_decay = options::satClauseDecay(); + d_minisat->restart_first = options::satRestartFirst(); + d_minisat->restart_inc = options::satRestartInc(); d_statistics.init(d_minisat); } diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 8da3856ff..bf04cec8d 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -21,6 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Sort.h" #include "prop/minisat/simp/SimpSolver.h" #include "prop/minisat/utils/System.h" +#include "prop/options.h" #include "proof/proof.h" using namespace Minisat; using namespace CVC4; @@ -52,7 +53,7 @@ SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* c , simp_garbage_frac (opt_simp_garbage_frac) , use_asymm (opt_use_asymm) , use_rcheck (opt_use_rcheck) - , use_elim (!enableIncremental) + , use_elim (options::minisatUseElim() && !enableIncremental) , merges (0) , asymm_lits (0) , eliminated_vars (0) @@ -63,6 +64,12 @@ SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* c , bwdsub_assigns (0) , n_touched (0) { + if(options::minisatUseElim() && + options::minisatUseElim.wasSetByUser() && + enableIncremental) { + WarningOnce() << "Incremental mode incompatible with --minisat-elimination" << std::endl; + } + vec<Lit> dummy(1,lit_Undef); ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below. bwdsub_tmpunit = ca.alloc(0, dummy); diff --git a/src/prop/options b/src/prop/options new file mode 100644 index 000000000..c3c2674c4 --- /dev/null +++ b/src/prop/options @@ -0,0 +1,31 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module PROP "prop/options.h" SAT layer + +option - --show-sat-solvers void :handler CVC4::prop::showSatSolvers :handler-include "prop/options_handlers.h" + show all available SAT solvers + +option satRandomFreq random-frequency --random-freq=P double :default 0.0 :predicate greater_equal(0.0) less_equal(1.0) + sets the frequency of random decisions in the sat solver (P=0.0 by default) +option satRandomSeed random-seed --random-seed=S double :default 91648253 :read-write + sets the random seed for the sat solver + +option satVarDecay double :default 0.95 :predicate less_equal(1.0) greater_equal(0.0) + variable activity decay factor for Minisat +option satClauseDecay double :default 0.999 :predicate less_equal(1.0) greater_equal(0.0) + clause activity decay factor for Minisat +option satRestartFirst --restart-int-base=N unsigned :default 25 + sets the base restart interval for the sat solver (N=25 by default) +option satRestartInc --restart-int-inc=F double :default 3.0 :predicate greater_equal(0.0) + sets the restart interval increase factor for the sat solver (F=3.0 by default) + +option sat_refine_conflicts --refine-conflicts bool + refine theory conflict clauses + +option minisatUseElim --minisat-elimination bool :default true + use Minisat elimination + +endmodule diff --git a/src/prop/options_handlers.h b/src/prop/options_handlers.h new file mode 100644 index 000000000..efcb8d911 --- /dev/null +++ b/src/prop/options_handlers.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file options_handlers.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 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 "cvc4_private.h" + +#ifndef __CVC4__PROP__OPTIONS_HANDLERS_H +#define __CVC4__PROP__OPTIONS_HANDLERS_H + +#include "prop/sat_solver_factory.h" +#include <string> +#include <vector> + +namespace CVC4 { +namespace prop { + +inline void showSatSolvers(std::string option, SmtEngine* smt) { + std::vector<std::string> solvers; + SatSolverFactory::getSolverIds(solvers); + printf("Available SAT solvers: "); + for (unsigned i = 0; i < solvers.size(); ++ i) { + if (i > 0) { + printf(", "); + } + printf("%s", solvers[i].c_str()); + } + printf("\n"); + exit(0); +} + +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PROP__OPTIONS_HANDLERS_H */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 0f138eb65..54309cd01 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -23,10 +23,12 @@ #include "prop/sat_solver_factory.h" #include "decision/decision_engine.h" +#include "decision/options.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" #include "util/Assert.h" -#include "util/options.h" +#include "options/options.h" +#include "smt/options.h" #include "util/output.h" #include "util/result.h" #include "expr/expr.h" @@ -80,8 +82,8 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* context) : d_cnfStream = new CVC4::prop::TseitinCnfStream (d_satSolver, registrar, // fullLitToNode Map = - Options::current()->threads > 1 || - Options::current()->decisionMode == Options::DECISION_STRATEGY_RELEVANCY); + options::threads() > 1 || + options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY); d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream)); @@ -165,7 +167,7 @@ Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) { // TODO This currently ignores conflicts (a dangerous practice). d_theoryEngine->presolve(); - if(Options::current()->preprocessOnly) { + if(options::preprocessOnly()) { millis = resource = 0; return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK); } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index dcfc5a9df..2d4e08db7 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -24,7 +24,7 @@ #define __CVC4__PROP_ENGINE_H #include "expr/node.h" -#include "util/options.h" +#include "options/options.h" #include "util/result.h" #include "smt/modal_exception.h" #include <sys/time.h> diff --git a/src/prop/sat_module.cpp b/src/prop/sat_module.cpp new file mode 100644 index 000000000..ca41eac2f --- /dev/null +++ b/src/prop/sat_module.cpp @@ -0,0 +1,478 @@ +/********************* */ +/*! \file sat.cpp + ** \verbatim + ** Original author: cconway + ** Major contributors: dejan, taking, mdeters, lianah + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "prop/prop_engine.h" +#include "prop/sat_module.h" +#include "context/context.h" +#include "theory/theory_engine.h" +#include "expr/expr_stream.h" +#include "prop/sat.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::incrementalSolving()); + // Setup the verbosity + d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1; + + // Setup the random decision parameters + d_minisat->random_var_freq = options::satRandomFreq(); + d_minisat->random_seed = options::satRandomSeed(); + // Give access to all possible options in the sat solver + d_minisat->var_decay = options::satVarDecay(); + d_minisat->clause_decay = options::satClauseDecay(); + d_minisat->restart_first = options::satRestartFirst(); + d_minisat->restart_inc = options::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 */ diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index c30f18d29..ac80e4422 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -23,7 +23,6 @@ #include <string> #include <stdint.h> -#include "util/options.h" #include "util/stats.h" #include "context/cdlist.h" #include "prop/sat_solver_types.h" diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 10d2aee8c..9ed2202fe 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -25,6 +25,7 @@ #include "theory/rewriter.h" #include "expr/expr_stream.h" #include "decision/decision_engine.h" +#include "decision/options.h" #include "util/lemma_input_channel.h" #include "util/lemma_output_channel.h" @@ -94,7 +95,7 @@ SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) { if(stopSearch) { Trace("decision") << " *** Decision Engine stopped search *** " << std::endl; } - return Options::current()->decisionOptions.stopOnly ? undefSatLiteral : ret; + return options::decisionStopOnly() ? undefSatLiteral : ret; } bool TheoryProxy::theoryNeedCheck() const { @@ -115,10 +116,10 @@ void TheoryProxy::notifyRestart() { static uint32_t lemmaCount = 0; - if(Options::current()->lemmaInputChannel != NULL) { - while(Options::current()->lemmaInputChannel->hasNewLemma()) { + if(options::lemmaInputChannel() != NULL) { + while(options::lemmaInputChannel()->hasNewLemma()) { Debug("shared") << "shared" << std::endl; - Expr lemma = Options::current()->lemmaInputChannel->getNewLemma(); + Expr lemma = options::lemmaInputChannel()->getNewLemma(); Node asNode = lemma.getNode(); asNode = theory::Rewriter::rewrite(asNode); @@ -142,10 +143,10 @@ void TheoryProxy::notifyRestart() { void TheoryProxy::notifyNewLemma(SatClause& lemma) { Assert(lemma.size() > 0); - if(Options::current()->lemmaOutputChannel != NULL) { + if(options::lemmaOutputChannel() != NULL) { if(lemma.size() == 1) { // cannot share units yet - //Options::current()->lemmaOutputChannel->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr()); + //options::lemmaOutputChannel()->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr()); } else { NodeBuilder<> b(kind::OR); for(unsigned i = 0, i_end = lemma.size(); i < i_end; ++i) { @@ -155,7 +156,7 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) { if(d_shared.find(n) == d_shared.end()) { d_shared.insert(n); - Options::current()->lemmaOutputChannel->notifyNewLemma(n.toExpr()); + options::lemmaOutputChannel()->notifyNewLemma(n.toExpr()); } else { Debug("shared") <<"drop new " << n << std::endl; } @@ -165,8 +166,8 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) { SatLiteral TheoryProxy::getNextReplayDecision() { #ifdef CVC4_REPLAY - if(Options::current()->replayStream != NULL) { - Expr e = Options::current()->replayStream->nextExpr(); + if(options::replayStream() != NULL) { + Expr e = options::replayStream()->nextExpr(); if(!e.isNull()) { // we get null node when out of decisions to replay // convert & return return d_cnfStream->getLiteral(e); @@ -179,9 +180,9 @@ SatLiteral TheoryProxy::getNextReplayDecision() { void TheoryProxy::logDecision(SatLiteral lit) { #ifdef CVC4_REPLAY - if(Options::current()->replayLog != NULL) { + if(options::replayLog() != NULL) { Assert(lit != undefSatLiteral, "logging an `undef' decision ?!"); - *Options::current()->replayLog << d_cnfStream->getNode(lit) << std::endl; + *options::replayLog() << d_cnfStream->getNode(lit) << std::endl; } #endif /* CVC4_REPLAY */ } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 26357886c..e8da202bd 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -26,7 +26,6 @@ #define __CVC4_USE_MINISAT #include "theory/theory.h" -#include "util/options.h" #include "util/stats.h" #include "context/cdqueue.h" |