24#include "absl/container/flat_hash_map.h"
25#include "absl/container/flat_hash_set.h"
26#include "absl/flags/flag.h"
27#include "absl/log/check.h"
28#include "absl/strings/str_cat.h"
29#include "absl/strings/string_view.h"
30#include "absl/types/span.h"
31#include "google/protobuf/descriptor.h"
32#include "google/protobuf/message.h"
33#include "google/protobuf/text_format.h"
41 "DEBUG ONLY. When set to true, SolveCpModel() will dump its model "
42 "protos (original model, presolved model, mapping model) in text "
43 "format to 'FLAGS_cp_model_dump_prefix'{model|presolved_model|"
44 "mapping_model}.pb.txt.");
47ABSL_FLAG(std::string, cp_model_dump_prefix,
".\\",
48 "Prefix filename for all dumped files");
50ABSL_FLAG(std::string, cp_model_dump_prefix,
"/tmp/",
51 "Prefix filename for all dumped files");
55 "DEBUG ONLY. When set to true, solve will dump all "
56 "lns or objective_shaving submodels proto in text format to "
57 "'FLAGS_cp_model_dump_prefix'xxx.pb.txt.");
64template <
typename IntList>
65void AddIndices(
const IntList& indices, std::vector<int>* output) {
66 output->insert(output->end(), indices.begin(), indices.end());
72 gcd = std::gcd(gcd, std::abs(expr.
offset()));
73 for (
const int64_t coeff : expr.
coeffs()) {
74 gcd = std::gcd(gcd, std::abs(coeff));
81 if (divisor == 1)
return;
83 DCHECK_EQ(expr->
offset() % divisor, 0);
86 DCHECK_EQ(expr->
coeffs(
i) % divisor, 0);
93 output_negated_expr->
Clear();
108 std::vector<int>* variables,
109 std::vector<int>* literals) {
131 AddIndices(expr.vars(), variables);
137 AddIndices(expr.vars(), variables);
143 AddIndices(expr.vars(), variables);
150 AddIndices(expr.vars(), variables);
158 AddIndices(expr.vars(), variables);
176 AddIndices(expr.vars(), variables);
193 AddIndices(time.vars(), variables);
197 AddIndices(level.vars(), variables);
203 AddIndices(ct.
table().
vars(), variables);
206 AddIndices(expr.vars(), variables);
215 AddIndices(expr.vars(), variables);
231 AddIndices(demand.vars(), variables);
239#define APPLY_TO_SINGULAR_FIELD(ct_name, field_name) \
241 int temp = ct->mutable_##ct_name()->field_name(); \
243 ct->mutable_##ct_name()->set_##field_name(temp); \
246#define APPLY_TO_REPEATED_FIELD(ct_name, field_name) \
248 for (int& r : *ct->mutable_##ct_name()->mutable_##field_name()) f(&r); \
329 for (
int i = 0;
i < ct->
int_div().exprs_size(); ++
i) {
335 for (
int i = 0;
i < ct->
int_mod().exprs_size(); ++
i) {
341 for (
int i = 0;
i < ct->
lin_max().exprs_size(); ++
i) {
347 for (
int i = 0;
i < ct->
int_prod().exprs_size(); ++
i) {
355 for (
int i = 0;
i < ct->
all_diff().exprs_size(); ++
i) {
373 for (
int i = 0;
i < ct->
element().exprs_size(); ++
i) {
387 for (
int i = 0;
i < ct->
reservoir().time_exprs_size(); ++
i) {
390 for (
int i = 0;
i < ct->
reservoir().level_changes_size(); ++
i) {
398 for (
int i = 0;
i < ct->
table().exprs_size(); ++
i) {
407 for (
int i = 0;
i < ct->
automaton().exprs_size(); ++
i) {
493#undef APPLY_TO_SINGULAR_FIELD
494#undef APPLY_TO_REPEATED_FIELD
498 switch (constraint_case) {
506 return "kExactlyOne";
522 return "kDummyConstraint";
542 return "kNoOverlap2D";
544 return "kCumulative";
551 std::vector<int> result;
553 for (
int& ref : result) {
564 std::vector<int> used_intervals;
620 return used_intervals;
624 absl::Span<const int64_t>
solution) {
625 int64_t objective_value = 0;
627 int64_t coeff = objective.
coeffs(
i);
628 const int ref = objective.
vars(
i);
631 objective_value += coeff *
solution[var];
633 return objective_value;
638 std::abs(expr.
coeffs(0)) == 1;
659 DCHECK(!linear->
domain().empty());
660 const int64_t shift = coefficient * expr.
offset();
670 if (coeff == 0)
return;
690 DCHECK(!linear->
domain().empty());
703 if (a.
vars_size() !=
b.vars_size())
return false;
704 if (a.
offset() !=
b.offset() * b_scaling)
return false;
705 absl::flat_hash_map<int, int64_t> coeffs;
708 coeffs[
b.vars(
i)] += -
b.coeffs(
i) * b_scaling;
711 for (
const auto [var, coeff] : coeffs) {
712 if (coeff != 0)
return false;
720 if (!lin.
vars().empty()) {
734 if (!ct.enforcement_literal().empty()) {
737 switch (ct.constraint_case()) {
821 ct.reservoir().level_changes()) {
826 if (!ct.table().vars().empty()) {
842 if (!ct.automaton().vars().empty()) {
900#if !defined(__PORTABLE_PLATFORM__)
911class InlineFieldPrinter
912 :
public google::protobuf::TextFormat::FastFieldValuePrinter {
913 void PrintMessageStart(
const google::protobuf::Message& ,
916 google::protobuf::TextFormat::BaseTextGenerator*
917 generator)
const override {
918 generator->PrintLiteral(
" { ");
922class InlineMessagePrinter
923 :
public google::protobuf::TextFormat::MessagePrinter {
925 InlineMessagePrinter() {
926 printer_.SetSingleLineMode(
true);
927 printer_.SetUseShortRepeatedPrimitives(
true);
930 void Print(
const google::protobuf::Message& message,
932 google::protobuf::TextFormat::BaseTextGenerator* generator)
935 printer_.PrintToString(message, &buffer_);
936 generator->Print(buffer_.data(), buffer_.size());
940 google::protobuf::TextFormat::Printer printer_;
941 mutable std::string buffer_;
946void RegisterFieldPrinters(
947 const google::protobuf::Descriptor* descriptor,
948 absl::flat_hash_set<const google::protobuf::Descriptor*>* descriptors,
949 google::protobuf::TextFormat::Printer* printer) {
951 if (!descriptors->insert(descriptor).second)
return;
953 for (
int i = 0;
i < descriptor->field_count(); ++
i) {
954 const google::protobuf::FieldDescriptor* field = descriptor->field(
i);
955 if (field->type() == google::protobuf::FieldDescriptor::TYPE_MESSAGE) {
958 printer->RegisterFieldValuePrinter(field,
new InlineFieldPrinter());
960 RegisterFieldPrinters(field->message_type(), descriptors, printer);
969 printer->SetUseShortRepeatedPrimitives(
true);
970 absl::flat_hash_set<const google::protobuf::Descriptor*> descriptors;
973 new InlineMessagePrinter());
975 new InlineMessagePrinter());
985 const int num_vars = cp_model.
variables().size();
986 for (
int v = 0; v < num_vars; ++v) {
996 num_clauses += ct.bool_and().literals().size();
1004 absl::StrAppend(out,
"p cnf ", num_vars,
" ", num_clauses,
"\n");
1007 CHECK(ct.enforcement_literal().empty());
1008 for (
const int lit : ct.bool_or().literals()) {
1012 absl::StrAppend(out, value,
" ");
1014 absl::StrAppend(out,
"0\n");
1016 CHECK(!ct.enforcement_literal().empty());
1018 for (
const int lit : ct.enforcement_literal()) {
1022 absl::StrAppend(&start, -value,
" ");
1024 for (
const int lit : ct.bool_and().literals()) {
1028 absl::StrAppend(out, start, value,
" 0\n");
Domain AdditionWith(const Domain &domain) const
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
::int32_t vars(int index) const
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
::int32_t literals(int index) const
::int32_t literals(int index) const
const ::operations_research::sat::TableConstraintProto & table() const
const ::operations_research::sat::BoolArgumentProto & bool_xor() const
ConstraintCase constraint_case() const
const ::operations_research::sat::InverseConstraintProto & inverse() const
::operations_research::sat::CumulativeConstraintProto *PROTOBUF_NONNULL mutable_cumulative()
::int32_t enforcement_literal(int index) const
const ::operations_research::sat::BoolArgumentProto & exactly_one() const
const ::operations_research::sat::NoOverlapConstraintProto & no_overlap() const
const ::operations_research::sat::ListOfVariablesProto & dummy_constraint() const
const ::operations_research::sat::AllDifferentConstraintProto & all_diff() const
const ::operations_research::sat::LinearConstraintProto & linear() const
const ::operations_research::sat::BoolArgumentProto & at_most_one() const
const ::operations_research::sat::IntervalConstraintProto & interval() const
const ::operations_research::sat::RoutesConstraintProto & routes() const
const ::operations_research::sat::LinearArgumentProto & lin_max() const
const ::operations_research::sat::ElementConstraintProto & element() const
const ::operations_research::sat::BoolArgumentProto & bool_and() const
const ::operations_research::sat::BoolArgumentProto & bool_or() const
const ::operations_research::sat::LinearArgumentProto & int_mod() const
::google::protobuf::RepeatedField<::int32_t > *PROTOBUF_NONNULL mutable_enforcement_literal()
const ::operations_research::sat::LinearArgumentProto & int_prod() const
const ::operations_research::sat::LinearArgumentProto & int_div() const
const ::operations_research::sat::AutomatonConstraintProto & automaton() const
const ::operations_research::sat::CircuitConstraintProto & circuit() const
const ::operations_research::sat::CumulativeConstraintProto & cumulative() const
const ::operations_research::sat::ReservoirConstraintProto & reservoir() const
const ::operations_research::sat::NoOverlap2DConstraintProto & no_overlap_2d() const
bool has_solution_hint() const
.operations_research.sat.PartialVariableAssignment solution_hint = 6;
bool has_floating_point_objective() const
.operations_research.sat.FloatObjectiveProto floating_point_objective = 9;
static const ::google::protobuf::Descriptor *PROTOBUF_NONNULL descriptor()
const ::operations_research::sat::IntegerVariableProto & variables(int index) const
const ::operations_research::sat::FloatObjectiveProto & floating_point_objective() const
const ::operations_research::sat::ConstraintProto & constraints(int index) const
bool has_objective() const
.operations_research.sat.CpObjectiveProto objective = 4;
const ::operations_research::sat::PartialVariableAssignment & solution_hint() const
const ::operations_research::sat::CpObjectiveProto & objective() const
::int64_t domain(int index) const
double scaling_factor() const
int vars_size() const
repeated int32 vars = 1;
::int32_t vars(int index) const
::int64_t coeffs(int index) const
const ::operations_research::sat::LinearExpressionProto & demands(int index) const
::operations_research::sat::LinearExpressionProto *PROTOBUF_NONNULL mutable_demands(int index)
::int32_t intervals(int index) const
const ::operations_research::sat::LinearExpressionProto & capacity() const
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
const ::operations_research::sat::LinearExpressionProto & linear_target() const
bool has_linear_index() const
.operations_research.sat.LinearExpressionProto linear_index = 4;
bool has_linear_target() const
.operations_research.sat.LinearExpressionProto linear_target = 5;
::int32_t vars(int index) const
const ::operations_research::sat::LinearExpressionProto & linear_index() const
::int32_t vars(int index) const
double coeffs(int index) const
::int64_t domain(int index) const
static const ::google::protobuf::Descriptor *PROTOBUF_NONNULL descriptor()
const ::operations_research::sat::LinearExpressionProto & size() const
const ::operations_research::sat::LinearExpressionProto & end() const
const ::operations_research::sat::LinearExpressionProto & start() const
::int32_t f_inverse(int index) const
::int32_t f_direct(int index) const
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
const ::operations_research::sat::LinearExpressionProto & target() const
::int32_t vars(int index) const
void add_vars(::int32_t value)
void add_coeffs(::int64_t value)
::int64_t domain(int index) const
::int64_t coeffs(int index) const
ABSL_ATTRIBUTE_REINITIALIZES void Clear() PROTOBUF_FINAL
::google::protobuf::RepeatedField<::int32_t > *PROTOBUF_NONNULL mutable_vars()
::int32_t vars(int index) const
void set_offset(::int64_t value)
void add_coeffs(::int64_t value)
void set_coeffs(int index, ::int64_t value)
static const ::google::protobuf::Descriptor *PROTOBUF_NONNULL descriptor()
void add_vars(::int32_t value)
int vars_size() const
repeated int32 vars = 1;
::int32_t vars(int index) const
::int32_t y_intervals(int index) const
::int32_t x_intervals(int index) const
::int32_t intervals(int index) const
::int64_t values(int index) const
::int32_t vars(int index) const
::int32_t active_literals(int index) const
const ::operations_research::sat::LinearExpressionProto & time_exprs(int index) const
const ::operations_research::sat::LinearExpressionProto & level_changes(int index) const
::int32_t literals(int index) const
::int32_t vars(int index) const
const ::operations_research::sat::LinearExpressionProto & exprs(int index) const
#define APPLY_TO_SINGULAR_FIELD(ct_name, field_name)
ABSL_FLAG(bool, cp_model_dump_models, false, "DEBUG ONLY. When set to true, SolveCpModel() will dump its model " "protos (original model, presolved model, mapping model) in text " "format to 'FLAGS_cp_model_dump_prefix'{model|presolved_model|" "mapping_model}.pb.txt.")
#define APPLY_TO_REPEATED_FIELD(ct_name, field_name)
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
void SetToNegatedLinearExpression(const LinearExpressionProto &input_expr, LinearExpressionProto *output_negated_expr)
Fills the target as negated ref.
constexpr uint64_t kDefaultFingerprintSeed
Default seed for fingerprints.
uint64_t FingerprintRepeatedField(const google::protobuf::RepeatedField< T > &sequence, uint64_t seed)
bool RefIsPositive(int ref)
int64_t ComputeInnerObjective(const CpObjectiveProto &objective, absl::Span< const int64_t > solution)
int CombineSeed(int base_seed, int64_t delta)
We assume delta >= 0 and we only use the low bit of delta.
void ApplyToAllIntervalIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
bool SafeAddLinearExpressionToLinearConstraint(const LinearExpressionProto &expr, int64_t coefficient, LinearConstraintProto *linear)
Same method, but returns if the addition was possible without overflowing.
uint64_t FingerprintSingleField(const T &field, uint64_t seed)
bool ConvertCpModelProtoToCnf(const CpModelProto &cp_model, std::string *out)
uint64_t FingerprintExpression(const LinearExpressionProto &lin, uint64_t seed)
Returns a stable fingerprint of a linear expression.
uint64_t FingerprintModel(const CpModelProto &model, uint64_t seed)
Returns a stable fingerprint of a model.
bool ExpressionIsAffine(const LinearExpressionProto &expr)
Checks if the expression is affine or constant.
std::vector< int > UsedVariables(const ConstraintProto &ct)
std::vector< int > UsedIntervals(const ConstraintProto &ct)
Returns the sorted list of interval used by a constraint.
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
Serializes a Domain into the domain field of a proto.
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
void SetupTextFormatPrinter(google::protobuf::TextFormat::Printer *printer)
absl::string_view ConstraintCaseName(ConstraintProto::ConstraintCase constraint_case)
bool ExpressionContainsSingleRef(const LinearExpressionProto &expr)
Returns true if a linear expression can be reduced to a single ref.
int64_t LinearExpressionGcd(const LinearExpressionProto &expr, int64_t gcd)
void ApplyToAllLiteralIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
void DivideLinearExpression(int64_t divisor, LinearExpressionProto *expr)
void AddLinearExpressionToLinearConstraint(const LinearExpressionProto &expr, int64_t coefficient, LinearConstraintProto *linear)
int GetSingleRefFromExpression(const LinearExpressionProto &expr)
int NegatedRef(int ref)
Small utility functions to deal with negative variable/literal references.
bool LinearExpressionProtosAreEqual(const LinearExpressionProto &a, const LinearExpressionProto &b, int64_t b_scaling)
Returns true iff a == b * b_scaling.
IndexReferences GetReferencesUsedByConstraint(const ConstraintProto &ct)
void ApplyToAllVariableIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
void AddWeightedLiteralToLinearConstraint(int lit, int64_t coeff, LinearConstraintProto *linear, int64_t *offset)
In SWIG mode, we don't want anything besides these top-level includes.
bool AtMinOrMaxInt64(int64_t x)
Checks if x is equal to the min or the max value of an int64_t.
Select next search node to expand Select next item_i to add this new search node to the search Generate a new search node where item_i is not in the knapsack Check validity of this new partial solution(using propagators) - If valid
ClosedInterval::Iterator end(ClosedInterval interval)
int64_t CapProd(int64_t x, int64_t y)
std::vector< int > variables
std::vector< int > literals