summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/Makefile.am3
-rw-r--r--src/prop/bvminisat/core/Solver.cc5
-rw-r--r--src/prop/cnf_stream.cpp2
-rw-r--r--src/prop/minisat/core/Solver.cc3
-rw-r--r--src/prop/minisat/minisat.cpp23
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc9
-rw-r--r--src/prop/options31
-rw-r--r--src/prop/options_handlers.h49
-rw-r--r--src/prop/prop_engine.cpp10
-rw-r--r--src/prop/prop_engine.h2
-rw-r--r--src/prop/sat_module.cpp478
-rw-r--r--src/prop/sat_solver.h1
-rw-r--r--src/prop/theory_proxy.cpp23
-rw-r--r--src/prop/theory_proxy.h1
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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback