14#ifndef OR_TOOLS_SAT_PRECEDENCES_H_
15#define OR_TOOLS_SAT_PRECEDENCES_H_
21#include "absl/container/inlined_vector.h"
58 watcher_id_(watcher_->Register(this)) {
82 IntegerVariable offset_var);
89 IntegerValue offset,
Literal l);
94 IntegerVariable offset_var,
118 std::vector<IntegerPrecedences>* output);
120 std::vector<Literal>* literal_reason,
121 std::vector<IntegerLiteral>* integer_reason)
const;
135 DEFINE_INT_TYPE(OptionalArcIndex,
int);
140 int AddGreaterThanAtLeastOneOfConstraintsFromClause(
141 const absl::Span<const Literal> clause,
Model*
model);
147 int AddGreaterThanAtLeastOneOfConstraintsWithClauseAutoDetection(
152 IntegerVariable tail_var;
153 IntegerVariable head_var;
156 IntegerVariable offset_var;
159 absl::InlinedVector<Literal, 6> presence_literals;
163 mutable bool is_marked;
171 void AdjustSizeFor(IntegerVariable i);
172 void AddArc(IntegerVariable
tail, IntegerVariable
head, IntegerValue offset,
173 IntegerVariable offset_var,
174 absl::Span<const Literal> presence_literals);
178 bool EnqueueAndCheck(
const ArcInfo& arc, IntegerValue new_head_lb,
180 IntegerValue ArcOffset(
const ArcInfo& arc)
const;
184 void PropagateOptionalArcs(
Trail* trail);
202 void InitializeBFQueueWithModifiedNodes();
203 bool BellmanFordTarjan(
Trail* trail);
204 bool DisassembleSubtree(
int source,
int target,
205 std::vector<bool>* can_be_skipped);
207 std::vector<Literal>* must_be_all_true,
208 std::vector<Literal>* literal_reason,
209 std::vector<IntegerLiteral>* integer_reason);
210 void CleanUpMarkedArcsAndParents();
214 bool NoPropagationLeft(
const Trail& trail)
const;
246 impacted_potential_arcs_;
254 IntegerValue lower_bound;
255 bool operator<(
const SortedVar& other)
const {
256 return lower_bound < other.lower_bound;
259 std::vector<SortedVar> tmp_sorted_vars_;
260 std::vector<IntegerPrecedences> tmp_precedences_;
270 literal_to_new_impacted_arcs_;
274 std::vector<Literal> literal_reason_;
275 std::vector<IntegerLiteral> integer_reason_;
280 std::deque<int> bf_queue_;
281 std::vector<bool> bf_in_queue_;
282 std::vector<bool> bf_can_be_skipped_;
283 std::vector<ArcIndex> bf_parent_arc_of_;
286 std::vector<int> tmp_vector_;
296 IntegerVariable i2) {
302 IntegerVariable i1, IntegerVariable i2, IntegerValue offset) {
314 IntegerVariable i1, IntegerVariable i2, IntegerValue offset,
Literal l) {
319 IntegerVariable i1, IntegerVariable i2, IntegerVariable offset_var) {
320 AddArc(i1, i2, IntegerValue(0), offset_var, {});
324 IntegerVariable i1, IntegerVariable i2, IntegerValue offset,
325 IntegerVariable offset_var, absl::Span<const Literal> presence_literals) {
326 AddArc(i1, i2, offset, offset_var, presence_literals);
347 a,
b, IntegerValue(offset));
360 IntegerVariable
a, IntegerVariable
b,
int64 ub,
361 const std::vector<Literal>& enforcement_literals) {
382 IntegerVariable
a, IntegerVariable
b, IntegerVariable c,
int64 ub,
383 const std::vector<Literal>& enforcement_literals) {
387 enforcement_literals);
420 IntegerVariable
a, IntegerVariable
b,
int64 offset,
Literal is_le) {
436 IntegerVariable
a, IntegerVariable
b, absl::Span<const Literal> literals) {
446 IntegerVariable
a, IntegerVariable
b,
int64 offset,
Literal is_le) {
void SetPropagatorPriority(int id, int priority)
void RegisterWatcher(SparseBitset< IntegerVariable > *p)
Class that owns everything related to a particular optimization model.
void AddPrecedenceReason(int arc_index, IntegerValue min_offset, std::vector< Literal > *literal_reason, std::vector< IntegerLiteral > *integer_reason) const
void AddConditionalPrecedence(IntegerVariable i1, IntegerVariable i2, Literal l)
void AddConditionalPrecedenceWithOffset(IntegerVariable i1, IntegerVariable i2, IntegerValue offset, Literal l)
void AddPrecedenceWithOffset(IntegerVariable i1, IntegerVariable i2, IntegerValue offset)
void AddPrecedenceWithAllOptions(IntegerVariable i1, IntegerVariable i2, IntegerValue offset, IntegerVariable offset_var, absl::Span< const Literal > presence_literals)
void ComputePrecedences(const std::vector< IntegerVariable > &vars, std::vector< IntegerPrecedences > *output)
void AddPrecedence(IntegerVariable i1, IntegerVariable i2)
int AddGreaterThanAtLeastOneOfConstraints(Model *model)
PrecedencesPropagator(Model *model)
void AddPrecedenceWithVariableOffset(IntegerVariable i1, IntegerVariable i2, IntegerVariable offset_var)
void Untrail(const Trail &trail, int trail_index) final
bool PropagateOutgoingArcs(IntegerVariable var)
std::function< void(Model *)> NotEqual(IntegerVariable a, IntegerVariable b)
std::function< void(Model *)> ConditionalSum3LowerOrEqual(IntegerVariable a, IntegerVariable b, IntegerVariable c, int64 ub, const std::vector< Literal > &enforcement_literals)
std::function< void(Model *)> Sum2LowerOrEqual(IntegerVariable a, IntegerVariable b, int64 ub)
std::function< void(Model *)> ConditionalLowerOrEqualWithOffset(IntegerVariable a, IntegerVariable b, int64 offset, Literal is_le)
const IntegerVariable kNoIntegerVariable(-1)
std::function< void(Model *)> GreaterOrEqual(IntegerVariable v, int64 lb)
std::function< void(Model *)> ConditionalSum2LowerOrEqual(IntegerVariable a, IntegerVariable b, int64 ub, const std::vector< Literal > &enforcement_literals)
std::function< void(Model *)> Sum3LowerOrEqual(IntegerVariable a, IntegerVariable b, IntegerVariable c, int64 ub)
std::function< void(Model *)> ReifiedEqualityWithOffset(IntegerVariable a, IntegerVariable b, int64 offset, Literal is_eq)
std::function< void(Model *)> ReifiedLowerOrEqualWithOffset(IntegerVariable a, IntegerVariable b, int64 offset, Literal is_le)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
std::function< void(Model *)> LowerOrEqual(IntegerVariable v, int64 ub)
std::function< void(Model *)> Equality(IntegerVariable v, int64 value)
std::function< void(Model *)> LowerOrEqualWithOffset(IntegerVariable a, IntegerVariable b, int64 offset)
std::function< void(Model *)> EqualityWithOffset(IntegerVariable a, IntegerVariable b, int64 offset)
std::function< void(Model *)> ReifiedBoolAnd(const std::vector< Literal > &literals, Literal r)
std::function< void(Model *)> ReifiedEquality(IntegerVariable a, IntegerVariable b, Literal is_eq)
std::function< BooleanVariable(Model *)> NewBooleanVariable()
std::function< void(Model *)> ConditionalLowerOrEqual(IntegerVariable a, IntegerVariable b, Literal is_le)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...