more bugfixes, some basic propagation, and testcases to cover them

5 files changed, 45 insertions, 11 deletions

diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h
index 6fa1b7d22..5d4212849 100644
--- a/src/theory/bv/equality_engine.h
+++ b/src/theory/bv/equality_engine.h
@@ -30,6 +30,7 @@
 #include "util/output.h"
 #include "util/stats.h"
 #include "theory/rewriter.h"
+#include "theory/bv/theory_bv_utils.h"
 
 namespace CVC4 {
 namespace theory {
@@ -447,7 +448,11 @@ bool EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addEquality(
   // Check for constants
   if (d_nodes[t1classId].getMetaKind() == kind::metakind::CONSTANT &&
       d_nodes[t2classId].getMetaKind() == kind::metakind::CONSTANT) {
-    d_notify.conflict(reason);
+    std::vector<TNode> reasons;
+    getExplanation(t1, d_nodes[t1classId], reasons);
+    getExplanation(t2, d_nodes[t2classId], reasons);
+    reasons.push_back(reason);
+    d_notify.conflict(utils::mkAnd(reasons));
     return false;
   }
 
@@ -665,12 +670,13 @@ std::string EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::edges
 
 template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences>
 void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
-  Assert(equalities.empty());
-  Assert(t1 != t2);
   Assert(getRepresentative(t1) == getRepresentative(t2));
 
   Debug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl;
 
+  // If the nodes are the same, we're done
+  if (t1 == t2) return;
+
   const_cast<EqualityEngine*>(this)->backtrack();
 
   // Queue for the BFS containing nodes
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 2df4c361c..381e90d47 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -6,7 +6,7 @@
 
 theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h"
 
-properties finite check  
+properties finite check propagate
 
 rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 2d989a563..51de8df28 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -139,10 +139,12 @@ bool TheoryBV::triggerEquality(size_t triggerId) {
   // If we have a negation asserted, we have a confict
   if (d_assertions.contains(equality.notNode())) {
 
-    vector<TNode> assertions;
-    d_eqEngine.getExplanation(equality[0], equality[1], assertions);
-    assertions.push_back(equality.notNode());
-    d_out->conflict(mkAnd(assertions));
+    std::vector<TNode> explanation;
+    d_eqEngine.getExplanation(equality[0], equality[1], explanation);
+    std::set<TNode> assumptions;
+    assumptions.insert(equality.notNode());
+    utils::getConjuncts(explanation, assumptions);
+    d_out->conflict(utils::mkConjunction(assumptions));
 
     return false;
   }
@@ -169,3 +171,16 @@ Node TheoryBV::getValue(TNode n, Valuation* valuation) {
     Unhandled(n.getKind());
   }
 }
+
+void TheoryBV::explain(TNode node) {
+  Debug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl;
+  if(node.getKind() == kind::EQUAL) {
+    std::vector<TNode> reasons;
+    d_eqEngine.getExplanation(node[0], node[1], reasons);
+    std::set<TNode> simpleReasons;
+    utils::getConjuncts(reasons, simpleReasons);
+    d_out->explanation(utils::mkConjunction(simpleReasons));
+    return;
+  }
+  Unreachable();
+}
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 474c4d0cd..f2c2fa332 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -45,7 +45,9 @@ public:
       return d_theoryBV.triggerEquality(triggerId);
     }
     void conflict(Node explanation) {
-      d_theoryBV.d_out->conflict(explanation);
+      std::set<TNode> assumptions;
+      utils::getConjuncts(explanation, assumptions);
+      d_theoryBV.d_out->conflict(utils::mkConjunction(assumptions));
     }
   };
 
@@ -119,7 +121,7 @@ public:
 
   void propagate(Effort e) { }
 
-  void explain(TNode n) { }
+  void explain(TNode n);
 
   Node getValue(TNode n, Valuation* valuation);
 
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index ad924f8a0..781b5cddb 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -50,7 +50,11 @@ inline Node mkFalse() {
 }
 
 inline Node mkAnd(std::vector<TNode>& children) {
-  return NodeManager::currentNM()->mkNode(kind::AND, children);
+  if (children.size() > 1) {
+    return NodeManager::currentNM()->mkNode(kind::AND, children);
+  } else {
+    return children[0];
+  }
 }
 
 inline Node mkAnd(std::vector<Node>& children) {
@@ -90,6 +94,13 @@ inline void getConjuncts(TNode node, std::set<TNode>& conjuncts) {
   }
 }
 
+inline void getConjuncts(std::vector<TNode>& nodes, std::set<TNode>& conjuncts) {
+  for (unsigned i = 0, i_end = nodes.size(); i < i_end; ++ i) {
+    getConjuncts(nodes[i], conjuncts);
+  }
+}
+
+
 inline Node mkConjunction(const std::set<TNode> nodes) {
   std::set<TNode> expandedNodes;