This should also fix bug 325.
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
- <name>cvc4-sharing</name>
+ <name>cvc4-bvprop</name>
<comment></comment>
<projects>
</projects>
-#Thu Mar 25 16:47:04 EDT 2010
builderLoc=builderLocRelative
builderRelPath=./generated
eclipse.preferences.version=1
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),
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) {
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]));
}
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),
BVMinisatSatSolver(context::Context* mainSatContext);
~BVMinisatSatSolver() throw(AssertionException);
+ void setNotify(Notify* notify);
+
void addClause(SatClause& clause, bool removable);
SatVariable newVar(bool theoryAtom = false);
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);
#include "core/Solver.h"
#include <vector>
#include <iostream>
+
#include "util/output.h"
#include "util/utility.h"
+#include "util/options.h"
using namespace BVMinisat;
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));
// 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)
// 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):
//
, conflict_budget (-1)
, propagation_budget (-1)
, asynch_interrupt (false)
- , d_explanations(c)
+ , clause_added(false)
{}
bool Solver::addClause_(vec<Lit>& ps)
{
- if (decisionLevel() > 0) {
- cancelUntil(0);
- }
+ if (decisionLevel() > 0) {
+ cancelUntil(0);
+ }
if (!ok) return false;
ps[j++] = p = ps[i];
ps.shrink(i - j);
+ clause_added = true;
+
if (ps.size() == 0)
return ok = false;
else if (ps.size() == 1){
return true;
}
-
void Solver::attachClause(CRef cr) {
const Clause& c = ca[cr];
assert(c.size() > 1);
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);
- }
}
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])))
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)
}
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;
}
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;
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{
}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:
// 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]));
}
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:
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.
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; };
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()')
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); }
// 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; }
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));
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]);
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)
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++)
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;
{
CRef confl = CRef_Undef;
recheck = false;
+ theoryConflict = false;
ScopedBool scoped_bool(minisat_busy, true);
// 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
(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
}
return l_True;
}
+ } else if (check_type == CHECK_FINAL_FAKE) {
+ check_type = CHECK_WITH_THEORY;
}
if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()) {
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) {
lemmas.clear();
lemmas_removable.clear();
+ if (conflict != CRef_Undef) {
+ theoryConflict = true;
+ }
+
return conflict;
}
// 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
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.
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;
#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;
namespace theory {
namespace bv{
-
std::string toString(Bits& bits) {
ostringstream os;
for (int i = bits.size() - 1; i >= 0; --i) {
}
/////// 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),
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();
*
*/
void Bitblaster::bbAtom(TNode node) {
+ node = node.getKind() == kind::NOT? node[0] : node;
+
if (hasBBAtom(node)) {
return;
}
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);
+ }
}
/// 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
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 */
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;
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;
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];
// 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
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:
: 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();
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);
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) {
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;
// 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);
return;
}
}
-
}
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:
}
-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;
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);
}
}
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
/** 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);
void preRegisterTerm(TNode n);
- //void registerTerm(TNode n) { }
-
void check(Effort e);
Node explain(TNode n);
std::string identify() const { return std::string("TheoryBV"); }
- //Node preprocessTerm(TNode term);
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
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);
}
};
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);
++ it;
}
- Assert(expandedNodes.size() > 0);
+ if (expandedNodes.size() == 0) {
+ return mkTrue();
+ }
+
if (expandedNodes.size() == 1) {
return *expandedNodes.begin();
}
}
bool PreRegisterVisitor::done(TNode node) {
+// <<<<<<< .working
+// d_engine->markActive(d_theories[node]);
+// =======
+// >>>>>>> .merge-right.r3396
return d_multipleTheories;
}
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);
}
d_decisionRequests(context),
d_decisionRequestsIndex(context, 0),
d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
+ d_inPreregister(false),
d_preRegistrationVisitor(this, context),
d_sharedTermsVisitor(d_sharedTerms)
{
}
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
+ // }
}
/**
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();
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);
*/
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:
/**
d_congruenceKinds |= fun;
}
+ /**
+ * 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.
*/
}
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 {
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:
/**
*/
static typename Visitor::return_type run(Visitor& visitor, TNode node) {
+ GuardReentry guard(d_inRun);
+
// Notify of a start
visitor.start(node);
};
+template <typename Visitor>
+bool NodeVisitor<Visitor>::d_inRun = false;
+
}
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)
{
}
--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\
";
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 */
/**
{ "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! */
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;
/** 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();
/**
--- /dev/null
+(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
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
# 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 =
--- /dev/null
+(benchmark fuzzsmt
+:logic QF_BV
+:extrafuns ((v0 BitVec[1]))
+:status unsat:formula
+(flet ($n1 (bvsgt v0 v0))
+$n1
+))
--- /dev/null
+(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
+)))))))))
--- /dev/null
+(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
+)))))))))))))))))))))))))))))))))))))))))))))))))
--- /dev/null
+(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
+)))))))))))))))))
--- /dev/null
+(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
+))))))))))))))))))))))))))))))))))))
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
// res = bb->solve();
// TS_ASSERT(res == false);
- delete bb;
+ //delete bb;
}
projects / cvc5.git / commitdiff