diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-09-24 15:03:28 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-09-24 15:03:28 +0000 |
commit | 353c6d5c3770365f0dffcbdf697199bed156cf50 (patch) | |
tree | e8a019cf24b3a4dd2b4eb458cbe066164b6eddee /src/theory/bv/theory_bv.h | |
parent | bb0fc300c810f68f1e901413272c6658e31d60f9 (diff) |
basic union find for bitvectors
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 28 |
1 files changed, 25 insertions, 3 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index ee331af02..912c453b4 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -23,19 +23,41 @@ #include "theory/theory.h" #include "context/context.h" +#include "context/cdlist.h" +#include "equality_engine.h" namespace CVC4 { namespace theory { namespace bv { class TheoryBV : public Theory { + public: + + class EqualityNotify { + TheoryBV& d_theoryBV; + public: + EqualityNotify(TheoryBV& theoryBV) + : d_theoryBV(theoryBV) {} + }; + +private: + + /** Equality reasoning engine */ + EqualityEngine<TheoryBV, EqualityNotify> d_eqEngine; + + /** The disequalities */ + context::CDList<TNode> d_disequalities; + +public: + TheoryBV(int id, context::Context* c, OutputChannel& out) : - Theory(id, c, out) { + Theory(id, c, out), d_eqEngine(*this, c), d_disequalities(c) { } - void preRegisterTerm(TNode n) { } + + void preRegisterTerm(TNode n); void registerTerm(TNode n) { } - void check(Effort e) {} + void check(Effort e); void propagate(Effort e) {} void explain(TNode n, Effort e) { } RewriteResponse postRewrite(TNode n, bool topLevel); |