28 const int size =
ct.bool_or().literals_size();
30 bool satisfied =
false;
31 for (
int i = 0; i < size; ++i) {
32 const int ref =
ct.bool_or().literals(i);
43 if (satisfied)
return;
46 const int first_ref =
ct.bool_or().literals(0);
51 std::vector<Domain>* domains) {
52 bool satisfied =
false;
53 std::vector<int> free_variables;
54 for (
const int ref :
ct.exactly_one().literals()) {
58 CHECK(!satisfied) <<
"Two variables at one in exactly one.";
62 free_variables.push_back(ref);
67 CHECK(!free_variables.empty()) <<
"All zero in exactly one";
68 const int ref = free_variables.back();
70 free_variables.pop_back();
74 for (
const int ref : free_variables) {
82 const std::vector<bool>& prefer_lower_value,
83 std::vector<Domain>* domains) {
84 int64 fixed_activity = 0;
85 const int size =
ct.linear().vars().size();
86 std::vector<int> free_vars;
87 std::vector<int64> free_coeffs;
88 for (
int i = 0; i < size; ++i) {
89 const int var =
ct.linear().vars(i);
90 const int64 coeff =
ct.linear().coeffs(i);
92 if (coeff == 0)
continue;
94 fixed_activity += (*domains)[
var].FixedValue() * coeff;
96 free_vars.push_back(
var);
97 free_coeffs.push_back(coeff);
100 if (free_vars.empty())
return;
104 if (free_vars.size() == 1) {
105 const int var = free_vars[0];
121 std::vector<Domain> rhs_domains;
122 rhs_domains.push_back(initial_rhs);
123 for (
int i = 0; i + 1 < free_vars.size(); ++i) {
130 rhs_domains.push_back(term.
AdditionWith(rhs_domains.back()));
132 for (
int i = free_vars.size() - 1; i >= 0; --i) {
136 const int var = free_vars[i];
137 const int64 coeff = free_coeffs[i];
138 const Domain domain = rhs_domains[i]
150 fixed_activity += coeff *
value;
159 for (
const int ref :
ct.int_max().vars()) {
171 const int target_ref =
ct.int_max().target();
174 (*domains)[target_var] = (*domains)[target_var].IntersectionWith(
Domain(m));
176 (*domains)[target_var] =
177 (*domains)[target_var].IntersectionWith(
Domain(-m));
179 CHECK(!(*domains)[target_var].IsEmpty());
184 const int index_ref =
ct.element().index();
186 const int target_ref =
ct.element().target();
192 if (!(*domains)[target_var].
IsFixed() && !(*domains)[index_var].
IsFixed()) {
193 const int64 index_value = (*domains)[index_var].Min();
194 (*domains)[index_var] =
Domain(index_value);
197 const int selected_ref =
ct.element().vars(
199 const int selected_var =
PositiveRef(selected_ref);
200 if (!(*domains)[selected_var].
IsFixed()) {
201 (*domains)[selected_var] =
Domain((*domains)[selected_var].Min());
206 if ((*domains)[index_var].
IsFixed()) {
207 const int64 index_value = (*domains)[index_var].FixedValue();
208 const int selected_ref =
ct.element().vars(
210 const int selected_var =
PositiveRef(selected_ref);
211 const int64 selected_value = (*domains)[selected_var].FixedValue();
212 (*domains)[target_var] = (*domains)[target_var].IntersectionWith(
216 DCHECK(!(*domains)[target_var].IsEmpty());
221 const int64 target_value = (*domains)[target_var].FixedValue();
222 int selected_index_value = -1;
223 for (
int i = 0; i <
ct.element().vars().size(); ++i) {
224 const int ref =
ct.element().vars(i);
228 if (
value == target_value) {
229 selected_index_value = i;
233 if (
value == -target_value) {
234 selected_index_value = i;
241 (*domains)[index_var] = (*domains)[index_var].IntersectionWith(
Domain(
242 RefIsPositive(index_var) ? selected_index_value : -selected_index_value));
243 DCHECK(!(*domains)[index_var].IsEmpty());
247 const CpModelProto& mapping_proto,
248 const std::vector<int>& postsolve_mapping,
252 *(
response->mutable_sufficient_assumptions_for_infeasibility())) {
258 if (
response->status() != CpSolverStatus::FEASIBLE &&
259 response->status() != CpSolverStatus::OPTIMAL) {
262 if (
response->solution_size() != postsolve_mapping.size())
return;
266 std::vector<Domain> domains(mapping_proto.variables_size());
267 for (
int i = 0; i < postsolve_mapping.size(); ++i) {
268 CHECK_LE(postsolve_mapping[i], domains.size());
271 for (
int i = 0; i < domains.size(); ++i) {
272 if (domains[i].IsEmpty()) {
275 CHECK(!domains[i].IsEmpty());
282 CHECK(!mapping_proto.has_objective());
283 std::vector<bool> prefer_lower_value(domains.size(),
true);
284 if (mapping_proto.has_objective()) {
285 const int size = mapping_proto.objective().vars().size();
286 for (
int i = 0; i < size; ++i) {
287 int var = mapping_proto.objective().vars(i);
288 int64 coeff = mapping_proto.objective().coeffs(i);
293 prefer_lower_value[i] = (coeff >= 0);
298 const int num_constraints = mapping_proto.constraints_size();
299 for (
int i = num_constraints - 1; i >= 0; i--) {
300 const ConstraintProto&
ct = mapping_proto.constraints(i);
303 bool enforced =
true;
304 for (
const int ref :
ct.enforcement_literal()) {
311 if (!enforced)
continue;
313 switch (
ct.constraint_case()) {
314 case ConstraintProto::kBoolOr:
317 case ConstraintProto::kExactlyOne:
320 case ConstraintProto::kLinear:
323 case ConstraintProto::kIntMax:
326 case ConstraintProto::kElement:
332 LOG(
FATAL) <<
"Unsupported constraint: " <<
ct.ShortDebugString();
337 response->mutable_solution()->Clear();
338 CHECK_LE(num_variables_in_original_model, domains.size());
339 for (
int i = 0; i < num_variables_in_original_model; ++i) {
340 if (prefer_lower_value[i]) {
341 response->add_solution(domains[i].Min());
343 response->add_solution(domains[i].Max());
#define CHECK_LT(val1, val2)
#define CHECK_NE(val1, val2)
#define DCHECK(condition)
#define CHECK_LE(val1, val2)
We call domain any subset of Int64 = [kint64min, kint64max].
Domain MultiplicationBy(int64 coeff, bool *exact=nullptr) const
Returns {x ∈ Int64, ∃ e ∈ D, x = e * coeff}.
Domain InverseMultiplicationBy(const int64 coeff) const
Returns {x ∈ Int64, ∃ e ∈ D, x * coeff = e}.
Domain AdditionWith(const Domain &domain) const
Returns {x ∈ Int64, ∃ a ∈ D, ∃ b ∈ domain, x = a + b}.
int64 Min() const
Returns the min value of the domain.
int64 Max() const
Returns the max value of the domain.
Domain IntersectionWith(const Domain &domain) const
Returns the intersection of D and domain.
bool IsEmpty() const
Returns true if this is the empty set.
bool Contains(int64 value) const
Returns true iff value is in Domain.
SharedResponseManager * response
static const int64 kint64min
void PostsolveElement(const ConstraintProto &ct, std::vector< Domain > *domains)
bool RefIsPositive(int ref)
void PostsolveIntMax(const ConstraintProto &ct, std::vector< Domain > *domains)
void PostsolveResponse(const int64 num_variables_in_original_model, const CpModelProto &mapping_proto, const std::vector< int > &postsolve_mapping, CpSolverResponse *response)
void PostsolveExactlyOne(const ConstraintProto &ct, std::vector< Domain > *domains)
void PostsolveLinear(const ConstraintProto &ct, const std::vector< bool > &prefer_lower_value, std::vector< Domain > *domains)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
void PostsolveClause(const ConstraintProto &ct, std::vector< Domain > *domains)
std::function< bool(const Model &)> IsFixed(IntegerVariable v)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...