From cbd8ba864155e828207ea2f9c39442095f26aff6 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Thu, 1 Jun 2017 16:28:29 +0200 Subject: [PATCH] introduce array slices and use them in sat --- ortools/algorithms/dynamic_partition.cc | 19 +- ortools/algorithms/dynamic_partition.h | 9 +- ortools/algorithms/find_graph_symmetries.cc | 2 +- ortools/base/inlined_vector.h | 665 ++++++++++++++++++++ ortools/base/span.h | 542 ++++++++++++++++ ortools/linear_solver/linear_solver.cc | 1 + ortools/sat/clause.cc | 10 +- ortools/sat/clause.h | 22 +- ortools/sat/cp_model.proto | 11 + ortools/sat/cp_model_checker.cc | 10 +- ortools/sat/cp_model_presolve.cc | 98 ++- ortools/sat/cp_model_solver.cc | 106 ++-- ortools/sat/drat.cc | 9 +- ortools/sat/drat.h | 6 +- ortools/sat/integer.cc | 42 +- ortools/sat/integer.h | 43 +- ortools/sat/no_cycle.cc | 5 +- ortools/sat/no_cycle.h | 3 +- ortools/sat/optimization.cc | 6 +- ortools/sat/pb_constraint.cc | 5 +- ortools/sat/pb_constraint.h | 9 +- ortools/sat/sat_base.h | 71 +-- ortools/sat/sat_parameters.proto | 2 +- ortools/sat/sat_solver.cc | 36 +- ortools/sat/sat_solver.h | 13 +- ortools/sat/simplification.cc | 59 +- ortools/sat/simplification.h | 16 +- ortools/sat/symmetry.cc | 10 +- ortools/sat/symmetry.h | 8 +- 29 files changed, 1562 insertions(+), 276 deletions(-) create mode 100644 ortools/base/inlined_vector.h create mode 100644 ortools/base/span.h diff --git a/ortools/algorithms/dynamic_partition.cc b/ortools/algorithms/dynamic_partition.cc index 78b7ff794c..590153754e 100644 --- a/ortools/algorithms/dynamic_partition.cc +++ b/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( diff --git a/ortools/algorithms/dynamic_partition.h b/ortools/algorithms/dynamic_partition.h index fe79fca23e..d3dd74090a 100644 --- a/ortools/algorithms/dynamic_partition.h +++ b/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_; // The disjoint parts. diff --git a/ortools/algorithms/find_graph_symmetries.cc b/ortools/algorithms/find_graph_symmetries.cc index 42ffabd3f3..b1c1599f40 100644 --- a/ortools/algorithms/find_graph_symmetries.cc +++ b/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 adjacency_directions(1, /*outgoing=*/true); + std::vector adjacency_directions(1, /*outgoing*/ true); if (!reverse_adj_list_index_.empty()) { adjacency_directions.push_back(false); // Also look at incoming arcs. } diff --git a/ortools/base/inlined_vector.h b/ortools/base/inlined_vector.h new file mode 100644 index 0000000000..55c873f3b4 --- /dev/null +++ b/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 is like a std::vector, 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, consider using util::bitmap::InlinedBitVector +// in ortools/base/inlined_bitvector.h +// + +#include + +#include +#include +#include +#include +#include +#include +#include +#include +#include // NOLINT(build/include_order) + +#include "ortools/base/logging.h" + +namespace gtl { + +template +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 + InlinedVector( + InputIterator range_start, InputIterator range_end, + typename std::enable_if::value>::type* = + NULL) { + InitRep(); + AppendRange(range_start, range_end); + } + + InlinedVector(std::initializer_list 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(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(u_.data); + } else { + return outofline_pointer(); + } + } + const_pointer data() const { + return const_cast*>(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 + void emplace_back(Args&&... args) { + size_t s = size(); + DCHECK_LE(s, capacity()); + if (s < capacity()) { + new (data() + s) T(std::forward(args)...); + set_size_internal(s + 1); + } else { + EmplaceBackSlow(std::forward(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(n, nullptr); } + void resize(size_t n, const value_type& elem) { Resize(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(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(u_.data[kSize - 1]); + if (s != kSentinel) { + return static_cast(s); + } else { + const uint64_t word = outofline_word(); + // The sentinel and capacity bits are most-significant bits in word. + return static_cast(word & 0xffffffffffffull); + } + } + + void set_size_internal(size_t n) { + if (is_inline()) { + DCHECK_LT(n, kSentinel); + u_.data[kSize - 1] = static_cast(n); + } else { + uint64_t word; + // The sentinel and capacity bits are most-significant bits in word. + word = (static_cast(n) | + (static_cast(u_.data[kSize - 2]) << 48) | + (static_cast(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 + void EmplaceBackSlow(Args&&... args) { + const size_t s = size(); + DCHECK_EQ(s, capacity()); + Grow(s + 1, std::forward(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::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 + void operator()(T* dst, Args&&... args) const { + new (dst) T(std::forward(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 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(malloc(target * sizeof(T))); + + // Need to copy elem before discarding src since it might alias src. + InitType{}(dst + s, std::forward(args)...); + Mover(src, s, dst); + DiscardStorage(); + + u_.data[kSize - 1] = kSentinel; + u_.data[kSize - 2] = static_cast(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 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 + void AppendRange(Iter first, Iter last, std::input_iterator_tag); + + // Faster path for forward iterators. + template + void AppendRange(Iter first, Iter last, std::forward_iterator_tag); + + template + void AppendRange(Iter first, Iter last); +}; + +// Provide linkage for constants. +template +const size_t InlinedVector::kSizeUnaligned; +template +const size_t InlinedVector::kSize; +template +const unsigned int InlinedVector::kSentinel; +template +const size_t InlinedVector::kFit1; +template +const size_t InlinedVector::kFit; + +template +inline void swap(InlinedVector& a, InlinedVector& b) { + a.swap(b); +} + +template +inline bool operator==(const InlinedVector& a, + const InlinedVector& b) { + return a.size() == b.size() && std::equal(a.begin(), a.end(), b.begin()); +} + +template +inline bool operator!=(const InlinedVector& a, + const InlinedVector& b) { + return !(a == b); +} + +template +inline bool operator<(const InlinedVector& a, + const InlinedVector& b) { + return std::lexicographical_compare(a.begin(), a.end(), b.begin(), b.end()); +} + +template +inline bool operator>(const InlinedVector& a, + const InlinedVector& b) { + return b < a; +} + +template +inline bool operator<=(const InlinedVector& a, + const InlinedVector& b) { + return !(b < a); +} + +template +inline bool operator>=(const InlinedVector& a, + const InlinedVector& b) { + return !(a < b); +} + +// ======================================== +// Implementation + +template +inline InlinedVector::InlinedVector() { + InitRep(); +} + +template +inline InlinedVector::InlinedVector(size_t n) { + InitRep(); + if (n > capacity()) { + Grow(n); // Must use Nop in case T is not copyable + } + set_size_internal(n); + ValueInit(nullptr, n, data()); +} + +template +inline InlinedVector::InlinedVector(size_t n, const value_type& elem) { + InitRep(); + if (n > capacity()) { + Grow(n); // Can use Nop since we know we have nothing to copy + } + set_size_internal(n); + Fill(&elem, n, data()); +} + +template +inline InlinedVector::InlinedVector(const InlinedVector& v) { + InitRep(); + *this = v; +} + +template +typename InlinedVector::iterator InlinedVector::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(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 InlinedVector::iterator InlinedVector::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 +void InlinedVector::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(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 +template +inline void InlinedVector::AppendRange(Iter first, Iter last, + std::input_iterator_tag) { + std::copy(first, last, std::back_inserter(*this)); +} + +template +template +inline void InlinedVector::AppendRange(Iter first, Iter last, + std::forward_iterator_tag) { + typedef typename std::iterator_traits::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 +template +inline void InlinedVector::AppendRange(Iter first, Iter last) { + typedef typename std::iterator_traits::iterator_category IterTag; + AppendRange(first, last, IterTag()); +} + +} // namespace gtl + +#endif // OR_TOOLS_BASE_INLINED_VECTOR_H_ diff --git a/ortools/base/span.h b/ortools/base/span.h new file mode 100644 index 0000000000..fea74883ea --- /dev/null +++ b/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 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 is somewhat analogous to a StringPiece, but for +// array elements of type T. +// +// Implicit conversion operations are provided from types such as +// std::vector and util::gtl::InlinedVector. 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 my_vector; +// MyRoutine(vector_as_array(&my_vector), my_vector.size()); +// +// util::gtl::InlinedVector 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 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 my_vector; +// MyRoutine(my_vector); +// +// util::gtl::InlinedVector my_inline_vector; +// MyRoutine(my_inline_vector); +// +// int my_array[10]; +// MyRoutine(my_array); +// +// int* my_array = new int[10]; +// MyRoutine(gtl::Span(my_array, 10)); +// +// MutableSpan 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 a) { +// for (int i = 0; i < a.size(); i++) { .. mutate a[i] .. } +// } +// +// std::vector my_vector; +// MyMutatingRoutine(&my_vector); +// +// int my_array[10]; +// MyMutatingRoutine(my_array); +// +// int* my_array = new int[10]; +// MyMutatingRoutine(gtl::MutableSpan(my_array, 10)); +// +// MyProto my_proto; +// for (int i = 0; i < 10; ++i) { my_proto.add_value(i); } +// MyMutatingRoutine(my_proto.mutable_value()); + +#include +#include +#include +#include + +#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 + static decltype(std::declval().data()) Get(C* v) { + return v->data(); + } +}; + +struct MutableData { + template + static decltype(std::declval().mutable_data()) Get(C* v) { + return v->mutable_data(); + } +}; + +struct Size { + template + static decltype(std::declval().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()==true. +template +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())); + return !std::is_same() && Checker::template valid(); + } +}; + +// Defines HasGet() for a particular method, container, and checker. If +// HasGet()==true, provides Get() that delegates to the method. +template ::HasGet()> +struct Wrapper { + static constexpr bool HasGet() { return false; } +}; + +template +struct Wrapper { + static constexpr bool HasGet() { return true; } + static decltype(M::Get(std::declval())) Get(C* v) { return M::Get(v); } +}; + +// Type checker for a method returning an integral value. +struct SizeChecker { + template + static constexpr bool valid() { + return std::is_integral::value; + } +}; + +// Type checker for a method returning either a pointer to T or a less const +// version of that. +template +struct DataChecker { + // We want to enable conversion from std::vector to Span + // but + // disable conversion from std::vector to Span. 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 + static constexpr bool valid() { + return std::is_convertible::value; + } +}; + +// Aliases to A if A::HasGet()==true, or to B otherwise. +template +using FirstWithGet = typename std::conditional::type; + +// Wraps C::data() const, returning a pointer to const data. +template +using ContainerData = Wrapper, 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 +using ContainerMutableData = + FirstWithGet, C>, + FirstWithGet, C>, + Wrapper, C>>>; + +// Wraps C::size() const. +template +using ContainerSize = Wrapper; + +// 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 +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 reverse_iterator; + typedef std::reverse_iterator const_reverse_iterator; + typedef size_t size_type; + typedef ptrdiff_t difference_type; + + static const size_type npos = static_cast(-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 +class SpanImpl : public SpanImplBase { + public: + using SpanImplBase::SpanImplBase; + + // Defined iff the data and size accessors for the container C have been + // defined. + template + using EnableIfConvertibleFrom = + typename std::enable_if::HasGet() && + ContainerSize::HasGet()>::type; + + // Constructs from a container when EnableIfConvertibleFrom is + // defined. std::addressof handles types with overloaded operator&. + template + explicit SpanImpl(const C& v) + : SpanImplBase(ContainerData::Get(std::addressof(v)), + ContainerSize::Get(std::addressof(v))) {} +}; + +template +class MutableSpanImpl : public SpanImplBase { + public: + using SpanImplBase::SpanImplBase; + + template + using EnableIfConvertibleFrom = + typename std::enable_if::HasGet() && + ContainerSize::HasGet()>::type; + + template + explicit MutableSpanImpl(C* v) + : SpanImplBase(ContainerMutableData::Get(v), + ContainerSize::Get(v)) {} +}; + +} // namespace array_slice_internal + + +template +class Span { + private: + typedef array_slice_internal::SpanImpl 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& v) // NOLINT(runtime/explicit) + : impl_(v.data(), v.size()) {} + + template + Span(const value_type (&a)[N]) // NOLINT(runtime/explicit) + : impl_(a, N) {} + + template + Span(const InlinedVector& 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, std::string and (since C++11) + // std::vector and std::array are examples of this. See + // array_slice_internal.h for details. + template > + 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 x); + // Process({1, 2, 3}); + // The data referenced by the initializer_list must outlive this + // Span. For example, "Span s={1,2};" and "return + // Span({3,4});" are errors, as the resulting Span may + // reference data that is no longer valid. + Span(std::initializer_list 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 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 other) const { return impl_ == other.impl_; } + bool operator!=(Span 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"; 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). +template +class MutableSpan { + private: + typedef array_slice_internal::MutableSpanImpl 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* v) // NOLINT(runtime/explicit) + : impl_(v->data(), v->size()) {} + + template + MutableSpan(value_type (&a)[N]) // NOLINT(runtime/explicit) + : impl_(a, N) {} + + template + MutableSpan( + InlinedVector* 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 > + 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 other) const { + return Span(*this) == other; + } + bool operator!=(Span other) const { + return Span(*this) != other; + } + + // DEPRECATED(jacobsa): Please use data() instead. + pointer mutable_data() const { return impl_.data(); } + + private: + Impl impl_; +}; + +template +const typename Span::size_type Span::npos; +template +const typename MutableSpan::size_type MutableSpan::npos; + +} // namespace gtl + +#endif // OR_TOOLS_BASE_SPAN_H_ diff --git a/ortools/linear_solver/linear_solver.cc b/ortools/linear_solver/linear_solver.cc index 7a415d3d05..e5a2c6d36d 100644 --- a/ortools/linear_solver/linear_solver.cc +++ b/ortools/linear_solver/linear_solver.cc @@ -1606,3 +1606,4 @@ int MPSolverParameters::GetIntegerParam(MPSolverParameters::IntegerParam param) } // namespace operations_research + diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc index 42691a6330..acc5cefac7 100644 --- a/ortools/sat/clause.cc +++ b/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 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 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 diff --git a/ortools/sat/clause.h b/ortools/sat/clause.h index 1e8c81bf5a..b4395dccd5 100644 --- a/ortools/sat/clause.h +++ b/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 PropagationReason() const { // Note that we don't need to include the propagated literal. - return ClauseRef(&(literals_[1]), end()); + return gtl::Span(&(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 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 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> 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> implications_; int64 num_implications_; // Some stats. diff --git a/ortools/sat/cp_model.proto b/ortools/sat/cp_model.proto index 2dc4fa1ab6..49bcf181f0 100644 --- a/ortools/sat/cp_model.proto +++ b/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. diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc index e1a7e3741a..3c01fb9ab9 100644 --- a/ortools/sat/cp_model_checker.cc +++ b/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; } } diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 7adcc442c6..eaeb1d5e10 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/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 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 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 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& 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. diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 5c1ccb99eb..190b7df994 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/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 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 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 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 ConstructSearchStrategy( + const std::unordered_map>& + var_to_coeff_offset_pair, const std::vector& strategies, Model* model) { IntegerEncoder* const integer_encoder = model->GetOrCreate(); IntegerTrail* const integer_trail = model->GetOrCreate(); // 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 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()->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 strategies; + std::unordered_map> 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()->NumVariables(); + VLOG(1) << "Solution #" << num_solutions + << " obj:" << response.objective_value() + << " num_bool:" << sat_model.Get()->NumVariables(); }; if (parameters.optimize_with_core()) { @@ -1120,7 +1146,7 @@ CpSolverResponse SolveCpModelWithoutPresolve(const CpModelProto& model_proto, std::vector 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); diff --git a/ortools/sat/drat.cc b/ortools/sat/drat.cc index 07da9122b7..c07f90ccce 100644 --- a/ortools/sat/drat.cc +++ b/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 clause) { + WriteClause(clause); +} -void DratWriter::DeleteClause(ClauseRef clause, bool ignore_call) { +void DratWriter::DeleteClause(gtl::Span clause, + bool ignore_call) { if (ignore_call) return; buffer_ += "d "; WriteClause(clause); } -void DratWriter::WriteClause(ClauseRef clause) { +void DratWriter::WriteClause(gtl::Span clause) { values_.clear(); for (const Literal l : clause) { CHECK_LT(l.Variable(), reverse_mapping_.size()); diff --git a/ortools/sat/drat.h b/ortools/sat/drat.h index d751773408..c76873c534 100644 --- a/ortools/sat/drat.h +++ b/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 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 clause, bool ignore_call = true); private: - void WriteClause(ClauseRef clause); + void WriteClause(gtl::Span clause); // We need to keep track of the variable newly created. int variable_index_; diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc index 6086ee7bcc..402789c797 100644 --- a/ortools/sat/integer.cc +++ b/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& literals, const std::vector& 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_reason, - const std::vector& integer_reason, + gtl::Span literal_reason, + gtl::Span 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* 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_reason, - const std::vector& integer_reason) { +std::string ReasonDebugString(gtl::Span literal_reason, + gtl::Span 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_reason, - const std::vector& integer_reason) { + gtl::Span literal_reason, + gtl::Span 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 l = literal_reason; + std::vector 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* 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 IntegerTrail::ReasonFor(IntegerLiteral literal) const { } bool IntegerTrail::AllLiteralsAreFalse( - const std::vector& literals) const { + gtl::Span 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& literals, +void IntegerTrail::MergeReasonInto(gtl::Span literals, std::vector* output) const { DCHECK(tmp_queue_.empty()); const int size = vars_.size(); @@ -945,7 +952,8 @@ void IntegerTrail::MergeReasonIntoInternal(std::vector* output) const { STLSortAndRemoveDuplicates(output); } -ClauseRef IntegerTrail::Reason(const Trail& trail, int trail_index) const { +gtl::Span IntegerTrail::Reason(const Trail& trail, + int trail_index) const { std::vector* 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_reason, - const std::vector& integer_reason) { + Literal literal, gtl::Span literal_reason, + gtl::Span 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 l = literal_reason; + std::vector 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" diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index f30fe92fe8..874ffe6a67 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -17,9 +17,11 @@ #include #include -#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; +using InlinedIntegerLiteralVector = gtl::InlinedVector; // 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 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_reason, - const std::vector& integer_reason); + MUST_USE_RESULT bool Enqueue(IntegerLiteral bound, + gtl::Span literal_reason, + gtl::Span 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_reason, - const std::vector& integer_reason); + void EnqueueLiteral(Literal literal, gtl::Span literal_reason, + gtl::Span 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& bounds, + void MergeReasonInto(gtl::Span bounds, std::vector* 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_reason, - const std::vector& integer_reason) { + bool ReportConflict(gtl::Span literal_reason, + gtl::Span integer_reason) { std::vector* 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& integer_reason) { + bool ReportConflict(gtl::Span integer_reason) { std::vector* 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& literals) const; + bool AllLiteralsAreFalse(gtl::Span literals) const; // Does the work of MergeReasonInto() when queue_ is already initialized. void MergeReasonIntoInternal(std::vector* 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_reason, - const std::vector& integer_reason, - BooleanVariable* variable_with_same_reason); + bool EnqueueAssociatedLiteral(Literal literal, IntegerLiteral i_lit, + gtl::Span literal_reason, + gtl::Span 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; } diff --git a/ortools/sat/no_cycle.cc b/ortools/sat/no_cycle.cc index a90aa2c6df..c0662a6eb2 100644 --- a/ortools/sat/no_cycle.cc +++ b/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 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 { diff --git a/ortools/sat/no_cycle.h b/ortools/sat/no_cycle.h index 3500427ac2..c8a9331c04 100644 --- a/ortools/sat/no_cycle.h +++ b/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 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 diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc index 5c6a7f96ff..736a1295dd 100644 --- a/ortools/sat/optimization.cc +++ b/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 constraint_vars; std::vector 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. diff --git a/ortools/sat/pb_constraint.cc b/ortools/sat/pb_constraint.cc index 12029e41b6..cd871e3b23 100644 --- a/ortools/sat/pb_constraint.cc +++ b/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 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* 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( diff --git a/ortools/sat/pb_constraint.h b/ortools/sat/pb_constraint.h index 64ccbbe1be..758632cc44 100644 --- a/ortools/sat/pb_constraint.h +++ b/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* 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& mapping, std::vector* 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 Reason(const Trail& trail, + int trail_index) const final; // Changes the number of variables. void Resize(int num_variables) { diff --git a/ortools/sat/sat_base.h b/ortools/sat/sat_base.h index 544b2d7c9b..2c652b21ed 100644 --- a/ortools/sat/sat_base.h +++ b/ortools/sat/sat_base.h @@ -16,12 +16,18 @@ #ifndef OR_TOOLS_SAT_SAT_BASE_H_ #define OR_TOOLS_SAT_SAT_BASE_H_ +#include +#include #include +#include #include #include +#include +#include #include #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. -// -// 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& 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 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& 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 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> reasons_repository_; - mutable ITIVector reasons_; + mutable ITIVector> reasons_; mutable ITIVector 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 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 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; diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index be453f5273..4c4b716b9e 100644 --- a/ortools/sat/sat_parameters.proto +++ b/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 diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc index fb251ec310..2e206d8a82 100644 --- a/ortools/sat/sat_solver.cc +++ b/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 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 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* 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 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* 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 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); diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h index 6eab08575d..c429836126 100644 --- a/ortools/sat/sat_solver.h +++ b/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 clause); // // TODO(user): also copy the learned clauses? template @@ -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(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 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 diff --git a/ortools/sat/simplification.cc b/ortools/sat/simplification.cc index 7612ca4826..88fa595976 100644 --- a/ortools/sat/simplification.cc +++ b/ortools/sat/simplification.cc @@ -147,14 +147,9 @@ std::vector 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 clause) { CHECK_GT(clause.size(), 0) << "Added an empty clause to the presolver"; const ClauseIndex ci(clauses_.size()); clauses_.push_back(std::vector(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* 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& 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& occurence_list_ref = + std::vector& 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& occurence_list_ref = + std::vector& 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& 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& clause, Literal to_exclude) { CHECK(!clause.empty()); LiteralIndex result = kNoLiteralIndex; - int num_occurences = std::numeric_limits::max(); + int num_occurrences = std::numeric_limits::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); } } } diff --git a/ortools/sat/simplification.h b/ortools/sat/simplification.h index 76d8940c77..343c2372f4 100644 --- a/ortools/sat/simplification.h +++ b/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 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& clause); - LiteralIndex FindLiteralWithShortestOccurenceListExcluding( + LiteralIndex FindLiteralWithShortestOccurrenceListExcluding( const std::vector& 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 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> 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> 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 literal_to_clause_sizes_; // Used for postsolve. diff --git a/ortools/sat/symmetry.cc b/ortools/sat/symmetry.cc index bc33512815..f64554d6c2 100644 --- a/ortools/sat/symmetry.cc +++ b/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* conflict = trail->MutableConflict(); - const ClauseRef initial_reason = + const gtl::Span 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 SymmetryPropagator::Reason(const Trail& trail, + int trail_index) const { SCOPED_TIME_STAT(&stats_); const ReasonInfo& reason_info = reasons_[trail_index]; std::vector* 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 input, std::vector* output) const { SCOPED_TIME_STAT(&stats_); diff --git a/ortools/sat/symmetry.h b/ortools/sat/symmetry.h index 977ed820c9..00f6a5f401 100644 --- a/ortools/sat/symmetry.h +++ b/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 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* output) const; + void Permute(int index, gtl::Span input, + std::vector* output) const; private: // Propagates the literal at propagation_trail_index_ from the trail.