26#include "absl/container/flat_hash_map.h"
27#include "absl/container/flat_hash_set.h"
28#include "absl/flags/flag.h"
29#include "absl/log/check.h"
30#include "absl/log/log.h"
31#include "absl/strings/match.h"
32#include "absl/strings/str_cat.h"
33#include "absl/types/span.h"
34#include "google/protobuf/arena.h"
35#include "google/protobuf/text_format.h"
49 "Default max value for unbounded integer variables.");
51 "If true, enable interleaved workers when num_workers is 1.");
58static const int kNoVar = std::numeric_limits<int>::min();
66int TrueLiteral(
int var) {
return var; }
67int FalseLiteral(
int var) {
return -var - 1; }
70struct CpModelProtoWithMapping {
71 CpModelProtoWithMapping()
72 : arena(std::make_unique<google::protobuf::Arena>()),
73 proto(*google::protobuf::Arena::Create<CpModelProto>(arena.get())) {}
76 int LookupConstant(int64_t value);
80 int LookupVar(
const fz::Argument& argument);
81 LinearExpressionProto LookupExpr(
const fz::Argument& argument,
83 LinearExpressionProto LookupExprAt(
const fz::Argument& argument,
int pos,
85 std::vector<int> LookupVars(
const fz::Argument& argument);
86 VarOrValue LookupVarOrValue(
const fz::Argument& argument);
87 std::vector<VarOrValue> LookupVarsOrValues(
const fz::Argument& argument);
90 int GetOrCreateLiteralForVarEqValue(
int var, int64_t value);
93 int GetOrCreateLiteralForVarEqVar(
int var1,
int var2);
98 std::vector<int> CreateIntervals(absl::Span<const VarOrValue> starts,
99 absl::Span<const VarOrValue> sizes);
108 std::vector<int> CreateNonZeroOrOptionalIntervals(
109 absl::Span<const VarOrValue> starts, absl::Span<const VarOrValue> sizes);
116 int GetOrCreateOptionalInterval(VarOrValue start_var, VarOrValue size,
121 int NonZeroLiteralFrom(VarOrValue size);
125 ConstraintProto* AddEnforcedConstraint(
int literal);
128 void FillAMinusBInDomain(
const std::vector<int64_t>& domain,
129 const fz::Constraint& fz_ct, ConstraintProto* ct);
130 void FillLinearConstraintWithGivenDomain(absl::Span<const int64_t> domain,
131 const fz::Constraint& fz_ct,
132 ConstraintProto* ct);
133 void FillConstraint(
const fz::Constraint& fz_ct, ConstraintProto* ct);
134 void FillReifOrImpliedConstraint(
const fz::Constraint& fz_ct,
135 ConstraintProto* ct);
136 void BuildTableFromDomainIntLinEq(
const fz::Constraint& fz_ct,
137 ConstraintProto* ct);
141 void TranslateSearchAnnotations(
142 absl::Span<const fz::Annotation> search_annotations,
143 SolverLogger* logger);
146 std::unique_ptr<google::protobuf::Arena> arena;
148 SatParameters parameters;
151 absl::flat_hash_map<fz::Variable*, int> fz_var_to_index;
152 absl::flat_hash_map<int64_t, int> constant_value_to_index;
153 absl::flat_hash_map<std::tuple<int, int64_t, int, int64_t, int>,
int>
154 interval_key_to_index;
155 absl::flat_hash_map<int, int> var_to_lit_implies_greater_than_zero;
156 absl::flat_hash_map<std::pair<int, int64_t>,
int> var_eq_value_to_literal;
157 absl::flat_hash_map<std::pair<int, int>,
int> var_eq_var_to_literal;
160int CpModelProtoWithMapping::LookupConstant(int64_t value) {
161 if (constant_value_to_index.contains(value)) {
162 return constant_value_to_index[value];
169 var_proto->add_domain(value);
170 constant_value_to_index[value] = index;
174int CpModelProtoWithMapping::LookupVar(
const fz::Argument& argument) {
175 if (argument.HasOneValue())
return LookupConstant(argument.Value());
176 CHECK_EQ(argument.type, fz::Argument::VAR_REF);
177 return fz_var_to_index[argument.Var()];
180LinearExpressionProto CpModelProtoWithMapping::LookupExpr(
181 const fz::Argument& argument,
bool negate) {
182 LinearExpressionProto expr;
183 if (argument.HasOneValue()) {
184 const int64_t value = argument.Value();
185 expr.set_offset(negate ? -value : value);
187 expr.add_vars(LookupVar(argument));
188 expr.add_coeffs(negate ? -1 : 1);
193LinearExpressionProto CpModelProtoWithMapping::LookupExprAt(
194 const fz::Argument& argument,
int pos,
bool negate) {
195 LinearExpressionProto expr;
196 if (argument.HasOneValueAt(pos)) {
197 const int64_t value = argument.ValueAt(pos);
198 expr.set_offset(negate ? -value : value);
200 expr.add_vars(fz_var_to_index[argument.VarAt(pos)]);
201 expr.add_coeffs(negate ? -1 : 1);
206std::vector<int> CpModelProtoWithMapping::LookupVars(
207 const fz::Argument& argument) {
208 std::vector<int> result;
209 if (argument.type == fz::Argument::VOID_ARGUMENT)
return result;
210 if (argument.type == fz::Argument::INT_LIST) {
211 for (int64_t value : argument.values) {
212 result.push_back(LookupConstant(value));
214 }
else if (argument.type == fz::Argument::INT_VALUE) {
215 result.push_back(LookupConstant(argument.Value()));
217 CHECK_EQ(argument.type, fz::Argument::VAR_REF_ARRAY);
218 for (fz::Variable* var : argument.variables) {
219 CHECK(var !=
nullptr);
220 result.push_back(fz_var_to_index[var]);
226VarOrValue CpModelProtoWithMapping::LookupVarOrValue(
227 const fz::Argument& argument) {
228 if (argument.type == fz::Argument::INT_VALUE) {
229 return {kNoVar, argument.Value()};
231 CHECK_EQ(argument.type, fz::Argument::VAR_REF);
232 fz::Variable* var = argument.Var();
233 CHECK(var !=
nullptr);
234 if (var->domain.HasOneValue()) {
235 return {kNoVar, var->domain.Value()};
237 return {fz_var_to_index[var], 0};
242std::vector<VarOrValue> CpModelProtoWithMapping::LookupVarsOrValues(
243 const fz::Argument& argument) {
244 std::vector<VarOrValue> result;
245 const int no_var = kNoVar;
246 if (argument.type == fz::Argument::VOID_ARGUMENT)
return result;
247 if (argument.type == fz::Argument::INT_LIST) {
248 for (int64_t value : argument.values) {
249 result.push_back({no_var, value});
251 }
else if (argument.type == fz::Argument::INT_VALUE) {
252 result.push_back({no_var, argument.Value()});
254 CHECK_EQ(argument.type, fz::Argument::VAR_REF_ARRAY);
255 for (fz::Variable* var : argument.variables) {
256 CHECK(var !=
nullptr);
257 if (var->domain.HasOneValue()) {
258 result.push_back({no_var, var->domain.Value()});
260 result.push_back({fz_var_to_index[var], 0});
267ConstraintProto* CpModelProtoWithMapping::AddEnforcedConstraint(
int literal) {
269 if (literal != kNoVar) {
270 result->add_enforcement_literal(literal);
275int CpModelProtoWithMapping::GetOrCreateLiteralForVarEqValue(
int var,
277 const std::pair<int, int64_t> key = {var, value};
278 const auto it = var_eq_value_to_literal.find(key);
279 if (it != var_eq_value_to_literal.end())
return it->second;
283 var_proto->add_domain(1);
285 ConstraintProto* is_eq = AddEnforcedConstraint(TrueLiteral(bool_var));
286 is_eq->mutable_linear()->add_vars(var);
287 is_eq->mutable_linear()->add_coeffs(1);
288 is_eq->mutable_linear()->add_domain(value);
289 is_eq->mutable_linear()->add_domain(value);
291 ConstraintProto* is_not_eq = AddEnforcedConstraint(FalseLiteral(bool_var));
292 is_not_eq->mutable_linear()->add_vars(var);
293 is_not_eq->mutable_linear()->add_coeffs(1);
294 is_not_eq->mutable_linear()->add_domain(std::numeric_limits<int64_t>::min());
295 is_not_eq->mutable_linear()->add_domain(value - 1);
296 is_not_eq->mutable_linear()->add_domain(value + 1);
297 is_not_eq->mutable_linear()->add_domain(std::numeric_limits<int64_t>::max());
299 var_eq_value_to_literal[key] = bool_var;
303int CpModelProtoWithMapping::GetOrCreateLiteralForVarEqVar(
int var1,
int var2) {
304 CHECK_NE(var1, kNoVar);
305 CHECK_NE(var2, kNoVar);
306 if (var1 > var2) std::swap(var1, var2);
307 if (var1 == var2)
return LookupConstant(1);
309 const std::pair<int, int> key = {var1, var2};
310 const auto it = var_eq_var_to_literal.find(key);
311 if (it != var_eq_var_to_literal.end())
return it->second;
316 var_proto->add_domain(1);
318 ConstraintProto* is_eq = AddEnforcedConstraint(TrueLiteral(bool_var));
319 is_eq->mutable_linear()->add_vars(var1);
320 is_eq->mutable_linear()->add_coeffs(1);
321 is_eq->mutable_linear()->add_vars(var2);
322 is_eq->mutable_linear()->add_coeffs(-1);
323 is_eq->mutable_linear()->add_domain(0);
324 is_eq->mutable_linear()->add_domain(0);
326 ConstraintProto* is_not_eq = AddEnforcedConstraint(FalseLiteral(bool_var));
327 is_not_eq->mutable_linear()->add_vars(var1);
328 is_not_eq->mutable_linear()->add_coeffs(1);
329 is_not_eq->mutable_linear()->add_vars(var2);
330 is_not_eq->mutable_linear()->add_coeffs(-1);
331 is_not_eq->mutable_linear()->add_domain(std::numeric_limits<int64_t>::min());
332 is_not_eq->mutable_linear()->add_domain(-1);
333 is_not_eq->mutable_linear()->add_domain(1);
334 is_not_eq->mutable_linear()->add_domain(std::numeric_limits<int64_t>::max());
336 var_eq_var_to_literal[key] = bool_var;
340int CpModelProtoWithMapping::GetOrCreateOptionalInterval(VarOrValue start,
344 const std::tuple<int, int64_t, int, int64_t, int> key =
345 std::make_tuple(start.var, start.value, size.var, size.value, opt_var);
346 const auto [it, inserted] =
347 interval_key_to_index.insert({key, interval_index});
352 if (size.var == kNoVar || start.var == kNoVar) {
353 auto* interval = AddEnforcedConstraint(opt_var)->mutable_interval();
354 if (start.var != kNoVar) {
355 interval->mutable_start()->add_vars(start.var);
356 interval->mutable_start()->add_coeffs(1);
357 interval->mutable_end()->add_vars(start.var);
358 interval->mutable_end()->add_coeffs(1);
360 interval->mutable_start()->set_offset(start.value);
361 interval->mutable_end()->set_offset(start.value);
364 if (size.var != kNoVar) {
365 interval->mutable_size()->add_vars(size.var);
366 interval->mutable_size()->add_coeffs(1);
367 interval->mutable_end()->add_vars(size.var);
368 interval->mutable_end()->add_coeffs(1);
370 interval->mutable_size()->set_offset(size.value);
371 interval->mutable_end()->set_offset(size.value +
372 interval->end().offset());
374 return interval_index;
383 auto* interval = AddEnforcedConstraint(opt_var)->mutable_interval();
384 interval->mutable_start()->add_vars(start.var);
385 interval->mutable_start()->add_coeffs(1);
386 interval->mutable_size()->add_vars(size.var);
387 interval->mutable_size()->add_coeffs(1);
388 interval->mutable_end()->add_vars(end_var);
389 interval->mutable_end()->add_coeffs(1);
393 auto* lin = AddEnforcedConstraint(opt_var)->mutable_linear();
394 lin->add_vars(start.var);
396 lin->add_vars(size.var);
398 lin->add_vars(end_var);
403 return interval_index;
407std::vector<int> CpModelProtoWithMapping::CreateIntervals(
408 absl::Span<const VarOrValue> starts, absl::Span<const VarOrValue> sizes) {
409 std::vector<int> intervals;
410 for (
int i = 0;
i < starts.size(); ++
i) {
412 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
417std::vector<int> CpModelProtoWithMapping::CreateNonZeroOrOptionalIntervals(
418 absl::Span<const VarOrValue> starts, absl::Span<const VarOrValue> sizes) {
419 std::vector<int> intervals;
420 for (
int i = 0;
i < starts.size(); ++
i) {
421 const int opt_var = NonZeroLiteralFrom(sizes[i]);
423 GetOrCreateOptionalInterval(starts[i], sizes[i], opt_var));
428int CpModelProtoWithMapping::NonZeroLiteralFrom(VarOrValue size) {
429 if (size.var == kNoVar) {
430 return LookupConstant(size.value > 0);
432 const auto it = var_to_lit_implies_greater_than_zero.find(size.var);
433 if (it != var_to_lit_implies_greater_than_zero.end()) {
437 const IntegerVariableProto& var_proto = proto.
variables(size.var);
439 DCHECK_GE(domain.
Min(), 0);
440 if (domain.
Min() > 0)
return LookupConstant(1);
441 if (domain.
Max() == 0) {
442 return LookupConstant(0);
448 lit_proto->add_domain(1);
450 ConstraintProto* is_greater =
451 AddEnforcedConstraint(TrueLiteral(var_greater_than_zero_lit));
452 is_greater->mutable_linear()->add_vars(size.var);
453 is_greater->mutable_linear()->add_coeffs(1);
454 const Domain positive = domain.IntersectionWith({1, domain.
Max()});
457 ConstraintProto* is_null =
458 AddEnforcedConstraint(FalseLiteral(var_greater_than_zero_lit));
459 is_null->mutable_linear()->add_vars(size.var);
460 is_null->mutable_linear()->add_coeffs(1);
461 is_null->mutable_linear()->add_domain(0);
462 is_null->mutable_linear()->add_domain(0);
464 var_to_lit_implies_greater_than_zero[size.var] = var_greater_than_zero_lit;
465 return var_greater_than_zero_lit;
468void CpModelProtoWithMapping::FillAMinusBInDomain(
469 const std::vector<int64_t>& domain,
const fz::Constraint& fz_ct,
470 ConstraintProto* ct) {
471 auto* arg = ct->mutable_linear();
472 if (fz_ct.arguments[1].type == fz::Argument::INT_VALUE) {
473 const int64_t value = fz_ct.arguments[1].Value();
474 const int var_a = LookupVar(fz_ct.arguments[0]);
475 for (
const int64_t domain_bound : domain) {
476 if (domain_bound == std::numeric_limits<int64_t>::min() ||
477 domain_bound == std::numeric_limits<int64_t>::max()) {
478 arg->add_domain(domain_bound);
480 arg->add_domain(domain_bound + value);
483 arg->add_vars(var_a);
485 }
else if (fz_ct.arguments[0].type == fz::Argument::INT_VALUE) {
486 const int64_t value = fz_ct.arguments[0].Value();
487 const int var_b = LookupVar(fz_ct.arguments[1]);
489 if (domain_bound == std::numeric_limits<int64_t>::min()) {
490 arg->add_domain(std::numeric_limits<int64_t>::max());
491 }
else if (domain_bound == std::numeric_limits<int64_t>::max()) {
492 arg->add_domain(std::numeric_limits<int64_t>::min());
494 arg->add_domain(value - domain_bound);
497 arg->add_vars(var_b);
500 for (
const int64_t domain_bound : domain) arg->add_domain(domain_bound);
501 arg->add_vars(LookupVar(fz_ct.arguments[0]));
503 arg->add_vars(LookupVar(fz_ct.arguments[1]));
508void CpModelProtoWithMapping::FillLinearConstraintWithGivenDomain(
509 absl::Span<const int64_t> domain,
const fz::Constraint& fz_ct,
510 ConstraintProto* ct) {
511 auto* arg = ct->mutable_linear();
512 for (
const int64_t domain_bound : domain) arg->add_domain(domain_bound);
513 std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
514 for (
int i = 0;
i < vars.size(); ++
i) {
515 arg->add_vars(vars[i]);
516 arg->add_coeffs(fz_ct.arguments[0].values[i]);
520void CpModelProtoWithMapping::BuildTableFromDomainIntLinEq(
521 const fz::Constraint& fz_ct, ConstraintProto* ct) {
522 const std::vector<int64_t>& coeffs = fz_ct.arguments[0].values;
523 const std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
524 const int rhs = fz_ct.arguments[2].Value();
525 CHECK_EQ(coeffs.back(), -1);
526 for (
const int var : vars) {
527 LinearExpressionProto* expr = ct->mutable_table()->add_exprs();
532 switch (vars.size()) {
536 for (
const int64_t v0 : domain0.Values()) {
537 for (
const int64_t v1 : domain1.Values()) {
538 const int64_t v2 = coeffs[0] * v0 + coeffs[1] * v1 - rhs;
539 ct->mutable_table()->add_values(v0);
540 ct->mutable_table()->add_values(v1);
541 ct->mutable_table()->add_values(v2);
550 for (
const int64_t v0 : domain0.Values()) {
551 for (
const int64_t v1 : domain1.Values()) {
552 for (
const int64_t v2 : domain2.Values()) {
554 coeffs[0] * v0 + coeffs[1] * v1 + coeffs[2] * v2 - rhs;
555 ct->mutable_table()->add_values(v0);
556 ct->mutable_table()->add_values(v1);
557 ct->mutable_table()->add_values(v2);
558 ct->mutable_table()->add_values(v3);
565 LOG(FATAL) <<
"Unsupported size";
569void CpModelProtoWithMapping::FillConstraint(
const fz::Constraint& fz_ct,
570 ConstraintProto* ct) {
571 if (fz_ct.type ==
"false_constraint") {
573 ct->mutable_bool_or();
574 }
else if (fz_ct.type ==
"bool_clause") {
575 auto* arg = ct->mutable_bool_or();
576 for (
const int var : LookupVars(fz_ct.arguments[0])) {
577 arg->add_literals(TrueLiteral(var));
579 for (
const int var : LookupVars(fz_ct.arguments[1])) {
580 arg->add_literals(FalseLiteral(var));
582 }
else if (fz_ct.type ==
"bool_xor") {
585 const int a = LookupVar(fz_ct.arguments[0]);
586 const int b = LookupVar(fz_ct.arguments[1]);
587 const int x = LookupVar(fz_ct.arguments[2]);
591 auto*
const refute = ct->mutable_linear();
593 refute->add_coeffs(1);
595 refute->add_coeffs(-1);
596 refute->add_domain(0);
597 refute->add_domain(0);
600 auto* enforce = AddEnforcedConstraint(x)->mutable_linear();
601 enforce->add_vars(a);
602 enforce->add_coeffs(1);
603 enforce->add_vars(b);
604 enforce->add_coeffs(1);
605 enforce->add_domain(1);
606 enforce->add_domain(1);
607 }
else if (fz_ct.type ==
"array_bool_or") {
608 auto* arg = ct->mutable_bool_or();
609 for (
const int var : LookupVars(fz_ct.arguments[0])) {
610 arg->add_literals(TrueLiteral(var));
612 }
else if (fz_ct.type ==
"array_bool_or_negated") {
613 auto* arg = ct->mutable_bool_and();
614 for (
const int var : LookupVars(fz_ct.arguments[0])) {
615 arg->add_literals(FalseLiteral(var));
617 }
else if (fz_ct.type ==
"array_bool_and") {
618 auto* arg = ct->mutable_bool_and();
619 for (
const int var : LookupVars(fz_ct.arguments[0])) {
620 arg->add_literals(TrueLiteral(var));
622 }
else if (fz_ct.type ==
"array_bool_and_negated") {
623 auto* arg = ct->mutable_bool_or();
624 for (
const int var : LookupVars(fz_ct.arguments[0])) {
625 arg->add_literals(FalseLiteral(var));
627 }
else if (fz_ct.type ==
"array_bool_xor") {
628 auto* arg = ct->mutable_bool_xor();
629 for (
const int var : LookupVars(fz_ct.arguments[0])) {
630 arg->add_literals(TrueLiteral(var));
632 }
else if (fz_ct.type ==
"bool_le" || fz_ct.type ==
"int_le") {
633 FillAMinusBInDomain({std::numeric_limits<int64_t>::min(), 0}, fz_ct, ct);
634 }
else if (fz_ct.type ==
"bool_ge" || fz_ct.type ==
"int_ge") {
635 FillAMinusBInDomain({0, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
636 }
else if (fz_ct.type ==
"bool_lt" || fz_ct.type ==
"int_lt") {
637 FillAMinusBInDomain({std::numeric_limits<int64_t>::min(), -1}, fz_ct, ct);
638 }
else if (fz_ct.type ==
"bool_gt" || fz_ct.type ==
"int_gt") {
639 FillAMinusBInDomain({1, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
640 }
else if (fz_ct.type ==
"bool_eq" || fz_ct.type ==
"int_eq" ||
641 fz_ct.type ==
"bool2int") {
642 FillAMinusBInDomain({0, 0}, fz_ct, ct);
643 }
else if (fz_ct.type ==
"bool_ne" || fz_ct.type ==
"bool_not") {
644 auto* arg = ct->mutable_linear();
645 arg->add_vars(LookupVar(fz_ct.arguments[0]));
647 arg->add_vars(LookupVar(fz_ct.arguments[1]));
651 }
else if (fz_ct.type ==
"int_ne") {
652 FillAMinusBInDomain({std::numeric_limits<int64_t>::min(), -1, 1,
653 std::numeric_limits<int64_t>::max()},
655 }
else if (fz_ct.type ==
"int_lin_eq") {
657 if (fz_ct.strong_propagation && fz_ct.arguments[0].Size() >= 3 &&
658 fz_ct.arguments[0].Size() <= 4 &&
659 fz_ct.arguments[0].values.back() == -1) {
660 BuildTableFromDomainIntLinEq(fz_ct, ct);
662 const int64_t rhs = fz_ct.arguments[2].values[0];
663 FillLinearConstraintWithGivenDomain({rhs, rhs}, fz_ct, ct);
665 }
else if (fz_ct.type ==
"bool_lin_eq") {
666 auto* arg = ct->mutable_linear();
667 const std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
668 for (
int i = 0;
i < vars.size(); ++
i) {
669 arg->add_vars(vars[i]);
670 arg->add_coeffs(fz_ct.arguments[0].values[i]);
672 if (fz_ct.arguments[2].IsVariable()) {
673 arg->add_vars(LookupVar(fz_ct.arguments[2]));
678 const int64_t v = fz_ct.arguments[2].Value();
682 }
else if (fz_ct.type ==
"int_lin_le" || fz_ct.type ==
"bool_lin_le") {
683 const int64_t rhs = fz_ct.arguments[2].values[0];
684 FillLinearConstraintWithGivenDomain(
685 {std::numeric_limits<int64_t>::min(), rhs}, fz_ct, ct);
686 }
else if (fz_ct.type ==
"int_lin_lt") {
687 const int64_t rhs = fz_ct.arguments[2].values[0];
688 FillLinearConstraintWithGivenDomain(
689 {std::numeric_limits<int64_t>::min(), rhs - 1}, fz_ct, ct);
690 }
else if (fz_ct.type ==
"int_lin_ge") {
691 const int64_t rhs = fz_ct.arguments[2].values[0];
692 FillLinearConstraintWithGivenDomain(
693 {rhs, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
694 }
else if (fz_ct.type ==
"int_lin_gt") {
695 const int64_t rhs = fz_ct.arguments[2].values[0];
696 FillLinearConstraintWithGivenDomain(
697 {rhs + 1, std::numeric_limits<int64_t>::max()}, fz_ct, ct);
698 }
else if (fz_ct.type ==
"int_lin_ne") {
699 const int64_t rhs = fz_ct.arguments[2].values[0];
700 FillLinearConstraintWithGivenDomain(
701 {std::numeric_limits<int64_t>::min(), rhs - 1, rhs + 1,
702 std::numeric_limits<int64_t>::max()},
704 }
else if (fz_ct.type ==
"set_in") {
705 auto* arg = ct->mutable_linear();
706 arg->add_vars(LookupVar(fz_ct.arguments[0]));
708 if (fz_ct.arguments[1].type == fz::Argument::INT_LIST) {
710 fz_ct.arguments[1].values.begin(),
711 fz_ct.arguments[1].values.end()}),
713 }
else if (fz_ct.arguments[1].type == fz::Argument::INT_INTERVAL) {
715 Domain(fz_ct.arguments[1].values[0], fz_ct.arguments[1].values[1]),
718 LOG(FATAL) <<
"Wrong format";
720 }
else if (fz_ct.type ==
"set_in_negated") {
721 auto* arg = ct->mutable_linear();
722 arg->add_vars(LookupVar(fz_ct.arguments[0]));
724 if (fz_ct.arguments[1].type == fz::Argument::INT_LIST) {
727 std::vector<int64_t>{fz_ct.arguments[1].values.begin(),
728 fz_ct.arguments[1].values.end()})
731 }
else if (fz_ct.arguments[1].type == fz::Argument::INT_INTERVAL) {
733 Domain(fz_ct.arguments[1].values[0], fz_ct.arguments[1].values[1])
737 LOG(FATAL) <<
"Wrong format";
739 }
else if (fz_ct.type ==
"int_min") {
740 auto* arg = ct->mutable_lin_max();
741 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0],
true);
742 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1],
true);
743 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2],
true);
744 }
else if (fz_ct.type ==
"array_int_minimum" || fz_ct.type ==
"minimum_int") {
745 auto* arg = ct->mutable_lin_max();
746 *arg->mutable_target() = LookupExpr(fz_ct.arguments[0],
true);
747 for (
int i = 0;
i < fz_ct.arguments[1].Size(); ++
i) {
748 *arg->add_exprs() = LookupExprAt(fz_ct.arguments[1], i,
true);
750 }
else if (fz_ct.type ==
"int_max") {
751 auto* arg = ct->mutable_lin_max();
752 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
753 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
754 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
755 }
else if (fz_ct.type ==
"array_int_maximum" || fz_ct.type ==
"maximum_int") {
756 auto* arg = ct->mutable_lin_max();
757 *arg->mutable_target() = LookupExpr(fz_ct.arguments[0]);
758 for (
int i = 0;
i < fz_ct.arguments[1].Size(); ++
i) {
759 *arg->add_exprs() = LookupExprAt(fz_ct.arguments[1], i);
761 }
else if (fz_ct.type ==
"int_times") {
762 auto* arg = ct->mutable_int_prod();
763 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
764 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
765 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
766 }
else if (fz_ct.type ==
"int_abs") {
767 auto* arg = ct->mutable_lin_max();
768 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
769 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0],
true);
770 *arg->mutable_target() = LookupExpr(fz_ct.arguments[1]);
771 }
else if (fz_ct.type ==
"int_plus") {
772 auto* arg = ct->mutable_linear();
774 arg->add_vars(LookupVar(fz_ct.arguments[0]));
776 arg->add_vars(LookupVar(fz_ct.arguments[1]));
778 arg->add_vars(LookupVar(fz_ct.arguments[2]));
780 }
else if (fz_ct.type ==
"int_div") {
781 auto* arg = ct->mutable_int_div();
782 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
783 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
784 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
785 }
else if (fz_ct.type ==
"int_mod") {
786 auto* arg = ct->mutable_int_mod();
787 *arg->add_exprs() = LookupExpr(fz_ct.arguments[0]);
788 *arg->add_exprs() = LookupExpr(fz_ct.arguments[1]);
789 *arg->mutable_target() = LookupExpr(fz_ct.arguments[2]);
790 }
else if (fz_ct.type ==
"array_int_element" ||
791 fz_ct.type ==
"array_bool_element" ||
792 fz_ct.type ==
"array_var_int_element" ||
793 fz_ct.type ==
"array_var_bool_element" ||
794 fz_ct.type ==
"array_int_element_nonshifted") {
795 auto* arg = ct->mutable_element();
796 *arg->mutable_linear_index() = LookupExpr(fz_ct.arguments[0]);
797 if (!absl::EndsWith(fz_ct.type,
"_nonshifted")) {
798 arg->mutable_linear_index()->set_offset(arg->linear_index().offset() - 1);
800 *arg->mutable_linear_target() = LookupExpr(fz_ct.arguments[2]);
802 for (
const VarOrValue elem : LookupVarsOrValues(fz_ct.arguments[1])) {
803 auto* elem_proto = ct->mutable_element()->add_exprs();
804 if (elem.var != kNoVar) {
805 elem_proto->add_vars(elem.var);
806 elem_proto->add_coeffs(1);
808 elem_proto->set_offset(elem.value);
811 }
else if (fz_ct.type ==
"ortools_array_int_element" ||
812 fz_ct.type ==
"ortools_array_bool_element" ||
813 fz_ct.type ==
"ortools_array_var_int_element" ||
814 fz_ct.type ==
"ortools_array_var_bool_element") {
815 auto* arg = ct->mutable_element();
818 *arg->mutable_linear_index() = LookupExpr(fz_ct.arguments[0]);
819 const int64_t index_min = fz_ct.arguments[1].values[0];
820 arg->mutable_linear_index()->set_offset(arg->linear_index().offset() -
824 *arg->mutable_linear_target() = LookupExpr(fz_ct.arguments[3]);
827 for (
const VarOrValue elem : LookupVarsOrValues(fz_ct.arguments[2])) {
828 auto* elem_proto = ct->mutable_element()->add_exprs();
829 if (elem.var != kNoVar) {
830 elem_proto->add_vars(elem.var);
831 elem_proto->add_coeffs(1);
833 elem_proto->set_offset(elem.value);
836 }
else if (fz_ct.type ==
"ortools_table_int") {
837 auto* arg = ct->mutable_table();
838 for (
const VarOrValue v : LookupVarsOrValues(fz_ct.arguments[0])) {
839 LinearExpressionProto* expr = arg->add_exprs();
840 if (v.var != kNoVar) {
841 expr->add_vars(v.var);
844 expr->set_offset(v.value);
847 for (
const int64_t value : fz_ct.arguments[1].values)
848 arg->add_values(value);
849 }
else if (fz_ct.type ==
"ortools_regular") {
850 auto* arg = ct->mutable_automaton();
851 for (
const VarOrValue v : LookupVarsOrValues(fz_ct.arguments[0])) {
852 LinearExpressionProto* expr = arg->add_exprs();
853 if (v.var != kNoVar) {
854 expr->add_vars(v.var);
857 expr->set_offset(v.value);
862 const int num_states = fz_ct.arguments[1].Value();
863 const int num_values = fz_ct.arguments[2].Value();
864 for (
int i = 1;
i <= num_states; ++
i) {
865 for (
int j = 1; j <= num_values; ++j) {
866 CHECK_LT(count, fz_ct.arguments[3].values.size());
867 const int next = fz_ct.arguments[3].values[count++];
868 if (next == 0)
continue;
869 arg->add_transition_tail(i);
870 arg->add_transition_label(j);
871 arg->add_transition_head(next);
875 arg->set_starting_state(fz_ct.arguments[4].Value());
876 switch (fz_ct.arguments[5].type) {
877 case fz::Argument::INT_VALUE: {
878 arg->add_final_states(fz_ct.arguments[5].values[0]);
881 case fz::Argument::INT_INTERVAL: {
882 for (
int v = fz_ct.arguments[5].values[0];
883 v <= fz_ct.arguments[5].values[1]; ++v) {
884 arg->add_final_states(v);
888 case fz::Argument::INT_LIST: {
889 for (
const int v : fz_ct.arguments[5].values) {
890 arg->add_final_states(v);
895 LOG(FATAL) <<
"Wrong constraint " << fz_ct.DebugString();
898 }
else if (fz_ct.type ==
"fzn_all_different_int") {
899 auto* arg = ct->mutable_all_diff();
900 for (
int i = 0;
i < fz_ct.arguments[0].Size(); ++
i) {
901 *arg->add_exprs() = LookupExprAt(fz_ct.arguments[0], i);
903 }
else if (fz_ct.type ==
"ortools_count_eq_cst") {
904 const std::vector<VarOrValue> counts =
905 LookupVarsOrValues(fz_ct.arguments[0]);
906 const int64_t value = fz_ct.arguments[1].Value();
907 const VarOrValue target = LookupVarOrValue(fz_ct.arguments[2]);
908 LinearConstraintProto* arg = ct->mutable_linear();
909 int64_t fixed_contributions = 0;
910 for (
const VarOrValue& count : counts) {
911 if (count.var == kNoVar) {
912 fixed_contributions += count.value == value ? 1 : 0;
914 const int boolvar = GetOrCreateLiteralForVarEqValue(count.var, value);
915 CHECK_GE(boolvar, 0);
916 arg->add_vars(boolvar);
920 if (target.var == kNoVar) {
921 arg->add_domain(target.value - fixed_contributions);
922 arg->add_domain(target.value - fixed_contributions);
924 arg->add_vars(target.var);
926 arg->add_domain(-fixed_contributions);
927 arg->add_domain(-fixed_contributions);
929 }
else if (fz_ct.type ==
"ortools_count_eq") {
930 const std::vector<VarOrValue> counts =
931 LookupVarsOrValues(fz_ct.arguments[0]);
932 const int var = LookupVar(fz_ct.arguments[1]);
933 const VarOrValue target = LookupVarOrValue(fz_ct.arguments[2]);
934 LinearConstraintProto* arg = ct->mutable_linear();
935 for (
const VarOrValue& count : counts) {
936 if (count.var == kNoVar) {
937 const int boolvar = GetOrCreateLiteralForVarEqValue(var, count.value);
938 CHECK_GE(boolvar, 0);
939 arg->add_vars(boolvar);
942 const int boolvar = GetOrCreateLiteralForVarEqVar(var, count.var);
943 CHECK_GE(boolvar, 0);
944 arg->add_vars(boolvar);
948 if (target.var == kNoVar) {
949 arg->add_domain(target.value);
950 arg->add_domain(target.value);
952 arg->add_vars(target.var);
957 }
else if (fz_ct.type ==
"ortools_circuit" ||
958 fz_ct.type ==
"ortools_subcircuit") {
959 const int64_t min_index = fz_ct.arguments[1].Value();
960 const int size = std::max(fz_ct.arguments[0].values.size(),
961 fz_ct.arguments[0].variables.size());
963 const int64_t max_index = min_index + size - 1;
965 auto* circuit_arg = ct->mutable_circuit();
969 int64_t index = min_index;
970 const bool is_circuit = (fz_ct.type ==
"ortools_circuit");
971 for (
const int var : LookupVars(fz_ct.arguments[0])) {
975 domain = domain.IntersectionWith(Domain(min_index, max_index));
978 domain = domain.IntersectionWith(Domain::FromIntervals(
979 {{std::numeric_limits<int64_t>::min(), index - 1},
980 {index + 1, std::numeric_limits<int64_t>::max()}}));
984 for (
const ClosedInterval interval : domain) {
985 for (int64_t value = interval.start; value <= interval.end; ++value) {
991 new_var->add_domain(1);
995 circuit_arg->add_tails(index);
996 circuit_arg->add_heads(value);
997 circuit_arg->add_literals(literal);
1001 auto* lin = AddEnforcedConstraint(literal)->mutable_linear();
1004 lin->add_domain(value);
1005 lin->add_domain(value);
1011 AddEnforcedConstraint(
NegatedRef(literal))->mutable_linear();
1014 lin->add_domain(std::numeric_limits<int64_t>::min());
1015 lin->add_domain(value - 1);
1016 lin->add_domain(value + 1);
1017 lin->add_domain(std::numeric_limits<int64_t>::max());
1024 }
else if (fz_ct.type ==
"ortools_inverse") {
1025 auto* arg = ct->mutable_inverse();
1027 const auto direct_variables = LookupVars(fz_ct.arguments[0]);
1028 const auto inverse_variables = LookupVars(fz_ct.arguments[1]);
1029 const int base_direct = fz_ct.arguments[2].Value();
1030 const int base_inverse = fz_ct.arguments[3].Value();
1032 CHECK_EQ(direct_variables.size(), inverse_variables.size());
1033 const int num_variables = direct_variables.size();
1034 const int end_direct = base_direct + num_variables;
1035 const int end_inverse = base_inverse + num_variables;
1057 const int arity = std::max(base_inverse, base_direct) + num_variables;
1058 for (
int i = 0;
i < arity; ++
i) {
1060 if (i < base_direct) {
1061 if (i < base_inverse) {
1062 arg->add_f_direct(LookupConstant(i));
1063 }
else if (i >= base_inverse) {
1064 arg->add_f_direct(LookupConstant(i + num_variables));
1066 }
else if (i >= base_direct && i < end_direct) {
1067 arg->add_f_direct(direct_variables[i - base_direct]);
1069 arg->add_f_direct(LookupConstant(i - num_variables));
1073 if (i < base_inverse) {
1074 if (i < base_direct) {
1075 arg->add_f_inverse(LookupConstant(i));
1076 }
else if (i >= base_direct) {
1077 arg->add_f_inverse(LookupConstant(i + num_variables));
1079 }
else if (i >= base_inverse && i < end_inverse) {
1080 arg->add_f_inverse(inverse_variables[i - base_inverse]);
1082 arg->add_f_inverse(LookupConstant(i - num_variables));
1085 }
else if (fz_ct.type ==
"fzn_disjunctive") {
1086 const std::vector<VarOrValue> starts =
1087 LookupVarsOrValues(fz_ct.arguments[0]);
1088 const std::vector<VarOrValue> sizes =
1089 LookupVarsOrValues(fz_ct.arguments[1]);
1091 auto* arg = ct->mutable_cumulative();
1092 arg->mutable_capacity()->set_offset(1);
1093 for (
int i = 0;
i < starts.size(); ++
i) {
1095 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
1096 arg->add_demands()->set_offset(1);
1098 }
else if (fz_ct.type ==
"fzn_disjunctive_strict") {
1099 const std::vector<VarOrValue> starts =
1100 LookupVarsOrValues(fz_ct.arguments[0]);
1101 const std::vector<VarOrValue> sizes =
1102 LookupVarsOrValues(fz_ct.arguments[1]);
1104 auto* arg = ct->mutable_no_overlap();
1105 for (
int i = 0;
i < starts.size(); ++
i) {
1107 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
1109 }
else if (fz_ct.type ==
"fzn_cumulative") {
1110 const std::vector<VarOrValue> starts =
1111 LookupVarsOrValues(fz_ct.arguments[0]);
1112 const std::vector<VarOrValue> sizes =
1113 LookupVarsOrValues(fz_ct.arguments[1]);
1114 const std::vector<VarOrValue> demands =
1115 LookupVarsOrValues(fz_ct.arguments[2]);
1117 auto* arg = ct->mutable_cumulative();
1118 if (fz_ct.arguments[3].HasOneValue()) {
1119 arg->mutable_capacity()->set_offset(fz_ct.arguments[3].Value());
1121 arg->mutable_capacity()->add_vars(LookupVar(fz_ct.arguments[3]));
1122 arg->mutable_capacity()->add_coeffs(1);
1124 for (
int i = 0;
i < starts.size(); ++
i) {
1127 if (demands[i].var != kNoVar &&
1131 fz_ct.arguments[3].HasOneValue() && fz_ct.arguments[3].Value() == 1) {
1133 GetOrCreateOptionalInterval(starts[i], sizes[i], demands[i].var));
1134 arg->add_demands()->set_offset(1);
1137 GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
1138 LinearExpressionProto* demand = arg->add_demands();
1139 if (demands[i].var == kNoVar) {
1140 demand->set_offset(demands[i].value);
1142 demand->add_vars(demands[i].var);
1143 demand->add_coeffs(1);
1147 }
else if (fz_ct.type ==
"ortools_cumulative_opt") {
1148 const std::vector<int> occurs = LookupVars(fz_ct.arguments[0]);
1149 const std::vector<VarOrValue> starts =
1150 LookupVarsOrValues(fz_ct.arguments[1]);
1151 const std::vector<VarOrValue> durations =
1152 LookupVarsOrValues(fz_ct.arguments[2]);
1153 const std::vector<VarOrValue> demands =
1154 LookupVarsOrValues(fz_ct.arguments[3]);
1156 auto* arg = ct->mutable_cumulative();
1157 if (fz_ct.arguments[3].HasOneValue()) {
1158 arg->mutable_capacity()->set_offset(fz_ct.arguments[4].Value());
1160 arg->mutable_capacity()->add_vars(LookupVar(fz_ct.arguments[4]));
1161 arg->mutable_capacity()->add_coeffs(1);
1163 for (
int i = 0;
i < starts.size(); ++
i) {
1165 GetOrCreateOptionalInterval(starts[i], durations[i], occurs[i]));
1166 LinearExpressionProto* demand = arg->add_demands();
1167 if (demands[i].var == kNoVar) {
1168 demand->set_offset(demands[i].value);
1170 demand->add_vars(demands[i].var);
1171 demand->add_coeffs(1);
1174 }
else if (fz_ct.type ==
"ortools_disjunctive_strict_opt") {
1175 const std::vector<int> occurs = LookupVars(fz_ct.arguments[0]);
1176 const std::vector<VarOrValue> starts =
1177 LookupVarsOrValues(fz_ct.arguments[1]);
1178 const std::vector<VarOrValue> durations =
1179 LookupVarsOrValues(fz_ct.arguments[2]);
1181 auto* arg = ct->mutable_no_overlap();
1182 for (
int i = 0;
i < starts.size(); ++
i) {
1184 GetOrCreateOptionalInterval(starts[i], durations[i], occurs[i]));
1186 }
else if (fz_ct.type ==
"fzn_diffn" || fz_ct.type ==
"fzn_diffn_nonstrict") {
1187 const bool is_strict = fz_ct.type ==
"fzn_diffn";
1188 const std::vector<VarOrValue>
x = LookupVarsOrValues(fz_ct.arguments[0]);
1189 const std::vector<VarOrValue> y = LookupVarsOrValues(fz_ct.arguments[1]);
1190 const std::vector<VarOrValue> dx = LookupVarsOrValues(fz_ct.arguments[2]);
1191 const std::vector<VarOrValue> dy = LookupVarsOrValues(fz_ct.arguments[3]);
1192 const std::vector<int> x_intervals =
1193 is_strict ? CreateIntervals(x, dx)
1194 : CreateNonZeroOrOptionalIntervals(
x, dx);
1195 const std::vector<int> y_intervals =
1196 is_strict ? CreateIntervals(y, dy)
1197 : CreateNonZeroOrOptionalIntervals(y, dy);
1198 auto* arg = ct->mutable_no_overlap_2d();
1199 for (
int i = 0;
i <
x.size(); ++
i) {
1200 arg->add_x_intervals(x_intervals[i]);
1201 arg->add_y_intervals(y_intervals[i]);
1203 }
else if (fz_ct.type ==
"ortools_network_flow" ||
1204 fz_ct.type ==
"ortools_network_flow_cost") {
1207 const bool has_cost = fz_ct.type ==
"ortools_network_flow_cost";
1208 const std::vector<int> flow = LookupVars(fz_ct.arguments[3]);
1211 const int num_nodes = fz_ct.arguments[1].values.size();
1212 const int base_node = fz_ct.arguments[2].Value();
1213 std::vector<std::vector<int>> flows_per_node(num_nodes);
1214 std::vector<std::vector<int>> coeffs_per_node(num_nodes);
1216 const int num_arcs = fz_ct.arguments[0].values.size() / 2;
1217 for (
int arc = 0; arc < num_arcs; arc++) {
1218 const int tail = fz_ct.arguments[0].values[2 * arc] - base_node;
1219 const int head = fz_ct.arguments[0].values[2 * arc + 1] - base_node;
1220 if (tail == head)
continue;
1222 flows_per_node[tail].push_back(flow[arc]);
1223 coeffs_per_node[tail].push_back(1);
1224 flows_per_node[head].push_back(flow[arc]);
1225 coeffs_per_node[head].push_back(-1);
1227 for (
int node = 0; node < num_nodes; node++) {
1229 arg->
add_domain(fz_ct.arguments[1].values[node]);
1230 arg->add_domain(fz_ct.arguments[1].values[node]);
1231 for (
int i = 0;
i < flows_per_node[node].size(); ++
i) {
1232 arg->add_vars(flows_per_node[node][i]);
1233 arg->add_coeffs(coeffs_per_node[node][i]);
1241 for (
int arc = 0; arc < num_arcs; arc++) {
1242 const int64_t weight = fz_ct.arguments[4].values[arc];
1244 arg->add_vars(flow[arc]);
1245 arg->add_coeffs(weight);
1248 arg->add_vars(LookupVar(fz_ct.arguments[5]));
1249 arg->add_coeffs(-1);
1252 LOG(FATAL) <<
" Not supported " << fz_ct.type;
1256void CpModelProtoWithMapping::FillReifOrImpliedConstraint(
1257 const fz::Constraint& fz_ct, ConstraintProto* ct) {
1259 std::string simplified_type;
1260 if (absl::EndsWith(fz_ct.type,
"_reif")) {
1262 simplified_type = fz_ct.type.substr(0, fz_ct.type.size() - 5);
1263 }
else if (absl::EndsWith(fz_ct.type,
"_imp")) {
1265 simplified_type = fz_ct.type.substr(0, fz_ct.type.size() - 4);
1268 simplified_type = fz_ct.type;
1272 fz::Constraint copy = fz_ct;
1273 copy.type = simplified_type;
1276 FillConstraint(copy, ct);
1279 std::string negated_type;
1282 if (simplified_type ==
"array_bool_or") {
1283 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[1])));
1284 negated_type =
"array_bool_or_negated";
1285 }
else if (simplified_type ==
"array_bool_and") {
1286 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[1])));
1287 negated_type =
"array_bool_and_negated";
1288 }
else if (simplified_type ==
"set_in") {
1289 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1290 negated_type =
"set_in_negated";
1291 }
else if (simplified_type ==
"bool_eq" || simplified_type ==
"int_eq") {
1292 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1293 negated_type =
"int_ne";
1294 }
else if (simplified_type ==
"bool_ne" || simplified_type ==
"int_ne") {
1295 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1296 negated_type =
"int_eq";
1297 }
else if (simplified_type ==
"bool_le" || simplified_type ==
"int_le") {
1298 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1299 negated_type =
"int_gt";
1300 }
else if (simplified_type ==
"bool_lt" || simplified_type ==
"int_lt") {
1301 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1302 negated_type =
"int_ge";
1303 }
else if (simplified_type ==
"bool_ge" || simplified_type ==
"int_ge") {
1304 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1305 negated_type =
"int_lt";
1306 }
else if (simplified_type ==
"bool_gt" || simplified_type ==
"int_gt") {
1307 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
1308 negated_type =
"int_le";
1309 }
else if (simplified_type ==
"int_lin_eq") {
1310 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1311 negated_type =
"int_lin_ne";
1312 }
else if (simplified_type ==
"int_lin_ne") {
1313 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1314 negated_type =
"int_lin_eq";
1315 }
else if (simplified_type ==
"int_lin_le") {
1316 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1317 negated_type =
"int_lin_gt";
1318 }
else if (simplified_type ==
"int_lin_ge") {
1319 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1320 negated_type =
"int_lin_lt";
1321 }
else if (simplified_type ==
"int_lin_lt") {
1322 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1323 negated_type =
"int_lin_ge";
1324 }
else if (simplified_type ==
"int_lin_gt") {
1325 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
1326 negated_type =
"int_lin_le";
1328 LOG(FATAL) <<
"Unsupported " << simplified_type;
1332 if (absl::EndsWith(fz_ct.type,
"_imp"))
return;
1337 negated_ct->
set_name(fz_ct.type +
" (negated)");
1338 negated_ct->add_enforcement_literal(
1339 sat::NegatedRef(ct->enforcement_literal(0)));
1340 copy.type = negated_type;
1341 FillConstraint(copy, negated_ct);
1344void CpModelProtoWithMapping::TranslateSearchAnnotations(
1345 absl::Span<const fz::Annotation> search_annotations, SolverLogger* logger) {
1346 std::vector<fz::Annotation> flat_annotations;
1347 for (
const fz::Annotation& annotation : search_annotations) {
1348 fz::FlattenAnnotations(annotation, &flat_annotations);
1352 absl::flat_hash_set<int> hinted_vars;
1354 for (
const fz::Annotation& annotation : flat_annotations) {
1355 if (annotation.IsFunctionCallWithIdentifier(
"warm_start")) {
1356 CHECK_EQ(2, annotation.annotations.size());
1357 const fz::Annotation& vars = annotation.annotations[0];
1358 const fz::Annotation& values = annotation.annotations[1];
1359 if (vars.type != fz::Annotation::VAR_REF_ARRAY ||
1360 values.type != fz::Annotation::INT_LIST) {
1363 for (
int i = 0;
i < vars.variables.size(); ++
i) {
1364 fz::Variable* fz_var = vars.variables[
i];
1365 const int var = fz_var_to_index.at(fz_var);
1366 const int64_t value = values.values[
i];
1367 if (hinted_vars.insert(var).second) {
1372 }
else if (annotation.IsFunctionCallWithIdentifier(
"int_search") ||
1373 annotation.IsFunctionCallWithIdentifier(
"bool_search")) {
1374 const std::vector<fz::Annotation>& args = annotation.annotations;
1375 std::vector<fz::Variable*> vars;
1376 args[0].AppendAllVariables(&vars);
1379 for (fz::Variable* v : vars) {
1380 strategy->add_variables(fz_var_to_index.at(v));
1383 const fz::Annotation& choose = args[1];
1384 if (choose.id ==
"input_order") {
1385 strategy->set_variable_selection_strategy(
1386 DecisionStrategyProto::CHOOSE_FIRST);
1387 }
else if (choose.id ==
"first_fail") {
1388 strategy->set_variable_selection_strategy(
1389 DecisionStrategyProto::CHOOSE_MIN_DOMAIN_SIZE);
1390 }
else if (choose.id ==
"anti_first_fail") {
1391 strategy->set_variable_selection_strategy(
1392 DecisionStrategyProto::CHOOSE_MAX_DOMAIN_SIZE);
1393 }
else if (choose.id ==
"smallest") {
1394 strategy->set_variable_selection_strategy(
1395 DecisionStrategyProto::CHOOSE_LOWEST_MIN);
1396 }
else if (choose.id ==
"largest") {
1397 strategy->set_variable_selection_strategy(
1398 DecisionStrategyProto::CHOOSE_HIGHEST_MAX);
1400 SOLVER_LOG(logger,
"Unsupported variable selection strategy '",
1401 choose.id,
"', falling back to 'smallest'");
1402 strategy->set_variable_selection_strategy(
1403 DecisionStrategyProto::CHOOSE_LOWEST_MIN);
1406 const fz::Annotation& select = args[2];
1407 if (select.id ==
"indomain_min" || select.id ==
"indomain") {
1408 strategy->set_domain_reduction_strategy(
1409 DecisionStrategyProto::SELECT_MIN_VALUE);
1410 }
else if (select.id ==
"indomain_max") {
1411 strategy->set_domain_reduction_strategy(
1412 DecisionStrategyProto::SELECT_MAX_VALUE);
1413 }
else if (select.id ==
"indomain_split") {
1414 strategy->set_domain_reduction_strategy(
1415 DecisionStrategyProto::SELECT_LOWER_HALF);
1416 }
else if (select.id ==
"indomain_reverse_split") {
1417 strategy->set_domain_reduction_strategy(
1418 DecisionStrategyProto::SELECT_UPPER_HALF);
1419 }
else if (select.id ==
"indomain_median") {
1420 strategy->set_domain_reduction_strategy(
1421 DecisionStrategyProto::SELECT_MEDIAN_VALUE);
1423 SOLVER_LOG(logger,
"Unsupported value selection strategy '", select.id,
1424 "', falling back to 'indomain_min'");
1425 strategy->set_domain_reduction_strategy(
1426 DecisionStrategyProto::SELECT_MIN_VALUE);
1433std::string SolutionString(
1434 const fz::SolutionOutputSpecs& output,
1435 const std::function<int64_t(fz::Variable*)>& value_func,
1436 double objective_value) {
1437 if (output.variable !=
nullptr && !output.variable->domain.is_float) {
1438 const int64_t value = value_func(output.variable);
1439 if (output.display_as_boolean) {
1440 return absl::StrCat(output.name,
" = ", value == 1 ?
"true" :
"false",
1443 return absl::StrCat(output.name,
" = ", value,
";");
1445 }
else if (output.variable !=
nullptr && output.variable->domain.is_float) {
1446 return absl::StrCat(output.name,
" = ", objective_value,
";");
1448 const int bound_size = output.bounds.size();
1449 std::string result =
1450 absl::StrCat(output.name,
" = array", bound_size,
"d(");
1451 for (
int i = 0;
i < bound_size; ++
i) {
1452 if (output.bounds[
i].max_value >= output.bounds[
i].min_value) {
1453 absl::StrAppend(&result, output.bounds[
i].min_value,
"..",
1454 output.bounds[
i].max_value,
", ");
1456 result.append(
"{},");
1460 for (
int i = 0;
i < output.flat_variables.size(); ++
i) {
1461 const int64_t value = value_func(output.flat_variables[
i]);
1462 if (output.display_as_boolean) {
1463 result.append(value ?
"true" :
"false");
1465 absl::StrAppend(&result, value);
1467 if (
i != output.flat_variables.size() - 1) {
1468 result.append(
", ");
1471 result.append(
"]);");
1477std::string SolutionString(
1478 const fz::Model& model,
1479 const std::function<int64_t(fz::Variable*)>& value_func,
1480 double objective_value) {
1481 std::string solution_string;
1482 for (
const auto& output_spec : model.output()) {
1483 solution_string.append(
1484 SolutionString(output_spec, value_func, objective_value));
1485 solution_string.append(
"\n");
1487 return solution_string;
1490void OutputFlatzincStats(
const CpSolverResponse& response,
1491 SolverLogger* solution_logger) {
1493 "%%%mzn-stat: objective=", response.objective_value());
1495 "%%%mzn-stat: objectiveBound=", response.best_objective_bound());
1497 "%%%mzn-stat: boolVariables=", response.num_booleans());
1499 "%%%mzn-stat: failures=", response.num_conflicts());
1501 solution_logger,
"%%%mzn-stat: propagations=",
1502 response.num_binary_propagations() + response.num_integer_propagations());
1503 SOLVER_LOG(solution_logger,
"%%%mzn-stat: solveTime=", response.wall_time());
1512 if (!ct->active)
continue;
1513 if (ct->type ==
"int2float") {
1514 ct->type =
"int_eq";
1515 fz::Domain& float_domain = ct->arguments[1].variables[0]->domain;
1517 for (
const double float_value : float_domain.
float_values) {
1518 float_domain.
values.push_back(
static_cast<int64_t
>(float_value));
1528 if (!var->active)
continue;
1529 if (var->domain.is_float) {
1530 CHECK(float_objective_var ==
nullptr);
1531 float_objective_var = var;
1536 if (float_objective_var !=
nullptr) {
1538 if (!ct->active)
continue;
1539 if (ct->type ==
"float_lin_eq") {
1540 CHECK(float_objective_ct ==
nullptr);
1541 float_objective_ct = ct;
1547 if (float_objective_ct !=
nullptr || float_objective_var !=
nullptr) {
1548 CHECK(float_objective_ct !=
nullptr);
1549 CHECK(float_objective_var !=
nullptr);
1550 const int arity = float_objective_ct->
arguments[0].Size();
1551 CHECK_EQ(float_objective_ct->
arguments[1].variables[arity - 1],
1552 float_objective_var);
1553 CHECK_EQ(float_objective_ct->
arguments[0].floats[arity - 1], -1.0);
1554 for (
int i = 0;
i + 1 < arity; ++
i) {
1556 float_objective_ct->
arguments[1].variables[
i],
1560 -float_objective_ct->
arguments[2].floats[0]);
1562 float_objective_var->
active =
false;
1563 float_objective_ct->
active =
false;
1569 const std::string& sat_params,
1572 CpModelProtoWithMapping m;
1573 m.proto.set_name(fz_model.
name());
1578 int num_variables = 0;
1580 if (!fz_var->active)
continue;
1581 CHECK(!fz_var->domain.is_float)
1582 <<
"CP-SAT does not support float variables";
1584 m.fz_var_to_index[fz_var] = num_variables++;
1587 if (fz_var->domain.is_interval) {
1588 if (fz_var->domain.values.empty()) {
1592 LOG_FIRST_N(WARNING, 1)
1593 <<
"Using flag --fz_int_max for unbounded integer variables.";
1594 LOG_FIRST_N(WARNING, 1)
1595 <<
" actual domain is [" << -absl::GetFlag(FLAGS_fz_int_max)
1596 <<
".." << absl::GetFlag(FLAGS_fz_int_max) <<
"]";
1597 var->
add_domain(-absl::GetFlag(FLAGS_fz_int_max));
1598 var->
add_domain(absl::GetFlag(FLAGS_fz_int_max));
1610 if (fz_ct ==
nullptr || !fz_ct->active)
continue;
1613 if (absl::EndsWith(fz_ct->type,
"_reif") ||
1614 absl::EndsWith(fz_ct->type,
"_imp") || fz_ct->type ==
"array_bool_or" ||
1615 fz_ct->type ==
"array_bool_and") {
1616 m.FillReifOrImpliedConstraint(*fz_ct, ct);
1618 m.FillConstraint(*fz_ct, ct);
1649 m.parameters.set_enumerate_all_solutions(
true);
1656 m.parameters.set_max_domain_size_when_encoding_eq_neq_constraints(32);
1659 int num_workers = 1;
1666 "Search for all solutions of a SAT problem in parallel is not "
1667 "supported. Switching back to sequential search.");
1675 "The number of search workers, is not specified. For better "
1676 "performances, please set the number of workers to 8, 16, or "
1677 "more depending on the number of cores of your computer.");
1685 m.parameters.set_keep_all_feasible_solutions_in_presolve(
true);
1689 (absl::GetFlag(FLAGS_force_interleave_search) || p.
ortools_mode)) {
1690 m.parameters.set_interleave_search(
true);
1691 m.parameters.set_use_rins_lns(
false);
1692 m.parameters.add_subsolvers(
"default_lp");
1693 m.parameters.add_subsolvers(
"max_lp");
1694 m.parameters.add_subsolvers(
"quick_restart");
1695 m.parameters.add_subsolvers(
"core_or_no_lp");
1696 m.parameters.set_num_violation_ls(1);
1697 if (!m.proto.search_strategy().empty()) {
1698 m.parameters.add_subsolvers(
"fixed");
1701 }
else if (num_workers > 1 && num_workers < 8 && p.
ortools_mode) {
1702 SOLVER_LOG(logger,
"Bumping number of workers from ", num_workers,
" to 8");
1705 m.parameters.set_num_workers(num_workers);
1715 CHECK(google::protobuf::TextFormat::ParseFromString(sat_params,
1718 m.parameters.MergeFrom(flag_parameters);
1724 solution_observer = [&fz_model, &m, &p,
1726 const std::string solution_string = SolutionString(
1729 return r.solution(m.fz_var_to_index.at(v));
1731 r.objective_value());
1732 SOLVER_LOG(solution_logger, solution_string);
1733 if (p.display_statistics) {
1734 OutputFlatzincStats(r, solution_logger);
1748 if (solution_observer !=
nullptr) {
1757 CHECK(CheckSolution(
1760 return response.
solution(m.fz_var_to_index.at(v));
1771 const std::string solution_string = SolutionString(
1774 return response.
solution(m.fz_var_to_index.at(v));
1777 SOLVER_LOG(solution_logger, solution_string);
1784 SOLVER_LOG(solution_logger,
"=====UNSATISFIABLE=====");
1787 VLOG(1) <<
"%% Error message = '" << error_message <<
"'";
1788 if (absl::StrContains(error_message,
"overflow")) {
1789 SOLVER_LOG(solution_logger,
"=====OVERFLOW=====");
1791 SOLVER_LOG(solution_logger,
"=====MODEL INVALID=====");
1797 OutputFlatzincStats(response, solution_logger);
static Domain FromValues(std::vector< int64_t > values)
Domain AdditionWith(const Domain &domain) const
const std::vector< double > & float_objective_coefficients() const
void AddFloatingPointObjectiveTerm(Variable *var, double coeff)
const std::vector< Variable * > & float_objective_variables() const
const std::vector< Constraint * > & constraints() const
void SetFloatingPointObjectiveOffset(double offset)
const std::vector< Variable * > & variables() const
--— Accessors and mutators --—
double float_objective_offset() const
const std::string & name() const
const std::vector< Annotation > & search_annotations() const
Variable * objective() const
::operations_research::sat::LinearConstraintProto *PROTOBUF_NONNULL mutable_linear()
void set_name(Arg_ &&arg, Args_... args)
const ::operations_research::sat::IntegerVariableProto & variables(int index) const
int constraints_size() const
repeated .operations_research.sat.ConstraintProto constraints = 3;
::operations_research::sat::IntegerVariableProto *PROTOBUF_NONNULL add_variables()
::operations_research::sat::PartialVariableAssignment *PROTOBUF_NONNULL mutable_solution_hint()
::operations_research::sat::ConstraintProto *PROTOBUF_NONNULL add_constraints()
int variables_size() const
repeated .operations_research.sat.IntegerVariableProto variables = 2;
::operations_research::sat::IntegerVariableProto *PROTOBUF_NONNULL mutable_variables(int index)
::operations_research::sat::DecisionStrategyProto *PROTOBUF_NONNULL add_search_strategy()
void set_scaling_factor(double value)
void add_coeffs(::int64_t value)
void add_vars(::int32_t value)
::operations_research::sat::CpSolverStatus status() const
double objective_value() const
::int64_t solution(int index) const
void set_offset(double value)
void add_coeffs(double value)
void set_maximize(bool value)
void add_vars(::int32_t value)
void add_domain(::int64_t value)
void set_name(Arg_ &&arg, Args_... args)
::int64_t domain(int index) const
void add_domain(::int64_t value)
T Add(std::function< T(Model *)> f)
void Register(T *non_owned_class)
void add_values(::int64_t value)
void add_vars(::int32_t value)
static constexpr SearchBranching AUTOMATIC_SEARCH
static constexpr SearchBranching FIXED_SEARCH
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::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.
std::function< SatParameters(Model *)> NewSatParameters(absl::string_view params)
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.
int64_t Min() const
Returns the min of the domain.
std::vector< Argument > arguments
std::vector< int64_t > values
These should never be modified from outside the class.
bool is_float
Float domain.
std::vector< double > float_values
bool search_all_solutions
double max_time_in_seconds
bool display_all_solutions
#define SOLVER_LOG(logger,...)