21 #include "absl/container/flat_hash_map.h"
22 #include "absl/strings/str_cat.h"
23 #include "absl/strings/str_format.h"
24 #include "absl/strings/str_split.h"
25 #include "absl/synchronization/mutex.h"
26 #include "google/protobuf/text_format.h"
35 #include "ortools/sat/cp_model.pb.h"
50 ABSL_FLAG(
bool, use_flatzinc_format,
true,
"Output uses the flatzinc format");
52 "Default max value for unbounded integer variables.");
60 int TrueLiteral(
int var) {
return var; }
61 int FalseLiteral(
int var) {
return -
var - 1; }
62 int NegatedCpModelVariable(
int var) {
return -
var - 1; }
65 struct CpModelProtoWithMapping {
71 int LookupVar(
const fz::Argument& argument);
72 std::vector<int> LookupVars(
const fz::Argument& argument);
77 std::vector<int> CreateIntervals(
const std::vector<int>& starts,
78 const std::vector<int>& durations);
83 int GetOrCreateInterval(
int start_var,
int size_var);
89 int GetOrCreateOptionalInterval(
int start_var,
int size_var,
int opt_var);
92 void FillAMinusBInDomain(
const std::vector<int64>& domain,
93 const fz::Constraint& fz_ct, ConstraintProto*
ct);
94 void FillLinearConstraintWithGivenDomain(
const std::vector<int64>& domain,
95 const fz::Constraint& fz_ct,
97 void FillConstraint(
const fz::Constraint& fz_ct, ConstraintProto*
ct);
98 void FillReifOrImpliedConstraint(
const fz::Constraint& fz_ct,
103 void TranslateSearchAnnotations(
104 const std::vector<fz::Annotation>& search_annotations);
113 absl::flat_hash_map<std::tuple<int, int, int>,
int>
117 int CpModelProtoWithMapping::LookupConstant(
int64 value) {
124 IntegerVariableProto* var_proto =
proto.add_variables();
125 var_proto->add_domain(
value);
126 var_proto->add_domain(
value);
131 int CpModelProtoWithMapping::LookupVar(
const fz::Argument& argument) {
132 if (argument.HasOneValue())
return LookupConstant(argument.Value());
137 std::vector<int> CpModelProtoWithMapping::LookupVars(
138 const fz::Argument& argument) {
139 std::vector<int> result;
143 result.push_back(LookupConstant(
value));
146 result.push_back(LookupConstant(argument.Value()));
149 for (fz::IntegerVariable*
var : argument.variables) {
157 int CpModelProtoWithMapping::GetOrCreateInterval(
int start_var,
int size_var) {
158 return GetOrCreateOptionalInterval(start_var, size_var,
kint32max);
161 int CpModelProtoWithMapping::GetOrCreateOptionalInterval(
int start_var,
164 const std::tuple<int, int, int> key =
165 std::make_tuple(start_var, size_var, opt_var);
169 const int interval_index =
proto.constraints_size();
171 auto*
ct =
proto.add_constraints();
173 ct->add_enforcement_literal(opt_var);
180 auto* end_var =
proto.add_variables();
181 const auto start_proto =
proto.variables(start_var);
182 const auto size_proto =
proto.variables(size_var);
183 end_var->add_domain(start_proto.domain(0) + size_proto.domain(0));
184 end_var->add_domain(start_proto.domain(start_proto.domain_size() - 1) +
185 size_proto.domain(size_proto.domain_size() - 1));
187 return interval_index;
190 std::vector<int> CpModelProtoWithMapping::CreateIntervals(
191 const std::vector<int>& starts,
const std::vector<int>& durations) {
192 std::vector<int> intervals;
193 for (
int i = 0; i < starts.size(); ++i) {
194 intervals.push_back(GetOrCreateInterval(starts[i], durations[i]));
199 void CpModelProtoWithMapping::FillAMinusBInDomain(
200 const std::vector<int64>& domain,
const fz::Constraint& fz_ct,
201 ConstraintProto*
ct) {
202 auto* arg =
ct->mutable_linear();
204 const int64 value = fz_ct.arguments[1].Value();
205 const int var_a = LookupVar(fz_ct.arguments[0]);
206 for (
const int64 domain_bound : domain) {
208 arg->add_domain(domain_bound);
210 arg->add_domain(domain_bound +
value);
213 arg->add_vars(var_a);
216 const int64 value = fz_ct.arguments[0].Value();
217 const int var_b = LookupVar(fz_ct.arguments[1]);
224 arg->add_domain(
value - domain_bound);
227 arg->add_vars(var_b);
230 for (
const int64 domain_bound : domain) arg->add_domain(domain_bound);
231 arg->add_vars(LookupVar(fz_ct.arguments[0]));
233 arg->add_vars(LookupVar(fz_ct.arguments[1]));
238 void CpModelProtoWithMapping::FillLinearConstraintWithGivenDomain(
239 const std::vector<int64>& domain,
const fz::Constraint& fz_ct,
240 ConstraintProto*
ct) {
241 auto* arg =
ct->mutable_linear();
242 for (
const int64 domain_bound : domain) arg->add_domain(domain_bound);
243 std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
244 for (
int i = 0; i < vars.size(); ++i) {
245 arg->add_vars(vars[i]);
246 arg->add_coeffs(fz_ct.arguments[0].values[i]);
250 void CpModelProtoWithMapping::FillConstraint(
const fz::Constraint& fz_ct,
251 ConstraintProto*
ct) {
252 if (fz_ct.type ==
"false_constraint") {
254 ct->mutable_bool_or();
255 }
else if (fz_ct.type ==
"bool_clause") {
256 auto* arg =
ct->mutable_bool_or();
257 for (
const int var : LookupVars(fz_ct.arguments[0])) {
258 arg->add_literals(TrueLiteral(
var));
260 for (
const int var : LookupVars(fz_ct.arguments[1])) {
261 arg->add_literals(FalseLiteral(
var));
263 }
else if (fz_ct.type ==
"bool_xor") {
266 const int a = LookupVar(fz_ct.arguments[0]);
267 const int b = LookupVar(fz_ct.arguments[1]);
268 const int x = LookupVar(fz_ct.arguments[2]);
272 auto*
const refute =
ct->mutable_linear();
274 refute->add_coeffs(1);
276 refute->add_coeffs(-1);
277 refute->add_domain(0);
278 refute->add_domain(0);
281 auto* ct2 =
proto.add_constraints();
282 ct2->add_enforcement_literal(x);
283 auto*
const enforce = ct2->mutable_linear();
284 enforce->add_vars(
a);
285 enforce->add_coeffs(1);
286 enforce->add_vars(
b);
287 enforce->add_coeffs(1);
288 enforce->add_domain(1);
289 enforce->add_domain(1);
290 }
else if (fz_ct.type ==
"array_bool_or") {
291 auto* arg =
ct->mutable_bool_or();
292 for (
const int var : LookupVars(fz_ct.arguments[0])) {
293 arg->add_literals(TrueLiteral(
var));
295 }
else if (fz_ct.type ==
"array_bool_or_negated") {
296 auto* arg =
ct->mutable_bool_and();
297 for (
const int var : LookupVars(fz_ct.arguments[0])) {
298 arg->add_literals(FalseLiteral(
var));
300 }
else if (fz_ct.type ==
"array_bool_and") {
301 auto* arg =
ct->mutable_bool_and();
302 for (
const int var : LookupVars(fz_ct.arguments[0])) {
303 arg->add_literals(TrueLiteral(
var));
305 }
else if (fz_ct.type ==
"array_bool_and_negated") {
306 auto* arg =
ct->mutable_bool_or();
307 for (
const int var : LookupVars(fz_ct.arguments[0])) {
308 arg->add_literals(FalseLiteral(
var));
310 }
else if (fz_ct.type ==
"array_bool_xor") {
311 auto* arg =
ct->mutable_bool_xor();
312 for (
const int var : LookupVars(fz_ct.arguments[0])) {
313 arg->add_literals(TrueLiteral(
var));
315 }
else if (fz_ct.type ==
"bool_le" || fz_ct.type ==
"int_le") {
317 }
else if (fz_ct.type ==
"bool_ge" || fz_ct.type ==
"int_ge") {
319 }
else if (fz_ct.type ==
"bool_lt" || fz_ct.type ==
"int_lt") {
321 }
else if (fz_ct.type ==
"bool_gt" || fz_ct.type ==
"int_gt") {
323 }
else if (fz_ct.type ==
"bool_eq" || fz_ct.type ==
"int_eq" ||
324 fz_ct.type ==
"bool2int") {
325 FillAMinusBInDomain({0, 0}, fz_ct,
ct);
326 }
else if (fz_ct.type ==
"bool_ne" || fz_ct.type ==
"bool_not") {
327 auto* arg =
ct->mutable_linear();
328 arg->add_vars(LookupVar(fz_ct.arguments[0]));
330 arg->add_vars(LookupVar(fz_ct.arguments[1]));
334 }
else if (fz_ct.type ==
"int_ne") {
336 }
else if (fz_ct.type ==
"int_lin_eq") {
337 const int64 rhs = fz_ct.arguments[2].values[0];
338 FillLinearConstraintWithGivenDomain({rhs, rhs}, fz_ct,
ct);
339 }
else if (fz_ct.type ==
"bool_lin_eq") {
340 auto* arg =
ct->mutable_linear();
341 const std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
342 for (
int i = 0; i < vars.size(); ++i) {
343 arg->add_vars(vars[i]);
344 arg->add_coeffs(fz_ct.arguments[0].values[i]);
346 if (fz_ct.arguments[2].IsVariable()) {
347 arg->add_vars(LookupVar(fz_ct.arguments[2]));
352 const int64 v = fz_ct.arguments[2].Value();
356 }
else if (fz_ct.type ==
"int_lin_le" || fz_ct.type ==
"bool_lin_le") {
357 const int64 rhs = fz_ct.arguments[2].values[0];
358 FillLinearConstraintWithGivenDomain({
kint64min, rhs}, fz_ct,
ct);
359 }
else if (fz_ct.type ==
"int_lin_lt") {
360 const int64 rhs = fz_ct.arguments[2].values[0];
361 FillLinearConstraintWithGivenDomain({
kint64min, rhs - 1}, fz_ct,
ct);
362 }
else if (fz_ct.type ==
"int_lin_ge") {
363 const int64 rhs = fz_ct.arguments[2].values[0];
364 FillLinearConstraintWithGivenDomain({rhs,
kint64max}, fz_ct,
ct);
365 }
else if (fz_ct.type ==
"int_lin_gt") {
366 const int64 rhs = fz_ct.arguments[2].values[0];
367 FillLinearConstraintWithGivenDomain({rhs + 1,
kint64max}, fz_ct,
ct);
368 }
else if (fz_ct.type ==
"int_lin_ne") {
369 const int64 rhs = fz_ct.arguments[2].values[0];
370 FillLinearConstraintWithGivenDomain(
372 }
else if (fz_ct.type ==
"set_in") {
373 auto* arg =
ct->mutable_linear();
374 arg->add_vars(LookupVar(fz_ct.arguments[0]));
378 fz_ct.arguments[1].values.begin(),
379 fz_ct.arguments[1].values.end()}),
383 Domain(fz_ct.arguments[1].values[0], fz_ct.arguments[1].values[1]),
388 }
else if (fz_ct.type ==
"set_in_negated") {
389 auto* arg =
ct->mutable_linear();
390 arg->add_vars(LookupVar(fz_ct.arguments[0]));
395 std::vector<int64>{fz_ct.arguments[1].values.begin(),
396 fz_ct.arguments[1].values.end()})
401 Domain(fz_ct.arguments[1].values[0], fz_ct.arguments[1].values[1])
407 }
else if (fz_ct.type ==
"int_min") {
408 auto* arg =
ct->mutable_int_min();
409 arg->set_target(LookupVar(fz_ct.arguments[2]));
410 arg->add_vars(LookupVar(fz_ct.arguments[0]));
411 arg->add_vars(LookupVar(fz_ct.arguments[1]));
412 }
else if (fz_ct.type ==
"array_int_minimum" || fz_ct.type ==
"minimum_int") {
413 auto* arg =
ct->mutable_int_min();
414 arg->set_target(LookupVar(fz_ct.arguments[0]));
415 for (
const int var : LookupVars(fz_ct.arguments[1])) arg->add_vars(
var);
416 }
else if (fz_ct.type ==
"int_max") {
417 auto* arg =
ct->mutable_int_max();
418 arg->set_target(LookupVar(fz_ct.arguments[2]));
419 arg->add_vars(LookupVar(fz_ct.arguments[0]));
420 arg->add_vars(LookupVar(fz_ct.arguments[1]));
421 }
else if (fz_ct.type ==
"array_int_maximum" || fz_ct.type ==
"maximum_int") {
422 auto* arg =
ct->mutable_int_max();
423 arg->set_target(LookupVar(fz_ct.arguments[0]));
424 for (
const int var : LookupVars(fz_ct.arguments[1])) arg->add_vars(
var);
425 }
else if (fz_ct.type ==
"int_times") {
426 auto* arg =
ct->mutable_int_prod();
427 arg->set_target(LookupVar(fz_ct.arguments[2]));
428 arg->add_vars(LookupVar(fz_ct.arguments[0]));
429 arg->add_vars(LookupVar(fz_ct.arguments[1]));
430 }
else if (fz_ct.type ==
"int_abs") {
431 auto* arg =
ct->mutable_int_max();
432 arg->set_target(LookupVar(fz_ct.arguments[1]));
433 arg->add_vars(LookupVar(fz_ct.arguments[0]));
434 arg->add_vars(-LookupVar(fz_ct.arguments[0]) - 1);
435 }
else if (fz_ct.type ==
"int_plus") {
436 auto* arg =
ct->mutable_linear();
438 arg->add_vars(LookupVar(fz_ct.arguments[0]));
440 arg->add_vars(LookupVar(fz_ct.arguments[1]));
442 arg->add_vars(LookupVar(fz_ct.arguments[2]));
444 }
else if (fz_ct.type ==
"int_div") {
445 auto* arg =
ct->mutable_int_div();
446 arg->add_vars(LookupVar(fz_ct.arguments[0]));
447 arg->add_vars(LookupVar(fz_ct.arguments[1]));
448 arg->set_target(LookupVar(fz_ct.arguments[2]));
449 }
else if (fz_ct.type ==
"int_mod") {
450 auto* arg =
ct->mutable_int_mod();
451 arg->set_target(LookupVar(fz_ct.arguments[2]));
452 arg->add_vars(LookupVar(fz_ct.arguments[0]));
453 arg->add_vars(LookupVar(fz_ct.arguments[1]));
454 }
else if (fz_ct.type ==
"array_int_element" ||
455 fz_ct.type ==
"array_bool_element" ||
456 fz_ct.type ==
"array_var_int_element" ||
457 fz_ct.type ==
"array_var_bool_element" ||
458 fz_ct.type ==
"array_int_element_nonshifted") {
461 auto* arg =
ct->mutable_element();
462 arg->set_index(LookupVar(fz_ct.arguments[0]));
463 arg->set_target(LookupVar(fz_ct.arguments[2]));
465 if (!absl::EndsWith(fz_ct.type,
"_nonshifted")) {
469 arg->add_vars(arg->target());
471 for (
const int var : LookupVars(fz_ct.arguments[1])) arg->add_vars(
var);
475 CHECK(!absl::EndsWith(fz_ct.type,
"_nonshifted"));
476 auto* arg =
ct->mutable_table();
480 for (
const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(
var);
481 arg->add_vars(LookupVar(fz_ct.arguments[2]));
483 const std::vector<int64>& values = fz_ct.arguments[1].values;
484 const int64 coeff1 = fz_ct.arguments[3].values[0];
485 const int64 coeff2 = fz_ct.arguments[3].values[1];
486 const int64 offset = fz_ct.arguments[4].values[0] - 1;
490 const int index = coeff1 *
a + coeff2 *
b + offset;
495 arg->add_values(values[
index]);
499 }
else if (fz_ct.type ==
"ortools_table_int") {
500 auto* arg =
ct->mutable_table();
501 for (
const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(
var);
502 for (
const int64 value : fz_ct.arguments[1].values) arg->add_values(
value);
503 }
else if (fz_ct.type ==
"ortools_regular") {
504 auto* arg =
ct->mutable_automaton();
505 for (
const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(
var);
508 const int num_states = fz_ct.arguments[1].Value();
509 const int num_values = fz_ct.arguments[2].Value();
510 for (
int i = 1; i <= num_states; ++i) {
511 for (
int j = 1; j <= num_values; ++j) {
512 CHECK_LT(count, fz_ct.arguments[3].values.size());
513 const int next = fz_ct.arguments[3].values[count++];
514 if (
next == 0)
continue;
515 arg->add_transition_tail(i);
516 arg->add_transition_label(j);
517 arg->add_transition_head(
next);
521 arg->set_starting_state(fz_ct.arguments[4].Value());
522 switch (fz_ct.arguments[5].type) {
524 arg->add_final_states(fz_ct.arguments[5].values[0]);
528 for (
int v = fz_ct.arguments[5].values[0];
529 v <= fz_ct.arguments[5].values[1]; ++v) {
530 arg->add_final_states(v);
535 for (
const int v : fz_ct.arguments[5].values) {
536 arg->add_final_states(v);
541 LOG(
FATAL) <<
"Wrong constraint " << fz_ct.DebugString();
544 }
else if (fz_ct.type ==
"fzn_all_different_int") {
545 auto* arg =
ct->mutable_all_diff();
546 for (
const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(
var);
547 }
else if (fz_ct.type ==
"fzn_circuit" || fz_ct.type ==
"fzn_subcircuit") {
549 bool found_zero =
false;
550 bool found_size =
false;
552 if (fz_ct.arguments[0].variables.empty() &&
553 !fz_ct.arguments[0].values.empty()) {
555 size = fz_ct.arguments[0].values.size();
556 for (
const int64 value : fz_ct.arguments[0].values) {
557 if (
value == 0) found_zero =
true;
558 if (
value == size) found_size =
true;
561 size = fz_ct.arguments[0].variables.size();
562 for (fz::IntegerVariable*
const var : fz_ct.arguments[0].variables) {
563 if (
var->domain.Min() == 0) found_zero =
true;
564 if (
var->domain.Max() == size) found_size =
true;
568 const bool is_one_based = !found_zero || found_size;
569 const int64 min_index = is_one_based ? 1 : 0;
570 const int64 max_index = min_index + size - 1;
572 auto* circuit_arg =
ct->mutable_circuit();
577 const bool is_circuit = (fz_ct.type ==
"fzn_circuit");
578 for (
const int var : LookupVars(fz_ct.arguments[0])) {
582 domain = domain.IntersectionWith(Domain(min_index, max_index));
590 for (
const ClosedInterval
interval : domain.intervals()) {
595 auto* new_var =
proto.add_variables();
596 new_var->add_domain(0);
597 new_var->add_domain(1);
601 circuit_arg->add_tails(
index);
602 circuit_arg->add_heads(
value);
603 circuit_arg->add_literals(
literal);
607 auto*
ct =
proto.add_constraints();
609 ct->mutable_linear()->add_coeffs(1);
610 ct->mutable_linear()->add_vars(
var);
611 ct->mutable_linear()->add_domain(
value);
612 ct->mutable_linear()->add_domain(
value);
617 auto*
ct =
proto.add_constraints();
619 ct->mutable_linear()->add_coeffs(1);
620 ct->mutable_linear()->add_vars(
var);
622 ct->mutable_linear()->add_domain(
value - 1);
623 ct->mutable_linear()->add_domain(
value + 1);
631 }
else if (fz_ct.type ==
"fzn_inverse") {
632 auto* arg =
ct->mutable_inverse();
634 const auto direct_variables = LookupVars(fz_ct.arguments[0]);
635 const auto inverse_variables = LookupVars(fz_ct.arguments[1]);
637 const int num_variables =
638 std::min(direct_variables.size(), inverse_variables.size());
641 bool found_zero =
false;
642 bool found_size =
false;
643 for (fz::IntegerVariable*
const var : fz_ct.arguments[0].variables) {
644 if (
var->domain.Min() == 0) found_zero =
true;
645 if (
var->domain.Max() == num_variables) found_size =
true;
647 for (fz::IntegerVariable*
const var : fz_ct.arguments[1].variables) {
648 if (
var->domain.Min() == 0) found_zero =
true;
649 if (
var->domain.Max() == num_variables) found_size =
true;
653 const bool is_one_based = !found_zero || found_size;
654 const int offset = is_one_based ? 1 : 0;
656 if (is_one_based) arg->add_f_direct(LookupConstant(0));
657 for (
const int var : direct_variables) {
658 arg->add_f_direct(
var);
666 if (is_one_based) arg->add_f_inverse(LookupConstant(0));
667 for (
const int var : inverse_variables) {
668 arg->add_f_inverse(
var);
675 }
else if (fz_ct.type ==
"fzn_cumulative") {
676 const std::vector<int> starts = LookupVars(fz_ct.arguments[0]);
677 const std::vector<int> durations = LookupVars(fz_ct.arguments[1]);
678 const std::vector<int> demands = LookupVars(fz_ct.arguments[2]);
679 const int capacity = LookupVar(fz_ct.arguments[3]);
681 auto* arg =
ct->mutable_cumulative();
683 for (
int i = 0; i < starts.size(); ++i) {
686 if (
proto.variables(demands[i]).domain().size() == 2 &&
687 proto.variables(demands[i]).domain(0) == 0 &&
688 proto.variables(demands[i]).domain(1) == 1 &&
691 GetOrCreateOptionalInterval(starts[i], durations[i], demands[i]));
692 arg->add_demands(LookupConstant(1));
694 arg->add_intervals(GetOrCreateInterval(starts[i], durations[i]));
695 arg->add_demands(demands[i]);
698 }
else if (fz_ct.type ==
"fzn_diffn" || fz_ct.type ==
"fzn_diffn_nonstrict") {
699 const std::vector<int> x = LookupVars(fz_ct.arguments[0]);
700 const std::vector<int> y = LookupVars(fz_ct.arguments[1]);
701 const std::vector<int> dx = LookupVars(fz_ct.arguments[2]);
702 const std::vector<int> dy = LookupVars(fz_ct.arguments[3]);
703 const std::vector<int> x_intervals = CreateIntervals(x, dx);
704 const std::vector<int> y_intervals = CreateIntervals(y, dy);
705 auto* arg =
ct->mutable_no_overlap_2d();
706 for (
int i = 0; i < x.size(); ++i) {
707 arg->add_x_intervals(x_intervals[i]);
708 arg->add_y_intervals(y_intervals[i]);
710 arg->set_boxes_with_null_area_can_overlap(fz_ct.type ==
711 "fzn_diffn_nonstrict");
712 }
else if (fz_ct.type ==
"ortools_network_flow" ||
713 fz_ct.type ==
"ortools_network_flow_cost") {
716 const bool has_cost = fz_ct.type ==
"ortools_network_flow_cost";
717 const std::vector<int> flow = LookupVars(fz_ct.arguments[has_cost ? 3 : 2]);
720 const int num_nodes = fz_ct.arguments[1].values.size();
721 std::vector<std::vector<int>> flows_per_node(num_nodes);
722 std::vector<std::vector<int>> coeffs_per_node(num_nodes);
723 const int num_arcs = fz_ct.arguments[0].values.size() / 2;
724 for (
int arc = 0; arc < num_arcs; arc++) {
725 const int tail = fz_ct.arguments[0].values[2 * arc] - 1;
726 const int head = fz_ct.arguments[0].values[2 * arc + 1] - 1;
729 flows_per_node[
tail].push_back(flow[arc]);
730 coeffs_per_node[
tail].push_back(1);
731 flows_per_node[
head].push_back(flow[arc]);
732 coeffs_per_node[
head].push_back(-1);
734 for (
int node = 0; node < num_nodes; node++) {
735 auto* arg =
proto.add_constraints()->mutable_linear();
736 arg->add_domain(fz_ct.arguments[1].values[node]);
737 arg->add_domain(fz_ct.arguments[1].values[node]);
738 for (
int i = 0; i < flows_per_node[node].size(); ++i) {
739 arg->add_vars(flows_per_node[node][i]);
740 arg->add_coeffs(coeffs_per_node[node][i]);
745 auto* arg =
proto.add_constraints()->mutable_linear();
748 for (
int arc = 0; arc < num_arcs; arc++) {
749 const int64 weight = fz_ct.arguments[2].values[arc];
751 arg->add_vars(flow[arc]);
755 arg->add_vars(LookupVar(fz_ct.arguments[4]));
759 LOG(
FATAL) <<
" Not supported " << fz_ct.type;
763 void CpModelProtoWithMapping::FillReifOrImpliedConstraint(
764 const fz::Constraint& fz_ct, ConstraintProto*
ct) {
766 std::string simplified_type;
767 if (absl::EndsWith(fz_ct.type,
"_reif")) {
769 simplified_type = fz_ct.type.substr(0, fz_ct.type.size() - 5);
770 }
else if (absl::EndsWith(fz_ct.type,
"_imp")) {
772 simplified_type = fz_ct.type.substr(0, fz_ct.type.size() - 4);
775 simplified_type = fz_ct.type;
779 fz::Constraint copy = fz_ct;
780 copy.type = simplified_type;
783 FillConstraint(copy,
ct);
786 std::string negated_type;
789 if (simplified_type ==
"array_bool_or") {
790 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[1])));
791 negated_type =
"array_bool_or_negated";
792 }
else if (simplified_type ==
"array_bool_and") {
793 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[1])));
794 negated_type =
"array_bool_and_negated";
795 }
else if (simplified_type ==
"set_in") {
796 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
797 negated_type =
"set_in_negated";
798 }
else if (simplified_type ==
"bool_eq" || simplified_type ==
"int_eq") {
799 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
800 negated_type =
"int_ne";
801 }
else if (simplified_type ==
"bool_ne" || simplified_type ==
"int_ne") {
802 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
803 negated_type =
"int_eq";
804 }
else if (simplified_type ==
"bool_le" || simplified_type ==
"int_le") {
805 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
806 negated_type =
"int_gt";
807 }
else if (simplified_type ==
"bool_lt" || simplified_type ==
"int_lt") {
808 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
809 negated_type =
"int_ge";
810 }
else if (simplified_type ==
"bool_ge" || simplified_type ==
"int_ge") {
811 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
812 negated_type =
"int_lt";
813 }
else if (simplified_type ==
"bool_gt" || simplified_type ==
"int_gt") {
814 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[2])));
815 negated_type =
"int_le";
816 }
else if (simplified_type ==
"int_lin_eq") {
817 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
818 negated_type =
"int_lin_ne";
819 }
else if (simplified_type ==
"int_lin_ne") {
820 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
821 negated_type =
"int_lin_eq";
822 }
else if (simplified_type ==
"int_lin_le") {
823 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
824 negated_type =
"int_lin_gt";
825 }
else if (simplified_type ==
"int_lin_ge") {
826 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
827 negated_type =
"int_lin_lt";
828 }
else if (simplified_type ==
"int_lin_lt") {
829 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
830 negated_type =
"int_lin_ge";
831 }
else if (simplified_type ==
"int_lin_gt") {
832 ct->add_enforcement_literal(TrueLiteral(LookupVar(fz_ct.arguments[3])));
833 negated_type =
"int_lin_le";
835 LOG(
FATAL) <<
"Unsupported " << simplified_type;
839 if (absl::EndsWith(fz_ct.type,
"_imp"))
return;
843 ConstraintProto* negated_ct =
proto.add_constraints();
844 negated_ct->set_name(fz_ct.type +
" (negated)");
845 negated_ct->add_enforcement_literal(
847 copy.type = negated_type;
848 FillConstraint(copy, negated_ct);
851 void CpModelProtoWithMapping::TranslateSearchAnnotations(
852 const std::vector<fz::Annotation>& search_annotations) {
853 std::vector<fz::Annotation> flat_annotations;
854 for (
const fz::Annotation& annotation : search_annotations) {
858 for (
const fz::Annotation& annotation : flat_annotations) {
859 if (annotation.IsFunctionCallWithIdentifier(
"int_search") ||
860 annotation.IsFunctionCallWithIdentifier(
"bool_search")) {
861 const std::vector<fz::Annotation>& args = annotation.annotations;
862 std::vector<fz::IntegerVariable*> vars;
863 args[0].AppendAllIntegerVariables(&vars);
865 DecisionStrategyProto* strategy =
proto.add_search_strategy();
866 for (fz::IntegerVariable* v : vars) {
870 const fz::Annotation& choose = args[1];
871 if (choose.id ==
"input_order") {
872 strategy->set_variable_selection_strategy(
873 DecisionStrategyProto::CHOOSE_FIRST);
874 }
else if (choose.id ==
"first_fail") {
875 strategy->set_variable_selection_strategy(
876 DecisionStrategyProto::CHOOSE_MIN_DOMAIN_SIZE);
877 }
else if (choose.id ==
"anti_first_fail") {
878 strategy->set_variable_selection_strategy(
879 DecisionStrategyProto::CHOOSE_MAX_DOMAIN_SIZE);
880 }
else if (choose.id ==
"smallest") {
881 strategy->set_variable_selection_strategy(
882 DecisionStrategyProto::CHOOSE_LOWEST_MIN);
883 }
else if (choose.id ==
"largest") {
884 strategy->set_variable_selection_strategy(
885 DecisionStrategyProto::CHOOSE_HIGHEST_MAX);
887 LOG(
FATAL) <<
"Unsupported order: " << choose.id;
890 const fz::Annotation& select = args[2];
891 if (select.id ==
"indomain_min" || select.id ==
"indomain") {
892 strategy->set_domain_reduction_strategy(
893 DecisionStrategyProto::SELECT_MIN_VALUE);
894 }
else if (select.id ==
"indomain_max") {
895 strategy->set_domain_reduction_strategy(
896 DecisionStrategyProto::SELECT_MAX_VALUE);
897 }
else if (select.id ==
"indomain_split") {
898 strategy->set_domain_reduction_strategy(
899 DecisionStrategyProto::SELECT_LOWER_HALF);
900 }
else if (select.id ==
"indomain_reverse_split") {
901 strategy->set_domain_reduction_strategy(
902 DecisionStrategyProto::SELECT_UPPER_HALF);
903 }
else if (select.id ==
"indomain_median") {
904 strategy->set_domain_reduction_strategy(
905 DecisionStrategyProto::SELECT_MEDIAN_VALUE);
907 LOG(
FATAL) <<
"Unsupported select: " << select.id;
914 std::string SolutionString(
915 const fz::SolutionOutputSpecs& output,
916 const std::function<
int64(fz::IntegerVariable*)>& value_func) {
917 if (output.variable !=
nullptr) {
918 const int64 value = value_func(output.variable);
919 if (output.display_as_boolean) {
920 return absl::StrCat(output.name,
" = ",
value == 1 ?
"true" :
"false",
923 return absl::StrCat(output.name,
" = ",
value,
";");
926 const int bound_size = output.bounds.size();
928 absl::StrCat(output.name,
" = array", bound_size,
"d(");
929 for (
int i = 0; i < bound_size; ++i) {
930 if (output.bounds[i].max_value >= output.bounds[i].min_value) {
931 absl::StrAppend(&result, output.bounds[i].min_value,
"..",
932 output.bounds[i].max_value,
", ");
934 result.append(
"{},");
938 for (
int i = 0; i < output.flat_variables.size(); ++i) {
939 const int64 value = value_func(output.flat_variables[i]);
940 if (output.display_as_boolean) {
941 result.append(
value ?
"true" :
"false");
943 absl::StrAppend(&result,
value);
945 if (i != output.flat_variables.size() - 1) {
949 result.append(
"]);");
955 std::string SolutionString(
956 const fz::Model&
model,
957 const std::function<
int64(fz::IntegerVariable*)>& value_func) {
958 std::string solution_string;
959 for (
const auto& output_spec :
model.output()) {
960 solution_string.append(SolutionString(output_spec, value_func));
961 solution_string.append(
"\n");
963 return solution_string;
966 void LogInFlatzincFormat(
const std::string& multi_line_input) {
967 std::vector<std::string> lines =
968 absl::StrSplit(multi_line_input,
'\n', absl::SkipEmpty());
969 for (
const std::string& line : lines) {
974 void OutputFlatzincStats(
const CpSolverResponse&
response) {
975 std::cout <<
"%%%mzn-stat: objective=" <<
response.objective_value()
977 std::cout <<
"%%%mzn-stat: objectiveBound=" <<
response.best_objective_bound()
979 std::cout <<
"%%%mzn-stat: boolVariables=" <<
response.num_booleans()
981 std::cout <<
"%%%mzn-stat: failures=" <<
response.num_conflicts()
983 std::cout <<
"%%%mzn-stat: propagations="
984 <<
response.num_binary_propagations() +
987 std::cout <<
"%%%mzn-stat: solveTime=" <<
response.wall_time() << std::endl;
994 const std::string& sat_params) {
995 if (!absl::GetFlag(FLAGS_use_flatzinc_format)) {
996 LOG(
INFO) <<
"*** Starting translation to CP-SAT";
998 FZLOG <<
"*** Starting translation to CP-SAT" <<
FZENDL;
1001 CpModelProtoWithMapping m;
1002 m.proto.set_name(fz_model.
name());
1007 int num_variables = 0;
1009 if (!fz_var->active)
continue;
1010 m.fz_var_to_index[fz_var] = num_variables++;
1011 IntegerVariableProto*
var = m.proto.add_variables();
1012 var->set_name(fz_var->name);
1013 if (fz_var->domain.is_interval) {
1014 if (fz_var->domain.values.empty()) {
1019 <<
"Using flag --fz_int_max for unbounded integer variables.";
1021 <<
" actual domain is [" << -absl::GetFlag(FLAGS_fz_int_max)
1022 <<
".." << absl::GetFlag(FLAGS_fz_int_max) <<
"]";
1023 var->add_domain(-absl::GetFlag(FLAGS_fz_int_max));
1024 var->add_domain(absl::GetFlag(FLAGS_fz_int_max));
1026 var->add_domain(fz_var->domain.values[0]);
1027 var->add_domain(fz_var->domain.values[1]);
1036 if (fz_ct ==
nullptr || !fz_ct->active)
continue;
1037 ConstraintProto*
ct = m.proto.add_constraints();
1038 ct->set_name(fz_ct->type);
1039 if (absl::EndsWith(fz_ct->type,
"_reif") ||
1040 absl::EndsWith(fz_ct->type,
"_imp") || fz_ct->type ==
"array_bool_or" ||
1041 fz_ct->type ==
"array_bool_and") {
1042 m.FillReifOrImpliedConstraint(*fz_ct,
ct);
1044 m.FillConstraint(*fz_ct,
ct);
1050 CpObjectiveProto* objective = m.proto.mutable_objective();
1051 objective->add_coeffs(1);
1053 objective->set_scaling_factor(-1);
1054 objective->add_vars(
1055 NegatedCpModelVariable(m.fz_var_to_index[fz_model.
objective()]));
1057 objective->add_vars(m.fz_var_to_index[fz_model.
objective()]);
1071 m.parameters.set_enumerate_all_solutions(
true);
1074 m.parameters.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
1076 m.parameters.set_interleave_search(
true);
1077 m.parameters.set_reduce_memory_usage_in_interleave_mode(
true);
1080 m.parameters.set_search_branching(SatParameters::FIXED_SEARCH);
1090 m.parameters.set_num_search_workers(1);
1097 sat::SatParameters flag_parameters;
1098 CHECK(google::protobuf::TextFormat::ParseFromString(sat_params,
1101 m.parameters.MergeFrom(flag_parameters);
1104 std::function<void(
const CpSolverResponse&)> solution_observer =
nullptr;
1106 solution_observer = [&fz_model, &m, &p](
const CpSolverResponse& r) {
1107 const std::string solution_string =
1111 std::cout << solution_string << std::endl;
1113 OutputFlatzincStats(r);
1115 std::cout <<
"----------" << std::endl;
1121 if (solution_observer !=
nullptr) {
1127 if (
response.status() == CpSolverStatus::FEASIBLE ||
1128 response.status() == CpSolverStatus::OPTIMAL) {
1135 if (absl::GetFlag(FLAGS_use_flatzinc_format)) {
1136 if (
response.status() == CpSolverStatus::FEASIBLE ||
1137 response.status() == CpSolverStatus::OPTIMAL) {
1139 const std::string solution_string =
1143 std::cout << solution_string << std::endl;
1144 std::cout <<
"----------" << std::endl;
1146 if (
response.status() == CpSolverStatus::OPTIMAL) {
1147 std::cout <<
"==========" << std::endl;
1149 }
else if (
response.status() == CpSolverStatus::INFEASIBLE) {
1150 std::cout <<
"=====UNSATISFIABLE=====" << std::endl;
1151 }
else if (
response.status() == CpSolverStatus::MODEL_INVALID) {
1153 VLOG(1) <<
"%% Error message = '" << error_message <<
"'";
1154 if (absl::StrContains(error_message,
"overflow")) {
1155 std::cout <<
"=====OVERFLOW=====" << std::endl;
1157 std::cout <<
"=====MODEL INVALID=====" << std::endl;
1160 std::cout <<
"%% TIMEOUT" << std::endl;
#define LOG_FIRST_N(severity, n)
#define CHECK_LT(val1, val2)
#define CHECK_EQ(val1, val2)
#define CHECK_GE(val1, val2)
#define VLOG(verboselevel)
static Domain FromValues(std::vector< int64 > values)
Creates a domain from the union of an unsorted list of integer values.
Domain IntersectionWith(const Domain &domain) const
Returns the intersection of D and domain.
static Domain FromIntervals(absl::Span< const ClosedInterval > intervals)
Creates a domain from the union of an unsorted list of intervals.
const std::vector< Constraint * > & constraints() const
IntegerVariable * objective() const
const std::vector< Annotation > & search_annotations() const
const std::vector< IntegerVariable * > & variables() const
const std::string & name() const
Class that owns everything related to a particular optimization model.
T Add(std::function< T(Model *)> f)
This makes it possible to have a nicer API on the client side, and it allows both of these forms:
absl::flat_hash_map< fz::IntegerVariable *, int > fz_var_to_index
absl::flat_hash_map< std::tuple< int, int, int >, int > start_size_opt_tuple_to_interval
ABSL_FLAG(bool, use_flatzinc_format, true, "Output uses the flatzinc format")
absl::flat_hash_map< int64, int > constant_value_to_index
SharedResponseManager * response
static const int64 kint64max
static const int32 kint32max
static const int64 kint64min
bool ContainsKey(const Collection &collection, const Key &key)
const Collection::value_type::second_type & FindOrDie(const Collection &collection, const typename Collection::value_type::first_type &key)
ReverseView< Container > reversed_view(const Container &c)
void FlattenAnnotations(const Annotation &ann, std::vector< Annotation > *out)
bool CheckSolution(const Model &model, const std::function< int64(IntegerVariable *)> &evaluator)
std::function< void(Model *)> NewFeasibleSolutionObserver(const std::function< void(const CpSolverResponse &response)> &observer)
Creates a solution observer with the model with model.Add(NewFeasibleSolutionObserver([](response){....
std::function< SatParameters(Model *)> NewSatParameters(const std::string ¶ms)
Creates parameters for the solver, which you can add to the model with.
std::vector< int64 > AllValuesInDomain(const ProtoWithDomain &proto)
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
std::string CpModelStats(const CpModelProto &model_proto)
Returns a string with some statistics on the given CpModelProto.
CpSolverResponse SolveCpModel(const CpModelProto &model_proto, Model *model)
Solves the given CpModelProto.
void SolveFzWithCpModelProto(const fz::Model &fz_model, const fz::FlatzincSatParameters &p, const std::string &sat_params)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
std::string ValidateCpModel(const CpModelProto &model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
double max_time_in_seconds
bool display_all_solutions