diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-05-08 21:54:55 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-05-08 21:54:55 +0000 |
commit | 8a0c0562cb8d0e26ea019ff782b25c1997a49a0b (patch) | |
tree | 28239db9bcb26b03d893ad61dd1a7ea099391fbe /src/prop/bvminisat | |
parent | 5082cb8349efbb287084293cd4bc6c3fa5a34f26 (diff) |
Merging in bvprop branch, with proper bit-vector propagation.
This should also fix bug 325.
Diffstat (limited to 'src/prop/bvminisat')
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 18 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 30 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 126 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 53 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 19 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 6 |
6 files changed, 159 insertions, 93 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 232502696..124fc35f1 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -25,6 +25,7 @@ using namespace prop; BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext) : context::ContextNotifyObj(mainSatContext, false), d_minisat(new BVMinisat::SimpSolver(mainSatContext)), + d_minisatNotify(0), d_solveCount(0), d_assertionsCount(0), d_assertionsRealCount(mainSatContext, 0), @@ -36,6 +37,12 @@ BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext) BVMinisatSatSolver::~BVMinisatSatSolver() throw(AssertionException) { delete d_minisat; + delete d_minisatNotify; +} + +void BVMinisatSatSolver::setNotify(Notify* notify) { + d_minisatNotify = new MinisatNotify(notify); + d_minisat->setNotify(d_minisatNotify); } void BVMinisatSatSolver::addClause(SatClause& clause, bool removable) { @@ -52,16 +59,9 @@ void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit) { d_minisat->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit))); } -bool BVMinisatSatSolver::getPropagations(std::vector<SatLiteral>& propagations) { - for (; d_lastPropagation < d_minisat->atom_propagations.size(); d_lastPropagation = d_lastPropagation + 1) { - propagations.push_back(toSatLiteral(d_minisat->atom_propagations[d_lastPropagation])); - } - return propagations.size() > 0; -} - -void BVMinisatSatSolver::explainPropagation(SatLiteral lit, std::vector<SatLiteral>& explanation) { +void BVMinisatSatSolver::explain(SatLiteral lit, std::vector<SatLiteral>& explanation) { std::vector<BVMinisat::Lit> minisat_explanation; - d_minisat->explainPropagation(toMinisatLit(lit), minisat_explanation); + d_minisat->explain(toMinisatLit(lit), minisat_explanation); for (unsigned i = 0; i < minisat_explanation.size(); ++i) { explanation.push_back(toSatLiteral(minisat_explanation[i])); } diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 19b605067..cd2a2c6b9 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -26,14 +26,36 @@ namespace CVC4 { namespace prop { -class BVMinisatSatSolver: public BVSatSolverInterface, public context::ContextNotifyObj { +class BVMinisatSatSolver : public BVSatSolverInterface, public context::ContextNotifyObj { + +private: + + class MinisatNotify : public BVMinisat::Notify { + BVSatSolverInterface::Notify* d_notify; + public: + MinisatNotify(BVSatSolverInterface::Notify* notify) + : d_notify(notify) + {} + bool notify(BVMinisat::Lit lit) { + return d_notify->notify(toSatLiteral(lit)); + } + void notify(BVMinisat::vec<BVMinisat::Lit>& clause) { + SatClause satClause; + toSatClause(clause, satClause); + d_notify->notify(satClause); + } + }; + BVMinisat::SimpSolver* d_minisat; + MinisatNotify* d_minisatNotify; + unsigned d_solveCount; unsigned d_assertionsCount; context::CDO<unsigned> d_assertionsRealCount; context::CDO<unsigned> d_lastPropagation; public: + BVMinisatSatSolver() : ContextNotifyObj(NULL, false), d_assertionsRealCount(NULL, (unsigned)0), @@ -42,6 +64,8 @@ public: BVMinisatSatSolver(context::Context* mainSatContext); ~BVMinisatSatSolver() throw(AssertionException); + void setNotify(Notify* notify); + void addClause(SatClause& clause, bool removable); SatVariable newVar(bool theoryAtom = false); @@ -76,9 +100,7 @@ public: static void toSatClause (BVMinisat::vec<BVMinisat::Lit>& clause, SatClause& sat_clause); void addMarkerLiteral(SatLiteral lit); - bool getPropagations(std::vector<SatLiteral>& propagations); - - void explainPropagation(SatLiteral lit, std::vector<SatLiteral>& explanation); + void explain(SatLiteral lit, std::vector<SatLiteral>& explanation); SatValue assertAssumption(SatLiteral lit, bool propagate); diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 9bded3db5..e24fcac1a 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -24,8 +24,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "core/Solver.h" #include <vector> #include <iostream> + #include "util/output.h" #include "util/utility.h" +#include "util/options.h" using namespace BVMinisat; @@ -51,14 +53,14 @@ 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, 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.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, 0)); +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", 2, DoubleRange(1, false, HUGE_VAL, false)); +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)); @@ -70,7 +72,8 @@ Solver::Solver(CVC4::context::Context* c) : // Parameters (user settable): // - verbosity (0) + c(c) + , verbosity (0) , var_decay (opt_var_decay) , clause_decay (opt_clause_decay) , random_var_freq (opt_random_var_freq) @@ -86,7 +89,7 @@ Solver::Solver(CVC4::context::Context* c) : // Parameters (the rest): // - , learntsize_factor((double)1/(double)3), learntsize_inc(1.1) + , learntsize_factor((double)1/(double)3), learntsize_inc(1.5) // Parameters (experimental): // @@ -115,7 +118,7 @@ Solver::Solver(CVC4::context::Context* c) : , conflict_budget (-1) , propagation_budget (-1) , asynch_interrupt (false) - , d_explanations(c) + , clause_added(false) {} @@ -153,9 +156,9 @@ Var Solver::newVar(bool sign, bool dvar) bool Solver::addClause_(vec<Lit>& ps) { - if (decisionLevel() > 0) { - cancelUntil(0); - } + if (decisionLevel() > 0) { + cancelUntil(0); + } if (!ok) return false; @@ -169,6 +172,8 @@ bool Solver::addClause_(vec<Lit>& ps) ps[j++] = p = ps[i]; ps.shrink(i - j); + clause_added = true; + if (ps.size() == 0) return ok = false; else if (ps.size() == 1){ @@ -183,7 +188,6 @@ bool Solver::addClause_(vec<Lit>& ps) return true; } - void Solver::attachClause(CRef cr) { const Clause& c = ca[cr]; assert(c.size() > 1); @@ -242,11 +246,6 @@ void Solver::cancelUntil(int level) { trail.shrink(trail.size() - trail_lim[level]); trail_lim.shrink(trail_lim.size() - level); } - - if (level < atom_propagations_lim.size()) { - atom_propagations.shrink(atom_propagations.size() - atom_propagations_lim[level]); - atom_propagations_lim.shrink(atom_propagations_lim.size() - level); - } } @@ -379,12 +378,24 @@ 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; + } + } + // Find correct backtrack level: // - if (out_learnt.size() == 1) - out_btlevel = 0; + if (out_learnt.size() == 1) { + out_btlevel = 0; + } 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]))) @@ -396,6 +407,10 @@ 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()->bitvector_share_lemmas) { + notify->notify(out_learnt); + } + for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) } @@ -452,17 +467,16 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) for (int i = trail.size()-1; i >= trail_lim[0]; i--){ Var x = var(trail[i]); - if (seen[x]){ - if (reason(x) == CRef_Undef){ - if (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; + if (seen[x]) { + if (reason(x) == CRef_Undef) { + 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; } @@ -478,31 +492,44 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) assigns[var(p)] = lbool(!sign(p)); vardata[var(p)] = mkVarData(from, decisionLevel()); trail.push_(p); - if (only_bcp && marker[var(p)] == 1 && from != CRef_Undef) { - atom_propagations.push(p); + if (decisionLevel() <= assumptions.size() && marker[var(p)] == 1) { + if (notify) { + notify->notify(p); + } } } void Solver::popAssumption() { - marker[var(assumptions.last())] = 1; - assumptions.pop(); - conflict.clear(); - cancelUntil(assumptions.size()); + assumptions.pop(); + conflict.clear(); + cancelUntil(assumptions.size()); } lbool Solver::assertAssumption(Lit p, bool propagate) { assert(marker[var(p)] == 1); - // add to the assumptions - assumptions.push(p); + if (decisionLevel() > assumptions.size()) { + cancelUntil(assumptions.size()); + } + conflict.clear(); + // add to the assumptions + if (c->getLevel() > 0) { + assumptions.push(p); + } else { + if (!addClause(p)) { + conflict.push(~p); + return l_False; + } + } + // run the propagation if (propagate) { only_bcp = true; ccmin_mode = 0; - lbool result = search(-1, UIP_FIRST); + lbool result = search(-1); return result; } else { return l_True; @@ -702,11 +729,12 @@ lbool Solver::search(int nof_conflicts, UIP uip) learnt_clause.clear(); analyze(confl, learnt_clause, backtrack_level, uip); - cancelUntil(backtrack_level); Lit p = learnt_clause[0]; bool assumption = marker[var(p)] == 2; + cancelUntil(backtrack_level); + if (learnt_clause.size() == 1){ uncheckedEnqueue(p); }else{ @@ -741,10 +769,10 @@ lbool Solver::search(int nof_conflicts, UIP uip) }else{ // NO CONFLICT - if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){ + if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){ // Reached bound on number of conflicts: progress_estimate = progressEstimate(); - cancelUntil(0); + cancelUntil(assumptions.size()); return l_Undef; } // Simplify the set of problem clauses: @@ -890,31 +918,27 @@ lbool Solver::solve_() // Bitvector propagations // -void Solver::storeExplanation(Lit p) { -} +void Solver::explain(Lit p, std::vector<Lit>& explanation) { -void Solver::explainPropagation(Lit p, std::vector<Lit>& explanation) { vec<Lit> queue; queue.push(p); __gnu_cxx::hash_set<Var> visited; visited.insert(var(p)); + while(queue.size() > 0) { Lit l = queue.last(); assert(value(l) == l_True); queue.pop(); if (reason(var(l)) == CRef_Undef) { - if (marker[var(l)] == 2) { - explanation.push_back(l); - visited.insert(var(l)); - } + if (level(var(l)) == 0) continue; + Assert(marker[var(l)] == 2); + explanation.push_back(l); + visited.insert(var(l)); } else { Clause& c = ca[reason(var(l))]; for (int i = 1; i < c.size(); ++i) { - if (var(c[i]) >= vardata.size()) { - std::cerr << "BOOM" << std::endl; - } - if (visited.count(var(c[i])) == 0) { + if (level(var(c[i])) > 0 && visited.count(var(c[i])) == 0) { queue.push(~c[i]); visited.insert(var(c[i])); } diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index c7346d7f7..c323bfe2b 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -34,10 +34,36 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA namespace BVMinisat { +/** Interface for minisat callbacks */ +class Notify { + +public: + + virtual ~Notify() {} + + /** + * If the notify returns false, the solver will break out of whatever it's currently doing + * with an "unknown" answer. + */ + virtual bool notify(Lit lit) = 0; + + /** + * Notify about a new learnt clause with marked literals only. + */ + virtual void notify(vec<Lit>& learnt) = 0; + +}; + //================================================================================================= // Solver -- the main class: - class Solver { + + /** To notify */ + Notify* notify; + + /** Cvc4 context */ + CVC4::context::Context* c; + public: // Constructor/Destructor: @@ -45,6 +71,8 @@ public: Solver(CVC4::context::Context* c); virtual ~Solver(); + void setNotify(Notify* toNotify) { notify = toNotify; } + // Problem specification: // Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. @@ -153,15 +181,15 @@ public: marker[var] = 1; } - __gnu_cxx::hash_set<Var> assumptions_vars; // all the variables that appear in the current assumptions - vec<Lit> atom_propagations; // the atom literals implied by the last call to solve with assumptions - vec<int> atom_propagations_lim; // for backtracking - bool only_bcp; // solving mode in which only boolean constraint propagation is done void setOnlyBCP (bool val) { only_bcp = val;} - void explainPropagation(Lit l, std::vector<Lit>& explanation); + void explain(Lit l, std::vector<Lit>& explanation); + protected: + // has a clause been added + bool clause_added; + // Helper structures: // struct VarData { CRef reason; int level; }; @@ -248,9 +276,6 @@ protected: UIP_LAST }; - CVC4::context::CDHashMap<Lit, std::vector<Lit>, LitHashFunction> d_explanations; - - void storeExplanation (Lit p); // make sure that the explanation of p is cached 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? bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') @@ -346,7 +371,7 @@ inline bool Solver::addClause (Lit p) { add_tmp.clear( inline bool Solver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); } inline bool Solver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); } inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; } -inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); atom_propagations_lim.push(atom_propagations.size()); } +inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } inline int Solver::decisionLevel () const { return trail_lim.size(); } inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } @@ -381,10 +406,10 @@ inline bool Solver::withinBudget() const { // FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a // pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or // all calls to solve must return an 'lbool'. I'm not yet sure which I prefer. -inline bool Solver::solve () { budgetOff(); assumptions.clear(); return solve_() == l_True; } -inline bool Solver::solve (Lit p) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; } -inline bool Solver::solve (Lit p, Lit q) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; } -inline bool Solver::solve (Lit p, Lit q, Lit r) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; } +inline bool Solver::solve () { budgetOff(); return solve_() == l_True; } +inline bool Solver::solve (Lit p) { budgetOff(); assumptions.push(p); return solve_() == l_True; } +inline bool Solver::solve (Lit p, Lit q) { budgetOff(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; } +inline bool Solver::solve (Lit p, Lit q, Lit r) { budgetOff(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; } inline bool Solver::solve (const vec<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; } inline lbool Solver::solveLimited (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); } inline bool Solver::okay () const { return ok; } diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index 903ffa270..c8ce13410 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -32,7 +32,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.", true); +static BoolOption opt_use_elim (_cat, "elim", "Perform variable elimination.", false); 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)); @@ -100,20 +100,14 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool freeze) { lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) { - vec<Lit> atom_propagations_backup; - atom_propagations.moveTo(atom_propagations_backup); - vec<int> atom_propagations_lim_backup; - atom_propagations_lim.moveTo(atom_propagations_lim_backup); - only_bcp = false; - cancelUntil(0); vec<Var> extra_frozen; lbool result = l_True; do_simp &= use_simplification; - if (do_simp){ + if (do_simp) { // Assumptions must be temporarily frozen to run variable elimination: for (int i = 0; i < assumptions.size(); i++){ Var v = var(assumptions[i]); @@ -127,7 +121,11 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) extra_frozen.push(v); } } - result = lbool(eliminate(turn_off_simp)); + if (do_simp && clause_added) { + cancelUntil(0); + result = lbool(eliminate(turn_off_simp)); + clause_added = false; + } } if (result == l_True) @@ -135,9 +133,6 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) else if (verbosity >= 1) printf("===============================================================================\n"); - atom_propagations_backup.moveTo(atom_propagations); - atom_propagations_lim_backup.moveTo(atom_propagations_lim); - if (do_simp) // Unfreeze the assumptions that were frozen: for (int i = 0; i < extra_frozen.size(); i++) diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index e3ef76212..378812e03 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -184,9 +184,9 @@ inline bool SimpSolver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } } inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); return solve_(do_simp, turn_off_simp) == l_True; } -inline bool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; } -inline bool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; } -inline bool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; } +inline bool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; } +inline bool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; } +inline bool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; } inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; |