always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[FZ] change the way we support element and element2d

Browse Source
This commit is contained in:
Laurent Perron
2024-10-18 11:51:43 +02:00
parent 956f4bc362
commit d7ea4008a1
10 changed files with 257 additions and 741 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
ortools/flatzinc/BUILD.bazel
View File

@@ -109,21 +109,6 @@ cc_library(
],
)
cc_library(
name = "presolve",
srcs = ["presolve.cc"],
hdrs = ["presolve.h"],
deps = [
":model",
"//ortools/base",
"//ortools/base:hash",
"//ortools/graph:cliques",
"//ortools/util:logging",
"//ortools/util:saturated_arithmetic",
"@com_google_absl//absl/strings",
],
)
cc_library(
name = "checker",
srcs = ["checker.cc"],
@@ -172,7 +157,6 @@ cc_binary(
":cp_model_fz_solver",
":model",
":parser_lib",
":presolve",
"//ortools/base",
"//ortools/base:path",
"//ortools/base:threadpool",

113
ortools/flatzinc/checker.cc
View File

@@ -150,10 +150,6 @@ bool CheckArrayBoolXor(const Constraint& ct,
bool CheckArrayIntElement(const Constraint& ct,
const std::function<int64_t(Variable*)>& evaluator) {
if (ct.arguments[0].variables.size() == 2) {
// TODO(user): Check 2D element.
return true;
}
// Flatzinc arrays are 1 based.
const int64_t shifted_index = Eval(ct.arguments[0], evaluator) - 1;
const int64_t element = EvalAt(ct.arguments[1], shifted_index, evaluator);
@@ -172,10 +168,6 @@ bool CheckArrayIntElementNonShifted(
bool CheckArrayVarIntElement(
const Constraint& ct, const std::function<int64_t(Variable*)>& evaluator) {
if (ct.arguments[0].variables.size() == 2) {
// TODO(user): Check 2D element.
return true;
}
// Flatzinc arrays are 1 based.
const int64_t shifted_index = Eval(ct.arguments[0], evaluator) - 1;
const int64_t element = EvalAt(ct.arguments[1], shifted_index, evaluator);
@@ -183,6 +175,15 @@ bool CheckArrayVarIntElement(
return element == target;
}
bool CheckOrtoolsArrayIntElement(
const Constraint& ct, const std::function<int64_t(Variable*)>& evaluator) {
const int64_t min_index = ct.arguments[1].values[0];
const int64_t index = Eval(ct.arguments[0], evaluator) - min_index;
const int64_t element = EvalAt(ct.arguments[2], index, evaluator);
const int64_t target = Eval(ct.arguments[3], evaluator);
return element == target;
}
bool CheckAtMostInt(const Constraint& ct,
const std::function<int64_t(Variable*)>& evaluator) {
const int64_t expected = Eval(ct.arguments[0], evaluator);
@@ -1184,7 +1185,6 @@ using CallMap =
// They are created at compilation time when using the or-tools mzn library.
CallMap CreateCallMap() {
CallMap m;
m["fzn_all_different_int"] = CheckAllDifferentInt;
m["alldifferent_except_0"] = CheckAlldifferentExcept0;
m["among"] = CheckAmong;
m["array_bool_and"] = CheckArrayBoolAnd;
@@ -1193,130 +1193,135 @@ CallMap CreateCallMap() {
m["array_bool_xor"] = CheckArrayBoolXor;
m["array_int_element"] = CheckArrayIntElement;
m["array_int_element_nonshifted"] = CheckArrayIntElementNonShifted;
m["array_int_maximum"] = CheckMaximumInt;
m["array_int_minimum"] = CheckMinimumInt;
m["array_var_bool_element"] = CheckArrayVarIntElement;
m["array_var_int_element"] = CheckArrayVarIntElement;
m["at_most_int"] = CheckAtMostInt;
m["bool_and"] = CheckBoolAnd;
m["bool_clause"] = CheckBoolClause;
m["bool_eq"] = CheckIntEq;
m["bool2int"] = CheckIntEq;
m["bool_eq_imp"] = CheckIntEqImp;
m["bool_eq_reif"] = CheckIntEqReif;
m["bool_ge"] = CheckIntGe;
m["bool_eq"] = CheckIntEq;
m["bool_ge_imp"] = CheckIntGeImp;
m["bool_ge_reif"] = CheckIntGeReif;
m["bool_gt"] = CheckIntGt;
m["bool_ge"] = CheckIntGe;
m["bool_gt_imp"] = CheckIntGtImp;
m["bool_gt_reif"] = CheckIntGtReif;
m["bool_le"] = CheckIntLe;
m["bool_gt"] = CheckIntGt;
m["bool_le_imp"] = CheckIntLeImp;
m["bool_le_reif"] = CheckIntLeReif;
m["bool_le"] = CheckIntLe;
m["bool_left_imp"] = CheckIntLe;
m["bool_lin_eq"] = CheckIntLinEq;
m["bool_lin_le"] = CheckIntLinLe;
m["bool_lt"] = CheckIntLt;
m["bool_lt_imp"] = CheckIntLtImp;
m["bool_lt_reif"] = CheckIntLtReif;
m["bool_ne"] = CheckIntNe;
m["bool_lt"] = CheckIntLt;
m["bool_ne_imp"] = CheckIntNeImp;
m["bool_ne_reif"] = CheckIntNeReif;
m["bool_ne"] = CheckIntNe;
m["bool_not"] = CheckBoolNot;
m["bool_or"] = CheckBoolOr;
m["bool_right_imp"] = CheckIntGe;
m["bool_xor"] = CheckBoolXor;
m["ortools_circuit"] = CheckCircuit;
m["bool2int"] = CheckIntEq;
m["count_eq"] = CheckCountEq;
m["count"] = CheckCountEq;
m["count_geq"] = CheckCountGeq;
m["count_gt"] = CheckCountGt;
m["count_leq"] = CheckCountLeq;
m["count_lt"] = CheckCountLt;
m["count_neq"] = CheckCountNeq;
m["count_reif"] = CheckCountReif;
m["fzn_cumulative"] = CheckCumulative;
m["var_cumulative"] = CheckCumulative;
m["variable_cumulative"] = CheckCumulative;
m["fixed_cumulative"] = CheckCumulative;
m["ortools_cumulative_opt"] = CheckCumulativeOpt;
m["fzn_diffn"] = CheckDiffn;
m["count"] = CheckCountEq;
m["diffn_k_with_sizes"] = CheckDiffnK;
m["fzn_diffn_nonstrict"] = CheckDiffnNonStrict;
m["diffn_nonstrict_k_with_sizes"] = CheckDiffnNonStrictK;
m["fzn_disjunctive"] = CheckDisjunctive;
m["fzn_disjunctive_strict"] = CheckDisjunctiveStrict;
m["ortools_disjunctive_strict_opt"] = CheckDisjunctiveStrictOpt;
m["false_constraint"] = CheckFalseConstraint;
m["global_cardinality"] = CheckGlobalCardinality;
m["fixed_cumulative"] = CheckCumulative;
m["fzn_all_different_int"] = CheckAllDifferentInt;
m["fzn_cumulative"] = CheckCumulative;
m["fzn_diffn_nonstrict"] = CheckDiffnNonStrict;
m["fzn_diffn"] = CheckDiffn;
m["fzn_disjunctive_strict"] = CheckDisjunctiveStrict;
m["fzn_disjunctive"] = CheckDisjunctive;
m["global_cardinality_closed"] = CheckGlobalCardinalityClosed;
m["global_cardinality_low_up"] = CheckGlobalCardinalityLowUp;
m["global_cardinality_low_up_closed"] = CheckGlobalCardinalityLowUpClosed;
m["global_cardinality_low_up"] = CheckGlobalCardinalityLowUp;
m["global_cardinality_old"] = CheckGlobalCardinalityOld;
m["global_cardinality"] = CheckGlobalCardinality;
m["int_abs"] = CheckIntAbs;
m["int_div"] = CheckIntDiv;
m["int_eq"] = CheckIntEq;
m["int_eq_imp"] = CheckIntEqImp;
m["int_eq_reif"] = CheckIntEqReif;
m["int_ge"] = CheckIntGe;
m["int_eq"] = CheckIntEq;
m["int_ge_imp"] = CheckIntGeImp;
m["int_ge_reif"] = CheckIntGeReif;
m["int_gt"] = CheckIntGt;
m["int_ge"] = CheckIntGe;
m["int_gt_imp"] = CheckIntGtImp;
m["int_gt_reif"] = CheckIntGtReif;
m["int_le"] = CheckIntLe;
m["int_gt"] = CheckIntGt;
m["int_in"] = CheckSetIn;
m["int_le_imp"] = CheckIntLeImp;
m["int_le_reif"] = CheckIntLeReif;
m["int_lin_eq"] = CheckIntLinEq;
m["int_le"] = CheckIntLe;
m["int_lin_eq_imp"] = CheckIntLinEqImp;
m["int_lin_eq_reif"] = CheckIntLinEqReif;
m["int_lin_ge"] = CheckIntLinGe;
m["int_lin_eq"] = CheckIntLinEq;
m["int_lin_ge_imp"] = CheckIntLinGeImp;
m["int_lin_ge_reif"] = CheckIntLinGeReif;
m["int_lin_le"] = CheckIntLinLe;
m["int_lin_ge"] = CheckIntLinGe;
m["int_lin_le_imp"] = CheckIntLinLeImp;
m["int_lin_le_reif"] = CheckIntLinLeReif;
m["int_lin_ne"] = CheckIntLinNe;
m["int_lin_le"] = CheckIntLinLe;
m["int_lin_ne_imp"] = CheckIntLinNeImp;
m["int_lin_ne_reif"] = CheckIntLinNeReif;
m["int_lt"] = CheckIntLt;
m["int_lin_ne"] = CheckIntLinNe;
m["int_lt_imp"] = CheckIntLtImp;
m["int_lt_reif"] = CheckIntLtReif;
m["int_lt"] = CheckIntLt;
m["int_max"] = CheckIntMax;
m["int_min"] = CheckIntMin;
m["int_minus"] = CheckIntMinus;
m["int_mod"] = CheckIntMod;
m["int_ne"] = CheckIntNe;
m["int_ne_imp"] = CheckIntNeImp;
m["int_ne_reif"] = CheckIntNeReif;
m["int_ne"] = CheckIntNe;
m["int_negate"] = CheckIntNegate;
m["int_not_in"] = CheckSetNotIn;
m["int_plus"] = CheckIntPlus;
m["int_times"] = CheckIntTimes;
m["ortools_inverse"] = CheckInverse;
m["lex_less_bool"] = CheckLexLessInt;
m["lex_less_int"] = CheckLexLessInt;
m["lex_lesseq_bool"] = CheckLexLesseqInt;
m["lex_lesseq_int"] = CheckLexLesseqInt;
m["maximum_arg_int"] = CheckMaximumArgInt;
m["maximum_int"] = CheckMaximumInt;
m["array_int_maximum"] = CheckMaximumInt;
m["minimum_arg_int"] = CheckMinimumArgInt;
m["minimum_int"] = CheckMinimumInt;
m["array_int_minimum"] = CheckMinimumInt;
m["ortools_network_flow"] = CheckNetworkFlow;
m["ortools_network_flow_cost"] = CheckNetworkFlowCost;
m["nvalue"] = CheckNvalue;
m["ortools_array_bool_element"] = CheckOrtoolsArrayIntElement;
m["ortools_array_int_element"] = CheckOrtoolsArrayIntElement;
m["ortools_array_var_bool_element"] = CheckOrtoolsArrayIntElement;
m["ortools_array_var_int_element"] = CheckOrtoolsArrayIntElement;
m["ortools_circuit"] = CheckCircuit;
m["ortools_cumulative_opt"] = CheckCumulativeOpt;
m["ortools_disjunctive_strict_opt"] = CheckDisjunctiveStrictOpt;
m["ortools_inverse"] = CheckInverse;
m["ortools_network_flow_cost"] = CheckNetworkFlowCost;
m["ortools_network_flow"] = CheckNetworkFlow;
m["ortools_regular"] = CheckRegular;
m["regular_nfa"] = CheckRegularNfa;
m["set_in"] = CheckSetIn;
m["int_in"] = CheckSetIn;
m["set_not_in"] = CheckSetNotIn;
m["int_not_in"] = CheckSetNotIn;
m["set_in_reif"] = CheckSetInReif;
m["sliding_sum"] = CheckSlidingSum;
m["sort"] = CheckSort;
m["ortools_subcircuit"] = CheckSubCircuit;
m["symmetric_all_different"] = CheckSymmetricAllDifferent;
m["ortools_table_bool"] = CheckTableInt;
m["ortools_table_int"] = CheckTableInt;
m["regular_nfa"] = CheckRegularNfa;
m["set_in_reif"] = CheckSetInReif;
m["set_in"] = CheckSetIn;
m["set_not_in"] = CheckSetNotIn;
m["sliding_sum"] = CheckSlidingSum;
m["sort"] = CheckSort;
m["symmetric_all_different"] = CheckSymmetricAllDifferent;
m["var_cumulative"] = CheckCumulative;
m["variable_cumulative"] = CheckCumulative;
return m;
}

3
ortools/flatzinc/cp-sat.msc.in
View File

@@ -8,7 +8,8 @@
"tags": ["cp-sat", "cp", "lcg", "int"],
"stdFlags": ["-a", "-i", "-f", "-p", "-r", "-s", "-v"],
"extraFlags": [
["--params", "Provide parameters interpreted as a text SatParameters proto", "string", ""]
["--params", "Provide parameters interpreted as a text SatParameters proto", "string", ""],
["--fz_int_max", "Provide the maximum value for integer variables", "int", "1125899906842624"]
],
"supportsMzn": false,
"supportsFzn": true,

186
ortools/flatzinc/cp_model_fz_solver.cc
View File

@@ -19,6 +19,7 @@
#include <limits>
#include <string>
#include <tuple>
#include <utility>
#include <vector>
#include "absl/container/flat_hash_map.h"
@@ -117,6 +118,8 @@ struct CpModelProtoWithMapping {
void FillConstraint(const fz::Constraint& fz_ct, ConstraintProto* ct);
void FillReifOrImpliedConstraint(const fz::Constraint& fz_ct,
ConstraintProto* ct);
void BuildTableFromDomainIntLinEq(const fz::Constraint& fz_ct,
ConstraintProto* ct);
// Translates the flatzinc search annotations into the CpModelProto
// search_order field.
@@ -415,6 +418,51 @@ void CpModelProtoWithMapping::FillLinearConstraintWithGivenDomain(
}
}
void CpModelProtoWithMapping::BuildTableFromDomainIntLinEq(
const fz::Constraint& fz_ct, ConstraintProto* ct) {
const std::vector<int64_t>& coeffs = fz_ct.arguments[0].values;
const std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
const int rhs = fz_ct.arguments[2].Value();
CHECK_EQ(coeffs.back(), -1);
for (const int var : vars) ct->mutable_table()->add_vars(var);
switch (vars.size()) {
case 3: {
const Domain domain0 = ReadDomainFromProto(proto.variables(vars[0]));
const Domain domain1 = ReadDomainFromProto(proto.variables(vars[1]));
for (const int64_t v0 : domain0.Values()) {
for (const int64_t v1 : domain1.Values()) {
const int64_t v2 = coeffs[0] * v0 + coeffs[1] * v1 - rhs;
ct->mutable_table()->add_values(v0);
ct->mutable_table()->add_values(v1);
ct->mutable_table()->add_values(v2);
}
}
break;
}
case 4: {
const Domain domain0 = ReadDomainFromProto(proto.variables(vars[0]));
const Domain domain1 = ReadDomainFromProto(proto.variables(vars[1]));
const Domain domain2 = ReadDomainFromProto(proto.variables(vars[2]));
for (const int64_t v0 : domain0.Values()) {
for (const int64_t v1 : domain1.Values()) {
for (const int64_t v2 : domain2.Values()) {
const int64_t v3 =
coeffs[0] * v0 + coeffs[1] * v1 + coeffs[2] * v2 - rhs;
ct->mutable_table()->add_values(v0);
ct->mutable_table()->add_values(v1);
ct->mutable_table()->add_values(v2);
ct->mutable_table()->add_values(v3);
}
}
}
break;
}
default:
LOG(FATAL) << "Unsupported size";
}
}
void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
ConstraintProto* ct) {
if (fz_ct.type == "false_constraint") {
@@ -502,8 +550,15 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
std::numeric_limits<int64_t>::max()},
fz_ct, ct);
} else if (fz_ct.type == "int_lin_eq") {
const int64_t rhs = fz_ct.arguments[2].values[0];
FillLinearConstraintWithGivenDomain({rhs, rhs}, fz_ct, ct);
// Special case for the index of element 2D and element 3D constraints.
if (fz_ct.strong_propagation && fz_ct.arguments[0].Size() >= 3 &&
fz_ct.arguments[0].Size() <= 4 &&
fz_ct.arguments[0].values.back() == -1) {
BuildTableFromDomainIntLinEq(fz_ct, ct);
} else {
const int64_t rhs = fz_ct.arguments[2].values[0];
FillLinearConstraintWithGivenDomain({rhs, rhs}, fz_ct, ct);
}
} else if (fz_ct.type == "bool_lin_eq") {
auto* arg = ct->mutable_linear();
const std::vector<int> vars = LookupVars(fz_ct.arguments[1]);
@@ -634,45 +689,45 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
fz_ct.type == "array_var_int_element" ||
fz_ct.type == "array_var_bool_element" ||
fz_ct.type == "array_int_element_nonshifted") {
if (fz_ct.arguments[0].type == fz::Argument::VAR_REF ||
fz_ct.arguments[0].type == fz::Argument::INT_VALUE) {
auto* arg = ct->mutable_element();
arg->set_index(LookupVar(fz_ct.arguments[0]));
arg->set_target(LookupVar(fz_ct.arguments[2]));
auto* arg = ct->mutable_element();
*arg->mutable_linear_index() = LookupExpr(fz_ct.arguments[0]);
if (!absl::EndsWith(fz_ct.type, "_nonshifted")) {
arg->mutable_linear_index()->set_offset(arg->linear_index().offset() - 1);
}
*arg->mutable_linear_target() = LookupExpr(fz_ct.arguments[2]);
if (!absl::EndsWith(fz_ct.type, "_nonshifted")) {
// Add a dummy variable at position zero because flatzinc index start
// at 1.
// TODO(user): Make sure that zero is not in the index domain...
arg->add_vars(LookupConstant(0));
for (const VarOrValue elem : LookupVarsOrValues(fz_ct.arguments[1])) {
auto* elem_proto = ct->mutable_element()->add_exprs();
if (elem.var != kNoVar) {
elem_proto->add_vars(elem.var);
elem_proto->add_coeffs(1);
} else {
elem_proto->set_offset(elem.value);
}
for (const int var : LookupVars(fz_ct.arguments[1])) arg->add_vars(var);
} else {
// Special case added by the presolve or in flatzinc. We encode this
// as a table constraint.
CHECK(!absl::EndsWith(fz_ct.type, "_nonshifted"));
auto* arg = ct->mutable_table();
}
} else if (fz_ct.type == "ortools_array_int_element" ||
fz_ct.type == "ortools_array_bool_element" ||
fz_ct.type == "ortools_array_var_int_element" ||
fz_ct.type == "ortools_array_var_bool_element") {
auto* arg = ct->mutable_element();
// the constraint is:
// values[coeff1 * vars[0] + coeff2 * vars[1] + offset] == target.
for (const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(var);
arg->add_vars(LookupVar(fz_ct.arguments[2])); // the target
// Index.
*arg->mutable_linear_index() = LookupExpr(fz_ct.arguments[0]);
const int64_t index_min = fz_ct.arguments[1].values[0];
arg->mutable_linear_index()->set_offset(arg->linear_index().offset() -
index_min);
const std::vector<int64_t>& values = fz_ct.arguments[1].values;
const int64_t coeff1 = fz_ct.arguments[3].values[0];
const int64_t coeff2 = fz_ct.arguments[3].values[1];
const int64_t offset = fz_ct.arguments[4].values[0] - 1;
// Target.
*arg->mutable_linear_target() = LookupExpr(fz_ct.arguments[3]);
for (const int64_t a : AllValuesInDomain(proto.variables(arg->vars(0)))) {
for (const int64_t b :
AllValuesInDomain(proto.variables(arg->vars(1)))) {
const int index = coeff1 * a + coeff2 * b + offset;
CHECK_GE(index, 0);
CHECK_LT(index, values.size());
arg->add_values(a);
arg->add_values(b);
arg->add_values(values[index]);
}
// Expressions.
for (const VarOrValue elem : LookupVarsOrValues(fz_ct.arguments[2])) {
auto* elem_proto = ct->mutable_element()->add_exprs();
if (elem.var != kNoVar) {
elem_proto->add_vars(elem.var);
elem_proto->add_coeffs(1);
} else {
elem_proto->set_offset(elem.value);
}
}
} else if (fz_ct.type == "ortools_table_int") {
@@ -1277,6 +1332,65 @@ void OutputFlatzincStats(const CpSolverResponse& response,
} // namespace
void ProcessFloatingPointOVariablesAndObjective(fz::Model* fz_model) {
// Scan the model, rename int2float to int_eq, change type of the floating
// point variables to integer.
for (fz::Constraint* ct : fz_model->constraints()) {
if (!ct->active) continue;
if (ct->type == "int2float") {
ct->type = "int_eq";
fz::Domain& float_domain = ct->arguments[1].variables[0]->domain;
float_domain.is_float = false;
for (const double float_value : float_domain.float_values) {
float_domain.values.push_back(static_cast<int64_t>(float_value));
}
float_domain.float_values.clear();
}
}
// Scan the model to find the float objective variable and the float objective
// constraint if defined.
fz::Variable* float_objective_var = nullptr;
for (fz::Variable* var : fz_model->variables()) {
if (!var->active) continue;
if (var->domain.is_float) {
CHECK(float_objective_var == nullptr);
float_objective_var = var;
}
}
fz::Constraint* float_objective_ct = nullptr;
if (float_objective_var != nullptr) {
for (fz::Constraint* ct : fz_model->constraints()) {
if (!ct->active) continue;
if (ct->type == "float_lin_eq") {
CHECK(float_objective_ct == nullptr);
float_objective_ct = ct;
break;
}
}
}
if (float_objective_ct != nullptr || float_objective_var != nullptr) {
CHECK(float_objective_ct != nullptr);
CHECK(float_objective_var != nullptr);
const int arity = float_objective_ct->arguments[0].Size();
CHECK_EQ(float_objective_ct->arguments[1].variables[arity - 1],
float_objective_var);
CHECK_EQ(float_objective_ct->arguments[0].floats[arity - 1], -1.0);
for (int i = 0; i + 1 < arity; ++i) {
fz_model->AddFloatingPointObjectiveTerm(
float_objective_ct->arguments[1].variables[i],
float_objective_ct->arguments[0].floats[i]);
}
fz_model->SetFloatingPointObjectiveOffset(
-float_objective_ct->arguments[2].floats[0]);
fz_model->ClearObjective();
float_objective_var->active = false;
float_objective_ct->active = false;
}
}
void SolveFzWithCpModelProto(const fz::Model& fz_model,
const fz::FlatzincSatParameters& p,
const std::string& sat_params,

10
ortools/flatzinc/cp_model_fz_solver.h
View File

@@ -38,6 +38,16 @@ struct FlatzincSatParameters {
namespace sat {
// Scan the model to replace all int2float to int_eq, and all floating point
// variables used in these int2float constraint to be integral.
//
// Scan the model to find a floating point objective (defined by a single
// floating point variable and a single float_lin_eq constraint defining it),
// and replace them by a single objective with integer variables and floating
// point weights.
void ProcessFloatingPointOVariablesAndObjective(fz::Model* fz_model);
// Solves the given flatzinc model using the CP-SAT solver.
void SolveFzWithCpModelProto(const fz::Model& model,
const fz::FlatzincSatParameters& p,
const std::string& sat_params,

14
ortools/flatzinc/fz.cc
View File

@@ -39,7 +39,6 @@
#include "ortools/flatzinc/cp_model_fz_solver.h"
#include "ortools/flatzinc/model.h"
#include "ortools/flatzinc/parser.h"
#include "ortools/flatzinc/presolve.h"
#include "ortools/util/logging.h"
ABSL_FLAG(double, time_limit, 0, "time limit in seconds.");
@@ -50,7 +49,6 @@ ABSL_FLAG(bool, free_search, false,
"If false, the solver must follow the defined search."
"If true, other search are allowed.");
ABSL_FLAG(int, threads, 0, "Number of threads the solver will use.");
ABSL_FLAG(bool, presolve, true, "Presolve the model to simplify it.");
ABSL_FLAG(bool, statistics, false, "Print solver statistics after search.");
ABSL_FLAG(bool, read_from_stdin, false,
"Read the FlatZinc from stdin, not from a file.");
@@ -153,15 +151,6 @@ Model ParseFlatzincModel(const std::string& input, bool input_is_filename,
" parsed in ", timer.GetInMs(), " ms");
SOLVER_LOG(logger, "");
// Presolve the model.
Presolver presolve(logger);
SOLVER_LOG(logger, "Presolve model");
timer.Reset();
timer.Start();
presolve.Run(&model);
SOLVER_LOG(logger, " - done in ", timer.GetInMs(), " ms");
SOLVER_LOG(logger);
// Print statistics.
ModelStatistics stats(model, logger);
stats.BuildStatistics();
@@ -216,9 +205,10 @@ int main(int argc, char** argv) {
logger.SetLogToStdOut(true);
}
const operations_research::fz::Model model =
operations_research::fz::Model model =
operations_research::fz::ParseFlatzincModel(
input, !absl::GetFlag(FLAGS_read_from_stdin), &logger);
operations_research::sat::ProcessFloatingPointOVariablesAndObjective(&model);
operations_research::fz::FlatzincSatParameters parameters;
parameters.display_all_solutions = absl::GetFlag(FLAGS_display_all_solutions);

32
ortools/flatzinc/mznlib/redefinitions-2.0.2.mzn Normal file
View File

@@ -0,0 +1,32 @@
% Ignore.
predicate symmetry_breaking_constraint(var bool: b) = b;
predicate redundant_constraint(var bool: b) = b;
% array_var_bool_element_nonshifted.
predicate ortools_array_var_bool_element(var int: idx,
set of int: domain_of_x,
array [int] of var bool: x,
var bool: c);
predicate array_var_bool_element_nonshifted(var int: idx,
array [int] of var bool: x,
var bool: c) =
ortools_array_var_bool_element(idx, index_set(x), x, c);
% array_var_int_element_nonshifted.
predicate ortools_array_var_int_element(var int: idx,
set of int: domain_of_x,
array [int] of var int: x,
var int: c);
predicate array_var_int_element_nonshifted(var int: idx,
array [int] of var int: x,
var int: c) =
ortools_array_var_int_element(idx, index_set(x), x, c);
predicate array_var_float_element_nonshifted(var int: idx, array[int] of var float: x, var float: c) =
array_var_float_element((idx-(min(index_set(x))-1))::domain,array1d(x),c);
predicate array_var_set_element_nonshifted(var int: idx, array[int] of var set of int: x, var set of int: c) =
array_var_set_element((idx-(min(index_set(x))-1))::domain,array1d(x),c);

14
ortools/flatzinc/parser_main.cc
View File

@@ -25,7 +25,6 @@
#include "ortools/base/timer.h"
#include "ortools/flatzinc/model.h"
#include "ortools/flatzinc/parser.h"
#include "ortools/flatzinc/presolve.h"
#include "ortools/util/logging.h"
ABSL_FLAG(std::string, input, "", "Input file in the flatzinc format.");
@@ -35,7 +34,7 @@ ABSL_FLAG(bool, statistics, false, "Print model statistics");
namespace operations_research {
namespace fz {
void ParseFile(const std::string& filename, bool presolve) {
void ParseFile(const std::string& filename) {
WallTimer timer;
timer.Start();
@@ -58,14 +57,6 @@ void ParseFile(const std::string& filename, bool presolve) {
Model model(problem_name);
CHECK(ParseFlatzincFile(filename, &model));
if (presolve) {
SOLVER_LOG(&logger, "Presolve model");
timer.Reset();
timer.Start();
Presolver presolve(&logger);
presolve.Run(&model);
SOLVER_LOG(&logger, " - done in ", timer.GetInMs(), " ms");
}
if (absl::GetFlag(FLAGS_statistics)) {
ModelStatistics stats(model, &logger);
stats.BuildStatistics();
@@ -85,7 +76,6 @@ int main(int argc, char** argv) {
absl::SetProgramUsageMessage(kUsage);
absl::ParseCommandLine(argc, argv);
google::InitGoogleLogging(argv[0]);
operations_research::fz::ParseFile(absl::GetFlag(FLAGS_input),
absl::GetFlag(FLAGS_presolve));
operations_research::fz::ParseFile(absl::GetFlag(FLAGS_input));
return 0;
}

495
ortools/flatzinc/presolve.cc
View File

@@ -1,495 +0,0 @@
// Copyright 2010-2024 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#include "ortools/flatzinc/presolve.h"
#include <cstdint>
#include <map>
#include <set>
#include <string>
#include <vector>
#include "absl/container/flat_hash_set.h"
#include "absl/flags/flag.h"
#include "absl/log/check.h"
#include "absl/strings/string_view.h"
#include "absl/types/span.h"
#include "ortools/flatzinc/model.h"
#include "ortools/util/logging.h"
ABSL_FLAG(bool, fz_floats_are_ints, false,
"Interpret floats as integers in all variables and constraints.");
namespace operations_research {
namespace fz {
namespace {
enum PresolveState { ALWAYS_FALSE, ALWAYS_TRUE, UNDECIDED };
template <class T>
bool IsArrayBoolean(const std::vector<T>& values) {
for (int i = 0; i < values.size(); ++i) {
if (values[i] != 0 && values[i] != 1) {
return false;
}
}
return true;
}
template <class T>
bool AtMostOne0OrAtMostOne1(const std::vector<T>& values) {
CHECK(IsArrayBoolean(values));
int num_zero = 0;
int num_one = 0;
for (T val : values) {
if (val) {
num_one++;
} else {
num_zero++;
}
if (num_one > 1 && num_zero > 1) {
return false;
}
}
return true;
}
template <class T>
void AppendIfNotInSet(T* value, absl::flat_hash_set<T*>* s,
std::vector<T*>* vec) {
if (s->insert(value).second) {
vec->push_back(value);
}
DCHECK_EQ(s->size(), vec->size());
}
} // namespace
// Note on documentation
//
// In order to document presolve rules, we will use the following naming
// convention:
// - x, x1, xi, y, y1, yi denote integer variables
// - b, b1, bi denote boolean variables
// - c, c1, ci denote integer constants
// - t, t1, ti denote boolean constants
// - => x after a constraint denotes the target variable of this constraint.
// Arguments are listed in order.
// Propagates cast constraint.
// Rule 1:
// Input: bool2int(b, c) or bool2int(t, x)
// Output: int_eq(...)
//
// Rule 2:
// Input: bool2int(b, x)
// Action: Replace all instances of x by b.
// Output: inactive constraint
void Presolver::PresolveBool2Int(Constraint* ct) {
DCHECK_EQ(ct->type, "bool2int");
if (ct->arguments[0].HasOneValue() || ct->arguments[1].HasOneValue()) {
// Rule 1.
UpdateRuleStats("bool2int: rename to int_eq");
ct->type = "int_eq";
} else {
// Rule 2.
UpdateRuleStats("bool2int: merge boolean and integer variables.");
AddVariableSubstitution(ct->arguments[1].Var(), ct->arguments[0].Var());
ct->MarkAsInactive();
}
}
// Propagates cast constraint.
// Rule 1:
// Input: int2float(x, y)
// Action: Replace all instances of y by x.
// Output: inactive constraint
void Presolver::PresolveInt2Float(Constraint* ct) {
DCHECK_EQ(ct->type, "int2float");
// Rule 1.
UpdateRuleStats("int2float: merge integer and floating point variables.");
AddVariableSubstitution(ct->arguments[1].Var(), ct->arguments[0].Var());
ct->MarkAsInactive();
}
void Presolver::PresolveStoreFlatteningMapping(Constraint* ct) {
CHECK_EQ(3, ct->arguments[1].variables.size());
Variable* const var0 = ct->arguments[1].variables[0];
Variable* const var1 = ct->arguments[1].variables[1];
Variable* const var2 = ct->arguments[1].variables[2];
const int64_t coeff0 = ct->arguments[0].values[0];
const int64_t coeff1 = ct->arguments[0].values[1];
const int64_t coeff2 = ct->arguments[0].values[2];
const int64_t rhs = ct->arguments[2].Value();
if (coeff0 == -1 && coeff2 == 1 && !array2d_index_map_.contains(var0)) {
array2d_index_map_[var0] =
Array2DIndexMapping(var1, coeff1, var2, -rhs, ct);
UpdateRuleStats("int_lin_eq: store 2d flattening mapping");
} else if (coeff0 == -1 && coeff1 == 1 &&
!array2d_index_map_.contains(var0)) {
array2d_index_map_[var0] =
Array2DIndexMapping(var2, coeff2, var1, -rhs, ct);
UpdateRuleStats("int_lin_eq: store 2d flattening mapping");
} else if (coeff2 == -1 && coeff1 == 1 &&
!array2d_index_map_.contains(var2)) {
array2d_index_map_[var2] =
Array2DIndexMapping(var0, coeff0, var1, -rhs, ct);
UpdateRuleStats("int_lin_eq: store 2d flattening mapping");
} else if (coeff2 == -1 && coeff0 == 1 &&
!array2d_index_map_.contains(var2)) {
array2d_index_map_[var2] =
Array2DIndexMapping(var1, coeff1, var0, -rhs, ct);
UpdateRuleStats("int_lin_eq: store 2d flattening mapping");
}
}
namespace {
bool IsIncreasingAndContiguous(absl::Span<const int64_t> values) {
for (int i = 0; i < values.size() - 1; ++i) {
if (values[i + 1] != values[i] + 1) {
return false;
}
}
return true;
}
bool AreOnesFollowedByMinusOne(absl::Span<const int64_t> coeffs) {
CHECK(!coeffs.empty());
for (int i = 0; i < coeffs.size() - 1; ++i) {
if (coeffs[i] != 1) {
return false;
}
}
return coeffs.back() == -1;
}
template <class T>
bool IsStrictPrefix(const std::vector<T>& v1, const std::vector<T>& v2) {
if (v1.size() >= v2.size()) {
return false;
}
for (int i = 0; i < v1.size(); ++i) {
if (v1[i] != v2[i]) {
return false;
}
}
return true;
}
} // namespace
// Rewrite array element: array_int_element:
//
// Rule 1:
// Input : array_int_element(x, [c1, .., cn], y) with x = a * x1 + x2 + b
// Output: array_int_element([x1, x2], [c_a1, .., c_am], b, [a, b])
// to be interpreted by the extraction process.
//
// Rule 2:
// Input : array_int_element(x, [c1, .., cn], y) with x0 ci = c0 + i
// Output: int_lin_eq([-1, 1], [y, x], 1 - c) (e.g. y = x + c - 1)
void Presolver::PresolveSimplifyElement(Constraint* ct) {
if (ct->arguments[0].variables.size() != 1) return;
Variable* const index_var = ct->arguments[0].Var();
// Rule 1.
if (array2d_index_map_.contains(index_var)) {
UpdateRuleStats("array_int_element: rewrite as a 2d element");
const Array2DIndexMapping& mapping = array2d_index_map_[index_var];
// Rewrite constraint.
ct->arguments[0] =
Argument::VarRefArray({mapping.variable1, mapping.variable2});
std::vector<int64_t> coefs;
coefs.push_back(mapping.coefficient);
coefs.push_back(1);
ct->arguments.push_back(Argument::IntegerList(coefs));
ct->arguments.push_back(Argument::IntegerValue(mapping.offset));
index_var->active = false;
mapping.constraint->MarkAsInactive();
return;
}
// Rule 2.
if (IsIncreasingAndContiguous(ct->arguments[1].values) &&
ct->arguments[2].type == Argument::VAR_REF) {
const int64_t start = ct->arguments[1].values.front();
Variable* const index = ct->arguments[0].Var();
Variable* const target = ct->arguments[2].Var();
UpdateRuleStats("array_int_element: rewrite as a linear constraint");
if (start == 1) {
ct->type = "int_eq";
ct->RemoveArg(1);
} else {
// Rewrite constraint into a int_lin_eq
ct->type = "int_lin_eq";
ct->arguments[0] = Argument::IntegerList({-1, 1});
ct->arguments[1] = Argument::VarRefArray({target, index});
ct->arguments[2] = Argument::IntegerValue(1 - start);
}
}
}
void Presolver::Run(Model* model) {
// Should rewrite float constraints.
if (absl::GetFlag(FLAGS_fz_floats_are_ints)) {
// Treat float variables as int variables, convert constraints to int.
for (Constraint* const ct : model->constraints()) {
const std::string& id = ct->type;
if (id == "int2float") {
ct->type = "int_eq";
} else if (id == "float_lin_le") {
ct->type = "int_lin_le";
} else if (id == "float_lin_eq") {
ct->type = "int_lin_eq";
}
}
}
// Regroup increasing sequence of int_lin_eq([1,..,1,-1], [x1, ..., xn, yn])
// into sequence of int_plus(x1, x2, y2), int_plus(y2, x3, y3)...
std::vector<Variable*> current_variables;
Variable* target_variable = nullptr;
Constraint* first_constraint = nullptr;
for (Constraint* const ct : model->constraints()) {
if (target_variable == nullptr) {
if (ct->type == "int_lin_eq" && ct->arguments[0].values.size() == 3 &&
AreOnesFollowedByMinusOne(ct->arguments[0].values) &&
ct->arguments[1].values.empty() && ct->arguments[2].Value() == 0) {
current_variables = ct->arguments[1].variables;
target_variable = current_variables.back();
current_variables.pop_back();
first_constraint = ct;
}
} else {
if (ct->type == "int_lin_eq" &&
AreOnesFollowedByMinusOne(ct->arguments[0].values) &&
ct->arguments[0].values.size() == current_variables.size() + 2 &&
IsStrictPrefix(current_variables, ct->arguments[1].variables)) {
current_variables = ct->arguments[1].variables;
// Rewrite ct into int_plus.
ct->type = "int_plus";
ct->arguments.clear();
ct->arguments.push_back(Argument::VarRef(target_variable));
ct->arguments.push_back(
Argument::VarRef(current_variables[current_variables.size() - 2]));
ct->arguments.push_back(Argument::VarRef(current_variables.back()));
target_variable = current_variables.back();
current_variables.pop_back();
// We clean the first constraint too.
if (first_constraint != nullptr) {
first_constraint = nullptr;
}
} else {
current_variables.clear();
target_variable = nullptr;
}
}
}
// First pass.
for (Constraint* const ct : model->constraints()) {
if (ct->active && ct->type == "bool2int") {
PresolveBool2Int(ct);
} else if (ct->active && ct->type == "int2float") {
PresolveInt2Float(ct);
} else if (ct->active && ct->type == "int_lin_eq" &&
ct->arguments[1].variables.size() == 3 &&
ct->strong_propagation) {
PresolveStoreFlatteningMapping(ct);
}
}
if (!var_representative_map_.empty()) {
// Some new substitutions were introduced. Let's process them.
SubstituteEverywhere(model);
var_representative_map_.clear();
var_representative_vector_.clear();
}
// Second pass.
for (Constraint* const ct : model->constraints()) {
if (ct->type == "array_int_element" || ct->type == "array_bool_element") {
PresolveSimplifyElement(ct);
}
}
// Third pass: process objective with floating point coefficients.
Variable* float_objective_var = nullptr;
for (Variable* var : model->variables()) {
if (!var->active) continue;
if (var->domain.is_float) {
CHECK(float_objective_var == nullptr);
float_objective_var = var;
}
}
Constraint* float_objective_ct = nullptr;
if (float_objective_var != nullptr) {
for (Constraint* ct : model->constraints()) {
if (!ct->active) continue;
if (ct->type == "float_lin_eq") {
CHECK(float_objective_ct == nullptr);
float_objective_ct = ct;
break;
}
}
}
if (float_objective_ct != nullptr || float_objective_var != nullptr) {
CHECK(float_objective_ct != nullptr);
CHECK(float_objective_var != nullptr);
const int arity = float_objective_ct->arguments[0].Size();
CHECK_EQ(float_objective_ct->arguments[1].variables[arity - 1],
float_objective_var);
CHECK_EQ(float_objective_ct->arguments[0].floats[arity - 1], -1.0);
for (int i = 0; i + 1 < arity; ++i) {
model->AddFloatingPointObjectiveTerm(
float_objective_ct->arguments[1].variables[i],
float_objective_ct->arguments[0].floats[i]);
}
model->SetFloatingPointObjectiveOffset(
-float_objective_ct->arguments[2].floats[0]);
model->ClearObjective();
float_objective_var->active = false;
float_objective_ct->active = false;
}
// Report presolve rules statistics.
if (!successful_rules_.empty()) {
for (const auto& rule : successful_rules_) {
if (rule.second == 1) {
SOLVER_LOG(logger_, " - rule '", rule.first, "' was applied 1 time");
} else {
SOLVER_LOG(logger_, " - rule '", rule.first, "' was applied ",
rule.second, " times");
}
}
}
}
// ----- Substitution support -----
void Presolver::AddVariableSubstitution(Variable* from, Variable* to) {
CHECK(from != nullptr);
CHECK(to != nullptr);
// Apply the substitutions, if any.
from = FindRepresentativeOfVar(from);
to = FindRepresentativeOfVar(to);
if (to->temporary) {
// Let's switch to keep a non temporary as representative.
Variable* tmp = to;
to = from;
from = tmp;
}
if (from != to) {
CHECK(to->Merge(from->name, from->domain, from->temporary));
from->active = false;
var_representative_map_[from] = to;
var_representative_vector_.push_back(from);
}
}
Variable* Presolver::FindRepresentativeOfVar(Variable* var) {
if (var == nullptr) return nullptr;
Variable* start_var = var;
// First loop: find the top parent.
for (;;) {
const auto& it = var_representative_map_.find(var);
Variable* parent = it == var_representative_map_.end() ? var : it->second;
if (parent == var) break;
var = parent;
}
// Second loop: attach all the path to the top parent.
while (start_var != var) {
Variable* const parent = var_representative_map_[start_var];
var_representative_map_[start_var] = var;
start_var = parent;
}
const auto& iter = var_representative_map_.find(var);
return iter == var_representative_map_.end() ? var : iter->second;
}
void Presolver::SubstituteEverywhere(Model* model) {
// Rewrite the constraints.
for (Constraint* const ct : model->constraints()) {
if (ct != nullptr && ct->active) {
for (int i = 0; i < ct->arguments.size(); ++i) {
Argument& argument = ct->arguments[i];
switch (argument.type) {
case Argument::VAR_REF:
case Argument::VAR_REF_ARRAY: {
for (int i = 0; i < argument.variables.size(); ++i) {
Variable* const old_var = argument.variables[i];
Variable* const new_var = FindRepresentativeOfVar(old_var);
if (new_var != old_var) {
argument.variables[i] = new_var;
}
}
break;
}
default: {
}
}
}
}
}
// Rewrite the search.
for (Annotation* const ann : model->mutable_search_annotations()) {
SubstituteAnnotation(ann);
}
// Rewrite the output.
for (SolutionOutputSpecs* const output : model->mutable_output()) {
output->variable = FindRepresentativeOfVar(output->variable);
for (int i = 0; i < output->flat_variables.size(); ++i) {
output->flat_variables[i] =
FindRepresentativeOfVar(output->flat_variables[i]);
}
}
// Do not forget to merge domain that could have evolved asynchronously
// during presolve.
for (const auto& iter : var_representative_map_) {
iter.second->domain.IntersectWithDomain(iter.first->domain);
}
// Change the objective variable.
Variable* const current_objective = model->objective();
if (current_objective == nullptr) return;
Variable* const new_objective = FindRepresentativeOfVar(current_objective);
if (new_objective != current_objective) {
model->SetObjective(new_objective);
}
}
void Presolver::SubstituteAnnotation(Annotation* ann) {
// TODO(user): Remove recursion.
switch (ann->type) {
case Annotation::ANNOTATION_LIST:
case Annotation::FUNCTION_CALL: {
for (int i = 0; i < ann->annotations.size(); ++i) {
SubstituteAnnotation(&ann->annotations[i]);
}
break;
}
case Annotation::VAR_REF:
case Annotation::VAR_REF_ARRAY: {
for (int i = 0; i < ann->variables.size(); ++i) {
ann->variables[i] = FindRepresentativeOfVar(ann->variables[i]);
}
break;
}
default: {
}
}
}
} // namespace fz
} // namespace operations_research

115
ortools/flatzinc/presolve.h
View File

@@ -1,115 +0,0 @@
// Copyright 2010-2024 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#ifndef OR_TOOLS_FLATZINC_PRESOLVE_H_
#define OR_TOOLS_FLATZINC_PRESOLVE_H_
#include <cstdint>
#include <functional>
#include <map>
#include <string>
#include <vector>
#include "absl/container/flat_hash_map.h"
#include "absl/container/flat_hash_set.h"
#include "absl/strings/match.h"
#include "ortools/base/hash.h"
#include "ortools/base/logging.h"
#include "ortools/base/types.h"
#include "ortools/flatzinc/model.h"
#include "ortools/util/logging.h"
namespace operations_research {
namespace fz {
// The Presolver "pre-solves" a Model by applying some iterative
// transformations to it, which may simplify and/or shrink the model.
//
// TODO(user): Error reporting of unfeasible models.
class Presolver {
public:
explicit Presolver(SolverLogger* logger) : logger_(logger) {}
// Recursively apply all the pre-solve rules to the model, until exhaustion.
// The reduced model will:
// - Have some unused variables.
// - Have some unused constraints (marked as inactive).
// - Have some modified constraints (for example, they will no longer
// refer to unused variables).
void Run(Model* model);
private:
// This struct stores the mapping of two index variables (of a 2D array; not
// included here) onto a single index variable (of the flattened 1D array).
// The original 2D array could be trimmed in the process; so we also need an
// offset.
// Eg. new_index_var = index_var1 * int_coeff + index_var2 + int_offset
struct Array2DIndexMapping {
Variable* variable1;
int64_t coefficient;
Variable* variable2;
int64_t offset;
Constraint* constraint;
Array2DIndexMapping()
: variable1(nullptr),
coefficient(0),
variable2(nullptr),
offset(0),
constraint(nullptr) {}
Array2DIndexMapping(Variable* v1, int64_t c, Variable* v2, int64_t o,
Constraint* ct)
: variable1(v1),
coefficient(c),
variable2(v2),
offset(o),
constraint(ct) {}
};
// Substitution support.
void SubstituteEverywhere(Model* model);
void SubstituteAnnotation(Annotation* ann);
// Presolve rules.
void PresolveBool2Int(Constraint* ct);
void PresolveInt2Float(Constraint* ct);
void PresolveStoreFlatteningMapping(Constraint* ct);
void PresolveSimplifyElement(Constraint* ct);
// Helpers.
void UpdateRuleStats(const std::string& rule_name) {
successful_rules_[rule_name]++;
}
// The presolver will discover some equivalence classes of variables [two
// variable are equivalent when replacing one by the other leads to the same
// logical model]. We will store them here, using a Union-find data structure.
// See http://en.wikipedia.org/wiki/Disjoint-set_data_structure.
// Note that the equivalence is directed. We prefer to replace all instances
// of 'from' with 'to', rather than the opposite.
void AddVariableSubstitution(Variable* from, Variable* to);
Variable* FindRepresentativeOfVar(Variable* var);
absl::flat_hash_map<const Variable*, Variable*> var_representative_map_;
std::vector<Variable*> var_representative_vector_;
// Stores array2d_index_map_[z] = a * x + y + b.
absl::flat_hash_map<const Variable*, Array2DIndexMapping> array2d_index_map_;
// Count applications of presolve rules. Use a sorted map for reporting
// purposes.
std::map<std::string, int> successful_rules_;
SolverLogger* logger_;
};
} // namespace fz
} // namespace operations_research
#endif // OR_TOOLS_FLATZINC_PRESOLVE_H_