diff options
33 files changed, 899 insertions, 358 deletions
@@ -1,6 +1,6 @@ <?xml version="1.0" encoding="UTF-8"?> <projectDescription> - <name>cvc4-sharing</name> + <name>cvc4-bvprop</name> <comment></comment> <projects> </projects> diff --git a/.settings/net.certiv.antlrdt.core.prefs b/.settings/net.certiv.antlrdt.core.prefs index fda7c5fb1..40873fc20 100644 --- a/.settings/net.certiv.antlrdt.core.prefs +++ b/.settings/net.certiv.antlrdt.core.prefs @@ -1,4 +1,3 @@ -#Thu Mar 25 16:47:04 EDT 2010 builderLoc=builderLocRelative builderRelPath=./generated eclipse.preferences.version=1 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; diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 79893a087..ea6cafdcd 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -657,6 +657,7 @@ CRef Solver::propagate(TheoryCheckType type) { CRef confl = CRef_Undef; recheck = false; + theoryConflict = false; ScopedBool scoped_bool(minisat_busy, true); @@ -694,7 +695,11 @@ CRef Solver::propagate(TheoryCheckType type) // If no conflict, do the theory check if (confl == CRef_Undef && type != CHECK_WITHOUTH_THEORY) { // Do the theory check - theoryCheck(CVC4::theory::Theory::EFFORT_STANDARD); + if (type == CHECK_FINAL_FAKE) { + theoryCheck(CVC4::theory::Theory::EFFORT_FULL); + } else { + theoryCheck(CVC4::theory::Theory::EFFORT_STANDARD); + } // Pick up the theory propagated literals propagateTheory(); // If there are lemmas (or conflicts) update them @@ -1018,8 +1023,12 @@ lbool Solver::search(int nof_conflicts) (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); } - // We have a conflict so, we are going back to standard checks - check_type = CHECK_WITH_THEORY; + if (theoryConflict && Options::current()->sat_refine_conflicts) { + check_type = CHECK_FINAL_FAKE; + } else { + check_type = CHECK_WITH_THEORY; + } + } else { // If this was a final check, we are satisfiable @@ -1043,6 +1052,8 @@ lbool Solver::search(int nof_conflicts) } return l_True; } + } else if (check_type == CHECK_FINAL_FAKE) { + check_type = CHECK_WITH_THEORY; } if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()) { @@ -1503,14 +1514,6 @@ CRef Solver::updateLemmas() { conflict = CRef_Lazy; } } else { -// if (Debug.isOn("minisat::lemmas")) { -// Debug("minisat::lemmas") << "Solver::updateLemmas(): " << lemma[0] << " from "; -// Clause& c = ca[lemma_ref]; -// for (int i = 0; i < c.size(); ++ i) { -// Debug("minisat::lemmas") << c[i] << "(" << value(c[i]) << "," << level(var(c[i])) << "," << trail_index(var(c[i])) << ") "; -// } -// Debug("minisat::lemmas") << std::endl; -// } Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; uncheckedEnqueue(lemma[0], lemma_ref); if(lemma.size() == 1 && assertionLevel > 0) { @@ -1528,5 +1531,9 @@ CRef Solver::updateLemmas() { lemmas.clear(); lemmas_removable.clear(); + if (conflict != CRef_Undef) { + theoryConflict = true; + } + return conflict; } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index ca5b2c30f..cfeb06211 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -308,7 +308,9 @@ protected: // Check and perform theory reasoning CHECK_WITH_THEORY, // The SAT abstraction of the problem is satisfiable, perform a full theory check - CHECK_FINAL + CHECK_FINAL, + // Perform a full theory check even if not done with everything + CHECK_FINAL_FAKE }; // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is @@ -336,6 +338,7 @@ protected: void newDecisionLevel (); // Begins a new decision level. void uncheckedEnqueue (Lit p, CRef from = CRef_Undef); // Enqueue a literal. Assumes value of literal is undefined. bool enqueue (Lit p, CRef from = CRef_Undef); // Test if fact 'p' contradicts current state, enqueue otherwise. + bool theoryConflict; // Was the last conflict a theory conflict CRef propagate (TheoryCheckType type); // Perform Boolean and Theory. Returns possibly conflicting clause. CRef propagateBool (); // Perform Boolean propagation. Returns possibly conflicting clause. void propagateTheory (); // Perform Theory propagation. diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 4fe24fc60..898709c43 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -73,15 +73,33 @@ public: class BVSatSolverInterface: public SatSolver { public: + /** Interface for notifications */ + 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(SatLiteral lit) = 0; + + /** + * Notify about a learnt clause. + */ + virtual void notify(SatClause& clause) = 0; +}; + + virtual void setNotify(Notify* notify) = 0; + virtual void markUnremovable(SatLiteral lit) = 0; virtual void getUnsatCore(SatClause& unsatCore) = 0; virtual void addMarkerLiteral(SatLiteral lit) = 0; - virtual bool getPropagations(std::vector<SatLiteral>& propagations) = 0; - - virtual void explainPropagation(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0; + virtual void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) = 0; virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0; diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp index 2f4ac1324..dcb33c9af 100644 --- a/src/theory/bv/bv_sat.cpp +++ b/src/theory/bv/bv_sat.cpp @@ -23,7 +23,8 @@ #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" -#include "theory_bv_rewrite_rules_simplification.h" +#include "theory/bv/theory_bv_rewrite_rules_simplification.h" +#include "theory/bv/theory_bv.h" using namespace std; @@ -35,7 +36,6 @@ namespace CVC4 { namespace theory { namespace bv{ - std::string toString(Bits& bits) { ostringstream os; for (int i = bits.size() - 1; i >= 0; --i) { @@ -52,7 +52,8 @@ std::string toString(Bits& bits) { } /////// Bitblaster -Bitblaster::Bitblaster(context::Context* c) : +Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) : + d_bvOutput(bv->d_out), d_termCache(), d_bitblastedAtoms(), d_assertedAtoms(c), @@ -61,6 +62,8 @@ Bitblaster::Bitblaster(context::Context* c) : d_satSolver = prop::SatSolverFactory::createMinisat(c); d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar()); + MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv); + d_satSolver->setNotify(notify); // initializing the bit-blasting strategies initAtomBBStrategies(); initTermBBStrategies(); @@ -79,6 +82,8 @@ Bitblaster::~Bitblaster() { * */ void Bitblaster::bbAtom(TNode node) { + node = node.getKind() == kind::NOT? node[0] : node; + if (hasBBAtom(node)) { return; } @@ -94,8 +99,13 @@ void Bitblaster::bbAtom(TNode node) { Node atom_definition = mkNode(kind::IFF, node, atom_bb); // do boolean simplifications if possible Node rewritten = Rewriter::rewrite(atom_definition); - d_cnfStream->convertAndAssert(rewritten, true, false); - d_bitblastedAtoms.insert(node); + + if (!Options::current()->bitvector_eager_bitblast) { + d_cnfStream->convertAndAssert(rewritten, true, false); + d_bitblastedAtoms.insert(node); + } else { + d_bvOutput->lemma(rewritten, false); + } } @@ -154,65 +164,21 @@ Node Bitblaster::bbOptimize(TNode node) { /// Public methods void Bitblaster::addAtom(TNode atom) { - d_cnfStream->ensureLiteral(atom); - SatLiteral lit = d_cnfStream->getLiteral(atom); - d_satSolver->addMarkerLiteral(lit); -} -bool Bitblaster::getPropagations(std::vector<TNode>& propagations) { - std::vector<SatLiteral> propagated_literals; - if (d_satSolver->getPropagations(propagated_literals)) { - for (unsigned i = 0; i < propagated_literals.size(); ++i) { - propagations.push_back(d_cnfStream->getNode(propagated_literals[i])); - } - return true; + if (!Options::current()->bitvector_eager_bitblast) { + d_cnfStream->ensureLiteral(atom); + SatLiteral lit = d_cnfStream->getLiteral(atom); + d_satSolver->addMarkerLiteral(lit); } - return false; } -void Bitblaster::explainPropagation(TNode atom, std::vector<Node>& explanation) { +void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) { std::vector<SatLiteral> literal_explanation; - d_satSolver->explainPropagation(d_cnfStream->getLiteral(atom), literal_explanation); + d_satSolver->explain(d_cnfStream->getLiteral(atom), literal_explanation); for (unsigned i = 0; i < literal_explanation.size(); ++i) { explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); } } -/** - * Called from preregistration bitblasts the node - * - * @param node - * - * @return - */ -void Bitblaster::bitblast(TNode node) { - TimerStat::CodeTimer codeTimer(d_statistics.d_bitblastTimer); - - /// strip the not - if (node.getKind() == kind::NOT) { - node = node[0]; - } - - if (node.getKind() == kind::EQUAL || - node.getKind() == kind::BITVECTOR_ULT || - node.getKind() == kind::BITVECTOR_ULE || - node.getKind() == kind::BITVECTOR_SLT || - node.getKind() == kind::BITVECTOR_SLE) - { - bbAtom(node); - } - else if (node.getKind() == kind::BITVECTOR_UGT || - node.getKind() == kind::BITVECTOR_UGE || - node.getKind() == kind::BITVECTOR_SGT || - node.getKind() == kind::BITVECTOR_SGE ) - { - Unhandled(node.getKind()); - } - else - { - Bits bits; - bbTerm(node, bits); - } -} /** * Asserts the clauses corresponding to the atom to the Sat Solver @@ -383,7 +349,22 @@ Bitblaster::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_bitblastTimer); } +bool Bitblaster::MinisatNotify::notify(prop::SatLiteral lit) { + return d_bv->storePropagation(d_cnf->getNode(lit), TheoryBV::SUB_BITBLASTER); +}; +void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) { + if (clause.size() > 1) { + NodeBuilder<> lemmab(kind::OR); + for (unsigned i = 0; i < clause.size(); ++ i) { + lemmab << d_cnf->getNode(clause[i]); + } + Node lemma = lemmab; + d_bv->d_out->lemma(lemma); + } else { + d_bv->d_out->lemma(d_cnf->getNode(clause[0])); + } +}; } /*bv namespace */ diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h index 2422da0b7..7016879a0 100644 --- a/src/theory/bv/bv_sat.h +++ b/src/theory/bv/bv_sat.h @@ -47,22 +47,37 @@ class CnfStream; class BVSatSolverInterface; } - namespace theory { + +class OutputChannel; + namespace bv { +typedef std::vector<Node> Bits; std::string toString (Bits& bits); +class TheoryBV; + /** * The Bitblaster that manages the mapping between Nodes * and their bitwise definition * */ - -typedef std::vector<Node> Bits; - class Bitblaster { + + /** This class gets callbacks from minisat on propagations */ + class MinisatNotify : public prop::BVSatSolverInterface::Notify { + prop::CnfStream* d_cnf; + TheoryBV *d_bv; + public: + MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv) + : d_cnf(cnf) + , d_bv(bv) + {} + bool notify(prop::SatLiteral lit); + void notify(prop::SatClause& clause); + }; typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction > TermDefMap; typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet; @@ -71,6 +86,7 @@ class Bitblaster { typedef Node (*AtomBBStrategy) (TNode, Bitblaster*); // sat solver used for bitblasting and associated CnfStream + theory::OutputChannel* d_bvOutput; prop::BVSatSolverInterface* d_satSolver; prop::CnfStream* d_cnfStream; @@ -88,9 +104,6 @@ class Bitblaster { bool hasBBTerm(TNode node); void getBBTerm(TNode node, Bits& bits); - - - /// function tables for the various bitblasting strategies indexed by node kind TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; @@ -102,7 +115,6 @@ class Bitblaster { // returns a node that might be easier to bitblast Node bbOptimize(TNode node); - void bbAtom(TNode node); void addAtom(TNode atom); // division is bitblasted in terms of constraints // so it needs to use private bitblaster interface @@ -111,17 +123,15 @@ class Bitblaster { public: void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division void bbTerm(TNode node, Bits& bits); + void bbAtom(TNode node); -public: - Bitblaster(context::Context* c); + Bitblaster(context::Context* c, bv::TheoryBV* bv); ~Bitblaster(); bool assertToSat(TNode node, bool propagate = true); bool solve(bool quick_solve = false); - void bitblast(TNode node); void getConflict(std::vector<TNode>& conflict); + void explain(TNode atom, std::vector<TNode>& explanation); - bool getPropagations(std::vector<TNode>& propagations); - void explainPropagation(TNode atom, std::vector<Node>& explanation); private: diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index b6f12793d..c9d58574e 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -40,15 +40,17 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& : Theory(THEORY_BV, c, u, out, valuation, logicInfo), d_context(c), d_assertions(c), - d_bitblaster(new Bitblaster(c) ), + d_bitblaster(new Bitblaster(c, this) ), d_alreadyPropagatedSet(c), d_statistics(), + d_sharedTermsSet(c), d_notify(*this), d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"), d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), - d_toBitBlast(c) + d_toBitBlast(c), + d_propagatedBy(c) { d_true = utils::mkTrue(); d_false = utils::mkFalse(); @@ -58,6 +60,11 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_equalityEngine.addTerm(d_false); d_equalityEngine.addTriggerEquality(d_true, d_false, d_false); + // add disequality between 0 and 1 bits + d_equalityEngine.addDisequality(utils::mkConst(BitVector((unsigned)1, (unsigned)0)), + utils::mkConst(BitVector((unsigned)1, (unsigned)1)), + d_true); + // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT); // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); @@ -113,12 +120,18 @@ TheoryBV::Statistics::~Statistics() { void TheoryBV::preRegisterTerm(TNode node) { BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; + + if (Options::current()->bitvector_eager_bitblast) { + // don't use the equality engine in the eager bit-blasting + return; + } + if (node.getKind() == kind::EQUAL || node.getKind() == kind::BITVECTOR_ULT || node.getKind() == kind::BITVECTOR_ULE || node.getKind() == kind::BITVECTOR_SLT || node.getKind() == kind::BITVECTOR_SLE) { - d_bitblaster->bitblast(node); + d_bitblaster->bbAtom(node); } if (d_useEqualityEngine) { @@ -140,56 +153,56 @@ void TheoryBV::preRegisterTerm(TNode node) { void TheoryBV::check(Effort e) { - BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; - BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl; + BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; + + if (Options::current()->bitvector_eager_bitblast) { + while (!done()) { + Assertion assertion = get(); + TNode fact = assertion.assertion; + if (fact.getKind() == kind::NOT) { + if (fact[0].getKind() != kind::BITVECTOR_BITOF) { + d_bitblaster->bbAtom(fact[0]); + } + } else { + if (fact.getKind() != kind::BITVECTOR_BITOF) { + d_bitblaster->bbAtom(fact); + } + } + } + return; + } + while (!done() && !d_conflict) { Assertion assertion = get(); TNode fact = assertion.assertion; BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; - // If the assertion doesn't have a literal, it's a shared equality - bool shared = !assertion.isPreregistered; - Assert(!d_useEqualityEngine || !shared || - ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) || - (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL && - d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1])))); - - // Notify the Equality Engine - switch (fact.getKind()) { - case kind::EQUAL: - if (d_useEqualityEngine) { - d_equalityEngine.addEquality(fact[0], fact[1], fact); - } - if (shared && !d_bitblaster->hasBBAtom(fact)) { - d_bitblaster->bitblast(fact); - } - break; - case kind::NOT: - if (fact[0].getKind() == kind::EQUAL) { - // Assert the dis-equality - if (d_useEqualityEngine) { - d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact); - } - if (shared && !d_bitblaster->hasBBAtom(fact[0])) { - d_bitblaster->bitblast(fact[0]); - } + // Notify the equality engine + if (d_useEqualityEngine && !d_conflict && !propagatedBy(fact, SUB_EQUALITY) ) { + bool negated = fact.getKind() == kind::NOT; + TNode predicate = negated ? fact[0] : fact; + if (predicate.getKind() == kind::EQUAL) { + if (negated) { + // dis-equality + d_equalityEngine.addDisequality(predicate[0], predicate[1], fact); } else { - if (d_useEqualityEngine) { - d_equalityEngine.addPredicate(fact[0], false, fact); - } - break; + // equality + d_equalityEngine.addEquality(predicate[0], predicate[1], fact); } - break; - default: - if (d_useEqualityEngine) { - d_equalityEngine.addPredicate(fact, true, fact); + } else { + // Adding predicate if the congruence over it is turned on + if (d_equalityEngine.isFunctionKind(predicate.getKind())) { + d_equalityEngine.addPredicate(predicate, !negated, fact); } - break; + } } - // make sure we do not assert things we propagated - if (!d_conflict && d_alreadyPropagatedSet.count(fact) == 0) { + // Bit-blaster + if (!d_conflict && !propagatedBy(fact, SUB_BITBLASTER)) { + // Some atoms have not been bit-blasted yet + d_bitblaster->bbAtom(fact); + // Assert to sat bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation); if (!ok) { std::vector<TNode> conflictAtoms; @@ -204,17 +217,15 @@ void TheoryBV::check(Effort e) // If in conflict, output the conflict if (d_conflict) { - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode << std::endl; + BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode; d_out->conflict(d_conflictNode); return; } - if (e == EFFORT_FULL) { - + if (e == EFFORT_FULL || Options::current()->bitvector_eager_fullcheck) { Assert(done() && !d_conflict); BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; - // in standard effort we only do boolean constraint propagation - bool ok = d_bitblaster->solve(false); + bool ok = d_bitblaster->solve(); if (!ok) { std::vector<TNode> conflictAtoms; d_bitblaster->getConflict(conflictAtoms); @@ -225,7 +236,6 @@ void TheoryBV::check(Effort e) return; } } - } @@ -253,77 +263,55 @@ void TheoryBV::propagate(Effort e) { return; } - // get new propagations from the equality engine - for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { + // go through stored propagations + for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); + d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) + { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): propagating from equality engine: " << literal << std::endl; - bool satValue; Node normalized = Rewriter::rewrite(literal); - if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { - d_out->propagate(literal); - } else { - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl; - Node negatedLiteral; - std::vector<TNode> assumptions; - if (normalized != d_false) { - negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); - assumptions.push_back(negatedLiteral); - } - explain(literal, assumptions); - d_conflictNode = mkAnd(assumptions); - d_conflict = true; - return; - } - } - // get new propagations from the sat solver - std::vector<TNode> propagations; - d_bitblaster->getPropagations(propagations); - - // propagate the facts on the propagation queue - for (unsigned i = 0; i < propagations.size(); ++ i) { - TNode node = propagations[i]; - BVDebug("bitvector") << "TheoryBV::propagate " << node <<" \n"; - if (!d_valuation.isSatLiteral(node)) { - // TODO: maybe propagate shared terms too? - continue; - } - if (d_valuation.getSatValue(node) == Node::null()) { - vector<Node> explanation; - d_bitblaster->explainPropagation(node, explanation); - if (explanation.size() == 0) { - d_out->lemma(node); + TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; + // check if it's a shared equality in the current context + if (atom.getKind() != kind::EQUAL || d_valuation.isSatLiteral(normalized) || + (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() && + d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end())) { + + bool satValue; + if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { + // check if we already propagated the negation + Node neg_literal = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal); + if (d_alreadyPropagatedSet.find(neg_literal) != d_alreadyPropagatedSet.end()) { + Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict " << literal << " and its negation both propagated \n"; + // we are in conflict + std::vector<TNode> assumptions; + explain(literal, assumptions); + explain(neg_literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + return; + } + + BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): " << literal << std::endl; + d_out->propagate(literal); + d_alreadyPropagatedSet.insert(literal); } else { - NodeBuilder<> nb(kind::OR); - nb << node; - for (unsigned i = 0; i < explanation.size(); ++ i) { - nb << explanation[i].notNode(); + Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl; + + Node negatedLiteral; + std::vector<TNode> assumptions; + if (normalized != d_false) { + negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); + assumptions.push_back(negatedLiteral); } - Node lemma = nb; - d_out->lemma(lemma); + explain(literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + return; } - d_alreadyPropagatedSet.insert(node); } } - } -// Node TheoryBV::explain(TNode n) { -// BVDebug("bitvector") << "TheoryBV::explain node " << n <<"\n"; -// std::vector<Node> explanation; -// d_bitblaster->explainPropagation(n, explanation); -// Node exp; - -// if (explanation.size() == 0) { -// return utils::mkTrue(); -// } - -// exp = utils::mkAnd(explanation); - -// BVDebug("bitvector") << "TheoryBV::explain with " << exp <<"\n"; -// return exp; -// } - Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { switch(in.getKind()) { case kind::EQUAL: @@ -351,42 +339,44 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu } -bool TheoryBV::propagate(TNode literal) +bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) { - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ")" << std::endl; + Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ")" << std::endl; // If already in conflict, no more propagation if (d_conflict) { - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << "): already in conflict" << std::endl; + Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << "): already in conflict" << std::endl; return false; } + // If propagated already, just skip + PropagatedMap::const_iterator find = d_propagatedBy.find(literal); + if (find != d_propagatedBy.end()) { + //unsigned theories = (*find).second | (unsigned) subtheory; + //d_propagatedBy[literal] = theories; + return true; + } else { + d_propagatedBy[literal] = subtheory; + } + // See if the literal has been asserted already - Node normalized = Rewriter::rewrite(literal); bool satValue = false; - bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue); - + bool hasSatValue = d_valuation.hasSatValue(literal, satValue); // If asserted, we might be in conflict - if (isAsserted) { - if (!satValue) { - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; + + if (hasSatValue && !satValue) { + Debug("bitvector-prop") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ") => conflict" << std::endl; std::vector<TNode> assumptions; - Node negatedLiteral; - if (normalized != d_false) { - negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); - assumptions.push_back(negatedLiteral); - } + Node negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode(); + assumptions.push_back(negatedLiteral); explain(literal, assumptions); d_conflictNode = mkAnd(assumptions); d_conflict = true; return false; - } - // Propagate even if already known in SAT - could be a new equation between shared terms - // (terms that weren't shared when the literal was asserted!) } // Nothing, just enqueue it for propagation and mark it as asserted already - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ") => enqueuing for propagation" << std::endl; + Debug("bitvector-prop") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ") => enqueuing for propagation" << std::endl; d_literalsToPropagate.push_back(literal); return true; @@ -394,46 +384,60 @@ bool TheoryBV::propagate(TNode literal) void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) { - TNode lhs, rhs; - switch (literal.getKind()) { - case kind::EQUAL: - lhs = literal[0]; - rhs = literal[1]; - break; - case kind::NOT: - if (literal[0].getKind() == kind::EQUAL) { - // Disequalities - d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions); - return; - } else { - // Predicates + + if (propagatedBy(literal, SUB_EQUALITY)) { + TNode lhs, rhs; + switch (literal.getKind()) { + case kind::EQUAL: lhs = literal[0]; + rhs = literal[1]; + break; + case kind::NOT: + if (literal[0].getKind() == kind::EQUAL) { + // Disequalities + d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions); + return; + } else { + // Predicates + lhs = literal[0]; + rhs = d_false; + break; + } + case kind::CONST_BOOLEAN: + // we get to explain true = false, since we set false to be the trigger of this + lhs = d_true; rhs = d_false; break; - } - case kind::CONST_BOOLEAN: - // we get to explain true = false, since we set false to be the trigger of this - lhs = d_true; - rhs = d_false; - break; - default: - Unreachable(); + default: + Unreachable(); + } + d_equalityEngine.explainEquality(lhs, rhs, assumptions); + } else { + Assert(propagatedBy(literal, SUB_BITBLASTER)); + d_bitblaster->explain(literal, assumptions); } - d_equalityEngine.explainEquality(lhs, rhs, assumptions); } Node TheoryBV::explain(TNode node) { BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl; std::vector<TNode> assumptions; + + // Ask for the explanation explain(node, assumptions); + // this means that it is something true at level 0 + if (assumptions.size() == 0) { + return utils::mkTrue(); + } + // return the explanation return mkAnd(assumptions); } void TheoryBV::addSharedTerm(TNode t) { Debug("bitvector::sharing") << spaces(getSatContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; - if (d_useEqualityEngine) { + d_sharedTermsSet.insert(t); + if (!Options::current()->bitvector_eager_bitblast && d_useEqualityEngine) { d_equalityEngine.addTriggerTerm(t); } } @@ -441,6 +445,10 @@ void TheoryBV::addSharedTerm(TNode t) { EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) { + if (Options::current()->bitvector_eager_bitblast) { + return EQUALITY_UNKNOWN; + } + if (d_useEqualityEngine) { if (d_equalityEngine.areEqual(a, b)) { // The terms are implied to be equal diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index c4953213d..0ced179ec 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -66,7 +66,7 @@ private: /** Context dependent set of atoms we already propagated */ context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet; - + context::CDHashSet<TNode, TNodeHashFunction> d_sharedTermsSet; public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); @@ -74,8 +74,6 @@ public: void preRegisterTerm(TNode n); - //void registerTerm(TNode n) { } - void check(Effort e); Node explain(TNode n); @@ -84,7 +82,6 @@ public: std::string identify() const { return std::string("TheoryBV"); } - //Node preprocessTerm(TNode term); PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); private: @@ -110,14 +107,14 @@ private: bool notify(TNode propagation) { Debug("bitvector") << spaces(d_bv.getSatContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl; // Just forward to bv - return d_bv.propagate(propagation); + return d_bv.storePropagation(propagation, SUB_EQUALITY); } void notify(TNode t1, TNode t2) { Debug("arrays") << spaces(d_bv.getSatContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; // Propagate equality between shared terms Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); - d_bv.propagate(t1.eqNode(t2)); + d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY); } }; @@ -141,16 +138,38 @@ private: context::CDQueue<Node> d_toBitBlast; + enum SubTheory { + SUB_EQUALITY = 1, + SUB_BITBLASTER = 2 + }; + + /** + * Keeps a map from nodes to the subtheory that propagated it so that we can explain it + * properly. + */ + typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap; + PropagatedMap d_propagatedBy; + + bool propagatedBy(TNode literal, SubTheory subtheory) const { + PropagatedMap::const_iterator find = d_propagatedBy.find(literal); + if (find == d_propagatedBy.end()) return false; + else return (*find).second == subtheory; + } + /** Should be called to propagate the literal. */ - bool propagate(TNode literal); + bool storePropagation(TNode literal, SubTheory subtheory); - /** Explain why this literal is true by adding assumptions */ + /** + * Explains why this literal (propagated by subtheory) is true by adding assumptions. + */ void explain(TNode literal, std::vector<TNode>& assumptions); void addSharedTerm(TNode t); EqualityStatus getEqualityStatus(TNode a, TNode b); + friend class Bitblaster; + public: void propagate(Effort e); diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 38547ad99..78835b75c 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -326,7 +326,10 @@ inline Node mkConjunction(const std::vector<TNode>& nodes) { ++ it; } - Assert(expandedNodes.size() > 0); + if (expandedNodes.size() == 0) { + return mkTrue(); + } + if (expandedNodes.size() == 1) { return *expandedNodes.begin(); } diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 1ed4525f4..75426cba4 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -103,6 +103,10 @@ void PreRegisterVisitor::start(TNode node) { } bool PreRegisterVisitor::done(TNode node) { +// <<<<<<< .working +// d_engine->markActive(d_theories[node]); +// ======= +// >>>>>>> .merge-right.r3396 return d_multipleTheories; } diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index cde65aa0f..1ed1f99ff 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -45,6 +45,7 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ void Theory::addSharedTermInternal(TNode n) { Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl; + Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl; d_sharedTerms.push_back(n); addSharedTerm(n); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 1122e09c6..a3aee985d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -59,6 +59,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_decisionRequests(context), d_decisionRequestsIndex(context, 0), d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), + d_inPreregister(false), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms) { @@ -84,15 +85,43 @@ TheoryEngine::~TheoryEngine() { } void TheoryEngine::preRegister(TNode preprocessed) { + if(Dump.isOn("missed-t-propagations")) { d_possiblePropagations.push_back(preprocessed); } - // Pre-register the terms in the atom - bool multipleTheories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed); - if (multipleTheories) { - // Collect the shared terms if there are multipe theories - NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed); + //<<<<<<< .working + d_preregisterQueue.push(preprocessed); + + if (!d_inPreregister) { + // We're in pre-register + d_inPreregister = true; + + // Process the pre-registration queue + while (!d_preregisterQueue.empty()) { + // Get the next atom to pre-register + preprocessed = d_preregisterQueue.front(); + d_preregisterQueue.pop(); + + // Pre-register the terms in the atom + bool multipleTheories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed); + if (multipleTheories) { + // Collect the shared terms if there are multipe theories + NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed); + // Mark the multiple theories flag + //d_sharedTermsExist = true; + } + } + // Leaving pre-register + d_inPreregister = false; } +// ======= + // Pre-register the terms in the atom + // bool multipleTheories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed); + // if (multipleTheories) { + // // Collect the shared terms if there are multipe theories + // NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed); + // //>>>>>>> .merge-right.r3396 + // } } /** @@ -618,7 +647,7 @@ Node TheoryEngine::preprocess(TNode assertion) { void TheoryEngine::assertFact(TNode node) { Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; - Trace("theory::assertFact") << "TheoryEngine::assertFact(" << node << ")" << std::endl; + // Trace("theory::assertions") << "TheoryEngine::assertFact(" << node << "): d_sharedTermsExist = " << (d_sharedTermsExist ? "true" : "false") << std::endl; d_propEngine->checkTime(); @@ -629,6 +658,8 @@ void TheoryEngine::assertFact(TNode node) if (d_logicInfo.isSharingEnabled()) { + Trace("theory::assertions") << "TheoryEngine::assertFact(" << node << "): hasShared terms = " << (d_sharedTerms.hasSharedTerms(atom) ? "true" : "false") << std::endl; + // If any shared terms, notify the theories if (d_sharedTerms.hasSharedTerms(atom)) { SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2b4fd24d1..0a0778ebc 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -499,6 +499,16 @@ private: */ Node ppTheoryRewrite(TNode term); + /** + * Queue of nodes for pre-registration. + */ + std::queue<TNode> d_preregisterQueue; + + /** + * Boolean flag denoting we are in pre-registration. + */ + bool d_inPreregister; + public: /** diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 4eabf63de..dccd5ba56 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -613,6 +613,13 @@ public: } /** + * Returns true if this kind is used for congruence closure. + */ + bool isFunctionKind(Kind fun) { + return d_congruenceKinds.tst(fun); + } + + /** * Adds a function application term to the database. */ diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 5eb4f0dc7..cae62570c 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -79,7 +79,6 @@ Node Valuation::getSatValue(TNode n) const { } bool Valuation::hasSatValue(TNode n, bool& value) const { - // Node normalized = Rewriter::rewrite(n); if (d_engine->getPropEngine()->isSatLiteral(n)) { return d_engine->getPropEngine()->hasValue(n, value); } else { diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h index 0dec26717..687272b56 100644 --- a/src/util/node_visitor.h +++ b/src/util/node_visitor.h @@ -31,6 +31,23 @@ namespace CVC4 { template<typename Visitor> class NodeVisitor { + /** For re-entry checking */ + static bool d_inRun; + + class GuardReentry { + bool& d_guard; + public: + GuardReentry(bool& guard) + : d_guard(guard) { + Assert(!d_guard); + d_guard = true; + } + ~GuardReentry() { + Assert(d_guard); + d_guard = false; + } + }; + public: /** @@ -52,6 +69,8 @@ public: */ static typename Visitor::return_type run(Visitor& visitor, TNode node) { + GuardReentry guard(d_inRun); + // Notify of a start visitor.start(node); @@ -91,5 +110,8 @@ public: }; +template <typename Visitor> +bool NodeVisitor<Visitor>::d_inRun = false; + } diff --git a/src/util/options.cpp b/src/util/options.cpp index e87c240a8..d72734f40 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -119,7 +119,11 @@ Options::Options() : threadArgv(), thread_id(-1), separateOutput(false), - sharingFilterByLength(-1) + sharingFilterByLength(-1), + bitvector_eager_bitblast(false), + bitvector_share_lemmas(false), + bitvector_eager_fullcheck(false), + sat_refine_conflicts(false) { } @@ -187,10 +191,14 @@ Additional CVC4 options:\n\ --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al., CADE 2011) [on by default only for QF_UF]\n\ --disable-symmetry-breaker turns off UF symmetry breaker\n\ --disable-dio-solver turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\ - --disable-arith-rewrite-equalities turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n \ + --disable-arith-rewrite-equalities turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n\ --threads=N sets the number of solver threads\n\ --threadN=string configures thread N (0..#threads-1)\n\ --filter-lemma-length=N don't share lemmas strictly longer than N\n\ + --bitblast-eager eagerly bitblast the bitvectors to the main SAT solver\n\ + --bitblast-share-lemmas share lemmas from the bitblsting solver with the main solver\n\ + --bitblast-eager-fullcheck check the bitblasting eagerly\n\ + --refine-conflicts refine theory conflict clauses\n\ "; @@ -381,7 +389,11 @@ enum OptionValue { TIME_LIMIT, TIME_LIMIT_PER, RESOURCE_LIMIT, - RESOURCE_LIMIT_PER + RESOURCE_LIMIT_PER, + BITVECTOR_EAGER_BITBLAST, + BITVECTOR_SHARE_LEMMAS, + BITVECTOR_EAGER_FULLCHECK, + SAT_REFINE_CONFLICTS };/* enum OptionValue */ /** @@ -473,6 +485,10 @@ static struct option cmdlineOptions[] = { { "tlimit-per" , required_argument, NULL, TIME_LIMIT_PER }, { "rlimit" , required_argument, NULL, RESOURCE_LIMIT }, { "rlimit-per" , required_argument, NULL, RESOURCE_LIMIT_PER }, + { "bitblast-eager", no_argument, NULL, BITVECTOR_EAGER_BITBLAST }, + { "bitblast-share-lemmas", no_argument, NULL, BITVECTOR_SHARE_LEMMAS }, + { "bitblast-eager-fullcheck", no_argument, NULL, BITVECTOR_EAGER_FULLCHECK }, + { "refine-conflicts", no_argument, NULL, SAT_REFINE_CONFLICTS }, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -894,7 +910,26 @@ throw(OptionException) { perCallResourceLimit = (unsigned long) i; break; } - + case BITVECTOR_EAGER_BITBLAST: + { + bitvector_eager_bitblast = true; + break; + } + case BITVECTOR_EAGER_FULLCHECK: + { + bitvector_eager_fullcheck = true; + break; + } + case BITVECTOR_SHARE_LEMMAS: + { + bitvector_share_lemmas = true; + break; + } + case SAT_REFINE_CONFLICTS: + { + sat_refine_conflicts = true; + break; + } case RANDOM_SEED: satRandomSeed = atof(optarg); break; diff --git a/src/util/options.h b/src/util/options.h index 6205c7543..eac09fabf 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -283,6 +283,18 @@ struct CVC4_PUBLIC Options { /** Filter depending on length of lemma */ int sharingFilterByLength; + /** Bitblast eagerly to the main sat solver */ + bool bitvector_eager_bitblast; + + /** Fullcheck at each check */ + bool bitvector_eager_fullcheck; + + /** Bitblast eagerly to the main sat solver */ + bool bitvector_share_lemmas; + + /** Refine conflicts by doing another full check after a conflict */ + bool sat_refine_conflicts; + Options(); /** diff --git a/test/regress/regress0/aufbv/fuzz00.smt b/test/regress/regress0/aufbv/fuzz00.smt new file mode 100644 index 000000000..36322112e --- /dev/null +++ b/test/regress/regress0/aufbv/fuzz00.smt @@ -0,0 +1,147 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:status unknown +:extrafuns ((v0 BitVec[2])) +:extrafuns ((v1 BitVec[11])) +:extrafuns ((a2 Array[5:15])) +:formula +(let (?e3 bv270[9]) +(let (?e4 bv10435[15]) +(let (?e5 (ite (bvugt ?e4 ?e4) bv1[1] bv0[1])) +(let (?e6 (bvsub (sign_extend[13] v0) ?e4)) +(let (?e7 (ite (= bv1[1] (extract[0:0] v1)) ?e4 (sign_extend[6] ?e3))) +(let (?e8 (store a2 (extract[8:4] ?e3) ?e4)) +(let (?e9 (store ?e8 (extract[7:3] ?e3) ?e6)) +(let (?e10 (select ?e8 (extract[6:2] ?e3))) +(let (?e11 (select ?e9 (extract[9:5] ?e10))) +(let (?e12 (select ?e8 (extract[6:2] v1))) +(let (?e13 (store ?e8 (extract[4:0] ?e7) (zero_extend[13] v0))) +(let (?e14 (select ?e8 (extract[4:0] ?e10))) +(let (?e15 (store a2 (extract[6:2] ?e3) ?e6)) +(let (?e16 (select ?e13 (zero_extend[4] ?e5))) +(let (?e17 (ite (= ?e4 ?e16) bv1[1] bv0[1])) +(let (?e18 (bvnor (zero_extend[6] ?e3) ?e14)) +(let (?e19 (ite (bvsgt ?e14 ?e16) bv1[1] bv0[1])) +(let (?e20 (bvashr ?e7 (zero_extend[13] v0))) +(let (?e21 (extract[12:1] ?e11)) +(let (?e22 (ite (bvuge ?e10 (sign_extend[14] ?e19)) bv1[1] bv0[1])) +(let (?e23 (bvmul (sign_extend[1] ?e5) v0)) +(let (?e24 (zero_extend[1] ?e12)) +(let (?e25 (ite (= ?e6 ?e11) bv1[1] bv0[1])) +(let (?e26 (ite (bvslt v1 (sign_extend[10] ?e5)) bv1[1] bv0[1])) +(flet ($e27 (= ?e7 (zero_extend[14] ?e17))) +(flet ($e28 (= ?e24 (zero_extend[15] ?e26))) +(flet ($e29 (= ?e19 ?e5)) +(flet ($e30 (= (sign_extend[15] ?e19) ?e24)) +(flet ($e31 (= ?e3 (zero_extend[7] ?e23))) +(flet ($e32 (= ?e11 (zero_extend[14] ?e19))) +(flet ($e33 (= ?e12 (sign_extend[4] v1))) +(flet ($e34 (= (zero_extend[14] ?e25) ?e14)) +(flet ($e35 (= ?e12 (sign_extend[14] ?e19))) +(flet ($e36 (= (zero_extend[14] ?e25) ?e12)) +(flet ($e37 (= (zero_extend[14] ?e5) ?e18)) +(flet ($e38 (= ?e16 (sign_extend[14] ?e22))) +(flet ($e39 (= ?e24 (sign_extend[4] ?e21))) +(flet ($e40 (= (zero_extend[8] ?e22) ?e3)) +(flet ($e41 (= ?e11 ?e10)) +(flet ($e42 (= (sign_extend[14] ?e26) ?e18)) +(flet ($e43 (= ?e18 ?e11)) +(flet ($e44 (= (zero_extend[10] ?e19) v1)) +(flet ($e45 (= ?e25 ?e22)) +(flet ($e46 (= ?e11 (zero_extend[14] ?e25))) +(flet ($e47 (= (zero_extend[6] ?e3) ?e6)) +(flet ($e48 (= ?e7 (zero_extend[6] ?e3))) +(flet ($e49 (= ?e24 (zero_extend[15] ?e19))) +(flet ($e50 (= (sign_extend[14] ?e19) ?e11)) +(flet ($e51 (= (sign_extend[14] ?e22) ?e6)) +(flet ($e52 (= v1 (zero_extend[2] ?e3))) +(flet ($e53 (= v1 v1)) +(flet ($e54 (= (sign_extend[1] ?e5) ?e23)) +(flet ($e55 (= ?e6 (zero_extend[4] v1))) +(flet ($e56 (= (zero_extend[14] ?e22) ?e4)) +(flet ($e57 (= ?e24 (zero_extend[15] ?e22))) +(flet ($e58 (= (zero_extend[13] v0) ?e11)) +(flet ($e59 (= ?e3 (sign_extend[7] ?e23))) +(flet ($e60 (= (zero_extend[14] ?e26) ?e10)) +(flet ($e61 (= (sign_extend[7] ?e3) ?e24)) +(flet ($e62 (= ?e23 (sign_extend[1] ?e17))) +(flet ($e63 (= (sign_extend[1] ?e10) ?e24)) +(flet ($e64 (= ?e3 (zero_extend[7] v0))) +(flet ($e65 (= (zero_extend[1] ?e11) ?e24)) +(flet ($e66 (= (sign_extend[14] ?e22) ?e14)) +(flet ($e67 (= (zero_extend[13] ?e23) ?e10)) +(flet ($e68 (= (zero_extend[6] ?e3) ?e6)) +(flet ($e69 (= ?e22 ?e25)) +(flet ($e70 (= ?e26 ?e22)) +(flet ($e71 (= ?e4 ?e7)) +(flet ($e72 (= ?e7 (zero_extend[14] ?e26))) +(flet ($e73 (= ?e14 (sign_extend[4] v1))) +(flet ($e74 (= ?e4 ?e10)) +(flet ($e75 (= ?e17 ?e5)) +(flet ($e76 (= ?e6 (sign_extend[14] ?e5))) +(flet ($e77 (= (zero_extend[14] ?e17) ?e16)) +(flet ($e78 (= ?e11 (sign_extend[14] ?e26))) +(flet ($e79 (= ?e12 (sign_extend[13] v0))) +(flet ($e80 (= ?e17 ?e5)) +(flet ($e81 (= (sign_extend[13] v0) ?e20)) +(flet ($e82 (implies $e64 $e68)) +(flet ($e83 (iff $e72 $e77)) +(flet ($e84 (and $e51 $e34)) +(flet ($e85 (implies $e76 $e80)) +(flet ($e86 (or $e59 $e58)) +(flet ($e87 (iff $e49 $e52)) +(flet ($e88 (xor $e55 $e60)) +(flet ($e89 (not $e50)) +(flet ($e90 (and $e41 $e47)) +(flet ($e91 (if_then_else $e39 $e46 $e78)) +(flet ($e92 (or $e56 $e44)) +(flet ($e93 (not $e82)) +(flet ($e94 (implies $e42 $e71)) +(flet ($e95 (if_then_else $e93 $e63 $e36)) +(flet ($e96 (if_then_else $e75 $e83 $e74)) +(flet ($e97 (iff $e30 $e29)) +(flet ($e98 (implies $e40 $e84)) +(flet ($e99 (if_then_else $e45 $e48 $e70)) +(flet ($e100 (xor $e95 $e33)) +(flet ($e101 (iff $e99 $e96)) +(flet ($e102 (xor $e81 $e98)) +(flet ($e103 (not $e62)) +(flet ($e104 (if_then_else $e90 $e31 $e90)) +(flet ($e105 (not $e61)) +(flet ($e106 (or $e37 $e102)) +(flet ($e107 (iff $e28 $e89)) +(flet ($e108 (not $e35)) +(flet ($e109 (if_then_else $e67 $e38 $e27)) +(flet ($e110 (implies $e108 $e57)) +(flet ($e111 (and $e79 $e94)) +(flet ($e112 (not $e101)) +(flet ($e113 (iff $e66 $e66)) +(flet ($e114 (not $e86)) +(flet ($e115 (iff $e85 $e112)) +(flet ($e116 (and $e54 $e111)) +(flet ($e117 (iff $e53 $e106)) +(flet ($e118 (if_then_else $e105 $e107 $e104)) +(flet ($e119 (implies $e91 $e91)) +(flet ($e120 (if_then_else $e97 $e100 $e110)) +(flet ($e121 (or $e65 $e117)) +(flet ($e122 (iff $e87 $e116)) +(flet ($e123 (if_then_else $e109 $e92 $e32)) +(flet ($e124 (iff $e103 $e73)) +(flet ($e125 (iff $e88 $e114)) +(flet ($e126 (not $e43)) +(flet ($e127 (xor $e121 $e115)) +(flet ($e128 (or $e122 $e126)) +(flet ($e129 (xor $e69 $e118)) +(flet ($e130 (if_then_else $e123 $e127 $e125)) +(flet ($e131 (or $e120 $e124)) +(flet ($e132 (implies $e113 $e113)) +(flet ($e133 (not $e132)) +(flet ($e134 (implies $e128 $e119)) +(flet ($e135 (implies $e133 $e134)) +(flet ($e136 (and $e131 $e135)) +(flet ($e137 (xor $e129 $e136)) +(flet ($e138 (or $e130 $e130)) +(flet ($e139 (or $e138 $e137)) +$e139 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index 7b9ff2efc..5048ca680 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -14,7 +14,21 @@ MAKEFLAGS = -k # put it below in "TESTS +=" # Regression tests for SMT inputs -SMT_TESTS = +SMT_TESTS = \ + fuzz01.smt \ + fuzz02.smt \ + fuzz03.smt \ + fuzz04.smt \ + fuzz05.smt \ + fuzz06.smt \ + fuzz07.smt \ + fuzz08.smt \ + fuzz09.smt \ + fuzz10.smt \ + fuzz11.smt \ + fuzz12.smt \ + fuzz13.smt \ + fuzz14.smt # Regression tests for SMT2 inputs SMT2_TESTS = diff --git a/test/regress/regress0/bv/fuzz10.smt b/test/regress/regress0/bv/fuzz10.smt new file mode 100644 index 000000000..859c1ec5b --- /dev/null +++ b/test/regress/regress0/bv/fuzz10.smt @@ -0,0 +1,7 @@ +(benchmark fuzzsmt +:logic QF_BV +:extrafuns ((v0 BitVec[1])) +:status unsat:formula +(flet ($n1 (bvsgt v0 v0)) +$n1 +)) diff --git a/test/regress/regress0/bv/fuzz11.smt b/test/regress/regress0/bv/fuzz11.smt new file mode 100644 index 000000000..b789d40dc --- /dev/null +++ b/test/regress/regress0/bv/fuzz11.smt @@ -0,0 +1,15 @@ +(benchmark fuzzsmt +:logic QF_BV +:extrafuns ((v0 BitVec[11])) +:status unsat +:formula +(let (?n1 bv0[16]) +(let (?n2 (zero_extend[5] v0)) +(flet ($n3 (bvsge ?n1 ?n2)) +(let (?n4 bv1[1]) +(let (?n5 bv0[1]) +(let (?n6 (ite $n3 ?n4 ?n5)) +(let (?n7 (zero_extend[10] ?n6)) +(flet ($n8 (= v0 ?n7)) +$n8 +))))))))) diff --git a/test/regress/regress0/bv/fuzz12.smt b/test/regress/regress0/bv/fuzz12.smt new file mode 100644 index 000000000..017732c4d --- /dev/null +++ b/test/regress/regress0/bv/fuzz12.smt @@ -0,0 +1,57 @@ +(benchmark fuzzsmt +:logic QF_BV +:extrafuns ((v1 BitVec[9])) +:extrafuns ((v2 BitVec[10])) +:extrafuns ((v0 BitVec[3])) +:status sat +:formula +(let (?n1 bv1[3]) +(flet ($n2 (= ?n1 v0)) +(let (?n3 bv0[9]) +(let (?n4 bv1[1]) +(let (?n5 (sign_extend[2] v2)) +(let (?n6 (extract[9:9] ?n5)) +(flet ($n7 (= ?n4 ?n6)) +(let (?n8 (bvneg v1)) +(let (?n9 bv1[11]) +(let (?n10 (zero_extend[8] v0)) +(flet ($n11 (bvsgt ?n9 ?n10)) +(let (?n12 bv0[1]) +(let (?n13 (ite $n11 ?n4 ?n12)) +(let (?n14 (zero_extend[8] ?n13)) +(let (?n15 (ite $n7 ?n8 ?n14)) +(flet ($n16 (= ?n3 ?n15)) +(let (?n17 bv1[12]) +(let (?n18 (zero_extend[3] v1)) +(flet ($n19 (bvult ?n17 ?n18)) +(let (?n20 (ite $n19 ?n4 ?n12)) +(let (?n21 (zero_extend[1] v1)) +(let (?n22 (bvlshr v2 ?n21)) +(let (?n23 (zero_extend[2] ?n22)) +(let (?n24 bv0[12]) +(flet ($n25 (= ?n23 ?n24)) +(let (?n26 (ite $n25 ?n4 ?n12)) +(flet ($n27 (= ?n20 ?n26)) +(flet ($n28 (or $n16 $n27)) +(let (?n29 (sign_extend[9] v0)) +(flet ($n30 (= ?n24 ?n29)) +(let (?n31 bv0[10]) +(let (?n32 (rotate_left[3] ?n8)) +(let (?n33 (zero_extend[1] ?n32)) +(let (?n34 (bvmul ?n22 ?n33)) +(let (?n35 (bvcomp ?n31 ?n34)) +(flet ($n36 (= ?n4 ?n35)) +(let (?n37 bv1[9]) +(let (?n38 (bvadd v1 ?n37)) +(let (?n39 (zero_extend[6] v0)) +(flet ($n40 (bvsge ?n38 ?n39)) +(let (?n41 (ite $n40 ?n4 ?n12)) +(let (?n42 (bvnor ?n41 ?n41)) +(flet ($n43 (= ?n4 ?n42)) +(let (?n44 (ite $n43 ?n31 ?n22)) +(flet ($n45 (= ?n31 ?n44)) +(flet ($n46 (if_then_else $n30 $n36 $n45)) +(flet ($n47 (xor $n28 $n46)) +(flet ($n48 (implies $n2 $n47)) +$n48 +))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/bv/fuzz13.smt b/test/regress/regress0/bv/fuzz13.smt new file mode 100644 index 000000000..6d84c00cb --- /dev/null +++ b/test/regress/regress0/bv/fuzz13.smt @@ -0,0 +1,23 @@ +(benchmark fuzzsmt +:logic QF_BV +:extrafuns ((v1 BitVec[13])) +:status sat +:formula +(let (?n1 bv1[13]) +(flet ($n2 (bvult v1 ?n1)) +(let (?n3 bv1[1]) +(let (?n4 bv0[1]) +(let (?n5 (ite $n2 ?n3 ?n4)) +(let (?n6 (zero_extend[12] ?n5)) +(flet ($n7 (bvuge ?n6 v1)) +(let (?n8 (ite $n7 ?n3 ?n4)) +(let (?n9 (zero_extend[12] ?n8)) +(flet ($n10 (bvult ?n9 ?n1)) +(let (?n11 (ite $n10 ?n3 ?n4)) +(let (?n12 (sign_extend[5] ?n5)) +(let (?n13 bv0[6]) +(flet ($n14 (bvsgt ?n12 ?n13)) +(let (?n15 (ite $n14 ?n3 ?n4)) +(flet ($n16 (= ?n11 ?n15)) +$n16 +))))))))))))))))) diff --git a/test/regress/regress0/bv/fuzz14.smt b/test/regress/regress0/bv/fuzz14.smt new file mode 100644 index 000000000..51a7b7cad --- /dev/null +++ b/test/regress/regress0/bv/fuzz14.smt @@ -0,0 +1,43 @@ +(benchmark fuzzsmt +:logic QF_BV +:extrafuns ((v2 BitVec[13])) +:extrafuns ((v1 BitVec[2])) +:status sat +:formula +(let (?n1 bv1[1]) +(let (?n2 bv0[2]) +(flet ($n3 (bvsge ?n2 v1)) +(let (?n4 bv0[1]) +(let (?n5 (ite $n3 ?n1 ?n4)) +(flet ($n6 (= ?n1 ?n5)) +(let (?n7 bv0[13]) +(flet ($n8 (bvslt ?n7 v2)) +(let (?n9 (ite $n8 ?n1 ?n4)) +(let (?n10 (bvneg ?n9)) +(let (?n11 (ite $n6 ?n10 ?n9)) +(let (?n12 (zero_extend[12] ?n11)) +(flet ($n13 (= v2 ?n12)) +(flet ($n14 (= ?n1 ?n9)) +(flet ($n15 (and $n13 $n14)) +(flet ($n16 (not $n15)) +(let (?n17 (bvashr v2 v2)) +(let (?n18 (bvshl v2 ?n17)) +(flet ($n19 (= ?n7 ?n18)) +(let (?n20 bv1[13]) +(let (?n21 (bvsub ?n20 v2)) +(flet ($n22 (= ?n17 ?n21)) +(let (?n23 bv1[10]) +(let (?n24 (sign_extend[9] ?n11)) +(flet ($n25 (= ?n23 ?n24)) +(flet ($n26 (if_then_else $n19 $n22 $n25)) +(flet ($n27 (bvult ?n10 ?n1)) +(let (?n28 (ite $n27 ?n1 ?n4)) +(flet ($n29 (= ?n11 ?n28)) +(let (?n30 bv0[4]) +(let (?n31 (sign_extend[3] ?n11)) +(flet ($n32 (= ?n30 ?n31)) +(flet ($n33 (implies $n29 $n32)) +(flet ($n34 (if_then_else $n26 $n33 $n26)) +(flet ($n35 (implies $n16 $n34)) +$n35 +)))))))))))))))))))))))))))))))))))) diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index 1a91364a4..bbc7a8f72 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -53,23 +53,23 @@ public: void setUp() { - d_ctxt = new Context(); - d_nm = new NodeManager(d_ctxt, NULL); - d_scope = new NodeManagerScope(d_nm); + // d_ctxt = new Context(); + // d_nm = new NodeManager(d_ctxt, NULL); + // d_scope = new NodeManagerScope(d_nm); } void tearDown() { - delete d_scope; - delete d_nm; - delete d_ctxt; + // delete d_scope; + // delete d_nm; + // delete d_ctxt; } void testBitblasterCore() { // ClauseManager tests - Context* ctx = new Context(); - Bitblaster* bb = new Bitblaster(ctx); + // Context* ctx = new Context(); + // Bitblaster* bb = new Bitblaster(ctx); // NodeManager* nm = NodeManager::currentNM(); // TODO: update this @@ -110,7 +110,7 @@ public: // res = bb->solve(); // TS_ASSERT(res == false); - delete bb; + //delete bb; } |