55 result.values.push_back(value);

56 return result;

57}

62 result.values.push_back(included_min);

63 result.values.push_back(included_max);

64 return result;

65}

70 result.values.push_back(0);

71 result.values.push_back(1);

72 return result;

73}

132 }

134 if (!domain.values.empty()) {

136 }

137 return false;

138 }

140 is_interval = false;

141 if (values.empty()) {

143 } else {

144 const int64_t imin = values[0];

145 const int64_t imax = values[1];

148 }

149 return true;

150 }

151

153}

160 if (interval_min > interval_max) {

163 return true;

165 if (values.empty()) {

166 values.push_back(interval_min);

167 values.push_back(interval_max);

168 return true;

169 } else {

170 if (values[0] >= interval_min && values[1] <= interval_max) return false;

171 values[0] = std::max(values[0], interval_min);

172 values[1] = std::min(values[1], interval_max);

179 }

180 return true;

181 }

182 } else {

183 if (!values.empty()) {

185 std::vector<int64_t> new_values;

186 new_values.reserve(values.size());

187 bool changed = false;

188 for (const int64_t val : values) {

189 if (val > interval_max) {

190 changed = true;

191 break;

192 }

193 if (val >= interval_min &&

194 (new_values.empty() || val != new_values.back())) {

195 new_values.push_back(val);

196 } else {

197 changed = true;

198 }

199 }

200 values.swap(new_values);

201 return changed;

202 }

203 }

204 return false;

205}

209 const int64_t dmin =

210 values.empty() ? std::numeric_limits<int64_t>::min() : values[0];

211 const int64_t dmax =

212 values.empty() ? std::numeric_limits<int64_t>::max() : values[1];

214 for (const int64_t v : integers) {

215 if (v >= dmin && v <= dmax) values.push_back(v);

216 }

218 if (!values.empty() &&

220 values.size() >= 2) {

221 if (values.size() > 2) {

222

223 const int64_t last = values.back();

226 }

227 return values[0] != dmin || values[1] != dmax;

228 } else {

229

231 return true;

232 }

233 } else {

234

236 absl::flat_hash_set<int64_t> other_values(integers.begin(), integers.end());

237 std::vector<int64_t> new_values;

238 new_values.reserve(std::min(values.size(), integers.size()));

239 bool changed = false;

240 for (const int64_t val : values) {

241 if (other_values.contains(val)) {

242 if (new_values.empty() || val != new_values.back()) {

243 new_values.push_back(val);

244 }

245 } else {

246 changed = true;

247 }

248 }

249 values.swap(new_values);

250 return changed;

251 }

252}

257

258 return false;

259 }

262 }

264

265 return false;

266 }

267

269

272 return true;

273 }

274

276

279 bool changed = false;

282 changed = true;

283 }

286 changed = true;

287 }

290 }

291 return changed;

292 } else {

298 return true;

299 }

301 }

302 } else {

303

309

310 return true;

311 }

313 } else {

316

317 return true;

318 }

320 }

321 }

322}

354 return values.front();

355}

359 (values.empty() || (values[0] == std::numeric_limits<int64_t>::min() &&

360 values[1] == std::numeric_limits<int64_t>::max()));

361}

365 if (values.empty()) {

366 return true;

367 } else {

368 return value >= values[0] && value <= values[1];

369 }

370 } else {

371 return std::find(values.begin(), values.end(), value) != values.end();

372 }

373}

389 return true;

390 }

392 CHECK(!values.empty());

393 return IntervalOverlapValues(values[0], values[1], vec);

394 } else {

395

396 const std::vector<int64_t>& to_scan =

398 const absl::flat_hash_set<int64_t> container =

399 values.size() <= vec.size()

400 ? absl::flat_hash_set<int64_t>(vec.begin(), vec.end())

401 : absl::flat_hash_set<int64_t>(values.begin(), values.end());

402 for (int64_t value : to_scan) {

403 if (container.contains(value)) {

404 return true;

405 }

406 }

407 return false;

408 }

409}

413 return true;

414 }

416 CHECK(!values.empty());

417 const int64_t dlb = values[0];

418 const int64_t dub = values[1];

419 return !(dub < lb || dlb > ub);

420 } else {

421 return IntervalOverlapValues(lb, ub, values);

422 }

423}

427 if (other.values.empty()) {

428 return true;

429 } else {

431 }

432 } else {

434 }

435}

439 if (values.empty()) {

440 return false;

441 } else if (value == values[0] && value != values[1]) {

443 return true;

444 } else if (value == values[1] && value != values[0]) {

446 return true;

448 value < values[1]) {

449 const int64_t vmax = values[1];

452 for (int64_t v = values[0] + 1; v <= vmax; ++v) {

453 if (v != value) {

455 }

456 }

458 return true;

459 }

460 } else {

463 return true;

464 }

465 return false;

466}

469 std::string prefix = "";

471 prefix = "fixed_set of ";

473 prefix = "set of ";

474 }

475

478 case 0:

479 return "float";

480 case 1:

481 return absl::StrCat(prefix, float_values[0]);

482 case 2:

484 "]");

485 default:

486 LOG(DFATAL) << "Error with float domain";

487 return "error_float";

488 }

489 }

491 if (values.empty()) {

492 return absl::StrCat(prefix, "int");

493 } else {

494 return absl::StrCat(prefix, "[", values[0], "..", values[1], "]");

495 }

496 } else if (values.size() == 1) {

497 return absl::StrCat(prefix, values.back());

498 } else {

499 return absl::StrFormat("%s[%s]", prefix, absl::StrJoin(values, ", "));

500 }

501}

508 result.values.push_back(value);

509 return result;

510}

515 result.values.push_back(imin);

516 result.values.push_back(imax);

517 return result;

518}

544 result.variables = std::move(vars);

545 return result;

546}

556 if (domain.values.empty()) {

558 std::numeric_limits<int64_t>::max());

559 } else {

561 }

562 } else {

564 }

565}

570 result.floats.push_back(value);

571 return result;

572}

577 result.floats.push_back(lb);

578 result.floats.push_back(ub);

579 return result;

580}

590 switch (type) {

592 return absl::StrFormat("%d", values[0]);

594 return absl::StrFormat("[%d..%d]", values[0], values[1]);

596 return absl::StrFormat("[%s]", absl::StrJoin(values, ", "));

602 std::string result = "[";

603 for (int i = 0; i < variables.size(); ++i) {

604 result.append(variables[i]->name);

605 result.append(i != variables.size() - 1 ? ", " : "]");

606 }

607 return result;

608 }

610 return "VoidArgument";

612 return absl::StrCat(floats[0]);

614 return absl::StrCat("[", floats[0], "..", floats[1], "]");

616 return absl::StrFormat("[%s]", absl::StrJoin(floats, ", "));

617 }

618 LOG(FATAL) << "Unhandled case in DebugString " << static_cast<int>(type);

619 ABSL_UNREACHABLE();

620}

631 DCHECK(HasOneValue()) << "Value() called on unbound Argument: "

633 switch (type) {

639 return variables[0]->domain.values[0];

640 default:

641 break;

642 }

643 ABSL_UNREACHABLE();

644}

647 switch (type) {

649 return false;

651 return false;

653 return true;

656 if (!domain.HasOneValue()) {

657 return false;

658 }

659 }

660 return true;

661 }

663 return false;

666 if (!var->domain.HasOneValue()) {

667 return false;

668 }

669 }

670 return true;

671 }

673 return false;

675 return false;

677 return false;

679 return false;

680 }

681 ABSL_UNREACHABLE();

682}

685 switch (type) {

687 return std::find(values.begin(), values.end(), value) != values.end();

689 return value >= values.front() && value <= values.back();

691 return value == values.front();

692 default:

693 break;

694 }

695

696 ABSL_UNREACHABLE();

697}

700 switch (type) {

702 CHECK_GE(pos, 0);

703 CHECK_LT(pos, values.size());

706 CHECK_GE(pos, 0);

707 CHECK_LT(pos, domains.size());

708 return domains[pos].Value();

709 }

711 CHECK_GE(pos, 0);

713 return variables[pos]->domain.Value();

714 }

715 default:

716 break;

717 }

718 ABSL_UNREACHABLE();

719}

722 switch (type) {

724 CHECK_GE(pos, 0);

725 CHECK_LT(pos, values.size());

726 return true;

728 CHECK_GE(pos, 0);

729 CHECK_LT(pos, domains.size());

730 return domains[pos].HasOneValue();

731 }

733 CHECK_GE(pos, 0);

735 return variables[pos]->domain.HasOneValue();

736 }

737 default:

738 break;

739 }

740 ABSL_UNREACHABLE();

741}

752 switch (type) {

754 return values.size();

757 }

760 }

762 return 0;

763 }

765 return floats.size();

766 }

767 default:

768 break;

769 }

770 ABSL_UNREACHABLE();

771}

784 bool other_temporary) {

785 if (temporary && !other_temporary) {

787 name = other_name;

788 }

789 domain.IntersectWithDomain(other_domain);

790 return true;

791}

794 if (!domain.is_interval && domain.values.size() == 1) {

795 return absl::StrFormat("% d", domain.values.back());

796 } else {

797 return absl::StrFormat("%s(%s%s)%s", name, domain.DebugString(),

799 active ? "" : " [removed during presolve]");

800 }

801}

806 const std::string strong = strong_propagation ? " strong propagation" : "";

807 const std::string presolve_status_str =

808 active ? "" : " [removed during presolve]";

809 const std::string symmetric_breaking_str =

811 const std::string redundant_str = is_redundant ? " redundant" : "";

813 presolve_status_str, symmetric_breaking_str,

814 redundant_str);

815}

827 type = "false_constraint";

829}

855 result.id = id;

856 return result;

857}

860 std::vector<Annotation> args) {

865 result.id = id;

867 return result;

868}

875 result.id = id;

876 return result;

877}

895 LOG(INFO) << "Create INT_LIST";

899 return result;

900}

931 ann.AppendAllVariables(vars);

932 }

935 }

936}

939 switch (type) {

943 return id;

951 return absl::StrFormat("[%s]", absl::StrJoin(values, ", "));

955 std::string result = "[";

956 for (int i = 0; i < variables.size(); ++i) {

958 result.append(i != variables.size() - 1 ? ", " : "]");

959 }

960 return result;

961 }

963 return absl::StrFormat("\"%s\"", string_value);

964 }

965 LOG(FATAL) << "Unhandled case in DebugString " << static_cast<int>(type);

966 ABSL_UNREACHABLE();

967}

985 absl::string_view name, std::vector<Bounds> bounds,

993 return result;

994}

1000 return result;

1001}

1005 return absl::StrFormat("output_var(%s)", variable->name);

1006 } else {

1007 return absl::StrFormat("output_array([%s] [%s])",

1010 }

1011}

1021 bool defined, bool set_is_fixed) {

1023 if (set_is_fixed) {

1026 }

1027 variables_.push_back(var);

1028 return var;

1029}

1035 variables_.push_back(var);

1036 return var;

1037}

1042 variables_.push_back(var);

1043 return var;

1044}

1047 bool is_domain, bool symmetry, bool redundant) {

1049 new Constraint(id, std::move(arguments), is_domain, symmetry, redundant);

1050 constraints_.push_back(constraint);

1051}

1054 std::vector<Argument> arguments) {

1055 AddConstraint(id, std::move(arguments), false, false, false);

1056}

1059 output_.push_back(std::move(output));

1060}

1063 objective_ = nullptr;

1065}

1069 objective_ = obj;

1070 maximize_ = false;

1072}

1076 objective_ = obj;

1077 maximize_ = true;

1079}

1082 std::string output = absl::StrFormat("Model %s\nVariables\n", name_);

1083 for (int i = 0; i < variables_.size(); ++i) {

1084 absl::StrAppendFormat(&output, " %s\n", variables_[i]->DebugString());

1085 }

1086 output.append("Constraints\n");

1087 for (int i = 0; i < constraints_.size(); ++i) {

1088 if (constraints_[i] != nullptr) {

1089 absl::StrAppendFormat(&output, " %s\n", constraints_[i]->DebugString());

1090 }

1091 }

1092 if (objective_ != nullptr) {

1093 absl::StrAppendFormat(&output, "%s %s\n %s\n",

1094 maximize_ ? "Maximize" : "Minimize", objective_->name,

1096 } else if (!float_objective_variables_.empty()) {

1097 absl::StrAppendFormat(&output, "%s [%s] * [%s] + %f\n %s\n",

1098 maximize_ ? "Maximize" : "Minimize",

1100 absl::StrJoin(float_objective_coefficients_, ", "),

1101 float_objective_offset_,

1103

1104 } else {

1105 absl::StrAppendFormat(&output, "Satisfy\n %s\n",

1107 }

1108 output.append("Output\n");

1109 for (int i = 0; i < output_.size(); ++i) {

1110 absl::StrAppendFormat(&output, " %s\n", output_[i].DebugString());

1111 }

1112

1114}

1117 for (Variable* var : variables_) {

1118 if (var->domain.empty()) {

1119 return true;

1120 }

1121 }

1122 for (Constraint* ct : constraints_) {

1123 if (ct->type == "false_constraint") {

1124 return true;

1125 }

1126 }

1127

1128 return false;

1129}

1134 SOLVER_LOG(logger_, "Model ", model_.name());

1135

1136

1137 int num_bool_vars = 0;

1138 int num_int_vars = 0;

1139 int num_float_vars = 0;

1140 int num_set_vars = 0;

1141 for (Variable* var : model_.variables()) {

1142 if (var->domain.is_float) {

1143 ++num_float_vars;

1144 } else if (var->domain.is_a_set) {

1145 ++num_set_vars;

1146 } else if (var->domain.display_as_boolean) {

1147 ++num_bool_vars;

1148 } else {

1149 ++num_int_vars;

1150 }

1151 }

1152 if (num_bool_vars > 0) {

1153 SOLVER_LOG(logger_, " - boolean variables:", num_bool_vars);

1154 }

1155 if (num_int_vars > 0) {

1156 SOLVER_LOG(logger_, " - integer variables:", num_int_vars);

1157 }

1158 if (num_float_vars > 0) {

1159 SOLVER_LOG(logger_, " - float variables:", num_float_vars);

1160 }

1161 if (num_set_vars > 0) {

1162 SOLVER_LOG(logger_, " - set variables:", num_set_vars);

1163 }

1165

1166

1167 int num_redundant_constraints = 0;

1168 int num_symmetry_breaking_constraints = 0;

1169 for (Constraint* const ct : model_.constraints()) {

1170 if (ct != nullptr && ct->active) {

1171 if (ct->is_redundant) {

1172 ++num_redundant_constraints;

1173 }

1174 if (ct->is_symmetric_breaking) {

1175 ++num_symmetry_breaking_constraints;

1176 }

1177 }

1178 }

1179 for (const auto& it : constraints_per_type_) {

1180 SOLVER_LOG(logger_, " - ", it.first, ": ", it.second.size());

1181 }

1183 if (num_redundant_constraints > 0) {

1185 " - redundant constraints: ", num_redundant_constraints);

1186 }

1187 if (num_symmetry_breaking_constraints > 0) {

1188 SOLVER_LOG(logger_, " - symmetry breaking constraints: ",

1189 num_symmetry_breaking_constraints);

1190 }

1191 if (model_.objective() == nullptr) {

1192 SOLVER_LOG(logger_, " - Satisfaction problem");

1193 } else {

1195 (model_.maximize() ? "Maximization" : "Minimization"),

1196 " problem");

1197 }

1199}

1202 constraints_per_type_.clear();

1203 constraints_per_variables_.clear();

1204 for (Constraint* const ct : model_.constraints()) {

1205 if (ct != nullptr && ct->active) {

1206 constraints_per_type_[ct->type].push_back(ct);

1207 absl::flat_hash_set<const Variable*> marked;

1208 for (const Argument& arg : ct->arguments) {

1210 marked.insert(var);

1211 }

1212 }

1213 for (const Variable* const var : marked) {

1214 constraints_per_variables_[var].push_back(ct);

1215 }

1216 }

1217 }

1218}

1226 }

1227 } else {

1228 out->push_back(ann);

1229 }

1230}

void BuildStatistics()

Definition model.cc:1201

void PrintStatistics() const

Definition model.cc:1133

void AddConstraint(absl::string_view id, std::vector< Argument > arguments, bool is_domain, bool symmetry, bool redundant)

Definition model.cc:1046

~Model()

Definition model.cc:1015

const std::vector< SolutionOutputSpecs > & output() const

Variable * AddVariable(absl::string_view name, const Domain &domain, bool defined, bool set_is_fixed=false)

Definition model.cc:1020

Variable * AddFloatConstant(double value)

Definition model.cc:1039

std::string DebugString() const

Definition model.cc:1081

void AddOutput(SolutionOutputSpecs output)

Definition model.cc:1058

void Maximize(Variable *obj, std::vector< Annotation > search_annotations)

Definition model.cc:1074

void Satisfy(std::vector< Annotation > search_annotations)

Definition model.cc:1062

const std::string & name() const

const std::vector< Annotation > & search_annotations() const

bool IsInconsistent() const

Definition model.cc:1116

void Minimize(Variable *obj, std::vector< Annotation > search_annotations)

Definition model.cc:1067

Variable * AddConstant(int64_t value)

Definition model.cc:1032

void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)

void STLDeleteElements(T *container)

void FlattenAnnotations(const Annotation &ann, std::vector< Annotation > *out)

Definition model.cc:1221

std::string JoinDebugStringPtr(const std::vector< T > &v, absl::string_view separator)

std::string JoinNameFieldPtr(const std::vector< T > &v, absl::string_view separator)

std::string JoinDebugString(const std::vector< T > &v, absl::string_view separator)

static Annotation String(absl::string_view str)

Definition model.cc:920

static Annotation FunctionCall(absl::string_view id)

Definition model.cc:870

void AppendAllVariables(std::vector< Variable * > *vars) const

Definition model.cc:929

static Annotation FunctionCallWithArguments(absl::string_view id, std::vector< Annotation > args)

Definition model.cc:859

static Annotation Empty()

Definition model.cc:833

static Annotation AnnotationList(std::vector< Annotation > list)

Definition model.cc:841

static Annotation IntegerList(const std::vector< int64_t > &values)

Definition model.cc:894

static Annotation VarRefArray(std::vector< Variable * > variables)

Definition model.cc:911

static Annotation Identifier(absl::string_view id)

Definition model.cc:850

std::vector< Variable * > variables

std::vector< int64_t > values

bool IsFunctionCallWithIdentifier(absl::string_view identifier) const

static Annotation VarRef(Variable *var)

Definition model.cc:902

static Annotation IntegerValue(int64_t value)

Definition model.cc:887

static Annotation Interval(int64_t interval_min, int64_t interval_max)

Definition model.cc:879

std::vector< Annotation > annotations

std::string DebugString() const

Definition model.cc:938

std::vector< Variable * > variables

static Argument FloatList(std::vector< double > floats)

Definition model.cc:582

int Size() const

Definition model.cc:751

Variable * Var() const

Definition model.cc:743

static Argument FloatValue(double value)

Definition model.cc:567

bool IsVariable() const

Definition model.cc:622

std::vector< Domain > domains

bool HasOneValueAt(int pos) const

Definition model.cc:721

Variable * VarAt(int pos) const

Definition model.cc:747

std::string DebugString() const

Definition model.cc:589

bool IsArrayOfValues() const

Definition model.cc:646

static Argument VoidArgument()

Definition model.cc:548

bool HasOneValue() const

Definition model.cc:624

static Argument IntegerValue(int64_t value)

Definition model.cc:505

int64_t ValueAt(int pos) const

Definition model.cc:699

static Argument Interval(int64_t imin, int64_t imax)

Definition model.cc:512

static Argument FromDomain(const Domain &domain)

Definition model.cc:554

int64_t Value() const

Definition model.cc:630

static Argument IntegerList(std::vector< int64_t > values)

Definition model.cc:520

static Argument VarRef(Variable *var)

Definition model.cc:534

static Argument FloatInterval(double lb, double ub)

Definition model.cc:574

std::vector< double > floats

bool Contains(int64_t value) const

Definition model.cc:684

static Argument DomainList(std::vector< Domain > domains)

Definition model.cc:527

static Argument VarRefArray(std::vector< Variable * > vars)

Definition model.cc:541

std::vector< int64_t > values

bool is_symmetric_breaking

std::string DebugString() const

Definition model.cc:805

void MarkAsInactive()

Definition model.cc:821

void RemoveArg(int arg_pos)

Definition model.cc:817

void SetAsFalse()

Definition model.cc:826

std::vector< Argument > arguments

static Domain Boolean()

Definition model.cc:67

static Domain AllFloats()

Definition model.cc:107

bool IntersectWithSingleton(int64_t value)

Definition model.cc:155

static Domain IntegerList(std::vector< int64_t > values)

Definition model.cc:40

bool OverlapsDomain(const Domain &other) const

Definition model.cc:425

static Domain IntegerValue(int64_t value)

Definition model.cc:53

int64_t Max() const

Definition model.cc:346

std::string DebugString() const

Definition model.cc:468

static Domain FloatValue(double value)

Definition model.cc:122

bool IntersectWithInterval(int64_t interval_min, int64_t interval_max)

Definition model.cc:159

bool IntersectWithDomain(const Domain &domain)

Definition model.cc:129

bool SetEmptyFloatDomain()

Definition model.cc:324

bool empty() const

Definition model.cc:335

static Domain EmptyDomain()

Definition model.cc:105

bool IntersectWithFloatDomain(const Domain &domain)

Definition model.cc:254

bool RemoveValue(int64_t value)

Definition model.cc:437

static Domain FloatInterval(double lb, double ub)

Definition model.cc:114

int64_t Min() const

Definition model.cc:340

std::vector< int64_t > values

static Domain SetOfBoolean()

Definition model.cc:99

static Domain Interval(int64_t included_min, int64_t included_max)

Definition model.cc:59

static Domain SetOfAllInt64()

Definition model.cc:81

static Domain SetOfInterval(int64_t included_min, int64_t included_max)

Definition model.cc:93

bool Contains(int64_t value) const

Definition model.cc:363

bool OverlapsIntInterval(int64_t lb, int64_t ub) const

Definition model.cc:411

std::vector< double > float_values

static Domain SetOfIntegerList(std::vector< int64_t > values)

Definition model.cc:75

static Domain SetOfIntegerValue(int64_t value)

Definition model.cc:87

bool HasOneValue() const

Definition model.cc:331

int64_t Value() const

Definition model.cc:352

static Domain AllInt64()

Definition model.cc:47

bool IntersectWithListOfIntegers(absl::Span< const int64_t > integers)

Definition model.cc:207

bool IsAllInt64() const

Definition model.cc:357

bool OverlapsIntList(const std::vector< int64_t > &vec) const

Definition model.cc:387

std::string DebugString() const

Definition model.cc:971

std::vector< Variable * > flat_variables

static SolutionOutputSpecs MultiDimensionalArray(absl::string_view name, std::vector< Bounds > bounds, std::vector< Variable * > flat_variables, bool display_as_boolean)

Definition model.cc:984

std::string DebugString() const

Definition model.cc:1003

static SolutionOutputSpecs VoidOutput()

Definition model.cc:996

static SolutionOutputSpecs SingleVariable(absl::string_view name, Variable *variable, bool display_as_boolean)

Definition model.cc:975

std::vector< Bounds > bounds

bool Merge(absl::string_view other_name, const Domain &other_domain, bool other_temporary)

Definition model.cc:783

std::string DebugString() const

Definition model.cc:793

#define SOLVER_LOG(logger,...)