14 #ifndef OR_TOOLS_SAT_SYMMETRY_H_
15 #define OR_TOOLS_SAT_SYMMETRY_H_
20 #include "absl/types/span.h"
68 absl::Span<const Literal>
Reason(
const Trail& trail,
69 int trail_index)
const final;
87 void AddSymmetry(std::unique_ptr<SparsePermutation> permutation);
96 std::vector<Literal>* output)
const;
100 bool PropagateNext(
Trail* trail);
104 std::vector<std::unique_ptr<SparsePermutation>> permutations_;
108 ImageInfo(
int p,
Literal i) : permutation_index(p), image(i) {}
110 int permutation_index;
118 struct AssignedLiteralInfo {
119 AssignedLiteralInfo(Literal l, Literal i,
int index)
120 :
literal(l), image(i), first_non_symmetric_info_index_so_far(
index) {}
131 int first_non_symmetric_info_index_so_far;
133 std::vector<std::vector<AssignedLiteralInfo>> permutation_trails_;
138 bool Enqueue(
const Trail& trail, Literal
literal, Literal image,
139 std::vector<AssignedLiteralInfo>* p_trail);
148 int source_trail_index;
151 std::vector<ReasonInfo> reasons_;
153 mutable StatsGroup stats_;
154 int num_propagations_;
bool Propagate(Trail *trail) final
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
~SymmetryPropagator() override
void AddSymmetry(std::unique_ptr< SparsePermutation > permutation)
int num_permutations() const
void Permute(int index, absl::Span< const Literal > input, std::vector< Literal > *output) const
void Untrail(const Trail &trail, int trail_index) final
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
static int input(yyscan_t yyscanner)