fixing bitvector bugs

* clauses shouldn't be erased when they could be a reason for outside propagation
* propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally

6 files changed, 75 insertions, 33 deletions

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index d512847d5..5bb906841 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -337,7 +337,7 @@ Bitblaster::Statistics::~Statistics() {
 }
 
 bool Bitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
-  return d_bv->storePropagation(d_cnf->getNode(lit), TheoryBV::SUB_BITBLAST);
+  return d_bv->storePropagation(d_cnf->getNode(lit), SUB_BITBLAST);
 };
 
 void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) {
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index a8813b7aa..f8c763e3f 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -30,6 +30,27 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
+enum SubTheory {
+  SUB_EQUALITY = 1,
+  SUB_BITBLAST = 2
+};
+
+inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) {
+  switch (subtheory) {
+  case SUB_BITBLAST:
+    out << "BITBLASTER";
+    break;
+  case SUB_EQUALITY:
+    out << "EQUALITY";
+    break;
+  default:
+    Unreachable();
+    break;
+  }
+  return out;
+}
+
+
 const bool d_useEqualityEngine = true;
 const bool d_useSatPropagation = true;
 
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index ff0fc2b1a..334a704e9 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -79,7 +79,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
   // propagation
   for (unsigned i = 0; i < assertions.size(); ++i) {
     TNode fact = assertions[i];
-    if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, TheoryBV::SUB_BITBLAST)) {
+    if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_BITBLAST)) {
       // Some atoms have not been bit-blasted yet
       d_bitblaster->bbAtom(fact);
       // Assert to sat
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index afb4a8b4a..cb08a1ad8 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -96,7 +96,7 @@ bool EqualitySolver::addAssertions(const std::vector<TNode>& assertions, Theory:
     TNode fact = assertions[i];
 
     // Notify the equality engine
-    if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, TheoryBV::TheoryBV::SUB_EQUALITY) ) {
+    if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_EQUALITY) ) {
       bool negated = fact.getKind() == kind::NOT;
       TNode predicate = negated ? fact[0] : fact;
       if (predicate.getKind() == kind::EQUAL) {
@@ -156,7 +156,7 @@ void EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
 }
 
 bool EqualitySolver::storePropagation(TNode literal) {
-  return d_bv->storePropagation(literal, TheoryBV::SUB_EQUALITY);
+  return d_bv->storePropagation(literal, SUB_EQUALITY);
 }
   
 void EqualitySolver::conflict(TNode a, TNode b) {
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 66f443d50..208ffba6c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -77,15 +77,25 @@ void TheoryBV::preRegisterTerm(TNode node) {
   d_equalitySolver.preRegister(node); 
 }
 
+void TheoryBV::sendConflict() {
+  Assert(d_conflict);
+  if (d_conflictNode.isNull()) {
+    return;
+  } else {
+    BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
+    d_out->conflict(d_conflictNode);
+    d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
+    d_conflictNode = Node::null();
+  }
+}
+
 void TheoryBV::check(Effort e)
 {
   BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
 
   // if we are already in conflict just return the conflict 
-  if (d_conflict) {
-    BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
-    d_out->conflict(d_conflictNode);
-    d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
+  if (inConflict()) {
+    sendConflict();
     return;
   }
   
@@ -98,20 +108,18 @@ void TheoryBV::check(Effort e)
     BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; 
   }
 
-  // sending assertions to the equality solver first
-  bool ok = d_equalitySolver.addAssertions(new_assertions, e);
+  if (!inConflict()) {
+    // sending assertions to the equality solver first
+    d_equalitySolver.addAssertions(new_assertions, e);
+  }
   
-  if (ok) {
+  if (!inConflict()) {
     // sending assertions to the bitblast solver
-    ok = d_bitblastSolver.addAssertions(new_assertions, e); 
+    d_bitblastSolver.addAssertions(new_assertions, e);
   }
   
-  if (!ok) {
-    // output conflict 
-    Assert (d_conflict);
-    BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
-    d_out->conflict(d_conflictNode);
-    d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
+  if (inConflict()) {
+    sendConflict();
   }
 }
 
@@ -136,14 +144,20 @@ Node TheoryBV::getValue(TNode n) {
 void TheoryBV::propagate(Effort e) {
   BVDebug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
 
-  if (d_conflict) {
+  if (inConflict()) {
     return;
   }
 
   // go through stored propagations
-  for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
+  bool ok = true;
+  for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
     TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
-    d_out->propagate(literal);
+    ok = d_out->propagate(literal);
+  }
+
+  if (!ok) {
+    BVDebug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl;
+    setConflict();
   }
 }
 
@@ -177,11 +191,11 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
 
 bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 {
-  Debug("bitvector") << indent() << "TheoryBV::storePropagation(" << literal  << ")" << std::endl;
+  Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
 
   // If already in conflict, no more propagation
   if (d_conflict) {
-    Debug("bitvector") << indent() << "TheoryBV::storePropagation(" << literal << "): already in conflict" << std::endl;
+    Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl;
     return false;
   }
 
@@ -190,6 +204,13 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
   if (find != d_propagatedBy.end()) {
     return true;
   } else {
+    bool polarity = literal.getKind() != kind::NOT;
+    Node negatedLiteral = polarity ? literal.notNode() : (Node) literal[0];
+    find = d_propagatedBy.find(negatedLiteral);
+    if (find != d_propagatedBy.end() && (*find).second != subtheory) {
+      // Safe to ignore this one, subtheory should produce a conflict
+      return true;
+    }
     d_propagatedBy[literal] = subtheory;
   }
 
@@ -199,7 +220,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 
   // If asserted, we might be in conflict
   if (hasSatValue && !satValue) {
-    Debug("bitvector-prop") << indent() << "TheoryBV::storePropagation(" << literal << ") => conflict" << std::endl;
+    Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ") => conflict" << std::endl;
     std::vector<TNode> assumptions;
     Node negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode();
     assumptions.push_back(negatedLiteral);
@@ -209,7 +230,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
   }
 
   // Nothing, just enqueue it for propagation and mark it as asserted already
-  Debug("bitvector-prop") << indent() << "TheoryBV::storePropagation(" << literal << ") => enqueuing for propagation" << std::endl;
+  Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ") => enqueuing for propagation" << std::endl;
   d_literalsToPropagate.push_back(literal);
 
   // No conflict
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index f79b7ab71..a2cf39049 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -91,11 +91,6 @@ private:
   /** Index of the next literal to propagate */
   context::CDO<unsigned> d_literalsToPropagateIndex;
 
-  enum SubTheory {
-    SUB_EQUALITY = 1,
-    SUB_BITBLAST = 2
-  };
-
   /**
    * Keeps a map from nodes to the subtheory that propagated it so that we can explain it
    * properly.
@@ -127,12 +122,16 @@ private:
     return indentStr;
   }
 
-  void setConflict(Node conflict) {
+  void setConflict(Node conflict = Node::null()) {
     d_conflict = true; 
-    d_conflictNode = conflict; 
+    d_conflictNode = conflict;
   }
 
-  bool inConflict() { return d_conflict == true; }
+  bool inConflict() {
+    return d_conflict;
+  }
+
+  void sendConflict();
 
   friend class Bitblaster;
   friend class BitblastSolver;
@@ -142,6 +141,7 @@ private:
 
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__BV__THEORY_BV_H */