19 #include "absl/strings/match.h"
20 #include "absl/strings/str_format.h"
21 #include "absl/strings/str_join.h"
22 #include "absl/strings/string_view.h"
31 "Interpret floats as integers in all variables and constraints.");
36 enum PresolveState { ALWAYS_FALSE, ALWAYS_TRUE, UNDECIDED };
39 bool Has01Values(IntegerVariable*
var) {
40 return var->domain.Min() == 0 &&
var->domain.Max() == 1;
47 for (
int i = 0; i < values.size(); ++i) {
48 if (values[i] != 0 && values[i] != 1) {
56 bool AtMostOne0OrAtMostOne1(
const std::vector<T>& values) {
60 for (T val : values) {
66 if (num_one > 1 && num_zero > 1) {
73 absl::flat_hash_set<int64> GetValueSet(
const Argument& arg) {
74 absl::flat_hash_set<int64> result;
75 if (arg.HasOneValue()) {
76 result.insert(arg.Value());
78 const Domain& domain = arg.Var()->domain;
79 if (domain.is_interval && !domain.values.empty()) {
80 for (
int64 v = domain.values[0]; v <= domain.values[1]; ++v) {
84 result.insert(domain.values.begin(), domain.values.end());
90 void SetConstraintAsIntEq(Constraint*
ct, IntegerVariable*
var,
int64 value) {
98 bool OverlapsAt(
const Argument& array,
int pos,
const Argument& other) {
100 const Domain& domain = array.variables[pos]->domain;
101 if (domain.IsAllInt64()) {
104 switch (other.type) {
106 return domain.Contains(other.Value());
109 return domain.OverlapsIntInterval(other.values[0], other.values[1]);
112 return domain.OverlapsIntList(other.values);
115 return domain.OverlapsDomain(other.variables[0]->domain);
118 LOG(
FATAL) <<
"Case not supported in OverlapsAt";
124 switch (other.type) {
126 return value == other.values[0];
129 return other.values[0] <=
value &&
value <= other.values[1];
132 return std::find(other.values.begin(), other.values.end(),
value) !=
136 return other.variables[0]->domain.Contains(
value);
139 LOG(
FATAL) <<
"Case not supported in OverlapsAt";
144 LOG(
FATAL) <<
"First argument not supported in OverlapsAt";
150 void AppendIfNotInSet(T*
value, absl::flat_hash_set<T*>* s,
151 std::vector<T*>* vec) {
152 if (s->insert(
value).second) {
153 vec->push_back(
value);
180 void Presolver::PresolveBool2Int(Constraint*
ct) {
182 if (
ct->arguments[0].HasOneValue() ||
ct->arguments[1].HasOneValue()) {
184 UpdateRuleStats(
"bool2int: rename to int_eq");
188 UpdateRuleStats(
"bool2int: merge boolean and integer variables.");
189 AddVariableSubstitution(
ct->arguments[1].Var(),
ct->arguments[0].Var());
190 ct->MarkAsInactive();
199 void Presolver::PresolveStoreAffineMapping(Constraint*
ct) {
200 CHECK_EQ(2,
ct->arguments[1].variables.size());
201 IntegerVariable*
const var0 =
ct->arguments[1].variables[0];
202 IntegerVariable*
const var1 =
ct->arguments[1].variables[1];
203 const int64 coeff0 =
ct->arguments[0].values[0];
204 const int64 coeff1 =
ct->arguments[0].values[1];
205 const int64 rhs =
ct->arguments[2].Value();
207 affine_map_[var0] = AffineMapping(var1, coeff0, -rhs,
ct);
208 UpdateRuleStats(
"int_lin_eq: store affine mapping");
210 affine_map_[var1] = AffineMapping(var0, coeff0, -rhs,
ct);
211 UpdateRuleStats(
"int_lin_eq: store affine mapping");
215 void Presolver::PresolveStoreFlatteningMapping(Constraint*
ct) {
216 CHECK_EQ(3,
ct->arguments[1].variables.size());
217 IntegerVariable*
const var0 =
ct->arguments[1].variables[0];
218 IntegerVariable*
const var1 =
ct->arguments[1].variables[1];
219 IntegerVariable*
const var2 =
ct->arguments[1].variables[2];
220 const int64 coeff0 =
ct->arguments[0].values[0];
221 const int64 coeff1 =
ct->arguments[0].values[1];
222 const int64 coeff2 =
ct->arguments[0].values[2];
223 const int64 rhs =
ct->arguments[2].Value();
224 if (coeff0 == -1 && coeff2 == 1 &&
226 array2d_index_map_[var0] =
227 Array2DIndexMapping(var1, coeff1, var2, -rhs,
ct);
228 UpdateRuleStats(
"int_lin_eq: store 2d flattening mapping");
229 }
else if (coeff0 == -1 && coeff1 == 1 &&
231 array2d_index_map_[var0] =
232 Array2DIndexMapping(var2, coeff2, var1, -rhs,
ct);
233 UpdateRuleStats(
"int_lin_eq: store 2d flattening mapping");
234 }
else if (coeff2 == -1 && coeff1 == 1 &&
236 array2d_index_map_[var2] =
237 Array2DIndexMapping(var0, coeff0, var1, -rhs,
ct);
238 UpdateRuleStats(
"int_lin_eq: store 2d flattening mapping");
239 }
else if (coeff2 == -1 && coeff0 == 1 &&
241 array2d_index_map_[var2] =
242 Array2DIndexMapping(var1, coeff1, var0, -rhs,
ct);
243 UpdateRuleStats(
"int_lin_eq: store 2d flattening mapping");
248 bool IsIncreasingAndContiguous(
const std::vector<int64>& values) {
249 for (
int i = 0; i < values.size() - 1; ++i) {
250 if (values[i + 1] != values[i] + 1) {
257 bool AreOnesFollowedByMinusOne(
const std::vector<int64>& coeffs) {
258 CHECK(!coeffs.empty());
259 for (
int i = 0; i < coeffs.size() - 1; ++i) {
260 if (coeffs[i] != 1) {
264 return coeffs.back() == -1;
268 bool IsStrictPrefix(
const std::vector<T>& v1,
const std::vector<T>& v2) {
269 if (v1.size() >= v2.size()) {
272 for (
int i = 0; i < v1.size(); ++i) {
273 if (v1[i] != v2[i]) {
299 void Presolver::PresolveSimplifyElement(Constraint*
ct) {
300 if (
ct->arguments[0].variables.size() != 1)
return;
301 IntegerVariable*
const index_var =
ct->arguments[0].Var();
305 const AffineMapping& mapping = affine_map_[index_var];
306 const Domain& domain = mapping.variable->domain;
307 if (domain.is_interval && domain.values.empty()) {
311 if (domain.values[0] == 0 && mapping.coefficient == 1 &&
312 mapping.offset > 1 && index_var->domain.is_interval) {
314 const int offset = mapping.offset - 1;
315 const int size =
ct->arguments[1].values.size();
316 for (
int i = 0; i < size - offset; ++i) {
317 ct->arguments[1].values[i] =
ct->arguments[1].values[i + offset];
319 ct->arguments[1].values.resize(size - offset);
320 affine_map_[index_var].constraint->arguments[2].values[0] = -1;
321 affine_map_[index_var].offset = 1;
322 index_var->domain.values[0] -= offset;
323 index_var->domain.values[1] -= offset;
324 UpdateRuleStats(
"array_int_element: simplify using affine mapping.");
326 }
else if (mapping.offset + mapping.coefficient > 0 &&
327 domain.values[0] > 0) {
328 const std::vector<int64>& values =
ct->arguments[1].values;
329 std::vector<int64> new_values;
330 for (
int64 i = 1; i <= domain.values.back(); ++i) {
331 const int64 index = i * mapping.coefficient + mapping.offset - 1;
335 if (
index > values.size()) {
338 new_values.push_back(values[
index]);
341 UpdateRuleStats(
"array_int_element: simplify using affine mapping.");
342 ct->arguments[0].variables[0] = mapping.variable;
343 ct->arguments[0].variables[0]->domain.IntersectWithInterval(
344 1, new_values.size());
346 ct->arguments[1].values.swap(new_values);
347 if (
ct->arguments[1].values.size() == 1) {
351 ct->presolve_propagation_done =
false;
353 mapping.constraint->MarkAsInactive();
354 index_var->active =
false;
361 UpdateRuleStats(
"array_int_element: rewrite as a 2d element");
362 const Array2DIndexMapping& mapping = array2d_index_map_[index_var];
366 std::vector<int64> coefs;
367 coefs.push_back(mapping.coefficient);
371 index_var->active =
false;
372 mapping.constraint->MarkAsInactive();
377 if (index_var->domain.Max() <
ct->arguments[1].values.size()) {
379 ct->arguments[1].values.resize(index_var->domain.Max());
380 ct->presolve_propagation_done =
false;
381 UpdateRuleStats(
"array_int_element: reduce array");
386 if (IsIncreasingAndContiguous(
ct->arguments[1].values)) {
387 const int64 start =
ct->arguments[1].values.front();
388 IntegerVariable*
const index =
ct->arguments[0].Var();
389 IntegerVariable*
const target =
ct->arguments[2].Var();
390 UpdateRuleStats(
"array_int_element: rewrite as a linear constraint");
397 ct->type =
"int_lin_eq";
409 void Presolver::PresolveSimplifyExprElement(Constraint*
ct) {
410 if (
ct->arguments[0].variables.size() != 1)
return;
412 IntegerVariable*
const index_var =
ct->arguments[0].Var();
414 const AffineMapping& mapping = affine_map_[index_var];
415 const Domain& domain = mapping.variable->domain;
416 if ((domain.is_interval && domain.values.empty()) ||
417 domain.values[0] != 1 || mapping.offset + mapping.coefficient <= 0) {
421 const std::vector<IntegerVariable*>& vars =
ct->arguments[1].variables;
422 std::vector<IntegerVariable*> new_vars;
423 for (
int64 i = domain.values.front(); i <= domain.values.back(); ++i) {
424 const int64 index = i * mapping.coefficient + mapping.offset - 1;
428 if (
index >= vars.size()) {
431 new_vars.push_back(vars[
index]);
434 UpdateRuleStats(
"array_var_int_element: simplify using affine mapping.");
435 ct->arguments[0].variables[0] = mapping.variable;
437 ct->arguments[1].variables.swap(new_vars);
439 mapping.constraint->MarkAsInactive();
440 index_var->active =
false;
441 }
else if (index_var->domain.is_interval &&
442 index_var->domain.values.size() == 2 &&
443 index_var->domain.Max() <
ct->arguments[1].variables.size()) {
445 ct->arguments[1].variables.resize(index_var->domain.Max());
446 UpdateRuleStats(
"array_var_int_element: reduce array");
452 if (absl::GetFlag(FLAGS_fz_floats_are_ints)) {
455 const std::string&
id =
ct->type;
456 if (
id ==
"int2float") {
458 }
else if (
id ==
"float_lin_le") {
459 ct->type =
"int_lin_le";
460 }
else if (
id ==
"float_lin_eq") {
461 ct->type =
"int_lin_eq";
468 std::vector<IntegerVariable*> current_variables;
472 if (target_variable ==
nullptr) {
473 if (
ct->type ==
"int_lin_eq" &&
ct->arguments[0].values.size() == 3 &&
474 AreOnesFollowedByMinusOne(
ct->arguments[0].values) &&
475 ct->arguments[1].values.empty() &&
ct->arguments[2].Value() == 0) {
477 current_variables =
ct->arguments[1].variables;
478 target_variable = current_variables.back();
479 current_variables.pop_back();
480 first_constraint =
ct;
483 if (
ct->type ==
"int_lin_eq" &&
484 AreOnesFollowedByMinusOne(
ct->arguments[0].values) &&
485 ct->arguments[0].values.size() == current_variables.size() + 2 &&
486 IsStrictPrefix(current_variables,
ct->arguments[1].variables)) {
487 FZVLOG <<
"Recognize hidden int_plus " <<
ct->DebugString() <<
FZENDL;
488 current_variables =
ct->arguments[1].variables;
490 ct->type =
"int_plus";
491 ct->arguments.clear();
494 current_variables[current_variables.size() - 2]));
496 target_variable = current_variables.back();
497 current_variables.pop_back();
500 if (first_constraint !=
nullptr) {
501 first_constraint =
nullptr;
504 current_variables.clear();
505 target_variable =
nullptr;
512 if (
ct->active &&
ct->type ==
"bool2int") {
513 PresolveBool2Int(
ct);
514 }
else if (
ct->active &&
ct->type ==
"int_lin_eq" &&
515 ct->arguments[1].variables.size() == 2 &&
516 ct->strong_propagation) {
517 PresolveStoreAffineMapping(
ct);
518 }
else if (
ct->active &&
ct->type ==
"int_lin_eq" &&
519 ct->arguments[1].variables.size() == 3 &&
520 ct->strong_propagation) {
521 PresolveStoreFlatteningMapping(
ct);
524 if (!var_representative_map_.empty()) {
526 SubstituteEverywhere(
model);
527 var_representative_map_.clear();
528 var_representative_vector_.clear();
533 if (
ct->type ==
"array_int_element" ||
ct->type ==
"array_bool_element") {
534 PresolveSimplifyElement(
ct);
536 if (
ct->type ==
"array_var_int_element" ||
537 ct->type ==
"array_var_bool_element") {
538 PresolveSimplifyExprElement(
ct);
543 if (!successful_rules_.empty()) {
544 for (
const auto& rule : successful_rules_) {
545 if (rule.second == 1) {
546 FZLOG <<
" - rule '" << rule.first <<
"' was applied 1 time" <<
FZENDL;
548 FZLOG <<
" - rule '" << rule.first <<
"' was applied " << rule.second
559 CHECK(from !=
nullptr);
560 CHECK(to !=
nullptr);
562 from = FindRepresentativeOfVar(from);
563 to = FindRepresentativeOfVar(to);
575 var_representative_map_[from] = to;
576 var_representative_vector_.push_back(from);
580 IntegerVariable* Presolver::FindRepresentativeOfVar(IntegerVariable*
var) {
581 if (
var ==
nullptr)
return nullptr;
582 IntegerVariable* start_var =
var;
585 IntegerVariable* parent =
587 if (parent ==
var)
break;
591 while (start_var !=
var) {
592 IntegerVariable*
const parent = var_representative_map_[start_var];
593 var_representative_map_[start_var] =
var;
599 void Presolver::SubstituteEverywhere(Model*
model) {
601 for (Constraint*
const ct :
model->constraints()) {
602 if (
ct !=
nullptr &&
ct->active) {
603 for (
int i = 0; i <
ct->arguments.size(); ++i) {
604 Argument& argument =
ct->arguments[i];
605 switch (argument.type) {
608 for (
int i = 0; i < argument.variables.size(); ++i) {
609 IntegerVariable*
const old_var = argument.variables[i];
610 IntegerVariable*
const new_var = FindRepresentativeOfVar(old_var);
611 if (new_var != old_var) {
612 argument.variables[i] = new_var;
624 for (Annotation*
const ann :
model->mutable_search_annotations()) {
625 SubstituteAnnotation(ann);
628 for (SolutionOutputSpecs*
const output :
model->mutable_output()) {
629 output->variable = FindRepresentativeOfVar(output->variable);
630 for (
int i = 0; i < output->flat_variables.size(); ++i) {
631 output->flat_variables[i] =
632 FindRepresentativeOfVar(output->flat_variables[i]);
637 for (
const auto& iter : var_representative_map_) {
638 iter.second->domain.IntersectWithDomain(iter.first->domain);
642 IntegerVariable*
const current_objective =
model->objective();
643 if (current_objective ==
nullptr)
return;
644 IntegerVariable*
const new_objective =
645 FindRepresentativeOfVar(current_objective);
646 if (new_objective != current_objective) {
647 model->SetObjective(new_objective);
651 void Presolver::SubstituteAnnotation(Annotation* ann) {
656 for (
int i = 0; i < ann->annotations.size(); ++i) {
657 SubstituteAnnotation(&ann->annotations[i]);
663 for (
int i = 0; i < ann->variables.size(); ++i) {
664 ann->variables[i] = FindRepresentativeOfVar(ann->variables[i]);