More like best than inc-adjincremental-adjacent-try3

2 files changed, 33 insertions, 70 deletions

diff --git a/src/theory/arith/idl/idl_extension.cpp b/src/theory/arith/idl/idl_extension.cpp
index 6c9a2f7e5..f3fdb4dca 100644
--- a/src/theory/arith/idl/idl_extension.cpp
+++ b/src/theory/arith/idl/idl_extension.cpp
@@ -34,7 +34,6 @@ IdlExtension::IdlExtension(Env& env, TheoryArith& parent)
       d_parent(parent),
       d_varMap(context()),
       d_varList(context()),
-      d_matrix(context()),
       d_facts(context()),
       conflict_cycle(context()),
       d_dirty(context(), false),
@@ -81,9 +80,11 @@ void IdlExtension::presolve()
       << "IdlExtension::preSolve(): d_numVars = " << d_numVars << std::endl;
   d_dist.reserve(d_numVars);
   d_pred.reserve(d_numVars);
+  d_matrix.reserve(d_numVars);
   for (size_t i = 0; i < d_numVars; i++) {
-    d_dist[i] = new(context()->getCMM()) context::CDO(context(), Integer());
-    d_pred[i] = new(context()->getCMM()) context::CDO(context(), i);
+    d_dist.push_back(new(context()->getCMM()) context::CDO(context(), Integer()));
+    d_pred.push_back(new(context()->getCMM()) context::CDO(context(), i));
+    d_matrix.push_back(new(context()->getCMM()) context::CDHashMap<size_t, Integer>(context()));
   }
 }
 
@@ -121,7 +122,7 @@ void IdlExtension::notifyFact(
   size_t src = d_varMap[var1];
   size_t dst = d_varMap[var2];
 
-  if (d_matrix.count(_P(src, dst)) && d_matrix[_P(src, dst)].get() <= value) {
+  if (d_matrix[src]->count(dst) && (*(d_matrix[src]))[dst].get() <= value) {
     // This does not tighten it at all.
     return;
   }
@@ -136,7 +137,7 @@ void IdlExtension::notifyFact(
   }
 
   // Otherwise, update that cell.
-  d_matrix.insert(_P(src, dst), value);
+  d_matrix[src]->insert(dst, value);
   d_facts.insert(_P(src, dst), fact);
   d_node_dirty[src] = true;
   d_dirty = true;
@@ -180,34 +181,32 @@ void IdlExtension::postCheck(Theory::Effort level)
     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;
-        Integer edge_weight = edge.second;
-        Integer 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;
+      for (size_t edge_src = 0; edge_src < d_numVars; edge_src++) {
+        if (!node_dirty[edge_src]) continue;
+        for (const auto &edge : *(d_matrix[edge_src])) {
+          size_t edge_dst = edge.first;
+          Integer edge_weight = edge.second;
+          Integer 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;
           }
-          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;
@@ -226,43 +225,7 @@ void IdlExtension::postCheck(Theory::Effort level)
 bool IdlExtension::collectModelInfo(TheoryModel* m,
                                     const std::set<Node>& termSet)
 {
-  Integer zero = Integer(); // 0 constructor
-  std::vector<Integer> distance(d_numVars, zero);
-  for (size_t i = 0; i < d_numVars - 1; i++) {
-    bool any_modified = false;
-    for (const auto &edge : d_matrix) {
-      size_t edge_dst = edge.first.first,
-             edge_src = edge.first.second;
-      Integer edge_weight = edge.second;
-      if (distance[edge_dst] <= distance[edge_src] + edge_weight) continue;
-      any_modified = true;
-      distance[edge_dst] = distance[edge_src] + edge_weight;
-    }
-    if (!any_modified) break;
-  }
-
-  if (d_varMap.count(zero_node)) {
-    Integer offset = distance[d_varMap[zero_node]];
-    for (size_t i = 0; i < d_numVars; i++) {
-      distance[i] = distance[i] - offset;
-    }
-  }
-
-  // Validate all the edges are respected
-  for (const auto &edge : d_matrix) {
-    size_t edge_src = edge.first.first,
-           edge_dst = edge.first.second;
-    Integer edge_weight = edge.second;
-    Assert((distance[edge_src] - distance[edge_dst]) <= edge_weight);
-  }
-
-  NodeManager* nm = NodeManager::currentNM();
-  for (size_t i = 0; i < d_numVars; i++)
-  {
-    // Assert that the variable's value is equal to its distance in the model
-    m->assertEquality(d_varList[i], nm->mkConstInt(distance[i]), true);
-  }
-
+  // TODO: Update
   return true;
 }
 
diff --git a/src/theory/arith/idl/idl_extension.h b/src/theory/arith/idl/idl_extension.h
index 62729f5d5..e95bfd7e3 100644
--- a/src/theory/arith/idl/idl_extension.h
+++ b/src/theory/arith/idl/idl_extension.h
@@ -100,7 +100,7 @@ class IdlExtension : protected EnvObj
    *   is updated and they are 'frozen' until a pop happens to clear
    *   conflict_cycle. */
   /** d_matrix[i][j] = tightest edge weight from i to j (if exists). */
-  context::CDHashMap<std::pair<size_t, size_t>, Integer, hash_pair> d_matrix;
+  std::vector<context::CDHashMap<size_t, Integer> *> d_matrix;
   /** d_facts[i][j] stores the literal that is responsible for edge i->j. */
   context::CDHashMap<std::pair<size_t, size_t>, TNode, hash_pair> d_facts;
   /** d_dist[i] = weight of the tightest path to i (Bellman-Ford). */