used strongly typed reversible data structures

ortools/sat/integer.cc

@@ -1686,11 +1686,12 @@ bool GenericLiteralWatcher::Propagate(Trail* trail) {
       // Before we propagate, make sure any reversible structure are up to date.
       // Note that we never do anything expensive more than once per level.
       {
-        const int low = id_to_greatest_common_level_since_last_call_[id];
+        const int low =
+            id_to_greatest_common_level_since_last_call_[IdType(id)];
         const int high = id_to_level_at_last_call_[id];
         if (low < high || level > low) {  // Equivalent to not all equal.
           id_to_level_at_last_call_[id] = level;
-          id_to_greatest_common_level_since_last_call_[id] = level;
+          id_to_greatest_common_level_since_last_call_[IdType(id)] = level;
           for (ReversibleInterface* rev : id_to_reversible_classes_[id]) {
             if (low < high) rev->SetLevel(low);
             if (level > low) rev->SetLevel(level);

ortools/sat/integer.h

@@ -1121,8 +1121,9 @@ class GenericLiteralWatcher : public SatPropagator {
   std::vector<bool> in_queue_;
 
   // Data for each propagator.
+  DEFINE_INT_TYPE(IdType, int32);
   std::vector<int> id_to_level_at_last_call_;
-  RevVector<int> id_to_greatest_common_level_since_last_call_;
+  RevVector<IdType, int> id_to_greatest_common_level_since_last_call_;
   std::vector<std::vector<ReversibleInterface*>> id_to_reversible_classes_;
   std::vector<std::vector<int*>> id_to_reversible_ints_;
   std::vector<std::vector<int>> id_to_watch_indices_;

ortools/util/rev.h

@@ -18,6 +18,7 @@
 #include <vector>
 
 #include "absl/container/flat_hash_map.h"
+#include "ortools/base/int_type_indexed_vector.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/map_util.h"
 
@@ -83,13 +84,13 @@ class RevRepository : public ReversibleInterface {
 };
 
 // A basic reversible vector implementation.
-template <class T>
+template <class IndexType, class T>
 class RevVector : public ReversibleInterface {
  public:
-  const T& operator[](int index) const { return vector_[index]; }
-  T& operator[](int index) {
+  const T& operator[](IndexType index) const { return vector_[index]; }
+  T& operator[](IndexType index) {
     // Save on the stack first.
-    stack_.push_back({index, vector_[index]});
+    if (!end_of_level_.empty()) stack_.push_back({index, vector_[index]});
     return vector_[index];
   }
 
@@ -121,8 +122,8 @@ class RevVector : public ReversibleInterface {
 
  private:
   std::vector<int> end_of_level_;  // In stack_.
-  std::vector<std::pair<int, T>> stack_;
-  std::vector<T> vector_;
+  std::vector<std::pair<IndexType, T>> stack_;
+  gtl::ITIVector<IndexType, T> vector_;
 };
 
 template <class T>