3 files changed, 27 insertions, 59 deletions

diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index 807d90137..98678a9b4 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -134,7 +134,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool v
 }
 
 bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
-  BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+  BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
   if (value) {
     return d_bv->storePropagation(predicate, TheoryBV::SUB_EQUALITY);
   } else {
@@ -143,7 +143,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool
 }
 
 bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
-  Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl;
+  Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
   if (value) {
     return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY);
   } else {
@@ -152,7 +152,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNod
 }
 
 bool EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-  Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
+  Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
   if (Theory::theoryOf(t1) == THEORY_BOOL) {
     return d_bv->storePropagation(t1.iffNode(t2), TheoryBV::SUB_EQUALITY);
   }
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 251650bf2..30493737a 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -141,58 +141,9 @@ void TheoryBV::propagate(Effort e) {
   }
 
   // go through stored propagations
-  for (; d_literalsToPropagateIndex < d_literalsToPropagate.size();
-       d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1)
-  {
+  for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
     TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
-    Node normalized = Rewriter::rewrite(literal);
-
-    TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;  
-    bool isSharedLiteral = (atom.getKind() == kind::EQUAL &&
-                            (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() &&
-                             d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end()));
-
-    // Check if this is a SAT literal
-    if (d_valuation.isSatLiteral(normalized)) {
-      bool satValue = false;
-      if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
-        // check if we already propagated the negation
-        Node negLiteral = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal);
-        if (d_alreadyPropagatedSet.find(negLiteral) != d_alreadyPropagatedSet.end()) {
-          Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict " << literal << " and its negation both propagated \n"; 
-          // we are in conflict
-          std::vector<TNode> assumptions;
-          explain(literal, assumptions);
-          explain(negLiteral, assumptions);
-          setConflict(mkAnd(assumptions)); 
-          return;
-        }
-        // If it's not a shared literal and hasn't already been set to true, we propagate the normalized version
-        // shared literals are handled below
-        if (!isSharedLiteral && !satValue) {
-          BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << normalized << std::endl;
-          d_out->propagate(normalized);
-          d_alreadyPropagatedSet.insert(normalized); 
-          return;
-        }
-      } else {
-        // 
-        Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
-        Node negatedLiteral;
-        std::vector<TNode> assumptions;
-        negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
-        assumptions.push_back(negatedLiteral);
-        explain(literal, assumptions);
-        setConflict(mkAnd(assumptions));
-        return;
-      }
-    }
-    // Either it was not a SAT literal or it was but it is also shared - in that case we have to propagate the original literal (not the normalized one)
-    if (isSharedLiteral) {
-      BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << literal << std::endl;
-      d_out->propagate(literal);
-      d_alreadyPropagatedSet.insert(literal); 
-    }
+    d_out->propagate(literal);
   }
 }
 
@@ -269,16 +220,18 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
   // Ask the appropriate subtheory for the explanation 
   if (propagatedBy(literal, SUB_EQUALITY)) {
+    BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl;
     d_equalitySolver.explain(literal, assumptions); 
   } else {
     Assert(propagatedBy(literal, SUB_BITBLAST));
+    BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;    
     d_bitblastSolver.explain(literal, assumptions); 
   }
 }
 
 
 Node TheoryBV::explain(TNode node) {
-  BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl;
+  BVDebug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
   std::vector<TNode> assumptions;
 
   // Ask for the explanation
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 3736da639..c456ef73f 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -72,11 +72,26 @@ inline Node mkVar(unsigned size) {
 }
 
 inline Node mkAnd(std::vector<TNode>& children) {
-  if (children.size() > 1) {
-    return NodeManager::currentNM()->mkNode(kind::AND, children);
-  } else {
-    return children[0];
+  std::set<TNode> distinctChildren;
+  distinctChildren.insert(children.begin(), children.end());
+  
+  if (children.size() == 0) {
+    return mkTrue();
+  }
+  
+  if (children.size() == 1) {
+    return *children.begin();
   }
+  
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = distinctChildren.begin();
+  std::set<TNode>::const_iterator it_end = distinctChildren.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
+  }
+
+  return conjunction;
 }
 
 inline Node mkSortedNode(Kind kind, std::vector<Node>& children) {