diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-05-08 21:54:55 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-05-08 21:54:55 +0000 |
commit | 8a0c0562cb8d0e26ea019ff782b25c1997a49a0b (patch) | |
tree | 28239db9bcb26b03d893ad61dd1a7ea099391fbe /src/theory/bv/theory_bv.h | |
parent | 5082cb8349efbb287084293cd4bc6c3fa5a34f26 (diff) |
Merging in bvprop branch, with proper bit-vector propagation.
This should also fix bug 325.
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 35 |
1 files changed, 27 insertions, 8 deletions
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); |