introduce array slices and use them in sat

ortools/algorithms/dynamic_partition.cc

@@ -28,19 +28,20 @@ uint64 FprintOfInt32(int i) {
 }
 }  // namespace
 
-DynamicPartition::DynamicPartition(int n) {
-  DCHECK_GE(n, 0);
-  element_.assign(n, -1);
-  index_of_.assign(n, -1);
-  for (int i = 0; i < n; ++i) {
+DynamicPartition::DynamicPartition(int num_elements) {
+  DCHECK_GE(num_elements, 0);
+  element_.assign(num_elements, -1);
+  index_of_.assign(num_elements, -1);
+  for (int i = 0; i < num_elements; ++i) {
     element_[i] = i;
     index_of_[i] = i;
   }
-  part_of_.assign(n, 0);
+  part_of_.assign(num_elements, 0);
   uint64 fprint = 0;
-  for (int i = 0; i < n; ++i) fprint ^= FprintOfInt32(i);
-  part_.push_back(Part(/*start_index=*/0, /*end_index=*/n, /*parent_part=*/0,
-                       /*fprint=*/ fprint));
+  for (int i = 0; i < num_elements; ++i) fprint ^= FprintOfInt32(i);
+  part_.push_back(Part(/*start_index=*/0, /*end_index=*/num_elements,
+                       /*parent_part=*/0,
+                       /*fprint=*/fprint));
 }
 
 DynamicPartition::DynamicPartition(

ortools/algorithms/dynamic_partition.h

@@ -49,7 +49,7 @@ class DynamicPartition {
  public:
   // Creates a DynamicPartition on n elements, numbered 0..n-1. Start with
   // the trivial partition (only one subset containing all elements).
-  explicit DynamicPartition(int n);
+  explicit DynamicPartition(int num_elements);
 
   // Ditto, but specify the initial part of each elements. Part indices must
   // form a dense integer set starting at 0; eg. [2, 1, 0, 1, 1, 3, 0] is valid.
@@ -164,8 +164,11 @@ class DynamicPartition {
     uint64 fprint;
 
     Part() : start_index(0), end_index(0), parent_part(0), fprint(0) {}
-    Part(int s, int e, int p, uint64 fp)
-        : start_index(s), end_index(e), parent_part(p), fprint(fp) {}
+    Part(int start_index, int end_index, int parent_part, uint64 fprint)
+        : start_index(start_index),
+          end_index(end_index),
+          parent_part(parent_part),
+          fprint(fprint) {}
   };
   std::vector<Part> part_;  // The disjoint parts.
 

ortools/algorithms/find_graph_symmetries.cc

@@ -196,7 +196,7 @@ void GraphSymmetryFinder::RecursivelyRefinePartitionByAdjacency(
   //
   // Thus, the following loop really does the full recursive refinement as
   // advertised.
-  std::vector<bool> adjacency_directions(1, /*outgoing=*/true);
+  std::vector<bool> adjacency_directions(1, /*outgoing*/ true);
   if (!reverse_adj_list_index_.empty()) {
     adjacency_directions.push_back(false);  // Also look at incoming arcs.
   }

ortools/base/inlined_vector.h

@@ -0,0 +1,665 @@
+// Copyright 2010-2014 Google
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#ifndef OR_TOOLS_BASE_INLINED_VECTOR_H_
+#define OR_TOOLS_BASE_INLINED_VECTOR_H_
+
+// An InlinedVector<T,N,A> is like a std::vector<T,A>, except that storage
+// for sequences of length <= N are provided inline without requiring
+// any heap allocation.  Typically N is very small (e.g., 4) so that
+// sequences that are expected to be short do not require allocations.
+//
+// Only some of the std::vector<> operations are currently implemented.
+// Other operations may be added as needed to facilitate migrating
+// code that uses std::vector<> to InlinedVector<>.
+//
+// NOTE: If you want an inlined version to replace use of a
+// std::vector<bool>, consider using util::bitmap::InlinedBitVector<NBITS>
+// in ortools/base/inlined_bitvector.h
+//
+
+#include <sys/types.h>
+
+#include <cstddef>
+#include <cstdlib>
+#include <cstring>
+#include <algorithm>
+#include <iterator>
+#include <memory>
+#include <type_traits>
+#include <vector>
+#include <initializer_list>  // NOLINT(build/include_order)
+
+#include "ortools/base/logging.h"
+
+namespace gtl {
+
+template <typename T, int N>
+class InlinedVector {
+ public:
+  typedef T value_type;
+  typedef T* pointer;
+  typedef const T* const_pointer;
+  typedef T& reference;
+  typedef const T& const_reference;
+  typedef size_t size_type;
+  typedef std::ptrdiff_t difference_type;
+  typedef pointer iterator;
+  typedef const_pointer const_iterator;
+
+  // Create an empty vector
+  InlinedVector();
+
+  // Create a vector with n copies of value_type().
+  explicit InlinedVector(size_t n);
+
+  // Create a vector with n copies of elem
+  InlinedVector(size_t n, const value_type& elem);
+
+  // Create and initialize with the elements [range_start .. range_end).
+  // The unused enable_if argument restricts this constructor so that it is
+  // elided when value_type is an integral type.  This prevents ambiguous
+  // interpretation between a call to this constructor with two integral
+  // arguments and a call to the preceding (n, elem) constructor.
+  template <typename InputIterator>
+  InlinedVector(
+      InputIterator range_start, InputIterator range_end,
+      typename std::enable_if<!std::is_integral<InputIterator>::value>::type* =
+          NULL) {
+    InitRep();
+    AppendRange(range_start, range_end);
+  }
+
+  InlinedVector(std::initializer_list<value_type> init) {
+    InitRep();
+    AppendRange(init.begin(), init.end());
+  }
+
+  InlinedVector(const InlinedVector& v);
+
+  ~InlinedVector() { clear(); }
+
+  InlinedVector& operator=(const InlinedVector& v) {
+    // Optimized to avoid reallocation.
+    // Prefer reassignment to copy construction for elements.
+    const size_t s = size();
+    const size_t vs = v.size();
+    if (s < vs) {  // grow
+      reserve(vs);
+      if (s) std::copy(v.begin(), v.begin() + s, begin());
+      std::copy(v.begin() + s, v.end(), std::back_inserter(*this));
+    } else {  // maybe shrink
+      erase(begin() + vs, end());
+      std::copy(v.begin(), v.end(), begin());
+    }
+    return *this;
+  }
+
+  size_t size() const { return size_internal(); }
+
+  bool empty() const { return (size() == 0); }
+
+  // Return number of elements that can be stored in vector
+  // without requiring a reallocation of underlying memory
+  size_t capacity() const {
+    if (is_inline()) {
+      return kFit;
+    } else {
+      return static_cast<size_t>(1) << u_.data[kSize - 2];
+    }
+  }
+
+  // Return a pointer to the underlying array.
+  // Only result[0,size()-1] are defined.
+  pointer data() {
+    if (is_inline()) {
+      return reinterpret_cast<T*>(u_.data);
+    } else {
+      return outofline_pointer();
+    }
+  }
+  const_pointer data() const {
+    return const_cast<InlinedVector<T, N>*>(this)->data();
+  }
+
+  // Remove all elements
+  void clear() {
+    DiscardStorage();
+    u_.data[kSize - 1] = 0;
+  }
+
+  // Return the ith element
+  // REQUIRES: 0 <= i < size()
+  const value_type& at(size_t i) const {
+    DCHECK_LT(i, size());
+    return data()[i];
+  }
+  const value_type& operator[](size_t i) const {
+    DCHECK_LT(i, size());
+    return data()[i];
+  }
+
+  // Return a non-const reference to the ith element
+  // REQUIRES: 0 <= i < size()
+  value_type& at(size_t i) {
+    DCHECK_LT(i, size());
+    return data()[i];
+  }
+  value_type& operator[](size_t i) {
+    DCHECK_LT(i, size());
+    return data()[i];
+  }
+
+  value_type& back() {
+    DCHECK(!empty());
+    return at(size() - 1);
+  }
+
+  const value_type& back() const {
+    DCHECK(!empty());
+    return at(size() - 1);
+  }
+
+  value_type& front() {
+    DCHECK(!empty());
+    return at(0);
+  }
+
+  const value_type& front() const {
+    DCHECK(!empty());
+    return at(0);
+  }
+
+  // Append a T constructed with args to the vector.
+  // Increases size() by one.
+  // Amortized complexity: O(1)
+  // Worst-case complexity: O(size())
+  template <typename... Args>
+  void emplace_back(Args&&... args) {
+    size_t s = size();
+    DCHECK_LE(s, capacity());
+    if (s < capacity()) {
+      new (data() + s) T(std::forward<Args>(args)...);
+      set_size_internal(s + 1);
+    } else {
+      EmplaceBackSlow(std::forward<Args>(args)...);
+    }
+  }
+
+  // Append t to the vector.
+  // Increases size() by one.
+  // Amortized complexity: O(1)
+  // Worst-case complexity: O(size())
+  void push_back(const value_type& t) { emplace_back(t); }
+  void push_back(value_type&& t) { emplace_back(std::move(t)); }
+
+  inline void pop_back() {
+    DCHECK(!empty());
+    const size_t s = size();
+    Destroy(data() + s - 1, 1);
+    set_size_internal(s - 1);
+  }
+
+  // Resizes the vector to contain "n" elements.
+  // If "n" is smaller than the initial size, extra elements are destroyed.
+  // If "n" is larger than the initial size, enough copies of "elem"
+  // are appended to increase the size to "n". If "elem" is omitted,
+  // new elements are value-initialized.
+  void resize(size_t n) { Resize<ValueInit>(n, nullptr); }
+  void resize(size_t n, const value_type& elem) { Resize<Fill>(n, &elem); }
+
+  iterator begin() { return data(); }
+  const_iterator begin() const { return data(); }
+
+  iterator end() { return data() + size(); }
+  const_iterator end() const { return data() + size(); }
+
+  iterator insert(iterator pos, const value_type& v);
+
+  iterator erase(iterator pos) {
+    DCHECK_LT(pos, end());
+    DCHECK_GE(pos, begin());
+    std::copy(pos + 1, end(), pos);
+    pop_back();
+    return pos;
+  }
+
+  iterator erase(iterator first, iterator last);
+
+  // Enlarges the underlying representation so it can hold at least
+  // "n" elements without reallocation.
+  // Does not change size() or the actual contents of the vector.
+  void reserve(size_t n) {
+    if (n > capacity()) {
+      // Make room for new elements
+      Grow<Move>(n);
+    }
+  }
+
+  // Swap the contents of *this with other.
+  // REQUIRES: value_type is swappable and copyable.
+  void swap(InlinedVector& other);
+
+ private:
+  // Representation can either be inlined or out-of-line.
+  // In either case, at least sizeof(void*) + 8 bytes are available.
+  //
+  // Inlined:
+  //   Last byte holds the length.
+  //   First (length*sizeof(T)) bytes stores the elements.
+  // Outlined:
+  //   Last byte holds kSentinel.
+  //   Second-last byte holds lg(capacity)
+  //   Preceding 6 bytes hold size.
+  //   First sizeof(T*) bytes hold pointer.
+
+  // Compute rep size.
+  static const size_t kSizeUnaligned = N * sizeof(T) + 1;  // Room for tag
+  static const size_t kSize = ((kSizeUnaligned + 15) / 16) * 16;  // Align
+
+  // See how many fit T we can fit inside kSize, but no more than 254
+  // since 255 is used as sentinel tag for out-of-line allocation.
+  static const unsigned int kSentinel = 255;
+  static const size_t kFit1 = (kSize - 1) / sizeof(T);
+  static const size_t kFit = (kFit1 >= kSentinel) ? (kSentinel - 1) : kFit1;
+
+  union {
+    unsigned char data[kSize];
+    // Force data to be aligned enough for a pointer.
+    T* unused_aligner;
+  } u_;
+
+  inline void InitRep() { u_.data[kSize - 1] = 0; }
+  inline bool is_inline() const { return u_.data[kSize - 1] != kSentinel; }
+
+  inline T* outofline_pointer() const {
+    T* ptr;
+    memcpy(&ptr, &u_.data[0], sizeof(ptr));
+    return ptr;
+  }
+
+  inline void set_outofline_pointer(T* p) {
+    memcpy(&u_.data[0], &p, sizeof(p));
+  }
+
+  inline uint64_t outofline_word() const {
+    uint64_t word;
+    memcpy(&word, &u_.data[kSize - 8], sizeof(word));
+    return word;
+  }
+
+  inline void set_outofline_word(uint64_t w) {
+    memcpy(&u_.data[kSize - 8], &w, sizeof(w));
+  }
+
+  inline size_t size_internal() const {
+    uint8_t s = static_cast<uint8_t>(u_.data[kSize - 1]);
+    if (s != kSentinel) {
+      return static_cast<size_t>(s);
+    } else {
+      const uint64_t word = outofline_word();
+      // The sentinel and capacity bits are most-significant bits in word.
+      return static_cast<size_t>(word & 0xffffffffffffull);
+    }
+  }
+
+  void set_size_internal(size_t n) {
+    if (is_inline()) {
+      DCHECK_LT(n, kSentinel);
+      u_.data[kSize - 1] = static_cast<unsigned char>(n);
+    } else {
+      uint64_t word;
+      // The sentinel and capacity bits are most-significant bits in word.
+      word = (static_cast<uint64_t>(n) |
+              (static_cast<uint64_t>(u_.data[kSize - 2]) << 48) |
+              (static_cast<uint64_t>(kSentinel) << 56));
+      set_outofline_word(word);
+      DCHECK_EQ(u_.data[kSize - 1], kSentinel) << n;
+    }
+  }
+
+  void DiscardStorage() {
+    T* base = data();
+    size_t n = size();
+    Destroy(base, n);
+    if (!is_inline()) {
+      free(base);
+    }
+  }
+
+  template <typename... Args>
+  void EmplaceBackSlow(Args&&... args) {
+    const size_t s = size();
+    DCHECK_EQ(s, capacity());
+    Grow<Move, Construct>(s + 1, std::forward<Args>(args)...);
+    set_size_internal(s + 1);
+  }
+
+  // Movers for Grow
+  // Does nothing.
+  static void Nop(T* src, size_t n, T* dst) {}
+
+  // Moves srcs[0,n-1] contents to dst[0,n-1].
+  static void Move(T* src, size_t n, T* dst) {
+    for (size_t i = 0; i < n; i++) {
+      new (dst + i) T(std::move(*(src + i)));
+    }
+  }
+
+  // Initializers for Resize.
+  // Initializes dst[0,n-1] with empty constructor.
+  static void ValueInit(const T*, size_t n, T* dst) {
+    for (size_t i = 0; i < n; i++) {
+      new (dst + i) T();
+    }
+  }
+
+  // Initializes dst[0,n-1] with copies of *src.
+  static void Fill(const T* src, size_t n, T* dst) {
+    for (size_t i = 0; i < n; i++) {
+      new (dst + i) T(*src);
+    }
+  }
+
+  void Destroy(T* src, int n) {
+    if (!std::is_trivially_destructible<T>::value) {
+      for (int i = 0; i < n; i++) {
+        (src + i)->~T();
+      }
+    }
+  }
+
+  // Initialization methods for Grow.
+  // 1) Leave uninitialized memory.
+  struct Uninitialized {
+    void operator()(T*) const {}
+  };
+  // 2) Construct a T with args at not-yet-initialized memory pointed by dst.
+  struct Construct {
+    template<class... Args>
+    void operator()(T* dst, Args&&... args) const {
+      new (dst) T(std::forward<Args>(args)...);
+    }
+  };
+
+  // Grow so that capacity >= n.  Uses Mover to move existing elements
+  // to new buffer, and possibly initialize the new element according
+  // to InitType.
+  // We pass the InitType and Mover as template arguments so that
+  // this code compiles even if T does not support copying or default
+  // construction.
+  template <void(Mover)(T*, size_t, T*), class InitType = Uninitialized,
+            class... Args>
+  void Grow(size_t n, Args&&... args) {
+    size_t s = size();
+    DCHECK_LE(s, capacity());
+
+    // Compute new capacity by repeatedly doubling current capacity
+    size_t target = 1;
+    size_t target_lg = 0;
+    while (target < kFit || target < n) {
+      target_lg++;
+      target <<= 1;
+    }
+
+    T* src = data();
+    T* dst = static_cast<T*>(malloc(target * sizeof(T)));
+
+    // Need to copy elem before discarding src since it might alias src.
+    InitType{}(dst + s, std::forward<Args>(args)...);
+    Mover(src, s, dst);
+    DiscardStorage();
+
+    u_.data[kSize - 1] = kSentinel;
+    u_.data[kSize - 2] = static_cast<unsigned char>(target_lg);
+    set_size_internal(s);
+    DCHECK_EQ(capacity(), target);
+    set_outofline_pointer(dst);
+  }
+
+  // Resize to size n.  Any new elements are initialized by passing
+  // elem and the destination to Initializer.  We pass the Initializer
+  // as a template argument so that this code compiles even if T does
+  // not support copying.
+  template <void(Initializer)(const T*, size_t, T*)>
+  void Resize(size_t n, const T* elem) {
+    size_t s = size();
+    if (n <= s) {
+      Destroy(data() + n, s - n);
+      set_size_internal(n);
+      return;
+    }
+    reserve(n);
+    DCHECK_GE(capacity(), n);
+    set_size_internal(n);
+    Initializer(elem, n - s, data() + s);
+  }
+
+  template <typename Iter>
+  void AppendRange(Iter first, Iter last, std::input_iterator_tag);
+
+  // Faster path for forward iterators.
+  template <typename Iter>
+  void AppendRange(Iter first, Iter last, std::forward_iterator_tag);
+
+  template <typename Iter>
+  void AppendRange(Iter first, Iter last);
+};
+
+// Provide linkage for constants.
+template <typename T, int N>
+const size_t InlinedVector<T, N>::kSizeUnaligned;
+template <typename T, int N>
+const size_t InlinedVector<T, N>::kSize;
+template <typename T, int N>
+const unsigned int InlinedVector<T, N>::kSentinel;
+template <typename T, int N>
+const size_t InlinedVector<T, N>::kFit1;
+template <typename T, int N>
+const size_t InlinedVector<T, N>::kFit;
+
+template <typename T, int N>
+inline void swap(InlinedVector<T, N>& a, InlinedVector<T, N>& b) {
+  a.swap(b);
+}
+
+template <typename T, int N>
+inline bool operator==(const InlinedVector<T, N>& a,
+                       const InlinedVector<T, N>& b) {
+  return a.size() == b.size() && std::equal(a.begin(), a.end(), b.begin());
+}
+
+template <typename T, int N>
+inline bool operator!=(const InlinedVector<T, N>& a,
+                       const InlinedVector<T, N>& b) {
+  return !(a == b);
+}
+
+template <typename T, int N>
+inline bool operator<(const InlinedVector<T, N>& a,
+                      const InlinedVector<T, N>& b) {
+  return std::lexicographical_compare(a.begin(), a.end(), b.begin(), b.end());
+}
+
+template <typename T, int N>
+inline bool operator>(const InlinedVector<T, N>& a,
+                      const InlinedVector<T, N>& b) {
+  return b < a;
+}
+
+template <typename T, int N>
+inline bool operator<=(const InlinedVector<T, N>& a,
+                       const InlinedVector<T, N>& b) {
+  return !(b < a);
+}
+
+template <typename T, int N>
+inline bool operator>=(const InlinedVector<T, N>& a,
+                       const InlinedVector<T, N>& b) {
+  return !(a < b);
+}
+
+// ========================================
+// Implementation
+
+template <typename T, int N>
+inline InlinedVector<T, N>::InlinedVector() {
+  InitRep();
+}
+
+template <typename T, int N>
+inline InlinedVector<T, N>::InlinedVector(size_t n) {
+  InitRep();
+  if (n > capacity()) {
+    Grow<Nop>(n);  // Must use Nop in case T is not copyable
+  }
+  set_size_internal(n);
+  ValueInit(nullptr, n, data());
+}
+
+template <typename T, int N>
+inline InlinedVector<T, N>::InlinedVector(size_t n, const value_type& elem) {
+  InitRep();
+  if (n > capacity()) {
+    Grow<Nop>(n);  // Can use Nop since we know we have nothing to copy
+  }
+  set_size_internal(n);
+  Fill(&elem, n, data());
+}
+
+template <typename T, int N>
+inline InlinedVector<T, N>::InlinedVector(const InlinedVector& v) {
+  InitRep();
+  *this = v;
+}
+
+template <typename T, int N>
+typename InlinedVector<T, N>::iterator InlinedVector<T, N>::insert(
+    iterator pos, const value_type& v) {
+  DCHECK_GE(pos, begin());
+  DCHECK_LE(pos, end());
+  if (pos == end()) {
+    push_back(v);
+    return end() - 1;
+  }
+  size_t s = size();
+  size_t idx = std::distance(begin(), pos);
+  if (s == capacity()) {
+    Grow<Move>(s + 1);
+  }
+  CHECK_LT(s, capacity());
+  pos = begin() + idx;  // Reset 'pos' into a post-enlarge iterator.
+  Fill(data() + s - 1, 1, data() + s);  // data[s] = data[s-1]
+  std::copy_backward(pos, data() + s - 1, data() + s);
+  *pos = v;
+
+  set_size_internal(s + 1);
+  return pos;
+}
+
+template <typename T, int N>
+typename InlinedVector<T, N>::iterator InlinedVector<T, N>::erase(
+    iterator first, iterator last) {
+  DCHECK_LE(begin(), first);
+  DCHECK_LE(first, last);
+  DCHECK_LE(last, end());
+
+  size_t s = size();
+  ptrdiff_t erase_gap = std::distance(first, last);
+  std::copy(last, data() + s, first);
+  Destroy(data() + s - erase_gap, erase_gap);
+  set_size_internal(s - erase_gap);
+  return first;
+}
+
+template <typename T, int N>
+void InlinedVector<T, N>::swap(InlinedVector& other) {
+  using std::swap;  // Augment ADL with std::swap.
+  if (&other == this) {
+    return;
+  }
+
+  InlinedVector* a = this;
+  InlinedVector* b = &other;
+
+  const bool a_inline = a->is_inline();
+  const bool b_inline = b->is_inline();
+
+  if (!a_inline && !b_inline) {
+    // Just swap the top-level representations.
+    T* aptr = a->outofline_pointer();
+    T* bptr = b->outofline_pointer();
+    a->set_outofline_pointer(bptr);
+    b->set_outofline_pointer(aptr);
+
+    uint64_t aword = a->outofline_word();
+    uint64_t bword = b->outofline_word();
+    a->set_outofline_word(bword);
+    b->set_outofline_word(aword);
+    return;
+  }
+
+  // Make a the larger of the two to reduce number of cases.
+  size_t a_size = a->size();
+  size_t b_size = b->size();
+  if (a->size() < b->size()) {
+    swap(a, b);
+    swap(a_size, b_size);
+  }
+  DCHECK_GE(a_size, b_size);
+
+  if (b->capacity() < a_size) {
+    b->Grow<Move>(a_size);
+  }
+
+  // One is inline and one is not.
+  // 'a' is larger. Swap the elements up to the smaller array size.
+  std::swap_ranges(a->data(), a->data() + b_size, b->data());
+  std::uninitialized_copy(a->data() + b_size, a->data() + a_size,
+                          b->data() + b_size);
+  Destroy(a->data() + b_size, a_size - b_size);
+  a->set_size_internal(b_size);
+  b->set_size_internal(a_size);
+  DCHECK_EQ(b->size(), a_size);
+  DCHECK_EQ(a->size(), b_size);
+}
+
+template <typename T, int N>
+template <typename Iter>
+inline void InlinedVector<T, N>::AppendRange(Iter first, Iter last,
+                                             std::input_iterator_tag) {
+  std::copy(first, last, std::back_inserter(*this));
+}
+
+template <typename T, int N>
+template <typename Iter>
+inline void InlinedVector<T, N>::AppendRange(Iter first, Iter last,
+                                             std::forward_iterator_tag) {
+  typedef typename std::iterator_traits<Iter>::difference_type Length;
+  Length length = std::distance(first, last);
+  size_t s = size();
+  reserve(s + length);
+  std::uninitialized_copy_n(first, length, data() + s);
+  set_size_internal(s + length);
+}
+
+template <typename T, int N>
+template <typename Iter>
+inline void InlinedVector<T, N>::AppendRange(Iter first, Iter last) {
+  typedef typename std::iterator_traits<Iter>::iterator_category IterTag;
+  AppendRange(first, last, IterTag());
+}
+
+}  // namespace gtl
+
+#endif  // OR_TOOLS_BASE_INLINED_VECTOR_H_

ortools/base/span.h

@@ -0,0 +1,542 @@
+// Copyright 2010-2014 Google
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#ifndef OR_TOOLS_BASE_SPAN_H_
+#define OR_TOOLS_BASE_SPAN_H_
+
+// An Span<T> represents an immutable array of elements of type
+// T.  It has a length "length", and a base pointer "ptr", and the
+// array it represents contains the elements "ptr[0] .. ptr[len-1]".
+// The backing store for the array is *not* owned by the Span
+// object, and clients must arrange for the backing store to remain
+// live while the Span object is in use.
+//
+// An Span<T> is somewhat analogous to a StringPiece, but for
+// array elements of type T.
+//
+// Implicit conversion operations are provided from types such as
+// std::vector<T> and util::gtl::InlinedVector<T, N>.  Note that Span
+// objects constructed from types in this way may be invalidated by
+// any operations that mutate the underlying vector.
+//
+// One common use for Span is when passing arguments to a
+// routine where you want to be able to accept a variety of array
+// types (e.g. a vector, a util::gtl::InlinedVector, a C-style array,
+// etc.).  The usual approach here is to have the client explicitly
+// pass in a pointer and a length, as in:
+//
+//   void MyRoutine(const int* elems, int N) {
+//     for (int i = 0; i < N; i++) { .. do something with elems[i] .. }
+//   }
+//
+// Unfortunately, this leads to ugly and error-prone code at the call site:
+//
+//   std::vector<int> my_vector;
+//   MyRoutine(vector_as_array(&my_vector), my_vector.size());
+//
+//   util::gtl::InlinedVector<int, 4> my_inline_vector;
+//   MyRoutine(my_inline_vector.array(), my_inline_vector.size());
+//
+//   int my_array[10];
+//   MyRoutine(my_array, 10);
+//
+// Instead, you can use an Span as the argument to the routine:
+//
+//   void MyRoutine(Span<int> a) {
+//     for (int i = 0; i < a.size(); i++) { .. do something with a[i] .. }
+//   }
+//
+// This makes the call sites cleaner, for the most part:
+//
+//   std::vector<int> my_vector;
+//   MyRoutine(my_vector);
+//
+//   util::gtl::InlinedVector<int, 4> my_inline_vector;
+//   MyRoutine(my_inline_vector);
+//
+//   int my_array[10];
+//   MyRoutine(my_array);
+//
+//   int* my_array = new int[10];
+//   MyRoutine(gtl::Span<int>(my_array, 10));
+//
+// MutableSpan<T> represents a mutable array of elements, and, like
+// Span, does not own the backing store. The implicit constructors it
+// provides allow functions not to worry about whether their mutable arguments
+// refer to vectors, arrays, google::protobuf::RepeatedFields, etc.:
+//
+//   void MyMutatingRoutine(MutableSpan<int> a) {
+//     for (int i = 0; i < a.size(); i++) { .. mutate a[i] .. }
+//   }
+//
+//   std::vector<int> my_vector;
+//   MyMutatingRoutine(&my_vector);
+//
+//   int my_array[10];
+//   MyMutatingRoutine(my_array);
+//
+//   int* my_array = new int[10];
+//   MyMutatingRoutine(gtl::MutableSpan<int>(my_array, 10));
+//
+//   MyProto my_proto;
+//   for (int i = 0; i < 10; ++i) { my_proto.add_value(i); }
+//   MyMutatingRoutine(my_proto.mutable_value());
+
+#include <initializer_list>
+#include <memory>
+#include <type_traits>
+#include <vector>
+
+#include "ortools/base/inlined_vector.h"
+
+namespace gtl {
+
+namespace array_slice_internal {
+
+// Template logic for generic constructors.
+
+// Wrappers whose Get() delegates to the appropriate method of a container, and
+// is defined when this method exists. Delegates to the const method if C is a
+// const type.
+struct Data {
+  template <typename C>
+  static decltype(std::declval<C>().data()) Get(C* v) {
+    return v->data();
+  }
+};
+
+struct MutableData {
+  template <typename C>
+  static decltype(std::declval<C>().mutable_data()) Get(C* v) {
+    return v->mutable_data();
+  }
+};
+
+struct Size {
+  template <typename C>
+  static decltype(std::declval<C>().size()) Get(C* v) {
+    return v->size();
+  }
+};
+
+struct MutableStringData {
+  // Defined only for std::string.
+  static char* Get(std::string* v) { return v->empty() ? nullptr : &*v->begin(); }
+};
+
+// Checks whether M::Get(C*) is defined and has a return type R such that
+// Checker::valid<R>()==true.
+template <typename M, typename Checker, typename C>
+struct HasGetHelper : public M {
+ private:
+  struct None {};
+  // M::Get is selected when it is viable. Get(...) is selected otherwise.
+  using M::Get;
+  static None Get(...);
+
+ public:
+  static constexpr bool HasGet() {
+    using Result = decltype(Get(std::declval<C*>()));
+    return !std::is_same<Result, None>() && Checker::template valid<Result>();
+  }
+};
+
+// Defines HasGet() for a particular method, container, and checker. If
+// HasGet()==true, provides Get() that delegates to the method.
+template <typename M, typename Checker, typename C,
+          bool /*has_get*/ = HasGetHelper<M, Checker, C>::HasGet()>
+struct Wrapper {
+  static constexpr bool HasGet() { return false; }
+};
+
+template <typename M, typename Checker, typename C>
+struct Wrapper<M, Checker, C, true> {
+  static constexpr bool HasGet() { return true; }
+  static decltype(M::Get(std::declval<C*>())) Get(C* v) { return M::Get(v); }
+};
+
+// Type checker for a method returning an integral value.
+struct SizeChecker {
+  template <typename R>
+  static constexpr bool valid() {
+    return std::is_integral<R>::value;
+  }
+};
+
+// Type checker for a method returning either a pointer to T or a less const
+// version of that.
+template <typename T>
+struct DataChecker {
+  // We want to enable conversion from std::vector<T*> to Span<const T*>
+  // but
+  // disable conversion from std::vector<Derived> to Span<Base>. Here we
+  // use
+  // the fact that U** is convertible to Q* const* if and only if Q is the same
+  // type or a more cv-qualified version of U.
+  template <typename R>
+  static constexpr bool valid() {
+    return std::is_convertible<R*, T* const*>::value;
+  }
+};
+
+// Aliases to A if A::HasGet()==true, or to B otherwise.
+template <typename A, typename B>
+using FirstWithGet = typename std::conditional<A::HasGet(), A, B>::type;
+
+// Wraps C::data() const, returning a pointer to const data.
+template <typename T, typename C>
+using ContainerData = Wrapper<Data, DataChecker<const T>, const C>;
+
+// Wraps a method returning a pointer to mutable data. Prefers data() over
+// mutable_data(), and handles strings when T==char. If data() returns a pointer
+// to mutable data, it is most likely overloaded, but may also be a single
+// method 'T* C::data() const' in a non-STL-compliant container.
+template <typename T, typename C>
+using ContainerMutableData =
+    FirstWithGet<Wrapper<Data, DataChecker<T>, C>,
+                 FirstWithGet<Wrapper<MutableData, DataChecker<T>, C>,
+                              Wrapper<MutableStringData, DataChecker<T>, C>>>;
+
+// Wraps C::size() const.
+template <typename C>
+using ContainerSize = Wrapper<Size, SizeChecker, const C>;
+
+// Implementation class for Span and MutableSpan. In the case of
+// Span, T will be a const type; for MutableSpan, T will be a
+// mutable type.
+template <typename T>
+class SpanImplBase {
+ public:
+  typedef T* pointer;
+  typedef const T* const_pointer;
+  typedef T& reference;
+  typedef const T& const_reference;
+  typedef pointer iterator;
+  typedef const_pointer const_iterator;
+  typedef std::reverse_iterator<iterator> reverse_iterator;
+  typedef std::reverse_iterator<const_iterator> const_reverse_iterator;
+  typedef size_t size_type;
+  typedef ptrdiff_t difference_type;
+
+  static const size_type npos = static_cast<size_type>(-1);
+
+  SpanImplBase(pointer array, size_type length)
+      : ptr_(array), length_(length) {}
+
+  // Substring of another Span.
+  // pos must be non-negative and <= x.length().
+  // len must be non-negative and will be pinned to at most x.length() - pos.
+  SpanImplBase(const SpanImplBase& x, size_type pos, size_type len)
+      : ptr_(x.ptr_ + pos), length_(std::min(x.length_ - pos, len)) {}
+
+  // Some of the const methods below return pointers and references to mutable
+  // data. This is only the case in this internal class; Span and
+  // MutableSpan provide deep-constness.
+
+  pointer data() const { return ptr_; }
+  size_type size() const { return length_; }
+
+  void clear() {
+    ptr_ = nullptr;
+    length_ = 0;
+  }
+
+  reference operator[](size_type i) const { return ptr_[i]; }
+  reference at(size_type i) const {
+    DCHECK_LT(i, length_);
+    return ptr_[i];
+  }
+  reference front() const {
+    DCHECK_GT(length_, 0);
+    return ptr_[0];
+  }
+  reference back() const {
+    DCHECK_GT(length_, 0);
+    return ptr_[length_ - 1];
+  }
+
+  void remove_prefix(size_type n) {
+    DCHECK_GE(length_, n);
+    ptr_ += n;
+    length_ -= n;
+  }
+  void remove_suffix(size_type n) {
+    DCHECK_GE(length_, n);
+    length_ -= n;
+  }
+
+  iterator begin() const { return ptr_; }
+  iterator end() const { return ptr_ + length_; }
+  reverse_iterator rbegin() const { return reverse_iterator(end()); }
+  reverse_iterator rend() const { return reverse_iterator(begin()); }
+
+  bool operator==(const SpanImplBase& other) const {
+    if (size() != other.size()) return false;
+    if (data() == other.data()) return true;
+    return std::equal(data(), data() + size(), other.data());
+  }
+  bool operator!=(const SpanImplBase& other) const {
+    return !(*this == other);
+  }
+
+ private:
+  pointer ptr_;
+  size_type length_;
+};
+
+template <typename T>
+class SpanImpl : public SpanImplBase<const T> {
+ public:
+  using SpanImplBase<const T>::SpanImplBase;
+
+  // Defined iff the data and size accessors for the container C have been
+  // defined.
+  template <typename C>
+  using EnableIfConvertibleFrom =
+      typename std::enable_if<ContainerData<T, C>::HasGet() &&
+                              ContainerSize<C>::HasGet()>::type;
+
+  // Constructs from a container when EnableIfConvertibleFrom is
+  // defined. std::addressof handles types with overloaded operator&.
+  template <typename C>
+  explicit SpanImpl(const C& v)
+      : SpanImplBase<const T>(ContainerData<T, C>::Get(std::addressof(v)),
+                                    ContainerSize<C>::Get(std::addressof(v))) {}
+};
+
+template <typename T>
+class MutableSpanImpl : public SpanImplBase<T> {
+ public:
+  using SpanImplBase<T>::SpanImplBase;
+
+  template <typename C>
+  using EnableIfConvertibleFrom =
+      typename std::enable_if<ContainerMutableData<T, C>::HasGet() &&
+                              ContainerSize<C>::HasGet()>::type;
+
+  template <typename C>
+  explicit MutableSpanImpl(C* v)
+      : SpanImplBase<T>(ContainerMutableData<T, C>::Get(v),
+                              ContainerSize<C>::Get(v)) {}
+};
+
+}  // namespace array_slice_internal
+
+
+template <typename T>
+class Span {
+ private:
+  typedef array_slice_internal::SpanImpl<T> Impl;
+
+ public:
+  typedef T value_type;
+  typedef typename Impl::pointer pointer;
+  typedef typename Impl::const_pointer const_pointer;
+  typedef typename Impl::reference reference;
+  typedef typename Impl::const_reference const_reference;
+  typedef typename Impl::iterator iterator;
+  typedef typename Impl::const_iterator const_iterator;
+  typedef typename Impl::reverse_iterator reverse_iterator;
+  typedef typename Impl::const_reverse_iterator const_reverse_iterator;
+  typedef typename Impl::size_type size_type;
+  typedef typename Impl::difference_type difference_type;
+
+  static const size_type npos = Impl::npos;
+
+  Span() : impl_(nullptr, 0) {}
+  Span(const_pointer array, size_type length) : impl_(array, length) {}
+
+  // Implicit conversion constructors
+  Span(const std::vector<value_type>& v)  // NOLINT(runtime/explicit)
+      : impl_(v.data(), v.size()) {}
+
+  template <size_t N>
+  Span(const value_type (&a)[N])  // NOLINT(runtime/explicit)
+      : impl_(a, N) {}
+
+  template <int N>
+  Span(const InlinedVector<value_type, N>& v)  // NOLINT(runtime/explicit)
+      : impl_(v.data(), v.size()) {}
+
+  // The constructor for any class supplying 'data() const' that returns either
+  // const T* or a less const-qualified version of it, and 'some_integral_type
+  // size() const'. google::protobuf::RepeatedField<T>, std::string and (since C++11)
+  // std::vector<T,A> and std::array<T, N> are examples of this. See
+  // array_slice_internal.h for details.
+  template <typename V,
+            typename = typename Impl::template EnableIfConvertibleFrom<V>>
+  Span(const V& v)  // NOLINT(runtime/explicit)
+      : impl_(v) {}
+
+  // Implicitly constructs an Span from an initializer list. This makes it
+  // possible to pass a brace-enclosed initializer list to a function expecting
+  // an Span:
+  //   void Process(Span<int> x);
+  //   Process({1, 2, 3});
+  // The data referenced by the initializer_list must outlive this
+  // Span. For example, "Span<int> s={1,2};" and "return
+  // Span<int>({3,4});" are errors, as the resulting Span may
+  // reference data that is no longer valid.
+  Span(std::initializer_list<value_type> v)  // NOLINT(runtime/explicit)
+      : impl_(v.begin(), v.size()) {}
+
+  // Substring of another Span.
+  // pos must be non-negative and <= x.length().
+  // len must be non-negative and will be pinned to at most x.length() - pos.
+  // If len==npos, the substring continues till the end of x.
+  Span(const Span& x, size_type pos, size_type len)
+      : impl_(x.impl_, pos, len) {}
+
+  const_pointer data() const { return impl_.data(); }
+  size_type size() const { return impl_.size(); }
+  size_type length() const { return size(); }
+  bool empty() const { return size() == 0; }
+
+  void clear() { impl_.clear(); }
+
+  const_reference operator[](size_type i) const { return impl_[i]; }
+  const_reference at(size_type i) const { return impl_.at(i); }
+  const_reference front() const { return impl_.front(); }
+  const_reference back() const { return impl_.back(); }
+
+  const_iterator begin() const { return impl_.begin(); }
+  const_iterator end() const { return impl_.end(); }
+  const_reverse_iterator rbegin() const { return impl_.rbegin(); }
+  const_reverse_iterator rend() const { return impl_.rend(); }
+
+  void remove_prefix(size_type n) { impl_.remove_prefix(n); }
+  void remove_suffix(size_type n) { impl_.remove_suffix(n); }
+  void pop_back() { remove_suffix(1); }
+  void pop_front() { remove_prefix(1); }
+
+  // These relational operators have the same semantics as the
+  // std::vector<T> relational operators: they do deep (elementwise)
+  // comparisons.  Array slices are equal iff their size is the same
+  // and all their elements are equal.
+  bool operator==(Span<T> other) const { return impl_ == other.impl_; }
+  bool operator!=(Span<T> other) const { return impl_ != other.impl_; }
+
+ private:
+  Impl impl_;
+};
+
+// Mutable version of Span, which allows the clients to mutate the
+// underlying data. It is implicitly convertible to Span since it provides
+// the data() and size() methods with correct signatures. When a
+// MutableSpan is created from a pointer to a container (as opposed to raw
+// memory pointer), the pointer must not be null.
+//
+// A note on const-ness: "mutable" here refers to the mutability of the
+// underlying data, not of the slice itself. It is perfectly reasonable to have
+// a variable of type "const MutableSpan<T>"; this means that the bounds
+// of the view on the array cannot be changed, but the underlying data in the
+// array still may be modified. This is akin to a "T* const" pointer, as opposed
+// to a "const T*" pointer (corresponding to a non-const Span<T>).
+template <typename T>
+class MutableSpan {
+ private:
+  typedef array_slice_internal::MutableSpanImpl<T> Impl;
+
+ public:
+  typedef T value_type;
+  typedef typename Impl::pointer pointer;
+  typedef typename Impl::const_pointer const_pointer;
+  typedef typename Impl::reference reference;
+  typedef typename Impl::const_reference const_reference;
+  typedef typename Impl::iterator iterator;
+  typedef typename Impl::const_iterator const_iterator;
+  typedef typename Impl::reverse_iterator reverse_iterator;
+  typedef typename Impl::const_reverse_iterator const_reverse_iterator;
+  typedef typename Impl::size_type size_type;
+  typedef typename Impl::difference_type difference_type;
+
+  static const size_type npos = Impl::npos;
+
+  MutableSpan() : impl_(nullptr, 0) {}
+  MutableSpan(pointer array, size_type length) : impl_(array, length) {}
+
+  // Implicit conversion constructors
+  MutableSpan(std::vector<value_type>* v)  // NOLINT(runtime/explicit)
+      : impl_(v->data(), v->size()) {}
+
+  template <size_t N>
+  MutableSpan(value_type (&a)[N])  // NOLINT(runtime/explicit)
+      : impl_(a, N) {}
+
+  template <int N>
+  MutableSpan(
+      InlinedVector<value_type, N>* v)  // NOLINT(runtime/explicit)
+      : impl_(v->data(), v->size()) {}
+
+  // The constructor for any class supplying 'T* data()' or 'T* mutable_data()'
+  // (the former is called if both exist), and 'some_integral_type size()
+  // const'. google::protobuf::RepeatedField is an example of this. Also supports std::string
+  // arguments, when T==char. The appropriate ctor is selected using SFINAE. See
+  // array_slice_internal.h for details.
+  template <typename V,
+            typename = typename Impl::template EnableIfConvertibleFrom<V>>
+  MutableSpan(V* v)  // NOLINT(runtime/explicit)
+      : impl_(v) {}
+
+  // Substring of another MutableSpan.
+  // pos must be non-negative and <= x.length().
+  // len must be non-negative and will be pinned to at most x.length() - pos.
+  // If len==npos, the substring continues till the end of x.
+  MutableSpan(const MutableSpan& x, size_type pos, size_type len)
+      : impl_(x.impl_, pos, len) {}
+
+  // Accessors.
+  pointer data() const { return impl_.data(); }
+  size_type size() const { return impl_.size(); }
+  size_type length() const { return size(); }
+  bool empty() const { return size() == 0; }
+
+  void clear() { impl_.clear(); }
+
+  reference operator[](size_type i) const { return impl_[i]; }
+  reference at(size_type i) const { return impl_.at(i); }
+  reference front() const { return impl_.front(); }
+  reference back() const { return impl_.back(); }
+
+  iterator begin() const { return impl_.begin(); }
+  iterator end() const { return impl_.end(); }
+  reverse_iterator rbegin() const { return impl_.rbegin(); }
+  reverse_iterator rend() const { return impl_.rend(); }
+
+  void remove_prefix(size_type n) { impl_.remove_prefix(n); }
+  void remove_suffix(size_type n) { impl_.remove_suffix(n); }
+  void pop_back() { remove_suffix(1); }
+  void pop_front() { remove_prefix(1); }
+
+  bool operator==(Span<T> other) const {
+    return Span<T>(*this) == other;
+  }
+  bool operator!=(Span<T> other) const {
+    return Span<T>(*this) != other;
+  }
+
+  // DEPRECATED(jacobsa): Please use data() instead.
+  pointer mutable_data() const { return impl_.data(); }
+
+ private:
+  Impl impl_;
+};
+
+template <typename T>
+const typename Span<T>::size_type Span<T>::npos;
+template <typename T>
+const typename MutableSpan<T>::size_type MutableSpan<T>::npos;
+
+}  // namespace gtl
+
+#endif  // OR_TOOLS_BASE_SPAN_H_

ortools/linear_solver/linear_solver.cc

@@ -1606,3 +1606,4 @@ int MPSolverParameters::GetIntegerParam(MPSolverParameters::IntegerParam param)
 
 
 }  // namespace operations_research
+

ortools/sat/clause.cc

@@ -172,7 +172,8 @@ bool LiteralWatchers::Propagate(Trail* trail) {
   return true;
 }
 
-ClauseRef LiteralWatchers::Reason(const Trail& trail, int trail_index) const {
+gtl::Span<Literal> LiteralWatchers::Reason(const Trail& trail,
+                                                  int trail_index) const {
   return reasons_[trail_index]->PropagationReason();
 }
 
@@ -311,10 +312,9 @@ bool BinaryImplicationGraph::Propagate(Trail* trail) {
   return true;
 }
 
-ClauseRef BinaryImplicationGraph::Reason(const Trail& trail,
-                                         int trail_index) const {
-  const Literal* p = &reasons_[trail_index];
-  return ClauseRef(p, p + 1);
+gtl::Span<Literal> BinaryImplicationGraph::Reason(
+    const Trail& trail, int trail_index) const {
+  return {&reasons_[trail_index], 1};
 }
 
 // Here, we remove all the literal whose negation are implied by the negation of

ortools/sat/clause.h

@@ -28,9 +28,11 @@
 #include "ortools/base/logging.h"
 #include "ortools/base/stringprintf.h"
 #include "ortools/base/timer.h"
+#include "ortools/base/inlined_vector.h"
 #include "ortools/base/int_type.h"
 #include "ortools/base/int_type_indexed_vector.h"
 #include "ortools/base/hash.h"
+#include "ortools/base/span.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_parameters.pb.h"
 #include "ortools/util/bitset.h"
@@ -94,9 +96,9 @@ class SatClause {
 
   // Returns the reason for the last unit propagation of this clause. The
   // preconditions are the same as for PropagatedLiteral().
-  ClauseRef PropagationReason() const {
+  gtl::Span<Literal> PropagationReason() const {
     // Note that we don't need to include the propagated literal.
-    return ClauseRef(&(literals_[1]), end());
+    return gtl::Span<Literal>(&(literals_[1]), size_ - 1);
   }
 
   // Removes literals that are fixed. This should only be called at level 0
@@ -164,7 +166,8 @@ class LiteralWatchers : public SatPropagator {
   ~LiteralWatchers() override;
 
   bool Propagate(Trail* trail) final;
-  ClauseRef Reason(const Trail& trail, int trail_index) const final;
+  gtl::Span<Literal> Reason(const Trail& trail,
+                                   int trail_index) const final;
 
   // Resizes the data structure.
   void Resize(int num_variables);
@@ -344,7 +347,8 @@ class BinaryImplicationGraph : public SatPropagator {
   }
 
   bool Propagate(Trail* trail) final;
-  ClauseRef Reason(const Trail& trail, int trail_index) const final;
+  gtl::Span<Literal> Reason(const Trail& trail,
+                                   int trail_index) const final;
 
   // Resizes the data structure.
   void Resize(int num_variables);
@@ -431,7 +435,15 @@ class BinaryImplicationGraph : public SatPropagator {
 
   // This is indexed by the Index() of a literal. Each list stores the
   // literals that are implied if the index literal becomes true.
-  ITIVector<LiteralIndex, std::vector<Literal>> implications_;
+  //
+  // Using InlinedVector helps quite a bit because on many problems, a literal
+  // only implies a few others. Note that on a 64 bits computer we get exactly
+  // 6 inlined int32 elements without extra space, and the size of the inlined
+  // vector is 4 times 64 bits.
+  //
+  // TODO(user): We could be even more efficient since a size of int32 is enough
+  // for us and we could store in common the inlined/not-inlined size.
+  ITIVector<LiteralIndex, gtl::InlinedVector<Literal, 6>> implications_;
   int64 num_implications_;
 
   // Some stats.

ortools/sat/cp_model.proto

@@ -267,6 +267,17 @@ message DecisionStrategyProto {
     SELECT_UPPER_HALF = 3;
   }
   DomainReductionStrategy domain_reduction_strategy = 3;
+
+  // Advanced usage. Some of the variable listed above may have been transformed
+  // by the presolve so this is needed to properly follow the given selection
+  // strategy. Instead of using a value X from one of the variable listed here,
+  // we will use positive_coeff * X + offset instead.
+  message AffineTransformation {
+    int32 var = 1;
+    int64 offset = 2;
+    int64 positive_coeff = 3;
+  }
+  repeated AffineTransformation transformations = 4;
 }
 
 // A constraint programming problem.

ortools/sat/cp_model_checker.cc

@@ -451,9 +451,9 @@ bool SolutionIsFeasible(const CpModelProto& model,
   // Check that all values fall in the variable domains.
   for (int i = 0; i < model.variables_size(); ++i) {
     if (!DomainInProtoContains(model.variables(i), variable_values[i])) {
-      LOG(ERROR) << "Variable #" << i << " has value " << variable_values[i]
-                 << " which do not fall in its domain: "
-                 << model.variables(i).ShortDebugString();
+      VLOG(1) << "Variable #" << i << " has value " << variable_values[i]
+              << " which do not fall in its domain: "
+              << model.variables(i).ShortDebugString();
       return false;
     }
   }
@@ -531,8 +531,8 @@ bool SolutionIsFeasible(const CpModelProto& model,
         LOG(FATAL) << "Unuspported constraint: " << ConstraintCaseName(type);
     }
     if (!is_feasible) {
-      LOG(ERROR) << "Failing constraint #" << c << " : "
-                 << model.constraints(c).ShortDebugString();
+      VLOG(1) << "Failing constraint #" << c << " : "
+              << model.constraints(c).ShortDebugString();
       return false;
     }
   }

ortools/sat/cp_model_presolve.cc

@@ -1409,6 +1409,56 @@ void PresolveCpModel(const CpModelProto& initial_model,
     arg->add_domain(r.offset);
   }
 
+  // The strategy variable indices will be remapped in ApplyVariableMapping()
+  // but first we use the representative of the affine relations for the
+  // variables that are not present anymore.
+  //
+  // Note that we properly take into account the sign of the coefficient which
+  // will result in the same domain reduction strategy. Moreover, if the
+  // variable order is not CHOOSE_FIRST, then we also encode the associated
+  // affine transformation in order to preserve the order.
+  std::unordered_set<int> used_variables;
+  for (DecisionStrategyProto& strategy :
+       *presolved_model->mutable_search_strategy()) {
+    DecisionStrategyProto copy = strategy;
+    strategy.clear_variables();
+    for (const int ref : copy.variables()) {
+      const int var = PositiveRef(ref);
+
+      // Remove fixed variables.
+      if (context.domains[var].IsFixed()) continue;
+
+      // There is not point having a variable appear twice, so we only keep
+      // the first occurrence in the first strategy in which it occurs.
+      if (ContainsKey(used_variables, var)) continue;
+      used_variables.insert(var);
+
+      if (context.var_to_constraints[var].empty()) {
+        const AffineRelation::Relation r = context.GetAffineRelation(var);
+        if (!context.var_to_constraints[r.representative].empty()) {
+          const int rep = (r.coeff > 0) == RefIsPositive(ref)
+                              ? r.representative
+                              : NegatedRef(r.representative);
+          strategy.add_variables(rep);
+          if (strategy.variable_selection_strategy() !=
+              DecisionStrategyProto::CHOOSE_FIRST) {
+            DecisionStrategyProto::AffineTransformation* t =
+                strategy.add_transformations();
+            t->set_var(rep);
+            t->set_offset(r.offset);
+            t->set_positive_coeff(std::abs(r.coeff));
+          }
+        } else {
+          // TODO(user): this variable was removed entirely by the presolve (no
+          // equivalent variable present). We simply ignore it entirely which
+          // might result in a different search...
+        }
+      } else {
+        strategy.add_variables(ref);
+      }
+    }
+  }
+
   // Update the variables domain of the presolved_model.
   for (int i = 0; i < context.domains.size(); ++i) {
     context.domains[i].CopyToIntegerVariableProto(
@@ -1418,28 +1468,6 @@ void PresolveCpModel(const CpModelProto& initial_model,
   // Set the variables of the mapping_model.
   mapping_model->mutable_variables()->CopyFrom(presolved_model->variables());
 
-  // The strategy variable indices will be remapped in ApplyVariableMapping()
-  // but first we use the representative of the affine relations for the
-  // variables that are not present anymore.
-  for (DecisionStrategyProto& strategy :
-       *presolved_model->mutable_search_strategy()) {
-    DecisionStrategyProto copy = strategy;
-    strategy.clear_variables();
-    for (const int ref : copy.variables()) {
-      const int var = PositiveRef(ref);
-      if (context.var_to_constraints[var].empty()) {
-        const AffineRelation::Relation r = context.GetAffineRelation(var);
-        if (r.representative != var) {
-          strategy.add_variables((r.coeff == 1) == RefIsPositive(ref)
-                                     ? r.representative
-                                     : NegatedRef(r.representative));
-        }
-      } else {
-        strategy.add_variables(ref);
-      }
-    }
-  }
-
   // Remove all the unused variables from the presolved model.
   postsolve_mapping->clear();
   std::vector<int> mapping(presolved_model->variables_size(), -1);
@@ -1451,19 +1479,19 @@ void PresolveCpModel(const CpModelProto& initial_model,
   ApplyVariableMapping(mapping, presolved_model);
 
   // Stats and checks.
-  LOG(INFO) << "- " << context.affine_relations.NumRelations()
-            << " affine relations where detected. " << num_affine_relations
-            << " where kept.";
-  LOG(INFO) << "- " << context.var_equiv_relations.NumRelations()
-            << " variable equivalence relations where detected.";
+  VLOG(1) << "- " << context.affine_relations.NumRelations()
+          << " affine relations where detected. " << num_affine_relations
+          << " where kept.";
+  VLOG(1) << "- " << context.var_equiv_relations.NumRelations()
+          << " variable equivalence relations where detected.";
   std::map<std::string, int> sorted_rules(context.stats_by_rule_name.begin(),
                                      context.stats_by_rule_name.end());
   for (const auto& entry : sorted_rules) {
     if (entry.second == 1) {
-      LOG(INFO) << "- rule '" << entry.first << "' was applied 1 time.";
+      VLOG(1) << "- rule '" << entry.first << "' was applied 1 time.";
     } else {
-      LOG(INFO) << "- rule '" << entry.first << "' was applied " << entry.second
-                << " times.";
+      VLOG(1) << "- rule '" << entry.first << "' was applied " << entry.second
+              << " times.";
     }
   }
   CHECK_EQ("", ValidateCpModel(*presolved_model));
@@ -1502,6 +1530,16 @@ void ApplyVariableMapping(const std::vector<int>& mapping,
         strategy.add_variables(ref >= 0 ? image : NegatedRef(image));
       }
     }
+    strategy.clear_transformations();
+    for (const auto& transform : copy.transformations()) {
+      const int ref = transform.var();
+      const int image = mapping[PositiveRef(ref)];
+      if (image >= 0) {
+        auto* new_transform = strategy.add_transformations();
+        *new_transform = transform;
+        new_transform->set_var(ref >= 0 ? image : NegatedRef(image));
+      }
+    }
   }
 
   // Move the variable definitions.

ortools/sat/cp_model_solver.cc

@@ -518,8 +518,12 @@ std::string Summarize(const std::string& input) {
 
 std::string CpModelStats(const CpModelProto& model_proto) {
   std::map<ConstraintProto::ConstraintCase, int> num_constraints_by_type;
-  for (int c = 0; c < model_proto.constraints_size(); ++c) {
-    num_constraints_by_type[model_proto.constraints(c).constraint_case()]++;
+  std::map<ConstraintProto::ConstraintCase, int> num_reif_constraints_by_type;
+  for (const ConstraintProto& ct : model_proto.constraints()) {
+    num_constraints_by_type[ct.constraint_case()]++;
+    if (!ct.enforcement_literal().empty()) {
+      num_reif_constraints_by_type[ct.constraint_case()]++;
+    }
   }
   const VariableUsage usage = ComputeVariableUsage(model_proto);
 
@@ -583,7 +587,9 @@ std::string CpModelStats(const CpModelProto& model_proto) {
   std::vector<std::string> constraints;
   for (const auto entry : num_constraints_by_type) {
     constraints.push_back(
-        StrCat("#", ConstraintCaseName(entry.first), ": ", entry.second));
+        StrCat("#", ConstraintCaseName(entry.first), ": ", entry.second,
+                     " (", num_reif_constraints_by_type[entry.first],
+                     " with enforcement literal)"));
   }
   std::sort(constraints.begin(), constraints.end());
   StrAppend(&result, strings::Join(constraints, "\n"));
@@ -869,15 +875,19 @@ struct Strategy {
   DecisionStrategyProto::DomainReductionStrategy domain_strategy;
 };
 const std::function<LiteralIndex()> ConstructSearchStrategy(
+    const std::unordered_map<int, std::pair<int64, int64>>&
+        var_to_coeff_offset_pair,
     const std::vector<Strategy>& strategies, Model* model) {
   IntegerEncoder* const integer_encoder = model->GetOrCreate<IntegerEncoder>();
   IntegerTrail* const integer_trail = model->GetOrCreate<IntegerTrail>();
 
   // Note that we copy strategies to keep the return function validity
   // independently of the life of the passed vector.
-  return [integer_encoder, integer_trail, strategies]() {
+  return [integer_encoder, integer_trail, strategies,
+          var_to_coeff_offset_pair]() {
     for (const Strategy& strategy : strategies) {
       IntegerVariable candidate = kNoIntegerVariable;
+      IntegerValue candidate_value = kMaxIntegerValue;
       IntegerValue candidate_lb;
       IntegerValue candidate_ub;
 
@@ -888,35 +898,42 @@ const std::function<LiteralIndex()> ConstructSearchStrategy(
         const IntegerValue lb = integer_trail->LowerBound(var);
         const IntegerValue ub = integer_trail->UpperBound(var);
         if (lb == ub) continue;
-        bool select = false;
-        if (candidate == kNoIntegerVariable) {
-          select = true;
-        } else {
-          switch (strategy.var_strategy) {
-            case DecisionStrategyProto::CHOOSE_FIRST:
-              break;
-            case DecisionStrategyProto::CHOOSE_LOWEST_MIN:
-              select = lb < candidate_lb;
-              break;
-            case DecisionStrategyProto::CHOOSE_HIGHEST_MAX:
-              select = ub > candidate_ub;
-              break;
-            case DecisionStrategyProto::CHOOSE_MIN_DOMAIN_SIZE:
-              select = (ub - lb) < (candidate_ub - candidate_lb);
-              break;
-            case DecisionStrategyProto::CHOOSE_MAX_DOMAIN_SIZE:
-              select = (ub - lb) > (candidate_ub - candidate_lb);
-              break;
-            default:
-              LOG(FATAL) << "Unknown VariableSelectionStrategy "
-                         << strategy.var_strategy;
-          }
+        IntegerValue value(0);
+        IntegerValue coeff(1);
+        IntegerValue offset(0);
+        if (ContainsKey(var_to_coeff_offset_pair, var.value())) {
+          const auto coeff_offset =
+              FindOrDie(var_to_coeff_offset_pair, var.value());
+          coeff = coeff_offset.first;
+          offset = coeff_offset.second;
         }
-        if (select) {
+        DCHECK_GT(coeff, 0);
+        switch (strategy.var_strategy) {
+          case DecisionStrategyProto::CHOOSE_FIRST:
+            break;
+          case DecisionStrategyProto::CHOOSE_LOWEST_MIN:
+            value = coeff * lb + offset;
+            break;
+          case DecisionStrategyProto::CHOOSE_HIGHEST_MAX:
+            value = -(coeff * ub + offset);
+            break;
+          case DecisionStrategyProto::CHOOSE_MIN_DOMAIN_SIZE:
+            value = coeff * (ub - lb);
+            break;
+          case DecisionStrategyProto::CHOOSE_MAX_DOMAIN_SIZE:
+            value = -coeff * (ub - lb);
+            break;
+          default:
+            LOG(FATAL) << "Unknown VariableSelectionStrategy "
+                       << strategy.var_strategy;
+        }
+        if (value < candidate_value) {
           candidate = var;
           candidate_lb = lb;
           candidate_ub = ub;
+          candidate_value = value;
         }
+        if (strategy.var_strategy == DecisionStrategyProto::CHOOSE_FIRST) break;
       }
       if (candidate == kNoIntegerVariable) continue;
 
@@ -1046,16 +1063,16 @@ CpSolverResponse SolveCpModelWithoutPresolve(const CpModelProto& model_proto,
               << " Boolean variable(s): " << ct.DebugString();
     }
     if (model->GetOrCreate<SatSolver>()->IsModelUnsat()) {
-      LOG(INFO) << "UNSAT during extraction (after adding '"
-                << ConstraintCaseName(ct.constraint_case()) << "'). "
-                << ct.DebugString();
+      VLOG(1) << "UNSAT during extraction (after adding '"
+              << ConstraintCaseName(ct.constraint_case()) << "'). "
+              << ct.DebugString();
       break;
     }
   }
   if (!unsupported_types.empty()) {
-    LOG(INFO) << "There is unsuported constraints types in this model: ";
+    VLOG(1) << "There is unsuported constraints types in this model: ";
     for (const std::string& type : unsupported_types) {
-      LOG(INFO) << " - " << type;
+      VLOG(1) << " - " << type;
     }
     return response;
   }
@@ -1077,6 +1094,7 @@ CpSolverResponse SolveCpModelWithoutPresolve(const CpModelProto& model_proto,
     next_decision = FirstUnassignedVarAtItsMinHeuristic(decisions, model);
   } else {
     std::vector<Strategy> strategies;
+    std::unordered_map<int, std::pair<int64, int64>> var_to_coeff_offset_pair;
     for (const DecisionStrategyProto& proto : model_proto.search_strategy()) {
       strategies.push_back(Strategy());
       Strategy& strategy = strategies.back();
@@ -1085,8 +1103,16 @@ CpSolverResponse SolveCpModelWithoutPresolve(const CpModelProto& model_proto,
       }
       strategy.var_strategy = proto.variable_selection_strategy();
       strategy.domain_strategy = proto.domain_reduction_strategy();
+      for (const auto& tranform : proto.transformations()) {
+        const IntegerVariable var = m.Integer(tranform.var());
+        if (!ContainsKey(var_to_coeff_offset_pair, var.value())) {
+          var_to_coeff_offset_pair[var.value()] = {tranform.positive_coeff(),
+                                                   tranform.offset()};
+        }
+      }
     }
-    next_decision = ConstructSearchStrategy(strategies, model);
+    next_decision =
+        ConstructSearchStrategy(var_to_coeff_offset_pair, strategies, model);
   }
 
   // Solve.
@@ -1110,9 +1136,9 @@ CpSolverResponse SolveCpModelWithoutPresolve(const CpModelProto& model_proto,
           FillSolutionInResponse(model_proto, m, &response);
           response.set_objective_value(
               ScaleObjectiveValue(obj, sat_model.Get(Value(objective_var))));
-          LOG(INFO) << "Solution #" << num_solutions
-                    << " obj:" << response.objective_value() << " num_bool:"
-                    << sat_model.Get<SatSolver>()->NumVariables();
+          VLOG(1) << "Solution #" << num_solutions
+                  << " obj:" << response.objective_value()
+                  << " num_bool:" << sat_model.Get<SatSolver>()->NumVariables();
         };
 
     if (parameters.optimize_with_core()) {
@@ -1120,7 +1146,7 @@ CpSolverResponse SolveCpModelWithoutPresolve(const CpModelProto& model_proto,
       std::vector<IntegerValue> linear_coeffs;
       ExtractLinearObjective(model_proto, &m, &linear_vars, &linear_coeffs);
       status = MinimizeWithCoreAndLazyEncoding(
-          /*log_info=*/true, objective_var, linear_vars, linear_coeffs,
+          VLOG_IS_ON(1), objective_var, linear_vars, linear_coeffs,
           next_decision, solution_observer, model);
     } else {
       status = MinimizeIntegerVariableWithLinearScanAndLazyEncoding(
@@ -1184,7 +1210,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
   {
     const std::string error = ValidateCpModel(model_proto);
     if (!error.empty()) {
-      LOG(INFO) << error;
+      VLOG(1) << error;
       CpSolverResponse response;
       response.set_status(CpSolverStatus::MODEL_INVALID);
       return response;
@@ -1197,7 +1223,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
   PresolveCpModel(model_proto, &presolved_proto, &mapping_proto,
                   &postsolve_mapping);
 
-  LOG(INFO) << CpModelStats(presolved_proto);
+  VLOG(1) << CpModelStats(presolved_proto);
 
   CpSolverResponse response =
       SolveCpModelWithoutPresolve(presolved_proto, model);

ortools/sat/drat.cc

@@ -68,15 +68,18 @@ void DratWriter::AddOneVariable() {
   reverse_mapping_.push_back(BooleanVariable(variable_index_++));
 }
 
-void DratWriter::AddClause(ClauseRef clause) { WriteClause(clause); }
+void DratWriter::AddClause(gtl::Span<Literal> clause) {
+  WriteClause(clause);
+}
 
-void DratWriter::DeleteClause(ClauseRef clause, bool ignore_call) {
+void DratWriter::DeleteClause(gtl::Span<Literal> clause,
+                              bool ignore_call) {
   if (ignore_call) return;
   buffer_ += "d ";
   WriteClause(clause);
 }
 
-void DratWriter::WriteClause(ClauseRef clause) {
+void DratWriter::WriteClause(gtl::Span<Literal> clause) {
   values_.clear();
   for (const Literal l : clause) {
     CHECK_LT(l.Variable(), reverse_mapping_.size());

ortools/sat/drat.h

@@ -55,7 +55,7 @@ class DratWriter {
   // newer variables always comes first. This is needed because in the DRAT
   // format, the clause is checked for the RAT property with only its first
   // literal.
-  void AddClause(ClauseRef clause);
+  void AddClause(gtl::Span<Literal> clause);
 
   // Writes a "deletion" information about a clause that has been added before
   // to the DRAT output. Note that it is also possible to delete a clause from
@@ -70,10 +70,10 @@ class DratWriter {
   //
   // TODO(user): an alternative would be to call AddClause() on all the problem
   // clause first.
-  void DeleteClause(ClauseRef clause, bool ignore_call = true);
+  void DeleteClause(gtl::Span<Literal> clause, bool ignore_call = true);
 
  private:
-  void WriteClause(ClauseRef clause);
+  void WriteClause(gtl::Span<Literal> clause);
 
   // We need to keep track of the variable newly created.
   int variable_index_;

ortools/sat/integer.cc

@@ -103,6 +103,7 @@ void IntegerEncoder::FullyEncodeVariable(IntegerVariable i_var, IntegerValue lb,
   return FullyEncodeVariable(i_var, std::move(values));
 }
 
+// TODO(user): merge the common code with FullyEncodeVariable().
 void IntegerEncoder::FullyEncodeVariableUsingGivenLiterals(
     IntegerVariable i_var, const std::vector<Literal>& literals,
     const std::vector<IntegerValue>& values) {
@@ -119,6 +120,12 @@ void IntegerEncoder::FullyEncodeVariableUsingGivenLiterals(
   }
   std::sort(encoding.begin(), encoding.end());
 
+  // We need the <= 1 constraint, and the >= 1 part is cheap. Note that the
+  // solver will discard it if it is of size 2 and contains a literal and its
+  // negation.
+  CHECK(sat_solver_->AddLinearConstraint(true, sat::Coefficient(1), true,
+                                         sat::Coefficient(1), &cst));
+
   full_encoding_index_[i_var] = full_encoding_.size();
   full_encoding_.push_back(encoding);  // copy because we need it below.
 
@@ -252,7 +259,7 @@ bool IntegerTrail::Propagate(Trail* trail) {
   //  1/ See if new variables are fully encoded and initialize them.
   //  2/ In the loop below, each time a "min" variable was assigned to false,
   //     update the associated variable bounds, and change the watched "min".
-  //     This step is is O(num variables at false between the old and new min).
+  //     This step is in O(num variables at false between the old and new min).
   //
   // The data structure are reversible.
   watched_min_.SetLevel(trail->CurrentDecisionLevel());
@@ -493,8 +500,8 @@ int IntegerTrail::FindLowestTrailIndexThatExplainBound(
 
 bool IntegerTrail::EnqueueAssociatedLiteral(
     Literal literal, IntegerLiteral i_lit,
-    const std::vector<Literal>& literal_reason,
-    const std::vector<IntegerLiteral>& integer_reason,
+    gtl::Span<Literal> literal_reason,
+    gtl::Span<IntegerLiteral> integer_reason,
     BooleanVariable* variable_with_same_reason) {
   if (!trail_->Assignment().VariableIsAssigned(literal.Variable())) {
     if (integer_decision_levels_.empty()) {
@@ -521,7 +528,7 @@ bool IntegerTrail::EnqueueAssociatedLiteral(
   }
   if (trail_->Assignment().LiteralIsFalse(literal)) {
     std::vector<Literal>* conflict = trail_->MutableConflict();
-    *conflict = literal_reason;
+    conflict->assign(literal_reason.begin(), literal_reason.end());
 
     // This is tricky, in some corner cases, the same Enqueue() will call
     // EnqueueAssociatedLiteral() on a literal and its opposite. In this case,
@@ -542,8 +549,8 @@ bool IntegerTrail::EnqueueAssociatedLiteral(
 
 namespace {
 
-std::string ReasonDebugString(const std::vector<Literal>& literal_reason,
-                         const std::vector<IntegerLiteral>& integer_reason) {
+std::string ReasonDebugString(gtl::Span<Literal> literal_reason,
+                         gtl::Span<IntegerLiteral> integer_reason) {
   std::string result = "literals:{";
   for (const Literal l : literal_reason) {
     if (result.back() != '{') result += ",";
@@ -580,8 +587,8 @@ std::string IntegerTrail::DebugString() {
 }
 
 bool IntegerTrail::Enqueue(IntegerLiteral i_lit,
-                           const std::vector<Literal>& literal_reason,
-                           const std::vector<IntegerLiteral>& integer_reason) {
+                           gtl::Span<Literal> literal_reason,
+                           gtl::Span<IntegerLiteral> integer_reason) {
   DCHECK(AllLiteralsAreFalse(literal_reason));
   CHECK(!IsCurrentlyIgnored(i_lit.Var()));
 
@@ -594,7 +601,7 @@ bool IntegerTrail::Enqueue(IntegerLiteral i_lit,
   // This may not indicate an incorectness, but just some propagators that
   // didn't reach a fixed-point at level zero.
   if (DEBUG_MODE && !integer_decision_levels_.empty()) {
-    std::vector<Literal> l = literal_reason;
+    std::vector<Literal> l(literal_reason.begin(), literal_reason.end());
     MergeReasonInto(integer_reason, &l);
     LOG_IF(WARNING, l.empty())
         << "Propagating a literal with no reason at a positive level!\n"
@@ -679,7 +686,7 @@ bool IntegerTrail::Enqueue(IntegerLiteral i_lit,
     if (!IsOptional(var) || trail_->Assignment().LiteralIsFalse(
                                 Literal(is_ignored_literals_[var]))) {
       std::vector<Literal>* conflict = trail_->MutableConflict();
-      *conflict = literal_reason;
+      conflict->assign(literal_reason.begin(), literal_reason.end());
       if (IsOptional(var)) {
         conflict->push_back(Literal(is_ignored_literals_[var]));
       }
@@ -815,7 +822,7 @@ std::vector<Literal> IntegerTrail::ReasonFor(IntegerLiteral literal) const {
 }
 
 bool IntegerTrail::AllLiteralsAreFalse(
-    const std::vector<Literal>& literals) const {
+    gtl::Span<Literal> literals) const {
   for (const Literal lit : literals) {
     if (!trail_->Assignment().LiteralIsFalse(lit)) return false;
   }
@@ -824,7 +831,7 @@ bool IntegerTrail::AllLiteralsAreFalse(
 
 // TODO(user): If this is called many time on the same variables, it could be
 // made faster by using some caching mecanism.
-void IntegerTrail::MergeReasonInto(const std::vector<IntegerLiteral>& literals,
+void IntegerTrail::MergeReasonInto(gtl::Span<IntegerLiteral> literals,
                                    std::vector<Literal>* output) const {
   DCHECK(tmp_queue_.empty());
   const int size = vars_.size();
@@ -945,7 +952,8 @@ void IntegerTrail::MergeReasonIntoInternal(std::vector<Literal>* output) const {
   STLSortAndRemoveDuplicates(output);
 }
 
-ClauseRef IntegerTrail::Reason(const Trail& trail, int trail_index) const {
+gtl::Span<Literal> IntegerTrail::Reason(const Trail& trail,
+                                               int trail_index) const {
   std::vector<Literal>* reason = trail.GetVectorToStoreReason(trail_index);
   reason->clear();
 
@@ -958,12 +966,12 @@ ClauseRef IntegerTrail::Reason(const Trail& trail, int trail_index) const {
     tmp_queue_.push_back(next_trail_index);
   }
   MergeReasonIntoInternal(reason);
-  return ClauseRef(*reason);
+  return *reason;
 }
 
 void IntegerTrail::EnqueueLiteral(
-    Literal literal, const std::vector<Literal>& literal_reason,
-    const std::vector<IntegerLiteral>& integer_reason) {
+    Literal literal, gtl::Span<Literal> literal_reason,
+    gtl::Span<IntegerLiteral> integer_reason) {
   DCHECK(AllLiteralsAreFalse(literal_reason));
   if (integer_decision_levels_.empty()) {
     // Level zero. We don't keep any reason.
@@ -974,7 +982,7 @@ void IntegerTrail::EnqueueLiteral(
   // This may not indicate an incorectness, but just some propagators that
   // didn't reach a fixed-point at level zero.
   if (DEBUG_MODE && !integer_decision_levels_.empty()) {
-    std::vector<Literal> l = literal_reason;
+    std::vector<Literal> l(literal_reason.begin(), literal_reason.end());
     MergeReasonInto(integer_reason, &l);
     LOG_IF(WARNING, l.empty())
         << "Propagating a literal with no reason at a positive level!\n"

ortools/sat/integer.h

@@ -17,9 +17,11 @@
 #include <queue>
 #include <set>
 
-#include "ortools/base/port.h"
 #include "ortools/base/logging.h"
+#include "ortools/base/port.h"
+#include "ortools/base/inlined_vector.h"
 #include "ortools/base/join.h"
+#include "ortools/base/span.h"
 #include "ortools/base/int_type.h"
 #include "ortools/base/map_util.h"
 #include "ortools/sat/model.h"
@@ -149,7 +151,7 @@ inline std::ostream& operator<<(std::ostream& os, IntegerLiteral i_lit) {
   return os;
 }
 
-using InlinedIntegerLiteralVector = std::vector<IntegerLiteral>;
+using InlinedIntegerLiteralVector = gtl::InlinedVector<IntegerLiteral, 2>;
 
 // Each integer variable x will be associated with a set of literals encoding
 // (x >= v) for some values of v. This class maintains the relationship between
@@ -362,7 +364,8 @@ class IntegerTrail : public SatPropagator {
   // correct state before calling any of its functions.
   bool Propagate(Trail* trail) final;
   void Untrail(const Trail& trail, int literal_trail_index) final;
-  ClauseRef Reason(const Trail& trail, int trail_index) const final;
+  gtl::Span<Literal> Reason(const Trail& trail,
+                                   int trail_index) const final;
 
   // Returns the number of created integer variables.
   //
@@ -457,15 +460,14 @@ class IntegerTrail : public SatPropagator {
   // TODO(user): If the given bound is equal to the current bound, maybe the new
   // reason is better? how to decide and what to do in this case? to think about
   // it. Currently we simply don't do anything.
-  MUST_USE_RESULT bool Enqueue(
-      IntegerLiteral bound, const std::vector<Literal>& literal_reason,
-      const std::vector<IntegerLiteral>& integer_reason);
+  MUST_USE_RESULT bool Enqueue(IntegerLiteral bound,
+                               gtl::Span<Literal> literal_reason,
+                               gtl::Span<IntegerLiteral> integer_reason);
 
   // Enqueues the given literal on the trail.
   // See the comment of Enqueue() for the reason format.
-  void EnqueueLiteral(Literal literal,
-                      const std::vector<Literal>& literal_reason,
-                      const std::vector<IntegerLiteral>& integer_reason);
+  void EnqueueLiteral(Literal literal, gtl::Span<Literal> literal_reason,
+                      gtl::Span<IntegerLiteral> integer_reason);
 
   // Returns the reason (as set of Literal currently false) for a given integer
   // literal. Note that the bound must be less restrictive than the current
@@ -474,7 +476,7 @@ class IntegerTrail : public SatPropagator {
 
   // Appends the reason for the given integer literals to the output and call
   // STLSortAndRemoveDuplicates() on it.
-  void MergeReasonInto(const std::vector<IntegerLiteral>& bounds,
+  void MergeReasonInto(gtl::Span<IntegerLiteral> bounds,
                        std::vector<Literal>* output) const;
 
   // Returns the number of enqueues that changed a variable bounds. We don't
@@ -495,14 +497,14 @@ class IntegerTrail : public SatPropagator {
 
   // Helper functions to report a conflict. Always return false so a client can
   // simply do: return integer_trail_->ReportConflict(...);
-  bool ReportConflict(const std::vector<Literal>& literal_reason,
-                      const std::vector<IntegerLiteral>& integer_reason) {
+  bool ReportConflict(gtl::Span<Literal> literal_reason,
+                      gtl::Span<IntegerLiteral> integer_reason) {
     std::vector<Literal>* conflict = trail_->MutableConflict();
-    *conflict = literal_reason;
+    conflict->assign(literal_reason.begin(), literal_reason.end());
     MergeReasonInto(integer_reason, conflict);
     return false;
   }
-  bool ReportConflict(const std::vector<IntegerLiteral>& integer_reason) {
+  bool ReportConflict(gtl::Span<IntegerLiteral> integer_reason) {
     std::vector<Literal>* conflict = trail_->MutableConflict();
     conflict->clear();
     MergeReasonInto(integer_reason, conflict);
@@ -517,22 +519,21 @@ class IntegerTrail : public SatPropagator {
  private:
   // Tests that all the literals in the given reason are assigned to false.
   // This is used to DCHECK the given reasons to the Enqueue*() functions.
-  bool AllLiteralsAreFalse(const std::vector<Literal>& literals) const;
+  bool AllLiteralsAreFalse(gtl::Span<Literal> literals) const;
 
   // Does the work of MergeReasonInto() when queue_ is already initialized.
   void MergeReasonIntoInternal(std::vector<Literal>* output) const;
 
   // Helper used by Enqueue() to propagate one of the literal associated to
   // the given i_lit and maintained by encoder_.
-  bool EnqueueAssociatedLiteral(
-      Literal literal, IntegerLiteral i_lit,
-      const std::vector<Literal>& literal_reason,
-      const std::vector<IntegerLiteral>& integer_reason,
-      BooleanVariable* variable_with_same_reason);
+  bool EnqueueAssociatedLiteral(Literal literal, IntegerLiteral i_lit,
+                                gtl::Span<Literal> literal_reason,
+                                gtl::Span<IntegerLiteral> integer_reason,
+                                BooleanVariable* variable_with_same_reason);
 
   // Returns a lower bound on the given var that will always be valid.
   IntegerValue LevelZeroBound(int var) const {
-    // The level zero bounds are stored at the begining of the trail and they
+    // The level zero bounds are stored at the beginning of the trail and they
     // also serves as sentinels. Their index match the variables index.
     return integer_trail_[var].bound;
   }

ortools/sat/no_cycle.cc

@@ -154,7 +154,8 @@ void NoCyclePropagator::Untrail(const Trail& trail, int trail_index) {
 
 // TODO(user): If one literal propagate many arcs, and more than one is needed
 // to form a cycle, this will not work properly.
-ClauseRef NoCyclePropagator::Reason(const Trail& trail, int trail_index) const {
+gtl::Span<Literal> NoCyclePropagator::Reason(const Trail& trail,
+                                                    int trail_index) const {
   const int source = reason_arc_[trail_index].second;
   const int target = reason_arc_[trail_index].first;
   const int trail_limit = reason_trail_limit_[trail_index];
@@ -163,7 +164,7 @@ ClauseRef NoCyclePropagator::Reason(const Trail& trail, int trail_index) const {
 
   // Note that this modify node_is_reached_ and reached_nodes_.
   FindReasonForPath(trail, source, target, trail_limit, reason);
-  return ClauseRef(*reason);
+  return *reason;
 }
 
 namespace {

ortools/sat/no_cycle.h

@@ -48,7 +48,8 @@ class NoCyclePropagator : public SatPropagator {
 
   bool Propagate(Trail* trail) final;
   void Untrail(const Trail& trail, int trail_index) final;
-  ClauseRef Reason(const Trail& trail, int trail_index) const final;
+  gtl::Span<Literal> Reason(const Trail& trail,
+                                   int trail_index) const final;
 
   // Stops doing anything when the number of arcs in the graph becomes greater
   // that the given value. This allows to use this class to model a circuit

ortools/sat/optimization.cc

@@ -1135,7 +1135,7 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding(
     }
 
     // TODO(user): Investigate if constraining the objective is better.
-    if (/* DISALBES CODE */ (false)) {
+    if (/* DISABLES CODE */ (false)) {
       sat_solver->Backtrack(0);
       sat_solver->SetAssumptionLevel(0);
       if (!integer_trail->Enqueue(
@@ -1328,7 +1328,7 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding(
     // Re-express the objective with the new terms.
     // TODO(user): Do more experiments to decide if this is better.
     // TODO(user): Experiment with FixedWeightedSum().
-    if (/* DISALBES CODE */ (false)) {
+    if (/* DISABLES CODE */ (false)) {
       std::vector<IntegerVariable> constraint_vars;
       std::vector<int64> constraint_coeffs;
       for (const ObjectiveTerm node : terms) {
@@ -1347,7 +1347,7 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding(
     // TODO(user): Do more experiments to decide if this is better. This
     // approach kind of mix the basic linear-scan one with the core based
     // approach.
-    if (/* DISALBES CODE */ (false)) {
+    if (/* DISABLES CODE */ (false)) {
       IntegerValue best = new_var_ub;
 
       // Simple linear scan algorithm to find the optimal of new_var.

ortools/sat/pb_constraint.cc

@@ -959,14 +959,15 @@ void PbConstraints::Untrail(const Trail& trail, int trail_index) {
   }
 }
 
-ClauseRef PbConstraints::Reason(const Trail& trail, int trail_index) const {
+gtl::Span<Literal> PbConstraints::Reason(const Trail& trail,
+                                                int trail_index) const {
   SCOPED_TIME_STAT(&stats_);
   const PbConstraintsEnqueueHelper::ReasonInfo& reason_info =
       enqueue_helper_.reasons[trail_index];
   std::vector<Literal>* reason = trail.GetVectorToStoreReason(trail_index);
   reason_info.pb_constraint->FillReason(trail, reason_info.source_trail_index,
                                         trail[trail_index].Variable(), reason);
-  return ClauseRef(*reason);
+  return *reason;
 }
 
 UpperBoundedLinearConstraint* PbConstraints::ReasonPbConstraint(

ortools/sat/pb_constraint.h

@@ -64,7 +64,7 @@ inline std::ostream& operator<<(std::ostream& os, LiteralWithCoeff term) {
 //      lhs + bound_shift < canonical_form < rhs + bound_shift
 //
 // Finally, this will return false, if some integer overflow or underflow
-// occured during the reduction to the canonical form.
+// occurred during the reduction to the canonical form.
 bool ComputeBooleanLinearExpressionCanonicalForm(
     std::vector<LiteralWithCoeff>* cst, Coefficient* bound_shift,
     Coefficient* max_value);
@@ -77,8 +77,8 @@ bool ComputeBooleanLinearExpressionCanonicalForm(
 // bound_shift and max_value like ComputeBooleanLinearExpressionCanonicalForm()
 // does.
 //
-// Finally, this will return false if some integer overflow or underflow occured
-// during the constraint simplification.
+// Finally, this will return false if some integer overflow or underflow
+// occurred during the constraint simplification.
 bool ApplyLiteralMapping(const ITIVector<LiteralIndex, LiteralIndex>& mapping,
                          std::vector<LiteralWithCoeff>* cst,
                          Coefficient* bound_shift, Coefficient* max_value);
@@ -518,7 +518,8 @@ class PbConstraints : public SatPropagator {
 
   bool Propagate(Trail* trail) final;
   void Untrail(const Trail& trail, int trail_index) final;
-  ClauseRef Reason(const Trail& trail, int trail_index) const final;
+  gtl::Span<Literal> Reason(const Trail& trail,
+                                   int trail_index) const final;
 
   // Changes the number of variables.
   void Resize(int num_variables) {

ortools/sat/sat_base.h

@@ -16,12 +16,18 @@
 #ifndef OR_TOOLS_SAT_SAT_BASE_H_
 #define OR_TOOLS_SAT_SAT_BASE_H_
 
+#include <cstddef>
+#include <algorithm>
 #include <deque>
+#include <iterator>
 #include <memory>
 #include <string>
+#include <type_traits>
+#include <utility>
 #include <vector>
 
 #include "ortools/base/stringprintf.h"
+#include "ortools/base/span.h"
 #include "ortools/base/int_type.h"
 #include "ortools/base/int_type_indexed_vector.h"
 #include "ortools/sat/model.h"
@@ -164,36 +170,6 @@ class VariablesAssignment {
   DISALLOW_COPY_AND_ASSIGN(VariablesAssignment);
 };
 
-// A simple wrapper used to pass a reference to a clause. This
-// abstraction is needed because not all clauses come from an underlying
-// SatClause or are encoded with a std::vector<Literal>.
-//
-// This class should be passed by value.
-class ClauseRef {
- public:
-  ClauseRef() : begin_(nullptr), end_(nullptr) {}
-  ClauseRef(Literal const* b, Literal const* e) : begin_(b), end_(e) {}
-  explicit ClauseRef(const std::vector<Literal>& literals)
-      : begin_(literals.empty() ? nullptr : &literals[0]),
-        end_(literals.empty() ? nullptr : &literals[0] + literals.size()) {}
-
-  // For testing so this can be used with EXPECT_THAT().
-  typedef Literal value_type;
-  typedef const Literal* const_iterator;
-
-  // Allows for range based iteration: for (Literal literal : clause_ref) {}.
-  Literal const* begin() const { return begin_; }
-  Literal const* end() const { return end_; }
-
-  // Returns true if this clause contains no literal.
-  bool IsEmpty() const { return begin_ == end_; }
-  int size() const { return end_ - begin_; }
-
- private:
-  Literal const* begin_;
-  Literal const* end_;
-};
-
 // Forward declaration.
 class SatClause;
 class SatPropagator;
@@ -298,7 +274,7 @@ class Trail {
   }
 
   // Returns the reason why this variable was assigned.
-  ClauseRef Reason(BooleanVariable var) const;
+  gtl::Span<Literal> Reason(BooleanVariable var) const;
 
   // Returns the "type" of an assignment (see AssignmentType). Note that this
   // function never returns kSameReasonAs or kCachedReason, it instead returns
@@ -324,9 +300,7 @@ class Trail {
   // Reason() function of the associated propagator.
   void NotifyThatReasonIsCached(BooleanVariable var) const {
     DCHECK(assignment_.VariableIsAssigned(var));
-    const std::vector<Literal>& reason =
-        reasons_repository_[info_[var].trail_index];
-    reasons_[var] = reason.empty() ? ClauseRef() : ClauseRef(reason);
+    reasons_[var] = reasons_repository_[info_[var].trail_index];
     old_type_[var] = info_[var].type;
     info_[var].type = AssignmentType::kCachedReason;
   }
@@ -353,9 +327,7 @@ class Trail {
   }
 
   // Returns the last conflict.
-  ClauseRef FailingClause() const {
-    return conflict_.empty() ? ClauseRef() : ClauseRef(conflict_);
-  }
+  gtl::Span<Literal> FailingClause() const { return conflict_; }
 
   // Specific SatClause interface so we can update the conflict clause activity.
   // Note that MutableConflict() automatically sets this to nullptr, so we can
@@ -426,7 +398,7 @@ class Trail {
   // variables, the memory address of the vectors (kept in reasons_) are still
   // valid.
   mutable std::deque<std::vector<Literal>> reasons_repository_;
-  mutable ITIVector<BooleanVariable, ClauseRef> reasons_;
+  mutable ITIVector<BooleanVariable, gtl::Span<Literal>> reasons_;
   mutable ITIVector<BooleanVariable, int> old_type_;
 
   // This is used by RegisterPropagator() and Reason().
@@ -470,21 +442,20 @@ class SatPropagator {
     propagation_trail_index_ = std::min(propagation_trail_index_, trail_index);
   }
 
-  // Explains why the literal at given trail_index was propagated by returning
-  // a reason ClauseRef for this propagation. This will only be called for
-  // literals that are on the trail and were propagated by this class.
+  // Explains why the literal at given trail_index was propagated by returning a
+  // reason for this propagation. This will only be called for literals that are
+  // on the trail and were propagated by this class.
   //
   // The interpretation is that because all the literals of a reason were
   // assigned to false, we could deduce the assignement of the given variable.
   //
-  // The returned ClauseRef has to be valid until the literal is untrailed.
-  // A client can use trail_.GetVectorToStoreReason() if it doesn't have a
-  // memory location that already contains the reason.
-  virtual ClauseRef Reason(const Trail& trail, int trail_index) const {
+  // The returned Span has to be valid until the literal is untrailed. A client
+  // can use trail_.GetVectorToStoreReason() if it doesn't have a memory
+  // location that already contains the reason.
+  virtual gtl::Span<Literal> Reason(const Trail& trail,
+                                           int trail_index) const {
     LOG(FATAL) << "Not implemented.";
-#if !defined(__linux__)  // for Mac OS and MSVC++.
-    return ClauseRef();
-#endif
+    return {};
   }
 
   // Returns true if all the preconditions for Propagate() are satisfied.
@@ -573,7 +544,7 @@ inline int Trail::AssignmentType(BooleanVariable var) const {
   return type != AssignmentType::kCachedReason ? type : old_type_[var];
 }
 
-inline ClauseRef Trail::Reason(BooleanVariable var) const {
+inline gtl::Span<Literal> Trail::Reason(BooleanVariable var) const {
   // Special case for AssignmentType::kSameReasonAs to avoid a recursive call.
   var = ReferenceVarWithSameReason(var);
 
@@ -583,7 +554,7 @@ inline ClauseRef Trail::Reason(BooleanVariable var) const {
   const AssignmentInfo& info = info_[var];
   if (info.type == AssignmentType::kUnitReason ||
       info.type == AssignmentType::kSearchDecision) {
-    reasons_[var] = ClauseRef();
+    reasons_[var] = {};
   } else {
     DCHECK_LT(info.type, propagators_.size());
     DCHECK(propagators_[info.type] != nullptr) << info.type;

ortools/sat/sat_parameters.proto

@@ -464,7 +464,7 @@ message SatParameters {
   // This always result in better propagation, but it is usually slow, so
   // depending on the problem, turning this off may lead to a faster solution.
   optional bool use_disjunctive_constraint_in_cumulative_constraint = 80
-      [default = false];
+      [default = true];
 
   // When this is true, then we extract all the linear constraints of the
   // CpModel and linearly encode some other constraints in an extra "linear

ortools/sat/sat_solver.cc

@@ -353,7 +353,7 @@ void SatSolver::AddLearnedClauseAndEnqueueUnitPropagation(
   // that where needed to infer the conflict may not be "reasons" anymore and
   // may be deleted.
   if (drat_writer_ != nullptr) {
-    drat_writer_->AddClause(ClauseRef(literals));
+    drat_writer_->AddClause(literals);
   }
 
   if (literals.size() == 1) {
@@ -1451,7 +1451,7 @@ void SatSolver::ProcessNewlyFixedVariables() {
   // others.
   for (SatClause* clause : clauses_) {
     if (clause->IsAttached()) {
-      const int old_size = clause->Size();
+      const size_t old_size = clause->Size();
       if (clause->RemoveFixedLiteralsAndTestIfTrue(trail_->Assignment())) {
         // The clause is always true, detach it.
         clauses_propagator_.LazyDetach(clause);
@@ -1469,13 +1469,14 @@ void SatSolver::ProcessNewlyFixedVariables() {
         }
       }
 
-      if (clause->Size() != old_size && drat_writer_ != nullptr) {
+      const size_t new_size = clause->Size();
+      if (new_size != old_size && drat_writer_ != nullptr) {
         // TODO(user): Instead delete the original clause in
         // DeleteDetachedClause(). The problem is that we currently don't have
         // the initial size anywhere.
-        drat_writer_->AddClause(ClauseRef(clause->begin(), clause->end()));
+        drat_writer_->AddClause({clause->begin(), new_size});
         drat_writer_->DeleteClause(
-            ClauseRef(clause->begin(), clause->begin() + old_size),
+            {clause->begin(), old_size},
             /*ignore_call=*/clauses_info_.find(clause) == clauses_info_.end());
       }
     }
@@ -1922,7 +1923,7 @@ std::string SatSolver::DebugString(const SatClause& clause) const {
   return result;
 }
 
-int SatSolver::ComputeMaxTrailIndex(ClauseRef clause) const {
+int SatSolver::ComputeMaxTrailIndex(gtl::Span<Literal> clause) const {
   SCOPED_TIME_STAT(&stats_);
   int trail_index = -1;
   for (const Literal literal : clause) {
@@ -1973,9 +1974,9 @@ void SatSolver::ComputeFirstUIPConflict(
   //
   // This last literal will be the first UIP because by definition all the
   // propagation done at the current level will pass though it at some point.
-  ClauseRef clause_to_expand = trail_->FailingClause();
+  gtl::Span<Literal> clause_to_expand = trail_->FailingClause();
   SatClause* sat_clause = trail_->FailingSatClause();
-  DCHECK(!clause_to_expand.IsEmpty());
+  DCHECK(!clause_to_expand.empty());
   int num_literal_at_highest_level_that_needs_to_be_processed = 0;
   while (true) {
     int num_new_vars_at_positive_level = 0;
@@ -2047,7 +2048,7 @@ void SatSolver::ComputeFirstUIPConflict(
     // which is what setting clause_to_expand to the empty clause do.
     if (same_reason_identifier_.FirstVariableWithSameReason(
             literal.Variable()) != literal.Variable()) {
-      clause_to_expand = ClauseRef();
+      clause_to_expand = {};
     } else {
       clause_to_expand = trail_->Reason(literal.Variable());
     }
@@ -2280,8 +2281,8 @@ void SatSolver::MinimizeConflictSimple(std::vector<Literal>* conflict) {
     bool can_be_removed = false;
     if (DecisionLevel(var) != current_level) {
       // It is important not to call Reason(var) when it can be avoided.
-      const ClauseRef reason = trail_->Reason(var);
-      if (!reason.IsEmpty()) {
+      const gtl::Span<Literal> reason = trail_->Reason(var);
+      if (!reason.empty()) {
         can_be_removed = true;
         for (Literal literal : reason) {
           if (DecisionLevel(literal.Variable()) == 0) continue;
@@ -2400,7 +2401,7 @@ bool SatSolver::CanBeInferedFromConflictVariables(BooleanVariable variable) {
   variable_to_process_.push_back(variable);
 
   // First we expand the reason for the given variable.
-  DCHECK(!trail_->Reason(variable).IsEmpty())
+  DCHECK(!trail_->Reason(variable).empty())
       << trail_->Info(variable).DebugString();
   for (Literal literal : trail_->Reason(variable)) {
     const BooleanVariable var = literal.Variable();
@@ -2462,7 +2463,7 @@ bool SatSolver::CanBeInferedFromConflictVariables(BooleanVariable variable) {
     // Expand the variable. This can be seen as making a recursive call.
     dfs_stack_.push_back(current_var);
     bool abort_early = false;
-    DCHECK(!trail_->Reason(current_var).IsEmpty());
+    DCHECK(!trail_->Reason(current_var).empty());
     for (Literal literal : trail_->Reason(current_var)) {
       const BooleanVariable var = literal.Variable();
       DCHECK_NE(var, current_var);
@@ -2542,8 +2543,8 @@ void SatSolver::MinimizeConflictExperimental(std::vector<Literal>* conflict) {
 
     // A nullptr reason means that this was a decision variable from the
     // previous levels.
-    const ClauseRef reason = trail_->Reason(var);
-    if (reason.IsEmpty()) continue;
+    const gtl::Span<Literal> reason = trail_->Reason(var);
+    if (reason.empty()) continue;
 
     // Compute how many and which literals from the current reason do not appear
     // in the current conflict. Level 0 literals are ignored.
@@ -2602,9 +2603,10 @@ void SatSolver::DeleteDetachedClauses() {
        ++it) {
     // We do not want to mark as deleted clause of size 2 because they are
     // still kept in the solver inside the BinaryImplicationGraph.
-    if (drat_writer_ != nullptr && (*it)->Size() > 2) {
+    const size_t size = (*it)->Size();
+    if (drat_writer_ != nullptr && size > 2) {
       drat_writer_->DeleteClause(
-          ClauseRef((*it)->begin(), (*it)->end()),
+          {(*it)->begin(), size},
           /*ignore_call=*/clauses_info_.find(*it) == clauses_info_.end());
     }
     clauses_info_.erase(*it);

ortools/sat/sat_solver.h

@@ -265,7 +265,7 @@ class SatSolver {
   int EnqueueDecisionAndBacktrackOnConflict(Literal true_literal);
 
   // Tries to enqueue the given decision and performs the propagation.
-  // Returns true if no conflict occured. Otherwise, returns false and restores
+  // Returns true if no conflict occurred. Otherwise, returns false and restores
   // the solver to the state just before this was called.
   //
   // Note(user): With this function, the solver doesn't learn anything.
@@ -292,7 +292,7 @@ class SatSolver {
   // Extract the current problem clauses. The Output type must support the two
   // functions:
   //  - void AddBinaryClause(Literal a, Literal b);
-  //  - void AddClause(ClauseRef clause);
+  //  - void AddClause(gtl::Span<Literal> clause);
   //
   // TODO(user): also copy the learned clauses?
   template <typename Output>
@@ -313,7 +313,8 @@ class SatSolver {
     binary_implication_graph_.ExtractAllBinaryClauses(out);
     for (SatClause* clause : clauses_) {
       if (!clause->IsRedundant()) {
-        out->AddClause(ClauseRef(clause->begin(), clause->end()));
+        out->AddClause(
+            gtl::Span<Literal>(clause->begin(), clause->Size()));
       }
     }
   }
@@ -386,7 +387,7 @@ class SatSolver {
   bool Propagate();
 
  private:
-  // Calls Propagate() and returns true if no conflict occured. Otherwise,
+  // Calls Propagate() and returns true if no conflict occurred. Otherwise,
   // learns the conflict, backtracks, enqueues the consequence of the learned
   // conflict and returns false.
   bool PropagateAndStopAfterOneConflictResolution();
@@ -423,7 +424,7 @@ class SatSolver {
   // backjumps. In this case, we will simply keep reapplying decisions from the
   // last one backtracked over and so on.
   //
-  // Returns MODEL_STAT if no conflict occured, MODEL_UNSAT if the model was
+  // Returns MODEL_STAT if no conflict occurred, MODEL_UNSAT if the model was
   // proven unsat and ASSUMPTION_UNSAT otherwise. In the last case the first non
   // taken old decision will be propagated to false by the ones before.
   //
@@ -528,7 +529,7 @@ class SatSolver {
 
   // Returns the maximum trail_index of the literals in the given clause.
   // All the literals must be assigned. Returns -1 if the clause is empty.
-  int ComputeMaxTrailIndex(ClauseRef clause) const;
+  int ComputeMaxTrailIndex(gtl::Span<Literal> clause) const;
 
   // Computes what is known as the first UIP (Unique implication point) conflict
   // clause starting from the failing clause. For a definition of UIP and a

ortools/sat/simplification.cc

@@ -147,14 +147,9 @@ std::vector<bool> SatPostsolver::PostsolveSolution(
   return postsolved_solution;
 }
 
-void SatPresolver::AddBinaryClause(Literal a, Literal b) {
-  Literal c[2];
-  c[0] = a;
-  c[1] = b;
-  AddClause(ClauseRef(c, c + 2));
-}
+void SatPresolver::AddBinaryClause(Literal a, Literal b) { AddClause({a, b}); }
 
-void SatPresolver::AddClause(ClauseRef clause) {
+void SatPresolver::AddClause(gtl::Span<Literal> clause) {
   CHECK_GT(clause.size(), 0) << "Added an empty clause to the presolver";
   const ClauseIndex ci(clauses_.size());
   clauses_.push_back(std::vector<Literal>(clause.begin(), clause.end()));
@@ -185,7 +180,7 @@ void SatPresolver::AddClause(ClauseRef clause) {
   }
 
   if (drat_writer_ != nullptr && clause_ref.size() < old_size) {
-    drat_writer_->AddClause(ClauseRef(clause_ref));
+    drat_writer_->AddClause(clause_ref);
     drat_writer_->DeleteClause(clause);
   }
 
@@ -212,7 +207,7 @@ void SatPresolver::SetNumVariables(int num_variables) {
 }
 
 void SatPresolver::AddClauseInternal(std::vector<Literal>* clause) {
-  if (drat_writer_ != nullptr) drat_writer_->AddClause(ClauseRef(*clause));
+  if (drat_writer_ != nullptr) drat_writer_->AddClause(*clause);
 
   DCHECK(std::is_sorted(clause->begin(), clause->end()));
   CHECK_GT(clause->size(), 0) << "TODO(fdid): Unsat during presolve?";
@@ -340,7 +335,7 @@ void SatPresolver::SimpleBva(LiteralIndex l) {
       // Find a literal different from l that occur in the less number of
       // clauses.
       const LiteralIndex l_min =
-          FindLiteralWithShortestOccurenceListExcluding(clause, Literal(l));
+          FindLiteralWithShortestOccurrenceListExcluding(clause, Literal(l));
       if (l_min == kNoLiteralIndex) continue;
 
       // Find all the clauses of the form "clause \ {l} + {l'}", for a literal
@@ -438,7 +433,7 @@ void SatPresolver::SimpleBva(LiteralIndex l) {
     const std::vector<Literal>& clause = clauses_[c];
     CHECK(!clause.empty());
     const LiteralIndex l_min =
-        FindLiteralWithShortestOccurenceListExcluding(clause, Literal(l));
+        FindLiteralWithShortestOccurrenceListExcluding(clause, Literal(l));
     for (const LiteralIndex lit : m_lit_) {
       if (lit == l) continue;
       for (const ClauseIndex d : literal_to_clauses_[l_min]) {
@@ -476,15 +471,15 @@ bool SatPresolver::ProcessClauseToSimplifyOthers(ClauseIndex clause_index) {
   DCHECK(std::is_sorted(clause.begin(), clause.end()));
 
   LiteralIndex opposite_literal;
-  const Literal lit = FindLiteralWithShortestOccurenceList(clause);
+  const Literal lit = FindLiteralWithShortestOccurrenceList(clause);
 
   // Try to simplify the clauses containing 'lit'. We take advantage of this
   // loop to also remove the empty sets from the list.
   {
     int new_index = 0;
-    std::vector<ClauseIndex>& occurence_list_ref =
+    std::vector<ClauseIndex>& occurrence_list_ref =
         literal_to_clauses_[lit.Index()];
-    for (ClauseIndex ci : occurence_list_ref) {
+    for (ClauseIndex ci : occurrence_list_ref) {
       if (clauses_[ci].empty()) continue;
       if (ci != clause_index &&
           SimplifyClause(clause, &clauses_[ci], &opposite_literal)) {
@@ -496,10 +491,10 @@ bool SatPresolver::ProcessClauseToSimplifyOthers(ClauseIndex clause_index) {
           if (clauses_[ci].empty()) return false;  // UNSAT.
           if (drat_writer_ != nullptr) {
             // TODO(user): remove the old clauses_[ci] afterwards.
-            drat_writer_->AddClause(ClauseRef(clauses_[ci]));
+            drat_writer_->AddClause(clauses_[ci]);
           }
 
-          // Remove ci from the occurence list. Note that the occurence list
+          // Remove ci from the occurrence list. Note that the occurrence list
           // can't be shortest_list or its negation.
           auto iter =
               std::find(literal_to_clauses_[opposite_literal].begin(),
@@ -516,10 +511,10 @@ bool SatPresolver::ProcessClauseToSimplifyOthers(ClauseIndex clause_index) {
           }
         }
       }
-      occurence_list_ref[new_index] = ci;
+      occurrence_list_ref[new_index] = ci;
       ++new_index;
     }
-    occurence_list_ref.resize(new_index);
+    occurrence_list_ref.resize(new_index);
     CHECK_EQ(literal_to_clause_sizes_[lit.Index()], new_index);
     literal_to_clause_sizes_[lit.Index()] = new_index;
   }
@@ -529,9 +524,9 @@ bool SatPresolver::ProcessClauseToSimplifyOthers(ClauseIndex clause_index) {
   {
     int new_index = 0;
     bool something_removed = false;
-    std::vector<ClauseIndex>& occurence_list_ref =
+    std::vector<ClauseIndex>& occurrence_list_ref =
         literal_to_clauses_[lit.NegatedIndex()];
-    for (ClauseIndex ci : occurence_list_ref) {
+    for (ClauseIndex ci : occurrence_list_ref) {
       if (clauses_[ci].empty()) continue;
 
       // TODO(user): not super optimal since we could abort earlier if
@@ -541,7 +536,7 @@ bool SatPresolver::ProcessClauseToSimplifyOthers(ClauseIndex clause_index) {
         if (clauses_[ci].empty()) return false;  // UNSAT.
         if (drat_writer_ != nullptr) {
           // TODO(user): remove the old clauses_[ci] afterwards.
-          drat_writer_->AddClause(ClauseRef(clauses_[ci]));
+          drat_writer_->AddClause(clauses_[ci]);
         }
         if (!in_clause_to_process_[ci]) {
           in_clause_to_process_[ci] = true;
@@ -550,10 +545,10 @@ bool SatPresolver::ProcessClauseToSimplifyOthers(ClauseIndex clause_index) {
         something_removed = true;
         continue;
       }
-      occurence_list_ref[new_index] = ci;
+      occurrence_list_ref[new_index] = ci;
       ++new_index;
     }
-    occurence_list_ref.resize(new_index);
+    occurrence_list_ref.resize(new_index);
     literal_to_clause_sizes_[lit.NegatedIndex()] = new_index;
     if (something_removed) {
       UpdatePriorityQueue(Literal(lit.NegatedIndex()).Variable());
@@ -668,7 +663,7 @@ void SatPresolver::Remove(ClauseIndex ci) {
     UpdateBvaPriorityQueue(Literal(e.Variable(), false).Index());
   }
   if (drat_writer_ != nullptr) {
-    drat_writer_->DeleteClause(ClauseRef(clauses_[ci]));
+    drat_writer_->DeleteClause(clauses_[ci]);
   }
   STLClearObject(&clauses_[ci]);
 }
@@ -678,7 +673,7 @@ void SatPresolver::RemoveAndRegisterForPostsolve(ClauseIndex ci, Literal x) {
   Remove(ci);
 }
 
-Literal SatPresolver::FindLiteralWithShortestOccurenceList(
+Literal SatPresolver::FindLiteralWithShortestOccurrenceList(
     const std::vector<Literal>& clause) {
   CHECK(!clause.empty());
   Literal result = clause.front();
@@ -691,16 +686,16 @@ Literal SatPresolver::FindLiteralWithShortestOccurenceList(
   return result;
 }
 
-LiteralIndex SatPresolver::FindLiteralWithShortestOccurenceListExcluding(
+LiteralIndex SatPresolver::FindLiteralWithShortestOccurrenceListExcluding(
     const std::vector<Literal>& clause, Literal to_exclude) {
   CHECK(!clause.empty());
   LiteralIndex result = kNoLiteralIndex;
-  int num_occurences = std::numeric_limits<int>::max();
+  int num_occurrences = std::numeric_limits<int>::max();
   for (const Literal l : clause) {
     if (l == to_exclude) continue;
-    if (literal_to_clause_sizes_[l.Index()] < num_occurences) {
+    if (literal_to_clause_sizes_[l.Index()] < num_occurrences) {
       result = l.Index();
-      num_occurences = literal_to_clause_sizes_[l.Index()];
+      num_occurrences = literal_to_clause_sizes_[l.Index()];
     }
   }
   return result;
@@ -1054,7 +1049,7 @@ void ProbeAndFindEquivalentLiteral(
           temp.push_back(assignment.LiteralIsTrue(Literal(i))
                              ? Literal(rep)
                              : Literal(rep).Negated());
-          drat_writer->AddClause(ClauseRef(temp));
+          drat_writer->AddClause(temp);
         }
       }
     }
@@ -1072,7 +1067,7 @@ void ProbeAndFindEquivalentLiteral(
             temp.push_back(assignment.LiteralIsTrue(Literal(rep))
                                ? Literal(i)
                                : Literal(i).Negated());
-            drat_writer->AddClause(ClauseRef(temp));
+            drat_writer->AddClause(temp);
           }
         }
       } else if (rep != i) {
@@ -1083,7 +1078,7 @@ void ProbeAndFindEquivalentLiteral(
         temp.push_back(Literal(i));
         temp.push_back(Literal(rep).Negated());
         postsolver->Add(Literal(i), temp);
-        if (drat_writer != nullptr) drat_writer->AddClause(ClauseRef(temp));
+        if (drat_writer != nullptr) drat_writer->AddClause(temp);
       }
     }
   }

ortools/sat/simplification.h

@@ -130,7 +130,7 @@ class SatPresolver {
   // Adds new clause to the SatPresolver.
   void SetNumVariables(int num_variables);
   void AddBinaryClause(Literal a, Literal b);
-  void AddClause(ClauseRef clause);
+  void AddClause(gtl::Span<Literal> clause);
 
   // Presolves the problem currently loaded. Returns false if the model is
   // proven to be UNSAT during the presolving.
@@ -202,9 +202,9 @@ class SatPresolver {
 
   // Finds the literal from the clause that occur the less in the clause
   // database.
-  Literal FindLiteralWithShortestOccurenceList(
+  Literal FindLiteralWithShortestOccurrenceList(
       const std::vector<Literal>& clause);
-  LiteralIndex FindLiteralWithShortestOccurenceListExcluding(
+  LiteralIndex FindLiteralWithShortestOccurrenceListExcluding(
       const std::vector<Literal>& clause, Literal to_exclude);
 
   // Tests and maybe perform a Simple Bounded Variable addition starting from
@@ -214,7 +214,7 @@ class SatPresolver {
   // 2013.
   // https://www.research.ibm.com/haifa/conferences/hvc2012/papers/paper16.pdf
   //
-  // This seems to have a mostly postive effect, except on the crafted problem
+  // This seems to have a mostly positive effect, except on the crafted problem
   // familly mugrauer_balint--GI.crafted_nxx_d6_cx_numxx where the reduction
   // is big, but apparently the problem is harder to prove UNSAT for the solver.
   void SimpleBva(LiteralIndex l);
@@ -248,7 +248,7 @@ class SatPresolver {
   AdjustablePriorityQueue<PQElement> var_pq_;
 
   // Literal priority queue for BVA. The literals are ordered by descending
-  // number of occurences in clauses.
+  // number of occurrences in clauses.
   void InitializeBvaPriorityQueue();
   void UpdateBvaPriorityQueue(LiteralIndex var);
   void AddToBvaPriorityQueue(LiteralIndex var);
@@ -287,12 +287,12 @@ class SatPresolver {
   // An empty clause means that it has been removed.
   std::vector<std::vector<Literal>> clauses_;  // Indexed by ClauseIndex
 
-  // Occurence list. For each literal, contains the ClauseIndex of the clause
+  // Occurrence list. For each literal, contains the ClauseIndex of the clause
   // that contains it (ordered by clause index).
   ITIVector<LiteralIndex, std::vector<ClauseIndex>> literal_to_clauses_;
 
-  // Because we only lazily clean the occurence list after clause deletions,
-  // we keep the size of the occurence list (without the deleted clause) here.
+  // Because we only lazily clean the occurrence list after clause deletions,
+  // we keep the size of the occurrence list (without the deleted clause) here.
   ITIVector<LiteralIndex, int> literal_to_clause_sizes_;
 
   // Used for postsolve.

ortools/sat/symmetry.cc

@@ -92,7 +92,7 @@ bool SymmetryPropagator::PropagateNext(Trail* trail) {
         // Set the conflict on the trail.
         // Note that we need to fetch a reason for this.
         std::vector<Literal>* conflict = trail->MutableConflict();
-        const ClauseRef initial_reason =
+        const gtl::Span<Literal> initial_reason =
             trail->Reason(non_symmetric.literal.Variable());
         Permute(p_index, initial_reason, conflict);
         conflict->push_back(non_symmetric.image);
@@ -141,15 +141,15 @@ void SymmetryPropagator::Untrail(const Trail& trail, int trail_index) {
   }
 }
 
-ClauseRef SymmetryPropagator::Reason(const Trail& trail,
-                                     int trail_index) const {
+gtl::Span<Literal> SymmetryPropagator::Reason(const Trail& trail,
+                                                     int trail_index) const {
   SCOPED_TIME_STAT(&stats_);
   const ReasonInfo& reason_info = reasons_[trail_index];
   std::vector<Literal>* reason = trail.GetVectorToStoreReason(trail_index);
   Permute(reason_info.symmetry_index,
           trail.Reason(trail[reason_info.source_trail_index].Variable()),
           reason);
-  return ClauseRef(*reason);
+  return *reason;
 }
 
 bool SymmetryPropagator::Enqueue(const Trail& trail, Literal literal,
@@ -186,7 +186,7 @@ bool SymmetryPropagator::Enqueue(const Trail& trail, Literal literal,
   return *index == p_trail->size();
 }
 
-void SymmetryPropagator::Permute(int index, ClauseRef input,
+void SymmetryPropagator::Permute(int index, gtl::Span<Literal> input,
                                  std::vector<Literal>* output) const {
   SCOPED_TIME_STAT(&stats_);
 

ortools/sat/symmetry.h

@@ -59,10 +59,11 @@ class SymmetryPropagator : public SatPropagator {
 
   bool Propagate(Trail* trail) final;
   void Untrail(const Trail& trail, int trail_index) final;
-  ClauseRef Reason(const Trail& trail, int trail_index) const final;
+  gtl::Span<Literal> Reason(const Trail& trail,
+                                   int trail_index) const final;
 
   // Adds a new permutation to this symmetry propagator. The ownership is
-  // transfered. This must be an integer permutation such that:
+  // transferred. This must be an integer permutation such that:
   // - Its domain is [0, 2 * num_variables) and corresponds to the index
   //   representation of the literals over num_variables variables.
   // - It must be compatible with the negation, for any literal l; not(p(l))
@@ -85,7 +86,8 @@ class SymmetryPropagator : public SatPropagator {
   // Permutes a list of literals from input into output using the permutation
   // with given index. This uses tmp_literal_mapping_ and has a complexity in
   // O(permutation_support + input_size).
-  void Permute(int index, ClauseRef input, std::vector<Literal>* output) const;
+  void Permute(int index, gtl::Span<Literal> input,
+               std::vector<Literal>* output) const;
 
  private:
   // Propagates the literal at propagation_trail_index_ from the trail.