fixed inequality bugs due to improper explanation

4 files changed, 32 insertions, 21 deletions

diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index a1d2efbb5..3dfeba140 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -358,7 +358,17 @@ bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) {
       return addInequality(a, b, true, explanation);
     }
     if (b.getKind() == kind::CONST_BITVECTOR) {
-      return addInequality(b, a, true, reason);
+      // then we know b cannot be smaller  than the assigned value so we try to make it larger
+      std::vector<ReasonId> explanation_ids; 
+      computeExplanation(UndefinedTermId, id_a, explanation_ids); 
+      std::vector<TNode> explanation_nodes;
+      explanation_nodes.push_back(reason);
+      for (unsigned i = 0; i < explanation_ids.size(); ++i) {
+        explanation_nodes.push_back(getReasonNode(explanation_ids[i])); 
+      }
+      Node explanation = utils::mkAnd(explanation_nodes);
+      d_reasonSet.insert(explanation); 
+      return addInequality(b, a, true, explanation);
     }
     // if none of the terms are constants just add the lemma 
     splitDisequality(reason);
@@ -410,8 +420,7 @@ void InequalityGraph::backtrack() {
       Debug("bv-inequality-internal") << getTermNode(it->next) <<" " << it->strict << "\n"; 
     }
     Assert (!edges.empty());
-    InequalityEdge back = edges.back(); 
-    Assert (back == edge);
+    Assert (edges.back() == edge);
     edges.pop_back(); 
   }
 }
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index ad12681f3..112f73083 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -205,7 +205,8 @@ bool CoreSolver::check(Theory::Effort e) {
     
     // only reason about equalities
     if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
-      ok = decomposeFact(fact);
+      // ok = decomposeFact(fact);
+      ok = assertFactToEqualityEngine(fact, fact); 
     } else {
       ok = assertFactToEqualityEngine(fact, fact); 
     }
@@ -214,13 +215,13 @@ bool CoreSolver::check(Theory::Effort e) {
   }
   
   // make sure to assert the new splits
-  std::vector<Node> new_splits;
-  d_slicer->getNewSplits(new_splits);
-  for (unsigned i = 0; i < new_splits.size(); ++i) {
-    ok = assertFactToEqualityEngine(new_splits[i], utils::mkTrue());
-    if (!ok)
-      return false; 
-  }
+  // std::vector<Node> new_splits;
+  // d_slicer->getNewSplits(new_splits);
+  // for (unsigned i = 0; i < new_splits.size(); ++i) {
+  //   ok = assertFactToEqualityEngine(new_splits[i], utils::mkTrue());
+  //   if (!ok)
+  //     return false; 
+  // }
   return true;
 }
 
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index 5382695cf..23ae5beec 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -209,9 +209,8 @@ ExtractTerm UnionFind::mkExtractTerm(TermId id, Index high, Index low) {
   ExtractTerm top = getExtractTerm(id);
   Assert (d_topLevelIds.find(top.id) != d_topLevelIds.end());
   
-  Index top_high = top.high;
   Index top_low = top.low;
-  Assert (top_high - top_low + 1 > high);
+  Assert (top.high - top_low + 1 > high);
   high += top_low; 
   low += top_low;
   id = top.id; 
@@ -602,8 +601,7 @@ void UnionFind::backtrack() {
 }
 
 void UnionFind::undoMerge(TermId id) {
-  TermId repr = getRepr(id);
-  Assert (repr != UndefinedId);
+  Assert (getRepr(id) != UndefinedId);
   setRepr(id, UndefinedId, UndefinedId); 
 }
 
@@ -781,7 +779,10 @@ bool Slicer::isCoreTerm(TNode node) {
     Kind kind = node.getKind(); 
     if (kind != kind::BITVECTOR_EXTRACT &&
         kind != kind::BITVECTOR_CONCAT &&
-        kind != kind::EQUAL && kind != kind::NOT &&
+        kind != kind::EQUAL &&
+        kind != kind::STORE &&
+        kind != kind::SELECT &&
+        kind != kind::NOT &&
         node.getMetaKind() != kind::metakind::VARIABLE &&
         kind != kind::CONST_BITVECTOR) {
       d_coreTermCache[node] = false;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index a62324946..43e290175 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -225,11 +225,11 @@ Node TheoryBV::ppRewrite(TNode t)
     return Rewriter::rewrite(result);
   }
   
-  if (t.getKind() == kind::EQUAL) {
-    std::vector<Node> equalities;
-    Slicer::splitEqualities(t, equalities);
-    return utils::mkAnd(equalities); 
-  }
+  // if (t.getKind() == kind::EQUAL) {
+  //   std::vector<Node> equalities;
+  //   Slicer::splitEqualities(t, equalities);
+  //   return utils::mkAnd(equalities); 
+  // }
   
   return t;
 }