26#include "absl/algorithm/container.h"
27#include "absl/container/btree_map.h"
28#include "absl/container/flat_hash_map.h"
29#include "absl/container/flat_hash_set.h"
30#include "absl/flags/flag.h"
31#include "absl/log/check.h"
32#include "absl/meta/type_traits.h"
33#include "absl/strings/str_cat.h"
34#include "absl/types/span.h"
45ABSL_FLAG(
bool, cp_model_check_dependent_variables,
false,
46 "When true, check that solutions can be computed only from their "
58#define RETURN_IF_NOT_EMPTY(statement) \
60 const std::string error_message = statement; \
61 if (!error_message.empty()) return error_message; \
64template <
typename ProtoWithDomain>
65bool DomainInProtoIsValid(
const ProtoWithDomain& proto) {
66 if (proto.domain().size() % 2)
return false;
67 std::vector<ClosedInterval> domain;
68 for (
int i = 0;
i < proto.domain_size();
i += 2) {
69 if (proto.domain(
i) > proto.domain(
i + 1))
return false;
70 domain.push_back({proto.domain(
i), proto.domain(
i + 1)});
75bool VariableReferenceIsValid(
const CpModelProto& model,
int reference) {
77 if (reference >= model.variables_size())
return false;
78 return reference >= -
static_cast<int>(model.variables_size());
85bool VariableIndexIsValid(
const CpModelProto& model,
int var) {
86 return var >= 0 && var < model.variables_size();
89bool LiteralReferenceIsValid(
const CpModelProto& model,
int reference) {
90 if (!VariableReferenceIsValid(model, reference))
return false;
91 const auto& var_proto = model.variables(
PositiveRef(reference));
92 const int64_t min_domain = var_proto.domain(0);
93 const int64_t max_domain = var_proto.domain(var_proto.domain_size() - 1);
94 return min_domain >= 0 && max_domain <= 1;
97std::string ValidateIntegerVariable(
const CpModelProto& model,
int v) {
99 if (proto.domain_size() == 0) {
100 return absl::StrCat(
"var #", v,
103 if (proto.domain_size() % 2 != 0) {
104 return absl::StrCat(
"var #", v,
" has an odd domain() size: ",
107 if (!DomainInProtoIsValid(proto)) {
108 return absl::StrCat(
"var #", v,
" has and invalid domain() format: ",
115 const int64_t lb = proto.
domain(0);
116 const int64_t ub = proto.domain(proto.domain_size() - 1);
117 if (lb < -std::numeric_limits<int64_t>::max() / 2 ||
118 ub > std::numeric_limits<int64_t>::max() / 2) {
120 "var #", v,
" domain do not fall in [-kint64max / 2, kint64max / 2]. ",
126 if (lb < 0 && lb + std::numeric_limits<int64_t>::max() < ub) {
129 " has a domain that is too large, i.e. |UB - LB| overflow an int64_t: ",
136std::string ValidateVariablesUsedInConstraint(
const CpModelProto& model,
140 for (
const int v : references.variables) {
141 if (!VariableReferenceIsValid(model, v)) {
142 return absl::StrCat(
"Out of bound integer variable ", v,
143 " in constraint #", c,
" : ",
147 for (
const int lit : ct.enforcement_literal()) {
148 if (!LiteralReferenceIsValid(model, lit)) {
149 return absl::StrCat(
"Invalid enforcement literal ", lit,
150 " in constraint #", c,
" : ",
154 for (
const int lit : references.literals) {
155 if (!LiteralReferenceIsValid(model, lit)) {
156 return absl::StrCat(
"Invalid literal ", lit,
" in constraint #", c,
" : ",
163std::string ValidateIntervalsUsedInConstraint(
bool after_presolve,
169 return absl::StrCat(
"Out of bound interval ",
i,
" in constraint #", c,
172 if (after_presolve &&
i >= c) {
173 return absl::StrCat(
"Interval ",
i,
" in constraint #", c,
174 " must appear before in the list of constraints :",
177 if (model.constraints(
i).constraint_case() !=
181 " does not refer to an interval constraint. Problematic constraint #",
191 return var_proto.domain(0);
193 return -var_proto.domain(var_proto.domain_size() - 1);
200 return var_proto.domain(var_proto.domain_size() - 1);
202 return -var_proto.domain(0);
206template <
class LinearExpressionProto>
209 int64_t sum_min = proto.offset();
210 for (
int i = 0;
i < proto.vars_size(); ++
i) {
211 const int ref = proto.vars(
i);
212 const int64_t coeff = proto.coeffs(
i);
214 CapAdd(sum_min, coeff >= 0 ?
CapProd(MinOfRef(model, ref), coeff)
215 :
CapProd(MaxOfRef(model, ref), coeff));
221template <
class LinearExpressionProto>
224 int64_t sum_max = proto.offset();
225 for (
int i = 0;
i < proto.vars_size(); ++
i) {
226 const int ref = proto.vars(
i);
227 const int64_t coeff = proto.coeffs(
i);
229 CapAdd(sum_max, coeff >= 0 ?
CapProd(MaxOfRef(model, ref), coeff)
230 :
CapProd(MinOfRef(model, ref), coeff));
238 for (
int i = 0;
i < expr.vars_size(); ++
i) {
239 if (expr.coeffs(
i) == 0)
continue;
241 if (var_proto.domain_size() != 2 ||
242 var_proto.domain(0) != var_proto.domain(1)) {
251 DCHECK(ExpressionIsFixed(model, expr));
252 return MinOfExpression(model, expr);
255int64_t IntervalSizeMax(
const CpModelProto& model,
int interval_index) {
257 model.constraints(interval_index).constraint_case());
259 model.constraints(interval_index).interval();
260 return MaxOfExpression(model, proto.size());
270 if (expr.coeffs_size() != expr.vars_size()) {
271 return absl::StrCat(
"coeffs_size() != vars_size() in linear expression: ",
276 return absl::StrCat(
"Possible overflow in linear expression: ",
279 for (
const int var : expr.vars()) {
281 return absl::StrCat(
"Invalid negated variable in linear expression: ",
288std::string ValidateAffineExpression(
const CpModelProto& model,
290 if (expr.vars_size() > 1) {
291 return absl::StrCat(
"expression must be affine: ",
297std::string ValidateConstantAffineExpression(
299 if (!expr.vars().empty()) {
300 return absl::StrCat(
"expression must be constant: ",
306std::string ValidateLinearConstraint(
const CpModelProto& model,
308 if (!DomainInProtoIsValid(ct.linear())) {
309 return absl::StrCat(
"Invalid domain in constraint : ",
312 if (ct.linear().coeffs_size() != ct.linear().vars_size()) {
313 return absl::StrCat(
"coeffs_size() != vars_size() in constraint: ",
316 for (
const int var : ct.linear().vars()) {
318 return absl::StrCat(
"Invalid negated variable in linear constraint: ",
324 return "Possible integer overflow in constraint: " +
330std::string ValidateIntModConstraint(
const CpModelProto& model,
332 if (ct.int_mod().exprs().size() != 2) {
333 return absl::StrCat(
"An int_mod constraint should have exactly 2 terms: ",
336 if (!ct.int_mod().has_target()) {
337 return absl::StrCat(
"An int_mod constraint should have a target: ",
346 if (MinOfExpression(model, mod_expr) <= 0) {
348 "An int_mod must have a strictly positive modulo argument: ",
355std::string ValidateIntProdConstraint(
const CpModelProto& model,
357 if (!ct.int_prod().has_target()) {
358 return absl::StrCat(
"An int_prod constraint should have a target: ",
368 Domain product_domain(1);
370 const int64_t min_expr = MinOfExpression(model, expr);
371 const int64_t max_expr = MaxOfExpression(model, expr);
372 if (min_expr == 0 && max_expr == 0) {
377 product_domain.ContinuousMultiplicationBy({min_expr, max_expr});
380 if (product_domain.Max() <= -std ::numeric_limits<int64_t>::max() ||
381 product_domain.Min() >= std::numeric_limits<int64_t>::max()) {
382 return absl::StrCat(
"integer overflow in constraint: ",
388 if (ct.int_prod().exprs_size() > 2 &&
389 (product_domain.Max() >= std ::numeric_limits<int64_t>::max() ||
390 product_domain.Min() <= -std::numeric_limits<int64_t>::max())) {
391 return absl::StrCat(
"Potential integer overflow in constraint: ",
398std::string ValidateIntDivConstraint(
const CpModelProto& model,
400 if (ct.int_div().exprs().size() != 2) {
401 return absl::StrCat(
"An int_div constraint should have exactly 2 terms: ",
404 if (!ct.int_div().has_target()) {
405 return absl::StrCat(
"An int_div constraint should have a target: ",
414 const int64_t offset = denom.
offset();
415 if (ExpressionIsFixed(model, denom)) {
416 if (ExpressionFixedValue(model, denom) == 0) {
420 const int64_t coeff = denom.coeffs(0);
422 const int64_t inverse_of_zero = -offset / coeff;
423 if (inverse_of_zero * coeff + offset == 0 &&
424 DomainOfRef(model, denom.vars(0)).Contains(inverse_of_zero)) {
425 return absl::StrCat(
"The domain of the divisor cannot contain 0: ",
435 output->mutable_vars()->Add(
input.vars().begin(),
input.vars().end());
436 for (
const int64_t coeff :
input.coeffs()) {
437 output->add_coeffs(coeff * prod);
443 CapAdd(std::abs(output->offset()), std::abs(
input.offset())));
446std::string ValidateElementConstraint(
const CpModelProto& model,
451 element.has_linear_target() ||
452 !element.exprs().empty();
453 const bool in_legacy_format =
454 !element.vars().empty() || element.index() != 0 || element.target() != 0;
455 if (in_linear_format && in_legacy_format) {
457 "Inconsistent element with both legacy and new format defined",
461 if (element.vars().empty() && element.exprs().empty()) {
462 return "Empty element constraint is interpreted as vars[], thus invalid "
463 "since the index will be out of bounds.";
468 if (!element.vars().empty()) {
470 overflow_detection.
add_vars(element.target());
471 overflow_detection.add_coeffs(1);
472 overflow_detection.add_vars( 0);
473 overflow_detection.add_coeffs(-1);
474 for (
const int ref : element.vars()) {
475 if (!VariableIndexIsValid(model, ref)) {
476 return absl::StrCat(
"Element vars must be valid variables: ",
479 overflow_detection.set_vars(1, ref);
481 overflow_detection.coeffs())) {
483 "Domain of the variables involved in element constraint may cause "
490 if (in_legacy_format) {
491 if (!VariableIndexIsValid(model, element.index()) ||
492 !VariableIndexIsValid(model, element.target())) {
494 "Element constraint index and target must valid variables: ",
499 if (in_linear_format) {
501 ValidateAffineExpression(model, element.linear_index()));
503 ValidateAffineExpression(model, element.linear_target()));
507 AppendToOverflowValidator(expr, &overflow_detection, -1);
508 const int64_t offset =
CapSub(overflow_detection.offset(), expr.offset());
509 overflow_detection.set_offset(offset);
511 overflow_detection.coeffs(),
512 overflow_detection.offset())) {
514 "Domain of the variables involved in element constraint may cause "
523std::string ValidateTableConstraint(
const CpModelProto& model,
526 if (!arg.vars().empty() && !arg.exprs().empty()) {
528 "Inconsistent table with both legacy and new format defined: ",
531 if (arg.vars().empty() && arg.exprs().empty() && !arg.values().empty()) {
533 "Inconsistent table empty expressions and non-empty tuples: ",
536 if (arg.vars().empty() && arg.exprs().empty() && arg.values().empty()) {
539 const int arity = arg.
vars().empty() ? arg.exprs().size() : arg.vars().size();
540 if (arg.values().size() % arity != 0) {
542 "The flat encoding of a table constraint tuples must be a multiple of "
543 "the number of expressions: ",
546 for (
const int var : arg.vars()) {
547 if (!VariableIndexIsValid(model, var)) {
548 return absl::StrCat(
"Invalid variable index in table constraint: ", var);
557std::string ValidateAutomatonConstraint(
const CpModelProto& model,
560 if (!automaton.vars().empty() && !automaton.exprs().empty()) {
562 "Inconsistent automaton with both legacy and new format defined: ",
566 if (num_transistions != automaton.transition_head().size() ||
567 num_transistions != automaton.transition_label().size()) {
569 "The transitions repeated fields must have the same size: ",
572 for (
const int var : automaton.vars()) {
573 if (!VariableIndexIsValid(model, var)) {
574 return absl::StrCat(
"Invalid variable index in automaton constraint: ",
581 absl::flat_hash_map<std::pair<int64_t, int64_t>, int64_t> tail_label_to_head;
582 for (
int i = 0;
i < num_transistions; ++
i) {
583 const int64_t tail = automaton.transition_tail(
i);
584 const int64_t head = automaton.transition_head(
i);
585 const int64_t label = automaton.transition_label(
i);
586 if (label <= std::numeric_limits<int64_t>::min() + 1 ||
587 label == std::numeric_limits<int64_t>::max()) {
588 return absl::StrCat(
"labels in the automaton constraint are too big: ",
591 const auto [it, inserted] =
592 tail_label_to_head.insert({{tail, label}, head});
594 if (it->second == head) {
595 return absl::StrCat(
"automaton: duplicate transition ", tail,
" --(",
596 label,
")--> ", head);
598 return absl::StrCat(
"automaton: incompatible transitions ", tail,
599 " --(", label,
")--> ", head,
" and ", tail,
" --(",
600 label,
")--> ", it->second);
607template <
typename GraphProto>
608std::string ValidateGraphInput(
bool is_route,
const GraphProto& graph) {
609 const int size = graph.tails().size();
610 if (graph.heads().size() != size || graph.literals().size() != size) {
611 return absl::StrCat(
"Wrong field sizes in graph: ",
616 absl::flat_hash_set<int> self_loops;
617 for (
int i = 0;
i < size; ++
i) {
618 if (graph.heads(
i) != graph.tails(
i))
continue;
619 if (!self_loops.insert(graph.heads(
i)).second) {
621 "Circuit/Route constraint contains multiple self-loop involving "
625 if (is_route && graph.tails(
i) == 0) {
627 "A route constraint cannot have a self-loop on the depot (node 0)");
634std::string ValidateRoutesConstraint(
const CpModelProto& model,
637 absl::flat_hash_set<int> nodes;
638 for (
const int node : ct.routes().tails()) {
640 return "All node in a route constraint must be in [0, num_nodes)";
643 max_node = std::max(max_node, node);
645 for (
const int node : ct.routes().heads()) {
647 return "All node in a route constraint must be in [0, num_nodes)";
650 max_node = std::max(max_node, node);
652 if (!nodes.empty() && max_node != nodes.size() - 1) {
654 "All nodes in a route constraint must have incident arcs");
658 ct.routes().dimensions()) {
659 if (dimension.exprs().size() != nodes.size()) {
661 "If the dimensions field in a route constraint is set, its elements "
662 "must be of size num_nodes:",
666 for (
const int v : expr.vars()) {
667 if (!VariableReferenceIsValid(model, v)) {
668 return absl::StrCat(
"Out of bound integer variable ", v,
669 " in route constraint ",
677 return ValidateGraphInput(
true, ct.routes());
680std::string ValidateIntervalConstraint(
const CpModelProto& model,
682 if (ct.enforcement_literal().size() > 1) {
684 "Interval with more than one enforcement literals are currently not "
690 if (!arg.has_start()) {
691 return absl::StrCat(
"Interval must have a start expression: ",
694 if (!arg.has_size()) {
695 return absl::StrCat(
"Interval must have a size expression: ",
698 if (!arg.has_end()) {
699 return absl::StrCat(
"Interval must have a end expression: ",
704 if (arg.start().vars_size() > 1) {
705 return "Interval with a start expression containing more than one "
706 "variable are currently not supported.";
709 AppendToOverflowValidator(arg.start(), &for_overflow_validation);
710 if (arg.size().vars_size() > 1) {
711 return "Interval with a size expression containing more than one "
712 "variable are currently not supported.";
715 if (ct.enforcement_literal().empty() &&
716 MinOfExpression(model, arg.size()) < 0) {
718 "The size of a performed interval must be >= 0 in constraint: ",
721 AppendToOverflowValidator(arg.size(), &for_overflow_validation);
722 if (arg.end().vars_size() > 1) {
723 return "Interval with a end expression containing more than one "
724 "variable are currently not supported.";
727 AppendToOverflowValidator(arg.end(), &for_overflow_validation, -1);
730 for_overflow_validation.coeffs(),
731 for_overflow_validation.offset())) {
732 return absl::StrCat(
"Possible overflow in interval: ",
739std::string ValidateCumulativeConstraint(
const CpModelProto& model,
741 if (ct.cumulative().intervals_size() != ct.cumulative().demands_size()) {
742 return absl::StrCat(
"intervals_size() != demands_size() in constraint: ",
753 if (MinOfExpression(model, demand_expr) < 0) {
758 if (demand_expr.vars_size() > 1) {
760 " must be affine or constant in constraint: ",
764 if (ct.cumulative().capacity().vars_size() > 1) {
770 int64_t sum_max_demands = 0;
772 const int64_t demand_max = MaxOfExpression(model, demand_expr);
773 DCHECK_GE(demand_max, 0);
774 sum_max_demands =
CapAdd(sum_max_demands, demand_max);
775 if (sum_max_demands == std::numeric_limits<int64_t>::max()) {
776 return "The sum of max demands do not fit on an int64_t in constraint: " +
784std::string ValidateNoOverlap2DConstraint(
const CpModelProto& model,
786 const int size_x = ct.no_overlap_2d().x_intervals().size();
787 const int size_y = ct.no_overlap_2d().y_intervals().size();
788 if (size_x != size_y) {
789 return absl::StrCat(
"The two lists of intervals must have the same size: ",
794 int64_t sum_max_areas = 0;
795 for (
int i = 0;
i < ct.no_overlap_2d().x_intervals().size(); ++
i) {
796 const int64_t max_size_x =
797 IntervalSizeMax(model, ct.no_overlap_2d().x_intervals(
i));
798 const int64_t max_size_y =
799 IntervalSizeMax(model, ct.no_overlap_2d().y_intervals(
i));
800 sum_max_areas =
CapAdd(sum_max_areas,
CapProd(max_size_x, max_size_y));
801 if (sum_max_areas == std::numeric_limits<int64_t>::max()) {
802 return "Integer overflow when summing all areas in "
810std::string ValidateReservoirConstraint(
const CpModelProto& model,
812 if (ct.enforcement_literal_size() > 0) {
813 return "Reservoir does not support enforcement literals.";
815 if (ct.reservoir().time_exprs().size() !=
816 ct.reservoir().level_changes().size()) {
818 "time_exprs and level_changes fields must be of the same size: ",
824 if (MinOfExpression(model, expr) <=
825 -std::numeric_limits<int64_t>::max() / 4 ||
826 MaxOfExpression(model, expr) >=
827 std::numeric_limits<int64_t>::max() / 4) {
829 "Potential integer overflow on time_expr of a reservoir: ",
836 if (ct.reservoir().min_level() > 0) {
838 "The min level of a reservoir must be <= 0. Please use fixed events to "
839 "setup initial state: ",
842 if (ct.reservoir().max_level() < 0) {
844 "The max level of a reservoir must be >= 0. Please use fixed events to "
845 "setup initial state: ",
852 const int64_t demand_min = MinOfExpression(model, demand);
853 const int64_t demand_max = MaxOfExpression(model, demand);
855 if (sum_abs == std::numeric_limits<int64_t>::max()) {
856 return "Possible integer overflow in constraint: " +
860 if (ct.reservoir().active_literals_size() > 0 &&
861 ct.reservoir().active_literals_size() !=
862 ct.reservoir().time_exprs_size()) {
863 return "Wrong array length of active_literals variables";
865 if (ct.reservoir().level_changes_size() > 0 &&
866 ct.reservoir().level_changes_size() != ct.reservoir().time_exprs_size()) {
867 return "Wrong array length of level_changes variables";
874 if (!DomainInProtoIsValid(obj)) {
875 return absl::StrCat(
"The objective has and invalid domain() format: ",
878 if (obj.vars().size() != obj.coeffs().size()) {
879 return absl::StrCat(
"vars and coeffs size do not match in objective: ",
882 for (
const int v : obj.vars()) {
883 if (!VariableIndexIsValid(model, v)) {
884 return absl::StrCat(
"Out of bound integer variable ", v,
888 std::pair<int64_t, int64_t> bounds;
890 return "Possible integer overflow in objective: " +
893 if (!std::isfinite(model.objective().offset())) {
896 if (model.objective().scaling_factor() != 0 &&
897 model.objective().scaling_factor() != 1 &&
898 model.objective().scaling_factor() != -1) {
900 std::abs(model.objective().scaling_factor() * bounds.first) +
901 std::abs(model.objective().offset())) ||
903 std::abs(model.objective().scaling_factor() * bounds.second) +
904 std::abs(model.objective().offset()))) {
905 return "Possible floating point overflow in objective when multiplied by "
906 "the scaling factor: " +
913std::string ValidateFloatingPointObjective(
double max_valid_magnitude,
916 if (obj.vars().size() != obj.coeffs().size()) {
917 return absl::StrCat(
"vars and coeffs size do not match in objective: ",
920 for (
const int v : obj.vars()) {
921 if (!VariableIndexIsValid(model, v)) {
922 return absl::StrCat(
"Out of bound integer variable ", v,
926 for (
const double coeff : obj.coeffs()) {
927 if (!std::isfinite(coeff)) {
928 return absl::StrCat(
"Coefficients must be finite in objective: ",
931 if (std::abs(coeff) > max_valid_magnitude) {
933 "Coefficients larger than params.mip_max_valid_magnitude() [value = ",
938 if (!std::isfinite(obj.offset())) {
939 return absl::StrCat(
"Offset must be finite in objective: ",
942 double sum_min = obj.offset();
943 double sum_max = obj.offset();
944 for (
int i = 0;
i < obj.vars().size(); ++
i) {
945 const int ref = obj.vars(
i);
946 const auto& var_proto = model.variables(
PositiveRef(ref));
947 const int64_t min_domain = var_proto.domain(0);
948 const int64_t max_domain = var_proto.domain(var_proto.domain_size() - 1);
949 const double coeff =
RefIsPositive(ref) ? obj.coeffs(
i) : -obj.coeffs(
i);
950 const double prod1 = min_domain * coeff;
951 const double prod2 = max_domain * coeff;
956 sum_min += std::min(0.0, std::min(prod1, prod2));
957 sum_max += std::max(0.0, std::max(prod1, prod2));
959 if (!std::isfinite(2.0 * sum_min) || !std::isfinite(2.0 * sum_max)) {
960 return absl::StrCat(
"Possible floating point overflow in objective: ",
966std::string ValidateSearchStrategies(
const CpModelProto& model) {
968 const int vss = strategy.variable_selection_strategy();
975 "Unknown or unsupported variable_selection_strategy: ", vss);
977 const int drs = strategy.domain_reduction_strategy();
984 return absl::StrCat(
"Unknown or unsupported domain_reduction_strategy: ",
987 if (!strategy.variables().empty() && !strategy.exprs().empty()) {
988 return absl::StrCat(
"Strategy can't have both variables and exprs: ",
991 for (
const int ref : strategy.variables()) {
992 if (!VariableReferenceIsValid(model, ref)) {
993 return absl::StrCat(
"Invalid variable reference in strategy: ",
999 return absl::StrCat(
"Variable #",
PositiveRef(ref),
1000 " has a domain too large to be used in a"
1001 " SELECT_MEDIAN_VALUE value selection strategy");
1005 for (
const int var : expr.vars()) {
1006 if (!VariableReferenceIsValid(model, var)) {
1007 return absl::StrCat(
"Invalid variable reference in strategy: ",
1011 if (!ValidateAffineExpression(model, expr).empty()) {
1012 return absl::StrCat(
"Invalid affine expr in strategy: ",
1016 for (
const int var : expr.vars()) {
1018 return absl::StrCat(
1020 " has a domain too large to be used in a"
1021 " SELECT_MEDIAN_VALUE value selection strategy");
1030std::string ValidateSolutionHint(
const CpModelProto& model) {
1031 if (!model.has_solution_hint())
return "";
1032 const auto& hint = model.solution_hint();
1033 if (hint.vars().size() != hint.values().size()) {
1034 return "Invalid solution hint: vars and values do not have the same size.";
1036 for (
const int var : hint.vars()) {
1037 if (!VariableIndexIsValid(model, var)) {
1038 return absl::StrCat(
"Invalid variable in solution hint: ", var);
1043 absl::flat_hash_set<int> indices;
1044 for (
const int var : hint.vars()) {
1045 const auto insert = indices.insert(
PositiveRef(var));
1046 if (!insert.second) {
1047 return absl::StrCat(
1048 "The solution hint contains duplicate variables like the variable "
1055 for (
const int64_t value : hint.values()) {
1056 if (value == std::numeric_limits<int64_t>::min() ||
1057 value == std::numeric_limits<int64_t>::max()) {
1058 return "The solution hint cannot contains the INT_MIN or INT_MAX values.";
1068 absl::Span<const int> vars,
1069 absl::Span<const int64_t> coeffs, int64_t offset,
1070 std::pair<int64_t, int64_t>* implied_domain) {
1071 if (offset == std::numeric_limits<int64_t>::min())
return true;
1072 int64_t sum_min = -std::abs(offset);
1073 int64_t sum_max = +std::abs(offset);
1074 for (
int i = 0;
i < vars.size(); ++
i) {
1075 const int ref = vars[
i];
1076 const auto& var_proto = model.variables(
PositiveRef(ref));
1077 const int64_t min_domain = var_proto.domain(0);
1078 const int64_t max_domain = var_proto.domain(var_proto.domain_size() - 1);
1079 if (coeffs[
i] == std::numeric_limits<int64_t>::min())
return true;
1081 const int64_t prod1 =
CapProd(min_domain, coeff);
1082 const int64_t prod2 =
CapProd(max_domain, coeff);
1087 sum_min =
CapAdd(sum_min, std::min(int64_t{0}, std::min(prod1, prod2)));
1088 sum_max =
CapAdd(sum_max, std::max(int64_t{0}, std::max(prod1, prod2)));
1089 for (
const int64_t v : {prod1, prod2, sum_min, sum_max}) {
1100 if (sum_min < -std::numeric_limits<int64_t>::max() / 2)
return true;
1101 if (sum_max > std::numeric_limits<int64_t>::max() / 2)
return true;
1102 if (implied_domain) {
1103 *implied_domain = {sum_min, sum_max};
1108std::string
ValidateCpModel(
const CpModelProto& model,
bool after_presolve) {
1109 int64_t int128_overflow = 0;
1110 for (
int v = 0; v < model.variables_size(); ++v) {
1113 const auto& domain = model.variables(v).domain();
1114 const int64_t min = domain[0];
1115 const int64_t max = domain[domain.size() - 1];
1116 int128_overflow =
CapAdd(
1117 int128_overflow, std::max({std::abs(min), std::abs(max), max - min}));
1123 if (int128_overflow == std::numeric_limits<int64_t>::max()) {
1124 return "The sum of all variable domains do not fit on an int64_t. This is "
1125 "needed to prevent overflows.";
1130 std::vector<int> constraints_using_intervals;
1132 for (
int c = 0; c < model.constraints_size(); ++c) {
1137 bool support_enforcement =
false;
1140 const ConstraintProto& ct = model.constraints(c);
1141 switch (ct.constraint_case()) {
1143 support_enforcement =
true;
1146 support_enforcement =
true;
1149 support_enforcement =
true;
1154 ValidateLinearExpression(model, ct.lin_max().target()));
1155 for (
const LinearExpressionProto& expr : ct.lin_max().exprs()) {
1170 if (ct.inverse().f_direct().size() != ct.inverse().f_inverse().size()) {
1171 return absl::StrCat(
"Non-matching fields size in inverse: ",
1185 support_enforcement =
true;
1192 ValidateGraphInput(
false, ct.circuit()));
1199 support_enforcement =
true;
1202 constraints_using_intervals.push_back(c);
1205 constraints_using_intervals.push_back(c);
1208 constraints_using_intervals.push_back(c);
1214 return "The dummy constraint should never appear in a model.";
1222 if (!support_enforcement && !ct.enforcement_literal().empty()) {
1223 for (
const int ref : ct.enforcement_literal()) {
1226 if (domain.Size() != 1) {
1227 return absl::StrCat(
1228 "Enforcement literal not supported in constraint: ",
1236 for (
const int c : constraints_using_intervals) {
1238 ValidateIntervalsUsedInConstraint(after_presolve, model, c));
1241 switch (ct.constraint_case()) {
1251 LOG(DFATAL) <<
"Shouldn't be here";
1255 if (model.has_objective() && model.has_floating_point_objective()) {
1256 return "A model cannot have both an objective and a floating point "
1259 if (model.has_objective()) {
1260 if (model.objective().scaling_factor() != 0 &&
1261 !std::isnormal(model.objective().scaling_factor())) {
1262 return "A model cannot have an objective with a nan, inf or subnormal "
1268 if (model.objective().integer_scaling_factor() != 0 ||
1269 model.objective().integer_before_offset() != 0 ||
1270 model.objective().integer_after_offset() != 0) {
1272 if (model.objective().domain().empty()) {
1273 return absl::StrCat(
1274 "Objective integer scaling or offset is set without an objective "
1280 bool overflow =
false;
1281 for (
const int64_t v : model.objective().domain()) {
1282 int64_t t =
CapAdd(v, model.objective().integer_before_offset());
1287 t =
CapProd(t, model.objective().integer_scaling_factor());
1292 t =
CapAdd(t, model.objective().integer_after_offset());
1299 return absl::StrCat(
1300 "Internal fields related to the postsolve of the integer objective "
1301 "are causing a potential integer overflow: ",
1308 for (
const int ref : model.assumptions()) {
1309 if (!LiteralReferenceIsValid(model, ref)) {
1310 return absl::StrCat(
"Invalid literal reference ", ref,
1311 " in the 'assumptions' field.");
1320 if (model.has_floating_point_objective()) {
1322 ValidateFloatingPointObjective(params.mip_max_valid_magnitude(), model,
1323 model.floating_point_objective()));
1328#undef RETURN_IF_NOT_EMPTY
1336class ConstraintChecker {
1338 explicit ConstraintChecker(absl::Span<const int64_t> variable_values)
1339 : variable_values_(variable_values.
begin(), variable_values.
end()) {}
1341 bool LiteralIsTrue(
int l)
const {
1342 if (l >= 0)
return variable_values_[l] != 0;
1343 return variable_values_[-l - 1] == 0;
1346 bool LiteralIsFalse(
int l)
const {
return !LiteralIsTrue(l); }
1348 int64_t
Value(
int var)
const {
1349 if (var >= 0)
return variable_values_[var];
1350 return -variable_values_[-var - 1];
1353 bool ConstraintIsEnforced(
const ConstraintProto& ct) {
1354 for (
const int lit : ct.enforcement_literal()) {
1355 if (LiteralIsFalse(lit))
return false;
1360 bool BoolOrConstraintIsFeasible(
const ConstraintProto& ct) {
1361 for (
const int lit : ct.bool_or().literals()) {
1362 if (LiteralIsTrue(lit))
return true;
1367 bool BoolAndConstraintIsFeasible(
const ConstraintProto& ct) {
1368 for (
const int lit : ct.bool_and().literals()) {
1369 if (LiteralIsFalse(lit))
return false;
1374 bool AtMostOneConstraintIsFeasible(
const ConstraintProto& ct) {
1375 int num_true_literals = 0;
1376 for (
const int lit : ct.at_most_one().literals()) {
1377 if (LiteralIsTrue(lit)) ++num_true_literals;
1379 return num_true_literals <= 1;
1382 bool ExactlyOneConstraintIsFeasible(
const ConstraintProto& ct) {
1383 int num_true_literals = 0;
1384 for (
const int lit : ct.exactly_one().literals()) {
1385 if (LiteralIsTrue(lit)) ++num_true_literals;
1387 return num_true_literals == 1;
1390 bool BoolXorConstraintIsFeasible(
const ConstraintProto& ct) {
1392 for (
const int lit : ct.bool_xor().literals()) {
1393 sum ^= LiteralIsTrue(lit) ? 1 : 0;
1398 bool LinearConstraintIsFeasible(
const ConstraintProto& ct) {
1400 const int num_variables = ct.linear().coeffs_size();
1401 const int*
const vars = ct.linear().vars().data();
1402 const int64_t*
const coeffs = ct.linear().coeffs().data();
1403 for (
int i = 0;
i < num_variables; ++
i) {
1406 sum += variable_values_[vars[
i]] * coeffs[
i];
1410 VLOG(1) <<
"Activity: " << sum;
1415 int64_t LinearExpressionValue(
const LinearExpressionProto& expr)
const {
1416 int64_t sum = expr.offset();
1417 const int num_variables = expr.vars_size();
1418 for (
int i = 0;
i < num_variables; ++
i) {
1419 sum +=
Value(expr.vars(
i)) * expr.coeffs(
i);
1424 bool LinMaxConstraintIsFeasible(
const ConstraintProto& ct) {
1425 const int64_t max = LinearExpressionValue(ct.lin_max().target());
1426 int64_t actual_max = std::numeric_limits<int64_t>::min();
1427 for (
int i = 0;
i < ct.lin_max().exprs_size(); ++
i) {
1428 const int64_t expr_value = LinearExpressionValue(ct.lin_max().exprs(
i));
1429 actual_max = std::max(actual_max, expr_value);
1431 return max == actual_max;
1434 bool IntProdConstraintIsFeasible(
const ConstraintProto& ct) {
1435 const int64_t prod = LinearExpressionValue(ct.int_prod().target());
1436 int64_t actual_prod = 1;
1437 for (
const LinearExpressionProto& expr : ct.int_prod().exprs()) {
1438 actual_prod =
CapProd(actual_prod, LinearExpressionValue(expr));
1440 return prod == actual_prod;
1443 bool IntDivConstraintIsFeasible(
const ConstraintProto& ct) {
1444 return LinearExpressionValue(ct.int_div().target()) ==
1445 LinearExpressionValue(ct.int_div().exprs(0)) /
1446 LinearExpressionValue(ct.int_div().exprs(1));
1449 bool IntModConstraintIsFeasible(
const ConstraintProto& ct) {
1450 return LinearExpressionValue(ct.int_mod().target()) ==
1451 LinearExpressionValue(ct.int_mod().exprs(0)) %
1452 LinearExpressionValue(ct.int_mod().exprs(1));
1455 bool AllDiffConstraintIsFeasible(
const ConstraintProto& ct) {
1456 absl::flat_hash_set<int64_t> values;
1457 for (
const LinearExpressionProto& expr : ct.all_diff().exprs()) {
1458 const int64_t value = LinearExpressionValue(expr);
1459 const auto [it, inserted] = values.insert(value);
1460 if (!inserted)
return false;
1465 int64_t IntervalStart(
const IntervalConstraintProto& interval)
const {
1466 return LinearExpressionValue(interval.start());
1469 int64_t IntervalSize(
const IntervalConstraintProto& interval)
const {
1470 return LinearExpressionValue(interval.size());
1473 int64_t IntervalEnd(
const IntervalConstraintProto& interval)
const {
1474 return LinearExpressionValue(interval.end());
1477 bool IntervalConstraintIsFeasible(
const ConstraintProto& ct) {
1478 const int64_t size = IntervalSize(ct.interval());
1479 if (size < 0)
return false;
1480 return IntervalStart(ct.interval()) + size == IntervalEnd(ct.interval());
1483 bool NoOverlapConstraintIsFeasible(
const CpModelProto& model,
1484 const ConstraintProto& ct) {
1485 std::vector<std::pair<int64_t, int64_t>> start_durations_pairs;
1486 for (
const int i : ct.no_overlap().intervals()) {
1487 const ConstraintProto& interval_constraint = model.constraints(
i);
1488 if (ConstraintIsEnforced(interval_constraint)) {
1489 const IntervalConstraintProto& interval =
1490 interval_constraint.interval();
1491 start_durations_pairs.push_back(
1492 {IntervalStart(interval), IntervalSize(interval)});
1495 std::sort(start_durations_pairs.begin(), start_durations_pairs.end());
1496 int64_t previous_end = std::numeric_limits<int64_t>::min();
1497 for (
const auto& pair : start_durations_pairs) {
1498 if (pair.first < previous_end)
return false;
1499 previous_end = pair.first + pair.second;
1504 bool NoOverlap2DConstraintIsFeasible(
const CpModelProto& model,
1505 const ConstraintProto& ct) {
1506 const auto& arg = ct.no_overlap_2d();
1509 bool has_zero_sizes =
false;
1510 std::vector<Rectangle> enforced_rectangles;
1512 const int num_intervals = arg.x_intervals_size();
1513 CHECK_EQ(arg.y_intervals_size(), num_intervals);
1514 for (
int i = 0;
i < num_intervals; ++
i) {
1515 const ConstraintProto&
x = model.constraints(arg.x_intervals(
i));
1516 const ConstraintProto& y = model.constraints(arg.y_intervals(
i));
1517 if (ConstraintIsEnforced(x) && ConstraintIsEnforced(y)) {
1518 enforced_rectangles.push_back({.x_min = IntervalStart(
x.interval()),
1519 .x_max = IntervalEnd(
x.interval()),
1520 .y_min = IntervalStart(y.interval()),
1521 .y_max = IntervalEnd(y.interval())});
1522 const auto& rect = enforced_rectangles.back();
1523 if (rect.x_min == rect.x_max || rect.y_min == rect.y_max) {
1524 has_zero_sizes =
true;
1530 std::optional<std::pair<int, int>> one_intersection;
1531 absl::c_stable_sort(enforced_rectangles,
1532 [](
const Rectangle& a,
const Rectangle&
b) {
1533 return a.x_min <
b.x_min;
1535 if (has_zero_sizes) {
1542 if (one_intersection != std::nullopt) {
1543 VLOG(1) <<
"Rectangles " << one_intersection->first <<
"("
1544 << enforced_rectangles[one_intersection->first] <<
") and "
1545 << one_intersection->second <<
"("
1546 << enforced_rectangles[one_intersection->second]
1547 <<
") are not disjoint.";
1553 bool CumulativeConstraintIsFeasible(
const CpModelProto& model,
1554 const ConstraintProto& ct) {
1555 const int64_t capacity = LinearExpressionValue(ct.cumulative().capacity());
1556 if (capacity < 0)
return false;
1557 const int num_intervals = ct.cumulative().intervals_size();
1558 std::vector<std::pair<int64_t, int64_t>> events;
1559 for (
int i = 0;
i < num_intervals; ++
i) {
1560 const ConstraintProto& interval_constraint =
1561 model.constraints(ct.cumulative().intervals(
i));
1562 if (!ConstraintIsEnforced(interval_constraint))
continue;
1563 const int64_t start = IntervalStart(interval_constraint.interval());
1564 const int64_t duration = IntervalSize(interval_constraint.interval());
1565 const int64_t demand = LinearExpressionValue(ct.cumulative().demands(
i));
1566 if (duration == 0 || demand == 0)
continue;
1567 events.emplace_back(start, demand);
1568 events.emplace_back(start + duration, -demand);
1570 if (events.empty())
return true;
1572 std::sort(events.begin(), events.end());
1575 int64_t current_load = 0;
1576 for (
const auto& [time, delta] : events) {
1577 current_load += delta;
1578 if (current_load > capacity) {
1579 VLOG(1) <<
"Cumulative constraint: load: " << current_load
1580 <<
" capacity: " << capacity <<
" time: " << time;
1584 DCHECK_EQ(current_load, 0);
1588 bool ElementConstraintIsFeasible(
const ConstraintProto& ct) {
1589 if (!ct.element().vars().empty()) {
1590 const int index =
Value(ct.element().index());
1591 if (index < 0 || index >= ct.element().vars_size())
return false;
1592 return Value(ct.element().vars(index)) ==
Value(ct.element().target());
1595 if (!ct.element().exprs().empty()) {
1596 const int index = LinearExpressionValue(ct.element().linear_index());
1597 if (index < 0 || index >= ct.element().exprs_size())
return false;
1598 return LinearExpressionValue(ct.element().exprs(index)) ==
1599 LinearExpressionValue(ct.element().linear_target());
1605 bool TableConstraintIsFeasible(
const ConstraintProto& ct) {
1607 if (ct.table().exprs().empty()) {
1608 for (
int i = 0;
i < ct.table().vars_size(); ++
i) {
1612 for (
int i = 0;
i < ct.table().exprs_size(); ++
i) {
1613 solution.push_back(LinearExpressionValue(ct.table().exprs(
i)));
1621 for (
int row_start = 0; row_start < ct.table().values_size();
1622 row_start += size) {
1624 while (
solution[
i] == ct.table().values(row_start +
i)) {
1626 if (
i == size)
return !ct.table().negated();
1629 return ct.table().negated();
1632 bool AutomatonConstraintIsFeasible(
const ConstraintProto& ct) {
1634 const AutomatonConstraintProto& automaton = ct.automaton();
1635 absl::flat_hash_map<std::pair<int64_t, int64_t>, int64_t> transition_map;
1636 const int num_transitions = automaton.transition_tail().size();
1637 for (
int i = 0;
i < num_transitions; ++
i) {
1638 transition_map[{automaton.transition_tail(
i),
1639 automaton.transition_label(
i)}] =
1640 automaton.transition_head(
i);
1644 int64_t current_state = automaton.starting_state();
1645 const int num_steps =
1646 std::max(automaton.vars_size(), automaton.exprs_size());
1647 for (
int i = 0;
i < num_steps; ++
i) {
1648 const std::pair<int64_t, int64_t> key = {
1649 current_state, automaton.vars().empty()
1650 ? LinearExpressionValue(automaton.exprs(
i))
1651 :
Value(automaton.vars(
i))};
1652 if (!transition_map.contains(key)) {
1655 current_state = transition_map[key];
1659 for (
const int64_t
final : automaton.final_states()) {
1660 if (current_state ==
final)
return true;
1665 bool CircuitConstraintIsFeasible(
const ConstraintProto& ct) {
1668 const int num_arcs = ct.circuit().tails_size();
1669 absl::flat_hash_set<int> nodes;
1670 absl::flat_hash_map<int, int> nexts;
1671 for (
int i = 0;
i < num_arcs; ++
i) {
1672 const int tail = ct.circuit().tails(
i);
1673 const int head = ct.circuit().heads(
i);
1676 if (LiteralIsFalse(ct.circuit().literals(
i)))
continue;
1677 if (nexts.contains(tail)) {
1678 VLOG(1) <<
"Node with two outgoing arcs";
1687 for (
const int node : nodes) {
1688 if (!nexts.contains(node)) {
1689 VLOG(1) <<
"Node with no next: " << node;
1692 if (nexts[node] == node)
continue;
1696 if (cycle_size == 0)
return true;
1700 absl::flat_hash_set<int> visited;
1701 int current = in_cycle;
1702 int num_visited = 0;
1703 while (!visited.contains(current)) {
1705 visited.insert(current);
1706 current = nexts[current];
1708 if (current != in_cycle) {
1709 VLOG(1) <<
"Rho shape";
1712 if (num_visited != cycle_size) {
1713 VLOG(1) <<
"More than one cycle";
1715 return num_visited == cycle_size;
1718 bool RoutesConstraintIsFeasible(
const ConstraintProto& ct) {
1719 const int num_arcs = ct.routes().tails_size();
1720 int num_used_arcs = 0;
1721 int num_self_arcs = 0;
1725 for (
int i = 0;
i < num_arcs; ++
i) {
1726 num_nodes = std::max(num_nodes, 1 + ct.routes().tails(
i));
1727 num_nodes = std::max(num_nodes, 1 + ct.routes().heads(
i));
1730 std::vector<int> tail_to_head(num_nodes, -1);
1731 std::vector<bool> has_incoming_arc(num_nodes,
false);
1732 std::vector<int> has_outgoing_arc(num_nodes,
false);
1733 std::vector<int> depot_nexts;
1734 for (
int i = 0;
i < num_arcs; ++
i) {
1735 const int tail = ct.routes().tails(
i);
1736 const int head = ct.routes().heads(
i);
1737 if (LiteralIsTrue(ct.routes().literals(
i))) {
1740 if (has_outgoing_arc[tail]) {
1741 VLOG(1) <<
"routes: node " << tail <<
"has two outgoing arcs";
1744 has_outgoing_arc[tail] =
true;
1747 if (has_incoming_arc[head]) {
1748 VLOG(1) <<
"routes: node " << head <<
"has two incoming arcs";
1751 has_incoming_arc[head] =
true;
1756 VLOG(1) <<
"Self loop on node 0 are forbidden.";
1764 depot_nexts.push_back(head);
1766 DCHECK_EQ(tail_to_head[tail], -1);
1767 tail_to_head[tail] = head;
1773 if (num_nodes == 0)
return true;
1777 for (
int start : depot_nexts) {
1779 while (start != 0) {
1780 if (tail_to_head[start] == -1)
return false;
1781 start = tail_to_head[start];
1786 if (count != num_used_arcs) {
1787 VLOG(1) <<
"count: " << count <<
" != num_used_arcs:" << num_used_arcs;
1795 if (count - depot_nexts.size() + 1 + num_self_arcs != num_nodes) {
1796 VLOG(1) <<
"Not all nodes are covered!";
1803 bool InverseConstraintIsFeasible(
const ConstraintProto& ct) {
1804 const int num_variables = ct.inverse().f_direct_size();
1805 if (num_variables != ct.inverse().f_inverse_size())
return false;
1807 for (
int i = 0;
i < num_variables;
i++) {
1808 const int fi =
Value(ct.inverse().f_direct(
i));
1809 if (fi < 0 || num_variables <= fi)
return false;
1810 if (
i !=
Value(ct.inverse().f_inverse(fi)))
return false;
1815 bool ReservoirConstraintIsFeasible(
const ConstraintProto& ct) {
1816 const int num_variables = ct.reservoir().time_exprs_size();
1817 const int64_t min_level = ct.reservoir().min_level();
1818 const int64_t max_level = ct.reservoir().max_level();
1819 absl::btree_map<int64_t, int64_t> deltas;
1820 const bool has_active_variables = ct.reservoir().active_literals_size() > 0;
1821 for (
int i = 0;
i < num_variables;
i++) {
1822 const int64_t time = LinearExpressionValue(ct.reservoir().time_exprs(
i));
1823 if (!has_active_variables ||
1824 Value(ct.reservoir().active_literals(
i)) == 1) {
1825 const int64_t level =
1826 LinearExpressionValue(ct.reservoir().level_changes(
i));
1827 deltas[time] += level;
1830 int64_t current_level = 0;
1831 for (
const auto& delta : deltas) {
1832 current_level += delta.second;
1833 if (current_level < min_level || current_level > max_level) {
1834 VLOG(1) <<
"Reservoir level " << current_level
1835 <<
" is out of bounds at time: " << delta.first;
1843 const ConstraintProto& ct) {
1845 if (!ConstraintIsEnforced(ct))
return true;
1850 return BoolOrConstraintIsFeasible(ct);
1852 return BoolAndConstraintIsFeasible(ct);
1854 return AtMostOneConstraintIsFeasible(ct);
1856 return ExactlyOneConstraintIsFeasible(ct);
1858 return BoolXorConstraintIsFeasible(ct);
1860 return LinearConstraintIsFeasible(ct);
1862 return IntProdConstraintIsFeasible(ct);
1864 return IntDivConstraintIsFeasible(ct);
1866 return IntModConstraintIsFeasible(ct);
1868 return LinMaxConstraintIsFeasible(ct);
1870 return AllDiffConstraintIsFeasible(ct);
1872 if (!IntervalConstraintIsFeasible(ct)) {
1873 if (ct.interval().has_start()) {
1879 VLOG(1) <<
"Warning, an interval constraint was likely used "
1880 "without a corresponding linear constraint linking "
1881 "its start, size and end.";
1887 return NoOverlapConstraintIsFeasible(model, ct);
1889 return NoOverlap2DConstraintIsFeasible(model, ct);
1891 return CumulativeConstraintIsFeasible(model, ct);
1893 return ElementConstraintIsFeasible(ct);
1895 return TableConstraintIsFeasible(ct);
1897 return AutomatonConstraintIsFeasible(ct);
1899 return CircuitConstraintIsFeasible(ct);
1901 return RoutesConstraintIsFeasible(ct);
1903 return InverseConstraintIsFeasible(ct);
1905 return ReservoirConstraintIsFeasible(ct);
1916 const std::vector<int64_t> variable_values_;
1923 absl::Span<const int64_t> variable_values) {
1924 ConstraintChecker checker(variable_values);
1925 return checker.ConstraintIsFeasible(model, constraint);
1929 absl::Span<const int64_t> variable_values,
1930 const CpModelProto* mapping_proto,
1931 const std::vector<int>* postsolve_mapping) {
1932 if (variable_values.size() != model.variables_size()) {
1933 VLOG(1) <<
"Wrong number of variables (" << variable_values.size()
1934 <<
") in the solution vector. It should be "
1935 << model.variables_size() <<
".";
1940 for (
int i = 0;
i < model.variables_size(); ++
i) {
1942 VLOG(1) <<
"Variable #" <<
i <<
" has value " << variable_values[
i]
1943 <<
" which do not fall in its domain: "
1949 CHECK_EQ(variable_values.size(), model.variables_size());
1950 ConstraintChecker checker(variable_values);
1952 for (
int c = 0;
c < model.constraints_size(); ++
c) {
1954 if (checker.ConstraintIsFeasible(model, ct))
continue;
1957 VLOG(1) <<
"Failing constraint #" <<
c <<
" : "
1959 if (mapping_proto !=
nullptr && postsolve_mapping !=
nullptr) {
1960 std::vector<int> reverse_map(mapping_proto->variables().size(), -1);
1961 for (
int var = 0; var < postsolve_mapping->size(); ++var) {
1962 reverse_map[(*postsolve_mapping)[var]] = var;
1965 VLOG(1) <<
"var: " << var <<
" mapped_to: " << reverse_map[var]
1966 <<
" value: " << variable_values[var] <<
" initial_domain: "
1968 <<
" postsolved_domain: "
1973 VLOG(1) <<
"var: " << var <<
" value: " << variable_values[var];
1984 if (model.has_objective()) {
1985 int64_t inner_objective = 0;
1986 const int num_variables = model.objective().coeffs_size();
1987 for (
int i = 0;
i < num_variables; ++
i) {
1988 inner_objective += checker.Value(model.objective().vars(
i)) *
1989 model.objective().coeffs(
i);
1991 if (!model.objective().domain().empty()) {
1993 VLOG(1) <<
"Objective value " << inner_objective <<
" not in domain! "
1998 double factor = model.objective().scaling_factor();
1999 if (factor == 0.0) factor = 1.0;
2000 const double scaled_objective =
2002 (
static_cast<double>(inner_objective) + model.objective().offset());
2003 VLOG(2) <<
"Checker inner objective = " << inner_objective;
2004 VLOG(2) <<
"Checker scaled objective = " << scaled_objective;
2011 absl::Span<const int64_t> variable_values) {
2012 if (absl::GetFlag(FLAGS_cp_model_check_dependent_variables)) {
2015 std::vector<int64_t> all_variables(variable_values.begin(),
2016 variable_values.end());
2017 for (
const int var : relationships.secondary_variables) {
2018 all_variables[var] = -999999;
2022 CHECK(absl::MakeSpan(all_variables) == variable_values);
::int64_t transition_tail(int index) const
static constexpr DomainReductionStrategy SELECT_MAX_VALUE
static constexpr DomainReductionStrategy SELECT_MIN_VALUE
static constexpr VariableSelectionStrategy CHOOSE_HIGHEST_MAX
static constexpr VariableSelectionStrategy CHOOSE_FIRST
static constexpr DomainReductionStrategy SELECT_MEDIAN_VALUE
static constexpr DomainReductionStrategy SELECT_UPPER_HALF
static constexpr VariableSelectionStrategy CHOOSE_LOWEST_MIN
static constexpr VariableSelectionStrategy CHOOSE_MAX_DOMAIN_SIZE
static constexpr VariableSelectionStrategy CHOOSE_MIN_DOMAIN_SIZE
static constexpr DomainReductionStrategy SELECT_LOWER_HALF
static constexpr DomainReductionStrategy SELECT_RANDOM_HALF
bool has_linear_index() const
.operations_research.sat.LinearExpressionProto linear_index = 4;
::int64_t domain(int index) const
void add_vars(::int32_t value)
RoutesConstraintProto_NodeExpressions NodeExpressions
nested types -------------------------------------------------—
::int32_t vars(int index) const
#define RETURN_IF_NOT_EMPTY(statement)
If the string returned by "statement" is not empty, returns it.
ABSL_FLAG(bool, cp_model_check_dependent_variables, false, "When true, check that solutions can be computed only from their " "free variables.")
absl::Status ValidateLinearExpression(const LinearExpressionProto &expression, const IdNameBiMap &variable_universe)
std::string ValidateInputCpModel(const SatParameters ¶ms, const CpModelProto &model)
bool RefIsPositive(int ref)
std::string ValidateCpModel(const CpModelProto &model, bool after_presolve)
bool SolutionIsFeasible(const CpModelProto &model, absl::Span< const int64_t > variable_values, const CpModelProto *mapping_proto, const std::vector< int > *postsolve_mapping)
bool SolutionCanBeOptimal(const CpModelProto &model, absl::Span< const int64_t > variable_values)
Verifies some invariants that any optimal solution must satisfy.
bool ConstraintIsFeasible(const CpModelProto &model, const ConstraintProto &constraint, absl::Span< const int64_t > variable_values)
bool DomainInProtoContains(const ProtoWithDomain &proto, int64_t value)
std::optional< std::pair< int, int > > FindOneIntersectionIfPresent(absl::Span< const Rectangle > rectangles)
bool PossibleIntegerOverflow(const CpModelProto &model, absl::Span< const int > vars, absl::Span< const int64_t > coeffs, int64_t offset, std::pair< int64_t, int64_t > *implied_domain)
std::vector< int > UsedVariables(const ConstraintProto &ct)
std::vector< int > UsedIntervals(const ConstraintProto &ct)
Returns the sorted list of interval used by a constraint.
std::function< int64_t(const Model &)> Value(IntegerVariable v)
This checks that the variable is fixed.
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
absl::string_view ConstraintCaseName(ConstraintProto::ConstraintCase constraint_case)
std::optional< std::pair< int, int > > FindOneIntersectionIfPresentWithZeroArea(absl::Span< const Rectangle > rectangles)
bool ComputeAllVariablesFromPrimaryVariables(const CpModelProto &model, const VariableRelationships &relationships, std::vector< int64_t > *solution)
IndexReferences GetReferencesUsedByConstraint(const ConstraintProto &ct)
VariableRelationships ComputeVariableRelationships(const CpModelProto &model)
In SWIG mode, we don't want anything besides these top-level includes.
bool AtMinOrMaxInt64(int64_t x)
Checks if x is equal to the min or the max value of an int64_t.
int64_t CapAdd(int64_t x, int64_t y)
Select next search node to expand Select next item_i to add this new search node to the search Generate a new search node where item_i is not in the knapsack Check validity of this new partial solution(using propagators) - If valid
int64_t CapSub(int64_t x, int64_t y)
ClosedInterval::Iterator end(ClosedInterval interval)
std::string ProtobufShortDebugString(const P &message)
int64_t CapProd(int64_t x, int64_t y)
int64_t CapAbs(int64_t v)
bool IntervalsAreSortedAndNonAdjacent(absl::Span< const ClosedInterval > intervals)
std::string ProtobufDebugString(const P &message)
ClosedInterval::Iterator begin(ClosedInterval interval)
static int input(yyscan_t yyscanner)