diff --git a/examples/flatzinc/another_kind_of_magic_square.fzn b/examples/flatzinc/another_kind_of_magic_square.fzn index b99c38f9c3..e8173474a9 100644 --- a/examples/flatzinc/another_kind_of_magic_square.fzn +++ b/examples/flatzinc/another_kind_of_magic_square.fzn @@ -1,6 +1,10 @@ predicate all_different_int(array [int] of var int: x); predicate count(array [int] of var int: x, var int: y, var int: c); +predicate fixed_cumulative(array [int] of var int: s, array [int] of int: d, array [int] of int: r, int: b); predicate global_cardinality(array [int] of var int: x, array [int] of int: cover, array [int] of var int: counts); +predicate maximum_int(var int: m, array [int] of var int: x); +predicate minimum_int(var int: m, array [int] of var int: x); +predicate sort(array [int] of var int: x, array [int] of var int: y); predicate table_bool(array [int] of var bool: x, array [int, int] of bool: t); predicate table_int(array [int] of var int: x, array [int, int] of int: t); var 4..36: INT____00001 :: is_defined_var :: var_is_introduced; diff --git a/src/constraint_solver/constraint_solver.h b/src/constraint_solver/constraint_solver.h index 3c51028267..727f537511 100644 --- a/src/constraint_solver/constraint_solver.h +++ b/src/constraint_solver/constraint_solver.h @@ -1829,6 +1829,34 @@ class Solver { int64 capacity, const string& name); + // This constraint forces that, for any integer t, the sum of the demands + // corresponding to an interval containing t does not exceed the given + // capacity. + // + // Intervals and demands should be vectors of equal size. + // + // Demands should only contain non-negative values. Zero values are supported, + // and the corresponding intervals are filtered out, as they neither impact + // nor are impacted by this constraint. + Constraint* MakeCumulative(const std::vector& intervals, + const std::vector& demands, + IntVar* const capacity, + const string& name); + + // This constraint forces that, for any integer t, the sum of the demands + // corresponding to an interval containing t does not exceed the given + // capacity. + // + // Intervals and demands should be vectors of equal size. + // + // Demands should only contain non-negative values. Zero values are supported, + // and the corresponding intervals are filtered out, as they neither impact + // nor are impacted by this constraint. + Constraint* MakeCumulative(const std::vector& intervals, + const std::vector& demands, + IntVar* const capacity, + const string& name); + // ----- Assignments ----- // This method creates an empty assignment. diff --git a/src/constraint_solver/constraints.cc b/src/constraint_solver/constraints.cc index 0ef1e2fccc..118c09c99b 100644 --- a/src/constraint_solver/constraints.cc +++ b/src/constraint_solver/constraints.cc @@ -889,15 +889,17 @@ class VariableModulo : public Constraint { virtual void Post() { Solver* const s = solver(); - IntVar* const div = s->MakeDiv(x_, mod_)->Var(); - s->AddConstraint(s->MakeLess(y_, mod_)); - s->AddConstraint(s->MakeGreaterOrEqual(y_, Zero())); - s->AddConstraint(s->MakeGreater(mod_, Zero())); - s->AddConstraint(s->MakeEquality(y_, s->MakeProd(div, mod_)->Var())); + IntVar* const d = s->MakeIntVar(std::min(x_->Min(), -x_->Max()), + std::max(x_->Max(), -x_->Min())); + s->AddConstraint(s->MakeEquality(x_, s->MakeSum(s->MakeProd(mod_, d), y_)->Var())); + s->AddConstraint(s->MakeGreater(y_, s->MakeOpposite(s->MakeAbs(mod_))->Var())); + s->AddConstraint(s->MakeLess(y_, s->MakeAbs(mod_)->Var())); + s->AddConstraint(s->MakeGreaterOrEqual(d, s->MakeMin(x_, s->MakeOpposite(x_))->Var())); + s->AddConstraint(s->MakeLessOrEqual(d, s->MakeMax(x_, s->MakeOpposite(x_))->Var())); } virtual void InitialPropagate() { - mod_->SetMin(1); + mod_->RemoveValue(0); } private: diff --git a/src/constraint_solver/resource.cc b/src/constraint_solver/resource.cc index a77edb000d..06552b3f14 100644 --- a/src/constraint_solver/resource.cc +++ b/src/constraint_solver/resource.cc @@ -2189,4 +2189,110 @@ Constraint* Solver::MakeCumulative(const std::vector& intervals, capacity, name)); } + +Constraint* Solver::MakeCumulative(const std::vector& intervals, + const std::vector& demands, + IntVar* const capacity, + const string& name) { + CHECK_EQ(intervals.size(), demands.size()); + for (int i = 0; i < intervals.size(); ++i) { + CHECK_GE(demands[i], 0); + } + if (capacity->Bound()) { + return MakeCumulative(intervals, demands, capacity->Min(), name); + } + std::vector a_intervals; + std::vector a_demands; + int64 horizon_min = kint64max; + int64 horizon_max = kint64min; + for (int i = 0; i < demands.size(); ++i) { + if (demands[i] > 0) { + a_intervals.push_back(intervals[i]); + a_demands.push_back(demands[i]); + horizon_max = std::max(horizon_max, intervals[i]->EndMax()); + horizon_min = std::min(horizon_min, intervals[i]->StartMin()); + } + } + const int64 total_duration = horizon_max = horizon_max + 1; + const int64 capacity_min = std::max(capacity->Min(), 0LL); + const int64 capacity_max = capacity->Max(); + const int64 delta_capacity = capacity_max - capacity_min; + std::vector o_vars; // Optional variables. + std::vector o_coefs; + for (int64 mult = 1; mult <= delta_capacity; mult *= 2) { + const string name = + StringPrintf("VariableCapacity<%" GG_LL_FORMAT "d>", mult); + IntervalVar* const var = MakeFixedDurationIntervalVar(horizon_min, + horizon_min, + total_duration, + true, + name); + a_intervals.push_back(var); + a_demands.push_back(mult); + o_vars.push_back(var->PerformedExpr()->Var()); + o_coefs.push_back(mult); + } + o_vars.push_back(capacity); + o_coefs.push_back(1); + AddConstraint(MakeScalProdEquality(o_vars, o_coefs, capacity_max)); + return RevAlloc(new CumulativeConstraint(this, + a_intervals.data(), + a_demands.data(), + a_intervals.size(), + capacity_max, + name)); +} + +Constraint* Solver::MakeCumulative(const std::vector& intervals, + const std::vector& demands, + IntVar* const capacity, + const string& name) { + CHECK_EQ(intervals.size(), demands.size()); + for (int i = 0; i < intervals.size(); ++i) { + CHECK_GE(demands[i], 0); + } + if (capacity->Bound()) { + return MakeCumulative(intervals, demands, capacity->Min(), name); + } + std::vector a_intervals; + std::vector a_demands; + int64 horizon_min = kint64max; + int64 horizon_max = kint64min; + for (int i = 0; i < demands.size(); ++i) { + if (demands[i] > 0) { + a_intervals.push_back(intervals[i]); + a_demands.push_back(demands[i]); + horizon_max = std::max(horizon_max, intervals[i]->EndMax()); + horizon_min = std::min(horizon_min, intervals[i]->StartMin()); + } + } + const int64 total_duration = horizon_max = horizon_max + 1; + const int64 capacity_min = std::max(capacity->Min(), 0LL); + const int64 capacity_max = capacity->Max(); + const int64 delta_capacity = capacity_max - capacity_min; + std::vector o_vars; // Optional variables. + std::vector o_coefs; + for (int64 mult = 1; mult <= delta_capacity; mult *= 2) { + const string name = + StringPrintf("VariableCapacity<%" GG_LL_FORMAT "d>", mult); + IntervalVar* const var = MakeFixedDurationIntervalVar(horizon_min, + horizon_min, + total_duration, + true, + name); + a_intervals.push_back(var); + a_demands.push_back(mult); + o_vars.push_back(var->PerformedExpr()->Var()); + o_coefs.push_back(mult); + } + o_vars.push_back(capacity); + o_coefs.push_back(1); + AddConstraint(MakeScalProdEquality(o_vars, o_coefs, capacity_max)); + return RevAlloc(new CumulativeConstraint(this, + a_intervals.data(), + a_demands.data(), + a_intervals.size(), + capacity_max, + name)); +} } // namespace operations_research diff --git a/src/flatzinc/mznlib/cumulative.mzn b/src/flatzinc/mznlib/cumulative.mzn index 343e752600..2289a38427 100644 --- a/src/flatzinc/mznlib/cumulative.mzn +++ b/src/flatzinc/mznlib/cumulative.mzn @@ -10,6 +10,11 @@ predicate fixed_cumulative(array[int] of var int: s, array[int] of int: r, int: b); +predicate var_cumulative(array[int] of var int: s, + array[int] of int: d, + array[int] of int: r, + var int: b); + predicate variable_cumulative(array[int] of var int: s, array[int] of var int: d, array[int] of var int: r, @@ -40,6 +45,12 @@ predicate cumulative(array[int] of var int: s, int: b) = fixed_cumulative(s, d, r, b); +predicate cumulative(array[int] of var int: s, + array[int] of int: d, + array[int] of int: r, + var int: b) = + var_cumulative(s, d, r, b); + predicate cumulative(array[int] of var int: s, array[int] of var int: d, array[int] of var int: r, diff --git a/src/flatzinc/registry.cc b/src/flatzinc/registry.cc index 1e01612897..0a137f26f7 100644 --- a/src/flatzinc/registry.cc +++ b/src/flatzinc/registry.cc @@ -1167,6 +1167,40 @@ void p_fixed_cumulative(FlatZincModel* const model, CtSpec* const spec) { solver->AddConstraint(ct); } +void p_var_cumulative(FlatZincModel* const model, CtSpec* const spec) { + Solver* const solver = model->solver(); + AST::Array* const array_variables = spec->Arg(0)->getArray(); + const int size = array_variables->a.size(); + std::vector start_variables(size); + for (int i = 0; i < size; ++i) { + start_variables[i] = model->GetIntVar(array_variables->a[i]); + } + AST::Array* const array_durations = spec->Arg(1)->getArray(); + const int dsize = array_durations->a.size(); + std::vector durations(dsize); + for (int i = 0; i < dsize; ++i) { + durations[i] = array_durations->a[i]->getInt(); + } + AST::Array* const array_usages = spec->Arg(2)->getArray(); + const int usize = array_usages->a.size(); + std::vector usages(usize); + for (int i = 0; i < usize; ++i) { + usages[i] = array_usages->a[i]->getInt(); + } + std::vector intervals; + solver->MakeFixedDurationIntervalVarArray(start_variables, + durations, + "", + &intervals); + IntVar* const capacity = model->GetIntVar(spec->Arg(3)); + Constraint* const ct = solver->MakeCumulative(intervals, + usages, + capacity, + ""); + VLOG(1) << "Posted " << ct->DebugString(); + solver->AddConstraint(ct); +} + class IntBuilder { public: IntBuilder(void) { @@ -1244,6 +1278,7 @@ class IntBuilder { global_model_builder.Register("minimum_int", &p_minimum_int); global_model_builder.Register("sort", &p_sort); global_model_builder.Register("fixed_cumulative", &p_fixed_cumulative); + global_model_builder.Register("var_cumulative", &p_var_cumulative); } }; IntBuilder __int_Builder;