diff --git a/src/constraint_solver/constraint_solver.h b/src/constraint_solver/constraint_solver.h index 5f07f9bbc8..f3505bb9de 100644 --- a/src/constraint_solver/constraint_solver.h +++ b/src/constraint_solver/constraint_solver.h @@ -1446,6 +1446,11 @@ class Solver { // Creates a demon from a closure. Demon* MakeCallbackDemon(Closure* const closure); + // Modulo constraint v % m == y + Constraint* MakeModuloConstraint(IntVar* const x, + int64 mod, + IntVar* const y); + // (l <= b <= u) Constraint* MakeBetweenCt(IntVar* const v, int64 l, int64 u); diff --git a/src/constraint_solver/constraints.cc b/src/constraint_solver/constraints.cc index ab98df6981..e78bced6d4 100644 --- a/src/constraint_solver/constraints.cc +++ b/src/constraint_solver/constraints.cc @@ -799,4 +799,67 @@ Constraint* Solver::MakePathCumul(const std::vector& nexts, cumuls.data(), cumuls.size(), transits.data())); } + +namespace { +class Modulo : public Constraint { + public: + Modulo(Solver* const solver, IntVar* const x, int64 mod, IntVar* const y) + : Constraint(solver), + x_(x), + mod_(mod), + y_(y), + x_iterator_(x_->MakeDomainIterator(true)), + y_iterator_(y_->MakeDomainIterator(true)) { + CHECK_GE(mod_, 0); + } + + virtual ~Modulo() {} + + virtual void Post() { + Demon* const demon = solver()->MakeConstraintInitialPropagateCallback(this); + x_->WhenDomain(demon); + y_->WhenDomain(demon); + } + + virtual void InitialPropagate() { + y_->SetRange(0, mod_ - 1); + to_remove_.clear(); + for (x_iterator_->Init(); x_iterator_->Ok(); x_iterator_->Next()) { + const int64 value = x_iterator_->Value(); + if (!y_->Contains(value % mod_)) { + to_remove_.push_back(value); + } + } + x_->RemoveValues(to_remove_); + to_remove_.clear(); + for (y_iterator_->Init(); y_iterator_->Ok(); y_iterator_->Next()) { + const int64 value = y_iterator_->Value(); + bool support = false; + for (int64 w = 0; w <= x_->Max() / mod_; ++w) { + if (x_->Contains(w * mod_ + value)) { + support = true; + break; + } + } + if (!support) { + to_remove_.push_back(value); + } + } + y_->RemoveValues(to_remove_); + } + + private: + IntVar* const x_; + IntVar* const y_; + const int64 mod_; + IntVarIterator* const x_iterator_; + IntVarIterator* const y_iterator_; + std::vector to_remove_; +}; +} // namespace +Constraint* Solver::MakeModuloConstraint(IntVar* const x, + int64 mod, + IntVar* const y) { + return RevAlloc(new Modulo(this, x, mod, y)); +} } // namespace operations_research diff --git a/src/flatzinc/registry.cc b/src/flatzinc/registry.cc index e31a8bd159..3872172f3c 100644 --- a/src/flatzinc/registry.cc +++ b/src/flatzinc/registry.cc @@ -541,10 +541,13 @@ void p_int_div(FlatZincModel* const model, CtSpec* const spec) { } void p_int_mod(FlatZincModel* const model, CtSpec* const spec) { - LOG(FATAL) << "int_mod(" << (spec->Arg(0)->DebugString()) << "," - << (spec->Arg(1)->DebugString()) << "," - << (spec->Arg(2)->DebugString()) - << ")::" << spec->annotations()->DebugString(); + Solver* const solver = model->solver(); + IntVar* const left = model->GetIntVar(spec->Arg(0)); + const int mod = spec->Arg(1)->getInt(); + IntVar* const target = model->GetIntVar(spec->Arg(2)); + Constraint* const ct = solver->MakeModuloConstraint(left, mod, target); + VLOG(1) << "Posted " << ct->DebugString(); + solver->AddConstraint(ct); } void p_int_min(FlatZincModel* const model, CtSpec* const spec) { diff --git a/src/flatzinc/spec.h b/src/flatzinc/spec.h index 9a960319a6..f96d3e77c5 100644 --- a/src/flatzinc/spec.h +++ b/src/flatzinc/spec.h @@ -142,13 +142,25 @@ class IntVarSpec : public VarSpec { } virtual string DebugString() const { - return StringPrintf( - "IntVarSpec(name = %s, id = %d, domain = %s)", - name.c_str(), - i, - (domain_.defined() ? - domain_.value()->DebugString().c_str() : - "no domain")); + if (alias) { + return StringPrintf( + "IntVarSpec(name = %s, alias to = %d)", + name.c_str(), + i); + } else if (assigned) { + return StringPrintf( + "IntVarSpec(name = %s, assigned to = %d)", + name.c_str(), + i); + } else { + return StringPrintf( + "IntVarSpec(name = %s, id = %d, domain = %s)", + name.c_str(), + i, + (domain_.defined() ? + domain_.value()->DebugString().c_str() : + "no domain")); + } } AST::SetLit* Domain() const {