Google OR-Tools v9.12
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
cp_model_fz_solver.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 <algorithm>
17#include <cstdint>
18#include <functional>
19#include <limits>
20#include <string>
21#include <tuple>
22#include <utility>
23#include <vector>
24
25#include "absl/container/flat_hash_map.h"
26#include "absl/container/flat_hash_set.h"
27#include "absl/flags/flag.h"
28#include "absl/log/check.h"
29#include "absl/strings/match.h"
30#include "absl/strings/str_cat.h"
31#include "absl/types/span.h"
32#include "google/protobuf/text_format.h"
37#include "ortools/sat/cp_model.pb.h"
41#include "ortools/sat/model.h"
42#include "ortools/sat/sat_parameters.pb.h"
45
46ABSL_FLAG(int64_t, fz_int_max, int64_t{1} << 40,
47 "Default max value for unbounded integer variables.");
48
49namespace operations_research {
50namespace sat {
51
52namespace {
53
54static const int kNoVar = std::numeric_limits<int>::min();
55
56struct VarOrValue {
57 int var = kNoVar;
58 int64_t value = 0;
59};
60
61// Returns the true/false literal corresponding to a CpModelProto variable.
62int TrueLiteral(int var) { return var; }
63int FalseLiteral(int var) { return -var - 1; }
64
65// Helper class to convert a flatzinc model to a CpModelProto.
66struct CpModelProtoWithMapping {
67 // Returns a constant CpModelProto variable created on-demand.
68 int LookupConstant(int64_t value);
69
70 // Convert a flatzinc argument to a variable or a list of variable.
71 // Note that we always encode a constant argument with a constant variable.
72 int LookupVar(const fz::Argument& argument);
73 LinearExpressionProto LookupExpr(const fz::Argument& argument,
74 bool negate = false);
75 LinearExpressionProto LookupExprAt(const fz::Argument& argument, int pos,
76 bool negate = false);
77 std::vector<int> LookupVars(const fz::Argument& argument);
78 std::vector<VarOrValue> LookupVarsOrValues(const fz::Argument& argument);
79
80 // Create and return the indices of the IntervalConstraint corresponding
81 // to the flatzinc "interval" specified by a start var and a size var.
82 // This method will cache intervals with the key <start, size>.
83 std::vector<int> CreateIntervals(absl::Span<const VarOrValue> starts,
84 absl::Span<const VarOrValue> sizes);
85
86 // Create and return the indices of the IntervalConstraint corresponding
87 // to the flatzinc "interval" specified by a start var and a size var.
88 // This method will cache intervals with the key <start, size>.
89 // This interval will be optional if the size can be 0.
90 // It also adds a constraint linking the enforcement literal with the size,
91 // stating that the interval will be performed if and only if the size is
92 // greater than 0.
93 std::vector<int> CreateNonZeroOrOptionalIntervals(
94 absl::Span<const VarOrValue> starts, absl::Span<const VarOrValue> sizes);
95
96 // Create and return the index of the optional IntervalConstraint
97 // corresponding to the flatzinc "interval" specified by a start var, the
98 // size_var, and the Boolean opt_var. This method will cache intervals with
99 // the key <start, size, opt_var>. If opt_var == kNoVar, the interval will not
100 // be optional.
101 int GetOrCreateOptionalInterval(VarOrValue start_var, VarOrValue size,
102 int opt_var);
103
104 // Get or Create a literal that implies the variable is > 0.
105 // Its negation implies the variable is == 0.
106 int NonZeroLiteralFrom(VarOrValue size);
107
108 // Adds a constraint to the model, add the enforcement literal if it is
109 // different from kNoVar, and returns a ptr to the ConstraintProto.
110 ConstraintProto* AddEnforcedConstraint(int literal);
111
112 // Helpers to fill a ConstraintProto.
113 void FillAMinusBInDomain(const std::vector<int64_t>& domain,
114 const fz::Constraint& fz_ct, ConstraintProto* ct);
115 void FillLinearConstraintWithGivenDomain(absl::Span<const int64_t> domain,
116 const fz::Constraint& fz_ct,
117 ConstraintProto* ct);
118 void FillConstraint(const fz::Constraint& fz_ct, ConstraintProto* ct);
119 void FillReifOrImpliedConstraint(const fz::Constraint& fz_ct,
120 ConstraintProto* ct);
121 void BuildTableFromDomainIntLinEq(const fz::Constraint& fz_ct,
122 ConstraintProto* ct);
123
124 // Translates the flatzinc search annotations into the CpModelProto
125 // search_order field.
126 void TranslateSearchAnnotations(
127 absl::Span<const fz::Annotation> search_annotations,
128 SolverLogger* logger);
129
130 // The output proto.
131 CpModelProto proto;
132 SatParameters parameters;
133
134 // Mapping from flatzinc variables to CpModelProto variables.
135 absl::flat_hash_map<fz::Variable*, int> fz_var_to_index;
136 absl::flat_hash_map<int64_t, int> constant_value_to_index;
137 absl::flat_hash_map<std::tuple<int, int64_t, int, int64_t, int>, int>
138 interval_key_to_index;
139 absl::flat_hash_map<int, int> var_to_lit_implies_greater_than_zero;
140};
141
142int CpModelProtoWithMapping::LookupConstant(int64_t value) {
143 if (constant_value_to_index.contains(value)) {
144 return constant_value_to_index[value];
145 }
146
147 // Create the constant on the fly.
148 const int index = proto.variables_size();
149 IntegerVariableProto* var_proto = proto.add_variables();
150 var_proto->add_domain(value);
151 var_proto->add_domain(value);
152 constant_value_to_index[value] = index;
153 return index;
154}
155
156int CpModelProtoWithMapping::LookupVar(const fz::Argument& argument) {
157 if (argument.HasOneValue()) return LookupConstant(argument.Value());
158 CHECK_EQ(argument.type, fz::Argument::VAR_REF);
159 return fz_var_to_index[argument.Var()];
160}
161
162LinearExpressionProto CpModelProtoWithMapping::LookupExpr(
163 const fz::Argument& argument, bool negate) {
164 LinearExpressionProto expr;
165 if (argument.HasOneValue()) {
166 const int64_t value = argument.Value();
167 expr.set_offset(negate ? -value : value);
168 } else {
169 expr.add_vars(LookupVar(argument));
170 expr.add_coeffs(negate ? -1 : 1);
171 }
172 return expr;
173}
174
175LinearExpressionProto CpModelProtoWithMapping::LookupExprAt(
176 const fz::Argument& argument, int pos, bool negate) {
177 LinearExpressionProto expr;
178 if (argument.HasOneValueAt(pos)) {
179 const int64_t value = argument.ValueAt(pos);
180 expr.set_offset(negate ? -value : value);
181 } else {
182 expr.add_vars(fz_var_to_index[argument.VarAt(pos)]);
183 expr.add_coeffs(negate ? -1 : 1);
184 }
185 return expr;
186}
187
188std::vector<int> CpModelProtoWithMapping::LookupVars(
189 const fz::Argument& argument) {
190 std::vector<int> result;
191 if (argument.type == fz::Argument::VOID_ARGUMENT) return result;
192 if (argument.type == fz::Argument::INT_LIST) {
193 for (int64_t value : argument.values) {
194 result.push_back(LookupConstant(value));
195 }
196 } else if (argument.type == fz::Argument::INT_VALUE) {
197 result.push_back(LookupConstant(argument.Value()));
198 } else {
199 CHECK_EQ(argument.type, fz::Argument::VAR_REF_ARRAY);
200 for (fz::Variable* var : argument.variables) {
201 CHECK(var != nullptr);
202 result.push_back(fz_var_to_index[var]);
203 }
204 }
205 return result;
206}
207
208std::vector<VarOrValue> CpModelProtoWithMapping::LookupVarsOrValues(
209 const fz::Argument& argument) {
210 std::vector<VarOrValue> result;
211 const int no_var = kNoVar;
212 if (argument.type == fz::Argument::VOID_ARGUMENT) return result;
213 if (argument.type == fz::Argument::INT_LIST) {
214 for (int64_t value : argument.values) {
215 result.push_back({no_var, value});
216 }
217 } else if (argument.type == fz::Argument::INT_VALUE) {
218 result.push_back({no_var, argument.Value()});
219 } else {
220 CHECK_EQ(argument.type, fz::Argument::VAR_REF_ARRAY);
221 for (fz::Variable* var : argument.variables) {
222 CHECK(var != nullptr);
223 if (var->domain.HasOneValue()) {
224 result.push_back({no_var, var->domain.Value()});
225 } else {
226 result.push_back({fz_var_to_index[var], 0});
227 }
228 }
229 }
230 return result;
231}
232
233ConstraintProto* CpModelProtoWithMapping::AddEnforcedConstraint(int literal) {
234 ConstraintProto* result = proto.add_constraints();
235 if (literal != kNoVar) {
236 result->add_enforcement_literal(literal);
237 }
238 return result;
239}
240
241int CpModelProtoWithMapping::GetOrCreateOptionalInterval(VarOrValue start,
242 VarOrValue size,
243 int opt_var) {
244 const int interval_index = proto.constraints_size();
245 const std::tuple<int, int64_t, int, int64_t, int> key =
246 std::make_tuple(start.var, start.value, size.var, size.value, opt_var);
247 const auto [it, inserted] =
248 interval_key_to_index.insert({key, interval_index});
249 if (!inserted) {
250 return it->second;
251 }
252
253 if (size.var == kNoVar || start.var == kNoVar) { // Size or start fixed.
254 auto* interval = AddEnforcedConstraint(opt_var)->mutable_interval();
255 if (start.var != kNoVar) {
256 interval->mutable_start()->add_vars(start.var);
257 interval->mutable_start()->add_coeffs(1);
258 interval->mutable_end()->add_vars(start.var);
259 interval->mutable_end()->add_coeffs(1);
260 } else {
261 interval->mutable_start()->set_offset(start.value);
262 interval->mutable_end()->set_offset(start.value);
263 }
264
265 if (size.var != kNoVar) {
266 interval->mutable_size()->add_vars(size.var);
267 interval->mutable_size()->add_coeffs(1);
268 interval->mutable_end()->add_vars(size.var);
269 interval->mutable_end()->add_coeffs(1);
270 } else {
271 interval->mutable_size()->set_offset(size.value);
272 interval->mutable_end()->set_offset(size.value +
273 interval->end().offset());
274 }
275 return interval_index;
276 } else { // start and size are variable.
277 const int end_var = proto.variables_size();
279 ReadDomainFromProto(proto.variables(start.var))
280 .AdditionWith(ReadDomainFromProto(proto.variables(size.var))),
281 proto.add_variables());
282
283 // Create the interval.
284 auto* interval = AddEnforcedConstraint(opt_var)->mutable_interval();
285 interval->mutable_start()->add_vars(start.var);
286 interval->mutable_start()->add_coeffs(1);
287 interval->mutable_size()->add_vars(size.var);
288 interval->mutable_size()->add_coeffs(1);
289 interval->mutable_end()->add_vars(end_var);
290 interval->mutable_end()->add_coeffs(1);
291
292 // Add the linear constraint (after the interval constraint as we have
293 // stored its index).
294 auto* lin = AddEnforcedConstraint(opt_var)->mutable_linear();
295 lin->add_vars(start.var);
296 lin->add_coeffs(1);
297 lin->add_vars(size.var);
298 lin->add_coeffs(1);
299 lin->add_vars(end_var);
300 lin->add_coeffs(-1);
301 lin->add_domain(0);
302 lin->add_domain(0);
303
304 return interval_index;
305 }
306}
307
308std::vector<int> CpModelProtoWithMapping::CreateIntervals(
309 absl::Span<const VarOrValue> starts, absl::Span<const VarOrValue> sizes) {
310 std::vector<int> intervals;
311 for (int i = 0; i < starts.size(); ++i) {
312 intervals.push_back(
313 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
314 }
315 return intervals;
316}
317
318std::vector<int> CpModelProtoWithMapping::CreateNonZeroOrOptionalIntervals(
319 absl::Span<const VarOrValue> starts, absl::Span<const VarOrValue> sizes) {
320 std::vector<int> intervals;
321 for (int i = 0; i < starts.size(); ++i) {
322 const int opt_var = NonZeroLiteralFrom(sizes[i]);
323 intervals.push_back(
324 GetOrCreateOptionalInterval(starts[i], sizes[i], opt_var));
325 }
326 return intervals;
327}
328
329int CpModelProtoWithMapping::NonZeroLiteralFrom(VarOrValue size) {
330 if (size.var == kNoVar) {
331 return LookupConstant(size.value > 0);
332 }
333 const auto it = var_to_lit_implies_greater_than_zero.find(size.var);
334 if (it != var_to_lit_implies_greater_than_zero.end()) {
335 return it->second;
336 }
337
338 const IntegerVariableProto& var_proto = proto.variables(size.var);
339 const Domain domain = ReadDomainFromProto(var_proto);
340 DCHECK_GE(domain.Min(), 0);
341 if (domain.Min() > 0) return LookupConstant(1);
342 if (domain.Max() == 0) {
343 return LookupConstant(0);
344 }
345
346 const int var_greater_than_zero_lit = proto.variables_size();
347 IntegerVariableProto* lit_proto = proto.add_variables();
348 lit_proto->add_domain(0);
349 lit_proto->add_domain(1);
350
351 ConstraintProto* is_greater =
352 AddEnforcedConstraint(TrueLiteral(var_greater_than_zero_lit));
353 is_greater->mutable_linear()->add_vars(size.var);
354 is_greater->mutable_linear()->add_coeffs(1);
355 const Domain positive = domain.IntersectionWith({1, domain.Max()});
356 FillDomainInProto(positive, is_greater->mutable_linear());
357
358 ConstraintProto* is_null =
359 AddEnforcedConstraint(FalseLiteral(var_greater_than_zero_lit));
360 is_null->mutable_linear()->add_vars(size.var);
361 is_null->mutable_linear()->add_coeffs(1);
362 is_null->mutable_linear()->add_domain(0);
363 is_null->mutable_linear()->add_domain(0);
364
365 var_to_lit_implies_greater_than_zero[size.var] = var_greater_than_zero_lit;
366 return var_greater_than_zero_lit;
367}
368
369void CpModelProtoWithMapping::FillAMinusBInDomain(
370 const std::vector<int64_t>& domain, const fz::Constraint& fz_ct,
371 ConstraintProto* ct) {
372 auto* arg = ct->mutable_linear();
373 if (fz_ct.arguments[1].type == fz::Argument::INT_VALUE) {
374 const int64_t value = fz_ct.arguments[1].Value();
375 const int var_a = LookupVar(fz_ct.arguments[0]);
376 for (const int64_t domain_bound : domain) {
377 if (domain_bound == std::numeric_limits<int64_t>::min() ||
378 domain_bound == std::numeric_limits<int64_t>::max()) {
379 arg->add_domain(domain_bound);
380 } else {
381 arg->add_domain(domain_bound + value);
382 }
383 }
384 arg->add_vars(var_a);
385 arg->add_coeffs(1);
386 } else if (fz_ct.arguments[0].type == fz::Argument::INT_VALUE) {
387 const int64_t value = fz_ct.arguments[0].Value();
388 const int var_b = LookupVar(fz_ct.arguments[1]);
389 for (int64_t domain_bound : gtl::reversed_view(domain)) {
390 if (domain_bound == std::numeric_limits<int64_t>::min()) {
391 arg->add_domain(std::numeric_limits<int64_t>::max());
392 } else if (domain_bound == std::numeric_limits<int64_t>::max()) {
393 arg->add_domain(std::numeric_limits<int64_t>::min());
394 } else {
395 arg->add_domain(value - domain_bound);
396 }
397 }
398 arg->add_vars(var_b);
399 arg->add_coeffs(1);
400 } else {
401 for (const int64_t domain_bound : domain) arg->add_domain(domain_bound);
402 arg->add_vars(LookupVar(fz_ct.arguments[0]));
403 arg->add_coeffs(1);
404 arg->add_vars(LookupVar(fz_ct.arguments[1]));
405 arg->add_coeffs(-1);
406 }
407}
408
409void CpModelProtoWithMapping::FillLinearConstraintWithGivenDomain(
410 absl::Span<const int64_t> domain, const fz::Constraint& fz_ct,
411 ConstraintProto* ct) {
412 auto* arg = ct->mutable_linear();
413 for (const int64_t domain_bound : domain) arg->add_domain(domain_bound);
414 std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
415 for (int i = 0; i < vars.size(); ++i) {
416 arg->add_vars(vars[i]);
417 arg->add_coeffs(fz_ct.arguments[0].values[i]);
418 }
419}
420
421void CpModelProtoWithMapping::BuildTableFromDomainIntLinEq(
422 const fz::Constraint& fz_ct, ConstraintProto* ct) {
423 const std::vector<int64_t>& coeffs = fz_ct.arguments[0].values;
424 const std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
425 const int rhs = fz_ct.arguments[2].Value();
426 CHECK_EQ(coeffs.back(), -1);
427 for (const int var : vars) {
428 LinearExpressionProto* expr = ct->mutable_table()->add_exprs();
429 expr->add_vars(var);
430 expr->add_coeffs(1);
431 }
432
433 switch (vars.size()) {
434 case 3: {
435 const Domain domain0 = ReadDomainFromProto(proto.variables(vars[0]));
436 const Domain domain1 = ReadDomainFromProto(proto.variables(vars[1]));
437 for (const int64_t v0 : domain0.Values()) {
438 for (const int64_t v1 : domain1.Values()) {
439 const int64_t v2 = coeffs[0] * v0 + coeffs[1] * v1 - rhs;
440 ct->mutable_table()->add_values(v0);
441 ct->mutable_table()->add_values(v1);
442 ct->mutable_table()->add_values(v2);
443 }
444 }
445 break;
446 }
447 case 4: {
448 const Domain domain0 = ReadDomainFromProto(proto.variables(vars[0]));
449 const Domain domain1 = ReadDomainFromProto(proto.variables(vars[1]));
450 const Domain domain2 = ReadDomainFromProto(proto.variables(vars[2]));
451 for (const int64_t v0 : domain0.Values()) {
452 for (const int64_t v1 : domain1.Values()) {
453 for (const int64_t v2 : domain2.Values()) {
454 const int64_t v3 =
455 coeffs[0] * v0 + coeffs[1] * v1 + coeffs[2] * v2 - rhs;
456 ct->mutable_table()->add_values(v0);
457 ct->mutable_table()->add_values(v1);
458 ct->mutable_table()->add_values(v2);
459 ct->mutable_table()->add_values(v3);
460 }
461 }
462 }
463 break;
464 }
465 default:
466 LOG(FATAL) << "Unsupported size";
467 }
468}
469
470void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
471 ConstraintProto* ct) {
472 if (fz_ct.type == "false_constraint") {
473 // An empty clause is always false.
474 ct->mutable_bool_or();
475 } else if (fz_ct.type == "bool_clause") {
476 auto* arg = ct->mutable_bool_or();
477 for (const int var : LookupVars(fz_ct.arguments[0])) {
478 arg->add_literals(TrueLiteral(var));
479 }
480 for (const int var : LookupVars(fz_ct.arguments[1])) {
481 arg->add_literals(FalseLiteral(var));
482 }
483 } else if (fz_ct.type == "bool_xor") {
484 // This is not the same semantics as the array_bool_xor as this constraint
485 // is actually a fully reified xor(a, b) <==> x.
486 const int a = LookupVar(fz_ct.arguments[0]);
487 const int b = LookupVar(fz_ct.arguments[1]);
488 const int x = LookupVar(fz_ct.arguments[2]);
489
490 // not(x) => a == b
491 ct->add_enforcement_literal(NegatedRef(x));
492 auto* const refute = ct->mutable_linear();
493 refute->add_vars(a);
494 refute->add_coeffs(1);
495 refute->add_vars(b);
496 refute->add_coeffs(-1);
497 refute->add_domain(0);
498 refute->add_domain(0);
499
500 // x => a + b == 1
501 auto* enforce = AddEnforcedConstraint(x)->mutable_linear();
502 enforce->add_vars(a);
503 enforce->add_coeffs(1);
504 enforce->add_vars(b);
505 enforce->add_coeffs(1);
506 enforce->add_domain(1);
507 enforce->add_domain(1);
508 } else if (fz_ct.type == "array_bool_or") {
509 auto* arg = ct->mutable_bool_or();
510 for (const int var : LookupVars(fz_ct.arguments[0])) {
511 arg->add_literals(TrueLiteral(var));
512 }
513 } else if (fz_ct.type == "array_bool_or_negated") {
514 auto* arg = ct->mutable_bool_and();
515 for (const int var : LookupVars(fz_ct.arguments[0])) {
516 arg->add_literals(FalseLiteral(var));
517 }
518 } else if (fz_ct.type == "array_bool_and") {
519 auto* arg = ct->mutable_bool_and();
520 for (const int var : LookupVars(fz_ct.arguments[0])) {
521 arg->add_literals(TrueLiteral(var));
522 }
523 } else if (fz_ct.type == "array_bool_and_negated") {
524 auto* arg = ct->mutable_bool_or();
525 for (const int var : LookupVars(fz_ct.arguments[0])) {
526 arg->add_literals(FalseLiteral(var));
527 }
528 } else if (fz_ct.type == "array_bool_xor") {
529 auto* arg = ct->mutable_bool_xor();
530 for (const int var : LookupVars(fz_ct.arguments[0])) {
531 arg->add_literals(TrueLiteral(var));
532 }
533 } else if (fz_ct.type == "bool_le" || fz_ct.type == "int_le") {
534 FillAMinusBInDomain({std::numeric_limits<int64_t>::min(), 0}, fz_ct, ct);
535 } else if (fz_ct.type == "bool_ge" || fz_ct.type == "int_ge") {
536 FillAMinusBInDomain({0, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
537 } else if (fz_ct.type == "bool_lt" || fz_ct.type == "int_lt") {
538 FillAMinusBInDomain({std::numeric_limits<int64_t>::min(), -1}, fz_ct, ct);
539 } else if (fz_ct.type == "bool_gt" || fz_ct.type == "int_gt") {
540 FillAMinusBInDomain({1, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
541 } else if (fz_ct.type == "bool_eq" || fz_ct.type == "int_eq" ||
542 fz_ct.type == "bool2int") {
543 FillAMinusBInDomain({0, 0}, fz_ct, ct);
544 } else if (fz_ct.type == "bool_ne" || fz_ct.type == "bool_not") {
545 auto* arg = ct->mutable_linear();
546 arg->add_vars(LookupVar(fz_ct.arguments[0]));
547 arg->add_coeffs(1);
548 arg->add_vars(LookupVar(fz_ct.arguments[1]));
549 arg->add_coeffs(1);
550 arg->add_domain(1);
551 arg->add_domain(1);
552 } else if (fz_ct.type == "int_ne") {
553 FillAMinusBInDomain({std::numeric_limits<int64_t>::min(), -1, 1,
554 std::numeric_limits<int64_t>::max()},
555 fz_ct, ct);
556 } else if (fz_ct.type == "int_lin_eq") {
557 // Special case for the index of element 2D and element 3D constraints.
558 if (fz_ct.strong_propagation && fz_ct.arguments[0].Size() >= 3 &&
559 fz_ct.arguments[0].Size() <= 4 &&
560 fz_ct.arguments[0].values.back() == -1) {
561 BuildTableFromDomainIntLinEq(fz_ct, ct);
562 } else {
563 const int64_t rhs = fz_ct.arguments[2].values[0];
564 FillLinearConstraintWithGivenDomain({rhs, rhs}, fz_ct, ct);
565 }
566 } else if (fz_ct.type == "bool_lin_eq") {
567 auto* arg = ct->mutable_linear();
568 const std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
569 for (int i = 0; i < vars.size(); ++i) {
570 arg->add_vars(vars[i]);
571 arg->add_coeffs(fz_ct.arguments[0].values[i]);
572 }
573 if (fz_ct.arguments[2].IsVariable()) {
574 arg->add_vars(LookupVar(fz_ct.arguments[2]));
575 arg->add_coeffs(-1);
576 arg->add_domain(0);
577 arg->add_domain(0);
578 } else {
579 const int64_t v = fz_ct.arguments[2].Value();
580 arg->add_domain(v);
581 arg->add_domain(v);
582 }
583 } else if (fz_ct.type == "int_lin_le" || fz_ct.type == "bool_lin_le") {
584 const int64_t rhs = fz_ct.arguments[2].values[0];
585 FillLinearConstraintWithGivenDomain(
586 {std::numeric_limits<int64_t>::min(), rhs}, fz_ct, ct);
587 } else if (fz_ct.type == "int_lin_lt") {
588 const int64_t rhs = fz_ct.arguments[2].values[0];
589 FillLinearConstraintWithGivenDomain(
590 {std::numeric_limits<int64_t>::min(), rhs - 1}, fz_ct, ct);
591 } else if (fz_ct.type == "int_lin_ge") {
592 const int64_t rhs = fz_ct.arguments[2].values[0];
593 FillLinearConstraintWithGivenDomain(
594 {rhs, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
595 } else if (fz_ct.type == "int_lin_gt") {
596 const int64_t rhs = fz_ct.arguments[2].values[0];
597 FillLinearConstraintWithGivenDomain(
598 {rhs + 1, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
599 } else if (fz_ct.type == "int_lin_ne") {
600 const int64_t rhs = fz_ct.arguments[2].values[0];
601 FillLinearConstraintWithGivenDomain(
602 {std::numeric_limits<int64_t>::min(), rhs - 1, rhs + 1,
603 std::numeric_limits<int64_t>::max()},
604 fz_ct, ct);
605 } else if (fz_ct.type == "set_in") {
606 auto* arg = ct->mutable_linear();
607 arg->add_vars(LookupVar(fz_ct.arguments[0]));
608 arg->add_coeffs(1);
609 if (fz_ct.arguments[1].type == fz::Argument::INT_LIST) {
610 FillDomainInProto(Domain::FromValues(std::vector<int64_t>{
611 fz_ct.arguments[1].values.begin(),
612 fz_ct.arguments[1].values.end()}),
613 arg);
614 } else if (fz_ct.arguments[1].type == fz::Argument::INT_INTERVAL) {
616 Domain(fz_ct.arguments[1].values[0], fz_ct.arguments[1].values[1]),
617 arg);
618 } else {
619 LOG(FATAL) << "Wrong format";
620 }
621 } else if (fz_ct.type == "set_in_negated") {
622 auto* arg = ct->mutable_linear();
623 arg->add_vars(LookupVar(fz_ct.arguments[0]));
624 arg->add_coeffs(1);
625 if (fz_ct.arguments[1].type == fz::Argument::INT_LIST) {
627 Domain::FromValues(
628 std::vector<int64_t>{fz_ct.arguments[1].values.begin(),
629 fz_ct.arguments[1].values.end()})
630 .Complement(),
631 arg);
632 } else if (fz_ct.arguments[1].type == fz::Argument::INT_INTERVAL) {
634 Domain(fz_ct.arguments[1].values[0], fz_ct.arguments[1].values[1])
635 .Complement(),
636 arg);
637 } else {
638 LOG(FATAL) << "Wrong format";
639 }
640 } else if (fz_ct.type == "int_min") {
641 auto* arg = ct->mutable_lin_max();
642 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0], /*negate=*/true);
643 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1], /*negate=*/true);
644 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2], /*negate=*/true);
645 } else if (fz_ct.type == "array_int_minimum" || fz_ct.type == "minimum_int") {
646 auto* arg = ct->mutable_lin_max();
647 *arg->mutable_target() = LookupExpr(fz_ct.arguments[0], /*negate=*/true);
648 for (int i = 0; i < fz_ct.arguments[1].Size(); ++i) {
649 *arg->add_exprs() = LookupExprAt(fz_ct.arguments[1], i, /*negate=*/true);
650 }
651 } else if (fz_ct.type == "int_max") {
652 auto* arg = ct->mutable_lin_max();
653 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
654 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
655 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
656 } else if (fz_ct.type == "array_int_maximum" || fz_ct.type == "maximum_int") {
657 auto* arg = ct->mutable_lin_max();
658 *arg->mutable_target() = LookupExpr(fz_ct.arguments[0]);
659 for (int i = 0; i < fz_ct.arguments[1].Size(); ++i) {
660 *arg->add_exprs() = LookupExprAt(fz_ct.arguments[1], i);
661 }
662 } else if (fz_ct.type == "int_times") {
663 auto* arg = ct->mutable_int_prod();
664 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
665 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
666 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
667 } else if (fz_ct.type == "int_abs") {
668 auto* arg = ct->mutable_lin_max();
669 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
670 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0], /*negate=*/true);
671 *arg->mutable_target() = LookupExpr(fz_ct.arguments[1]);
672 } else if (fz_ct.type == "int_plus") {
673 auto* arg = ct->mutable_linear();
674 FillDomainInProto(Domain(0, 0), arg);
675 arg->add_vars(LookupVar(fz_ct.arguments[0]));
676 arg->add_coeffs(1);
677 arg->add_vars(LookupVar(fz_ct.arguments[1]));
678 arg->add_coeffs(1);
679 arg->add_vars(LookupVar(fz_ct.arguments[2]));
680 arg->add_coeffs(-1);
681 } else if (fz_ct.type == "int_div") {
682 auto* arg = ct->mutable_int_div();
683 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
684 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
685 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
686 } else if (fz_ct.type == "int_mod") {
687 auto* arg = ct->mutable_int_mod();
688 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
689 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
690 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
691 } else if (fz_ct.type == "array_int_element" ||
692 fz_ct.type == "array_bool_element" ||
693 fz_ct.type == "array_var_int_element" ||
694 fz_ct.type == "array_var_bool_element" ||
695 fz_ct.type == "array_int_element_nonshifted") {
696 auto* arg = ct->mutable_element();
697 *arg->mutable_linear_index() = LookupExpr(fz_ct.arguments[0]);
698 if (!absl::EndsWith(fz_ct.type, "_nonshifted")) {
699 arg->mutable_linear_index()->set_offset(arg->linear_index().offset() - 1);
700 }
701 *arg->mutable_linear_target() = LookupExpr(fz_ct.arguments[2]);
702
703 for (const VarOrValue elem : LookupVarsOrValues(fz_ct.arguments[1])) {
704 auto* elem_proto = ct->mutable_element()->add_exprs();
705 if (elem.var != kNoVar) {
706 elem_proto->add_vars(elem.var);
707 elem_proto->add_coeffs(1);
708 } else {
709 elem_proto->set_offset(elem.value);
710 }
711 }
712 } else if (fz_ct.type == "ortools_array_int_element" ||
713 fz_ct.type == "ortools_array_bool_element" ||
714 fz_ct.type == "ortools_array_var_int_element" ||
715 fz_ct.type == "ortools_array_var_bool_element") {
716 auto* arg = ct->mutable_element();
717
718 // Index.
719 *arg->mutable_linear_index() = LookupExpr(fz_ct.arguments[0]);
720 const int64_t index_min = fz_ct.arguments[1].values[0];
721 arg->mutable_linear_index()->set_offset(arg->linear_index().offset() -
722 index_min);
723
724 // Target.
725 *arg->mutable_linear_target() = LookupExpr(fz_ct.arguments[3]);
726
727 // Expressions.
728 for (const VarOrValue elem : LookupVarsOrValues(fz_ct.arguments[2])) {
729 auto* elem_proto = ct->mutable_element()->add_exprs();
730 if (elem.var != kNoVar) {
731 elem_proto->add_vars(elem.var);
732 elem_proto->add_coeffs(1);
733 } else {
734 elem_proto->set_offset(elem.value);
735 }
736 }
737 } else if (fz_ct.type == "ortools_table_int") {
738 auto* arg = ct->mutable_table();
739 for (const VarOrValue v : LookupVarsOrValues(fz_ct.arguments[0])) {
740 LinearExpressionProto* expr = arg->add_exprs();
741 if (v.var != kNoVar) {
742 expr->add_vars(v.var);
743 expr->add_coeffs(1);
744 } else {
745 expr->set_offset(v.value);
746 }
747 }
748 for (const int64_t value : fz_ct.arguments[1].values)
749 arg->add_values(value);
750 } else if (fz_ct.type == "ortools_regular") {
751 auto* arg = ct->mutable_automaton();
752 for (const VarOrValue v : LookupVarsOrValues(fz_ct.arguments[0])) {
753 LinearExpressionProto* expr = arg->add_exprs();
754 if (v.var != kNoVar) {
755 expr->add_vars(v.var);
756 expr->add_coeffs(1);
757 } else {
758 expr->set_offset(v.value);
759 }
760 }
761
762 int count = 0;
763 const int num_states = fz_ct.arguments[1].Value();
764 const int num_values = fz_ct.arguments[2].Value();
765 for (int i = 1; i <= num_states; ++i) {
766 for (int j = 1; j <= num_values; ++j) {
767 CHECK_LT(count, fz_ct.arguments[3].values.size());
768 const int next = fz_ct.arguments[3].values[count++];
769 if (next == 0) continue; // 0 is a failing state.
770 arg->add_transition_tail(i);
771 arg->add_transition_label(j);
772 arg->add_transition_head(next);
773 }
774 }
775
776 arg->set_starting_state(fz_ct.arguments[4].Value());
777 switch (fz_ct.arguments[5].type) {
778 case fz::Argument::INT_VALUE: {
779 arg->add_final_states(fz_ct.arguments[5].values[0]);
780 break;
781 }
782 case fz::Argument::INT_INTERVAL: {
783 for (int v = fz_ct.arguments[5].values[0];
784 v <= fz_ct.arguments[5].values[1]; ++v) {
785 arg->add_final_states(v);
786 }
787 break;
788 }
789 case fz::Argument::INT_LIST: {
790 for (const int v : fz_ct.arguments[5].values) {
791 arg->add_final_states(v);
792 }
793 break;
794 }
795 default: {
796 LOG(FATAL) << "Wrong constraint " << fz_ct.DebugString();
797 }
798 }
799 } else if (fz_ct.type == "fzn_all_different_int") {
800 auto* arg = ct->mutable_all_diff();
801 for (int i = 0; i < fz_ct.arguments[0].Size(); ++i) {
802 *arg->add_exprs() = LookupExprAt(fz_ct.arguments[0], i);
803 }
804 } else if (fz_ct.type == "ortools_circuit" ||
805 fz_ct.type == "ortools_subcircuit") {
806 const int64_t min_index = fz_ct.arguments[1].Value();
807 const int size = std::max(fz_ct.arguments[0].values.size(),
808 fz_ct.arguments[0].variables.size());
809
810 const int64_t max_index = min_index + size - 1;
811 // The arc-based mutable circuit.
812 auto* circuit_arg = ct->mutable_circuit();
813
814 // We fully encode all variables so we can use the literal based circuit.
815 // TODO(user): avoid fully encoding more than once?
816 int64_t index = min_index;
817 const bool is_circuit = (fz_ct.type == "ortools_circuit");
818 for (const int var : LookupVars(fz_ct.arguments[0])) {
819 Domain domain = ReadDomainFromProto(proto.variables(var));
820
821 // Restrict the domain of var to [min_index, max_index]
822 domain = domain.IntersectionWith(Domain(min_index, max_index));
823 if (is_circuit) {
824 // We simply make sure that the variable cannot take the value index.
825 domain = domain.IntersectionWith(Domain::FromIntervals(
826 {{std::numeric_limits<int64_t>::min(), index - 1},
827 {index + 1, std::numeric_limits<int64_t>::max()}}));
828 }
829 FillDomainInProto(domain, proto.mutable_variables(var));
830
831 for (const ClosedInterval interval : domain) {
832 for (int64_t value = interval.start; value <= interval.end; ++value) {
833 // Create one Boolean variable for this arc.
834 const int literal = proto.variables_size();
835 {
836 auto* new_var = proto.add_variables();
837 new_var->add_domain(0);
838 new_var->add_domain(1);
839 }
840
841 // Add the arc.
842 circuit_arg->add_tails(index);
843 circuit_arg->add_heads(value);
844 circuit_arg->add_literals(literal);
845
846 // literal => var == value.
847 {
848 auto* lin = AddEnforcedConstraint(literal)->mutable_linear();
849 lin->add_coeffs(1);
850 lin->add_vars(var);
851 lin->add_domain(value);
852 lin->add_domain(value);
853 }
854
855 // not(literal) => var != value
856 {
857 auto* lin =
858 AddEnforcedConstraint(NegatedRef(literal))->mutable_linear();
859 lin->add_coeffs(1);
860 lin->add_vars(var);
861 lin->add_domain(std::numeric_limits<int64_t>::min());
862 lin->add_domain(value - 1);
863 lin->add_domain(value + 1);
864 lin->add_domain(std::numeric_limits<int64_t>::max());
865 }
866 }
867 }
868
869 ++index;
870 }
871 } else if (fz_ct.type == "ortools_inverse") {
872 auto* arg = ct->mutable_inverse();
873
874 const auto direct_variables = LookupVars(fz_ct.arguments[0]);
875 const auto inverse_variables = LookupVars(fz_ct.arguments[1]);
876 const int base_direct = fz_ct.arguments[2].Value();
877 const int base_inverse = fz_ct.arguments[3].Value();
878
879 CHECK_EQ(direct_variables.size(), inverse_variables.size());
880 const int num_variables = direct_variables.size();
881 const int end_direct = base_direct + num_variables;
882 const int end_inverse = base_inverse + num_variables;
883
884 // Any convention that maps the "fixed values" to the one of the inverse and
885 // back works. We decided to follow this one:
886 // There are 3 cases:
887 // (A) base_direct == base_inverse, we fill the arrays
888 // direct = [0, .., base_direct - 1] U [direct_vars]
889 // inverse = [0, .., base_direct - 1] U [inverse_vars]
890 // (B) base_direct == base_inverse + offset (> 0), we fill the arrays
891 // direct = [0, .., base_inverse - 1] U
892 // [end_inverse, .., end_inverse + offset - 1] U
893 // [direct_vars]
894 // inverse = [0, .., base_inverse - 1] U
895 // [inverse_vars] U
896 // [base_inverse, .., base_base_inverse + offset - 1]
897 // (C): base_inverse == base_direct + offset (> 0), we fill the arrays
898 // direct = [0, .., base_direct - 1] U
899 // [direct_vars] U
900 // [base_direct, .., base_direct + offset - 1]
901 // inverse [0, .., base_direct - 1] U
902 // [end_direct, .., end_direct + offset - 1] U
903 // [inverse_vars]
904 const int arity = std::max(base_inverse, base_direct) + num_variables;
905 for (int i = 0; i < arity; ++i) {
906 // Fill the direct array.
907 if (i < base_direct) {
908 if (i < base_inverse) {
909 arg->add_f_direct(LookupConstant(i));
910 } else if (i >= base_inverse) {
911 arg->add_f_direct(LookupConstant(i + num_variables));
912 }
913 } else if (i >= base_direct && i < end_direct) {
914 arg->add_f_direct(direct_variables[i - base_direct]);
915 } else {
916 arg->add_f_direct(LookupConstant(i - num_variables));
917 }
918
919 // Fill the inverse array.
920 if (i < base_inverse) {
921 if (i < base_direct) {
922 arg->add_f_inverse(LookupConstant(i));
923 } else if (i >= base_direct) {
924 arg->add_f_inverse(LookupConstant(i + num_variables));
925 }
926 } else if (i >= base_inverse && i < end_inverse) {
927 arg->add_f_inverse(inverse_variables[i - base_inverse]);
928 } else {
929 arg->add_f_inverse(LookupConstant(i - num_variables));
930 }
931 }
932 } else if (fz_ct.type == "fzn_disjunctive") {
933 const std::vector<VarOrValue> starts =
934 LookupVarsOrValues(fz_ct.arguments[0]);
935 const std::vector<VarOrValue> sizes =
936 LookupVarsOrValues(fz_ct.arguments[1]);
937
938 auto* arg = ct->mutable_cumulative();
939 arg->mutable_capacity()->set_offset(1);
940 for (int i = 0; i < starts.size(); ++i) {
941 arg->add_intervals(
942 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
943 arg->add_demands()->set_offset(1);
944 }
945 } else if (fz_ct.type == "fzn_disjunctive_strict") {
946 const std::vector<VarOrValue> starts =
947 LookupVarsOrValues(fz_ct.arguments[0]);
948 const std::vector<VarOrValue> sizes =
949 LookupVarsOrValues(fz_ct.arguments[1]);
950
951 auto* arg = ct->mutable_no_overlap();
952 for (int i = 0; i < starts.size(); ++i) {
953 arg->add_intervals(
954 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
955 }
956 } else if (fz_ct.type == "fzn_cumulative") {
957 const std::vector<VarOrValue> starts =
958 LookupVarsOrValues(fz_ct.arguments[0]);
959 const std::vector<VarOrValue> sizes =
960 LookupVarsOrValues(fz_ct.arguments[1]);
961 const std::vector<VarOrValue> demands =
962 LookupVarsOrValues(fz_ct.arguments[2]);
963
964 auto* arg = ct->mutable_cumulative();
965 if (fz_ct.arguments[3].HasOneValue()) {
966 arg->mutable_capacity()->set_offset(fz_ct.arguments[3].Value());
967 } else {
968 arg->mutable_capacity()->add_vars(LookupVar(fz_ct.arguments[3]));
969 arg->mutable_capacity()->add_coeffs(1);
970 }
971 for (int i = 0; i < starts.size(); ++i) {
972 // Special case for a 0-1 demand, we mark the interval as optional
973 // instead and fix the demand to 1.
974 if (demands[i].var != kNoVar &&
975 proto.variables(demands[i].var).domain().size() == 2 &&
976 proto.variables(demands[i].var).domain(0) == 0 &&
977 proto.variables(demands[i].var).domain(1) == 1 &&
978 fz_ct.arguments[3].HasOneValue() && fz_ct.arguments[3].Value() == 1) {
979 arg->add_intervals(
980 GetOrCreateOptionalInterval(starts[i], sizes[i], demands[i].var));
981 arg->add_demands()->set_offset(1);
982 } else {
983 arg->add_intervals(
984 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
985 LinearExpressionProto* demand = arg->add_demands();
986 if (demands[i].var == kNoVar) {
987 demand->set_offset(demands[i].value);
988 } else {
989 demand->add_vars(demands[i].var);
990 demand->add_coeffs(1);
991 }
992 }
993 }
994 } else if (fz_ct.type == "ortools_cumulative_opt") {
995 const std::vector<int> occurs = LookupVars(fz_ct.arguments[0]);
996 const std::vector<VarOrValue> starts =
997 LookupVarsOrValues(fz_ct.arguments[1]);
998 const std::vector<VarOrValue> durations =
999 LookupVarsOrValues(fz_ct.arguments[2]);
1000 const std::vector<VarOrValue> demands =
1001 LookupVarsOrValues(fz_ct.arguments[3]);
1002
1003 auto* arg = ct->mutable_cumulative();
1004 if (fz_ct.arguments[3].HasOneValue()) {
1005 arg->mutable_capacity()->set_offset(fz_ct.arguments[4].Value());
1006 } else {
1007 arg->mutable_capacity()->add_vars(LookupVar(fz_ct.arguments[4]));
1008 arg->mutable_capacity()->add_coeffs(1);
1009 }
1010 for (int i = 0; i < starts.size(); ++i) {
1011 arg->add_intervals(
1012 GetOrCreateOptionalInterval(starts[i], durations[i], occurs[i]));
1013 LinearExpressionProto* demand = arg->add_demands();
1014 if (demands[i].var == kNoVar) {
1015 demand->set_offset(demands[i].value);
1016 } else {
1017 demand->add_vars(demands[i].var);
1018 demand->add_coeffs(1);
1019 }
1020 }
1021 } else if (fz_ct.type == "ortools_disjunctive_strict_opt") {
1022 const std::vector<int> occurs = LookupVars(fz_ct.arguments[0]);
1023 const std::vector<VarOrValue> starts =
1024 LookupVarsOrValues(fz_ct.arguments[1]);
1025 const std::vector<VarOrValue> durations =
1026 LookupVarsOrValues(fz_ct.arguments[2]);
1027
1028 auto* arg = ct->mutable_no_overlap();
1029 for (int i = 0; i < starts.size(); ++i) {
1030 arg->add_intervals(
1031 GetOrCreateOptionalInterval(starts[i], durations[i], occurs[i]));
1032 }
1033 } else if (fz_ct.type == "fzn_diffn" || fz_ct.type == "fzn_diffn_nonstrict") {
1034 const bool is_strict = fz_ct.type == "fzn_diffn";
1035 const std::vector<VarOrValue> x = LookupVarsOrValues(fz_ct.arguments[0]);
1036 const std::vector<VarOrValue> y = LookupVarsOrValues(fz_ct.arguments[1]);
1037 const std::vector<VarOrValue> dx = LookupVarsOrValues(fz_ct.arguments[2]);
1038 const std::vector<VarOrValue> dy = LookupVarsOrValues(fz_ct.arguments[3]);
1039 const std::vector<int> x_intervals =
1040 is_strict ? CreateIntervals(x, dx)
1041 : CreateNonZeroOrOptionalIntervals(x, dx);
1042 const std::vector<int> y_intervals =
1043 is_strict ? CreateIntervals(y, dy)
1044 : CreateNonZeroOrOptionalIntervals(y, dy);
1045 auto* arg = ct->mutable_no_overlap_2d();
1046 for (int i = 0; i < x.size(); ++i) {
1047 arg->add_x_intervals(x_intervals[i]);
1048 arg->add_y_intervals(y_intervals[i]);
1049 }
1050 } else if (fz_ct.type == "ortools_network_flow" ||
1051 fz_ct.type == "ortools_network_flow_cost") {
1052 // Note that we leave ct empty here (with just the name set).
1053 // We simply do a linear encoding of this constraint.
1054 const bool has_cost = fz_ct.type == "ortools_network_flow_cost";
1055 const std::vector<int> flow = LookupVars(fz_ct.arguments[3]);
1056
1057 // Flow conservation constraints.
1058 const int num_nodes = fz_ct.arguments[1].values.size();
1059 const int base_node = fz_ct.arguments[2].Value();
1060 std::vector<std::vector<int>> flows_per_node(num_nodes);
1061 std::vector<std::vector<int>> coeffs_per_node(num_nodes);
1062
1063 const int num_arcs = fz_ct.arguments[0].values.size() / 2;
1064 for (int arc = 0; arc < num_arcs; arc++) {
1065 const int tail = fz_ct.arguments[0].values[2 * arc] - base_node;
1066 const int head = fz_ct.arguments[0].values[2 * arc + 1] - base_node;
1067 if (tail == head) continue;
1068
1069 flows_per_node[tail].push_back(flow[arc]);
1070 coeffs_per_node[tail].push_back(1);
1071 flows_per_node[head].push_back(flow[arc]);
1072 coeffs_per_node[head].push_back(-1);
1073 }
1074 for (int node = 0; node < num_nodes; node++) {
1075 auto* arg = proto.add_constraints()->mutable_linear();
1076 arg->add_domain(fz_ct.arguments[1].values[node]);
1077 arg->add_domain(fz_ct.arguments[1].values[node]);
1078 for (int i = 0; i < flows_per_node[node].size(); ++i) {
1079 arg->add_vars(flows_per_node[node][i]);
1080 arg->add_coeffs(coeffs_per_node[node][i]);
1081 }
1082 }
1083
1084 if (has_cost) {
1085 auto* arg = proto.add_constraints()->mutable_linear();
1086 arg->add_domain(0);
1087 arg->add_domain(0);
1088 for (int arc = 0; arc < num_arcs; arc++) {
1089 const int64_t weight = fz_ct.arguments[4].values[arc];
1090 if (weight != 0) {
1091 arg->add_vars(flow[arc]);
1092 arg->add_coeffs(weight);
1093 }
1094 }
1095 arg->add_vars(LookupVar(fz_ct.arguments[5]));
1096 arg->add_coeffs(-1);
1097 }
1098 } else {
1099 LOG(FATAL) << " Not supported " << fz_ct.type;
1100 }
1101} // NOLINT(readability/fn_size)
1102
1103void CpModelProtoWithMapping::FillReifOrImpliedConstraint(
1104 const fz::Constraint& fz_ct, ConstraintProto* ct) {
1105 // Start by adding a non-reified version of the same constraint.
1106 std::string simplified_type;
1107 if (absl::EndsWith(fz_ct.type, "_reif")) {
1108 // Remove _reif.
1109 simplified_type = fz_ct.type.substr(0, fz_ct.type.size() - 5);
1110 } else if (absl::EndsWith(fz_ct.type, "_imp")) {
1111 // Remove _imp.
1112 simplified_type = fz_ct.type.substr(0, fz_ct.type.size() - 4);
1113 } else {
1114 // Keep name as it is an implicit reified constraint.
1115 simplified_type = fz_ct.type;
1116 }
1117
1118 // We need a copy to be able to change the type of the constraint.
1119 fz::Constraint copy = fz_ct;
1120 copy.type = simplified_type;
1121
1122 // Create the CP-SAT constraint.
1123 FillConstraint(copy, ct);
1124
1125 // In case of reified constraints, the type of the opposite constraint.
1126 std::string negated_type;
1127
1128 // Fill enforcement_literal and set copy.type to the negated constraint.
1129 if (simplified_type == "array_bool_or") {
1130 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[1])));
1131 negated_type = "array_bool_or_negated";
1132 } else if (simplified_type == "array_bool_and") {
1133 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[1])));
1134 negated_type = "array_bool_and_negated";
1135 } else if (simplified_type == "set_in") {
1136 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1137 negated_type = "set_in_negated";
1138 } else if (simplified_type == "bool_eq" || simplified_type == "int_eq") {
1139 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1140 negated_type = "int_ne";
1141 } else if (simplified_type == "bool_ne" || simplified_type == "int_ne") {
1142 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1143 negated_type = "int_eq";
1144 } else if (simplified_type == "bool_le" || simplified_type == "int_le") {
1145 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1146 negated_type = "int_gt";
1147 } else if (simplified_type == "bool_lt" || simplified_type == "int_lt") {
1148 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1149 negated_type = "int_ge";
1150 } else if (simplified_type == "bool_ge" || simplified_type == "int_ge") {
1151 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1152 negated_type = "int_lt";
1153 } else if (simplified_type == "bool_gt" || simplified_type == "int_gt") {
1154 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1155 negated_type = "int_le";
1156 } else if (simplified_type == "int_lin_eq") {
1157 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1158 negated_type = "int_lin_ne";
1159 } else if (simplified_type == "int_lin_ne") {
1160 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1161 negated_type = "int_lin_eq";
1162 } else if (simplified_type == "int_lin_le") {
1163 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1164 negated_type = "int_lin_gt";
1165 } else if (simplified_type == "int_lin_ge") {
1166 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1167 negated_type = "int_lin_lt";
1168 } else if (simplified_type == "int_lin_lt") {
1169 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1170 negated_type = "int_lin_ge";
1171 } else if (simplified_type == "int_lin_gt") {
1172 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1173 negated_type = "int_lin_le";
1174 } else {
1175 LOG(FATAL) << "Unsupported " << simplified_type;
1176 }
1177
1178 // One way implication. We can stop here.
1179 if (absl::EndsWith(fz_ct.type, "_imp")) return;
1180
1181 // Add the other side of the reification because CpModelProto only support
1182 // half reification.
1183 ConstraintProto* negated_ct = proto.add_constraints();
1184 negated_ct->set_name(fz_ct.type + " (negated)");
1185 negated_ct->add_enforcement_literal(
1186 sat::NegatedRef(ct->enforcement_literal(0)));
1187 copy.type = negated_type;
1188 FillConstraint(copy, negated_ct);
1189}
1190
1191void CpModelProtoWithMapping::TranslateSearchAnnotations(
1192 absl::Span<const fz::Annotation> search_annotations, SolverLogger* logger) {
1193 std::vector<fz::Annotation> flat_annotations;
1194 for (const fz::Annotation& annotation : search_annotations) {
1195 fz::FlattenAnnotations(annotation, &flat_annotations);
1196 }
1197
1198 // CP-SAT rejects models containing variables duplicated in hints.
1199 absl::flat_hash_set<int> hinted_vars;
1200
1201 for (const fz::Annotation& annotation : flat_annotations) {
1202 if (annotation.IsFunctionCallWithIdentifier("warm_start")) {
1203 CHECK_EQ(2, annotation.annotations.size());
1204 const fz::Annotation& vars = annotation.annotations[0];
1205 const fz::Annotation& values = annotation.annotations[1];
1206 if (vars.type != fz::Annotation::VAR_REF_ARRAY ||
1207 values.type != fz::Annotation::INT_LIST) {
1208 continue;
1209 }
1210 for (int i = 0; i < vars.variables.size(); ++i) {
1211 fz::Variable* fz_var = vars.variables[i];
1212 const int var = fz_var_to_index.at(fz_var);
1213 const int64_t value = values.values[i];
1214 if (hinted_vars.insert(var).second) {
1215 proto.mutable_solution_hint()->add_vars(var);
1216 proto.mutable_solution_hint()->add_values(value);
1217 }
1218 }
1219 } else if (annotation.IsFunctionCallWithIdentifier("int_search") ||
1220 annotation.IsFunctionCallWithIdentifier("bool_search")) {
1221 const std::vector<fz::Annotation>& args = annotation.annotations;
1222 std::vector<fz::Variable*> vars;
1223 args[0].AppendAllVariables(&vars);
1224
1225 DecisionStrategyProto* strategy = proto.add_search_strategy();
1226 for (fz::Variable* v : vars) {
1227 strategy->add_variables(fz_var_to_index.at(v));
1228 }
1229
1230 const fz::Annotation& choose = args[1];
1231 if (choose.id == "input_order") {
1232 strategy->set_variable_selection_strategy(
1233 DecisionStrategyProto::CHOOSE_FIRST);
1234 } else if (choose.id == "first_fail") {
1235 strategy->set_variable_selection_strategy(
1236 DecisionStrategyProto::CHOOSE_MIN_DOMAIN_SIZE);
1237 } else if (choose.id == "anti_first_fail") {
1238 strategy->set_variable_selection_strategy(
1239 DecisionStrategyProto::CHOOSE_MAX_DOMAIN_SIZE);
1240 } else if (choose.id == "smallest") {
1241 strategy->set_variable_selection_strategy(
1242 DecisionStrategyProto::CHOOSE_LOWEST_MIN);
1243 } else if (choose.id == "largest") {
1244 strategy->set_variable_selection_strategy(
1245 DecisionStrategyProto::CHOOSE_HIGHEST_MAX);
1246 } else {
1247 SOLVER_LOG(logger, "Unsupported variable selection strategy '",
1248 choose.id, "', falling back to 'smallest'");
1249 strategy->set_variable_selection_strategy(
1250 DecisionStrategyProto::CHOOSE_LOWEST_MIN);
1251 }
1252
1253 const fz::Annotation& select = args[2];
1254 if (select.id == "indomain_min" || select.id == "indomain") {
1255 strategy->set_domain_reduction_strategy(
1256 DecisionStrategyProto::SELECT_MIN_VALUE);
1257 } else if (select.id == "indomain_max") {
1258 strategy->set_domain_reduction_strategy(
1259 DecisionStrategyProto::SELECT_MAX_VALUE);
1260 } else if (select.id == "indomain_split") {
1261 strategy->set_domain_reduction_strategy(
1262 DecisionStrategyProto::SELECT_LOWER_HALF);
1263 } else if (select.id == "indomain_reverse_split") {
1264 strategy->set_domain_reduction_strategy(
1265 DecisionStrategyProto::SELECT_UPPER_HALF);
1266 } else if (select.id == "indomain_median") {
1267 strategy->set_domain_reduction_strategy(
1268 DecisionStrategyProto::SELECT_MEDIAN_VALUE);
1269 } else {
1270 SOLVER_LOG(logger, "Unsupported value selection strategy '", select.id,
1271 "', falling back to 'indomain_min'");
1272 strategy->set_domain_reduction_strategy(
1273 DecisionStrategyProto::SELECT_MIN_VALUE);
1274 }
1275 }
1276 }
1277}
1278
1279// The format is fixed in the flatzinc specification.
1280std::string SolutionString(
1281 const fz::SolutionOutputSpecs& output,
1282 const std::function<int64_t(fz::Variable*)>& value_func,
1283 double objective_value) {
1284 if (output.variable != nullptr && !output.variable->domain.is_float) {
1285 const int64_t value = value_func(output.variable);
1286 if (output.display_as_boolean) {
1287 return absl::StrCat(output.name, " = ", value == 1 ? "true" : "false",
1288 ";");
1289 } else {
1290 return absl::StrCat(output.name, " = ", value, ";");
1291 }
1292 } else if (output.variable != nullptr && output.variable->domain.is_float) {
1293 return absl::StrCat(output.name, " = ", objective_value, ";");
1294 } else {
1295 const int bound_size = output.bounds.size();
1296 std::string result =
1297 absl::StrCat(output.name, " = array", bound_size, "d(");
1298 for (int i = 0; i < bound_size; ++i) {
1299 if (output.bounds[i].max_value >= output.bounds[i].min_value) {
1300 absl::StrAppend(&result, output.bounds[i].min_value, "..",
1301 output.bounds[i].max_value, ", ");
1302 } else {
1303 result.append("{},");
1304 }
1305 }
1306 result.append("[");
1307 for (int i = 0; i < output.flat_variables.size(); ++i) {
1308 const int64_t value = value_func(output.flat_variables[i]);
1309 if (output.display_as_boolean) {
1310 result.append(value ? "true" : "false");
1311 } else {
1312 absl::StrAppend(&result, value);
1313 }
1314 if (i != output.flat_variables.size() - 1) {
1315 result.append(", ");
1316 }
1317 }
1318 result.append("]);");
1319 return result;
1320 }
1321 return "";
1322}
1323
1324std::string SolutionString(
1325 const fz::Model& model,
1326 const std::function<int64_t(fz::Variable*)>& value_func,
1327 double objective_value) {
1328 std::string solution_string;
1329 for (const auto& output_spec : model.output()) {
1330 solution_string.append(
1331 SolutionString(output_spec, value_func, objective_value));
1332 solution_string.append("\n");
1333 }
1334 return solution_string;
1335}
1336
1337void OutputFlatzincStats(const CpSolverResponse& response,
1338 SolverLogger* solution_logger) {
1339 SOLVER_LOG(solution_logger,
1340 "%%%mzn-stat: objective=", response.objective_value());
1341 SOLVER_LOG(solution_logger,
1342 "%%%mzn-stat: objectiveBound=", response.best_objective_bound());
1343 SOLVER_LOG(solution_logger,
1344 "%%%mzn-stat: boolVariables=", response.num_booleans());
1345 SOLVER_LOG(solution_logger,
1346 "%%%mzn-stat: failures=", response.num_conflicts());
1347 SOLVER_LOG(
1348 solution_logger, "%%%mzn-stat: propagations=",
1349 response.num_binary_propagations() + response.num_integer_propagations());
1350 SOLVER_LOG(solution_logger, "%%%mzn-stat: solveTime=", response.wall_time());
1351}
1352
1353} // namespace
1354
1356 // Scan the model, rename int2float to int_eq, change type of the floating
1357 // point variables to integer.
1358 for (fz::Constraint* ct : fz_model->constraints()) {
1359 if (!ct->active) continue;
1360 if (ct->type == "int2float") {
1361 ct->type = "int_eq";
1362 fz::Domain& float_domain = ct->arguments[1].variables[0]->domain;
1363 float_domain.is_float = false;
1364 for (const double float_value : float_domain.float_values) {
1365 float_domain.values.push_back(static_cast<int64_t>(float_value));
1366 }
1367 float_domain.float_values.clear();
1368 }
1369 }
1370
1371 // Scan the model to find the float objective variable and the float objective
1372 // constraint if defined.
1373 fz::Variable* float_objective_var = nullptr;
1374 for (fz::Variable* var : fz_model->variables()) {
1375 if (!var->active) continue;
1376 if (var->domain.is_float) {
1377 CHECK(float_objective_var == nullptr);
1378 float_objective_var = var;
1379 }
1380 }
1381
1382 fz::Constraint* float_objective_ct = nullptr;
1383 if (float_objective_var != nullptr) {
1384 for (fz::Constraint* ct : fz_model->constraints()) {
1385 if (!ct->active) continue;
1386 if (ct->type == "float_lin_eq") {
1387 CHECK(float_objective_ct == nullptr);
1388 float_objective_ct = ct;
1389 break;
1390 }
1391 }
1392 }
1393
1394 if (float_objective_ct != nullptr || float_objective_var != nullptr) {
1395 CHECK(float_objective_ct != nullptr);
1396 CHECK(float_objective_var != nullptr);
1397 const int arity = float_objective_ct->arguments[0].Size();
1398 CHECK_EQ(float_objective_ct->arguments[1].variables[arity - 1],
1399 float_objective_var);
1400 CHECK_EQ(float_objective_ct->arguments[0].floats[arity - 1], -1.0);
1401 for (int i = 0; i + 1 < arity; ++i) {
1403 float_objective_ct->arguments[1].variables[i],
1404 float_objective_ct->arguments[0].floats[i]);
1405 }
1407 -float_objective_ct->arguments[2].floats[0]);
1408 fz_model->ClearObjective();
1409 float_objective_var->active = false;
1410 float_objective_ct->active = false;
1411 }
1412}
1413
1416 const std::string& sat_params,
1417 SolverLogger* logger,
1418 SolverLogger* solution_logger) {
1419 CpModelProtoWithMapping m;
1420 m.proto.set_name(fz_model.name());
1421
1422 // The translation is easy, we create one variable per flatzinc variable,
1423 // plus eventually a bunch of constant variables that will be created
1424 // lazily.
1425 int num_variables = 0;
1426 for (fz::Variable* fz_var : fz_model.variables()) {
1427 if (!fz_var->active) continue;
1428 CHECK(!fz_var->domain.is_float)
1429 << "CP-SAT does not support float variables";
1430
1431 m.fz_var_to_index[fz_var] = num_variables++;
1432 IntegerVariableProto* var = m.proto.add_variables();
1433 var->set_name(fz_var->name);
1434 if (fz_var->domain.is_interval) {
1435 if (fz_var->domain.values.empty()) {
1436 // The CP-SAT solver checks that constraints cannot overflow during
1437 // their propagation. Because of that, we trim undefined variable
1438 // domains (i.e. int in minizinc) to something hopefully large enough.
1439 LOG_FIRST_N(WARNING, 1)
1440 << "Using flag --fz_int_max for unbounded integer variables.";
1441 LOG_FIRST_N(WARNING, 1)
1442 << " actual domain is [" << -absl::GetFlag(FLAGS_fz_int_max)
1443 << ".." << absl::GetFlag(FLAGS_fz_int_max) << "]";
1444 var->add_domain(-absl::GetFlag(FLAGS_fz_int_max));
1445 var->add_domain(absl::GetFlag(FLAGS_fz_int_max));
1446 } else {
1447 var->add_domain(fz_var->domain.values[0]);
1448 var->add_domain(fz_var->domain.values[1]);
1449 }
1450 } else {
1451 FillDomainInProto(Domain::FromValues(fz_var->domain.values), var);
1452 }
1453 }
1454
1455 // Translate the constraints.
1456 for (fz::Constraint* fz_ct : fz_model.constraints()) {
1457 if (fz_ct == nullptr || !fz_ct->active) continue;
1458 ConstraintProto* ct = m.proto.add_constraints();
1459 ct->set_name(fz_ct->type);
1460 if (absl::EndsWith(fz_ct->type, "_reif") ||
1461 absl::EndsWith(fz_ct->type, "_imp") || fz_ct->type == "array_bool_or" ||
1462 fz_ct->type == "array_bool_and") {
1463 m.FillReifOrImpliedConstraint(*fz_ct, ct);
1464 } else {
1465 m.FillConstraint(*fz_ct, ct);
1466 }
1467 }
1468
1469 // Fill the objective.
1470 if (fz_model.objective() != nullptr) {
1471 CpObjectiveProto* objective = m.proto.mutable_objective();
1472 if (fz_model.maximize()) {
1473 objective->set_scaling_factor(-1);
1474 objective->add_coeffs(-1);
1475 objective->add_vars(m.fz_var_to_index[fz_model.objective()]);
1476 } else {
1477 objective->add_coeffs(1);
1478 objective->add_vars(m.fz_var_to_index[fz_model.objective()]);
1479 }
1480 } else if (!fz_model.float_objective_variables().empty()) {
1481 FloatObjectiveProto* objective = m.proto.mutable_floating_point_objective();
1482 for (int i = 0; i < fz_model.float_objective_variables().size(); ++i) {
1483 objective->add_vars(
1484 m.fz_var_to_index[fz_model.float_objective_variables()[i]]);
1485 objective->add_coeffs(fz_model.float_objective_coefficients()[i]);
1486 }
1487 objective->set_offset(fz_model.float_objective_offset());
1488 objective->set_maximize(fz_model.maximize());
1489 }
1490
1491 // Fill the search order.
1492 m.TranslateSearchAnnotations(fz_model.search_annotations(), logger);
1493
1494 if (p.search_all_solutions && !m.proto.has_objective()) {
1495 // Enumerate all sat solutions.
1496 m.parameters.set_enumerate_all_solutions(true);
1497 }
1498
1499 m.parameters.set_log_search_progress(p.log_search_progress);
1500 m.parameters.set_log_to_stdout(!p.ortools_mode);
1501
1502 // Helps with challenge unit tests.
1503 m.parameters.set_max_domain_size_when_encoding_eq_neq_constraints(32);
1504
1505 // Computes the number of workers.
1506 int num_workers = 1;
1507 if (p.search_all_solutions && fz_model.objective() == nullptr) {
1508 if (p.number_of_threads > 1) {
1509 // We don't support enumerating all solution in parallel for a SAT
1510 // problem. But note that we do support it for an optimization problem
1511 // since the meaning of p.all_solutions is not the same in this case.
1512 SOLVER_LOG(logger,
1513 "Search for all solutions of a SAT problem in parallel is not "
1514 "supported. Switching back to sequential search.");
1515 }
1516 } else if (p.number_of_threads <= 0) {
1517 // TODO(user): Supports setting the number of workers to 0, which will
1518 // then query the number of cores available. This is complex now as we
1519 // need to still support the expected behabior (no flags -> 1 thread
1520 // fixed search, -f -> 1 thread free search).
1521 SOLVER_LOG(logger,
1522 "The number of search workers, is not specified. For better "
1523 "performances, please set the number of workers to 8, 16, or "
1524 "more depending on the number of cores of your computer.");
1525 } else {
1526 num_workers = p.number_of_threads;
1527 }
1528
1529 // Specifies single thread specific search modes.
1530 if (num_workers == 1 && !p.use_free_search) { // Fixed search.
1531 m.parameters.set_search_branching(SatParameters::FIXED_SEARCH);
1532 m.parameters.set_keep_all_feasible_solutions_in_presolve(true);
1533 } else if (num_workers == 1 && p.use_free_search) { // Free search.
1534 m.parameters.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
1535 if (!p.search_all_solutions && p.ortools_mode) {
1536 m.parameters.set_interleave_search(true);
1537 if (fz_model.objective() != nullptr) {
1538 m.parameters.add_subsolvers("default_lp");
1539 m.parameters.add_subsolvers(
1540 m.proto.search_strategy().empty() ? "quick_restart" : "fixed");
1541 m.parameters.add_subsolvers("core_or_no_lp"),
1542 m.parameters.add_subsolvers("max_lp");
1543
1544 } else {
1545 m.parameters.add_subsolvers("default_lp");
1546 m.parameters.add_subsolvers(
1547 m.proto.search_strategy().empty() ? "probing" : "fixed");
1548 m.parameters.add_subsolvers("no_lp");
1549 m.parameters.add_subsolvers("max_lp");
1550 m.parameters.add_subsolvers("quick_restart");
1551 }
1552 }
1553 } else if (num_workers > 1 && num_workers < 8 && p.ortools_mode) {
1554 SOLVER_LOG(logger, "Bumping number of workers from ", num_workers, " to 8");
1555 num_workers = 8;
1556 }
1557 m.parameters.set_num_workers(num_workers);
1558
1559 // Time limit.
1560 if (p.max_time_in_seconds > 0) {
1561 m.parameters.set_max_time_in_seconds(p.max_time_in_seconds);
1562 }
1563
1564 // The order is important, we want the flag parameters to overwrite anything
1565 // set in m.parameters.
1566 sat::SatParameters flag_parameters;
1567 CHECK(google::protobuf::TextFormat::ParseFromString(sat_params,
1568 &flag_parameters))
1569 << sat_params;
1570 m.parameters.MergeFrom(flag_parameters);
1571
1572 // We only need an observer if 'p.display_all_solutions' or
1573 // 'p.search_all_solutions' are true.
1574 std::function<void(const CpSolverResponse&)> solution_observer = nullptr;
1576 solution_observer = [&fz_model, &m, &p,
1577 solution_logger](const CpSolverResponse& r) {
1578 const std::string solution_string = SolutionString(
1579 fz_model,
1580 [&m, &r](fz::Variable* v) {
1581 return r.solution(m.fz_var_to_index.at(v));
1582 },
1583 r.objective_value());
1584 SOLVER_LOG(solution_logger, solution_string);
1585 if (p.display_statistics) {
1586 OutputFlatzincStats(r, solution_logger);
1587 }
1588 SOLVER_LOG(solution_logger, "----------");
1589 };
1590 }
1591
1592 Model sat_model;
1593
1594 // Setup logging.
1595 // Note that we need to do that before we start calling the sat functions
1596 // below that might create a SolverLogger() themselves.
1597 sat_model.Register<SolverLogger>(logger);
1598
1599 sat_model.Add(NewSatParameters(m.parameters));
1600 if (solution_observer != nullptr) {
1601 sat_model.Add(NewFeasibleSolutionObserver(solution_observer));
1602 }
1603
1604 const CpSolverResponse response = SolveCpModel(m.proto, &sat_model);
1605
1606 // Check the returned solution with the fz model checker.
1607 if (response.status() == CpSolverStatus::FEASIBLE ||
1608 response.status() == CpSolverStatus::OPTIMAL) {
1609 CHECK(CheckSolution(
1610 fz_model,
1611 [&response, &m](fz::Variable* v) {
1612 return response.solution(m.fz_var_to_index.at(v));
1613 },
1614 logger));
1615 }
1616
1617 // Output the solution in the flatzinc official format.
1618 if (p.ortools_mode) {
1619 if (response.status() == CpSolverStatus::FEASIBLE ||
1620 response.status() == CpSolverStatus::OPTIMAL) {
1622 // Already printed otherwise.
1623 const std::string solution_string = SolutionString(
1624 fz_model,
1625 [&response, &m](fz::Variable* v) {
1626 return response.solution(m.fz_var_to_index.at(v));
1627 },
1628 response.objective_value());
1629 SOLVER_LOG(solution_logger, solution_string);
1630 SOLVER_LOG(solution_logger, "----------");
1631 }
1632 if (response.status() == CpSolverStatus::OPTIMAL) {
1633 SOLVER_LOG(solution_logger, "==========");
1634 }
1635 } else if (response.status() == CpSolverStatus::INFEASIBLE) {
1636 SOLVER_LOG(solution_logger, "=====UNSATISFIABLE=====");
1637 } else if (response.status() == CpSolverStatus::MODEL_INVALID) {
1638 const std::string error_message = ValidateCpModel(m.proto);
1639 VLOG(1) << "%% Error message = '" << error_message << "'";
1640 if (absl::StrContains(error_message, "overflow")) {
1641 SOLVER_LOG(solution_logger, "=====OVERFLOW=====");
1642 } else {
1643 SOLVER_LOG(solution_logger, "=====MODEL INVALID=====");
1644 }
1645 } else {
1646 SOLVER_LOG(solution_logger, "%% TIMEOUT");
1647 }
1648 if (p.display_statistics) {
1649 OutputFlatzincStats(response, solution_logger);
1650 }
1651 }
1652}
1653
1654} // namespace sat
1655} // namespace operations_research
static Domain FromValues(std::vector< int64_t > values)
Domain AdditionWith(const Domain &domain) const
const std::vector< double > & float_objective_coefficients() const
Definition model.h:393
void AddFloatingPointObjectiveTerm(Variable *var, double coeff)
Definition model.h:399
const std::vector< Variable * > & float_objective_variables() const
Definition model.h:390
const std::vector< Constraint * > & constraints() const
Definition model.h:373
void SetFloatingPointObjectiveOffset(double offset)
Definition model.h:403
const std::vector< Variable * > & variables() const
--— Accessors and mutators --—
Definition model.h:372
double float_objective_offset() const
Definition model.h:396
const std::string & name() const
Definition model.h:410
const std::vector< Annotation > & search_annotations() const
Definition model.h:374
Variable * objective() const
Definition model.h:389
T Add(std::function< T(Model *)> f)
Definition model.h:87
void Register(T *non_owned_class)
Definition model.h:177
ABSL_FLAG(int64_t, fz_int_max, int64_t{1}<< 40, "Default max value for unbounded integer variables.")
ReverseView< Container > reversed_view(const Container &c)
std::function< SatParameters(Model *)> NewSatParameters(const std::string &params)
std::string ValidateCpModel(const CpModelProto &model, bool after_presolve)
void SolveFzWithCpModelProto(const fz::Model &fz_model, const fz::FlatzincSatParameters &p, const std::string &sat_params, SolverLogger *logger, SolverLogger *solution_logger)
Solves the given flatzinc model using the CP-SAT solver.
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
Serializes a Domain into the domain field of a proto.
CpSolverResponse SolveCpModel(const CpModelProto &model_proto, Model *model)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
std::function< void(Model *)> NewFeasibleSolutionObserver(const std::function< void(const CpSolverResponse &response)> &callback)
int NegatedRef(int ref)
Small utility functions to deal with negative variable/literal references.
void ProcessFloatingPointOVariablesAndObjective(fz::Model *fz_model)
In SWIG mode, we don't want anything besides these top-level includes.
int64_t Max() const
Returns the max of the domain.
Definition model.cc:346
int64_t Min() const
Returns the min of the domain.
Definition model.cc:340
std::vector< Argument > arguments
Definition model.h:240
std::vector< int64_t > values
These should never be modified from outside the class.
Definition model.h:107
bool is_float
Float domain.
Definition model.h:113
std::vector< double > float_values
Definition model.h:114
#define SOLVER_LOG(logger,...)
Definition logging.h:109