Remove the rest of my CDHashMapsstarter-bellman-incincremental-no-hashmap

2 files changed, 92 insertions, 52 deletions

diff --git a/src/theory/arith/idl/idl_extension.cpp b/src/theory/arith/idl/idl_extension.cpp
index 6c9a2f7e5..60285a609 100644
--- a/src/theory/arith/idl/idl_extension.cpp
+++ b/src/theory/arith/idl/idl_extension.cpp
@@ -34,8 +34,7 @@ IdlExtension::IdlExtension(Env& env, TheoryArith& parent)
       d_parent(parent),
       d_varMap(context()),
       d_varList(context()),
-      d_matrix(context()),
-      d_facts(context()),
+      d_edges(context()),
       conflict_cycle(context()),
       d_dirty(context(), false),
       d_numVars(0)
@@ -57,11 +56,33 @@ IdlExtension::~IdlExtension() {
   // }
   d_dist.clear();
   d_pred.clear();
+  // TODO: Rest if necessary
 }
 
 void IdlExtension::preRegisterTerm(TNode node)
 {
   Assert(d_numVars == 0);
+  if (node.getKind() == kind::MINUS && node[0].isVar() && node[1].isVar()) {
+    size_t idx_src = d_varMap[node[0]],
+           idx_dst = d_varMap[node[1]];
+    // Extend the relevant matrices.
+    d_matrix[idx_src].resize(d_varMap.size(), nullptr);
+    d_matrix[idx_dst].resize(d_varMap.size(), nullptr);
+    d_facts[idx_src].resize(d_varMap.size(), nullptr);
+    d_facts[idx_dst].resize(d_varMap.size(), nullptr);
+    d_adj[idx_src].resize(d_varMap.size(), nullptr);
+    d_adj[idx_dst].resize(d_varMap.size(), nullptr);
+    // src->dst
+    d_overapprox_adj_set[idx_src].emplace(idx_dst);
+    d_matrix[idx_src][idx_dst] = new(context()->getCMM()) context::CDO<Integer>(context());
+    d_facts[idx_src][idx_dst] = new(context()->getCMM()) context::CDO<TNode>(context());
+    d_adj[idx_src][idx_dst] = new(context()->getCMM()) context::CDO<bool>(context());
+    // dst->src
+    d_overapprox_adj_set[idx_dst].emplace(idx_src);
+    d_matrix[idx_dst][idx_src] = new(context()->getCMM()) context::CDO<Integer>(context());
+    d_facts[idx_dst][idx_src] = new(context()->getCMM()) context::CDO<TNode>(context());
+    d_adj[idx_dst][idx_src] = new(context()->getCMM()) context::CDO<bool>(context());
+  }
   if (node.isVar())
   {
     Trace("theory::arith::idl")
@@ -71,6 +92,10 @@ void IdlExtension::preRegisterTerm(TNode node)
     d_varMap[node] = size;
     d_varList.push_back(node);
     d_node_dirty.push_back(false);
+    d_matrix.emplace_back();
+    d_facts.emplace_back();
+    d_overapprox_adj_set.emplace_back();
+    d_adj.emplace_back();
   }
 }
 
@@ -82,8 +107,11 @@ void IdlExtension::presolve()
   d_dist.reserve(d_numVars);
   d_pred.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[i].resize(d_numVars, nullptr);
+    d_facts[i].resize(d_numVars, nullptr);
+    d_adj[i].resize(d_numVars, nullptr);
   }
 }
 
@@ -121,7 +149,8 @@ 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) {
+  Assert(d_adj[src][dst] && d_matrix[src][dst] && d_facts[src][dst]);
+  if (d_adj[src][dst]->get() && d_matrix[src][dst]->get() <= value) {
     // This does not tighten it at all.
     return;
   }
@@ -136,8 +165,12 @@ void IdlExtension::notifyFact(
   }
 
   // Otherwise, update that cell.
-  d_matrix.insert(_P(src, dst), value);
-  d_facts.insert(_P(src, dst), fact);
+  d_matrix[src][dst]->set(value);
+  d_facts[src][dst]->set(fact);
+  if (!d_adj[src][dst]->get()) {
+    d_adj[src][dst]->set(true);
+    d_edges.push_back(std::make_pair(src, dst));
+  }
   d_node_dirty[src] = true;
   d_dirty = true;
 }
@@ -153,7 +186,7 @@ void IdlExtension::traceCycle(size_t dst, context::CDList<TNode> *into) {
   cycle.erase(cycle.begin(), cycle.begin() + node_to_cycle_idx[cycle.back()]);
   Assert(cycle.size() >= 2);
   for (size_t i = 0; i < cycle.size() - 1; i++) {
-    into->push_back(d_facts[_P(cycle[i+1], cycle[i])].get());
+    into->push_back(d_facts[cycle[i+1]][cycle[i]]->get());
   }
 }
 
@@ -180,14 +213,12 @@ 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;
+      for (auto it = d_edges.end(); it != d_edges.begin();) {
+        it--;
+        if (!node_dirty[it->first]) continue;
+        size_t edge_src = it->first,
+               edge_dst = it->second;
+        Integer edge_weight = d_matrix[edge_src][edge_dst]->get();
         Integer alt_distance = d_dist[edge_src]->get() + edge_weight;
         if (d_dist[edge_dst]->get() <= alt_distance) continue;
         any_modified = true;
@@ -226,44 +257,46 @@ 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;
-  }
+  return true;
+  // TODO: Update me to use the new data structures
+  // 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;
-    }
-  }
+  // 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);
-  }
+  // // 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);
-  }
+  // 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);
+  // }
 
-  return true;
+  // return true;
 }
 
 void IdlExtension::printMatrix(const std::vector<std::vector<Integer>>& matrix,
diff --git a/src/theory/arith/idl/idl_extension.h b/src/theory/arith/idl/idl_extension.h
index 62729f5d5..9350664cf 100644
--- a/src/theory/arith/idl/idl_extension.h
+++ b/src/theory/arith/idl/idl_extension.h
@@ -100,9 +100,16 @@ 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<std::vector<context::CDO<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;
+  std::vector<std::vector<context::CDO<TNode> *>> d_facts;
+  /** d_overapprox_adj[i] stores an overapproximation of the nodes adjacent to
+   * i (any direction) */
+  std::vector<std::set<size_t>> d_overapprox_adj_set;
+  std::vector<std::vector<bool>> d_overapprox_adj_vector;
+  /** Stores the actual adjacency */
+  std::vector<std::vector<context::CDO<bool> *>> d_adj;
+  context::CDList<std::pair<size_t, size_t>> d_edges;
   /** d_dist[i] = weight of the tightest path to i (Bellman-Ford). */
   std::vector<context::CDO<Integer> *> d_dist;
   /** d_pred[i] = predecessor along tightest path to i (Bellman-Ford) */