allow minimal solve on flatzinc

ortools/flatzinc/cp_model_fz_solver.cc

@@ -139,6 +139,9 @@ std::vector<int> CpModelProtoWithMapping::LookupVars(
     for (int64 value : argument.values) {
       result.push_back(LookupConstant(value));
     }
+
+  } else if (argument.type == fz::Argument::INT_VALUE) {
+    result.push_back(LookupConstant(argument.Value()));
   } else {
     CHECK_EQ(argument.type, fz::Argument::INT_VAR_REF_ARRAY);
     for (fz::IntegerVariable* var : argument.variables) {
@@ -256,9 +259,32 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
       arg->add_literals(FalseLiteral(var));
     }
   } else if (fz_ct.type == "bool_xor") {
-    auto* arg = ct->mutable_bool_xor();
-    arg->add_literals(TrueLiteral(LookupVar(fz_ct.arguments[0])));
-    arg->add_literals(TrueLiteral(LookupVar(fz_ct.arguments[1])));
+    // This is not the same semantics as the array_bool_xor as this constraint
+    // is actually a fully reified xor(a, b) <==> x.
+    const int a = LookupVar(fz_ct.arguments[0]);
+    const int b = LookupVar(fz_ct.arguments[1]);
+    const int x = LookupVar(fz_ct.arguments[2]);
+
+    // not(x) => a == b
+    ct->add_enforcement_literal(NegatedRef(x));
+    auto* const refute = ct->mutable_linear();
+    refute->add_vars(a);
+    refute->add_coeffs(1);
+    refute->add_vars(b);
+    refute->add_coeffs(-1);
+    refute->add_domain(0);
+    refute->add_domain(0);
+
+    // x => a + b == 1
+    auto* ct2 = proto.add_constraints();
+    ct2->add_enforcement_literal(x);
+    auto* const enforce = ct2->mutable_linear();
+    enforce->add_vars(a);
+    enforce->add_coeffs(1);
+    enforce->add_vars(b);
+    enforce->add_coeffs(1);
+    enforce->add_domain(1);
+    enforce->add_domain(1);
   } else if (fz_ct.type == "array_bool_or") {
     auto* arg = ct->mutable_bool_or();
     for (const int var : LookupVars(fz_ct.arguments[0])) {
@@ -428,7 +454,8 @@ 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::INT_VAR_REF) {
+    if (fz_ct.arguments[0].type == fz::Argument::INT_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]));

ortools/flatzinc/fz.cc

@@ -150,6 +150,12 @@ Model ParseFlatzincModel(const std::string& input, bool input_is_filename) {
     timer.Start();
     presolve.Run(&model);
     FZLOG << "  - done in " << timer.GetInMs() << " ms" << FZENDL;
+  } else {
+    FZLOG << "Presolve model using minimal rules" << FZENDL;
+    timer.Reset();
+    timer.Start();
+    presolve.RunMinimal(&model);
+    FZLOG << "  - done in " << timer.GetInMs() << " ms" << FZENDL;
   }
 
   // Print statistics.

ortools/flatzinc/presolve.cc

@@ -3644,6 +3644,50 @@ bool Presolver::RegroupDifferent(Model* model) {
   return killed > 0;
 }
 
+bool Presolver::RunMinimal(Model* model) {
+  auto constraint = [model](int index) { return model->constraints()[index]; };
+
+  // Rebuild var_constraint map if empty.
+  if (var_to_constraint_indices_.empty()) {
+    for (int i = 0; i < model->constraints().size(); ++i) {
+      AddConstraintToMapping(i, constraint(i));
+    }
+  }
+
+  bool changed = false;
+  // Let's presolve the bool2int predicates first.
+  for (int index = 0; index < model->constraints().size(); ++index) {
+    Constraint* const ct = constraint(index);
+    if (ct->active && ct->type == "bool2int") {
+      std::string log;
+      ApplyRule(index, ct, "PresolveBool2Int",
+                [this](Constraint* ct, std::string* log) {
+                  return PresolveBool2Int(ct, log);
+                });
+      changed = true;
+    }
+  }
+  if (!var_representative_map_.empty()) {
+    // Some new substitutions were introduced. Let's process them.
+    SubstituteEverywhere(model);
+    var_representative_map_.clear();
+    var_representative_vector_.clear();
+  }
+
+  // Report presolve rules statistics.
+  if (!successful_rules_.empty()) {
+    for (const auto& rule : successful_rules_) {
+      if (rule.second == 1) {
+        FZLOG << "  - rule " << rule.first << " was applied 1 time" << FZENDL;
+      } else {
+        FZLOG << "  - rule " << rule.first << " was applied " << rule.second
+              << " times" << FZENDL;
+      }
+    }
+  }
+  return changed;
+}
+
 bool Presolver::Run(Model* model) {
   // Check the validity of variable domains.
   for (const IntegerVariable* var : model->variables()) {

ortools/flatzinc/presolve.h

@@ -48,6 +48,11 @@ class Presolver {
   // TODO(user): Returns the number of rules applied instead.
   bool Run(Model* model);
 
+  // Minimal version of the presolve.
+  // TODO(user): Currently, without this, the solver fails on a series of
+  // problems like hrc_exp1-1-945_sat.fzn. To investigate.
+  bool RunMinimal(Model* model);
+
   // Cleans the model for the CP solver.
   // In particular, it knows if we use a sat solver inside the CP
   // solver. In that case, for Boolean constraints, it remove the link