diff options
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 69 |
1 files changed, 65 insertions, 4 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index d147c8bb5..940eaef56 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -27,6 +27,8 @@ #include "context/cdhashset.h" #include "theory/bv/theory_bv_utils.h" #include "util/stats.h" +#include "theory/uf/equality_engine.h" +#include "context/cdqueue.h" namespace BVMinisat { class SimpSolver; @@ -40,6 +42,12 @@ namespace bv { /// forward declarations class Bitblaster; +static inline std::string spaces(int level) +{ + std::string indentStr(level, ' '); + return indentStr; +} + class TheoryBV : public Theory { @@ -54,11 +62,11 @@ private: /** Bitblaster */ Bitblaster* d_bitblaster; Node d_true; - + Node d_false; + /** Context dependent set of atoms we already propagated */ context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet; - bool hasBeenPropagated(TNode node); public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); @@ -70,8 +78,6 @@ public: void check(Effort e); - void propagate(Effort e); - Node explain(TNode n); Node getValue(TNode n); @@ -93,6 +99,61 @@ private: Statistics d_statistics; + // Added by Clark + // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module + class NotifyClass { + TheoryBV& d_bv; + public: + NotifyClass(TheoryBV& uf): d_bv(uf) {} + + bool notify(TNode propagation) { + Debug("bitvector") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl; + // Just forward to bv + return d_bv.propagate(propagation); + } + + void notify(TNode t1, TNode t2) { + Debug("arrays") << spaces(d_bv.getContext()->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)); + } + }; + + /** The notify class for d_equalityEngine */ + NotifyClass d_notify; + + /** Equaltity engine */ + uf::EqualityEngine<NotifyClass> d_equalityEngine; + + // Are we in conflict? + context::CDO<bool> d_conflict; + + /** The conflict node */ + Node d_conflictNode; + + /** Literals to propagate */ + context::CDList<Node> d_literalsToPropagate; + + /** Index of the next literal to propagate */ + context::CDO<unsigned> d_literalsToPropagateIndex; + + context::CDQueue<Node> d_toBitBlast; + + /** Should be called to propagate the literal. */ + bool propagate(TNode literal); + + /** Explain why this literal is true by adding assumptions */ + void explain(TNode literal, std::vector<TNode>& assumptions); + + void addSharedTerm(TNode t); + + EqualityStatus getEqualityStatus(TNode a, TNode b); + +public: + + void propagate(Effort e); + };/* class TheoryBV */ }/* CVC4::theory::bv namespace */ |