Google OR-Tools: ortools/constraint_solver/range_cst.cc Source File

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16#include <stddef.h>

17

18#include <string>

19

20#include "absl/strings/str_format.h"

24

26

27

28

29

30namespace {

31class RangeEquality : public Constraint {

32 public:

33 RangeEquality(Solver* const s, IntExpr* const l, IntExpr* const r)

34 : Constraint(s), left_(l), right_(r) {}

35

36 ~RangeEquality() override {}

37

38 void Post() override {

39 Demon* const d = solver()->MakeConstraintInitialPropagateCallback(this);

40 left_->WhenRange(d);

41 right_->WhenRange(d);

42 }

43

44 void InitialPropagate() override {

45 left_->SetRange(right_->Min(), right_->Max());

46 right_->SetRange(left_->Min(), left_->Max());

47 }

48

49 std::string DebugString() const override {

50 return left_->DebugString() + " == " + right_->DebugString();

51 }

52

53 IntVar* Var() override { return solver()->MakeIsEqualVar(left_, right_); }

54

55 void Accept(ModelVisitor* const visitor) const override {

59 right_);

61 }

62

63 private:

64 IntExpr* const left_;

65 IntExpr* const right_;

66};

67

68

69

70

71class RangeLessOrEqual : public Constraint {

72 public:

73 RangeLessOrEqual(Solver* s, IntExpr* l, IntExpr* r);

74 ~RangeLessOrEqual() override {}

75 void Post() override;

76 void InitialPropagate() override;

77 std::string DebugString() const override;

78 IntVar* Var() override {

79 return solver()->MakeIsLessOrEqualVar(left_, right_);

80 }

81 void Accept(ModelVisitor* const visitor) const override {

85 right_);

87 }

88

89 private:

90 IntExpr* const left_;

91 IntExpr* const right_;

92 Demon* demon_;

93};

94

95RangeLessOrEqual::RangeLessOrEqual(Solver* const s, IntExpr* const l,

97 : Constraint(s), left_(l), right_(r), demon_(nullptr) {}

98

99void RangeLessOrEqual::Post() {

100 demon_ = solver()->MakeConstraintInitialPropagateCallback(this);

101 left_->WhenRange(demon_);

102 right_->WhenRange(demon_);

103}

104

105void RangeLessOrEqual::InitialPropagate() {

106 left_->SetMax(right_->Max());

107 right_->SetMin(left_->Min());

108 if (left_->Max() <= right_->Min()) {

109 demon_->inhibit(solver());

110 }

111}

112

113std::string RangeLessOrEqual::DebugString() const {

114 return left_->DebugString() + " <= " + right_->DebugString();

115}

116

117

118

119

121 public:

122 RangeLess(Solver* s, IntExpr* l, IntExpr* r);

123 ~RangeLess() override {}

124 void Post() override;

125 void InitialPropagate() override;

126 std::string DebugString() const override;

127 IntVar* Var() override { return solver()->MakeIsLessVar(left_, right_); }

128 void Accept(ModelVisitor* const visitor) const override {

129 visitor->BeginVisitConstraint(ModelVisitor::kLess, this);

130 visitor->VisitIntegerExpressionArgument(ModelVisitor::kLeftArgument, left_);

131 visitor->VisitIntegerExpressionArgument(ModelVisitor::kRightArgument,

132 right_);

133 visitor->EndVisitConstraint(ModelVisitor::kLess, this);

134 }

135

136 private:

137 IntExpr* const left_;

138 IntExpr* const right_;

139 Demon* demon_;

140};

141

142RangeLess::RangeLess(Solver* const s, IntExpr* const l, IntExpr* const r)

143 : Constraint(s), left_(l), right_(r), demon_(nullptr) {}

144

145void RangeLess::Post() {

146 demon_ = solver()->MakeConstraintInitialPropagateCallback(this);

147 left_->WhenRange(demon_);

148 right_->WhenRange(demon_);

149}

150

151void RangeLess::InitialPropagate() {

152 if (right_->Max() == kint64min) solver()->Fail();

153 left_->SetMax(right_->Max() - 1);

154 if (left_->Min() == kint64max) solver()->Fail();

155 right_->SetMin(left_->Min() + 1);

156 if (left_->Max() < right_->Min()) {

157 demon_->inhibit(solver());

158 }

159}

160

161std::string RangeLess::DebugString() const {

162 return left_->DebugString() + " < " + right_->DebugString();

163}

164

165

166

167

169 public:

170 DiffVar(Solver* s, IntVar* l, IntVar* r);

171 ~DiffVar() override {}

172 void Post() override;

173 void InitialPropagate() override;

174 std::string DebugString() const override;

175 IntVar* Var() override { return solver()->MakeIsDifferentVar(left_, right_); }

176 void LeftBound();

177 void RightBound();

178

179 void Accept(ModelVisitor* const visitor) const override {

180 visitor->BeginVisitConstraint(ModelVisitor::kNonEqual, this);

181 visitor->VisitIntegerExpressionArgument(ModelVisitor::kLeftArgument, left_);

182 visitor->VisitIntegerExpressionArgument(ModelVisitor::kRightArgument,

183 right_);

184 visitor->EndVisitConstraint(ModelVisitor::kNonEqual, this);

185 }

186

187 private:

188 IntVar* const left_;

189 IntVar* const right_;

190};

191

192DiffVar::DiffVar(Solver* const s, IntVar* const l, IntVar* const r)

193 : Constraint(s), left_(l), right_(r) {}

194

195void DiffVar::Post() {

196 Demon* const left_demon =

198 Demon* const right_demon =

200 left_->WhenBound(left_demon);

201 right_->WhenBound(right_demon);

202

203}

204

205void DiffVar::LeftBound() {

206 if (right_->Size() < 0xFFFFFF) {

207 right_->RemoveValue(left_->Min());

208 } else {

209 solver()->AddConstraint(solver()->MakeNonEquality(right_, left_->Min()));

210 }

211}

212

213void DiffVar::RightBound() {

214 if (left_->Size() < 0xFFFFFF) {

215 left_->RemoveValue(right_->Min());

216 } else {

217 solver()->AddConstraint(solver()->MakeNonEquality(left_, right_->Min()));

218 }

219}

220

221void DiffVar::InitialPropagate() {

222 if (left_->Bound()) {

223 LeftBound();

224 }

225 if (right_->Bound()) {

226 RightBound();

227 }

228}

229

230std::string DiffVar::DebugString() const {

231 return left_->DebugString() + " != " + right_->DebugString();

232}

233

234

235

236

237

238

239

240

241class IsEqualCt : public CastConstraint {

242 public:

243 IsEqualCt(Solver* const s, IntExpr* const l, IntExpr* const r,

244 IntVar* const b)

245 : CastConstraint(s, b), left_(l), right_(r), range_demon_(nullptr) {}

246

247 ~IsEqualCt() override {}

248

249 void Post() override {

250 range_demon_ = solver()->MakeConstraintInitialPropagateCallback(this);

251 left_->WhenRange(range_demon_);

252 right_->WhenRange(range_demon_);

254 solver(), this, &IsEqualCt::PropagateTarget, "PropagateTarget");

255 target_var_->WhenBound(target_demon);

256 }

257

258 void InitialPropagate() override {

259 if (target_var_->Bound()) {

260 PropagateTarget();

261 return;

262 }

263 if (left_->Min() > right_->Max() || left_->Max() < right_->Min()) {

264 target_var_->SetValue(0);

265 range_demon_->inhibit(solver());

266 } else if (left_->Bound()) {

267 if (right_->Bound()) {

268 target_var_->SetValue(left_->Min() == right_->Min());

269 } else if (right_->IsVar() && !right_->Var()->Contains(left_->Min())) {

270 range_demon_->inhibit(solver());

271 target_var_->SetValue(0);

272 }

273 } else if (right_->Bound() && left_->IsVar() &&

274 !left_->Var()->Contains(right_->Min())) {

275 range_demon_->inhibit(solver());

276 target_var_->SetValue(0);

277 }

278 }

279

280 void PropagateTarget() {

281 if (target_var_->Min() == 0) {

282 if (left_->Bound()) {

283 range_demon_->inhibit(solver());

284 if (right_->IsVar()) {

285 right_->Var()->RemoveValue(left_->Min());

286 } else {

287 solver()->AddConstraint(

288 solver()->MakeNonEquality(right_, left_->Min()));

289 }

290 } else if (right_->Bound()) {

291 range_demon_->inhibit(solver());

292 if (left_->IsVar()) {

293 left_->Var()->RemoveValue(right_->Min());

294 } else {

295 solver()->AddConstraint(

296 solver()->MakeNonEquality(left_, right_->Min()));

297 }

298 }

299 } else {

300 left_->SetRange(right_->Min(), right_->Max());

301 right_->SetRange(left_->Min(), left_->Max());

302 }

303 }

304

305 std::string DebugString() const override {

306 return absl::StrFormat("IsEqualCt(%s, %s, %s)", left_->DebugString(),

307 right_->DebugString(), target_var_->DebugString());

308 }

309

310 void Accept(ModelVisitor* const visitor) const override {

311 visitor->BeginVisitConstraint(ModelVisitor::kIsEqual, this);

312 visitor->VisitIntegerExpressionArgument(ModelVisitor::kLeftArgument, left_);

313 visitor->VisitIntegerExpressionArgument(ModelVisitor::kRightArgument,

314 right_);

315 visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,

316 target_var_);

317 visitor->EndVisitConstraint(ModelVisitor::kIsEqual, this);

318 }

319

320 private:

321 IntExpr* const left_;

322 IntExpr* const right_;

323 Demon* range_demon_;

324};

325

326

327

328class IsDifferentCt : public CastConstraint {

329 public:

330 IsDifferentCt(Solver* const s, IntExpr* const l, IntExpr* const r,

331 IntVar* const b)

332 : CastConstraint(s, b), left_(l), right_(r), range_demon_(nullptr) {}

333

334 ~IsDifferentCt() override {}

335

336 void Post() override {

337 range_demon_ = solver()->MakeConstraintInitialPropagateCallback(this);

338 left_->WhenRange(range_demon_);

339 right_->WhenRange(range_demon_);

341 solver(), this, &IsDifferentCt::PropagateTarget, "PropagateTarget");

342 target_var_->WhenBound(target_demon);

343 }

344

345 void InitialPropagate() override {

346 if (target_var_->Bound()) {

347 PropagateTarget();

348 return;

349 }

350 if (left_->Min() > right_->Max() || left_->Max() < right_->Min()) {

351 target_var_->SetValue(1);

352 range_demon_->inhibit(solver());

353 } else if (left_->Bound()) {

354 if (right_->Bound()) {

355 target_var_->SetValue(left_->Min() != right_->Min());

356 } else if (right_->IsVar() && !right_->Var()->Contains(left_->Min())) {

357 range_demon_->inhibit(solver());

358 target_var_->SetValue(1);

359 }

360 } else if (right_->Bound() && left_->IsVar() &&

361 !left_->Var()->Contains(right_->Min())) {

362 range_demon_->inhibit(solver());

363 target_var_->SetValue(1);

364 }

365 }

366

367 void PropagateTarget() {

368 if (target_var_->Min() == 0) {

369 left_->SetRange(right_->Min(), right_->Max());

370 right_->SetRange(left_->Min(), left_->Max());

371 } else {

372 if (left_->Bound()) {

373 range_demon_->inhibit(solver());

374 solver()->AddConstraint(

375 solver()->MakeNonEquality(right_, left_->Min()));

376 } else if (right_->Bound()) {

377 range_demon_->inhibit(solver());

378 solver()->AddConstraint(

379 solver()->MakeNonEquality(left_, right_->Min()));

380 }

381 }

382 }

383

384 std::string DebugString() const override {

385 return absl::StrFormat("IsDifferentCt(%s, %s, %s)", left_->DebugString(),

386 right_->DebugString(), target_var_->DebugString());

387 }

388

389 void Accept(ModelVisitor* const visitor) const override {

390 visitor->BeginVisitConstraint(ModelVisitor::kIsDifferent, this);

391 visitor->VisitIntegerExpressionArgument(ModelVisitor::kLeftArgument, left_);

392 visitor->VisitIntegerExpressionArgument(ModelVisitor::kRightArgument,

393 right_);

394 visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,

395 target_var_);

396 visitor->EndVisitConstraint(ModelVisitor::kIsDifferent, this);

397 }

398

399 private:

400 IntExpr* const left_;

401 IntExpr* const right_;

402 Demon* range_demon_;

403};

404

405class IsLessOrEqualCt : public CastConstraint {

406 public:

407 IsLessOrEqualCt(Solver* const s, IntExpr* const l, IntExpr* const r,

408 IntVar* const b)

409 : CastConstraint(s, b), left_(l), right_(r), demon_(nullptr) {}

410

411 ~IsLessOrEqualCt() override {}

412

413 void Post() override {

414 demon_ = solver()->MakeConstraintInitialPropagateCallback(this);

415 left_->WhenRange(demon_);

416 right_->WhenRange(demon_);

417 target_var_->WhenBound(demon_);

418 }

419

420 void InitialPropagate() override {

421 if (target_var_->Bound()) {

422 if (target_var_->Min() == 0) {

423 right_->SetMax(left_->Max() - 1);

424 left_->SetMin(right_->Min() + 1);

425 } else {

426 right_->SetMin(left_->Min());

427 left_->SetMax(right_->Max());

428 }

429 } else if (right_->Min() >= left_->Max()) {

430 demon_->inhibit(solver());

431 target_var_->SetValue(1);

432 } else if (right_->Max() < left_->Min()) {

433 demon_->inhibit(solver());

434 target_var_->SetValue(0);

435 }

436 }

437

438 std::string DebugString() const override {

439 return absl::StrFormat("IsLessOrEqualCt(%s, %s, %s)", left_->DebugString(),

440 right_->DebugString(), target_var_->DebugString());

441 }

442

443 void Accept(ModelVisitor* const visitor) const override {

444 visitor->BeginVisitConstraint(ModelVisitor::kIsLessOrEqual, this);

445 visitor->VisitIntegerExpressionArgument(ModelVisitor::kLeftArgument, left_);

446 visitor->VisitIntegerExpressionArgument(ModelVisitor::kRightArgument,

447 right_);

448 visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,

449 target_var_);

450 visitor->EndVisitConstraint(ModelVisitor::kIsLessOrEqual, this);

451 }

452

453 private:

454 IntExpr* const left_;

455 IntExpr* const right_;

456 Demon* demon_;

457};

458

459class IsLessCt : public CastConstraint {

460 public:

461 IsLessCt(Solver* const s, IntExpr* const l, IntExpr* const r, IntVar* const b)

462 : CastConstraint(s, b), left_(l), right_(r), demon_(nullptr) {}

463

464 ~IsLessCt() override {}

465

466 void Post() override {

467 demon_ = solver()->MakeConstraintInitialPropagateCallback(this);

468 left_->WhenRange(demon_);

469 right_->WhenRange(demon_);

470 target_var_->WhenBound(demon_);

471 }

472

473 void InitialPropagate() override {

474 if (target_var_->Bound()) {

475 if (target_var_->Min() == 0) {

476 right_->SetMax(left_->Max());

477 left_->SetMin(right_->Min());

478 } else {

479 right_->SetMin(left_->Min() + 1);

480 left_->SetMax(right_->Max() - 1);

481 }

482 } else if (right_->Min() > left_->Max()) {

483 demon_->inhibit(solver());

484 target_var_->SetValue(1);

485 } else if (right_->Max() <= left_->Min()) {

486 demon_->inhibit(solver());

487 target_var_->SetValue(0);

488 }

489 }

490

491 std::string DebugString() const override {

492 return absl::StrFormat("IsLessCt(%s, %s, %s)", left_->DebugString(),

493 right_->DebugString(), target_var_->DebugString());

494 }

495

496 void Accept(ModelVisitor* const visitor) const override {

497 visitor->BeginVisitConstraint(ModelVisitor::kIsLess, this);

498 visitor->VisitIntegerExpressionArgument(ModelVisitor::kLeftArgument, left_);

499 visitor->VisitIntegerExpressionArgument(ModelVisitor::kRightArgument,

500 right_);

501 visitor->VisitIntegerExpressionArgument(ModelVisitor::kTargetArgument,

502 target_var_);

503 visitor->EndVisitConstraint(ModelVisitor::kIsLess, this);

504 }

505

506 private:

507 IntExpr* const left_;

508 IntExpr* const right_;

509 Demon* demon_;

510};

511}

512

513Constraint* Solver::MakeEquality(IntExpr* const l, IntExpr* const r) {

514 CHECK(l != nullptr) << "left expression nullptr, maybe a bad cast";

515 CHECK(r != nullptr) << "left expression nullptr, maybe a bad cast";

516 CHECK_EQ(this, l->solver());

517 CHECK_EQ(this, r->solver());

518 if (l->Bound()) {

520 } else if (r->Bound()) {

521 return MakeEquality(l, r->Min());

522 } else {

523 return RevAlloc(new RangeEquality(this, l, r));

524 }

525}

526

527Constraint* Solver::MakeLessOrEqual(IntExpr* const l, IntExpr* const r) {

528 CHECK(l != nullptr) << "left expression nullptr, maybe a bad cast";

529 CHECK(r != nullptr) << "left expression nullptr, maybe a bad cast";

530 CHECK_EQ(this, l->solver());

531 CHECK_EQ(this, r->solver());

532 if (l == r) {

534 } else if (l->Bound()) {

535 return MakeGreaterOrEqual(r, l->Min());

536 } else if (r->Bound()) {

537 return MakeLessOrEqual(l, r->Min());

538 } else {

539 return RevAlloc(new RangeLessOrEqual(this, l, r));

540 }

541}

542

543Constraint* Solver::MakeGreaterOrEqual(IntExpr* const l, IntExpr* const r) {

544 return MakeLessOrEqual(r, l);

545}

546

548 CHECK(l != nullptr) << "left expression nullptr, maybe a bad cast";

549 CHECK(r != nullptr) << "left expression nullptr, maybe a bad cast";

550 CHECK_EQ(this, l->solver());

552 if (l->Bound()) {

554 } else if (r->Bound()) {

555 return MakeLess(l, r->Min());

556 } else {

557 return RevAlloc(new RangeLess(this, l, r));

558 }

559}

560

561Constraint* Solver::MakeGreater(IntExpr* const l, IntExpr* const r) {

562 return MakeLess(r, l);

563}

564

566 CHECK(l != nullptr) << "left expression nullptr, maybe a bad cast";

567 CHECK(r != nullptr) << "left expression nullptr, maybe a bad cast";

568 CHECK_EQ(this, l->solver());

570 if (l->Bound()) {

572 } else if (r->Bound()) {

573 return MakeNonEquality(l, r->Min());

574 }

575 return RevAlloc(new DiffVar(this, l->Var(), r->Var()));

576}

577

578IntVar* Solver::MakeIsEqualVar(IntExpr* const v1, IntExpr* const v2) {

579 CHECK_EQ(this, v1->solver());

580 CHECK_EQ(this, v2->solver());

581 if (v1->Bound()) {

583 } else if (v2->Bound()) {

584 return MakeIsEqualCstVar(v1, v2->Min());

585 }

586 IntExpr* cache = model_cache_->FindExprExprExpression(

587 v1, v2, ModelCache::EXPR_EXPR_IS_EQUAL);

588 if (cache == nullptr) {

589 cache = model_cache_->FindExprExprExpression(

590 v2, v1, ModelCache::EXPR_EXPR_IS_EQUAL);

591 }

592 if (cache != nullptr) {

593 return cache->Var();

594 } else {

595 IntVar* boolvar = nullptr;

596 IntExpr* reverse_cache = model_cache_->FindExprExprExpression(

597 v1, v2, ModelCache::EXPR_EXPR_IS_NOT_EQUAL);

598 if (reverse_cache == nullptr) {

599 reverse_cache = model_cache_->FindExprExprExpression(

600 v2, v1, ModelCache::EXPR_EXPR_IS_NOT_EQUAL);

601 }

602 if (reverse_cache != nullptr) {

603 boolvar = MakeDifference(1, reverse_cache)->Var();

604 } else {

605 std::string name1 = v1->name();

606 if (name1.empty()) {

607 name1 = v1->DebugString();

608 }

609 std::string name2 = v2->name();

610 if (name2.empty()) {

611 name2 = v2->DebugString();

612 }

613 boolvar =

614 MakeBoolVar(absl::StrFormat("IsEqualVar(%s, %s)", name1, name2));

615 AddConstraint(MakeIsEqualCt(v1, v2, boolvar));

616 model_cache_->InsertExprExprExpression(boolvar, v1, v2,

617 ModelCache::EXPR_EXPR_IS_EQUAL);

618 }

619 return boolvar;

620 }

621}

622

623Constraint* Solver::MakeIsEqualCt(IntExpr* const v1, IntExpr* const v2,

624 IntVar* b) {

625 CHECK_EQ(this, v1->solver());

626 CHECK_EQ(this, v2->solver());

627 if (v1->Bound()) {

629 } else if (v2->Bound()) {

630 return MakeIsEqualCstCt(v1, v2->Min(), b);

631 }

632 if (b->Bound()) {

633 if (b->Min() == 0) {

634 return MakeNonEquality(v1, v2);

635 } else {

636 return MakeEquality(v1, v2);

637 }

638 }

639 return RevAlloc(new IsEqualCt(this, v1, v2, b));

640}

641

642IntVar* Solver::MakeIsDifferentVar(IntExpr* const v1, IntExpr* const v2) {

643 CHECK_EQ(this, v1->solver());

644 CHECK_EQ(this, v2->solver());

645 if (v1->Bound()) {

647 } else if (v2->Bound()) {

648 return MakeIsDifferentCstVar(v1, v2->Min());

649 }

650 IntExpr* cache = model_cache_->FindExprExprExpression(

651 v1, v2, ModelCache::EXPR_EXPR_IS_NOT_EQUAL);

652 if (cache == nullptr) {

653 cache = model_cache_->FindExprExprExpression(

654 v2, v1, ModelCache::EXPR_EXPR_IS_NOT_EQUAL);

655 }

656 if (cache != nullptr) {

657 return cache->Var();

658 } else {

659 IntVar* boolvar = nullptr;

660 IntExpr* reverse_cache = model_cache_->FindExprExprExpression(

661 v1, v2, ModelCache::EXPR_EXPR_IS_EQUAL);

662 if (reverse_cache == nullptr) {

663 reverse_cache = model_cache_->FindExprExprExpression(

664 v2, v1, ModelCache::EXPR_EXPR_IS_EQUAL);

665 }

666 if (reverse_cache != nullptr) {

667 boolvar = MakeDifference(1, reverse_cache)->Var();

668 } else {

669 std::string name1 = v1->name();

670 if (name1.empty()) {

671 name1 = v1->DebugString();

672 }

673 std::string name2 = v2->name();

674 if (name2.empty()) {

675 name2 = v2->DebugString();

676 }

677 boolvar =

678 MakeBoolVar(absl::StrFormat("IsDifferentVar(%s, %s)", name1, name2));

679 AddConstraint(MakeIsDifferentCt(v1, v2, boolvar));

680 }

681 model_cache_->InsertExprExprExpression(boolvar, v1, v2,

682 ModelCache::EXPR_EXPR_IS_NOT_EQUAL);

683 return boolvar;

684 }

685}

686

687Constraint* Solver::MakeIsDifferentCt(IntExpr* const v1, IntExpr* const v2,

688 IntVar* b) {

689 CHECK_EQ(this, v1->solver());

690 CHECK_EQ(this, v2->solver());

691 if (v1->Bound()) {

693 } else if (v2->Bound()) {

694 return MakeIsDifferentCstCt(v1, v2->Min(), b);

695 }

696 return RevAlloc(new IsDifferentCt(this, v1, v2, b));

697}

698

699IntVar* Solver::MakeIsLessOrEqualVar(IntExpr* const left,

700 IntExpr* const right) {

701 CHECK_EQ(this, left->solver());

702 CHECK_EQ(this, right->solver());

703 if (left->Bound()) {

705 } else if (right->Bound()) {

706 return MakeIsLessOrEqualCstVar(left, right->Min());

707 }

708 IntExpr* const cache = model_cache_->FindExprExprExpression(

709 left, right, ModelCache::EXPR_EXPR_IS_LESS_OR_EQUAL);

710 if (cache != nullptr) {

711 return cache->Var();

712 } else {

713 std::string name1 = left->name();

714 if (name1.empty()) {

715 name1 = left->DebugString();

716 }

717 std::string name2 = right->name();

718 if (name2.empty()) {

719 name2 = right->DebugString();

720 }

721 IntVar* const boolvar =

722 MakeBoolVar(absl::StrFormat("IsLessOrEqual(%s, %s)", name1, name2));

723

724 AddConstraint(RevAlloc(new IsLessOrEqualCt(this, left, right, boolvar)));

725 model_cache_->InsertExprExprExpression(

726 boolvar, left, right, ModelCache::EXPR_EXPR_IS_LESS_OR_EQUAL);

727 return boolvar;

728 }

729}

730

731Constraint* Solver::MakeIsLessOrEqualCt(IntExpr* const left,

732 IntExpr* const right, IntVar* const b) {

733 CHECK_EQ(this, left->solver());

734 CHECK_EQ(this, right->solver());

735 if (left->Bound()) {

737 } else if (right->Bound()) {

738 return MakeIsLessOrEqualCstCt(left, right->Min(), b);

739 }

740 return RevAlloc(new IsLessOrEqualCt(this, left, right, b));

741}

742

743IntVar* Solver::MakeIsLessVar(IntExpr* const left, IntExpr* const right) {

744 CHECK_EQ(this, left->solver());

745 CHECK_EQ(this, right->solver());

746 if (left->Bound()) {

748 } else if (right->Bound()) {

749 return MakeIsLessCstVar(left, right->Min());

750 }

751 IntExpr* const cache = model_cache_->FindExprExprExpression(

752 left, right, ModelCache::EXPR_EXPR_IS_LESS);

753 if (cache != nullptr) {

754 return cache->Var();

755 } else {

756 std::string name1 = left->name();

757 if (name1.empty()) {

758 name1 = left->DebugString();

759 }

760 std::string name2 = right->name();

761 if (name2.empty()) {

762 name2 = right->DebugString();

763 }

764 IntVar* const boolvar =

765 MakeBoolVar(absl::StrFormat("IsLessOrEqual(%s, %s)", name1, name2));

766

767 AddConstraint(RevAlloc(new IsLessCt(this, left, right, boolvar)));

768 model_cache_->InsertExprExprExpression(boolvar, left, right,

769 ModelCache::EXPR_EXPR_IS_LESS);

770 return boolvar;

771 }

772}

773

774Constraint* Solver::MakeIsLessCt(IntExpr* const left, IntExpr* const right,

775 IntVar* const b) {

776 CHECK_EQ(this, left->solver());

777 CHECK_EQ(this, right->solver());

778 if (left->Bound()) {

780 } else if (right->Bound()) {

781 return MakeIsLessCstCt(left, right->Min(), b);

782 }

783 return RevAlloc(new IsLessCt(this, left, right, b));

784}

785

786IntVar* Solver::MakeIsGreaterOrEqualVar(IntExpr* const left,

787 IntExpr* const right) {

788 return MakeIsLessOrEqualVar(right, left);

789}

796

798 return MakeIsLessVar(right, left);

799}

800

804}

std::string DebugString() const override

virtual bool Bound() const

Returns true if the min and the max of the expression are equal.

virtual int64_t Min() const =0

virtual IntVar * Var()=0

Creates a variable from the expression.

static const char kLessOrEqual[]

static const char kRightArgument[]

static const char kEquality[]

static const char kLeftArgument[]

Constraint * MakeIsLessOrEqualCt(IntExpr *left, IntExpr *right, IntVar *b)

b == (left <= right)

Definition range_cst.cc:735

Constraint * MakeIsEqualCstCt(IntExpr *var, int64_t value, IntVar *boolvar)

boolvar == (var == value)

Constraint * MakeIsGreaterCt(IntExpr *left, IntExpr *right, IntVar *b)

b == (left > right)

Definition range_cst.cc:805

Constraint * MakeIsGreaterOrEqualCt(IntExpr *left, IntExpr *right, IntVar *b)

b == (left >= right)

Definition range_cst.cc:795

Constraint * MakeNonEquality(IntExpr *left, IntExpr *right)

left != right

Definition range_cst.cc:569

IntVar * MakeIsEqualCstVar(IntExpr *var, int64_t value)

status var of (var == value)

IntVar * MakeIsGreaterVar(IntExpr *left, IntExpr *right)

status var of (left > right)

Definition range_cst.cc:801

Constraint * MakeIsGreaterCstCt(IntExpr *v, int64_t c, IntVar *b)

b == (v > c)

IntVar * MakeIsGreaterCstVar(IntExpr *var, int64_t value)

status var of (var > value)

Constraint * MakeLess(IntExpr *left, IntExpr *right)

left < right

Definition range_cst.cc:551

Constraint * MakeGreater(IntExpr *left, IntExpr *right)

left > right

Definition range_cst.cc:565

IntVar * MakeIsDifferentCstVar(IntExpr *var, int64_t value)

status var of (var != value)

IntVar * MakeIsGreaterOrEqualCstVar(IntExpr *var, int64_t value)

status var of (var >= value)

Constraint * MakeIsLessCt(IntExpr *left, IntExpr *right, IntVar *b)

b == (left < right)

Definition range_cst.cc:778

Constraint * MakeEquality(IntExpr *left, IntExpr *right)

left == right

Definition range_cst.cc:517

Constraint * MakeTrueConstraint()

This constraint always succeeds.

Constraint * MakeIsGreaterOrEqualCstCt(IntExpr *var, int64_t value, IntVar *boolvar)

boolvar == (var >= value)

Constraint * MakeIsDifferentCstCt(IntExpr *var, int64_t value, IntVar *boolvar)

boolvar == (var != value)

Demon * MakeConstraintDemon0(Solver *const s, T *const ct, void(T::*method)(), const std::string &name)

std::string DebugString() const

static const int64_t kint64max

static const int64_t kint64min