diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 45 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 11 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 129 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 1 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 16 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 6 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 6 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 4 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.h | 2 |
9 files changed, 150 insertions, 70 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index fa5f53113..46b521e6b 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -22,14 +22,15 @@ using namespace CVC4; using namespace prop; -BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext) +BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name) : context::ContextNotifyObj(mainSatContext, false), d_minisat(new BVMinisat::SimpSolver(mainSatContext)), d_minisatNotify(0), d_solveCount(0), d_assertionsCount(0), d_assertionsRealCount(mainSatContext, 0), - d_lastPropagation(mainSatContext, 0) + d_lastPropagation(mainSatContext, 0), + d_statistics(name) { d_statistics.init(d_minisat); } @@ -61,6 +62,7 @@ SatValue BVMinisatSatSolver::propagate() { void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit) { d_minisat->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit))); + markUnremovable(lit); } void BVMinisatSatSolver::explain(SatLiteral lit, std::vector<SatLiteral>& explanation) { @@ -113,9 +115,9 @@ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){ } else { d_minisat->setConfBudget(resource); } - BVMinisat::vec<BVMinisat::Lit> empty; + // BVMinisat::vec<BVMinisat::Lit> empty; unsigned long conflictsBefore = d_minisat->conflicts; - SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); + SatValue result = toSatLiteralValue(d_minisat->solveLimited()); d_minisat->clearInterrupt(); resource = d_minisat->conflicts - conflictsBefore; Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl; @@ -211,20 +213,24 @@ void BVMinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause, // Satistics for BVMinisatSatSolver -BVMinisatSatSolver::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"), - d_statCallsToSolve("theory::bv::bvminisat::calls_to_solve", 0), - d_statSolveTime("theory::bv::bvminisat::solve_time", 0) +BVMinisatSatSolver::Statistics::Statistics(const std::string& prefix) : + d_statStarts("theory::bv::"+prefix+"bvminisat::starts"), + d_statDecisions("theory::bv::"+prefix+"bvminisat::decisions"), + d_statRndDecisions("theory::bv::"+prefix+"bvminisat::rnd_decisions"), + d_statPropagations("theory::bv::"+prefix+"bvminisat::propagations"), + d_statConflicts("theory::bv::"+prefix+"bvminisat::conflicts"), + d_statClausesLiterals("theory::bv::"+prefix+"bvminisat::clauses_literals"), + d_statLearntsLiterals("theory::bv::"+prefix+"bvminisat::learnts_literals"), + d_statMaxLiterals("theory::bv::"+prefix+"bvminisat::max_literals"), + d_statTotLiterals("theory::bv::"+prefix+"bvminisat::tot_literals"), + d_statEliminatedVars("theory::bv::"+prefix+"bvminisat::eliminated_vars"), + d_statCallsToSolve("theory::bv::"+prefix+"bvminisat::calls_to_solve", 0), + d_statSolveTime("theory::bv::"+prefix+"bvminisat::solve_time", 0), + d_registerStats(!prefix.empty()) { + if (!d_registerStats) + return; + StatisticsRegistry::registerStat(&d_statStarts); StatisticsRegistry::registerStat(&d_statDecisions); StatisticsRegistry::registerStat(&d_statRndDecisions); @@ -240,6 +246,8 @@ BVMinisatSatSolver::Statistics::Statistics() : } BVMinisatSatSolver::Statistics::~Statistics() { + if (!d_registerStats) + return; StatisticsRegistry::unregisterStat(&d_statStarts); StatisticsRegistry::unregisterStat(&d_statDecisions); StatisticsRegistry::unregisterStat(&d_statRndDecisions); @@ -255,6 +263,9 @@ BVMinisatSatSolver::Statistics::~Statistics() { } void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ + if (!d_registerStats) + return; + d_statStarts.setData(minisat->starts); d_statDecisions.setData(minisat->decisions); d_statRndDecisions.setData(minisat->rnd_decisions); diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index ebf4a44b4..568d89f7f 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -69,9 +69,10 @@ public: BVMinisatSatSolver() : ContextNotifyObj(NULL, false), d_assertionsRealCount(NULL, (unsigned)0), - d_lastPropagation(NULL, (unsigned)0) + d_lastPropagation(NULL, (unsigned)0), + d_statistics("") { Unreachable(); } - BVMinisatSatSolver(context::Context* mainSatContext); + BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name = ""); ~BVMinisatSatSolver() throw(AssertionException); void setNotify(Notify* notify); @@ -91,7 +92,6 @@ public: SatValue solve(); SatValue solve(long unsigned int&); - SatValue solve(bool quick_solve); void getUnsatCore(SatClause& unsatCore); SatValue value(SatLiteral l); @@ -129,8 +129,9 @@ public: ReferenceStat<uint64_t> d_statTotLiterals; ReferenceStat<int> d_statEliminatedVars; IntStat d_statCallsToSolve; - BackedStat<double> d_statSolveTime; - Statistics(); + BackedStat<double> d_statSolveTime; + bool d_registerStats; + Statistics(const std::string& prefix); ~Statistics(); void init(BVMinisat::SimpSolver* minisat); }; diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 68969c78b..8833eec78 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -59,19 +59,31 @@ std::ostream& operator << (std::ostream& out, const BVMinisat::Clause& c) { static const char* _cat = "CORE"; +// static DoubleOption opt_var_decay (_cat, "var-decay", "The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false)); +// static DoubleOption opt_clause_decay (_cat, "cla-decay", "The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false)); +// static DoubleOption opt_random_var_freq (_cat, "rnd-freq", "The frequency with which the decision heuristic tries to choose a random variable", 0.0, DoubleRange(0, true, 1, true)); +// static DoubleOption opt_random_seed (_cat, "rnd-seed", "Used by the random variable selection", 91648253, DoubleRange(0, false, HUGE_VAL, false)); +// static IntOption opt_ccmin_mode (_cat, "ccmin-mode", "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 0, IntRange(0, 2)); +// static IntOption opt_phase_saving (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2)); +// static BoolOption opt_rnd_init_act (_cat, "rnd-init", "Randomize the initial activity", false); +// static BoolOption opt_luby_restart (_cat, "luby", "Use the Luby restart sequence", true); +// static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 100, IntRange(1, INT32_MAX)); +// static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 1.5, DoubleRange(1, false, HUGE_VAL, false)); +// static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false)); + + static DoubleOption opt_var_decay (_cat, "var-decay", "The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false)); static DoubleOption opt_clause_decay (_cat, "cla-decay", "The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false)); -static DoubleOption opt_random_var_freq (_cat, "rnd-freq", "The frequency with which the decision heuristic tries to choose a random variable", 0.0, DoubleRange(0, true, 1, true)); +static DoubleOption opt_random_var_freq (_cat, "rnd-freq", "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true)); static DoubleOption opt_random_seed (_cat, "rnd-seed", "Used by the random variable selection", 91648253, DoubleRange(0, false, HUGE_VAL, false)); -static IntOption opt_ccmin_mode (_cat, "ccmin-mode", "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 0, IntRange(0, 2)); +static IntOption opt_ccmin_mode (_cat, "ccmin-mode", "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2)); static IntOption opt_phase_saving (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2)); static BoolOption opt_rnd_init_act (_cat, "rnd-init", "Randomize the initial activity", false); static BoolOption opt_luby_restart (_cat, "luby", "Use the Luby restart sequence", true); -static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 100, IntRange(1, INT32_MAX)); -static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 1.5, DoubleRange(1, false, HUGE_VAL, false)); +static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 25, IntRange(1, INT32_MAX)); +static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 3, DoubleRange(1, false, HUGE_VAL, false)); static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false)); - //================================================================================================= // Constructor/Destructor: @@ -395,10 +407,8 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip out_learnt.shrink(i - j); tot_literals += out_learnt.size(); - bool clause_all_marker = true; for (int i = 0; i < out_learnt.size(); ++ i) { if (marker[var(out_learnt[i])] == 0) { - clause_all_marker = false; break; } } @@ -410,9 +420,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip } else{ int max_i = 1; - if (marker[var(out_learnt[0])] == 0) { - clause_all_marker = false; - } // Find the first literal assigned at the next-highest level: for (int i = 2; i < out_learnt.size(); i++) if (level(var(out_learnt[i])) > level(var(out_learnt[max_i]))) @@ -424,10 +431,6 @@ 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::bitvectorShareLemmas()) { - notify->notify(out_learnt); - } - for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) } @@ -462,6 +465,48 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) return true; } +/** + * Specialized analyzeFinal procedure where we test the consistency + * of the assumptions before backtracking bellow the assumption level. + * + * @param p the original uip (may be unit) + * @param confl_clause the conflict clause + * @param out_conflict the conflict in terms of assumptions we are building + */ +void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) { + assert (confl_clause != CRef_Undef); + assert (decisionLevel() == assumptions.size()); + assert (level(var(p)) == assumptions.size()); + + out_conflict.clear(); + + Clause& cl = ca[confl_clause]; + for (int i = 0; i < cl.size(); ++i) { + seen[var(cl[i])] = 1; + } + + for (int i = trail.size() - 1; i >= trail_lim[0]; i--) { + Var x = var(trail[i]); + if (seen[x]) { + if (reason(x) == CRef_Undef) { + // this is the case when p was a unit + if (x == var(p)) + continue; + + assert (marker[x] == 2); + assert (level(x) > 0); + out_conflict.push(~trail[i]); + } else { + Clause& c = ca[reason(x)]; + for (int j = 1; j < c.size(); j++) + if (level(var(c[j])) > 0) + seen[var(c[j])] = 1; + } + seen[x] = 0; + } + } + assert (out_conflict.size()); +} /*_________________________________________________________________________________________________ | @@ -475,7 +520,9 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) { out_conflict.clear(); - out_conflict.push(p); + if (marker[var(p)] == 2) { + out_conflict.push(p); + } if (decisionLevel() == 0) return; @@ -500,6 +547,7 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) } seen[var(p)] = 0; + assert (out_conflict.size()); } @@ -755,28 +803,46 @@ lbool Solver::search(int nof_conflicts, UIP uip) analyze(confl, learnt_clause, backtrack_level, uip); Lit p = learnt_clause[0]; - bool assumption = marker[var(p)] == 2; - - cancelUntil(backtrack_level); - - if (learnt_clause.size() == 1){ - uncheckedEnqueue(p); - }else{ - CRef cr = ca.alloc(learnt_clause, true); - learnts.push(cr); - attachClause(cr); - claBumpActivity(ca[cr]); - uncheckedEnqueue(p, cr); + //bool assumption = marker[var(p)] == 2; + + CRef cr = CRef_Undef; + if (learnt_clause.size() > 1) { + cr = ca.alloc(learnt_clause, true); + learnts.push(cr); + attachClause(cr); + claBumpActivity(ca[cr]); } - // if an assumption, we're done - if (assumption) { - assert(decisionLevel() < assumptions.size()); + // if the uip was an assumption we are unsat + if (level(var(p)) <= assumptions.size()) { + for (int i = 0; i < learnt_clause.size(); ++i) { + assert (level(var(learnt_clause[i])) <= decisionLevel()); + seen[var(learnt_clause[i])] = 1; + } analyzeFinal(p, conflict); Debug("bvminisat::search") << OUTPUT_TAG << " conflict on assumptions " << std::endl; return l_False; } - + + if (!CVC4::options::bvEagerExplanations()) { + // check if uip leads to a conflict + if (backtrack_level < assumptions.size()) { + cancelUntil(assumptions.size()); + uncheckedEnqueue(p, cr); + + CRef new_confl = propagate(); + if (new_confl != CRef_Undef) { + // we have a conflict we now need to explain it + analyzeFinal2(p, new_confl, conflict); + return l_False; + } + } + } + + cancelUntil(backtrack_level); + uncheckedEnqueue(p, cr); + + varDecayActivity(); claDecayActivity(); @@ -835,6 +901,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) // Dummy decision level: newDecisionLevel(); }else if (value(p) == l_False){ + marker[var(p)] = 2; analyzeFinal(~p, conflict); Debug("bvminisat::search") << OUTPUT_TAG << " assumption false, we're unsat" << std::endl; return l_False; diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 53d92ac39..882f23ef7 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -290,6 +290,7 @@ protected: void analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip = UIP_FIRST); // (bt = backtrack) void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? + void analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict); bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') lbool search (int nof_conflicts, UIP uip = UIP_FIRST); // Search for a given number of conflicts. lbool solve_ (); // Main solve method (assumptions given in 'assumptions'). diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index 59820e9e3..c65189985 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -21,7 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "mtl/Sort.h" #include "simp/SimpSolver.h" #include "utils/System.h" - +#include "theory/bv/options.h" +#include "smt/options.h" using namespace BVMinisat; //================================================================================================= @@ -32,7 +33,7 @@ static const char* _cat = "SIMP"; static BoolOption opt_use_asymm (_cat, "asymm", "Shrink clauses by asymmetric branching.", false); static BoolOption opt_use_rcheck (_cat, "rcheck", "Check if a clause is already implied. (costly)", false); -static BoolOption opt_use_elim (_cat, "elim", "Perform variable elimination.", false); +static BoolOption opt_use_elim (_cat, "elim", "Perform variable elimination.", true); static IntOption opt_grow (_cat, "grow", "Allow a variable elimination step to grow by a number of clauses.", 0); static IntOption opt_clause_lim (_cat, "cl-lim", "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20, IntRange(-1, INT32_MAX)); static IntOption opt_subsumption_lim (_cat, "sub-lim", "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX)); @@ -51,11 +52,12 @@ SimpSolver::SimpSolver(CVC4::context::Context* c) : , simp_garbage_frac (opt_simp_garbage_frac) , use_asymm (opt_use_asymm) , use_rcheck (opt_use_rcheck) - , use_elim (opt_use_elim) + , use_elim (opt_use_elim && + CVC4::options::bitblastMode() == CVC4::theory::bv::BITBLAST_MODE_EAGER && + !CVC4::options::produceModels()) , merges (0) , asymm_lits (0) , eliminated_vars (0) - , total_eliminate_time("theory::bv::bvminisat::TotalVariableEliminationTime") , elimorder (1) , use_simplification (true) , occurs (ClauseDeleted(ca)) @@ -63,7 +65,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* c) : , bwdsub_assigns (0) , n_touched (0) { - CVC4::StatisticsRegistry::registerStat(&total_eliminate_time); + vec<Lit> dummy(1,lit_Undef); ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below. bwdsub_tmpunit = ca.alloc(dummy); @@ -87,7 +89,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* c) : SimpSolver::~SimpSolver() { - CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time); + // CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time); } @@ -606,7 +608,7 @@ void SimpSolver::extendModel() bool SimpSolver::eliminate(bool turn_off_elim) { - CVC4::TimerStat::CodeTimer codeTimer(total_eliminate_time); + // CVC4::TimerStat::CodeTimer codeTimer(total_eliminate_time); if (!simplify()) return false; diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 4af82b02d..d808daa22 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -58,6 +58,7 @@ class SimpSolver : public Solver { // bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false); lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false); + lbool solveLimited(bool do_simp = true, bool turn_off_simp = false); bool solve ( bool do_simp = true, bool turn_off_simp = false); bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false); bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); @@ -96,7 +97,7 @@ class SimpSolver : public Solver { int merges; int asymm_lits; int eliminated_vars; - CVC4::TimerStat total_eliminate_time; + // CVC4::TimerStat total_eliminate_time; protected: @@ -195,6 +196,9 @@ inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, boo inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); } +inline lbool SimpSolver::solveLimited (bool do_simp, bool turn_off_simp){ + return solve_(do_simp, turn_off_simp); } + //================================================================================================= } diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 47d352949..3d2c29798 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -228,12 +228,6 @@ SatLiteral CnfStream::convertAtom(TNode node) { theoryLiteral = true; canEliminate = false; preRegister = true; - - if (options::bitvectorEagerBitblast() && theory::Theory::theoryOf(node) == theory::THEORY_BV) { - // All BV atoms are treated as boolean except for equality - theoryLiteral = false; - canEliminate = true; - } } // Make a new literal (variables are not considered theory literals) diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 6cda02c00..e937c718c 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -25,8 +25,8 @@ namespace prop { template class SatSolverConstructor<MinisatSatSolver>; template class SatSolverConstructor<BVMinisatSatSolver>; -BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext) { - return new BVMinisatSatSolver(mainSatContext); +BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, const std::string& name) { + return new BVMinisatSatSolver(mainSatContext, name); } DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() { diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index 7d3a45c59..291609de7 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -28,7 +28,7 @@ namespace prop { class SatSolverFactory { public: - static BVSatSolverInterface* createMinisat(context::Context* mainSatContext); + static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, const std::string& name = ""); static DPLLSatSolverInterface* createDPLLMinisat(); static SatSolver* create(const char* id); |