added bv inequality lemmas

2 files changed, 38 insertions, 11 deletions

diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index c6a92a439..4b894fe2a 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -37,9 +37,9 @@ bool InequalitySolver::check(Theory::Effort e) {
     if (fact.getKind() == kind::EQUAL) {
       TNode a = fact[0];
       TNode b = fact[1];
-      ok = d_inequalityGraph.addInequality(a, b, false, fact);
+      ok = addInequality(a, b, false, fact);
       if (ok)
-        ok = d_inequalityGraph.addInequality(b, a, false, fact);
+        ok = addInequality(b, a, false, fact);
     } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL) {
       TNode a = fact[0][0];
       TNode b = fact[0][1];
@@ -48,7 +48,7 @@ bool InequalitySolver::check(Theory::Effort e) {
     if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) {
       TNode a = fact[0][1];
       TNode b = fact[0][0];
-      ok = d_inequalityGraph.addInequality(a, b, true, fact);
+      ok = addInequality(a, b, true, fact);
       // propagate
       // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
       //   Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b));
@@ -58,11 +58,11 @@ bool InequalitySolver::check(Theory::Effort e) {
     } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULT) {
       TNode a = fact[0][1];
       TNode b = fact[0][0];
-      ok = d_inequalityGraph.addInequality(a, b, false, fact);
+      ok = addInequality(a, b, false, fact);
     } else if (fact.getKind() == kind::BITVECTOR_ULT) {
       TNode a = fact[0];
       TNode b = fact[1];
-      ok = d_inequalityGraph.addInequality(a, b, true, fact);
+      ok = addInequality(a, b, true, fact);
       // propagate
       // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
       //   Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b));
@@ -72,7 +72,7 @@ bool InequalitySolver::check(Theory::Effort e) {
     } else if (fact.getKind() == kind::BITVECTOR_ULE) {
       TNode a = fact[0];
       TNode b = fact[1];
-      ok = d_inequalityGraph.addInequality(a, b, false, fact);
+      ok = addInequality(a, b, false, fact);
     }
   }
 
@@ -137,8 +137,8 @@ void InequalitySolver::assertFact(TNode fact) {
 }
 
 bool InequalitySolver::isInequalityOnly(TNode node) {
-  if (d_ineqTermCache.find(node) != d_ineqTermCache.end()) {
-    return d_ineqTermCache[node];
+  if (d_ineqOnlyCache.find(node) != d_ineqOnlyCache.end()) {
+    return d_ineqOnlyCache[node];
   }
 
   if (node.getKind() == kind::NOT) {
@@ -158,7 +158,7 @@ bool InequalitySolver::isInequalityOnly(TNode node) {
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
     res = res && isInequalityOnly(node[i]);
   }
-  d_ineqTermCache[node] = res;
+  d_ineqOnlyCache[node] = res;
   return res;
 }
 
@@ -198,6 +198,28 @@ Node InequalitySolver::getModelValue(TNode var) {
   return result;
 }
 
+void InequalitySolver::preRegister(TNode node) {
+  Kind kind = node.getKind(); 
+  if (kind == kind::EQUAL ||
+      kind == kind::BITVECTOR_ULE ||
+      kind == kind::BITVECTOR_ULT) {
+    d_ineqTerms.insert(node[0]);
+    d_ineqTerms.insert(node[1]);
+  }
+}
+
+bool InequalitySolver::addInequality(TNode a, TNode b, bool strict, TNode fact) {
+  bool ok = d_inequalityGraph.addInequality(a, b, strict, fact);
+  if (!ok || !strict) return ok;
+
+  Node one = utils::mkConst(utils::getSize(a), 1);
+  Node a_plus_one = Rewriter::rewrite(utils::mkNode(kind::BITVECTOR_PLUS, a, one));
+  if (d_ineqTerms.find(a_plus_one) != d_ineqTerms.end()) {
+    ok = d_inequalityGraph.addInequality(a_plus_one, b, false, fact);
+  }
+  return ok;
+}
+
 InequalitySolver::Statistics::Statistics()
   : d_numCallstoCheck("theory::bv::InequalitySolver::NumCallsToCheck", 0)
 {
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index f142ff7be..ef03166e6 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -38,8 +38,11 @@ class InequalitySolver: public SubtheorySolver {
   InequalityGraph d_inequalityGraph;
   context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations;
   context::CDO<bool> d_isComplete;
-  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache;
+  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqOnlyCache;
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+  TNodeSet d_ineqTerms;
   bool isInequalityOnly(TNode node);
+  bool addInequality(TNode a, TNode b, bool strict, TNode fact);
   Statistics d_statistics;
 public:
   InequalitySolver(context::Context* c, TheoryBV* bv)
@@ -48,7 +51,8 @@ public:
       d_inequalityGraph(c),
       d_explanations(c),
       d_isComplete(c, true),
-      d_ineqTermCache(),
+      d_ineqOnlyCache(),
+      d_ineqTerms(),
       d_statistics()
   {}
 
@@ -60,6 +64,7 @@ public:
   Node getModelValue(TNode var);
   EqualityStatus getEqualityStatus(TNode a, TNode b);
   void assertFact(TNode fact);
+  void preRegister(TNode node);
 };
 
 }