806 lines
26 KiB
C++
806 lines
26 KiB
C++
// Copyright 2010-2022 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.
|
|
|
|
//
|
|
// Range constraints
|
|
|
|
#include <stddef.h>
|
|
|
|
#include <string>
|
|
|
|
#include "absl/strings/str_format.h"
|
|
#include "ortools/base/logging.h"
|
|
#include "ortools/constraint_solver/constraint_solver.h"
|
|
#include "ortools/constraint_solver/constraint_solveri.h"
|
|
|
|
namespace operations_research {
|
|
|
|
//-----------------------------------------------------------------------------
|
|
// RangeEquality
|
|
|
|
namespace {
|
|
class RangeEquality : public Constraint {
|
|
public:
|
|
RangeEquality(Solver* const s, IntExpr* const l, IntExpr* const r)
|
|
: Constraint(s), left_(l), right_(r) {}
|
|
|
|
~RangeEquality() override {}
|
|
|
|
void Post() override {
|
|
Demon* const d = solver()->MakeConstraintInitialPropagateCallback(this);
|
|
left_->WhenRange(d);
|
|
right_->WhenRange(d);
|
|
}
|
|
|
|
void InitialPropagate() override {
|
|
left_->SetRange(right_->Min(), right_->Max());
|
|
right_->SetRange(left_->Min(), left_->Max());
|
|
}
|
|
|
|
std::string DebugString() const override {
|
|
return left_->DebugString() + " == " + right_->DebugString();
|
|
}
|
|
|
|
IntVar* Var() override { return solver()->MakeIsEqualVar(left_, right_); }
|
|
|
|
void Accept(ModelVisitor* const visitor) const override {
|
|
visitor->BeginVisitConstraint(ModelVisitor::kEquality, this);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kLeftArgument, left_);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kRightArgument,
|
|
right_);
|
|
visitor->EndVisitConstraint(ModelVisitor::kEquality, this);
|
|
}
|
|
|
|
private:
|
|
IntExpr* const left_;
|
|
IntExpr* const right_;
|
|
};
|
|
|
|
//-----------------------------------------------------------------------------
|
|
// RangeLessOrEqual
|
|
|
|
class RangeLessOrEqual : public Constraint {
|
|
public:
|
|
RangeLessOrEqual(Solver* const s, IntExpr* const l, IntExpr* const r);
|
|
~RangeLessOrEqual() override {}
|
|
void Post() override;
|
|
void InitialPropagate() override;
|
|
std::string DebugString() const override;
|
|
IntVar* Var() override {
|
|
return solver()->MakeIsLessOrEqualVar(left_, right_);
|
|
}
|
|
void Accept(ModelVisitor* const visitor) const override {
|
|
visitor->BeginVisitConstraint(ModelVisitor::kLessOrEqual, this);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kLeftArgument, left_);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kRightArgument,
|
|
right_);
|
|
visitor->EndVisitConstraint(ModelVisitor::kLessOrEqual, this);
|
|
}
|
|
|
|
private:
|
|
IntExpr* const left_;
|
|
IntExpr* const right_;
|
|
Demon* demon_;
|
|
};
|
|
|
|
RangeLessOrEqual::RangeLessOrEqual(Solver* const s, IntExpr* const l,
|
|
IntExpr* const r)
|
|
: Constraint(s), left_(l), right_(r), demon_(nullptr) {}
|
|
|
|
void RangeLessOrEqual::Post() {
|
|
demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
|
|
left_->WhenRange(demon_);
|
|
right_->WhenRange(demon_);
|
|
}
|
|
|
|
void RangeLessOrEqual::InitialPropagate() {
|
|
left_->SetMax(right_->Max());
|
|
right_->SetMin(left_->Min());
|
|
if (left_->Max() <= right_->Min()) {
|
|
demon_->inhibit(solver());
|
|
}
|
|
}
|
|
|
|
std::string RangeLessOrEqual::DebugString() const {
|
|
return left_->DebugString() + " <= " + right_->DebugString();
|
|
}
|
|
|
|
//-----------------------------------------------------------------------------
|
|
// RangeLess
|
|
|
|
class RangeLess : public Constraint {
|
|
public:
|
|
RangeLess(Solver* const s, IntExpr* const l, IntExpr* const r);
|
|
~RangeLess() override {}
|
|
void Post() override;
|
|
void InitialPropagate() override;
|
|
std::string DebugString() const override;
|
|
IntVar* Var() override { return solver()->MakeIsLessVar(left_, right_); }
|
|
void Accept(ModelVisitor* const visitor) const override {
|
|
visitor->BeginVisitConstraint(ModelVisitor::kLess, this);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kLeftArgument, left_);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kRightArgument,
|
|
right_);
|
|
visitor->EndVisitConstraint(ModelVisitor::kLess, this);
|
|
}
|
|
|
|
private:
|
|
IntExpr* const left_;
|
|
IntExpr* const right_;
|
|
Demon* demon_;
|
|
};
|
|
|
|
RangeLess::RangeLess(Solver* const s, IntExpr* const l, IntExpr* const r)
|
|
: Constraint(s), left_(l), right_(r), demon_(nullptr) {}
|
|
|
|
void RangeLess::Post() {
|
|
demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
|
|
left_->WhenRange(demon_);
|
|
right_->WhenRange(demon_);
|
|
}
|
|
|
|
void RangeLess::InitialPropagate() {
|
|
left_->SetMax(right_->Max() - 1);
|
|
right_->SetMin(left_->Min() + 1);
|
|
if (left_->Max() < right_->Min()) {
|
|
demon_->inhibit(solver());
|
|
}
|
|
}
|
|
|
|
std::string RangeLess::DebugString() const {
|
|
return left_->DebugString() + " < " + right_->DebugString();
|
|
}
|
|
|
|
//-----------------------------------------------------------------------------
|
|
// DiffVar
|
|
|
|
class DiffVar : public Constraint {
|
|
public:
|
|
DiffVar(Solver* const s, IntVar* const l, IntVar* const r);
|
|
~DiffVar() override {}
|
|
void Post() override;
|
|
void InitialPropagate() override;
|
|
std::string DebugString() const override;
|
|
IntVar* Var() override { return solver()->MakeIsDifferentVar(left_, right_); }
|
|
void LeftBound();
|
|
void RightBound();
|
|
|
|
void Accept(ModelVisitor* const visitor) const override {
|
|
visitor->BeginVisitConstraint(ModelVisitor::kNonEqual, this);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kLeftArgument, left_);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kRightArgument,
|
|
right_);
|
|
visitor->EndVisitConstraint(ModelVisitor::kNonEqual, this);
|
|
}
|
|
|
|
private:
|
|
IntVar* const left_;
|
|
IntVar* const right_;
|
|
};
|
|
|
|
DiffVar::DiffVar(Solver* const s, IntVar* const l, IntVar* const r)
|
|
: Constraint(s), left_(l), right_(r) {}
|
|
|
|
void DiffVar::Post() {
|
|
Demon* const left_demon =
|
|
MakeConstraintDemon0(solver(), this, &DiffVar::LeftBound, "LeftBound");
|
|
Demon* const right_demon =
|
|
MakeConstraintDemon0(solver(), this, &DiffVar::RightBound, "RightBound");
|
|
left_->WhenBound(left_demon);
|
|
right_->WhenBound(right_demon);
|
|
// TODO(user) : improve me, separated demons, actually to test
|
|
}
|
|
|
|
void DiffVar::LeftBound() {
|
|
if (right_->Size() < 0xFFFFFF) {
|
|
right_->RemoveValue(left_->Min()); // we use min instead of value
|
|
} else {
|
|
solver()->AddConstraint(solver()->MakeNonEquality(right_, left_->Min()));
|
|
}
|
|
}
|
|
|
|
void DiffVar::RightBound() {
|
|
if (left_->Size() < 0xFFFFFF) {
|
|
left_->RemoveValue(right_->Min()); // see above
|
|
} else {
|
|
solver()->AddConstraint(solver()->MakeNonEquality(left_, right_->Min()));
|
|
}
|
|
}
|
|
|
|
void DiffVar::InitialPropagate() {
|
|
if (left_->Bound()) {
|
|
LeftBound();
|
|
}
|
|
if (right_->Bound()) {
|
|
RightBound();
|
|
}
|
|
}
|
|
|
|
std::string DiffVar::DebugString() const {
|
|
return left_->DebugString() + " != " + right_->DebugString();
|
|
}
|
|
|
|
// --------------------- Reified API -------------------
|
|
// A reified API transforms an constraint into a status variables.
|
|
// For example x == y is transformed into IsEqual(x, y, b) where
|
|
// b is a boolean variable which is true if and only if x is equal to b.
|
|
|
|
// IsEqualCt
|
|
|
|
class IsEqualCt : public CastConstraint {
|
|
public:
|
|
IsEqualCt(Solver* const s, IntExpr* const l, IntExpr* const r,
|
|
IntVar* const b)
|
|
: CastConstraint(s, b), left_(l), right_(r), range_demon_(nullptr) {}
|
|
|
|
~IsEqualCt() override {}
|
|
|
|
void Post() override {
|
|
range_demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
|
|
left_->WhenRange(range_demon_);
|
|
right_->WhenRange(range_demon_);
|
|
Demon* const target_demon = MakeConstraintDemon0(
|
|
solver(), this, &IsEqualCt::PropagateTarget, "PropagateTarget");
|
|
target_var_->WhenBound(target_demon);
|
|
}
|
|
|
|
void InitialPropagate() override {
|
|
if (target_var_->Bound()) {
|
|
PropagateTarget();
|
|
return;
|
|
}
|
|
if (left_->Min() > right_->Max() || left_->Max() < right_->Min()) {
|
|
target_var_->SetValue(0);
|
|
range_demon_->inhibit(solver());
|
|
} else if (left_->Bound()) {
|
|
if (right_->Bound()) {
|
|
target_var_->SetValue(left_->Min() == right_->Min());
|
|
} else if (right_->IsVar() && !right_->Var()->Contains(left_->Min())) {
|
|
range_demon_->inhibit(solver());
|
|
target_var_->SetValue(0);
|
|
}
|
|
} else if (right_->Bound() && left_->IsVar() &&
|
|
!left_->Var()->Contains(right_->Min())) {
|
|
range_demon_->inhibit(solver());
|
|
target_var_->SetValue(0);
|
|
}
|
|
}
|
|
|
|
void PropagateTarget() {
|
|
if (target_var_->Min() == 0) {
|
|
if (left_->Bound()) {
|
|
range_demon_->inhibit(solver());
|
|
if (right_->IsVar()) {
|
|
right_->Var()->RemoveValue(left_->Min());
|
|
} else {
|
|
solver()->AddConstraint(
|
|
solver()->MakeNonEquality(right_, left_->Min()));
|
|
}
|
|
} else if (right_->Bound()) {
|
|
range_demon_->inhibit(solver());
|
|
if (left_->IsVar()) {
|
|
left_->Var()->RemoveValue(right_->Min());
|
|
} else {
|
|
solver()->AddConstraint(
|
|
solver()->MakeNonEquality(left_, right_->Min()));
|
|
}
|
|
}
|
|
} else { // Var is true.
|
|
left_->SetRange(right_->Min(), right_->Max());
|
|
right_->SetRange(left_->Min(), left_->Max());
|
|
}
|
|
}
|
|
|
|
std::string DebugString() const override {
|
|
return absl::StrFormat("IsEqualCt(%s, %s, %s)", left_->DebugString(),
|
|
right_->DebugString(), target_var_->DebugString());
|
|
}
|
|
|
|
void Accept(ModelVisitor* const visitor) const override {
|
|
visitor->BeginVisitConstraint(ModelVisitor::kIsEqual, this);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kLeftArgument, left_);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kRightArgument,
|
|
right_);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,
|
|
target_var_);
|
|
visitor->EndVisitConstraint(ModelVisitor::kIsEqual, this);
|
|
}
|
|
|
|
private:
|
|
IntExpr* const left_;
|
|
IntExpr* const right_;
|
|
Demon* range_demon_;
|
|
};
|
|
|
|
// IsDifferentCt
|
|
|
|
class IsDifferentCt : public CastConstraint {
|
|
public:
|
|
IsDifferentCt(Solver* const s, IntExpr* const l, IntExpr* const r,
|
|
IntVar* const b)
|
|
: CastConstraint(s, b), left_(l), right_(r), range_demon_(nullptr) {}
|
|
|
|
~IsDifferentCt() override {}
|
|
|
|
void Post() override {
|
|
range_demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
|
|
left_->WhenRange(range_demon_);
|
|
right_->WhenRange(range_demon_);
|
|
Demon* const target_demon = MakeConstraintDemon0(
|
|
solver(), this, &IsDifferentCt::PropagateTarget, "PropagateTarget");
|
|
target_var_->WhenBound(target_demon);
|
|
}
|
|
|
|
void InitialPropagate() override {
|
|
if (target_var_->Bound()) {
|
|
PropagateTarget();
|
|
return;
|
|
}
|
|
if (left_->Min() > right_->Max() || left_->Max() < right_->Min()) {
|
|
target_var_->SetValue(1);
|
|
range_demon_->inhibit(solver());
|
|
} else if (left_->Bound()) {
|
|
if (right_->Bound()) {
|
|
target_var_->SetValue(left_->Min() != right_->Min());
|
|
} else if (right_->IsVar() && !right_->Var()->Contains(left_->Min())) {
|
|
range_demon_->inhibit(solver());
|
|
target_var_->SetValue(1);
|
|
}
|
|
} else if (right_->Bound() && left_->IsVar() &&
|
|
!left_->Var()->Contains(right_->Min())) {
|
|
range_demon_->inhibit(solver());
|
|
target_var_->SetValue(1);
|
|
}
|
|
}
|
|
|
|
void PropagateTarget() {
|
|
if (target_var_->Min() == 0) {
|
|
left_->SetRange(right_->Min(), right_->Max());
|
|
right_->SetRange(left_->Min(), left_->Max());
|
|
} else { // Var is true.
|
|
if (left_->Bound()) {
|
|
range_demon_->inhibit(solver());
|
|
solver()->AddConstraint(
|
|
solver()->MakeNonEquality(right_, left_->Min()));
|
|
} else if (right_->Bound()) {
|
|
range_demon_->inhibit(solver());
|
|
solver()->AddConstraint(
|
|
solver()->MakeNonEquality(left_, right_->Min()));
|
|
}
|
|
}
|
|
}
|
|
|
|
std::string DebugString() const override {
|
|
return absl::StrFormat("IsDifferentCt(%s, %s, %s)", left_->DebugString(),
|
|
right_->DebugString(), target_var_->DebugString());
|
|
}
|
|
|
|
void Accept(ModelVisitor* const visitor) const override {
|
|
visitor->BeginVisitConstraint(ModelVisitor::kIsDifferent, this);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kLeftArgument, left_);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kRightArgument,
|
|
right_);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,
|
|
target_var_);
|
|
visitor->EndVisitConstraint(ModelVisitor::kIsDifferent, this);
|
|
}
|
|
|
|
private:
|
|
IntExpr* const left_;
|
|
IntExpr* const right_;
|
|
Demon* range_demon_;
|
|
};
|
|
|
|
class IsLessOrEqualCt : public CastConstraint {
|
|
public:
|
|
IsLessOrEqualCt(Solver* const s, IntExpr* const l, IntExpr* const r,
|
|
IntVar* const b)
|
|
: CastConstraint(s, b), left_(l), right_(r), demon_(nullptr) {}
|
|
|
|
~IsLessOrEqualCt() override {}
|
|
|
|
void Post() override {
|
|
demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
|
|
left_->WhenRange(demon_);
|
|
right_->WhenRange(demon_);
|
|
target_var_->WhenBound(demon_);
|
|
}
|
|
|
|
void InitialPropagate() override {
|
|
if (target_var_->Bound()) {
|
|
if (target_var_->Min() == 0) {
|
|
right_->SetMax(left_->Max() - 1);
|
|
left_->SetMin(right_->Min() + 1);
|
|
} else { // Var is true.
|
|
right_->SetMin(left_->Min());
|
|
left_->SetMax(right_->Max());
|
|
}
|
|
} else if (right_->Min() >= left_->Max()) {
|
|
demon_->inhibit(solver());
|
|
target_var_->SetValue(1);
|
|
} else if (right_->Max() < left_->Min()) {
|
|
demon_->inhibit(solver());
|
|
target_var_->SetValue(0);
|
|
}
|
|
}
|
|
|
|
std::string DebugString() const override {
|
|
return absl::StrFormat("IsLessOrEqualCt(%s, %s, %s)", left_->DebugString(),
|
|
right_->DebugString(), target_var_->DebugString());
|
|
}
|
|
|
|
void Accept(ModelVisitor* const visitor) const override {
|
|
visitor->BeginVisitConstraint(ModelVisitor::kIsLessOrEqual, this);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kLeftArgument, left_);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kRightArgument,
|
|
right_);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,
|
|
target_var_);
|
|
visitor->EndVisitConstraint(ModelVisitor::kIsLessOrEqual, this);
|
|
}
|
|
|
|
private:
|
|
IntExpr* const left_;
|
|
IntExpr* const right_;
|
|
Demon* demon_;
|
|
};
|
|
|
|
class IsLessCt : public CastConstraint {
|
|
public:
|
|
IsLessCt(Solver* const s, IntExpr* const l, IntExpr* const r, IntVar* const b)
|
|
: CastConstraint(s, b), left_(l), right_(r), demon_(nullptr) {}
|
|
|
|
~IsLessCt() override {}
|
|
|
|
void Post() override {
|
|
demon_ = solver()->MakeConstraintInitialPropagateCallback(this);
|
|
left_->WhenRange(demon_);
|
|
right_->WhenRange(demon_);
|
|
target_var_->WhenBound(demon_);
|
|
}
|
|
|
|
void InitialPropagate() override {
|
|
if (target_var_->Bound()) {
|
|
if (target_var_->Min() == 0) {
|
|
right_->SetMax(left_->Max());
|
|
left_->SetMin(right_->Min());
|
|
} else { // Var is true.
|
|
right_->SetMin(left_->Min() + 1);
|
|
left_->SetMax(right_->Max() - 1);
|
|
}
|
|
} else if (right_->Min() > left_->Max()) {
|
|
demon_->inhibit(solver());
|
|
target_var_->SetValue(1);
|
|
} else if (right_->Max() <= left_->Min()) {
|
|
demon_->inhibit(solver());
|
|
target_var_->SetValue(0);
|
|
}
|
|
}
|
|
|
|
std::string DebugString() const override {
|
|
return absl::StrFormat("IsLessCt(%s, %s, %s)", left_->DebugString(),
|
|
right_->DebugString(), target_var_->DebugString());
|
|
}
|
|
|
|
void Accept(ModelVisitor* const visitor) const override {
|
|
visitor->BeginVisitConstraint(ModelVisitor::kIsLess, this);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kLeftArgument, left_);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kRightArgument,
|
|
right_);
|
|
visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,
|
|
target_var_);
|
|
visitor->EndVisitConstraint(ModelVisitor::kIsLess, this);
|
|
}
|
|
|
|
private:
|
|
IntExpr* const left_;
|
|
IntExpr* const right_;
|
|
Demon* demon_;
|
|
};
|
|
} // namespace
|
|
|
|
Constraint* Solver::MakeEquality(IntExpr* const l, IntExpr* const r) {
|
|
CHECK(l != nullptr) << "left expression nullptr, maybe a bad cast";
|
|
CHECK(r != nullptr) << "left expression nullptr, maybe a bad cast";
|
|
CHECK_EQ(this, l->solver());
|
|
CHECK_EQ(this, r->solver());
|
|
if (l->Bound()) {
|
|
return MakeEquality(r, l->Min());
|
|
} else if (r->Bound()) {
|
|
return MakeEquality(l, r->Min());
|
|
} else {
|
|
return RevAlloc(new RangeEquality(this, l, r));
|
|
}
|
|
}
|
|
|
|
Constraint* Solver::MakeLessOrEqual(IntExpr* const l, IntExpr* const r) {
|
|
CHECK(l != nullptr) << "left expression nullptr, maybe a bad cast";
|
|
CHECK(r != nullptr) << "left expression nullptr, maybe a bad cast";
|
|
CHECK_EQ(this, l->solver());
|
|
CHECK_EQ(this, r->solver());
|
|
if (l == r) {
|
|
return MakeTrueConstraint();
|
|
} else if (l->Bound()) {
|
|
return MakeGreaterOrEqual(r, l->Min());
|
|
} else if (r->Bound()) {
|
|
return MakeLessOrEqual(l, r->Min());
|
|
} else {
|
|
return RevAlloc(new RangeLessOrEqual(this, l, r));
|
|
}
|
|
}
|
|
|
|
Constraint* Solver::MakeGreaterOrEqual(IntExpr* const l, IntExpr* const r) {
|
|
return MakeLessOrEqual(r, l);
|
|
}
|
|
|
|
Constraint* Solver::MakeLess(IntExpr* const l, IntExpr* const r) {
|
|
CHECK(l != nullptr) << "left expression nullptr, maybe a bad cast";
|
|
CHECK(r != nullptr) << "left expression nullptr, maybe a bad cast";
|
|
CHECK_EQ(this, l->solver());
|
|
CHECK_EQ(this, r->solver());
|
|
if (l->Bound()) {
|
|
return MakeGreater(r, l->Min());
|
|
} else if (r->Bound()) {
|
|
return MakeLess(l, r->Min());
|
|
} else {
|
|
return RevAlloc(new RangeLess(this, l, r));
|
|
}
|
|
}
|
|
|
|
Constraint* Solver::MakeGreater(IntExpr* const l, IntExpr* const r) {
|
|
return MakeLess(r, l);
|
|
}
|
|
|
|
Constraint* Solver::MakeNonEquality(IntExpr* const l, IntExpr* const r) {
|
|
CHECK(l != nullptr) << "left expression nullptr, maybe a bad cast";
|
|
CHECK(r != nullptr) << "left expression nullptr, maybe a bad cast";
|
|
CHECK_EQ(this, l->solver());
|
|
CHECK_EQ(this, r->solver());
|
|
if (l->Bound()) {
|
|
return MakeNonEquality(r, l->Min());
|
|
} else if (r->Bound()) {
|
|
return MakeNonEquality(l, r->Min());
|
|
}
|
|
return RevAlloc(new DiffVar(this, l->Var(), r->Var()));
|
|
}
|
|
|
|
IntVar* Solver::MakeIsEqualVar(IntExpr* const v1, IntExpr* const v2) {
|
|
CHECK_EQ(this, v1->solver());
|
|
CHECK_EQ(this, v2->solver());
|
|
if (v1->Bound()) {
|
|
return MakeIsEqualCstVar(v2, v1->Min());
|
|
} else if (v2->Bound()) {
|
|
return MakeIsEqualCstVar(v1, v2->Min());
|
|
}
|
|
IntExpr* cache = model_cache_->FindExprExprExpression(
|
|
v1, v2, ModelCache::EXPR_EXPR_IS_EQUAL);
|
|
if (cache == nullptr) {
|
|
cache = model_cache_->FindExprExprExpression(
|
|
v2, v1, ModelCache::EXPR_EXPR_IS_EQUAL);
|
|
}
|
|
if (cache != nullptr) {
|
|
return cache->Var();
|
|
} else {
|
|
IntVar* boolvar = nullptr;
|
|
IntExpr* reverse_cache = model_cache_->FindExprExprExpression(
|
|
v1, v2, ModelCache::EXPR_EXPR_IS_NOT_EQUAL);
|
|
if (reverse_cache == nullptr) {
|
|
reverse_cache = model_cache_->FindExprExprExpression(
|
|
v2, v1, ModelCache::EXPR_EXPR_IS_NOT_EQUAL);
|
|
}
|
|
if (reverse_cache != nullptr) {
|
|
boolvar = MakeDifference(1, reverse_cache)->Var();
|
|
} else {
|
|
std::string name1 = v1->name();
|
|
if (name1.empty()) {
|
|
name1 = v1->DebugString();
|
|
}
|
|
std::string name2 = v2->name();
|
|
if (name2.empty()) {
|
|
name2 = v2->DebugString();
|
|
}
|
|
boolvar =
|
|
MakeBoolVar(absl::StrFormat("IsEqualVar(%s, %s)", name1, name2));
|
|
AddConstraint(MakeIsEqualCt(v1, v2, boolvar));
|
|
model_cache_->InsertExprExprExpression(boolvar, v1, v2,
|
|
ModelCache::EXPR_EXPR_IS_EQUAL);
|
|
}
|
|
return boolvar;
|
|
}
|
|
}
|
|
|
|
Constraint* Solver::MakeIsEqualCt(IntExpr* const v1, IntExpr* const v2,
|
|
IntVar* b) {
|
|
CHECK_EQ(this, v1->solver());
|
|
CHECK_EQ(this, v2->solver());
|
|
if (v1->Bound()) {
|
|
return MakeIsEqualCstCt(v2, v1->Min(), b);
|
|
} else if (v2->Bound()) {
|
|
return MakeIsEqualCstCt(v1, v2->Min(), b);
|
|
}
|
|
if (b->Bound()) {
|
|
if (b->Min() == 0) {
|
|
return MakeNonEquality(v1, v2);
|
|
} else {
|
|
return MakeEquality(v1, v2);
|
|
}
|
|
}
|
|
return RevAlloc(new IsEqualCt(this, v1, v2, b));
|
|
}
|
|
|
|
IntVar* Solver::MakeIsDifferentVar(IntExpr* const v1, IntExpr* const v2) {
|
|
CHECK_EQ(this, v1->solver());
|
|
CHECK_EQ(this, v2->solver());
|
|
if (v1->Bound()) {
|
|
return MakeIsDifferentCstVar(v2, v1->Min());
|
|
} else if (v2->Bound()) {
|
|
return MakeIsDifferentCstVar(v1, v2->Min());
|
|
}
|
|
IntExpr* cache = model_cache_->FindExprExprExpression(
|
|
v1, v2, ModelCache::EXPR_EXPR_IS_NOT_EQUAL);
|
|
if (cache == nullptr) {
|
|
cache = model_cache_->FindExprExprExpression(
|
|
v2, v1, ModelCache::EXPR_EXPR_IS_NOT_EQUAL);
|
|
}
|
|
if (cache != nullptr) {
|
|
return cache->Var();
|
|
} else {
|
|
IntVar* boolvar = nullptr;
|
|
IntExpr* reverse_cache = model_cache_->FindExprExprExpression(
|
|
v1, v2, ModelCache::EXPR_EXPR_IS_EQUAL);
|
|
if (reverse_cache == nullptr) {
|
|
reverse_cache = model_cache_->FindExprExprExpression(
|
|
v2, v1, ModelCache::EXPR_EXPR_IS_EQUAL);
|
|
}
|
|
if (reverse_cache != nullptr) {
|
|
boolvar = MakeDifference(1, reverse_cache)->Var();
|
|
} else {
|
|
std::string name1 = v1->name();
|
|
if (name1.empty()) {
|
|
name1 = v1->DebugString();
|
|
}
|
|
std::string name2 = v2->name();
|
|
if (name2.empty()) {
|
|
name2 = v2->DebugString();
|
|
}
|
|
boolvar =
|
|
MakeBoolVar(absl::StrFormat("IsDifferentVar(%s, %s)", name1, name2));
|
|
AddConstraint(MakeIsDifferentCt(v1, v2, boolvar));
|
|
}
|
|
model_cache_->InsertExprExprExpression(boolvar, v1, v2,
|
|
ModelCache::EXPR_EXPR_IS_NOT_EQUAL);
|
|
return boolvar;
|
|
}
|
|
}
|
|
|
|
Constraint* Solver::MakeIsDifferentCt(IntExpr* const v1, IntExpr* const v2,
|
|
IntVar* b) {
|
|
CHECK_EQ(this, v1->solver());
|
|
CHECK_EQ(this, v2->solver());
|
|
if (v1->Bound()) {
|
|
return MakeIsDifferentCstCt(v2, v1->Min(), b);
|
|
} else if (v2->Bound()) {
|
|
return MakeIsDifferentCstCt(v1, v2->Min(), b);
|
|
}
|
|
return RevAlloc(new IsDifferentCt(this, v1, v2, b));
|
|
}
|
|
|
|
IntVar* Solver::MakeIsLessOrEqualVar(IntExpr* const left,
|
|
IntExpr* const right) {
|
|
CHECK_EQ(this, left->solver());
|
|
CHECK_EQ(this, right->solver());
|
|
if (left->Bound()) {
|
|
return MakeIsGreaterOrEqualCstVar(right, left->Min());
|
|
} else if (right->Bound()) {
|
|
return MakeIsLessOrEqualCstVar(left, right->Min());
|
|
}
|
|
IntExpr* const cache = model_cache_->FindExprExprExpression(
|
|
left, right, ModelCache::EXPR_EXPR_IS_LESS_OR_EQUAL);
|
|
if (cache != nullptr) {
|
|
return cache->Var();
|
|
} else {
|
|
std::string name1 = left->name();
|
|
if (name1.empty()) {
|
|
name1 = left->DebugString();
|
|
}
|
|
std::string name2 = right->name();
|
|
if (name2.empty()) {
|
|
name2 = right->DebugString();
|
|
}
|
|
IntVar* const boolvar =
|
|
MakeBoolVar(absl::StrFormat("IsLessOrEqual(%s, %s)", name1, name2));
|
|
|
|
AddConstraint(RevAlloc(new IsLessOrEqualCt(this, left, right, boolvar)));
|
|
model_cache_->InsertExprExprExpression(
|
|
boolvar, left, right, ModelCache::EXPR_EXPR_IS_LESS_OR_EQUAL);
|
|
return boolvar;
|
|
}
|
|
}
|
|
|
|
Constraint* Solver::MakeIsLessOrEqualCt(IntExpr* const left,
|
|
IntExpr* const right, IntVar* const b) {
|
|
CHECK_EQ(this, left->solver());
|
|
CHECK_EQ(this, right->solver());
|
|
if (left->Bound()) {
|
|
return MakeIsGreaterOrEqualCstCt(right, left->Min(), b);
|
|
} else if (right->Bound()) {
|
|
return MakeIsLessOrEqualCstCt(left, right->Min(), b);
|
|
}
|
|
return RevAlloc(new IsLessOrEqualCt(this, left, right, b));
|
|
}
|
|
|
|
IntVar* Solver::MakeIsLessVar(IntExpr* const left, IntExpr* const right) {
|
|
CHECK_EQ(this, left->solver());
|
|
CHECK_EQ(this, right->solver());
|
|
if (left->Bound()) {
|
|
return MakeIsGreaterCstVar(right, left->Min());
|
|
} else if (right->Bound()) {
|
|
return MakeIsLessCstVar(left, right->Min());
|
|
}
|
|
IntExpr* const cache = model_cache_->FindExprExprExpression(
|
|
left, right, ModelCache::EXPR_EXPR_IS_LESS);
|
|
if (cache != nullptr) {
|
|
return cache->Var();
|
|
} else {
|
|
std::string name1 = left->name();
|
|
if (name1.empty()) {
|
|
name1 = left->DebugString();
|
|
}
|
|
std::string name2 = right->name();
|
|
if (name2.empty()) {
|
|
name2 = right->DebugString();
|
|
}
|
|
IntVar* const boolvar =
|
|
MakeBoolVar(absl::StrFormat("IsLessOrEqual(%s, %s)", name1, name2));
|
|
|
|
AddConstraint(RevAlloc(new IsLessCt(this, left, right, boolvar)));
|
|
model_cache_->InsertExprExprExpression(boolvar, left, right,
|
|
ModelCache::EXPR_EXPR_IS_LESS);
|
|
return boolvar;
|
|
}
|
|
}
|
|
|
|
Constraint* Solver::MakeIsLessCt(IntExpr* const left, IntExpr* const right,
|
|
IntVar* const b) {
|
|
CHECK_EQ(this, left->solver());
|
|
CHECK_EQ(this, right->solver());
|
|
if (left->Bound()) {
|
|
return MakeIsGreaterCstCt(right, left->Min(), b);
|
|
} else if (right->Bound()) {
|
|
return MakeIsLessCstCt(left, right->Min(), b);
|
|
}
|
|
return RevAlloc(new IsLessCt(this, left, right, b));
|
|
}
|
|
|
|
IntVar* Solver::MakeIsGreaterOrEqualVar(IntExpr* const left,
|
|
IntExpr* const right) {
|
|
return MakeIsLessOrEqualVar(right, left);
|
|
}
|
|
|
|
Constraint* Solver::MakeIsGreaterOrEqualCt(IntExpr* const left,
|
|
IntExpr* const right,
|
|
IntVar* const b) {
|
|
return MakeIsLessOrEqualCt(right, left, b);
|
|
}
|
|
|
|
IntVar* Solver::MakeIsGreaterVar(IntExpr* const left, IntExpr* const right) {
|
|
return MakeIsLessVar(right, left);
|
|
}
|
|
|
|
Constraint* Solver::MakeIsGreaterCt(IntExpr* const left, IntExpr* const right,
|
|
IntVar* const b) {
|
|
return MakeIsLessCt(right, left, b);
|
|
}
|
|
|
|
} // namespace operations_research
|