this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2
3/*
4 * Main authors:
5 * Jip J. Dekker <jip.dekker@monash.edu>
6 */
7
8/* This Source Code Form is subject to the terms of the Mozilla Public
9 * License, v. 2.0. If a copy of the MPL was not distributed with this
10 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
11
12#include <minizinc/solvers/geas/geas_constraints.hh>
13#include <minizinc/solvers/geas_solverinstance.hh>
14
15namespace MiniZinc {
16GeasSolverInstance::GeasSolverInstance(Env& env, std::ostream& log,
17 SolverInstanceBase::Options* opt)
18 : SolverInstanceImpl<GeasTypes>(env, log, opt), _flat(env.flat()) {
19 registerConstraints();
20}
21
22void GeasSolverInstance::registerConstraint(const std::string& name, poster p) {
23 _constraintRegistry.add("geas_" + name, p);
24 _constraintRegistry.add(name, p);
25}
26
27void GeasSolverInstance::registerConstraints() {
28 GCLock lock;
29
30 /* Integer Comparison Constraints */
31 registerConstraint("int_eq", GeasConstraints::p_int_eq);
32 registerConstraint("int_ne", GeasConstraints::p_int_ne);
33 registerConstraint("int_le", GeasConstraints::p_int_le);
34 registerConstraint("int_lt", GeasConstraints::p_int_lt);
35 registerConstraint("int_eq_imp", GeasConstraints::p_int_eq_imp);
36 registerConstraint("int_ne_imp", GeasConstraints::p_int_ne_imp);
37 registerConstraint("int_le_imp", GeasConstraints::p_int_le_imp);
38 registerConstraint("int_lt_imp", GeasConstraints::p_int_lt_imp);
39 registerConstraint("int_eq_reif", GeasConstraints::p_int_eq_reif);
40 registerConstraint("int_ne_reif", GeasConstraints::p_int_ne_reif);
41 registerConstraint("int_le_reif", GeasConstraints::p_int_le_reif);
42 registerConstraint("int_lt_reif", GeasConstraints::p_int_lt_reif);
43
44 /* Integer Arithmetic Constraints */
45 registerConstraint("int_abs", GeasConstraints::p_int_abs);
46 registerConstraint("int_times", GeasConstraints::p_int_times);
47 registerConstraint("int_div", GeasConstraints::p_int_div);
48 // registerConstraint("int_mod", GeasConstraints::p_int_mod);
49 registerConstraint("int_min", GeasConstraints::p_int_min);
50 registerConstraint("int_max", GeasConstraints::p_int_max);
51
52 /* Integer Linear Constraints */
53 registerConstraint("int_lin_eq", GeasConstraints::p_int_lin_eq);
54 registerConstraint("int_lin_ne", GeasConstraints::p_int_lin_ne);
55 registerConstraint("int_lin_le", GeasConstraints::p_int_lin_le);
56 registerConstraint("int_lin_eq_imp", GeasConstraints::p_int_lin_eq_imp);
57 registerConstraint("int_lin_ne_imp", GeasConstraints::p_int_lin_ne_imp);
58 registerConstraint("int_lin_le_imp", GeasConstraints::p_int_lin_le_imp);
59 registerConstraint("int_lin_eq_reif", GeasConstraints::p_int_lin_eq_reif);
60 registerConstraint("int_lin_ne_reif", GeasConstraints::p_int_lin_ne_reif);
61 registerConstraint("int_lin_le_reif", GeasConstraints::p_int_lin_le_reif);
62
63 /* Boolean Comparison Constraints */
64 registerConstraint("bool_eq", GeasConstraints::p_bool_eq);
65 registerConstraint("bool_ne", GeasConstraints::p_bool_ne);
66 registerConstraint("bool_le", GeasConstraints::p_bool_le);
67 registerConstraint("bool_lt", GeasConstraints::p_bool_lt);
68 registerConstraint("bool_eq_imp", GeasConstraints::p_bool_eq_imp);
69 registerConstraint("bool_ne_imp", GeasConstraints::p_bool_ne_imp);
70 registerConstraint("bool_le_imp", GeasConstraints::p_bool_le_imp);
71 registerConstraint("bool_lt_imp", GeasConstraints::p_bool_lt_imp);
72 registerConstraint("bool_eq_reif", GeasConstraints::p_bool_eq_reif);
73 registerConstraint("bool_ne_reif", GeasConstraints::p_bool_ne_reif);
74 registerConstraint("bool_le_reif", GeasConstraints::p_bool_le_reif);
75 registerConstraint("bool_lt_reif", GeasConstraints::p_bool_lt_reif);
76
77 /* Boolean Arithmetic Constraints */
78 registerConstraint("bool_or", GeasConstraints::p_bool_or);
79 registerConstraint("bool_and", GeasConstraints::p_bool_and);
80 registerConstraint("bool_xor", GeasConstraints::p_bool_xor);
81 registerConstraint("bool_not", GeasConstraints::p_bool_not);
82 registerConstraint("bool_or_imp", GeasConstraints::p_bool_or_imp);
83 registerConstraint("bool_and_imp", GeasConstraints::p_bool_and_imp);
84 registerConstraint("bool_xor_imp", GeasConstraints::p_bool_xor_imp);
85
86 registerConstraint("bool_clause", GeasConstraints::p_bool_clause);
87 registerConstraint("array_bool_or", GeasConstraints::p_array_bool_or);
88 registerConstraint("array_bool_and", GeasConstraints::p_array_bool_and);
89 registerConstraint("bool_clause_imp", GeasConstraints::p_bool_clause_imp);
90 registerConstraint("array_bool_or_imp", GeasConstraints::p_array_bool_or_imp);
91 registerConstraint("array_bool_and_imp", GeasConstraints::p_array_bool_and_imp);
92 registerConstraint("bool_clause_reif", GeasConstraints::p_bool_clause_reif);
93
94 /* Boolean Linear Constraints */
95 registerConstraint("bool_lin_eq", GeasConstraints::p_bool_lin_eq);
96 registerConstraint("bool_lin_ne", GeasConstraints::p_bool_lin_ne);
97 registerConstraint("bool_lin_le", GeasConstraints::p_bool_lin_le);
98 registerConstraint("bool_lin_eq_imp", GeasConstraints::p_bool_lin_eq_imp);
99 registerConstraint("bool_lin_ne_imp", GeasConstraints::p_bool_lin_ne_imp);
100 registerConstraint("bool_lin_le_imp", GeasConstraints::p_bool_lin_le_imp);
101 registerConstraint("bool_lin_eq_reif", GeasConstraints::p_bool_lin_eq_reif);
102 registerConstraint("bool_lin_ne_reif", GeasConstraints::p_bool_lin_ne_reif);
103 registerConstraint("bool_lin_le_reif", GeasConstraints::p_bool_lin_le_reif);
104
105 /* Coercion Constraints */
106 registerConstraint("bool2int", GeasConstraints::p_bool2int);
107
108 /* Element Constraints */
109 registerConstraint("array_int_element", GeasConstraints::p_array_int_element);
110 registerConstraint("array_bool_element", GeasConstraints::p_array_bool_element);
111 registerConstraint("array_var_int_element", GeasConstraints::p_array_var_int_element);
112 registerConstraint("array_var_bool_element", GeasConstraints::p_array_var_bool_element);
113
114 /* Global Constraints */
115 registerConstraint("all_different_int", GeasConstraints::p_all_different);
116 registerConstraint("alldifferent_except_0", GeasConstraints::p_all_different_except_0);
117 registerConstraint("at_most", GeasConstraints::p_at_most);
118 registerConstraint("at_most1", GeasConstraints::p_at_most1);
119 registerConstraint("cumulative", GeasConstraints::p_cumulative);
120 registerConstraint("cumulative_var", GeasConstraints::p_cumulative);
121 registerConstraint("disjunctive", GeasConstraints::p_disjunctive);
122 registerConstraint("disjunctive_var", GeasConstraints::p_disjunctive);
123 registerConstraint("global_cardinality", GeasConstraints::p_global_cardinality);
124 registerConstraint("table_int", GeasConstraints::p_table_int);
125
126 /**** TODO: NOT YET SUPPORTED: ****/
127 /* Boolean Arithmetic Constraints */
128 // registerConstraint("array_bool_xor", GeasConstraints::p_array_bool_xor);
129 // registerConstraint("array_bool_xor_imp", GeasConstraints::p_array_bool_xor_imp);
130
131 /* Floating Point Comparison Constraints */
132 // registerConstraint("float_eq", GeasConstraints::p_float_eq);
133 // registerConstraint("float_le", GeasConstraints::p_float_le);
134 // registerConstraint("float_lt", GeasConstraints::p_float_lt);
135 // registerConstraint("float_ne", GeasConstraints::p_float_ne);
136 // registerConstraint("float_eq_reif", GeasConstraints::p_float_eq_reif);
137 // registerConstraint("float_le_reif", GeasConstraints::p_float_le_reif);
138 // registerConstraint("float_lt_reif", GeasConstraints::p_float_lt_reif);
139
140 /* Floating Point Arithmetic Constraints */
141 // registerConstraint("float_abs", GeasConstraints::p_float_abs);
142 // registerConstraint("float_sqrt", GeasConstraints::p_float_sqrt);
143 // registerConstraint("float_times", GeasConstraints::p_float_times);
144 // registerConstraint("float_div", GeasConstraints::p_float_div);
145 // registerConstraint("float_plus", GeasConstraints::p_float_plus);
146 // registerConstraint("float_max", GeasConstraints::p_float_max);
147 // registerConstraint("float_min", GeasConstraints::p_float_min);
148 // registerConstraint("float_acos", GeasConstraints::p_float_acos);
149 // registerConstraint("float_asin", GeasConstraints::p_float_asin);
150 // registerConstraint("float_atan", GeasConstraints::p_float_atan);
151 // registerConstraint("float_cos", GeasConstraints::p_float_cos);
152 // registerConstraint("float_exp", GeasConstraints::p_float_exp);
153 // registerConstraint("float_ln", GeasConstraints::p_float_ln);
154 // registerConstraint("float_log10", GeasConstraints::p_float_log10);
155 // registerConstraint("float_log2", GeasConstraints::p_float_log2);
156 // registerConstraint("float_sin", GeasConstraints::p_float_sin);
157 // registerConstraint("float_tan", GeasConstraints::p_float_tan);
158
159 /* Floating Linear Constraints */
160 // registerConstraint("float_lin_eq", GeasConstraints::p_float_lin_eq);
161 // registerConstraint("float_lin_eq_reif", GeasConstraints::p_float_lin_eq_reif);
162 // registerConstraint("float_lin_le", GeasConstraints::p_float_lin_le);
163 // registerConstraint("float_lin_le_reif", GeasConstraints::p_float_lin_le_reif);
164
165 /* Coercion Constraints */
166 // registerConstraint("int2float", GeasConstraints::p_int2float);
167}
168
169void GeasSolverInstance::processFlatZinc() {
170 auto _opt = static_cast<GeasOptions&>(*_options);
171 // Create variables
172 zero = _solver.new_intvar(0, 0);
173 for (auto it = _flat->vardecls().begin(); it != _flat->vardecls().end(); ++it) {
174 if (!it->removed() && it->e()->type().isvar() && it->e()->type().dim() == 0) {
175 VarDecl* vd = it->e();
176
177 if (vd->type().isbool()) {
178 if (vd->e() == nullptr) {
179 Expression* domain = vd->ti()->domain();
180 long long int lb;
181 long long int ub;
182 if (domain != nullptr) {
183 IntBounds ib = compute_int_bounds(_env.envi(), domain);
184 lb = ib.l.toInt();
185 ub = ib.u.toInt();
186 } else {
187 lb = 0;
188 ub = 1;
189 }
190 if (lb == ub) {
191 geas::patom_t val = (lb == 0) ? geas::at_False : geas::at_True;
192 _variableMap.insert(vd->id(), GeasVariable(val));
193 } else {
194 auto var = _solver.new_boolvar();
195 _variableMap.insert(vd->id(), GeasVariable(var));
196 }
197 } else {
198 Expression* init = vd->e();
199 if (init->isa<Id>() || init->isa<ArrayAccess>()) {
200 GeasVariable& var = resolveVar(init);
201 assert(var.isBool());
202 _variableMap.insert(vd->id(), GeasVariable(var.boolVar()));
203 } else {
204 auto b = init->cast<BoolLit>()->v();
205 geas::patom_t val = b ? geas::at_True : geas::at_False;
206 _variableMap.insert(vd->id(), GeasVariable(val));
207 }
208 }
209 } else if (vd->type().isfloat()) {
210 if (vd->e() == nullptr) {
211 Expression* domain = vd->ti()->domain();
212 double lb;
213 double ub;
214 if (domain != nullptr) {
215 FloatBounds fb = compute_float_bounds(_env.envi(), vd->id());
216 lb = fb.l.toDouble();
217 ub = fb.u.toDouble();
218 } else {
219 std::ostringstream ss;
220 ss << "GeasSolverInstance::processFlatZinc: Error: Unbounded variable: "
221 << vd->id()->str();
222 throw Error(ss.str());
223 }
224 // TODO: Error correction from double to float??
225 auto var = _solver.new_floatvar(static_cast<geas::fp::val_t>(lb),
226 static_cast<geas::fp::val_t>(ub));
227 _variableMap.insert(vd->id(), GeasVariable(var));
228 } else {
229 Expression* init = vd->e();
230 if (init->isa<Id>() || init->isa<ArrayAccess>()) {
231 GeasVariable& var = resolveVar(init);
232 assert(var.isFloat());
233 _variableMap.insert(vd->id(), GeasVariable(var.floatVar()));
234 } else {
235 double fl = init->cast<FloatLit>()->v().toDouble();
236 auto var = _solver.new_floatvar(static_cast<geas::fp::val_t>(fl),
237 static_cast<geas::fp::val_t>(fl));
238 _variableMap.insert(vd->id(), GeasVariable(var));
239 }
240 }
241 } else if (vd->type().isint()) {
242 if (vd->e() == nullptr) {
243 Expression* domain = vd->ti()->domain();
244 if (domain != nullptr) {
245 IntSetVal* isv = eval_intset(env().envi(), domain);
246 auto var = _solver.new_intvar(static_cast<geas::intvar::val_t>(isv->min().toInt()),
247 static_cast<geas::intvar::val_t>(isv->max().toInt()));
248 if (isv->size() > 1) {
249 vec<int> vals(static_cast<int>(isv->card().toInt()));
250 int i = 0;
251 for (int j = 0; j < isv->size(); ++j) {
252 for (auto k = isv->min(j).toInt(); k <= isv->max(j).toInt(); ++k) {
253 vals[i++] = static_cast<int>(k);
254 }
255 }
256 assert(i == isv->card().toInt());
257 auto res = geas::make_sparse(var, vals);
258 assert(res);
259 }
260 _variableMap.insert(vd->id(), GeasVariable(var));
261 } else {
262 std::ostringstream ss;
263 ss << "GeasSolverInstance::processFlatZinc: Error: Unbounded variable: "
264 << vd->id()->str();
265 throw Error(ss.str());
266 }
267 } else {
268 Expression* init = vd->e();
269 if (init->isa<Id>() || init->isa<ArrayAccess>()) {
270 GeasVariable& var = resolveVar(init);
271 assert(var.isInt());
272 _variableMap.insert(vd->id(), GeasVariable(var.intVar()));
273 } else {
274 auto il = init->cast<IntLit>()->v().toInt();
275 auto var = _solver.new_intvar(static_cast<geas::intvar::val_t>(il),
276 static_cast<geas::intvar::val_t>(il));
277 _variableMap.insert(vd->id(), GeasVariable(var));
278 }
279 }
280 } else {
281 std::stringstream ssm;
282 ssm << "Type " << *vd->ti() << " is currently not supported by Geas.";
283 throw InternalError(ssm.str());
284 }
285 }
286 }
287
288 // Post constraints
289 for (ConstraintIterator it = _flat->constraints().begin(); it != _flat->constraints().end();
290 ++it) {
291 if (!it->removed()) {
292 if (auto* c = it->e()->dynamicCast<Call>()) {
293 _constraintRegistry.post(c);
294 }
295 }
296 }
297 // Set objective
298 SolveI* si = _flat->solveItem();
299 if (si->e() != nullptr) {
300 _objType = si->st();
301 if (_objType == SolveI::ST_MIN) {
302 _objVar = std::unique_ptr<GeasTypes::Variable>(new GeasTypes::Variable(resolveVar(si->e())));
303 } else if (_objType == SolveI::ST_MAX) {
304 _objType = SolveI::ST_MIN;
305 _objVar = std::unique_ptr<GeasTypes::Variable>(new GeasTypes::Variable(-asIntVar(si->e())));
306 }
307 }
308 if (!si->ann().isEmpty()) {
309 std::vector<Expression*> flatAnn;
310 flattenSearchAnnotations(si->ann(), flatAnn);
311
312 for (auto& ann : flatAnn) {
313 if (ann->isa<Call>()) {
314 Call* call = ann->cast<Call>();
315 if (call->id() == "warm_start") {
316 auto* vars = eval_array_lit(env().envi(), call->arg(0));
317 auto* vals = eval_array_lit(env().envi(), call->arg(1));
318 assert(vars->size() == vals->size());
319 vec<geas::patom_t> ws(static_cast<int>(vars->size()));
320
321 if (vars->type().isIntArray()) {
322 assert(vals->type().isIntArray());
323 for (int i = 0; i < vars->size(); ++i) {
324 geas::intvar var = asIntVar((*vars)[i]);
325 int val = asInt((*vals)[i]);
326 ws.push(var == val);
327 }
328 } else if (vars->type().isBoolArray()) {
329 assert(vals->type().isBoolArray());
330 for (int i = 0; i < vars->size(); ++i) {
331 geas::patom_t var = asBoolVar((*vars)[i]);
332 bool val = asBool((*vals)[i]);
333 ws.push(val ? var : ~var);
334 }
335 } else {
336 std::cerr << "WARNING Geas: ignoring warm start annotation of invalid type: " << *ann
337 << std::endl;
338 continue;
339 }
340 _solver.data->branchers.push(geas::warmstart_brancher(ws));
341 continue;
342 }
343
344 vec<geas::pid_t> pids;
345 geas::VarChoice select = geas::Var_FirstFail;
346 geas::ValChoice choice = geas::Val_Min;
347 if (call->id() == "int_search") {
348 vec<geas::intvar> iv = asIntVar(eval_array_lit(env().envi(), call->arg(0)));
349 pids.growTo(iv.size());
350 for (int i = 0; i < iv.size(); ++i) {
351 pids[i] = iv[i].p;
352 }
353 } else if (call->id() == "bool_search") {
354 vec<geas::patom_t> bv = asBoolVar(eval_array_lit(env().envi(), call->arg(0)));
355 pids.growTo(bv.size());
356 for (int i = 0; i < bv.size(); ++i) {
357 pids[i] = bv[i].pid;
358 }
359 } else {
360 std::cerr << "WARNING Geas: ignoring unknown search annotation: " << *ann << std::endl;
361 continue;
362 }
363 ASTString select_str = call->arg(1)->cast<Id>()->str();
364 if (select_str == "input_order") {
365 select = geas::Var_InputOrder;
366 } else if (select_str == "first_fail") {
367 select = geas::Var_FirstFail;
368 } else if (select_str == "largest") {
369 select = geas::Var_Largest;
370 } else if (select_str == "smallest") {
371 select = geas::Var_Smallest;
372 } else {
373 std::cerr << "WARNING Geas: unknown variable selection '" << select_str
374 << "', using default value First Fail." << std::endl;
375 }
376 ASTString choice_str = call->arg(2)->cast<Id>()->str();
377 if (choice_str == "indomain_max") {
378 choice = geas::Val_Max;
379 } else if (choice_str == "indomain_min") {
380 choice = geas::Val_Min;
381 } else if (choice_str == "indomain_split") {
382 choice = geas::Val_Split;
383 } else {
384 std::cerr << "WARNING Geas: unknown value selection '" << choice_str
385 << "', using Indomain Min." << std::endl;
386 }
387
388 geas::brancher* b = geas::basic_brancher(select, choice, pids);
389 if (_opt.freeSearch) {
390 vec<geas::brancher*> brv({b, _solver.data->last_branch});
391 _solver.data->branchers.push(geas::toggle_brancher(brv));
392 } else {
393 _solver.data->branchers.push(b);
394 }
395 }
396 }
397 }
398}
399
400bool GeasSolverInstance::addSolutionNoGood() {
401 assert(!_varsWithOutput.empty());
402 geas::model solution = _solver.get_model();
403 vec<geas::clause_elt> clause;
404 for (auto& var : _varsWithOutput) {
405 if (Expression::dynamicCast<Call>(
406 get_annotation(var->ann(), constants().ann.output_array.aststr())) != nullptr) {
407 if (auto* al = var->e()->dynamicCast<ArrayLit>()) {
408 for (int j = 0; j < al->size(); j++) {
409 if (Id* id = (*al)[j]->dynamicCast<Id>()) {
410 auto geas_var = resolveVar(id);
411 if (geas_var.isBool()) {
412 geas::patom_t bv = geas_var.boolVar();
413 clause.push(solution.value(bv) ? ~bv : bv);
414 } else if (geas_var.isFloat()) {
415 geas::fp::fpvar fv = geas_var.floatVar();
416 clause.push(fv < solution[fv]);
417 clause.push(fv > solution[fv]);
418 } else {
419 geas::intvar iv = geas_var.intVar();
420 clause.push(~(iv == solution[iv]));
421 }
422 }
423 }
424 }
425 } else {
426 auto geas_var = resolveVar(var);
427 if (geas_var.isBool()) {
428 geas::patom_t bv = geas_var.boolVar();
429 clause.push(solution.value(bv) ? ~bv : bv);
430 } else if (geas_var.isFloat()) {
431 geas::fp::fpvar fv = geas_var.floatVar();
432 clause.push(fv < solution[fv]);
433 clause.push(fv > solution[fv]);
434 } else {
435 geas::intvar iv = geas_var.intVar();
436 clause.push(iv != solution[iv]);
437 }
438 }
439 }
440 return geas::add_clause(*_solver.data, clause);
441}
442
443SolverInstanceBase::Status MiniZinc::GeasSolverInstance::solve() {
444 SolverInstanceBase::Status status = SolverInstance::ERROR;
445 auto _opt = static_cast<GeasOptions&>(*_options);
446 auto remaining_time = [_opt] {
447 if (_opt.time == std::chrono::milliseconds(0)) {
448 return 0.0;
449 }
450 using geas_time = std::chrono::duration<double>;
451 static auto timeout = std::chrono::high_resolution_clock::now() + _opt.time;
452 return geas_time(timeout - std::chrono::high_resolution_clock::now()).count();
453 };
454 if (_objType == SolveI::ST_SAT) {
455 int nr_solutions = 0;
456 geas::solver::result res = geas::solver::UNKNOWN;
457 while ((_opt.allSolutions || nr_solutions < _opt.nrSolutions) && remaining_time() >= 0.0) {
458 res = _solver.solve({remaining_time(), _opt.conflicts - _solver.data->stats.conflicts});
459 printSolution();
460 if (res != geas::solver::SAT) {
461 break;
462 }
463 nr_solutions++;
464 _solver.restart();
465 if (!addSolutionNoGood()) {
466 res = geas::solver::UNSAT;
467 break;
468 }
469 }
470 switch (res) {
471 case geas::solver::SAT:
472 status = SolverInstance::SAT;
473 break;
474 case geas::solver::UNSAT:
475 if (nr_solutions > 0) {
476 status = SolverInstance::OPT;
477 } else {
478 status = SolverInstance::UNSAT;
479 }
480 break;
481 case geas::solver::UNKNOWN:
482 if (nr_solutions > 0) {
483 status = SolverInstance::SAT;
484 } else {
485 status = SolverInstance::UNKNOWN;
486 }
487 break;
488 default:
489 status = SolverInstance::ERROR;
490 break;
491 }
492 } else {
493 assert(_objType == SolveI::ST_MIN);
494 // TODO: Add float objectives
495 assert(_objVar->isInt());
496 geas::intvar obj = _objVar->intVar();
497 geas::solver::result res;
498 while (true) {
499 res = _solver.solve({remaining_time(), _opt.conflicts - _solver.data->stats.conflicts});
500 geas::intvar::val_t obj_val;
501 if (res != geas::solver::SAT) {
502 break;
503 }
504 status = SolverInstance::SAT;
505 if (_opt.allSolutions) {
506 printSolution();
507 }
508 obj_val = _solver.get_model()[obj];
509
510 int step = 1;
511 while (_opt.objProbeLimit > 0) {
512 geas::intvar::val_t assumed_obj;
513 assumed_obj = obj_val - step;
514 assumed_obj = obj.lb(_solver.data) > assumed_obj ? obj.lb(_solver.data) : assumed_obj;
515 if (!_solver.assume(obj == assumed_obj)) {
516 _solver.retract();
517 break;
518 }
519 res = _solver.solve({remaining_time(), _opt.objProbeLimit});
520 _solver.retract();
521 if (res != geas::solver::SAT) {
522 break;
523 }
524 step *= 2;
525 if (_opt.allSolutions) {
526 printSolution();
527 }
528 obj_val = _solver.get_model()[obj];
529 }
530 _solver.post(obj < obj_val);
531 }
532 if (status == SolverInstance::ERROR) {
533 switch (res) {
534 case geas::solver::UNSAT:
535 status = SolverInstance::UNSAT;
536 break;
537 case geas::solver::UNKNOWN:
538 status = SolverInstance::UNKNOWN;
539 break;
540 default:
541 assert(false);
542 status = SolverInstance::ERROR;
543 break;
544 }
545 } else {
546 if (res == geas::solver::UNSAT) {
547 status = SolverInstance::OPT;
548 }
549 if (!_opt.allSolutions) {
550 printSolution();
551 }
552 }
553 }
554 if (_opt.statistics) {
555 printStatistics();
556 }
557 return status;
558}
559
560Expression* GeasSolverInstance::getSolutionValue(Id* id) {
561 id = id->decl()->id();
562 if (id->type().isvar()) {
563 GeasVariable& var = resolveVar(id->decl()->id());
564 geas::model solution = _solver.get_model();
565 switch (id->type().bt()) {
566 case Type::BT_BOOL:
567 assert(var.isBool());
568 return constants().boollit(solution.value(var.boolVar()));
569 case Type::BT_FLOAT:
570 assert(var.isFloat());
571 return FloatLit::a(solution[var.floatVar()]);
572 case Type::BT_INT:
573 assert(var.isInt());
574 return IntLit::a(solution[var.intVar()]);
575 default:
576 return nullptr;
577 }
578 } else {
579 return id->decl()->e();
580 }
581}
582
583void GeasSolverInstance::resetSolver() { assert(false); }
584
585GeasTypes::Variable& GeasSolverInstance::resolveVar(Expression* e) {
586 if (auto* id = e->dynamicCast<Id>()) {
587 return _variableMap.get(id->decl()->id());
588 }
589 if (auto* vd = e->dynamicCast<VarDecl>()) {
590 return _variableMap.get(vd->id()->decl()->id());
591 }
592 if (auto* aa = e->dynamicCast<ArrayAccess>()) {
593 auto* ad = aa->v()->cast<Id>()->decl();
594 auto idx = aa->idx()[0]->cast<IntLit>()->v().toInt();
595 auto* al = eval_array_lit(_env.envi(), ad->e());
596 return _variableMap.get((*al)[idx]->cast<Id>());
597 }
598 std::stringstream ssm;
599 ssm << "Expected Id, VarDecl or ArrayAccess instead of \"" << *e << "\"";
600 throw InternalError(ssm.str());
601}
602
603vec<bool> GeasSolverInstance::asBool(ArrayLit* al) {
604 vec<bool> vec(static_cast<int>(al->size()));
605 for (int i = 0; i < al->size(); ++i) {
606 vec[i] = asBool((*al)[i]);
607 }
608 return vec;
609}
610
611geas::patom_t GeasSolverInstance::asBoolVar(Expression* e) {
612 if (e->type().isvar()) {
613 GeasVariable& var = resolveVar(follow_id_to_decl(e));
614 assert(var.isBool());
615 return var.boolVar();
616 }
617 if (auto* bl = e->dynamicCast<BoolLit>()) {
618 return bl->v() ? geas::at_True : geas::at_False;
619 }
620 std::stringstream ssm;
621 ssm << "Expected bool or int literal instead of: " << *e;
622 throw InternalError(ssm.str());
623}
624
625vec<geas::patom_t> GeasSolverInstance::asBoolVar(ArrayLit* al) {
626 vec<geas::patom_t> vec(static_cast<int>(al->size()));
627 for (int i = 0; i < al->size(); ++i) {
628 vec[i] = this->asBoolVar((*al)[i]);
629 }
630 return vec;
631}
632
633vec<int> GeasSolverInstance::asInt(ArrayLit* al) {
634 vec<int> vec(static_cast<int>(al->size()));
635 for (int i = 0; i < al->size(); ++i) {
636 vec[i] = this->asInt((*al)[i]);
637 }
638 return vec;
639}
640
641geas::intvar GeasSolverInstance::asIntVar(Expression* e) {
642 if (e->type().isvar()) {
643 GeasVariable& var = resolveVar(follow_id_to_decl(e));
644 assert(var.isInt());
645 return var.intVar();
646 }
647 IntVal i;
648 if (auto* il = e->dynamicCast<IntLit>()) {
649 i = il->v().toInt();
650 } else if (auto* bl = e->dynamicCast<BoolLit>()) {
651 i = static_cast<long long>(bl->v());
652 } else {
653 std::stringstream ssm;
654 ssm << "Expected bool or int literal instead of: " << *e;
655 throw InternalError(ssm.str());
656 }
657 if (i == 0) {
658 return zero;
659 }
660 return _solver.new_intvar(static_cast<geas::intvar::val_t>(i.toInt()),
661 static_cast<geas::intvar::val_t>(i.toInt()));
662}
663
664vec<geas::intvar> GeasSolverInstance::asIntVar(ArrayLit* al) {
665 vec<geas::intvar> vec(static_cast<int>(al->size()));
666 for (int i = 0; i < al->size(); ++i) {
667 vec[i] = this->asIntVar((*al)[i]);
668 }
669 return vec;
670}
671
672void GeasSolverInstance::printStatistics() {
673 auto& st = _solver.data->stats;
674 auto& out = getSolns2Out()->getOutput();
675
676 out << "%%%mzn-stat: failures=" << st.conflicts << std::endl; // TODO: Statistic name
677 out << "%%%mzn-stat: solveTime=" << st.time << std::endl;
678 out << "%%%mzn-stat: solutions=" << st.solutions << std::endl;
679 out << "%%%mzn-stat: restarts=" << st.restarts << std::endl;
680 out << "%%%mzn-stat: nogoods=" << st.num_learnts << std::endl; // TODO: Statistic name
681 out << "%%%mzn-stat: learntLiterals=" << st.num_learnt_lits << std::endl; // TODO: Statistic name
682}
683
684GeasSolverFactory::GeasSolverFactory() {
685 SolverConfig sc("org.minizinc.geas", getVersion(nullptr));
686 sc.name("Geas");
687 sc.mznlib("-Ggeas");
688 sc.mznlibVersion(1);
689 sc.supportsMzn(false);
690 sc.description(getDescription(nullptr));
691 sc.tags({
692 "api",
693 "cp",
694 "float",
695 "int",
696 "lcg",
697 });
698 sc.stdFlags({"-a", "-f", "-n", "-s", "-t"});
699 sc.extraFlags({
700 SolverConfig::ExtraFlag("--conflicts",
701 "Limit the maximum number of conflicts to be used during solving.",
702 SolverConfig::ExtraFlag::FlagType::T_INT, {}, "0"),
703 SolverConfig::ExtraFlag(
704 "--obj-probe",
705 "Number of conflicts to use to probe for better solutions after a new solution is found.",
706 SolverConfig::ExtraFlag::FlagType::T_INT, {}, "0"),
707 });
708 SolverConfigs::registerBuiltinSolver(sc);
709};
710
711SolverInstanceBase::Options* GeasSolverFactory::createOptions() { return new GeasOptions; }
712
713SolverInstanceBase* GeasSolverFactory::doCreateSI(Env& env, std::ostream& log,
714 SolverInstanceBase::Options* opt) {
715 return new GeasSolverInstance(env, log, opt);
716}
717
718bool GeasSolverFactory::processOption(SolverInstanceBase::Options* opt, int& i,
719 std::vector<std::string>& argv,
720 const std::string& workingDir) {
721 auto* _opt = static_cast<GeasOptions*>(opt);
722 if (argv[i] == "-a" || argv[i] == "--all-solutions") {
723 _opt->allSolutions = true;
724 } else if (argv[i] == "--conflicts") {
725 if (++i == argv.size()) {
726 return false;
727 }
728 int nodes = atoi(argv[i].c_str());
729 if (nodes >= 0) {
730 _opt->conflicts = nodes;
731 }
732 } else if (argv[i] == "-f") {
733 _opt->freeSearch = true;
734 } else if (argv[i] == "-n") {
735 if (++i == argv.size()) {
736 return false;
737 }
738 int n = atoi(argv[i].c_str());
739 if (n >= 0) {
740 _opt->nrSolutions = n;
741 }
742 } else if (argv[i] == "--obj-probe") {
743 if (++i == argv.size()) {
744 return false;
745 }
746 int limit = atoi(argv[i].c_str());
747 if (limit >= 0) {
748 _opt->objProbeLimit = limit;
749 }
750 } else if (argv[i] == "--solver-statistics" || argv[i] == "-s") {
751 _opt->statistics = true;
752 } else if (argv[i] == "--solver-time-limit" || argv[i] == "-t") {
753 if (++i == argv.size()) {
754 return false;
755 }
756 int time = atoi(argv[i].c_str());
757 if (time >= 0) {
758 _opt->time = std::chrono::milliseconds(time);
759 }
760 } else {
761 return false;
762 }
763 return true;
764}
765
766void GeasSolverFactory::printHelp(std::ostream& os) {
767 os << "Geas solver plugin options:" << std::endl
768 << " --conflicts <int>" << std::endl
769 << " Limit the maximum number of conflicts to be used during solving." << std::endl
770 << " --obj-probe <int>" << std::endl
771 << " Number of conflicts to use to probe for better solutions after a new solution is "
772 "found."
773 << std::endl
774 << std::endl;
775}
776} // namespace MiniZinc