Fix BV inequality solver caching.

2 files changed, 17 insertions, 8 deletions

diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 4f9eb0823..917b10c33 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -137,14 +137,14 @@ void InequalitySolver::assertFact(TNode fact) {
 }
 
 bool InequalitySolver::isInequalityOnly(TNode node) {
-  if (d_ineqOnlyCache.find(node) != d_ineqOnlyCache.end()) {
-    return d_ineqOnlyCache[node];
-  }
-
   if (node.getKind() == kind::NOT) {
     node = node[0];
   }
 
+  if (node.getAttribute(IneqOnlyComputedAttribute())) {
+    return node.getAttribute(IneqOnlyAttribute());
+  }
+
   if (node.getKind() != kind::EQUAL &&
       node.getKind() != kind::BITVECTOR_ULT &&
       node.getKind() != kind::BITVECTOR_ULE &&
@@ -152,13 +152,15 @@ bool InequalitySolver::isInequalityOnly(TNode node) {
       node.getKind() != kind::SELECT &&
       node.getKind() != kind::STORE &&
       node.getMetaKind() != kind::metakind::VARIABLE) {
+    // not worth caching
     return false;
   }
   bool res = true;
-  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+  for (unsigned i = 0; res && i < node.getNumChildren(); ++i) {
     res = res && isInequalityOnly(node[i]);
   }
-  d_ineqOnlyCache[node] = res;
+  node.setAttribute(IneqOnlyComputedAttribute(), true);
+  node.setAttribute(IneqOnlyAttribute(), res);
   return res;
 }
 
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index b9195c7d1..c9d9dabd3 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -22,11 +22,20 @@
 #include "theory/bv/bv_subtheory.h"
 #include "theory/bv/bv_inequality_graph.h"
 #include "context/cdhashset.h"
+#include "expr/attribute.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
+/** Cache for InequalitySolver::isInequalityOnly() */
+struct IneqOnlyAttributeId {};
+typedef expr::Attribute<IneqOnlyAttributeId, bool> IneqOnlyAttribute;
+
+/** Whether the above has been computed yet or not for an expr */
+struct IneqOnlyComputedAttributeId {};
+typedef expr::Attribute<IneqOnlyComputedAttributeId, bool> IneqOnlyComputedAttribute;
+
 class InequalitySolver: public SubtheorySolver {
   struct Statistics {
     IntStat d_numCallstoCheck;
@@ -38,7 +47,6 @@ 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_ineqOnlyCache;
   typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
   TNodeSet d_ineqTerms;
   bool isInequalityOnly(TNode node);
@@ -51,7 +59,6 @@ public:
       d_inequalityGraph(c),
       d_explanations(c),
       d_isComplete(c, true),
-      d_ineqOnlyCache(),
       d_ineqTerms(),
       d_statistics()
   {}