Merging in bvprop branch, with proper bit-vector propagation.

This should also fix bug 325. 

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);