Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
integer_base.cc
Go to the documentation of this file.
1// Copyright 2010-2025 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
15
16#include <cstdint>
17#include <numeric>
18#include <utility>
19
20#include "absl/log/check.h"
21
23
25 if (coeffs[0] == 0) vars[0] = kNoIntegerVariable;
26 if (coeffs[1] == 0) vars[1] = kNoIntegerVariable;
27
28 // Corner case when the underlying variable is the same.
30 // Make sure variable are positive before merging.
31 for (int i = 0; i < 2; ++i) {
32 if (!VariableIsPositive(vars[i])) {
33 coeffs[i] = -coeffs[i];
34 vars[i] = NegationOf(vars[i]);
35 }
36 }
37
38 coeffs[0] += coeffs[1];
39 coeffs[1] = 0;
41 if (coeffs[0] == 0) vars[0] = kNoIntegerVariable;
42 }
43
44 // Make sure coeff are positive.
45 for (int i = 0; i < 2; ++i) {
46 if (coeffs[i] < 0) {
47 coeffs[i] = -coeffs[i];
48 vars[i] = NegationOf(vars[i]);
49 }
50 }
51
52 // Make sure variable are sorted.
53 if (vars[0] > vars[1]) {
54 std::swap(vars[0], vars[1]);
55 std::swap(coeffs[0], coeffs[1]);
56 }
57}
58
60 const uint64_t gcd = std::gcd(coeffs[0].value(), coeffs[1].value());
61 if (gcd > 1) {
62 coeffs[0] /= gcd;
63 coeffs[1] /= gcd;
64 return IntegerValue(gcd);
65 }
66 return IntegerValue(1);
67}
68
70 bool negate = false;
71 if (coeffs[0] == 0) {
72 if (coeffs[1] != 0) {
73 negate = !VariableIsPositive(vars[1]);
74 }
75 } else {
76 negate = !VariableIsPositive(vars[0]);
77 }
78 if (negate) Negate();
79 return negate;
80}
81
83 IntegerValue& ub,
84 bool allow_negation) {
86 if (coeffs[0] == 0 || coeffs[1] == 0) return; // abort.
87
88 if (allow_negation) {
89 const bool negated = NegateForCanonicalization();
90 if (negated) {
91 // We need to be able to negate without overflow.
92 CHECK_GE(lb, kMinIntegerValue);
93 CHECK_LE(ub, kMaxIntegerValue);
94 std::swap(lb, ub);
95 lb = -lb;
96 ub = -ub;
97 }
98 }
99
100 // Do gcd division.
101 const uint64_t gcd = std::gcd(coeffs[0].value(), coeffs[1].value());
102 if (gcd > 1) {
103 coeffs[0] /= gcd;
104 coeffs[1] /= gcd;
105 ub = FloorRatio(ub, IntegerValue(gcd));
106 lb = CeilRatio(lb, IntegerValue(gcd));
107 }
108
109 CHECK(coeffs[0] != 0 || vars[0] == kNoIntegerVariable);
110 CHECK(coeffs[1] != 0 || vars[1] == kNoIntegerVariable);
111}
112
114 IntegerValue ub) {
115 expr.CanonicalizeAndUpdateBounds(lb, ub);
116 if (expr.coeffs[0] == 0 || expr.coeffs[1] == 0) return false;
117
118 auto [it, inserted] = best_bounds_.insert({expr, {lb, ub}});
119 if (inserted) return true;
120
121 const auto [known_lb, known_ub] = it->second;
122 bool restricted = false;
123 if (lb > known_lb) {
124 it->second.first = lb;
125 restricted = true;
126 }
127 if (ub < known_ub) {
128 it->second.second = ub;
129 restricted = true;
130 }
131 return restricted;
132}
133
135 IntegerValue lb,
136 IntegerValue ub) const {
137 expr.CanonicalizeAndUpdateBounds(lb, ub);
138 if (expr.coeffs[0] == 0 || expr.coeffs[1] == 0) {
140 }
141
142 const auto it = best_bounds_.find(expr);
143 if (it != best_bounds_.end()) {
144 const auto [known_lb, known_ub] = it->second;
145 if (lb <= known_lb && ub >= known_ub) return RelationStatus::IS_TRUE;
146 if (lb > known_ub || ub < known_lb) return RelationStatus::IS_FALSE;
147 }
149}
150
152 LinearExpression2 expr) const {
154 const IntegerValue gcd = expr.DivideByGcd();
155 const bool negated = expr.NegateForCanonicalization();
156 const auto it = best_bounds_.find(expr);
157 if (it != best_bounds_.end()) {
158 const auto [known_lb, known_ub] = it->second;
159 if (negated) {
160 return CapProdI(gcd, -known_lb);
161 } else {
162 return CapProdI(gcd, known_ub);
163 }
164 }
165 return kMaxIntegerValue;
166}
167
168} // namespace operations_research::sat
IntegerValue GetUpperBound(LinearExpression2 expr) const
bool Add(LinearExpression2 expr, IntegerValue lb, IntegerValue ub)
RelationStatus GetStatus(LinearExpression2 expr, IntegerValue lb, IntegerValue ub) const
Returns the known status of expr <= bound.
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
IntegerValue CeilRatio(IntegerValue dividend, IntegerValue positive_divisor)
std::vector< IntegerVariable > NegationOf(absl::Span< const IntegerVariable > vars)
Returns the vector of the negated variables.
Definition integer.cc:52
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue.value())
const IntegerVariable kNoIntegerVariable(-1)
IntegerVariable PositiveVariable(IntegerVariable i)
bool VariableIsPositive(IntegerVariable i)
IntegerValue CapProdI(IntegerValue a, IntegerValue b)
Overflows and saturated arithmetic.
void CanonicalizeAndUpdateBounds(IntegerValue &lb, IntegerValue &ub, bool allow_negation=false)
void Negate()
Take the negation of this expression.