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