24#include "absl/cleanup/cleanup.h"
25#include "absl/container/btree_set.h"
26#include "absl/container/flat_hash_map.h"
27#include "absl/container/flat_hash_set.h"
28#include "absl/container/inlined_vector.h"
29#include "absl/log/check.h"
30#include "absl/log/log.h"
31#include "absl/log/vlog_is_on.h"
32#include "absl/types/span.h"
74 if (!add_ub && !add_lb) {
79 AddInternal(expr, ub);
82 AddInternal(expr_for_lb, -lb);
91 if (!is_built_ && max_node >= graph_.num_nodes()) {
92 graph_.AddNode(max_node);
112 for (
const Literal l : enforcements) {
113 CHECK(trail_->Assignment().LiteralIsTrue(l));
117 if (enforcements.empty() || trail_->CurrentDecisionLevel() == 0) {
127 const auto [it, inserted] = best_relations_.insert({expr, rhs});
129 if (rhs >= it->second)
return;
134 const int new_index = conditional_stack_.size();
135 const auto [it, inserted] = conditional_relations_.insert({expr, new_index});
137 CreateLevelEntryIfNeeded();
138 conditional_stack_.emplace_back(-1, rhs, expr, enforcements);
142 std::max(expr.
vars[0].value(), expr.
vars[1].value()) + 1;
143 if (new_size > conditional_after_.size()) {
144 conditional_after_.resize(new_size);
152 const int prev_entry = it->second;
153 DCHECK_LT(rhs, conditional_stack_[prev_entry].rhs);
156 it->second = new_index;
157 CreateLevelEntryIfNeeded();
158 conditional_stack_.emplace_back(prev_entry, rhs, expr, enforcements);
162void PrecedenceRelations::CreateLevelEntryIfNeeded() {
164 if (!level_to_stack_size_.empty() &&
165 level_to_stack_size_.back().first == current)
167 level_to_stack_size_.push_back({current, conditional_stack_.size()});
172 while (!level_to_stack_size_.empty() &&
173 level_to_stack_size_.back().first > level) {
174 const int target = level_to_stack_size_.back().second;
175 DCHECK_GE(conditional_stack_.size(), target);
176 while (conditional_stack_.size() > target) {
177 const ConditionalEntry& back = conditional_stack_.back();
178 if (back.prev_entry != -1) {
179 conditional_relations_[back.key] = back.prev_entry;
180 UpdateBestRelation(back.key, conditional_stack_[back.prev_entry].rhs);
183 conditional_relations_.erase(back.key);
185 if (back.key.
coeffs[0] == 1 && back.key.
coeffs[1] == 1) {
186 DCHECK_EQ(conditional_after_[back.key.
vars[0]].back(),
188 DCHECK_EQ(conditional_after_[back.key.
vars[1]].back(),
190 conditional_after_[back.key.
vars[0]].pop_back();
191 conditional_after_[back.key.
vars[1]].pop_back();
194 conditional_stack_.pop_back();
196 level_to_stack_size_.pop_back();
204 const auto it = root_relations_.find(expr);
205 if (it != root_relations_.end()) {
213 std::vector<Literal>* literal_reason,
214 std::vector<IntegerLiteral>* )
const {
218 const auto it = conditional_relations_.find(expr);
219 DCHECK(it != conditional_relations_.end());
221 const ConditionalEntry& entry = conditional_stack_[it->second];
223 for (
const Literal l : entry.enforcements) {
224 CHECK(trail_->Assignment().LiteralIsTrue(l));
228 DCHECK_LE(
CapProdI(gcd, entry.rhs), ub);
229 for (
const Literal l : entry.enforcements) {
230 literal_reason->push_back(l.
Negated());
237 const auto it = best_relations_.find(expr);
238 if (it != best_relations_.end()) {
241 DCHECK(!root_relations_.contains(expr));
242 DCHECK(!conditional_relations_.contains(expr));
247 if (is_built_)
return;
250 const int num_nodes = graph_.num_nodes();
256 CHECK(arc_offsets_.empty());
257 graph_.ReserveArcs(2 * root_relations_.size());
258 std::vector<std::pair<LinearExpression2, IntegerValue>> root_relations_sorted(
259 root_relations_.begin(), root_relations_.end());
260 std::sort(root_relations_sorted.begin(), root_relations_sorted.end());
261 for (
const auto [var_pair, negated_offset] : root_relations_sorted) {
267 const IntegerValue offset = -negated_offset;
268 if (offset < 0)
continue;
270 if (var_pair.coeffs[0] != 1 || var_pair.coeffs[1] != 1) {
277 const IntegerVariable tail = var_pair.vars[0];
278 const IntegerVariable head =
NegationOf(var_pair.vars[1]);
279 graph_.AddArc(tail.value(), head.value());
280 arc_offsets_.push_back(offset);
281 CHECK_LT(var_pair.vars[1], before.size());
285 const IntegerVariable tail = var_pair.vars[1];
286 const IntegerVariable head =
NegationOf(var_pair.vars[0]);
287 graph_.AddArc(tail.value(), head.value());
288 arc_offsets_.push_back(offset);
289 CHECK_LT(var_pair.vars[1], before.size());
294 std::vector<int> permutation;
295 graph_.Build(&permutation);
308 for (
int arc = 0; arc < graph_.num_arcs(); ++arc) {
309 sorter.
AddEdge(graph_.Tail(arc), graph_.Head(arc));
312 bool graph_has_cycle =
false;
313 topological_order_.clear();
314 while (sorter.
GetNext(&next, &graph_has_cycle,
nullptr)) {
315 topological_order_.push_back(IntegerVariable(next));
316 if (graph_has_cycle) {
321 is_dag_ = !graph_has_cycle;
325 if (!is_dag_)
return;
328 const int kWorkLimit = 1e6;
329 for (
const IntegerVariable tail_var : topological_order_) {
330 if (++work > kWorkLimit)
break;
331 for (
const int arc : graph_.OutgoingArcs(tail_var.value())) {
332 DCHECK_EQ(tail_var.value(), graph_.Tail(arc));
333 const IntegerVariable head_var = IntegerVariable(graph_.Head(arc));
334 const IntegerValue arc_offset = arc_offsets_[arc];
336 if (++work > kWorkLimit)
break;
342 for (
const IntegerVariable before_var : before[tail_var]) {
343 if (++work > kWorkLimit)
break;
346 const IntegerValue offset =
347 -root_relations_.at(expr_for_key) + arc_offset;
356 VLOG(2) <<
"Full precedences. Work=" << work
357 <<
" Relations=" << root_relations_.size();
361 absl::Span<const IntegerVariable> vars,
362 std::vector<FullIntegerPrecedence>* output) {
364 if (!is_built_)
Build();
365 if (!is_dag_)
return;
367 VLOG(2) <<
"num_nodes: " << graph_.num_nodes()
368 <<
" num_arcs: " << graph_.num_arcs() <<
" is_dag: " << is_dag_;
375 absl::flat_hash_set<IntegerVariable> is_interesting;
376 absl::flat_hash_set<IntegerVariable> to_consider(vars.begin(), vars.end());
377 absl::flat_hash_map<IntegerVariable,
378 absl::flat_hash_map<IntegerVariable, IntegerValue>>
379 vars_before_with_offset;
380 absl::flat_hash_map<IntegerVariable, IntegerValue> tail_map;
381 for (
const IntegerVariable tail_var : topological_order_) {
382 if (!to_consider.contains(tail_var) &&
383 !vars_before_with_offset.contains(tail_var)) {
391 const auto it = vars_before_with_offset.find(tail_var);
392 if (it != vars_before_with_offset.end()) {
393 tail_map = it->second;
397 for (
const int arc : graph_.OutgoingArcs(tail_var.value())) {
398 CHECK_EQ(tail_var.value(), graph_.Tail(arc));
399 const IntegerVariable head_var = IntegerVariable(graph_.Head(arc));
400 const IntegerValue arc_offset = arc_offsets_[arc];
403 if (tail_map.empty() && !to_consider.contains(tail_var))
continue;
405 auto& to_update = vars_before_with_offset[head_var];
406 for (
const auto& [var_before, offset] : tail_map) {
407 if (!to_update.contains(var_before)) {
408 to_update[var_before] = arc_offset + offset;
410 to_update[var_before] =
411 std::max(arc_offset + offset, to_update[var_before]);
414 if (to_consider.contains(tail_var)) {
415 if (!to_update.contains(tail_var)) {
416 to_update[tail_var] = arc_offset;
418 to_update[tail_var] = std::max(arc_offset, to_update[tail_var]);
426 if (to_update.size() > tail_map.size() + 1) {
427 is_interesting.insert(head_var);
429 is_interesting.erase(head_var);
437 if (!is_interesting.contains(tail_var))
continue;
438 if (tail_map.size() == 1)
continue;
443 for (
int i = 0;
i < vars.size(); ++
i) {
444 const auto offset_it = tail_map.find(vars[
i]);
445 if (offset_it == tail_map.end())
continue;
447 data.
offsets.push_back(offset_it->second);
448 min_offset = std::min(data.
offsets.back(), min_offset);
450 output->push_back(std::move(data));
455 absl::Span<const IntegerVariable> vars,
456 std::vector<PrecedenceData>* output) {
458 const int needed_size =
459 std::max(after_.size(), conditional_after_.size()) + 1;
460 var_to_degree_.resize(needed_size);
461 var_to_last_index_.resize(needed_size);
462 var_with_positive_degree_.resize(needed_size);
463 tmp_precedences_.clear();
467 int num_relevants = 0;
468 IntegerVariable* var_with_positive_degree = var_with_positive_degree_.data();
469 int* var_to_degree = var_to_degree_.data();
470 int* var_to_last_index = var_to_last_index_.data();
471 const auto process = [&](
int index, absl::Span<const IntegerVariable> v) {
472 for (
const IntegerVariable after : v) {
473 DCHECK_LT(after, needed_size);
474 if (var_to_degree[after.value()] == 0) {
475 var_with_positive_degree[num_relevants++] = after;
478 if (var_to_last_index[after.value()] == index)
continue;
481 tmp_precedences_.push_back({after, index});
482 var_to_degree[after.value()]++;
483 var_to_last_index[after.value()] = index;
487 for (
int index = 0; index < vars.size(); ++index) {
488 const IntegerVariable var = vars[index];
489 if (var < after_.size()) {
490 process(index, after_[var]);
492 if (var < conditional_after_.size()) {
493 process(index, conditional_after_[var]);
501 for (
int i = 0;
i < num_relevants; ++
i) {
502 const IntegerVariable var = var_with_positive_degree[
i];
503 const int degree = var_to_degree[var.value()];
505 var_to_degree[var.value()] = start;
509 var_to_degree[var.value()] = -1;
513 output->resize(start);
514 for (
const auto& precedence : tmp_precedences_) {
516 const int pos = var_to_degree[precedence.var.value()]++;
517 if (pos < 0)
continue;
518 (*output)[pos] = precedence;
523 for (
int i = 0;
i < num_relevants; ++
i) {
524 const IntegerVariable var = var_with_positive_degree[
i];
525 var_to_degree[var.value()] = 0;
531void AppendLowerBoundReasonIfValid(IntegerVariable var,
533 std::vector<IntegerLiteral>* reason) {
542 if (!VLOG_IS_ON(1))
return;
543 if (shared_stats_ ==
nullptr)
return;
544 std::vector<std::pair<std::string, int64_t>> stats;
545 stats.push_back({
"precedences/num_cycles", num_cycles_});
546 stats.push_back({
"precedences/num_pushes", num_pushes_});
548 {
"precedences/num_enforcement_pushes", num_enforcement_pushes_});
549 shared_stats_->AddStats(stats);
557 if (literal.
Index() >= literal_to_new_impacted_arcs_.size())
continue;
561 for (
const ArcIndex arc_index :
562 literal_to_new_impacted_arcs_[literal.
Index()]) {
563 if (--arc_counts_[arc_index] == 0) {
564 const ArcInfo& arc = arcs_[arc_index];
565 PushConditionalRelations(arc);
566 impacted_arcs_[arc.tail_var].push_back(arc_index);
572 for (
const ArcIndex arc_index :
573 literal_to_new_impacted_arcs_[literal.
Index()]) {
574 if (arc_counts_[arc_index] > 0)
continue;
575 const ArcInfo& arc = arcs_[arc_index];
576 const IntegerValue new_head_lb =
577 integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc);
578 if (new_head_lb > integer_trail_->LowerBound(arc.head_var)) {
579 if (!EnqueueAndCheck(arc, new_head_lb, trail_))
return false;
585 InitializeBFQueueWithModifiedNodes();
586 if (!BellmanFordTarjan(trail_))
return false;
596 DCHECK(NoPropagationLeft(*trail_));
600 PropagateOptionalArcs(trail_);
603 modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
609 if (var >= impacted_arcs_.size())
return true;
610 for (
const ArcIndex arc_index : impacted_arcs_[var]) {
611 const ArcInfo& arc = arcs_[arc_index];
612 const IntegerValue new_head_lb =
613 integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc);
614 if (new_head_lb > integer_trail_->LowerBound(arc.head_var)) {
615 if (!EnqueueAndCheck(arc, new_head_lb, trail_))
return false;
622void PrecedencesPropagator::PushConditionalRelations(
const ArcInfo& arc) {
627 const IntegerValue offset = ArcOffset(arc);
629 arc.presence_literals,
638 modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
642 if (literal.
Index() >= literal_to_new_impacted_arcs_.size())
continue;
643 for (
const ArcIndex arc_index :
644 literal_to_new_impacted_arcs_[literal.
Index()]) {
645 if (arc_counts_[arc_index]++ == 0) {
646 const ArcInfo& arc = arcs_[arc_index];
647 impacted_arcs_[arc.tail_var].pop_back();
653void PrecedencesPropagator::AdjustSizeFor(IntegerVariable
i) {
654 const int index = std::max(
i.value(),
NegationOf(
i).value());
655 if (index >= impacted_arcs_.size()) {
658 for (IntegerVariable var(impacted_arcs_.size()); var <= index; ++var) {
661 impacted_arcs_.
resize(index + 1);
662 impacted_potential_arcs_.
resize(index + 1);
666void PrecedencesPropagator::AddArc(
667 IntegerVariable tail, IntegerVariable head, IntegerValue offset,
668 IntegerVariable offset_var, absl::Span<const Literal> presence_literals) {
674 absl::InlinedVector<Literal, 6> enforcement_literals;
676 for (
const Literal l : presence_literals) {
677 enforcement_literals.push_back(l);
681 if (trail_->CurrentDecisionLevel() == 0) {
683 for (
const Literal l : enforcement_literals) {
684 if (trail_->Assignment().LiteralIsTrue(Literal(l))) {
686 }
else if (trail_->Assignment().LiteralIsFalse(Literal(l))) {
689 enforcement_literals[new_size++] = l;
691 enforcement_literals.resize(new_size);
699 VLOG(1) <<
"Self arc! This could be presolved. "
700 <<
"var:" << tail <<
" offset:" << offset
701 <<
" offset_var:" << offset_var
702 <<
" conditioned_by:" << presence_literals;
708 const IntegerValue lb = integer_trail_->LevelZeroLowerBound(offset_var);
709 if (lb == integer_trail_->LevelZeroUpperBound(offset_var)) {
716 if (!enforcement_literals.empty()) {
717 const OptionalArcIndex arc_index(potential_arcs_.size());
718 potential_arcs_.push_back(
719 {tail, head, offset, offset_var, enforcement_literals});
720 impacted_potential_arcs_[tail].push_back(arc_index);
721 impacted_potential_arcs_[
NegationOf(head)].push_back(arc_index);
723 impacted_potential_arcs_[offset_var].push_back(arc_index);
729 IntegerVariable tail_var;
730 IntegerVariable head_var;
731 IntegerVariable offset_var;
733 std::vector<InternalArc> to_add;
741 to_add.push_back({tail, head, offset_var});
742 to_add.push_back({offset_var, head, tail});
750 for (
const InternalArc a : to_add) {
765 modified_vars_.Set(a.tail_var);
769 const ArcIndex arc_index(arcs_.size());
771 {a.tail_var, a.head_var, offset, a.offset_var, enforcement_literals});
772 auto& presence_literals = arcs_.back().presence_literals;
774 if (presence_literals.empty()) {
775 impacted_arcs_[a.tail_var].push_back(arc_index);
777 for (
const Literal l : presence_literals) {
778 if (l.Index() >= literal_to_new_impacted_arcs_.size()) {
779 literal_to_new_impacted_arcs_.resize(l.Index().value() + 1);
781 literal_to_new_impacted_arcs_[l.Index()].push_back(arc_index);
785 if (trail_->CurrentDecisionLevel() == 0) {
786 arc_counts_.push_back(presence_literals.size());
788 arc_counts_.push_back(0);
789 for (
const Literal l : presence_literals) {
790 if (!trail_->Assignment().LiteralIsTrue(l)) {
791 ++arc_counts_.back();
794 CHECK(presence_literals.empty() || arc_counts_.back() > 0);
801 IntegerValue offset) {
802 DCHECK_EQ(trail_->CurrentDecisionLevel(), 0);
803 if (i1 < impacted_arcs_.size() && i2 < impacted_arcs_.size()) {
804 for (
const ArcIndex index : impacted_arcs_[i1]) {
805 const ArcInfo& arc = arcs_[index];
806 if (arc.head_var == i2) {
807 const IntegerValue current = ArcOffset(arc);
808 if (offset <= current) {
827void PrecedencesPropagator::PropagateOptionalArcs(
Trail* trail) {
830 if (var >= impacted_potential_arcs_.size())
continue;
834 for (
const OptionalArcIndex arc_index : impacted_potential_arcs_[var]) {
835 const ArcInfo& arc = potential_arcs_[arc_index];
836 int num_not_true = 0;
838 for (
const Literal l : arc.presence_literals) {
844 if (num_not_true != 1)
continue;
849 const IntegerValue tail_lb = integer_trail_->
LowerBound(arc.tail_var);
850 const IntegerValue head_ub = integer_trail_->
UpperBound(arc.head_var);
851 if (tail_lb + ArcOffset(arc) > head_ub) {
852 integer_reason_.clear();
853 integer_reason_.push_back(
855 integer_reason_.push_back(
857 AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
859 literal_reason_.clear();
860 for (
const Literal l : arc.presence_literals) {
861 if (l != to_propagate) literal_reason_.push_back(l.Negated());
863 ++num_enforcement_pushes_;
864 integer_trail_->EnqueueLiteral(to_propagate.
Negated(), literal_reason_,
871IntegerValue PrecedencesPropagator::ArcOffset(
const ArcInfo& arc)
const {
874 : integer_trail_->
LowerBound(arc.offset_var));
877bool PrecedencesPropagator::EnqueueAndCheck(
const ArcInfo& arc,
878 IntegerValue new_head_lb,
881 DCHECK_GT(new_head_lb, integer_trail_->LowerBound(arc.head_var));
888 literal_reason_.clear();
889 for (
const Literal l : arc.presence_literals) {
890 literal_reason_.push_back(l.Negated());
893 integer_reason_.clear();
894 integer_reason_.push_back(integer_trail_->LowerBoundAsLiteral(arc.tail_var));
895 AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
906 if (new_head_lb > integer_trail_->UpperBound(arc.head_var)) {
907 const IntegerValue slack =
908 new_head_lb - integer_trail_->UpperBound(arc.head_var) - 1;
909 integer_reason_.push_back(
910 integer_trail_->UpperBoundAsLiteral(arc.head_var));
911 std::vector<IntegerValue> coeffs(integer_reason_.size(), IntegerValue(1));
912 integer_trail_->RelaxLinearReason(slack, coeffs, &integer_reason_);
913 return integer_trail_->ReportConflict(literal_reason_, integer_reason_);
916 return integer_trail_->Enqueue(
918 literal_reason_, integer_reason_);
921bool PrecedencesPropagator::NoPropagationLeft(
const Trail& trail)
const {
922 const int num_nodes = impacted_arcs_.size();
923 for (IntegerVariable var(0); var < num_nodes; ++var) {
924 for (
const ArcIndex arc_index : impacted_arcs_[var]) {
925 const ArcInfo& arc = arcs_[arc_index];
926 if (integer_trail_->LowerBound(arc.tail_var) + ArcOffset(arc) >
927 integer_trail_->LowerBound(arc.head_var)) {
935void PrecedencesPropagator::InitializeBFQueueWithModifiedNodes() {
938 const int num_nodes = impacted_arcs_.size();
939 bf_in_queue_.resize(num_nodes,
false);
940 for (
const int node : bf_queue_) bf_in_queue_[node] =
false;
942 DCHECK(std::none_of(bf_in_queue_.begin(), bf_in_queue_.end(),
943 [](
bool v) { return v; }));
944 for (
const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
945 if (var >= num_nodes)
continue;
946 bf_queue_.push_back(var.value());
947 bf_in_queue_[var.value()] =
true;
951void PrecedencesPropagator::CleanUpMarkedArcsAndParents() {
954 const int num_nodes = impacted_arcs_.size();
955 for (
const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
956 if (var >= num_nodes)
continue;
957 const ArcIndex parent_arc_index = bf_parent_arc_of_[var.value()];
958 if (parent_arc_index != -1) {
959 arcs_[parent_arc_index].is_marked =
false;
960 bf_parent_arc_of_[var.value()] = -1;
961 bf_can_be_skipped_[var.value()] =
false;
964 DCHECK(std::none_of(bf_parent_arc_of_.begin(), bf_parent_arc_of_.end(),
965 [](ArcIndex v) { return v != -1; }));
966 DCHECK(std::none_of(bf_can_be_skipped_.begin(), bf_can_be_skipped_.end(),
967 [](
bool v) { return v; }));
970bool PrecedencesPropagator::DisassembleSubtree(
971 int source,
int target, std::vector<bool>* can_be_skipped) {
975 tmp_vector_.push_back(source);
976 while (!tmp_vector_.empty()) {
977 const int tail = tmp_vector_.back();
978 tmp_vector_.pop_back();
979 for (
const ArcIndex arc_index : impacted_arcs_[IntegerVariable(tail)]) {
980 const ArcInfo& arc = arcs_[arc_index];
982 arc.is_marked =
false;
983 if (arc.head_var.value() == target)
return true;
984 DCHECK(!(*can_be_skipped)[arc.head_var.value()]);
985 (*can_be_skipped)[arc.head_var.value()] =
true;
986 tmp_vector_.push_back(arc.head_var.value());
993void PrecedencesPropagator::AnalyzePositiveCycle(
994 ArcIndex first_arc,
Trail* trail, std::vector<Literal>* must_be_all_true,
995 std::vector<Literal>* literal_reason,
996 std::vector<IntegerLiteral>* integer_reason) {
997 must_be_all_true->clear();
998 literal_reason->clear();
999 integer_reason->clear();
1002 const IntegerVariable first_arc_head = arcs_[first_arc].head_var;
1003 ArcIndex arc_index = first_arc;
1004 std::vector<ArcIndex> arc_on_cycle;
1010 const int num_nodes = impacted_arcs_.size();
1011 while (arc_on_cycle.size() <= num_nodes) {
1012 arc_on_cycle.push_back(arc_index);
1013 const ArcInfo& arc = arcs_[arc_index];
1014 if (arc.tail_var == first_arc_head)
break;
1015 arc_index = bf_parent_arc_of_[arc.tail_var.value()];
1016 CHECK_NE(arc_index, ArcIndex(-1));
1018 CHECK_NE(arc_on_cycle.size(), num_nodes + 1) <<
"Infinite loop.";
1021 IntegerValue sum(0);
1022 for (
const ArcIndex arc_index : arc_on_cycle) {
1023 const ArcInfo& arc = arcs_[arc_index];
1024 sum += ArcOffset(arc);
1025 AppendLowerBoundReasonIfValid(arc.offset_var, *integer_trail_,
1027 for (
const Literal l : arc.presence_literals) {
1028 literal_reason->push_back(l.Negated());
1042bool PrecedencesPropagator::BellmanFordTarjan(
Trail* trail) {
1043 const int num_nodes = impacted_arcs_.size();
1046 bf_can_be_skipped_.resize(num_nodes,
false);
1047 bf_parent_arc_of_.resize(num_nodes, ArcIndex(-1));
1048 const auto cleanup =
1049 ::absl::MakeCleanup([
this]() { CleanUpMarkedArcsAndParents(); });
1052 while (!bf_queue_.empty()) {
1053 const int node = bf_queue_.front();
1054 bf_queue_.pop_front();
1055 bf_in_queue_[node] =
false;
1065 if (bf_can_be_skipped_[node]) {
1066 DCHECK_NE(bf_parent_arc_of_[node], -1);
1067 DCHECK(!arcs_[bf_parent_arc_of_[node]].is_marked);
1071 const IntegerValue tail_lb =
1072 integer_trail_->LowerBound(IntegerVariable(node));
1073 for (
const ArcIndex arc_index : impacted_arcs_[IntegerVariable(node)]) {
1074 const ArcInfo& arc = arcs_[arc_index];
1075 DCHECK_EQ(arc.tail_var, node);
1076 const IntegerValue candidate = tail_lb + ArcOffset(arc);
1077 if (candidate > integer_trail_->LowerBound(arc.head_var)) {
1078 if (!EnqueueAndCheck(arc, candidate, trail))
return false;
1086 if (DisassembleSubtree(arc.head_var.value(), arc.tail_var.value(),
1087 &bf_can_be_skipped_)) {
1088 std::vector<Literal> must_be_all_true;
1089 AnalyzePositiveCycle(arc_index, trail, &must_be_all_true,
1090 &literal_reason_, &integer_reason_);
1091 if (must_be_all_true.empty()) {
1093 return integer_trail_->ReportConflict(literal_reason_,
1097 for (
const Literal l : must_be_all_true) {
1098 if (trail_->Assignment().LiteralIsFalse(l)) {
1099 literal_reason_.push_back(l);
1100 return integer_trail_->ReportConflict(literal_reason_,
1104 for (
const Literal l : must_be_all_true) {
1105 if (trail_->Assignment().LiteralIsTrue(l))
continue;
1106 integer_trail_->EnqueueLiteral(l, literal_reason_,
1119 if (bf_parent_arc_of_[arc.head_var.value()] != -1) {
1120 arcs_[bf_parent_arc_of_[arc.head_var.value()]].is_marked =
false;
1129 const IntegerValue new_bound = integer_trail_->LowerBound(arc.head_var);
1130 if (new_bound == candidate) {
1131 bf_parent_arc_of_[arc.head_var.value()] = arc_index;
1132 arcs_[arc_index].is_marked =
true;
1136 bf_parent_arc_of_[arc.head_var.value()] = -1;
1141 bf_can_be_skipped_[arc.head_var.value()] =
false;
1142 if (!bf_in_queue_[arc.head_var.value()] && new_bound >= candidate) {
1143 bf_queue_.push_back(arc.head_var.value());
1144 bf_in_queue_[arc.head_var.value()] =
true;
1153 IntegerValue lhs, IntegerValue rhs) {
1155 num_enforced_relations_++;
1159 DCHECK_NE(a.
coeff, 0);
1160 DCHECK_NE(
b.coeff, 0);
1182 relations_.push_back(std::move(r));
1187 IntegerVariable
b) {
1197 std::vector<std::pair<LiteralIndex, int>> literal_key_values;
1198 std::vector<std::pair<IntegerVariable, int>> var_key_values;
1199 const int num_relations = relations_.size();
1200 literal_key_values.reserve(num_enforced_relations_);
1201 var_key_values.reserve(num_relations - num_enforced_relations_);
1202 for (
int i = 0;
i < num_relations; ++
i) {
1205 var_key_values.emplace_back(r.
a.
var,
i);
1206 var_key_values.emplace_back(r.
b.
var,
i);
1207 std::pair<IntegerVariable, IntegerVariable> key(r.
a.
var, r.
b.
var);
1208 if (relations_[
i].a.var > relations_[
i].b.var) {
1209 std::swap(key.first, key.second);
1211 var_pair_to_relations_[key].push_back(
i);
1216 lit_to_relations_.ResetFromPairs(literal_key_values);
1217 var_to_relations_.ResetFromPairs(var_key_values);
1222 const absl::flat_hash_map<IntegerVariable, IntegerValue>&
input,
1223 absl::flat_hash_map<IntegerVariable, IntegerValue>* output)
const {
1226 auto get_lower_bound = [&](IntegerVariable var) {
1227 const auto it =
input.find(var);
1228 if (it !=
input.end())
return it->second;
1231 auto get_upper_bound = [&](IntegerVariable var) {
1234 auto update_lower_bound_by_var = [&](IntegerVariable var, IntegerValue lb) {
1236 const auto [it, inserted] = output->insert({var, lb});
1238 it->second = std::max(it->second, lb);
1241 auto update_upper_bound_by_var = [&](IntegerVariable var, IntegerValue ub) {
1242 update_lower_bound_by_var(
NegationOf(var), -ub);
1245 IntegerValue lhs, IntegerValue rhs) {
1246 if (a.
coeff == 0)
return;
1251 lhs = lhs -
b.coeff * get_upper_bound(
b.var);
1252 rhs = rhs -
b.coeff * get_lower_bound(
b.var);
1257 auto update_var_bounds_from_relation = [&](
Relation r) {
1258 r.a.MakeCoeffPositive();
1259 r.b.MakeCoeffPositive();
1260 update_var_bounds(r.a, r.b, r.lhs, r.rhs);
1261 update_var_bounds(r.b, r.a, r.lhs, r.rhs);
1263 if (lit.
Index() < lit_to_relations_.size()) {
1264 for (
const int relation_index : lit_to_relations_[lit]) {
1265 update_var_bounds_from_relation(relations_[relation_index]);
1268 for (
const auto& [var, _] :
input) {
1269 if (var >= var_to_relations_.size())
continue;
1270 for (
const int relation_index : var_to_relations_[var]) {
1271 update_var_bounds_from_relation(relations_[relation_index]);
1277 for (
const auto [var, lb] : *output) {
1283bool GreaterThanAtLeastOneOfDetector::AddRelationFromIndices(
1284 IntegerVariable var, absl::Span<const Literal> clause,
1285 absl::Span<const int> indices,
Model* model) {
1286 std::vector<AffineExpression> exprs;
1287 std::vector<Literal> selectors;
1288 absl::flat_hash_set<LiteralIndex> used;
1292 for (
const int index : indices) {
1304 exprs.push_back(AffineExpression(r.
b.
var, r.
b.
coeff, -r.
rhs));
1308 if (var_lb >= integer_trail->LevelZeroUpperBound(exprs.back())) {
1320 std::vector<Literal> enforcements;
1321 for (
const Literal l : clause) {
1322 if (!used.contains(l.Index())) {
1323 enforcements.push_back(l.Negated());
1329 if (used.size() <= 1)
return false;
1332 GreaterThanAtLeastOneOfPropagator* constraint =
1333 new GreaterThanAtLeastOneOfPropagator(var, exprs, selectors, enforcements,
1335 constraint->RegisterWith(model->
GetOrCreate<GenericLiteralWatcher>());
1340int GreaterThanAtLeastOneOfDetector::
1341 AddGreaterThanAtLeastOneOfConstraintsFromClause(
1342 const absl::Span<const Literal> clause,
Model* model) {
1343 CHECK_EQ(model->GetOrCreate<Trail>()->CurrentDecisionLevel(), 0);
1344 if (clause.size() < 2)
return 0;
1347 std::vector<std::pair<IntegerVariable, int>> infos;
1348 for (
const Literal l : clause) {
1349 for (
const int index :
1350 repository_.IndicesOfRelationsEnforcedBy(l.Index())) {
1351 const Relation& r = repository_.relation(index);
1353 infos.push_back({r.a.var, index});
1356 infos.push_back({r.b.var, index});
1360 if (infos.size() <= 1)
return 0;
1363 std::stable_sort(infos.begin(), infos.end());
1366 int num_added_constraints = 0;
1367 std::vector<int> indices;
1368 for (
int i = 0;
i < infos.size();) {
1369 const int start =
i;
1370 const IntegerVariable var = infos[start].first;
1373 for (;
i < infos.size() && infos[
i].first == var; ++
i) {
1374 indices.push_back(infos[
i].second);
1378 if (indices.size() < 2)
continue;
1384 if (indices.size() + 1 < clause.size())
continue;
1386 if (AddRelationFromIndices(var, clause, indices, model)) {
1387 ++num_added_constraints;
1389 if (AddRelationFromIndices(
NegationOf(var), clause, indices, model)) {
1390 ++num_added_constraints;
1393 return num_added_constraints;
1396int GreaterThanAtLeastOneOfDetector::
1397 AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection(
Model* model) {
1398 auto*
time_limit = model->GetOrCreate<TimeLimit>();
1399 auto* solver = model->GetOrCreate<SatSolver>();
1402 util_intops::StrongVector<IntegerVariable, std::vector<int>> var_to_relations;
1403 for (
int index = 0; index < repository_.size(); ++index) {
1404 const Relation& r = repository_.relation(index);
1407 if (r.a.var >= var_to_relations.size()) {
1408 var_to_relations.resize(r.a.var + 1);
1410 var_to_relations[r.a.var].push_back(index);
1413 if (r.b.var >= var_to_relations.size()) {
1414 var_to_relations.resize(r.b.var + 1);
1416 var_to_relations[r.b.var].push_back(index);
1420 int num_added_constraints = 0;
1421 for (IntegerVariable target(0); target < var_to_relations.size(); ++target) {
1422 if (var_to_relations[target].size() <= 1)
continue;
1423 if (
time_limit->LimitReached())
return num_added_constraints;
1428 solver->Backtrack(0);
1429 if (solver->ModelIsUnsat())
return num_added_constraints;
1430 std::vector<Literal> clause;
1431 for (
const int index : var_to_relations[target]) {
1432 const Literal literal = repository_.relation(index).enforcement;
1433 if (solver->Assignment().LiteralIsFalse(literal))
continue;
1435 solver->EnqueueDecisionAndBacktrackOnConflict(literal.Negated());
1439 clause = solver->GetLastIncompatibleDecisions();
1440 for (Literal& ref : clause) ref = ref.Negated();
1444 solver->Backtrack(0);
1445 if (clause.size() <= 1)
continue;
1448 const absl::btree_set<Literal> clause_set(clause.begin(), clause.end());
1450 std::vector<int> indices;
1451 for (
const int index : var_to_relations[target]) {
1452 const Literal literal = repository_.relation(index).enforcement;
1453 if (clause_set.contains(literal)) {
1454 indices.push_back(index);
1459 if (AddRelationFromIndices(target, clause, indices, model)) {
1460 ++num_added_constraints;
1462 if (AddRelationFromIndices(
NegationOf(target), clause, indices, model)) {
1463 ++num_added_constraints;
1467 solver->Backtrack(0);
1468 return num_added_constraints;
1472 Model* model,
bool auto_detect_clauses) {
1478 int num_added_constraints = 0;
1479 SOLVER_LOG(logger,
"[Precedences] num_relations=", repository_.size(),
1480 " num_clauses=", clauses->AllClausesInCreationOrder().size());
1488 if (!auto_detect_clauses &&
1489 clauses->AllClausesInCreationOrder().size() < 1e6) {
1497 for (
const SatClause* clause : clauses->AllClausesInCreationOrder()) {
1498 if (
time_limit->LimitReached())
return num_added_constraints;
1499 if (solver->ModelIsUnsat())
return num_added_constraints;
1500 num_added_constraints += AddGreaterThanAtLeastOneOfConstraintsFromClause(
1501 clause->AsSpan(), model);
1508 const int num_booleans = solver->NumVariables();
1509 if (num_booleans < 1e6) {
1510 for (
int i = 0;
i < num_booleans; ++
i) {
1511 if (
time_limit->LimitReached())
return num_added_constraints;
1512 if (solver->ModelIsUnsat())
return num_added_constraints;
1513 num_added_constraints +=
1514 AddGreaterThanAtLeastOneOfConstraintsFromClause(
1515 {
Literal(BooleanVariable(
i),
true),
1516 Literal(BooleanVariable(
i),
false)},
1522 num_added_constraints +=
1523 AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection(model);
1526 if (num_added_constraints > 0) {
1527 SOLVER_LOG(logger,
"[Precedences] Added ", num_added_constraints,
1528 " GreaterThanAtLeastOneOf() constraints.");
1531 return num_added_constraints;
1542 DCHECK_EQ(trail->CurrentDecisionLevel(), 0);
1543 absl::flat_hash_set<Literal> relevant_true_literals;
1544 for (; index < trail->Index(); ++index) {
1545 const Literal l = (*trail)[index];
1546 if (variable_appearing_in_reified_relations_.contains(l.Variable())) {
1547 relevant_true_literals.insert(l);
1550 if (relevant_true_literals.empty())
return true;
1553 for (
const auto [l, expr, ub] : all_reified_relations_) {
1554 if (relevant_true_literals.contains(l)) {
1556 VLOG(2) <<
"New fixed precedence: " << expr <<
" <= " << ub
1557 <<
" (was reified by " << l <<
")";
1558 }
else if (relevant_true_literals.contains(l.Negated())) {
1560 VLOG(2) <<
"New fixed precedence: " << expr <<
" > " << ub
1561 <<
" (was reified by not(" << l <<
"))";
1569 if (!VLOG_IS_ON(1))
return;
1570 std::vector<std::pair<std::string, int64_t>> stats;
1571 stats.push_back({
"BinaryRelationsMaps/num_relations", num_updates_});
1573 {
"BinaryRelationsMaps/num_affine_updates", num_affine_updates_});
1574 shared_stats_->AddStats(stats);
1577IntegerValue BinaryRelationsMaps::GetImpliedUpperBound(
1579 DCHECK_GE(expr.
coeffs[0], 0);
1580 DCHECK_GE(expr.
coeffs[1], 0);
1581 IntegerValue implied_ub = 0;
1582 for (
const int i : {0, 1}) {
1583 if (expr.
coeffs[i] > 0) {
1584 implied_ub += expr.
coeffs[i] * integer_trail_->UpperBound(expr.
vars[i]);
1590std::pair<IntegerValue, IntegerValue>
1591BinaryRelationsMaps::GetImpliedLevelZeroBounds(
1592 const LinearExpression2& expr)
const {
1594 IntegerValue implied_lb = 0;
1595 IntegerValue implied_ub = 0;
1596 if (expr.coeffs[0] != 0) {
1597 CHECK_GE(expr.vars[0], 0);
1599 expr.coeffs[0] * integer_trail_->LevelZeroLowerBound(expr.vars[0]);
1601 expr.coeffs[0] * integer_trail_->LevelZeroUpperBound(expr.vars[0]);
1603 if (expr.coeffs[1] != 0) {
1604 CHECK_GE(expr.vars[1], 0);
1606 expr.coeffs[1] * integer_trail_->LevelZeroLowerBound(expr.vars[1]);
1608 expr.coeffs[1] * integer_trail_->LevelZeroUpperBound(expr.vars[1]);
1611 return {implied_lb, implied_ub};
1615 IntegerValue lb, IntegerValue ub) {
1617 const auto [implied_lb, implied_ub] = GetImpliedLevelZeroBounds(expr);
1618 lb = std::max(lb, implied_lb);
1619 ub = std::min(ub, implied_ub);
1621 if (lb > ub)
return;
1622 if (lb == implied_lb && ub == implied_ub)
return;
1624 if (best_root_level_bounds_.Add(expr, lb, ub)) {
1633 IntegerValue ub)
const {
1635 const auto [implied_lb, implied_ub] = GetImpliedLevelZeroBounds(expr);
1636 lb = std::max(lb, implied_lb);
1637 ub = std::min(ub, implied_ub);
1647 return best_root_level_bounds_.GetStatus(expr, lb, ub);
1650std::pair<LinearExpression2, IntegerValue> BinaryRelationsMaps::FromDifference(
1654 expr.
vars[1] =
b.var;
1658 IntegerValue ub =
b.constant - a.
constant;
1660 return {std::move(expr), ub};
1665 const auto [expr, ub] = FromDifference(a,
b);
1672 const auto [expr, ub] = FromDifference(a,
b);
1676 relation_to_lit_.insert({{expr, ub}, l});
1678 variable_appearing_in_reified_relations_.insert(l.
Variable());
1679 all_reified_relations_.push_back({l, expr, ub});
1684 const auto [expr, ub] = FromDifference(a,
b);
1687 return integer_encoder_->GetTrueLiteral().Index();
1690 return integer_encoder_->GetFalseLiteral().Index();
1693 const auto it = relation_to_lit_.find({expr, ub});
1700 const IntegerValue new_ub = integer_trail_->UpperBound(affine_ub);
1704 if (GetImpliedUpperBound(expr) <= new_ub)
return false;
1707 if (best_root_level_bounds_.GetUpperBound(expr) <= new_ub)
return false;
1711 const auto it = best_affine_ub_.find(expr);
1712 if (it != best_affine_ub_.end()) {
1713 const auto [old_affine_ub, old_gcd] = it->second;
1716 if (old_affine_ub == affine_ub && old_gcd == gcd) {
1718 NotifyWatchingPropagators();
1721 const IntegerValue old_ub =
1722 FloorRatio(integer_trail_->UpperBound(old_affine_ub), old_gcd);
1723 if (old_ub <= new_ub)
return false;
1728 ++num_affine_updates_;
1729 best_affine_ub_[expr] = {affine_ub, gcd};
1730 NotifyWatchingPropagators();
1734void BinaryRelationsMaps::NotifyWatchingPropagators()
const {
1735 for (
const int id : propagator_ids_) {
1736 watcher_->CallOnNextPropagate(
id);
1743 const IntegerValue trivial_ub = GetImpliedUpperBound(expr);
1744 const IntegerValue root_level_ub =
1745 best_root_level_bounds_.GetUpperBound(expr);
1746 const IntegerValue best_ub = std::min(root_level_ub, trivial_ub);
1749 const auto it = best_affine_ub_.find(expr);
1750 if (it == best_affine_ub_.end()) {
1753 const auto [affine, divisor] = it->second;
1754 const IntegerValue canonical_ub =
1755 FloorRatio(integer_trail_->UpperBound(affine), divisor);
1756 return std::min(best_ub,
CapProdI(gcd, canonical_ub));
1763 std::vector<Literal>* ,
1764 std::vector<IntegerLiteral>* integer_reason)
const {
1767 if (expr.
coeffs[0] == 0 && expr.
coeffs[1] == 0)
return;
1770 if (best_root_level_bounds_.GetUpperBound(expr) <= ub)
return;
1773 const IntegerValue implied_ub = GetImpliedUpperBound(expr);
1774 if (implied_ub <= ub) {
1775 const IntegerValue slack = ub - implied_ub;
1777 absl::Span<const IntegerVariable> vars = expr.
non_zero_vars();
1779 integer_trail_->AppendRelaxedLinearReason(slack, coeffs, vars,
1787 const auto it = best_affine_ub_.find(expr);
1788 if (it == best_affine_ub_.end())
return;
1795 const auto [affine, divisor] = it->second;
1796 integer_reason->push_back(
1800std::vector<LinearExpression2>
1802 std::vector<LinearExpression2> result;
1803 for (
const auto [expr, info] : best_affine_ub_) {
1804 result.push_back(expr);
static IntegralType CeilOfRatio(IntegralType numerator, IntegralType denominator)
static IntegralType FloorOfRatio(IntegralType numerator, IntegralType denominator)
const std::vector< IntegerType > & PositionsSetAtLeastOnce() const
bool PropagateLocalBounds(const IntegerTrail &integer_trail, Literal lit, const absl::flat_hash_map< IntegerVariable, IntegerValue > &input, absl::flat_hash_map< IntegerVariable, IntegerValue > *output) const
const Relation & relation(int index) const
The returned relation is guaranteed to only have positive variables.
void AddPartialRelation(Literal lit, IntegerVariable a, IntegerVariable b)
void Add(Literal lit, LinearTerm a, LinearTerm b, IntegerValue lhs, IntegerValue rhs)
void AddReifiedPrecedenceIfNonTrivial(Literal l, AffineExpression a, AffineExpression b)
IntegerValue UpperBound(LinearExpression2 expr) const
std::vector< LinearExpression2 > GetAllExpressionsWithAffineBounds() const
Warning, the order will not be deterministic.
RelationStatus GetLevelZeroPrecedenceStatus(AffineExpression a, AffineExpression b) const
Return the status of a <= b;.
LiteralIndex GetReifiedPrecedence(AffineExpression a, AffineExpression b)
void AddReasonForUpperBoundLowerThan(LinearExpression2 expr, IntegerValue ub, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason) const
RelationStatus GetLevelZeroStatus(LinearExpression2 expr, IntegerValue lb, IntegerValue ub) const
BinaryRelationsMaps(Model *model)
bool AddAffineUpperBound(LinearExpression2 expr, AffineExpression affine_ub)
void AddRelationBounds(LinearExpression2 expr, IntegerValue lb, IntegerValue ub)
void WatchLowerBound(IntegerVariable var, int id, int watch_index=-1)
int AddGreaterThanAtLeastOneOfConstraints(Model *model, bool auto_detect_clauses=false)
IntegerValue LowerBound(IntegerVariable i) const
Returns the current lower/upper bound of the given integer variable.
IntegerLiteral UpperBoundAsLiteral(IntegerVariable i) const
IntegerValue UpperBound(IntegerVariable i) const
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
Returns globally valid lower/upper bound on the given integer variable.
LiteralIndex Index() const
BooleanVariable Variable() const
void CollectPrecedences(absl::Span< const IntegerVariable > vars, std::vector< PrecedenceData > *output)
bool AddBounds(LinearExpression2 expr, IntegerValue lb, IntegerValue ub)
IntegerValue UpperBound(LinearExpression2 expr) const
void PushConditionalRelation(absl::Span< const Literal > enforcements, LinearExpression2 expr, IntegerValue rhs)
IntegerValue LevelZeroUpperBound(LinearExpression2 expr) const
void ComputeFullPrecedences(absl::Span< const IntegerVariable > vars, std::vector< FullIntegerPrecedence > *output)
bool AddUpperBound(LinearExpression2 expr, IntegerValue ub)
Same as above, but only for the upper bound.
void SetLevel(int level) final
Called each time we change decision level.
void AddReasonForUpperBoundLowerThan(LinearExpression2 expr, IntegerValue ub, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason) const
bool PropagateOutgoingArcs(IntegerVariable var)
bool AddPrecedenceWithOffsetIfNew(IntegerVariable i1, IntegerVariable i2, IntegerValue offset)
This version check current precedence. It is however "slow".
void AddPrecedenceWithOffset(IntegerVariable i1, IntegerVariable i2, IntegerValue offset)
~PrecedencesPropagator() override
void Untrail(const Trail &trail, int trail_index) final
int propagation_trail_index_
Simple class to add statistics by name and print them at the end.
int CurrentDecisionLevel() const
const VariablesAssignment & Assignment() const
bool LiteralIsFalse(Literal literal) const
bool LiteralIsTrue(Literal literal) const
void AddEdge(int from, int to)
bool GetNext(int *next_node_index, bool *cyclic, std::vector< int > *output_cycle_nodes=nullptr)
void push_back(const value_type &val)
void resize(size_type new_size)
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
IntType IntTypeAbs(IntType t)
const LiteralIndex kNoLiteralIndex(-1)
std::function< int64_t(const Model &)> LowerBound(IntegerVariable v)
std::vector< IntegerVariable > NegationOf(absl::Span< const IntegerVariable > vars)
Returns the vector of the negated variables.
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue.value())
const IntegerVariable kNoIntegerVariable(-1)
IntegerVariable PositiveVariable(IntegerVariable i)
bool VariableIsPositive(IntegerVariable i)
IntegerValue CapProdI(IntegerValue a, IntegerValue b)
Overflows and saturated arithmetic.
In SWIG mode, we don't want anything besides these top-level includes.
int64_t FloorRatio(int64_t value, int64_t positive_coeff)
void Permute(const IntVector &permutation, Array *array_to_permute)
static int input(yyscan_t yyscanner)
std::vector< IntegerValue > offsets
std::vector< int > indices
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
std::vector< std::function< bool()> > callbacks
absl::Span< const IntegerValue > non_zero_coeffs() const
absl::Span< const IntegerVariable > non_zero_vars() const
void CanonicalizeAndUpdateBounds(IntegerValue &lb, IntegerValue &ub, bool allow_negation=false)
static LinearExpression2 Difference(IntegerVariable v1, IntegerVariable v2)
Build (v1 - v2)
IntegerValue DivideByGcd()
void Negate()
Take the negation of this expression.
void SimpleCanonicalization()
::util::DenseIntStableTopologicalSorter DenseIntStableTopologicalSorter
#define SOLVER_LOG(logger,...)