add flatzinc support for disjunctive and disjunctive_strict

ortools/flatzinc/checker.cc

@@ -360,11 +360,41 @@ bool CheckDiffnNonStrictK(const Constraint& ct,
 
 bool CheckDisjunctive(const Constraint& ct,
                       const std::function<int64_t(Variable*)>& evaluator) {
+  // TODO(user): Improve complexity for large size.
+  const int size = Size(ct.arguments[0]);
+  CHECK_EQ(size, Size(ct.arguments[1]));
+  absl::flat_hash_map<int64_t, int64_t> usage;
+  for (int i = 0; i < size; ++i) {
+    const int64_t start = EvalAt(ct.arguments[0], i, evaluator);
+    const int64_t duration = EvalAt(ct.arguments[1], i, evaluator);
+    for (int64_t t = start; t < start + duration; ++t) {
+      ++usage[t];
+      if (usage[t] > 1) {
+        return false;
+      }
+    }
+  }
   return true;
 }
 
 bool CheckDisjunctiveStrict(
     const Constraint& ct, const std::function<int64_t(Variable*)>& evaluator) {
+  // TODO(user): Improve complexity for large size.
+  const int size = Size(ct.arguments[0]);
+  CHECK_EQ(size, Size(ct.arguments[1]));
+  absl::flat_hash_map<int64_t, int64_t> usage;
+  for (int i = 0; i + 1 < size; ++i) {
+    const int64_t start_i = EvalAt(ct.arguments[0], i, evaluator);
+    const int64_t duration_i = EvalAt(ct.arguments[1], i, evaluator);
+    for (int j = i + 1; j < size; ++j) {
+      const int64_t start_j = EvalAt(ct.arguments[0], j, evaluator);
+      const int64_t duration_j = EvalAt(ct.arguments[1], j, evaluator);
+      if (start_i + duration_i <= start_j || start_j + duration_j <= start_i) {
+        continue;
+      }
+      return false;
+    }
+  }
   return true;
 }
 
@@ -1157,8 +1187,8 @@ CallMap CreateCallMap() {
   m["diffn_k_with_sizes"] = CheckDiffnK;
   m["fzn_diffn_nonstrict"] = CheckDiffnNonStrict;
   m["diffn_nonstrict_k_with_sizes"] = CheckDiffnNonStrictK;
-  m["disjunctive"] = CheckDisjunctive;
-  m["disjunctive_strict"] = CheckDisjunctiveStrict;
+  m["fzn_disjunctive"] = CheckDisjunctive;
+  m["fzn_disjunctive_strict"] = CheckDisjunctiveStrict;
   m["false_constraint"] = CheckFalseConstraint;
   m["global_cardinality"] = CheckGlobalCardinality;
   m["global_cardinality_closed"] = CheckGlobalCardinalityClosed;

ortools/flatzinc/cp_model_fz_solver.cc

@@ -844,6 +844,28 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
         arg->add_f_inverse(LookupConstant(i - num_variables));
       }
     }
+  } else if (fz_ct.type == "fzn_disjunctive") {
+    const std::vector<int> starts = LookupVars(fz_ct.arguments[0]);
+    const std::vector<VarOrValue> sizes =
+        LookupVarsOrValues(fz_ct.arguments[1]);
+
+    auto* arg = ct->mutable_cumulative();
+    arg->mutable_capacity()->set_offset(1);
+    for (int i = 0; i < starts.size(); ++i) {
+      arg->add_intervals(
+          GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
+      arg->add_demands()->set_offset(1);
+    }
+  } else if (fz_ct.type == "fzn_disjunctive_strict") {
+    const std::vector<int> starts = LookupVars(fz_ct.arguments[0]);
+    const std::vector<VarOrValue> sizes =
+        LookupVarsOrValues(fz_ct.arguments[1]);
+
+    auto* arg = ct->mutable_no_overlap();
+    for (int i = 0; i < starts.size(); ++i) {
+      arg->add_intervals(
+          GetOrCreateOptionalInterval(starts[i], sizes[i], kNoVar));
+    }
   } else if (fz_ct.type == "fzn_cumulative") {
     const std::vector<int> starts = LookupVars(fz_ct.arguments[0]);
     const std::vector<VarOrValue> sizes =
@@ -1313,6 +1335,7 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
             m.proto.search_strategy().empty() ? "quick_restart" : "fixed");
         m.parameters.add_subsolvers("core_or_no_lp"),
             m.parameters.add_subsolvers("max_lp");
+
       } else {
         m.parameters.add_subsolvers("default_lp");
         m.parameters.add_subsolvers(

ortools/flatzinc/mznlib/fzn_disjunctive.mzn

@@ -0,0 +1,9 @@
+%-----------------------------------------------------------------------------%
+% Requires that a set of tasks given by start times 's', durations 'd', and
+% resource requirements 'r', never require more than a global resource bound
+% 'b' at any one time.
+% Assumptions:
+% - forall i, d[i] >= 0 and r[i] >= 0
+%-----------------------------------------------------------------------------%
+predicate fzn_disjunctive(array[int] of var int: s,
+                          array[int] of var int: d);

ortools/flatzinc/mznlib/fzn_disjunctive_strict.mzn

@@ -0,0 +1,9 @@
+%-----------------------------------------------------------------------------%
+% Requires that a set of tasks given by start times 's', durations 'd', and
+% resource requirements 'r', never require more than a global resource bound
+% 'b' at any one time.
+% Assumptions:
+% - forall i, d[i] >= 0 and r[i] >= 0
+%-----------------------------------------------------------------------------%
+predicate fzn_disjunctive_strict(array[int] of var int: s,
+                                 array[int] of var int: d);