Dirty nodes for the int64_t onestarter-inc-longs

2 files changed, 67 insertions, 50 deletions

diff --git a/src/theory/arith/idl/idl_extension.cpp b/src/theory/arith/idl/idl_extension.cpp
index 34c65b3ff..58ec73ff3 100644
--- a/src/theory/arith/idl/idl_extension.cpp
+++ b/src/theory/arith/idl/idl_extension.cpp
@@ -37,6 +37,7 @@ IdlExtension::IdlExtension(Env& env, TheoryArith& parent)
       d_matrix(context()),
       d_facts(context()),
       conflict_cycle(context()),
+      d_dirty(context(), false),
       d_numVars(0)
 {
   // Thanks to Andres and Aina for clarifying how to get an internal variable!
@@ -69,6 +70,7 @@ void IdlExtension::preRegisterTerm(TNode node)
     unsigned size = d_varMap.size();
     d_varMap[node] = size;
     d_varList.push_back(node);
+    d_node_dirty.push_back(false);
   }
 }
 
@@ -136,6 +138,8 @@ void IdlExtension::notifyFact(
   // Otherwise, update that cell.
   d_matrix.insert(_P(src, dst), value);
   d_facts.insert(_P(src, dst), fact);
+  d_node_dirty[src] = true;
+  d_dirty = true;
 }
 
 void IdlExtension::traceCycle(size_t dst, context::CDList<TNode> *into) {
@@ -153,6 +157,65 @@ void IdlExtension::traceCycle(size_t dst, context::CDList<TNode> *into) {
   }
 }
 
+void IdlExtension::postCheck(Theory::Effort level)
+{
+  Trace("theory::arith::idl")
+      << "IdlExtension::postCheck(): number of facts = " << d_facts.size()
+      << std::endl;
+  /* Only run for standard effort TODO: last call? */
+  if (!conflict_cycle.empty()) {
+    Assert(conflict_cycle.size() == 1);
+    // TODO: Handle this in notifyFact?
+    d_parent.getInferenceManager().conflict(conflict_cycle[0],
+                                            InferenceId::ARITH_CONF_IDL_EXT);
+    return;
+  }
+  if (!Theory::fullEffort(level)) {
+    Assert(conflict_cycle.empty());
+    if (!d_dirty.get()) return;
+    std::vector<bool> node_dirty = d_node_dirty;
+    std::vector<bool> next_node_dirty(d_numVars, false);
+    std::fill(std::begin(d_node_dirty), std::end(d_node_dirty), false);
+    d_dirty = false;
+    for (size_t i = 0; i < d_numVars; i++) { // TODO: d_diameter
+      std::fill(std::begin(next_node_dirty), std::end(next_node_dirty), false);
+      bool any_modified = false;
+      // TODO: The order of these edges does seem to make a difference, but I
+      // haven't yet found a better ordering than this (I guess, insertion
+      // order?).
+      for (const auto &edge : d_matrix) {
+        if (!node_dirty[edge.first.first]) continue;
+        size_t edge_src = edge.first.first,
+               edge_dst = edge.first.second;
+        int64_t edge_weight = edge.second;
+        int64_t alt_distance = d_dist[edge_src]->get() + edge_weight;
+        if (d_dist[edge_dst]->get() <= alt_distance) continue;
+        any_modified = true;
+        node_dirty[edge_dst] = true;
+        next_node_dirty[edge_dst] = true;
+        d_dist[edge_dst]->set(alt_distance);
+        d_pred[edge_dst]->set(edge_src);
+        if ((i + 1) == d_numVars) {
+          traceCycle(edge_dst, &conflict_cycle);
+          NodeBuilder conjunction(kind::AND);
+          for (Node fact : conflict_cycle) {
+            conjunction << fact;
+          }
+          Node conflict = conjunction;
+          // Send the conflict using the inference manager. Each conflict is assigned
+          // an ID. Here, we use  ARITH_CONF_IDL_EXT, which indicates a generic
+          // conflict detected by this extension
+          d_parent.getInferenceManager().conflict(conflict,
+                                                  InferenceId::ARITH_CONF_IDL_EXT);
+          return;
+        }
+      }
+      if (!any_modified) return;
+      std::swap(node_dirty, next_node_dirty);
+    }
+  }
+}
+
 Node IdlExtension::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
 {
   // We are only interested in predicates
@@ -331,56 +394,6 @@ Node IdlExtension::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
   return atom;
 }
 
-void IdlExtension::postCheck(Theory::Effort level)
-{
-  Trace("theory::arith::idl")
-      << "IdlExtension::postCheck(): number of facts = " << d_facts.size()
-      << std::endl;
-  /* Only run for standard effort TODO: last call? */
-  if (!conflict_cycle.empty()) {
-    Assert(conflict_cycle.size() == 1);
-    // TODO: Handle this in notifyFact?
-    d_parent.getInferenceManager().conflict(conflict_cycle[0],
-                                            InferenceId::ARITH_CONF_IDL_EXT);
-    return;
-  }
-  if (!Theory::fullEffort(level)) {
-    Assert(conflict_cycle.empty());
-    // TODO: I think this can be instead of d_numVars, just
-    // d_numVarsAdjacentToAnything.
-    for (size_t i = 0; i < d_numVars; i++) {
-      bool any_modified = false;
-      // TODO: The order of these edges does seem to make a difference, but I
-      // haven't yet found a better ordering than this (I guess, insertion
-      // order?).
-      for (const auto &edge : d_matrix) {
-        size_t edge_src = edge.first.first,
-               edge_dst = edge.first.second;
-        int64_t edge_weight = edge.second;
-        if (d_dist[edge_dst]->get() <= d_dist[edge_src]->get() + edge_weight) continue;
-        any_modified = true;
-        d_dist[edge_dst]->set(d_dist[edge_src]->get() + edge_weight);
-        d_pred[edge_dst]->set(edge_src);
-        if ((i + 1) == d_numVars) {
-          traceCycle(edge_dst, &conflict_cycle);
-          NodeBuilder conjunction(kind::AND);
-          for (Node fact : conflict_cycle) {
-            conjunction << fact;
-          }
-          Node conflict = conjunction;
-          // Send the conflict using the inference manager. Each conflict is assigned
-          // an ID. Here, we use  ARITH_CONF_IDL_EXT, which indicates a generic
-          // conflict detected by this extension
-          d_parent.getInferenceManager().conflict(conflict,
-                                                  InferenceId::ARITH_CONF_IDL_EXT);
-          return;
-        }
-      }
-      if (!any_modified) return;
-    }
-  }
-}
-
 // Idea is to assign each node its shortest distance from any other given node
 // (including itself). Flip the directions of the edges, so x->y is the upper
 // bound of y-x. Then for an edge x->y, we want to guarantee that y-x is _at
diff --git a/src/theory/arith/idl/idl_extension.h b/src/theory/arith/idl/idl_extension.h
index 340c269d4..22a810c70 100644
--- a/src/theory/arith/idl/idl_extension.h
+++ b/src/theory/arith/idl/idl_extension.h
@@ -110,6 +110,10 @@ class IdlExtension : protected EnvObj
   /** If a conflict (negative cycle) is found, it is stored here. */
   context::CDList<TNode> conflict_cycle;
 
+  context::CDO<bool> d_dirty;
+
+  std::vector<bool> d_node_dirty;
+
   void traceCycle(size_t dst, context::CDList<TNode> *into);
 
   /** Shifted to zero always in the model. */