Revert "Slightly better sorting key"inc-adj-list

This reverts commit 61b0ee9fc9208b49b2a8f35d93cef8af140f14b5.

2 files changed, 23 insertions, 10 deletions

diff --git a/src/theory/arith/idl/idl_extension.cpp b/src/theory/arith/idl/idl_extension.cpp
index 5a54d591a..e0c9bafab 100644
--- a/src/theory/arith/idl/idl_extension.cpp
+++ b/src/theory/arith/idl/idl_extension.cpp
@@ -18,6 +18,7 @@
 #include <iomanip>
 #include <queue>
 #include <set>
+#include <tuple>
 
 #include "expr/node_builder.h"
 #include "theory/arith/theory_arith.h"
@@ -186,12 +187,13 @@ inline bool IdlExtension::traceConflict(size_t dst) {
 
 class CompareWorkItems {
 public:
-  bool operator()(const std::pair<size_t, Integer> &a,
-                  const std::pair<size_t, Integer> &b) {
-    return a.second < b.second;
+  bool operator()(const std::tuple<size_t, Integer, Integer> &a,
+                  const std::tuple<size_t, Integer, Integer> &b) {
+    return std::get<1>(a) < std::get<1>(b);
   }
 };
 
+
 void IdlExtension::postCheck(Theory::Effort level)
 {
   Trace("theory::arith::idl")
@@ -212,11 +214,11 @@ void IdlExtension::postCheck(Theory::Effort level)
   Assert(conflict_cycle.empty());
   // Init the running worklist, dirty bits, clear the old dirty bits
   // {node, change_amt, change_to}
-  std::priority_queue<std::pair<size_t, Integer>, std::vector<std::pair<size_t, Integer>>, CompareWorkItems> worklist;
+  std::priority_queue<std::tuple<size_t, Integer, Integer>, std::vector<std::tuple<size_t, Integer, Integer>>, CompareWorkItems> worklist;
   for (size_t item : d_dirty_list) {
     const Integer &dist = d_dist[item]->get();
     // TODO: -1000
-    worklist.emplace(item, dist);
+    worklist.emplace(std::make_tuple(item, Integer(-1000), dist));
     pc_node_best[item] = dist;
   }
   d_dirty_list.clear();
@@ -230,8 +232,8 @@ void IdlExtension::postCheck(Theory::Effort level)
     // Pop the next workitem.
     auto workitem = worklist.top();
     worklist.pop();
-    if (workitem.second != pc_node_best[workitem.first]) continue;
-    size_t edge_src = workitem.first;
+    if (std::get<2>(workitem) != pc_node_best[std::get<0>(workitem)]) continue;
+    size_t edge_src = std::get<0>(workitem);
     pc_node_in_queue[edge_src] = false;
     // Check if any neighbors need to be updated.
     for (const auto &edge : *(d_matrix[edge_src])) {
@@ -240,9 +242,11 @@ void IdlExtension::postCheck(Theory::Effort level)
       const Integer alt_distance = std::move(d_dist[edge_src]->get() + edge_weight);
       const Integer &old_dist = d_dist[edge_dst]->get();
       if (old_dist <= alt_distance) continue;
+      const Integer delta = alt_distance - old_dist;
       d_dist[edge_dst]->set(alt_distance);
       d_pred[edge_dst]->set({edge_src, edge.second.second});
       n_updates++;
+      // TODO: Can this check against the in-degree?
       if (n_updates % 32 == 0 || alt_distance < path_lb) { // TODO: off-by-one?
         // TODO: Do waves and keep track of them so that this doesn't need an
         // if guard.
@@ -252,9 +256,7 @@ void IdlExtension::postCheck(Theory::Effort level)
       }
       // Make sure this node is in the queue to be handled next time.
       pc_node_in_queue[edge_dst] = true;
-      // NOTE: I've tried also sorting this based on the delta, but the raw
-      // 'new distance' seems to do somewhat better.
-      worklist.emplace(edge_dst, alt_distance);
+      worklist.emplace(std::make_tuple(edge_dst, delta, alt_distance));
       pc_node_best[edge_dst] = alt_distance;
     }
   }
diff --git a/src/theory/arith/idl/idl_extension.h b/src/theory/arith/idl/idl_extension.h
index cd7b8ec35..8b570cb45 100644
--- a/src/theory/arith/idl/idl_extension.h
+++ b/src/theory/arith/idl/idl_extension.h
@@ -34,6 +34,17 @@ class TheoryArith;
 
 namespace idl {
 
+// https://www.geeksforgeeks.org/how-to-create-an-unordered_map-of-pairs-in-c/
+struct hash_pair {
+  template <class T1, class T2>
+  size_t operator()(const std::pair<T1, T2>& p) const
+  {
+    auto hash1 = std::hash<T1>{}(p.first);
+    auto hash2 = std::hash<T2>{}(p.second);
+    return hash1 ^ hash2;
+  }
+};
+
 /**
  * Handles integer difference logic (IDL) constraints.
  */