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.");
36enum PresolveState { ALWAYS_FALSE, ALWAYS_TRUE, UNDECIDED };
39bool 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) {
56bool AtMostOne0OrAtMostOne1(
const std::vector<T>& values) {
60 for (T val : values) {
66 if (num_one > 1 && num_zero > 1) {
73absl::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());
90void SetConstraintAsIntEq(Constraint*
ct, IntegerVariable*
var,
int64 value) {
98bool 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";
150void 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);
180void 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();
199void 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");
215void 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");
248bool IsIncreasingAndContiguous(
const std::vector<int64>& values) {
249 for (
int i = 0; i < values.size() - 1; ++i) {
250 if (values[i + 1] != values[i] + 1) {
257bool 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;
268bool 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]) {
299void 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) &&
388 const int64 start =
ct->arguments[1].values.front();
389 IntegerVariable*
const index =
ct->arguments[0].Var();
390 IntegerVariable*
const target =
ct->arguments[2].Var();
391 UpdateRuleStats(
"array_int_element: rewrite as a linear constraint");
398 ct->type =
"int_lin_eq";
410void Presolver::PresolveSimplifyExprElement(Constraint*
ct) {
411 if (
ct->arguments[0].variables.size() != 1)
return;
413 IntegerVariable*
const index_var =
ct->arguments[0].Var();
415 const AffineMapping& mapping = affine_map_[index_var];
416 const Domain& domain = mapping.variable->domain;
417 if ((domain.is_interval && domain.values.empty()) ||
418 domain.values[0] != 1 || mapping.offset + mapping.coefficient <= 0) {
422 const std::vector<IntegerVariable*>& vars =
ct->arguments[1].variables;
423 std::vector<IntegerVariable*> new_vars;
424 for (
int64 i = domain.values.front(); i <= domain.values.back(); ++i) {
425 const int64 index = i * mapping.coefficient + mapping.offset - 1;
429 if (
index >= vars.size()) {
432 new_vars.push_back(vars[
index]);
435 UpdateRuleStats(
"array_var_int_element: simplify using affine mapping.");
436 ct->arguments[0].variables[0] = mapping.variable;
438 ct->arguments[1].variables.swap(new_vars);
440 mapping.constraint->MarkAsInactive();
441 index_var->active =
false;
442 }
else if (index_var->domain.is_interval &&
443 index_var->domain.values.size() == 2 &&
444 index_var->domain.Max() <
ct->arguments[1].variables.size()) {
446 ct->arguments[1].variables.resize(index_var->domain.Max());
447 UpdateRuleStats(
"array_var_int_element: reduce array");
453 if (absl::GetFlag(FLAGS_fz_floats_are_ints)) {
456 const std::string&
id =
ct->type;
457 if (
id ==
"int2float") {
459 }
else if (
id ==
"float_lin_le") {
460 ct->type =
"int_lin_le";
461 }
else if (
id ==
"float_lin_eq") {
462 ct->type =
"int_lin_eq";
469 std::vector<IntegerVariable*> current_variables;
473 if (target_variable ==
nullptr) {
474 if (
ct->type ==
"int_lin_eq" &&
ct->arguments[0].values.size() == 3 &&
475 AreOnesFollowedByMinusOne(
ct->arguments[0].values) &&
476 ct->arguments[1].values.empty() &&
ct->arguments[2].Value() == 0) {
478 current_variables =
ct->arguments[1].variables;
479 target_variable = current_variables.back();
480 current_variables.pop_back();
481 first_constraint =
ct;
484 if (
ct->type ==
"int_lin_eq" &&
485 AreOnesFollowedByMinusOne(
ct->arguments[0].values) &&
486 ct->arguments[0].values.size() == current_variables.size() + 2 &&
487 IsStrictPrefix(current_variables,
ct->arguments[1].variables)) {
488 FZVLOG <<
"Recognize hidden int_plus " <<
ct->DebugString() <<
FZENDL;
489 current_variables =
ct->arguments[1].variables;
491 ct->type =
"int_plus";
492 ct->arguments.clear();
495 current_variables[current_variables.size() - 2]));
497 target_variable = current_variables.back();
498 current_variables.pop_back();
501 if (first_constraint !=
nullptr) {
502 first_constraint =
nullptr;
505 current_variables.clear();
506 target_variable =
nullptr;
513 if (
ct->active &&
ct->type ==
"bool2int") {
514 PresolveBool2Int(
ct);
515 }
else if (
ct->active &&
ct->type ==
"int_lin_eq" &&
516 ct->arguments[1].variables.size() == 2 &&
517 ct->strong_propagation) {
518 PresolveStoreAffineMapping(
ct);
519 }
else if (
ct->active &&
ct->type ==
"int_lin_eq" &&
520 ct->arguments[1].variables.size() == 3 &&
521 ct->strong_propagation) {
522 PresolveStoreFlatteningMapping(
ct);
525 if (!var_representative_map_.empty()) {
527 SubstituteEverywhere(
model);
528 var_representative_map_.clear();
529 var_representative_vector_.clear();
534 if (
ct->type ==
"array_int_element" ||
ct->type ==
"array_bool_element") {
535 PresolveSimplifyElement(
ct);
537 if (
ct->type ==
"array_var_int_element" ||
538 ct->type ==
"array_var_bool_element") {
539 PresolveSimplifyExprElement(
ct);
544 if (!successful_rules_.empty()) {
545 for (
const auto& rule : successful_rules_) {
546 if (rule.second == 1) {
547 FZLOG <<
" - rule '" << rule.first <<
"' was applied 1 time" <<
FZENDL;
549 FZLOG <<
" - rule '" << rule.first <<
"' was applied " << rule.second
560 CHECK(from !=
nullptr);
561 CHECK(to !=
nullptr);
563 from = FindRepresentativeOfVar(from);
564 to = FindRepresentativeOfVar(to);
576 var_representative_map_[from] = to;
577 var_representative_vector_.push_back(from);
581IntegerVariable* Presolver::FindRepresentativeOfVar(IntegerVariable*
var) {
582 if (
var ==
nullptr)
return nullptr;
583 IntegerVariable* start_var =
var;
586 IntegerVariable* parent =
588 if (parent ==
var)
break;
592 while (start_var !=
var) {
593 IntegerVariable*
const parent = var_representative_map_[start_var];
594 var_representative_map_[start_var] =
var;
600void Presolver::SubstituteEverywhere(Model*
model) {
602 for (Constraint*
const ct :
model->constraints()) {
603 if (
ct !=
nullptr &&
ct->active) {
604 for (
int i = 0; i <
ct->arguments.size(); ++i) {
605 Argument& argument =
ct->arguments[i];
606 switch (argument.type) {
609 for (
int i = 0; i < argument.variables.size(); ++i) {
610 IntegerVariable*
const old_var = argument.variables[i];
611 IntegerVariable*
const new_var = FindRepresentativeOfVar(old_var);
612 if (new_var != old_var) {
613 argument.variables[i] = new_var;
625 for (Annotation*
const ann :
model->mutable_search_annotations()) {
626 SubstituteAnnotation(ann);
629 for (SolutionOutputSpecs*
const output :
model->mutable_output()) {
630 output->variable = FindRepresentativeOfVar(output->variable);
631 for (
int i = 0; i < output->flat_variables.size(); ++i) {
632 output->flat_variables[i] =
633 FindRepresentativeOfVar(output->flat_variables[i]);
638 for (
const auto& iter : var_representative_map_) {
639 iter.second->domain.IntersectWithDomain(iter.first->domain);
643 IntegerVariable*
const current_objective =
model->objective();
644 if (current_objective ==
nullptr)
return;
645 IntegerVariable*
const new_objective =
646 FindRepresentativeOfVar(current_objective);
647 if (new_objective != current_objective) {
648 model->SetObjective(new_objective);
652void Presolver::SubstituteAnnotation(Annotation* ann) {
657 for (
int i = 0; i < ann->annotations.size(); ++i) {
658 SubstituteAnnotation(&ann->annotations[i]);
664 for (
int i = 0; i < ann->variables.size(); ++i) {
665 ann->variables[i] = FindRepresentativeOfVar(ann->variables[i]);
#define CHECK_EQ(val1, val2)
#define DCHECK_EQ(val1, val2)
bool ContainsKey(const Collection &collection, const Key &key)
const Collection::value_type::second_type & FindWithDefault(const Collection &collection, const typename Collection::value_type::first_type &key, const typename Collection::value_type::second_type &value)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
bool IsArrayBoolean(const std::vector< T > &values)
ABSL_FLAG(bool, fz_floats_are_ints, true, "Interpret floats as integers in all variables and constraints.")
static Argument IntVarRefArray(std::vector< IntegerVariable * > vars)
static Argument IntegerList(std::vector< int64 > values)
static Argument IntVarRef(IntegerVariable *const var)
static Argument IntegerValue(int64 value)
std::vector< Argument > arguments
std::string DebugString() const
bool Merge(const std::string &other_name, const Domain &other_domain, bool other_temporary)