this repo has no description
dekker.one
1/*
2 * Main authors:
3 * Kevin Leo <kevin.leo@monash.edu>
4 * Andrea Rendl <andrea.rendl@nicta.com.au>
5 * Guido Tack <guido.tack@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/ast.hh>
13#include <minizinc/eval_par.hh>
14#include <minizinc/exception.hh>
15#include <minizinc/solvers/gecode/fzn_space.hh>
16#include <minizinc/solvers/gecode/gecode_constraints.hh>
17#include <minizinc/solvers/gecode_solverinstance.hh>
18
19#include "aux_brancher.hh"
20
21using namespace std;
22using namespace Gecode;
23
24namespace MiniZinc {
25
26Gecode_SolverFactory::Gecode_SolverFactory(void) {
27 SolverConfig sc("org.minizinc.gecode_presolver", GECODE_VERSION);
28 sc.name("Presolver");
29 sc.mznlib("-Ggecode_presolver");
30 sc.mznlibVersion(1);
31 sc.supportsMzn(false);
32 sc.description("Internal Gecode presolver plugin");
33 sc.tags({"cp", "float", "api", "set", "gecode_presolver", "__internal__"});
34 sc.stdFlags({"-a", "-n"});
35 SolverConfigs::registerBuiltinSolver(sc);
36}
37
38SolverInstanceBase::Options* Gecode_SolverFactory::createOptions(void) { return new GecodeOptions; }
39
40SolverInstanceBase* Gecode_SolverFactory::doCreateSI(std::ostream& log,
41 SolverInstanceBase::Options* opt) {
42 return new GecodeSolverInstance(log, opt);
43}
44
45string Gecode_SolverFactory::getDescription(SolverInstanceBase::Options*) {
46 string v = "Gecode solver plugin, compiled " __DATE__ ", using: Gecode version " +
47 string(GECODE_VERSION);
48 return v;
49}
50
51string Gecode_SolverFactory::getVersion(SolverInstanceBase::Options*) {
52 return string(GECODE_VERSION);
53}
54
55bool Gecode_SolverFactory::processOption(SolverInstanceBase::Options* opt, int& i,
56 std::vector<std::string>& argv) {
57 GecodeOptions& _opt = static_cast<GecodeOptions&>(*opt);
58 if (string(argv[i]) == "--allow-unbounded-vars") {
59 _opt.allow_unbounded_vars = true;
60 } else if (string(argv[i]) == "--only-range-domains") {
61 _opt.only_range_domains = true;
62 } else if (string(argv[i]) == "--sac") {
63 _opt.sac = true;
64 } else if (string(argv[i]) == "--shave") {
65 _opt.shave = true;
66 } else if (string(argv[i]) == "--pre-passes") {
67 if (++i == argv.size()) return false;
68 int passes = atoi(argv[i].c_str());
69 if (passes >= 0) _opt.pre_passes = passes;
70 } else if (string(argv[i]) == "-a" || string(argv[i]) == "--all-solutions") {
71 _opt.all_solutions = true;
72 } else if (string(argv[i]) == "-n") {
73 if (++i == argv.size()) return false;
74 int n = atoi(argv[i].c_str());
75 if (n >= 0) _opt.n_solutions = n;
76 } else if (string(argv[i]) == "--node") {
77 if (++i == argv.size()) return false;
78 int nodes = atoi(argv[i].c_str());
79 if (nodes >= 0) _opt.nodes = nodes;
80 } else if (string(argv[i]) == "--fail") {
81 if (++i == argv.size()) return false;
82 int fails = atoi(argv[i].c_str());
83 if (fails >= 0) _opt.fails = fails;
84 } else if (argv[i] == "--solver-time-limit" || argv[i] == "-t") {
85 if (++i == argv.size()) return false;
86 int time = atoi(argv[i].c_str());
87 if (time >= 0) _opt.time = time;
88 } else if (string(argv[i]) == "-v" || string(argv[i]) == "--verbose-solving") {
89 _opt.verbose = true;
90 } else if (string(argv[i]) == "-s" || string(argv[i]) == "--solver-statistics") {
91 _opt.statistics = true;
92 } else {
93 return false;
94 }
95 return true;
96}
97
98void Gecode_SolverFactory::printHelp(ostream& os) {
99 os << "Gecode solver plugin options:" << std::endl
100 << " --allow-unbounded-vars" << std::endl
101 << " give unbounded variables maximum bounds (this may lead to incorrect behaviour)"
102 << std::endl
103 << " --only-range-domains" << std::endl
104 << " only tighten bounds" << std::endl
105 << " --sac" << std ::endl
106 << " singleton arc consistency" << std::endl
107 << " --shave" << std::endl
108 << " shave domains" << std::endl
109 << " --pre-passes <n>" << std::endl
110 << " n passes of sac/shaving, 0 for fixed point" << std::endl
111 << " --node <n>" << std::endl
112 << " node cutoff (0 = none, solution mode)" << std::endl
113 << " --fail <f>" << std::endl
114 << " failure cutoff (0 = none, solution mode)" << std::endl
115 << " --time <ms>" << std::endl
116 << " time (in ms) cutoff (0 = none, solution mode)" << std::endl
117 << " -a, --all-solutions" << std::endl
118 << " print intermediate solutions" << std::endl
119 << " -n <sols>" << std::endl
120 << " number of solutions" << std::endl
121 << std::endl;
122}
123
124class GecodeEngine {
125public:
126 virtual FznSpace* next(void) = 0;
127 virtual bool stopped(void) = 0;
128 virtual ~GecodeEngine(void) {}
129 virtual Gecode::Search::Statistics statistics(void) = 0;
130};
131
132template <template <class> class Engine, template <class, template <class> class> class Meta>
133class MetaEngine : public GecodeEngine {
134 Meta<FznSpace, Engine> e;
135
136public:
137 MetaEngine(FznSpace* s, Search::Options& o) : e(s, o) {}
138 virtual FznSpace* next(void) { return e.next(); }
139 virtual bool stopped(void) { return e.stopped(); }
140 virtual Gecode::Search::Statistics statistics(void) { return e.statistics(); }
141};
142
143GecodeSolverInstance::GecodeSolverInstance(std::ostream& log, SolverInstanceBase::Options* opt)
144 : SolverInstanceImpl<GecodeSolver>(log, opt),
145 _n_found_solutions(0),
146 _current_space(new FznSpace()),
147 _solution(NULL),
148 engine(NULL) {
149 registerConstraints();
150 _current_space->_solveType = MiniZinc::SolveI::SolveType::ST_SAT;
151 // _flat = env.flat();
152}
153
154GecodeSolverInstance::~GecodeSolverInstance(void) {
155 delete engine;
156 // delete _current_space;
157 // delete _solution; // TODO: is this necessary?
158}
159
160void GecodeSolverInstance::registerConstraint(std::string name, poster p) {
161 std::stringstream ss;
162 ss << "gecode_" << name;
163 _constraintRegistry.add(ss.str(), p);
164 std::stringstream ss2;
165 ss2 << "fzn_" << name;
166 _constraintRegistry.add(ss2.str(), p);
167 // TODO: DO NOT USE global names directly
168 _constraintRegistry.add(name, p);
169}
170
171void GecodeSolverInstance::registerConstraints(void) {
172 GCLock lock;
173 registerConstraint("all_different_int", GecodeConstraints::p_distinct);
174 registerConstraint("all_different_offset", GecodeConstraints::p_distinctOffset);
175 registerConstraint("all_equal_int", GecodeConstraints::p_all_equal);
176 registerConstraint("int_eq", GecodeConstraints::p_int_eq);
177 registerConstraint("int_ne", GecodeConstraints::p_int_ne);
178 registerConstraint("int_ge", GecodeConstraints::p_int_ge);
179 registerConstraint("int_gt", GecodeConstraints::p_int_gt);
180 registerConstraint("int_le", GecodeConstraints::p_int_le);
181 registerConstraint("int_lt", GecodeConstraints::p_int_lt);
182 registerConstraint("int_eq_reif", GecodeConstraints::p_int_eq_reif);
183 registerConstraint("int_ne_reif", GecodeConstraints::p_int_ne_reif);
184 registerConstraint("int_ge_reif", GecodeConstraints::p_int_ge_reif);
185 registerConstraint("int_gt_reif", GecodeConstraints::p_int_gt_reif);
186 registerConstraint("int_le_reif", GecodeConstraints::p_int_le_reif);
187 registerConstraint("int_lt_reif", GecodeConstraints::p_int_lt_reif);
188 registerConstraint("int_eq_imp", GecodeConstraints::p_int_eq_imp);
189 registerConstraint("int_ne_imp", GecodeConstraints::p_int_ne_imp);
190 registerConstraint("int_ge_imp", GecodeConstraints::p_int_ge_imp);
191 registerConstraint("int_gt_imp", GecodeConstraints::p_int_gt_imp);
192 registerConstraint("int_le_imp", GecodeConstraints::p_int_le_imp);
193 registerConstraint("int_lt_imp", GecodeConstraints::p_int_lt_imp);
194 registerConstraint("int_lin_eq", GecodeConstraints::p_int_lin_eq);
195 registerConstraint("int_lin_eq_reif", GecodeConstraints::p_int_lin_eq_reif);
196 registerConstraint("int_lin_eq_imp", GecodeConstraints::p_int_lin_eq_imp);
197 registerConstraint("int_lin_le", GecodeConstraints::p_int_lin_le);
198 registerConstraint("int_lin_le_reif", GecodeConstraints::p_int_lin_le_reif);
199 registerConstraint("int_lin_le_imp", GecodeConstraints::p_int_lin_le_imp);
200 registerConstraint("int_lin_lt", GecodeConstraints::p_int_lin_lt);
201 registerConstraint("int_lin_lt_reif", GecodeConstraints::p_int_lin_lt_reif);
202 registerConstraint("int_lin_lt_imp", GecodeConstraints::p_int_lin_lt_imp);
203 registerConstraint("int_lin_ge", GecodeConstraints::p_int_lin_ge);
204 registerConstraint("int_lin_ge_reif", GecodeConstraints::p_int_lin_ge_reif);
205 registerConstraint("int_lin_ge_imp", GecodeConstraints::p_int_lin_ge_imp);
206 registerConstraint("int_lin_gt", GecodeConstraints::p_int_lin_gt);
207 registerConstraint("int_lin_gt_reif", GecodeConstraints::p_int_lin_gt_reif);
208 registerConstraint("int_lin_gt_imp", GecodeConstraints::p_int_lin_gt_imp);
209 // registerConstraint("int_plus", GecodeConstraints::p_int_plus);
210 registerConstraint("int_sum", GecodeConstraints::p_int_sum);
211 // registerConstraint("int_minus", GecodeConstraints::p_int_minus);
212 registerConstraint("int_times", GecodeConstraints::p_int_times);
213 registerConstraint("int_div", GecodeConstraints::p_int_div);
214 registerConstraint("int_mod", GecodeConstraints::p_int_mod);
215 registerConstraint("int_min", GecodeConstraints::p_int_min);
216 registerConstraint("int_max", GecodeConstraints::p_int_max);
217 registerConstraint("int_abs", GecodeConstraints::p_abs);
218 registerConstraint("int_negate", GecodeConstraints::p_int_negate);
219 registerConstraint("bool_eq", GecodeConstraints::p_bool_eq);
220 registerConstraint("bool_eq_reif", GecodeConstraints::p_bool_eq_reif);
221 registerConstraint("bool_eq_imp", GecodeConstraints::p_bool_eq_imp);
222 registerConstraint("bool_not", GecodeConstraints::p_bool_ne);
223 registerConstraint("bool_ne", GecodeConstraints::p_bool_ne);
224 registerConstraint("bool_ne_reif", GecodeConstraints::p_bool_ne_reif);
225 registerConstraint("bool_ne_imp", GecodeConstraints::p_bool_ne_imp);
226 registerConstraint("bool_ge", GecodeConstraints::p_bool_ge);
227 registerConstraint("bool_ge_reif", GecodeConstraints::p_bool_ge_reif);
228 registerConstraint("bool_ge_imp", GecodeConstraints::p_bool_ge_imp);
229 registerConstraint("bool_le", GecodeConstraints::p_bool_le);
230 registerConstraint("bool_le_reif", GecodeConstraints::p_bool_le_reif);
231 registerConstraint("bool_le_imp", GecodeConstraints::p_bool_le_imp);
232 registerConstraint("bool_gt", GecodeConstraints::p_bool_gt);
233 registerConstraint("bool_gt_reif", GecodeConstraints::p_bool_gt_reif);
234 registerConstraint("bool_gt_imp", GecodeConstraints::p_bool_gt_imp);
235 registerConstraint("bool_lt", GecodeConstraints::p_bool_lt);
236 registerConstraint("bool_lt_reif", GecodeConstraints::p_bool_lt_reif);
237 registerConstraint("bool_lt_imp", GecodeConstraints::p_bool_lt_imp);
238 registerConstraint("bool_or", GecodeConstraints::p_bool_or);
239 registerConstraint("bool_or_imp", GecodeConstraints::p_bool_or_imp);
240 registerConstraint("bool_and", GecodeConstraints::p_bool_and);
241 registerConstraint("forall", GecodeConstraints::p_forall);
242 registerConstraint("bool_and_imp", GecodeConstraints::p_bool_and_imp);
243 registerConstraint("bool_xor", GecodeConstraints::p_bool_xor);
244 registerConstraint("bool_xor_imp", GecodeConstraints::p_bool_xor_imp);
245 registerConstraint("array_bool_and", GecodeConstraints::p_array_bool_and);
246 registerConstraint("array_bool_and_imp", GecodeConstraints::p_array_bool_and_imp);
247 registerConstraint("array_bool_or", GecodeConstraints::p_array_bool_or);
248 // registerConstraint("exists", GecodeConstraints::p_exists);
249 registerConstraint("array_bool_or_imp", GecodeConstraints::p_array_bool_or_imp);
250 registerConstraint("array_bool_xor", GecodeConstraints::p_array_bool_xor);
251 registerConstraint("array_bool_xor_imp", GecodeConstraints::p_array_bool_xor_imp);
252 registerConstraint("bool_clause", GecodeConstraints::p_array_bool_clause);
253 registerConstraint("bool_clause_reif", GecodeConstraints::p_array_bool_clause_reif);
254 registerConstraint("bool_clause_imp", GecodeConstraints::p_array_bool_clause_imp);
255 registerConstraint("bool_left_imp", GecodeConstraints::p_bool_l_imp);
256 registerConstraint("bool_right_imp", GecodeConstraints::p_bool_r_imp);
257 // registerConstraint("bool_not", GecodeConstraints::p_bool_not);
258 registerConstraint("array_int_element", GecodeConstraints::p_array_int_element);
259 registerConstraint("array_var_int_element", GecodeConstraints::p_array_int_element);
260 registerConstraint("array_bool_element", GecodeConstraints::p_array_bool_element);
261 registerConstraint("array_var_bool_element", GecodeConstraints::p_array_bool_element);
262 registerConstraint("bool2int", GecodeConstraints::p_bool2int);
263 registerConstraint("int_in", GecodeConstraints::p_int_in);
264 registerConstraint("int_in_reif", GecodeConstraints::p_int_in_reif);
265 registerConstraint("int_in_imp", GecodeConstraints::p_int_in_imp);
266 //#ifndef GECODE_HAS_SET_VARS
267 registerConstraint("set_in", GecodeConstraints::p_int_in);
268 registerConstraint("set_in_reif", GecodeConstraints::p_int_in_reif);
269 registerConstraint("set_in_imp", GecodeConstraints::p_int_in_imp);
270 //#endif
271
272 registerConstraint("array_int_lt", GecodeConstraints::p_array_int_lt);
273 registerConstraint("array_int_lq", GecodeConstraints::p_array_int_lq);
274 registerConstraint("array_bool_lt", GecodeConstraints::p_array_bool_lt);
275 registerConstraint("array_bool_lq", GecodeConstraints::p_array_bool_lq);
276 registerConstraint("count", GecodeConstraints::p_count);
277 registerConstraint("count_reif", GecodeConstraints::p_count_reif);
278 registerConstraint("count_imp", GecodeConstraints::p_count_imp);
279 registerConstraint("at_least_int", GecodeConstraints::p_at_least);
280 registerConstraint("at_most_int", GecodeConstraints::p_at_most);
281 registerConstraint("bin_packing_load", GecodeConstraints::p_bin_packing_load);
282 registerConstraint("global_cardinality", GecodeConstraints::p_global_cardinality);
283 registerConstraint("global_cardinality_closed", GecodeConstraints::p_global_cardinality_closed);
284 registerConstraint("global_cardinality_low_up", GecodeConstraints::p_global_cardinality_low_up);
285 registerConstraint("global_cardinality_low_up_closed",
286 GecodeConstraints::p_global_cardinality_low_up_closed);
287 registerConstraint("array_int_minimum", GecodeConstraints::p_minimum);
288 registerConstraint("array_int_maximum", GecodeConstraints::p_maximum);
289 registerConstraint("minimum_arg_int", GecodeConstraints::p_minimum_arg);
290 registerConstraint("maximum_arg_int", GecodeConstraints::p_maximum_arg);
291 registerConstraint("regular", GecodeConstraints::p_regular);
292 registerConstraint("sort", GecodeConstraints::p_sort);
293 registerConstraint("inverse_offsets", GecodeConstraints::p_inverse_offsets);
294 registerConstraint("increasing_int", GecodeConstraints::p_increasing_int);
295 registerConstraint("increasing_bool", GecodeConstraints::p_increasing_bool);
296 registerConstraint("decreasing_int", GecodeConstraints::p_decreasing_int);
297 registerConstraint("decreasing_bool", GecodeConstraints::p_decreasing_bool);
298 registerConstraint("table_int", GecodeConstraints::p_table_int);
299 registerConstraint("table_bool", GecodeConstraints::p_table_bool);
300 registerConstraint("cumulatives", GecodeConstraints::p_cumulatives);
301 registerConstraint("among_seq_int", GecodeConstraints::p_among_seq_int);
302 registerConstraint("among_seq_bool", GecodeConstraints::p_among_seq_bool);
303
304 registerConstraint("bool_lin_eq", GecodeConstraints::p_bool_lin_eq);
305 registerConstraint("bool_lin_ne", GecodeConstraints::p_bool_lin_ne);
306 registerConstraint("bool_lin_le", GecodeConstraints::p_bool_lin_le);
307 registerConstraint("bool_lin_lt", GecodeConstraints::p_bool_lin_lt);
308 registerConstraint("bool_lin_ge", GecodeConstraints::p_bool_lin_ge);
309 registerConstraint("bool_lin_gt", GecodeConstraints::p_bool_lin_gt);
310
311 registerConstraint("bool_lin_eq_reif", GecodeConstraints::p_bool_lin_eq_reif);
312 registerConstraint("bool_lin_eq_imp", GecodeConstraints::p_bool_lin_eq_imp);
313 registerConstraint("bool_lin_ne_reif", GecodeConstraints::p_bool_lin_ne_reif);
314 registerConstraint("bool_lin_ne_imp", GecodeConstraints::p_bool_lin_ne_imp);
315 registerConstraint("bool_lin_le_reif", GecodeConstraints::p_bool_lin_le_reif);
316 registerConstraint("bool_lin_le_imp", GecodeConstraints::p_bool_lin_le_imp);
317 registerConstraint("bool_lin_lt_reif", GecodeConstraints::p_bool_lin_lt_reif);
318 registerConstraint("bool_lin_lt_imp", GecodeConstraints::p_bool_lin_lt_imp);
319 registerConstraint("bool_lin_ge_reif", GecodeConstraints::p_bool_lin_ge_reif);
320 registerConstraint("bool_lin_ge_imp", GecodeConstraints::p_bool_lin_ge_imp);
321 registerConstraint("bool_lin_gt_reif", GecodeConstraints::p_bool_lin_gt_reif);
322 registerConstraint("bool_lin_gt_imp", GecodeConstraints::p_bool_lin_gt_imp);
323
324 registerConstraint("schedule_unary", GecodeConstraints::p_schedule_unary);
325 registerConstraint("schedule_unary_optional", GecodeConstraints::p_schedule_unary_optional);
326 registerConstraint("schedule_cumulative_optional", GecodeConstraints::p_cumulative_opt);
327
328 registerConstraint("circuit", GecodeConstraints::p_circuit);
329 registerConstraint("circuit_cost_array", GecodeConstraints::p_circuit_cost_array);
330 registerConstraint("circuit_cost", GecodeConstraints::p_circuit_cost);
331 registerConstraint("nooverlap", GecodeConstraints::p_nooverlap);
332 registerConstraint("precede", GecodeConstraints::p_precede);
333 registerConstraint("nvalue", GecodeConstraints::p_nvalue);
334 registerConstraint("among", GecodeConstraints::p_among);
335 registerConstraint("member_int", GecodeConstraints::p_member_int);
336 registerConstraint("member_int_reif", GecodeConstraints::p_member_int_reif);
337 registerConstraint("member_bool", GecodeConstraints::p_member_bool);
338 registerConstraint("member_bool_reif", GecodeConstraints::p_member_bool_reif);
339
340#ifdef GECODE_HAS_FLOAT_VARS
341 registerConstraint("int2float", GecodeConstraints::p_int2float);
342 registerConstraint("float_abs", GecodeConstraints::p_float_abs);
343 registerConstraint("float_sqrt", GecodeConstraints::p_float_sqrt);
344 registerConstraint("float_eq", GecodeConstraints::p_float_eq);
345 registerConstraint("float_eq_reif", GecodeConstraints::p_float_eq_reif);
346 registerConstraint("float_le", GecodeConstraints::p_float_le);
347 registerConstraint("float_le_reif", GecodeConstraints::p_float_le_reif);
348 registerConstraint("float_lt", GecodeConstraints::p_float_lt);
349 registerConstraint("float_lt_reif", GecodeConstraints::p_float_lt_reif);
350 registerConstraint("float_ne", GecodeConstraints::p_float_ne);
351 registerConstraint("float_times", GecodeConstraints::p_float_times);
352 registerConstraint("float_div", GecodeConstraints::p_float_div);
353 registerConstraint("float_plus", GecodeConstraints::p_float_plus);
354 registerConstraint("float_max", GecodeConstraints::p_float_max);
355 registerConstraint("float_min", GecodeConstraints::p_float_min);
356 registerConstraint("float_lin_eq", GecodeConstraints::p_float_lin_eq);
357 registerConstraint("float_lin_eq_reif", GecodeConstraints::p_float_lin_eq_reif);
358 registerConstraint("float_lin_le", GecodeConstraints::p_float_lin_le);
359 registerConstraint("float_lin_le_reif", GecodeConstraints::p_float_lin_le_reif);
360#endif
361#ifdef GECODE_HAS_MPFR
362 registerConstraint("float_acos", GecodeConstraints::p_float_acos);
363 registerConstraint("float_asin", GecodeConstraints::p_float_asin);
364 registerConstraint("float_atan", GecodeConstraints::p_float_atan);
365 registerConstraint("float_cos", GecodeConstraints::p_float_cos);
366 registerConstraint("float_exp", GecodeConstraints::p_float_exp);
367 registerConstraint("float_ln", GecodeConstraints::p_float_ln);
368 registerConstraint("float_log10", GecodeConstraints::p_float_log10);
369 registerConstraint("float_log2", GecodeConstraints::p_float_log2);
370 registerConstraint("float_sin", GecodeConstraints::p_float_sin);
371 registerConstraint("float_tan", GecodeConstraints::p_float_tan);
372#endif
373#ifdef GECODE_HAS_SET_VARS
374 registerConstraint("set_eq", GecodeConstraints::p_set_eq);
375 registerConstraint("set_le", GecodeConstraints::p_set_le);
376 registerConstraint("set_lt", GecodeConstraints::p_set_lt);
377 registerConstraint("equal", GecodeConstraints::p_set_eq);
378 registerConstraint("set_ne", GecodeConstraints::p_set_ne);
379 registerConstraint("set_union", GecodeConstraints::p_set_union);
380 registerConstraint("array_set_element", GecodeConstraints::p_array_set_element);
381 registerConstraint("array_var_set_element", GecodeConstraints::p_array_set_element);
382 registerConstraint("set_intersect", GecodeConstraints::p_set_intersect);
383 registerConstraint("set_diff", GecodeConstraints::p_set_diff);
384 registerConstraint("set_symdiff", GecodeConstraints::p_set_symdiff);
385 registerConstraint("set_subset", GecodeConstraints::p_set_subset);
386 registerConstraint("set_superset", GecodeConstraints::p_set_superset);
387 registerConstraint("set_card", GecodeConstraints::p_set_card);
388 registerConstraint("set_in", GecodeConstraints::p_set_in);
389 registerConstraint("set_eq_reif", GecodeConstraints::p_set_eq_reif);
390 registerConstraint("set_le_reif", GecodeConstraints::p_set_le_reif);
391 registerConstraint("set_lt_reif", GecodeConstraints::p_set_lt_reif);
392 registerConstraint("equal_reif", GecodeConstraints::p_set_eq_reif);
393 registerConstraint("set_ne_reif", GecodeConstraints::p_set_ne_reif);
394 registerConstraint("set_subset_reif", GecodeConstraints::p_set_subset_reif);
395 registerConstraint("set_superset_reif", GecodeConstraints::p_set_superset_reif);
396 registerConstraint("set_in_reif", GecodeConstraints::p_set_in_reif);
397 registerConstraint("set_in_imp", GecodeConstraints::p_set_in_imp);
398 registerConstraint("disjoint", GecodeConstraints::p_set_disjoint);
399 registerConstraint("link_set_to_booleans", GecodeConstraints::p_link_set_to_booleans);
400 registerConstraint("array_set_union", GecodeConstraints::p_array_set_union);
401 registerConstraint("array_set_partition", GecodeConstraints::p_array_set_partition);
402 registerConstraint("set_convex", GecodeConstraints::p_set_convex);
403 registerConstraint("array_set_seq", GecodeConstraints::p_array_set_seq);
404 registerConstraint("array_set_seq_union", GecodeConstraints::p_array_set_seq_union);
405 registerConstraint("array_set_element_union", GecodeConstraints::p_array_set_element_union);
406 registerConstraint("array_set_element_intersect",
407 GecodeConstraints::p_array_set_element_intersect);
408 registerConstraint("array_set_element_intersect_in",
409 GecodeConstraints::p_array_set_element_intersect_in);
410 registerConstraint("array_set_element_partition",
411 GecodeConstraints::p_array_set_element_partition);
412 registerConstraint("int_set_channel", GecodeConstraints::p_int_set_channel);
413 registerConstraint("range", GecodeConstraints::p_range);
414 registerConstraint("set_weights", GecodeConstraints::p_weights);
415 registerConstraint("inverse_set", GecodeConstraints::p_inverse_set);
416 registerConstraint("precede_set", GecodeConstraints::p_precede_set);
417#endif
418}
419
420inline bool GecodeSolverInstance::valueWithinBounds(double b) {
421 long long int bo = round_to_longlong(b);
422 return bo >= Gecode::Int::Limits::min && bo <= Gecode::Int::Limits::max;
423}
424
425void GecodeSolverInstance::addConstraint(const std::vector<BytecodeProc>& bs, Constraint* c) {
426 const std::string& name = bs[c->pred()].name;
427
428 if (name == "solve_this") {
429 IntVal solve_mode = c->arg(0).toIntVal();
430 Val obj = c->arg(1);
431 SolveI* si;
432 if (solve_mode != 1) {
433 _current_space->_optVarIsInt = true;
434 _current_space->_solveType = solve_mode == 1 ? MiniZinc::SolveI::SolveType::ST_MIN
435 : MiniZinc::SolveI::SolveType::ST_MAX;
436 GecodeVariable var = resolveVar(obj.toVar());
437 IntVar intVar = var.intVar(_current_space);
438 for (unsigned int i = 0; i < _current_space->iv.size(); i++) {
439 if (_current_space->iv[i].varimp() == intVar.varimp()) {
440 _current_space->_optVarIdx = i;
441 break;
442 }
443 }
444 GCLock lock;
445 solveExpr = new Id(Location().introduce(), obj.timestamp(), nullptr);
446 }
447 // TODO: Use correct search heuristic
448 /* if (c->size() == 5) {
449 Val search_a = c->arg(2);
450 IntVal var_sel = c->arg(3).toIntVal();
451 IntVal val_sel = c->arg(4).toIntVal();
452 if (search_a.isVec() && search_a.size() > 0 && var_sel > 0 && val_sel > 0) {
453 Expression* search_vars = val_to_expr(Type::varint(1), search_a);
454 ASTString var_sel_s(var_sel == 1 ? "input_order" : "first_fail");
455 ASTString val_sel_s(val_sel == 1 ? "indomain_min" : "indomain_max");
456 Id* var_sel_id = new Id(Location().introduce(), var_sel_s, nullptr);
457 Id* val_sel_id = new Id(Location().introduce(), val_sel_s, nullptr);
458 Id* complete_id = new Id(Location().introduce(), "complete", nullptr);
459 si->ann().add(new Call(Location().introduce(), ASTString("int_search"),
460 {search_vars, var_sel_id, val_sel_id, complete_id}));
461 } */
462 return;
463 }
464 _constraintRegistry.post(name, c);
465}
466void GecodeSolverInstance::addVariable(Variable* var, bool isOutput) {
467 GecodeConstraints::p_mk_intvar(*this, var, isOutput);
468}
469
470void GecodeSolverInstance::processFlatZinc(void) {
471 return;
472 assert(false);
473 // GecodeOptions& _opt = static_cast<GecodeOptions&>(*_options);
474 // _only_range_domains = _opt.only_range_domains;
475 // _run_sac = _opt.sac;
476 // _run_shave = _opt.shave;
477 // _pre_passes = _opt.pre_passes;
478 // _print_stats = _opt.statistics;
479 // _all_solutions = _opt.all_solutions;
480 // _n_max_solutions = _opt.n_solutions;
481 // _allow_unbounded_vars = _opt.allow_unbounded_vars;
482 // _current_space = new FznSpace();
483
484 // // iterate over VarDecls of the flat model and create variables
485 // for (VarDeclIterator it = _flat->begin_vardecls(); it != _flat->end_vardecls(); ++it) {
486 // if (!it->removed() && it->e()->type().isvar()) {
487 // // check if it has an output-annotation
488 // VarDecl* vd = it->e();
489 // if(!vd->ann().isEmpty()) {
490 // if(vd->ann().containsCall(constants().ann.output_array.aststr())) {
491 // ArrayLit* al = vd->e()->dyn_cast<ArrayLit>();
492 // if(!al) {
493 // std::stringstream ssm;
494 // ssm << "GecodeSolverInstance::processFlatZinc: Error: Array without right hand
495 // side: " << *vd->id() << std::endl; throw InternalError(ssm.str());
496 // }
497 // for(int i=0; i<al->size(); i++) {
498 // if(Id* id = (*al)[i]->dyn_cast<Id>()) {
499 // GecodeVariable var = resolveVar(id);
500 // if(var.isint()) {
501 // _current_space->iv_introduced[var.index()] = false;
502 // } else if(var.isbool()) {
503 // _current_space->bv_introduced[var.index()] = false;
504 // } else if(var.isfloat()) {
505 // _current_space->fv_introduced[var.index()] = false;
506 // } else if(var.isset()) {
507 // _current_space->sv_introduced[var.index()] = false;
508 // }
509 // }
510 // }
511 // _varsWithOutput.push_back(vd);
512 // } else if (vd->ann().contains(constants().ann.output_var)) {
513 // _varsWithOutput.push_back(vd);
514 // }
515 // }
516
517 // if (it->e()->type().dim() != 0) {
518 // // we ignore arrays - all their elements are defined
519 // continue;
520 // }
521 // MiniZinc::TypeInst* ti = it->e()->ti();
522 // bool isDefined, isIntroduced = false;
523
524 // if(vd->type().isint()) {
525 // if(!it->e()->e()) { // if there is no initialisation expression
526 // Expression* domain = ti->domain();
527 // if(domain) {
528 // IntVar intVar(*this->_current_space, arg2intset(_env.envi(), domain));
529 // _current_space->iv.push_back(intVar);
530 // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::INT_TYPE,
531 // _current_space->iv.size()-1));
532 // } else {
533 // if(_allow_unbounded_vars) {
534 // IntVar intVar(*this->_current_space, Gecode::Int::Limits::min,
535 // Gecode::Int::Limits::max); _current_space->iv.push_back(intVar);
536 // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::INT_TYPE,
537 // _current_space->iv.size()-1)); std::cerr << "%
538 // GecodeSolverInstance::processFlatZinc: Warning: Unbounded variable " <<
539 // *vd->id() << " given maximum integer bounds, this may be incorrect: " <<
540 // std::endl;
541 // } else {
542 // std::stringstream ssm;
543 // ssm << "GecodeSolverInstance::processFlatZinc: Error: Unbounded variable: "
544 // << *vd->id() << ", rerun with --allow-unbounded-vars to add arbitrary
545 // bounds."<< std::endl; throw InternalError(ssm.str());
546 // }
547 // }
548 // } else { // there is an initialisation expression
549 // Expression* init = it->e()->e();
550 // if (init->isa<Id>() || init->isa<ArrayAccess>()) {
551 // // root->iv[root->intVarCount++] = root->iv[*(int*)resolveVar(init)];
552 // GecodeVariable var = resolveVar(init);
553 // assert(var.isint());
554 // _current_space->iv.push_back(var.intVar(_current_space));
555 // insertVar(it->e()->id(), var);
556 // } else {
557 // double il = init->cast<IntLit>()->v().toInt();
558 // if(valueWithinBounds(il)) {
559 // IntVar intVar(*this->_current_space, il, il);
560 // _current_space->iv.push_back(intVar);
561 // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::INT_TYPE,
562 // _current_space->iv.size()-1));
563 // } else {
564 // std::stringstream ssm;
565 // ssm << "GecodeSolverInstance::processFlatZinc: Error: Unsafe value for
566 // Gecode: " << il << std::endl; throw InternalError(ssm.str());
567 // }
568 // }
569 // }
570 // isIntroduced = it->e()->introduced() || (MiniZinc::getAnnotation(it->e()->ann(),
571 // constants().ann.is_introduced.str()) != NULL);
572 // _current_space->iv_introduced.push_back(isIntroduced);
573 // isDefined = MiniZinc::getAnnotation(it->e()->ann(),
574 // constants().ann.is_defined_var->str().str()) != NULL;
575 // _current_space->iv_defined.push_back(isDefined);
576
577 // } else if(vd->type().isbool()) {
578 // double lb=0, ub=1;
579 // if(!it->e()->e()) { // there is NO initialisation expression
580 // Expression* domain = ti->domain();
581 // if(domain) {
582 // IntBounds ib = compute_int_bounds(_env.envi(), domain);
583 // lb = ib.l.toInt();
584 // ub = ib.u.toInt();
585 // } else {
586 // lb = 0;
587 // ub = 1;
588 // }
589 // BoolVar boolVar(*this->_current_space, lb, ub);
590 // _current_space->bv.push_back(boolVar);
591 // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::BOOL_TYPE,
592 // _current_space->bv.size()-1));
593 // } else { // there is an initialisation expression
594 // Expression* init = it->e()->e();
595 // if (init->isa<Id>() || init->isa<ArrayAccess>()) {
596 // // root->bv[root->boolVarCount++] = root->bv[*(int*)resolveVar(init)];
597 // //int index = *(int*) resolveVar(init);
598 // GecodeVariable var = resolveVar(init);
599 // assert(var.isbool());
600 // _current_space->bv.push_back(var.boolVar(_current_space));
601 // insertVar(it->e()->id(), var);
602 // } else {
603 // double b = (double) init->cast<BoolLit>()->v();
604 // BoolVar boolVar(*this->_current_space, b, b);
605 // _current_space->bv.push_back(boolVar);
606 // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::BOOL_TYPE,
607 // _current_space->bv.size()-1));
608 // }
609 // }
610 // isIntroduced = it->e()->introduced() || (MiniZinc::getAnnotation(it->e()->ann(),
611 // constants().ann.is_introduced.str()) != NULL);
612 // _current_space->bv_introduced.push_back(isIntroduced);
613 // isDefined = MiniZinc::getAnnotation(it->e()->ann(),
614 // constants().ann.is_defined_var->str().str()) != NULL;
615 // _current_space->bv_defined.push_back(isDefined);
616 // #ifdef GECODE_HAS_FLOAT_VARS
617 // } else if(vd->type().isfloat()) {
618 // if(it->e()->e() == NULL) { // there is NO initialisation expression
619 // Expression* domain = ti->domain();
620 // double lb, ub;
621 // if (domain) {
622 // FloatBounds fb = compute_float_bounds(_env.envi(), vd->id());
623 // lb = fb.l.toDouble();
624 // ub = fb.u.toDouble();
625 // } else {
626 // if(_allow_unbounded_vars) {
627 // lb = Gecode::Float::Limits::min;
628 // ub = Gecode::Float::Limits::max;
629 // std::cerr << "%% GecodeSolverInstance::processFlatZinc: Warning: Unbounded
630 // variable " << *vd->id() << " given maximum float bounds, this may be
631 // incorrect: " << std::endl;
632 // } else {
633 // std::stringstream ssm;
634 // ssm << "GecodeSolverInstance::processFlatZinc: Error: Unbounded variable: "
635 // << *vd->id() << ", rerun with --allow-unbounded-vars to add arbitrary
636 // bounds."<< std::endl; throw InternalError(ssm.str());
637 // }
638 // }
639 // FloatVar floatVar(*this->_current_space, lb, ub);
640 // _current_space->fv.push_back(floatVar);
641 // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::FLOAT_TYPE,
642 // _current_space->fv.size()-1));
643 // } else {
644 // Expression* init = it->e()->e();
645 // if (init->isa<Id>() || init->isa<ArrayAccess>()) {
646 // // root->fv[root->floatVarCount++] = root->fv[*(int*)resolveVar(init)];
647 // GecodeVariable var = resolveVar(init);
648 // assert(var.isfloat());
649 // _current_space->fv.push_back(var.floatVar(_current_space));
650 // insertVar(it->e()->id(), var);
651 // } else {
652 // double il = init->cast<FloatLit>()->v().toDouble();
653 // FloatVar floatVar(*this->_current_space, il, il);
654 // _current_space->fv.push_back(floatVar);
655 // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::FLOAT_TYPE,
656 // _current_space->fv.size()-1));
657 // }
658 // }
659 // isIntroduced = it->e()->introduced() || (MiniZinc::getAnnotation(it->e()->ann(),
660 // constants().ann.is_introduced.str()) != NULL);
661 // _current_space->fv_introduced.push_back(isIntroduced);
662 // isDefined = MiniZinc::getAnnotation(it->e()->ann(),
663 // constants().ann.is_defined_var->str().str()) != NULL;
664 // _current_space->fv_defined.push_back(isDefined);
665 // #endif
666 // #ifdef GECODE_HAS_SET_VARS
667 // } else if(vd->type().isintset()) {
668 // Expression* domain = ti->domain();
669 // auto d = arg2intset(_env.envi(), domain);
670 // SetVar setVar(*this->_current_space, Gecode::IntSet::empty, d);
671 // _current_space->sv.push_back(setVar);
672 // isIntroduced = it->e()->introduced() || (MiniZinc::getAnnotation(it->e()->ann(),
673 // constants().ann.is_introduced.str()) != NULL);
674 // _current_space->sv_introduced.push_back(isIntroduced);
675 // isDefined = MiniZinc::getAnnotation(it->e()->ann(),
676 // constants().ann.is_defined_var->str().str()) != NULL;
677 // _current_space->sv_defined.push_back(isDefined);
678 // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::SET_TYPE,
679 // _current_space->sv.size()-1));
680 // #endif
681 // } else {
682 // std::stringstream ssm;
683 // ssm << "Type " << *ti << " is currently not supported by Gecode." << std::endl;
684 // throw InternalError(ssm.str());
685 // }
686 // } // end if it is a variable
687 // } // end for all var decls
688
689 // // post the constraints
690 // for (ConstraintIterator it = _flat->begin_constraints(); it != _flat->end_constraints();
691 // ++it) {
692 // if(!it->removed()) {
693 // if (Call* c = it->e()->dyn_cast<Call>()) {
694 // // _constraintRegistry.post(c);
695 // }
696 // }
697 // }
698
699 // // objective
700 // SolveI* si = _flat->solveItem();
701 // _current_space->_solveType = si->st();
702 // if(si->e()) {
703 // _current_space->_optVarIsInt = (si->e()->type().isvarint());
704 // if(Id* id = si->e()->dyn_cast<Id>()) {
705 // if (si->e()->type().isvar()) {
706 // GecodeVariable var = resolveVar(id->decl());
707 // if(_current_space->_optVarIsInt) {
708 // IntVar intVar = var.intVar(_current_space);
709 // for(unsigned int i=0; i<_current_space->iv.size(); i++) {
710 // if(_current_space->iv[i].varimp()==intVar.varimp()) {
711 // _current_space->_optVarIdx = i;
712 // break;
713 // }
714 // }
715 // assert(_current_space->_optVarIdx >= 0);
716 // #ifdef GECODE_HAS_FLOAT_VARS
717 // } else {
718 // FloatVar floatVar = var.floatVar(_current_space);
719 // for(unsigned int i=0; i<_current_space->fv.size(); i++) {
720 // if(_current_space->fv[i].varimp()==floatVar.varimp()) {
721 // _current_space->_optVarIdx = i;
722 // break;
723 // }
724 // }
725 // assert(_current_space->_optVarIdx >= 0);
726 // #endif
727 // }
728 // }
729 // }
730 // else { // the solve expression has to be a variable/id
731 // assert(false);
732 // }
733
734 // }
735
736 // //std::cout << "DEBUG: at end of processFlatZinc: " << std::endl
737 // // << "iv has " << _current_space->iv.size() << " variables " << std::endl
738 // // << "bv has " << _current_space->bv.size() << " variables " << std::endl
739 // // << "fv has " << _current_space->fv.size() << " variables " << std::endl
740 // // << "sv has " << _current_space->sv.size() << " variables " << std::endl;
741}
742
743Gecode::IntArgs GecodeSolverInstance::arg2intargs(Expression* arg, int offset) {
744 if (!arg->isa<Id>() && !arg->isa<ArrayLit>()) {
745 std::stringstream ssm;
746 ssm << "Invalid argument in arg2intargs: " << *arg;
747 ssm << ". Expected Id or ArrayLit.";
748 throw InternalError(ssm.str());
749 }
750 ArrayLit* a =
751 arg->isa<Id>() ? arg->cast<Id>()->decl()->e()->cast<ArrayLit>() : arg->cast<ArrayLit>();
752 IntArgs ia(a->size() + offset);
753 for (int i = offset; i--;) ia[i] = 0;
754 for (int i = a->size(); i--;) {
755 ia[i + offset] = (*a)[i]->cast<IntLit>()->v().toInt();
756 }
757 return ia;
758}
759
760Gecode::IntArgs GecodeSolverInstance::arg2intargs(const Val& vec, int offset) {
761 if (!vec.isVec()) {
762 std::stringstream ssm;
763 ssm << "Invalid argument in arg2intargs: " << vec.toString();
764 ssm << ". Expected Array.";
765 throw InternalError(ssm.str());
766 }
767 assert(!vec.toVec()->hasIndexSet());
768 IntArgs ia(vec.size() + offset);
769 for (int i = offset; i--;) ia[i] = 0;
770 for (int i = vec.size(); i--;) {
771 ia[i + offset] = vec[i].toInt();
772 }
773 return ia;
774}
775
776Gecode::IntArgs GecodeSolverInstance::arg2boolargs(Expression* arg, int offset) {
777 if (!arg->isa<Id>() && !arg->isa<ArrayLit>()) {
778 std::stringstream ssm;
779 ssm << "Invalid argument in arg2boolargs: " << *arg;
780 ssm << ". Expected Id or ArrayLit.";
781 throw InternalError(ssm.str());
782 }
783 ArrayLit* a =
784 arg->isa<Id>() ? arg->cast<Id>()->decl()->e()->cast<ArrayLit>() : arg->cast<ArrayLit>();
785 IntArgs ia(a->size() + offset);
786 for (int i = offset; i--;) ia[i] = 0;
787 for (int i = a->size(); i--;) ia[i + offset] = (*a)[i]->cast<BoolLit>()->v();
788 return ia;
789}
790
791Gecode::IntArgs GecodeSolverInstance::arg2boolargs(const Val& vec, int offset) {
792 if (!vec.isVec()) {
793 std::stringstream ssm;
794 ssm << "Invalid argument in arg2intargs: " << vec.toString();
795 ssm << ". Expected Vec.";
796 throw InternalError(ssm.str());
797 }
798 assert(!vec.toVec()->hasIndexSet());
799 IntArgs ia(vec.size() + offset);
800 for (int i = offset; i--;) ia[i] = 0;
801 for (int i = vec.size(); i--;) {
802 ia[i + offset] = vec[i].toInt();
803 }
804 return ia;
805}
806
807class GecodeRangeIter {
808public:
809 GecodeSolverInstance& si;
810 IntSetRanges& isr;
811 GecodeRangeIter(GecodeSolverInstance& gsi, IntSetRanges& isr0) : si(gsi), isr(isr0) {}
812 int min(void) const {
813 long long int val = isr.min().toInt();
814 if (si.valueWithinBounds(val)) {
815 return (int)val;
816 } else {
817 std::stringstream ssm;
818 ssm << "GecodeRangeIter::min: Error: " << val << " outside 32-bit int." << std::endl;
819 throw InternalError(ssm.str());
820 }
821 }
822 int max(void) const {
823 long long int val = isr.max().toInt();
824 if (si.valueWithinBounds(val)) {
825 return (int)val;
826 } else {
827 std::stringstream ssm;
828 ssm << "GecodeRangeIter::max: Error: " << val << " outside 32-bit int." << std::endl;
829 throw InternalError(ssm.str());
830 }
831 }
832 int width(void) const { return isr.width().toInt(); }
833 bool operator()(void) { return isr(); }
834 void operator++(void) { ++isr; }
835};
836
837Gecode::IntSet GecodeSolverInstance::arg2intset(EnvI& envi, Expression* arg) {
838 GCLock lock;
839 IntSetVal* isv = eval_intset(envi, arg);
840 IntSetRanges isr(isv);
841 GecodeRangeIter isr_g(*this, isr);
842 IntSet d(isr_g);
843 return d;
844}
845Gecode::IntSet GecodeSolverInstance::arg2intset(const Val& sl) {
846 GCLock lock;
847 assert(sl.isVec());
848 assert(sl.size() >= 2 && sl.size() % 2 == 0);
849 std::vector<IntSetVal::Range> ranges;
850 for (int i = 0; i < sl.size(); i += 2) {
851 ranges.emplace_back(sl[i].toIntVal(), sl[i + 1].toIntVal());
852 }
853 IntSetVal* isv = IntSetVal::a(ranges);
854 IntSetRanges isr(isv);
855 GecodeRangeIter isr_g(*this, isr);
856 IntSet d(isr_g);
857 return d;
858}
859IntSetArgs GecodeSolverInstance::arg2intsetargs(EnvI& envi, Expression* arg, int offset) {
860 ArrayLit* a = arg2arraylit(arg);
861 if (a->size() == 0) {
862 IntSetArgs emptyIa(0);
863 return emptyIa;
864 }
865 IntSetArgs ia(a->size() + offset);
866 for (int i = offset; i--;) ia[i] = IntSet::empty;
867 for (int i = a->size(); i--;) {
868 ia[i + offset] = arg2intset(envi, (*a)[i]);
869 }
870 return ia;
871}
872
873Gecode::IntVarArgs GecodeSolverInstance::arg2intvarargs(const Val& vec, int offset) {
874 assert(!vec.toVec()->hasIndexSet());
875 if (vec.size() == 0) {
876 IntVarArgs emptyIa(0);
877 return emptyIa;
878 }
879 IntVarArgs ia(vec.size() + offset);
880 for (int i = offset; i--;) ia[i] = IntVar(*this->_current_space, 0, 0);
881 for (int i = vec.size(); i--;) {
882 const Val& val = Val::follow_alias(vec[i]);
883 if (val.isVar()) {
884 // ia[i+offset] = _current_space->iv[*(int*)resolveVar(getVarDecl(e))];
885 GecodeSolver::Variable var = resolveVar(val.toVar());
886 if (var.isbool()) {
887 // TODO: We should cache the channeling
888 IntVar intVar(*_current_space, 0, 1);
889 _current_space->iv.push_back(intVar);
890 // insertVar(def, GecodeVariable(GecodeVariable::INT_TYPE,
891 // _current_space->iv.size()-1));
892 _current_space->iv_introduced.push_back(true);
893 _current_space->iv_defined.push_back(true);
894 channel(*_current_space, intVar, var.boolVar(_current_space), MZ_ICL_DEF);
895 ia[i + offset] = intVar;
896 } else {
897 assert(var.isint());
898 Gecode::IntVar v = var.intVar(_current_space);
899 ia[i + offset] = v;
900 }
901 } else {
902 long long int value = val.toInt();
903 if (valueWithinBounds(value)) {
904 IntVar iv(*this->_current_space, value, value);
905 ia[i + offset] = iv;
906 } else {
907 std::stringstream ssm;
908 ssm << "GecodeSolverInstance::arg2intvarargs Error: " << value << " outside 32-bit int."
909 << std::endl;
910 throw InternalError(ssm.str());
911 }
912 }
913 }
914 return ia;
915}
916Gecode::IntVarArgs GecodeSolverInstance::arg2intvarargs(Expression* arg, int offset) {
917 ArrayLit* a = arg2arraylit(arg);
918 if (a->size() == 0) {
919 IntVarArgs emptyIa(0);
920 return emptyIa;
921 }
922 IntVarArgs ia(a->size() + offset);
923 for (int i = offset; i--;) ia[i] = IntVar(*this->_current_space, 0, 0);
924 for (int i = a->size(); i--;) {
925 Expression* e = (*a)[i];
926 if (e->type().isvar()) {
927 // ia[i+offset] = _current_space->iv[*(int*)resolveVar(getVarDecl(e))];
928 GecodeSolver::Variable var = resolveVar(getVarDecl(e));
929 assert(var.isint());
930 Gecode::IntVar v = var.intVar(_current_space);
931 ia[i + offset] = v;
932 } else {
933 long long int value = e->cast<IntLit>()->v().toInt();
934 if (valueWithinBounds(value)) {
935 IntVar iv(*this->_current_space, value, value);
936 ia[i + offset] = iv;
937 } else {
938 std::stringstream ssm;
939 ssm << "GecodeSolverInstance::arg2intvarargs Error: " << value << " outside 32-bit int."
940 << std::endl;
941 throw InternalError(ssm.str());
942 }
943 }
944 }
945 return ia;
946}
947
948Gecode::BoolVarArgs GecodeSolverInstance::arg2boolvarargs(const Val& vec, int offset, int siv) {
949 assert(!vec.toVec()->hasIndexSet());
950 if (vec.size() == 0) {
951 BoolVarArgs emptyIa(0);
952 return emptyIa;
953 }
954 BoolVarArgs ia(vec.size() + offset - ((siv < 0 || siv >= vec.size()) ? 0 : 1));
955 for (int i = offset; i--;) ia[i] = BoolVar(*this->_current_space, 0, 0);
956 for (int i = 0; i < static_cast<int>(vec.size()); i++) {
957 if (i == siv) continue;
958 const Val& v = Val::follow_alias(vec[i]);
959 if (v.isVar()) {
960 GecodeVariable var = resolveVar(v.toVar());
961 if (var.isbool()) {
962 // assert(var.isbool());
963 ia[offset++] = var.boolVar(_current_space);
964 } else if (var.hasBoolAlias()) {
965 ia[offset++] = _current_space->bv[var.boolAliasIndex()];
966 } else {
967 std::stringstream ssm;
968 ssm << "expected bool-var or alias int var instead of " << v.toString();
969 throw InternalError(ssm.str());
970 }
971 } else {
972 long long int i = v.toInt();
973 if (i >= 0 && i <= 1) {
974 BoolVar iv(*this->_current_space, i, i);
975 ia[offset++] = iv;
976 } else {
977 std::stringstream ssm;
978 ssm << "Expected bool literal instead of: " << v.toString();
979 throw new InternalError(ssm.str());
980 }
981 }
982 }
983 return ia;
984}
985Gecode::BoolVarArgs GecodeSolverInstance::arg2boolvarargs(Expression* arg, int offset, int siv) {
986 ArrayLit* a = arg2arraylit(arg);
987 if (a->length() == 0) {
988 BoolVarArgs emptyIa(0);
989 return emptyIa;
990 }
991 BoolVarArgs ia(a->length() + offset - (siv == -1 ? 0 : 1));
992 for (int i = offset; i--;) ia[i] = BoolVar(*this->_current_space, 0, 0);
993 for (int i = 0; i < static_cast<int>(a->length()); i++) {
994 if (i == siv) continue;
995 Expression* e = (*a)[i];
996 if (e->type().isvar()) {
997 GecodeVariable var = resolveVar(getVarDecl(e));
998 if (e->type().isvarbool()) {
999 assert(var.isbool());
1000 ia[offset++] = var.boolVar(_current_space);
1001 } else if (e->type().isvarint() && var.hasBoolAlias()) {
1002 ia[offset++] = _current_space->bv[var.boolAliasIndex()];
1003 } else {
1004 std::stringstream ssm;
1005 ssm << "expected bool-var or alias int var instead of " << *e << " with type "
1006 << e->type().toString(env().envi());
1007 throw InternalError(ssm.str());
1008 }
1009 } else {
1010 if (BoolLit* bl = e->dyn_cast<BoolLit>()) {
1011 bool value = bl->v();
1012 BoolVar iv(*this->_current_space, value, value);
1013 ia[offset++] = iv;
1014 } else {
1015 std::stringstream ssm;
1016 ssm << "Expected bool literal instead of: " << *e;
1017 throw new InternalError(ssm.str());
1018 }
1019 }
1020 }
1021 return ia;
1022}
1023
1024Gecode::BoolVar GecodeSolverInstance::reifyVar(const Variable* var) {
1025 BoolVar boolVar(*_current_space, 0, 1);
1026 _current_space->bv.push_back(boolVar);
1027 insertVar(var, GecodeVariable(GecodeVariable::BOOL_TYPE, _current_space->bv.size() - 1));
1028 _current_space->bv_introduced.push_back(true);
1029 _current_space->bv_defined.push_back(true);
1030 return boolVar;
1031}
1032
1033Gecode::BoolVar GecodeSolverInstance::arg2boolvar(const Val& v) {
1034 Val _v = Val::follow_alias(v);
1035 BoolVar x0;
1036 if (_v.isVar()) {
1037 // x0 = _current_space->bv[*(int*)resolveVar(getVarDecl(e))];
1038 GecodeVariable var = resolveVar(_v.toVar());
1039 assert(var.isbool());
1040 x0 = var.boolVar(_current_space);
1041 } else {
1042 long long int i = _v.toInt();
1043 if (i < 0 || i > 1) {
1044 std::stringstream ssm;
1045 ssm << "Expected bool literal instead of: " << _v.toString();
1046 throw new InternalError(ssm.str());
1047 } else {
1048 x0 = BoolVar(*this->_current_space, i, i);
1049 }
1050 }
1051 return x0;
1052}
1053Gecode::BoolVar GecodeSolverInstance::arg2boolvar(Expression* e) {
1054 BoolVar x0;
1055 if (e->type().isvar()) {
1056 // x0 = _current_space->bv[*(int*)resolveVar(getVarDecl(e))];
1057 GecodeVariable var = resolveVar(getVarDecl(e));
1058 assert(var.isbool());
1059 x0 = var.boolVar(_current_space);
1060 } else {
1061 if (BoolLit* bl = e->dyn_cast<BoolLit>()) {
1062 x0 = BoolVar(*this->_current_space, bl->v(), bl->v());
1063 } else {
1064 std::stringstream ssm;
1065 ssm << "Expected bool literal instead of: " << *e;
1066 throw new InternalError(ssm.str());
1067 }
1068 }
1069 return x0;
1070}
1071
1072Gecode::IntVar GecodeSolverInstance::arg2intvar(Expression* e) {
1073 IntVar x0;
1074 if (e->type().isvar()) {
1075 // x0 = _current_space->iv[*(int*)resolveVar(getVarDecl(e))];
1076 GecodeVariable var = resolveVar(getVarDecl(e));
1077 assert(var.isint());
1078 x0 = var.intVar(_current_space);
1079 } else {
1080 IntVal i;
1081 if (IntLit* il = e->dyn_cast<IntLit>())
1082 i = il->v().toInt();
1083 else if (BoolLit* bl = e->dyn_cast<BoolLit>())
1084 i = bl->v();
1085 else {
1086 std::stringstream ssm;
1087 ssm << "Expected bool or int literal instead of: " << *e;
1088 throw InternalError(ssm.str());
1089 }
1090 x0 = IntVar(*this->_current_space, i.toInt(), i.toInt());
1091 }
1092 return x0;
1093}
1094Gecode::IntVar GecodeSolverInstance::arg2intvar(const Val& val) {
1095 IntVar x0;
1096 Val _val = Val::follow_alias(val);
1097 if (_val.isVar()) {
1098 Variable* v = _val.toVar();
1099 // x0 = _current_space->iv[*(int*)resolveVar(getVarDecl(e))];
1100 GecodeVariable var = resolveVar(v);
1101 if (var.isbool()) {
1102 // TODO: We should cache the channeling
1103 IntVar intVar(*_current_space, 0, 1);
1104 _current_space->iv.push_back(intVar);
1105 // insertVar(def, GecodeVariable(GecodeVariable::INT_TYPE,
1106 // _current_space->iv.size()-1));
1107 _current_space->iv_introduced.push_back(true);
1108 _current_space->iv_defined.push_back(true);
1109 channel(*_current_space, intVar, var.boolVar(_current_space), MZ_ICL_DEF);
1110 x0 = intVar;
1111 } else {
1112 assert(var.isint());
1113 x0 = var.intVar(_current_space);
1114 }
1115 } else {
1116 IntVal i = _val.toIntVal();
1117 x0 = IntVar(*this->_current_space, i.toInt(), i.toInt());
1118 }
1119 return x0;
1120}
1121
1122ArrayLit* GecodeSolverInstance::arg2arraylit(Expression* arg) {
1123 ArrayLit* a;
1124 if (Id* id = arg->dyn_cast<Id>()) {
1125 VarDecl* vd = id->decl();
1126 if (vd->e()) {
1127 a = vd->e()->cast<ArrayLit>();
1128 } else {
1129 std::vector<Expression*>* array = arrayMap[vd];
1130 std::vector<Expression*> ids;
1131 for (unsigned int i = 0; i < array->size(); i++)
1132 ids.push_back(((*array)[i])->cast<VarDecl>()->id());
1133 a = new ArrayLit(vd->loc(), ids);
1134 }
1135 } else if (ArrayLit* al = arg->dyn_cast<ArrayLit>()) {
1136 a = al;
1137 } else {
1138 std::stringstream ssm;
1139 ssm << "Invalid argument in arg2arrayLit: " << *arg;
1140 ssm << ". Expected Id or ArrayLit.";
1141 throw new InternalError(ssm.str());
1142 }
1143 return a;
1144}
1145
1146bool GecodeSolverInstance::isBoolArray(const Val& arr, int& singleInt) {
1147 assert(!arr.toVec()->hasIndexSet());
1148 singleInt = -1;
1149 if (arr.size() == 0) return true;
1150 for (int i = arr.size(); i--;) {
1151 const Val& val = Val::follow_alias(arr[i]);
1152 if (val.isInt() && val >= 0 && val <= 1) {
1153 continue;
1154 } else if (val.isVar()) {
1155 if (val.lb() >= Val(int(0)) && val.ub() <= Val(int(1))) {
1156 continue;
1157 }
1158 return false;
1159 // TODO: Check variable domain
1160 // GecodeVariable var = resolveVar(getVarDecl((*a)[i]));
1161 // if (var.hasBoolAlias()) {
1162 // singleInt = var.boolAliasIndex();
1163 // }
1164 // else {
1165 // }
1166 } else {
1167 return false;
1168 }
1169 }
1170 return singleInt == -1 || arr.size() > 1;
1171}
1172bool GecodeSolverInstance::isBoolArray(ArrayLit* a, int& singleInt) {
1173 singleInt = -1;
1174 if (a->length() == 0) return true;
1175 for (int i = a->length(); i--;) {
1176 if ((*a)[i]->type().isbool()) {
1177 continue;
1178 } else if (((*a)[i])->type().isvarint()) {
1179 GecodeVariable var = resolveVar(getVarDecl((*a)[i]));
1180 if (var.hasBoolAlias()) {
1181 if (singleInt != -1) {
1182 return false;
1183 }
1184 singleInt = var.boolAliasIndex();
1185 } else
1186 return false;
1187 } else {
1188 return false;
1189 }
1190 }
1191 return singleInt == -1 || a->length() > 1;
1192}
1193#ifdef GECODE_HAS_SET_VARS
1194SetVar GecodeSolverInstance::arg2setvar(Expression* e) {
1195 SetVar x0;
1196 if (!e->type().isvar()) {
1197 Gecode::IntSet d = arg2intset(_env.envi(), e);
1198 x0 = SetVar(*this->_current_space, d, d);
1199 } else {
1200 GecodeVariable var = resolveVar(getVarDecl(e));
1201 assert(var.isset());
1202 x0 = var.setVar(_current_space);
1203 }
1204 return x0;
1205}
1206Gecode::SetVarArgs GecodeSolverInstance::arg2setvarargs(Expression* arg, int offset, int doffset,
1207 const Gecode::IntSet& od) {
1208 ArrayLit* a = arg2arraylit(arg);
1209 SetVarArgs ia(a->size() + offset);
1210 for (int i = offset; i--;) {
1211 Gecode::IntSet d = i < doffset ? od : Gecode::IntSet::empty;
1212 ia[i] = SetVar(*this->_current_space, d, d);
1213 }
1214 for (int i = a->size(); i--;) {
1215 ia[i + offset] = arg2setvar((*a)[i]);
1216 }
1217 return ia;
1218}
1219#endif
1220#ifdef GECODE_HAS_FLOAT_VARS
1221Gecode::FloatValArgs GecodeSolverInstance::arg2floatargs(Expression* arg, int offset) {
1222 assert(arg->isa<Id>() || arg->isa<ArrayLit>());
1223 ArrayLit* a =
1224 arg->isa<Id>() ? arg->cast<Id>()->decl()->e()->cast<ArrayLit>() : arg->cast<ArrayLit>();
1225 FloatValArgs fa(a->size() + offset);
1226 for (int i = offset; i--;) fa[i] = 0.0;
1227 for (int i = a->size(); i--;) fa[i + offset] = (*a)[i]->cast<FloatLit>()->v().toDouble();
1228 return fa;
1229}
1230
1231Gecode::FloatVar GecodeSolverInstance::arg2floatvar(Expression* e) {
1232 FloatVar x0;
1233 if (e->type().isvar()) {
1234 GecodeVariable var = resolveVar(getVarDecl(e));
1235 assert(var.isfloat());
1236 x0 = var.floatVar(_current_space);
1237 } else {
1238 FloatVal i;
1239 if (IntLit* il = e->dyn_cast<IntLit>())
1240 i = il->v().toInt();
1241 else if (BoolLit* bl = e->dyn_cast<BoolLit>())
1242 i = bl->v();
1243 else if (FloatLit* fl = e->dyn_cast<FloatLit>())
1244 i = fl->v();
1245 else {
1246 std::stringstream ssm;
1247 ssm << "Expected bool, int or float literal instead of: " << *e;
1248 throw InternalError(ssm.str());
1249 }
1250 x0 = FloatVar(*this->_current_space, i.toDouble(), i.toDouble());
1251 }
1252 return x0;
1253}
1254
1255Gecode::FloatVarArgs GecodeSolverInstance::arg2floatvarargs(Expression* arg, int offset) {
1256 ArrayLit* a = arg2arraylit(arg);
1257 if (a->size() == 0) {
1258 FloatVarArgs emptyFa(0);
1259 return emptyFa;
1260 }
1261 FloatVarArgs fa(a->size() + offset);
1262 for (int i = offset; i--;) fa[i] = FloatVar(*this->_current_space, 0.0, 0.0);
1263 for (int i = a->size(); i--;) {
1264 Expression* e = (*a)[i];
1265 if (e->type().isvar()) {
1266 GecodeVariable var = resolveVar(getVarDecl(e));
1267 assert(var.isfloat());
1268 fa[i + offset] = var.floatVar(_current_space);
1269 } else {
1270 if (FloatLit* fl = e->dyn_cast<FloatLit>()) {
1271 double value = fl->v().toDouble();
1272 FloatVar fv(*this->_current_space, value, value);
1273 fa[i + offset] = fv;
1274 } else {
1275 std::stringstream ssm;
1276 ssm << "Expected float literal instead of: " << *e;
1277 throw InternalError(ssm.str());
1278 }
1279 }
1280 }
1281 return fa;
1282}
1283#endif
1284
1285MZ_IntConLevel GecodeSolverInstance::ann2icl(const Annotation& ann) {
1286 if (!ann.isEmpty()) {
1287 if (getAnnotation(ann, "val")) return MZ_ICL_VAL;
1288 if (getAnnotation(ann, "domain")) return MZ_ICL_DOM;
1289 if (getAnnotation(ann, "bounds") || getAnnotation(ann, "boundsR") ||
1290 getAnnotation(ann, "boundsD") || getAnnotation(ann, "boundsZ"))
1291 return MZ_ICL_BND;
1292 }
1293 return MZ_ICL_DEF;
1294}
1295
1296VarDecl* GecodeSolverInstance::getVarDecl(Expression* expr) {
1297 VarDecl* vd = NULL;
1298 if ((vd = expr->dyn_cast<VarDecl>())) {
1299 vd = expr->cast<VarDecl>();
1300 } else if (Id* id = expr->dyn_cast<Id>()) {
1301 vd = id->decl();
1302 } else if (ArrayAccess* aa = expr->dyn_cast<ArrayAccess>()) {
1303 vd = resolveArrayAccess(aa);
1304 } else {
1305 std::stringstream ssm;
1306 ssm << "Can not extract vardecl from " << *expr;
1307 throw new InternalError(ssm.str());
1308 }
1309 return vd;
1310}
1311
1312VarDecl* GecodeSolverInstance::resolveArrayAccess(ArrayAccess* aa) {
1313 VarDecl* vd = aa->v()->cast<Id>()->decl();
1314 int idx = aa->idx()[0]->cast<IntLit>()->v().toInt();
1315 return resolveArrayAccess(vd, idx);
1316}
1317
1318VarDecl* GecodeSolverInstance::resolveArrayAccess(VarDecl* vd, int index) {
1319 std::unordered_map<VarDecl*, std::vector<Expression*>*>::iterator it = arrayMap.find(vd);
1320 if (it != arrayMap.end()) {
1321 std::vector<Expression*>* exprs = it->second;
1322 Expression* expr = (*exprs)[index - 1];
1323 return expr->cast<VarDecl>();
1324 } else {
1325 std::stringstream ssm;
1326 ssm << "Unknown array: " << vd->id();
1327 throw new InternalError(ssm.str());
1328 }
1329}
1330
1331GecodeSolver::Variable GecodeSolverInstance::resolveVar(Expression* e) {
1332 std::stringstream ssm;
1333 ssm << "USING OLD SOLVER INTERFACE THINGS!";
1334 throw InternalError(ssm.str());
1335 // if (Id* id = e->dyn_cast<Id>()) {
1336 // return _variableMap.get(id->decl()->id()); //lookupVar(id->decl());
1337 // } else if (VarDecl* vd = e->dyn_cast<VarDecl>()) {
1338 // return _variableMap.get(vd->id()->decl()->id());
1339 // } else if (ArrayAccess* aa = e->dyn_cast<ArrayAccess>()) {
1340 // return _variableMap.get(resolveArrayAccess(aa)->id()->decl()->id());
1341 // } else {
1342 // std::stringstream ssm;
1343 // ssm << "Expected Id, VarDecl or ArrayAccess instead of \"" << *e << "\"";
1344 // throw InternalError(ssm.str());
1345 // }
1346}
1347
1348GecodeSolver::Variable GecodeSolverInstance::resolveVar(Variable* v) {
1349 int i = _variableMap.size() - 1;
1350 std::unordered_map<int, VarId>::iterator it;
1351 while (i >= 0) {
1352 it = _variableMap[i].find(v->timestamp());
1353 if (it != _variableMap[i].end()) {
1354 break;
1355 }
1356 i--;
1357 }
1358 assert(it != _variableMap[0].end());
1359 return it->second; // lookupVar(id->decl());
1360}
1361
1362SolverInstance::Status GecodeSolverInstance::next(void) {
1363 GCLock lock;
1364 prepareEngine();
1365
1366 _solution = engine->next();
1367
1368 if (_solution) {
1369 assignSolutionToOutput();
1370 return SolverInstance::SAT;
1371 } else if (engine->stopped()) {
1372 return SolverInstance::UNKNOWN;
1373 } else {
1374 return SolverInstance::UNSAT;
1375 }
1376}
1377
1378void GecodeSolverInstance::resetSolver(void) {
1379 assert(false); // TODO: implement
1380}
1381
1382Expression* GecodeSolverInstance::getSolutionValue(Id* id) {
1383 id = id->decl()->id();
1384 if (id->type().isvar()) {
1385 GecodeVariable var = resolveVar(id->decl()->id());
1386#ifdef GECODE_HAS_SET_VARS
1387 if (id->type().is_set()) {
1388 SetVar& sv = var.setVar(_solution);
1389 assert(sv.assigned());
1390 SetVarGlbRanges svr(sv);
1391 assert(svr());
1392
1393 IntVal mi = svr.min();
1394 IntVal ma = svr.max();
1395 ++svr;
1396 vector<IntVal> vals;
1397 if (svr()) {
1398 SetVarGlbValues svv(sv);
1399 IntVal i = svv.val();
1400 vals.push_back(i);
1401 ++svv;
1402 for (; svv(); ++svv) vals.push_back(svv.val());
1403 return new SetLit(Location().introduce(), IntSetVal::a(vals));
1404 } else {
1405 return new SetLit(Location().introduce(), IntSetVal::a(mi, ma));
1406 }
1407 }
1408#endif
1409 switch (id->type().bt()) {
1410 case Type::BT_INT:
1411 assert(var.intVar(_solution).assigned());
1412 return IntLit::a(var.intVar(_solution).val());
1413 case Type::BT_BOOL:
1414 assert(var.boolVar(_solution).assigned());
1415 return constants().boollit(var.boolVar(_solution).val());
1416#ifdef GECODE_HAS_FLOAT_VARS
1417 case Type::BT_FLOAT:
1418 assert(var.floatVar(_solution).assigned());
1419 return FloatLit::a(var.floatVar(_solution).val().med());
1420#endif
1421 default:
1422 return NULL;
1423 }
1424 } else {
1425 return id->decl()->e();
1426 }
1427}
1428
1429Val GecodeSolverInstance::getSolutionValue(Variable* v) {
1430 GecodeVariable var = resolveVar(v);
1431
1432 if (var.isbool()) {
1433 assert(var.boolVar(_solution).assigned());
1434 return Val(var.boolVar(_solution).val());
1435 } else {
1436 assert(var.intVar(_solution).assigned());
1437 return Val(var.intVar(_solution).val());
1438 }
1439}
1440
1441void GecodeSolverInstance::prepareEngine(void) {
1442 GCLock lock;
1443 GecodeOptions& _opt = static_cast<GecodeOptions&>(*_options);
1444 delete engine;
1445 engine = nullptr;
1446 if (engine == NULL) {
1447 // TODO: check what we need to do options-wise
1448 std::vector<Expression*> branch_vars;
1449 std::vector<Expression*> solve_args;
1450 Expression* optSearch = NULL;
1451
1452 switch (_current_space->_solveType) {
1453 case MiniZinc::SolveI::SolveType::ST_MIN:
1454 assert(solveExpr != NULL);
1455 branch_vars.push_back(solveExpr);
1456 solve_args.push_back(new ArrayLit(Location(), branch_vars));
1457 if (!_current_space->_optVarIsInt) // TODO: why??
1458 solve_args.push_back(FloatLit::a(0.0));
1459 solve_args.push_back(new Id(Location(), "input_order", NULL));
1460 solve_args.push_back(new Id(
1461 Location(), _current_space->_optVarIsInt ? "indomain_min" : "indomain_split", NULL));
1462 solve_args.push_back(new Id(Location(), "complete", NULL));
1463 optSearch = new Call(
1464 Location(), _current_space->_optVarIsInt ? "int_search" : "float_search", solve_args);
1465 break;
1466 case MiniZinc::SolveI::SolveType::ST_MAX:
1467 branch_vars.push_back(solveExpr);
1468 solve_args.push_back(new ArrayLit(Location(), branch_vars));
1469 if (!_current_space->_optVarIsInt) solve_args.push_back(FloatLit::a(0.0));
1470 solve_args.push_back(new Id(Location(), "input_order", NULL));
1471 solve_args.push_back(
1472 new Id(Location(),
1473 _current_space->_optVarIsInt ? "indomain_max" : "indomain_split_reverse", NULL));
1474 solve_args.push_back(new Id(Location(), "complete", NULL));
1475 optSearch = new Call(
1476 Location(), _current_space->_optVarIsInt ? "int_search" : "float_search", solve_args);
1477 break;
1478 case MiniZinc::SolveI::SolveType::ST_SAT:
1479 break;
1480 default:
1481 assert(false);
1482 }
1483
1484 int seed = _opt.seed;
1485 double decay = _opt.decay;
1486
1487 Annotation search_ann;
1488 createBranchers(search_ann, optSearch, seed, decay, false, /* ignoreUnknown */
1489 std::cerr);
1490
1491 int nodeStop = _opt.nodes;
1492 int failStop = _opt.fails;
1493 int timeStop = _opt.time;
1494
1495 engine_options.stop = Driver::CombinedStop::create(nodeStop, failStop, timeStop, false);
1496 // TODO: add presolving part
1497 if (_current_space->_solveType == MiniZinc::SolveI::SolveType::ST_SAT) {
1498 engine = new MetaEngine<DFS, Driver::EngineToMeta>(this->_current_space, engine_options);
1499 } else {
1500 engine = new MetaEngine<BAB, Driver::EngineToMeta>(this->_current_space, engine_options);
1501 }
1502 }
1503}
1504
1505void GecodeSolverInstance::print_stats() {
1506 Gecode::Search::Statistics stat = engine->statistics();
1507 std::cerr << "%% variables: "
1508 << (_current_space->iv.size() +
1509 _current_space->bv.size() /*+
1510 _current_space->sv.size()*/) << std::endl
1511 << "%% propagators: " << Gecode::PropagatorGroup::all.size(*_current_space) << endl
1512 << "%% propagations: " << stat.propagate << std::endl
1513 << "%% nodes: " << stat.node << std::endl
1514 << "%% failures: " << stat.fail << std::endl
1515 << "%% restarts: " << stat.restart << std::endl
1516 << "%% peak depth: " << stat.depth << std::endl
1517 << std::endl;
1518}
1519
1520void GecodeSolverInstance::processSolution(bool last_sol) {
1521 if (_solution) {
1522 assignSolutionToOutput();
1523 printSolution();
1524 if (_current_space->_solveType == MiniZinc::SolveI::SolveType::ST_SAT) {
1525 if (engine->stopped() || !last_sol) {
1526 _status = SolverInstance::SAT;
1527 } else {
1528 _status = SolverInstance::OPT;
1529 }
1530 } else {
1531 if (engine->stopped()) {
1532 Gecode::Search::Statistics stat = engine->statistics();
1533 Driver::CombinedStop* cs = static_cast<Driver::CombinedStop*>(engine_options.stop);
1534 std::cerr << "% GecodeSolverInstance: ";
1535 int r = cs->reason(stat, engine_options);
1536 if (r & Driver::CombinedStop::SR_INT)
1537 std::cerr << "user interrupt " << std::endl;
1538 else {
1539 if (r & Driver::CombinedStop::SR_NODE) {
1540 _status_reason = SolverInstance::SR_LIMIT;
1541 std::cerr << "node ";
1542 }
1543 if (r & Driver::CombinedStop::SR_FAIL) {
1544 _status_reason = SolverInstance::SR_LIMIT;
1545 std::cerr << "failure ";
1546 }
1547 if (r & Driver::CombinedStop::SR_TIME) {
1548 _status_reason = SolverInstance::SR_LIMIT;
1549 std::cerr << "time ";
1550 }
1551 std::cerr << "limit reached" << std::endl << std::endl;
1552 }
1553 if (_n_found_solutions > 0) {
1554 _status = SolverInstance::SAT;
1555 } else {
1556 _status = SolverInstance::UNKNOWN;
1557 }
1558 } else {
1559 _status = last_sol ? SolverInstance::OPT : SolverInstance::SAT;
1560 }
1561 }
1562 } else {
1563 if (engine->stopped()) {
1564 _status = SolverInstance::UNKNOWN;
1565 } else {
1566 _status = SolverInstance::UNSAT;
1567 }
1568 }
1569}
1570
1571SolverInstanceBase::Status GecodeSolverInstance::solve(void) {
1572 GCLock lock;
1573 SolverInstanceBase::Status ret;
1574 // Reset solutions previously found
1575 _n_found_solutions = 0;
1576 delete _solution;
1577 _solution = nullptr;
1578
1579 GecodeOptions& _opt = static_cast<GecodeOptions&>(*_options);
1580 _only_range_domains = _opt.only_range_domains;
1581 _run_sac = _opt.sac;
1582 _run_shave = _opt.shave;
1583 _pre_passes = _opt.pre_passes;
1584 _print_stats = _opt.statistics;
1585 _all_solutions = _opt.all_solutions;
1586 _n_max_solutions = _opt.n_solutions;
1587 _allow_unbounded_vars = _opt.allow_unbounded_vars;
1588
1589 prepareEngine();
1590
1591 if (_run_sac || _run_shave) {
1592 presolve();
1593 }
1594
1595 int n_max_solutions = _n_max_solutions;
1596 if (n_max_solutions == -1) {
1597 if (_all_solutions) {
1598 n_max_solutions = 0;
1599 } else if (_current_space->_solveType == MiniZinc::SolveI::SolveType::ST_SAT) {
1600 n_max_solutions = 1;
1601 }
1602 }
1603
1604 FznSpace* next_sol = engine->next();
1605 while (next_sol) {
1606 delete _solution;
1607 _solution = next_sol;
1608 _n_found_solutions++;
1609
1610 if (n_max_solutions == 0 || _n_found_solutions <= n_max_solutions) {
1611 // processSolution();
1612 if (_print_stats) print_stats();
1613 }
1614 if (_n_found_solutions == n_max_solutions) {
1615 break;
1616 }
1617 next_sol = engine->next();
1618 }
1619 if (_current_space->_solveType != MiniZinc::SolveI::SolveType::ST_SAT) {
1620 if (n_max_solutions == -1) {
1621 // Print last solution
1622 // processSolution(next_sol == NULL);
1623 if (_print_stats) print_stats();
1624 }
1625 }
1626 if (next_sol == NULL) {
1627 if (_solution) {
1628 ret = engine->stopped() ? SolverInstance::SAT : SolverInstance::OPT;
1629 } else {
1630 ret = engine->stopped() ? SolverInstance::UNKNOWN : SolverInstance::UNSAT;
1631 }
1632 } else {
1633 ret = SolverInstance::SAT;
1634 }
1635 delete engine;
1636 engine = nullptr;
1637 return ret;
1638}
1639
1640class IntVarComp {
1641public:
1642 std::vector<Gecode::IntVar> iv;
1643 IntVarComp(std::vector<Gecode::IntVar> b) { iv = b; }
1644 int operator()(int a, int b) { return iv[a].size() < iv[b].size(); }
1645};
1646
1647class IntVarRangesBwd : public Int::IntVarImpBwd {
1648public:
1649 IntVarRangesBwd(void) {}
1650 IntVarRangesBwd(const IntVar& x) : Int::IntVarImpBwd(x.varimp()) {}
1651 void init(const IntVar& x) { Int::IntVarImpBwd(x.varimp()); }
1652};
1653
1654bool GecodeSolverInstance::sac(bool toFixedPoint = false, bool shaving = false) {
1655 if (_current_space->status() == SS_FAILED) return false;
1656 bool modified;
1657 std::vector<int> sorted_iv;
1658
1659 for (unsigned int i = 0; i < _current_space->iv.size(); i++)
1660 if (!_current_space->iv[i].assigned()) sorted_iv.push_back(i);
1661 IntVarComp ivc(_current_space->iv);
1662 sort(sorted_iv.begin(), sorted_iv.end(), ivc);
1663
1664 do {
1665 modified = false;
1666 for (unsigned int idx = 0; idx < _current_space->bv.size(); idx++) {
1667 BoolVar bvar = _current_space->bv[idx];
1668 if (!bvar.assigned()) {
1669 for (int val = bvar.min(); val <= bvar.max(); ++val) {
1670 FznSpace* f = static_cast<FznSpace*>(_current_space->clone());
1671 rel(*f, f->bv[idx], IRT_EQ, val);
1672 if (f->status() == SS_FAILED) {
1673 rel(*_current_space, bvar, IRT_NQ, val);
1674 modified = true;
1675 if (_current_space->status() == SS_FAILED) return false;
1676 }
1677 delete f;
1678 }
1679 }
1680 }
1681
1682 for (unsigned int i = 0; i < sorted_iv.size(); i++) {
1683 unsigned int idx = sorted_iv[i];
1684 IntVar ivar = _current_space->iv[idx];
1685 bool tight = false;
1686 unsigned int nnq = 0;
1687 int fwd_min;
1688 IntArgs nq(ivar.size());
1689 for (IntVarValues vv(ivar); vv() && !tight; ++vv) {
1690 FznSpace* f = static_cast<FznSpace*>(_current_space->clone());
1691 rel(*f, f->iv[idx], IRT_EQ, vv.val());
1692 if (f->status() == SS_FAILED) {
1693 nq[nnq++] = vv.val();
1694 } else {
1695 fwd_min = vv.val();
1696 tight = shaving;
1697 }
1698 delete f;
1699 }
1700 if (shaving) {
1701 tight = false;
1702 for (IntVarRangesBwd vr(ivar); vr() && !tight; ++vr) {
1703 for (int i = vr.max(); i >= vr.min() && i >= fwd_min; i--) {
1704 FznSpace* f = static_cast<FznSpace*>(_current_space->clone());
1705 rel(*f, f->iv[idx], IRT_EQ, i);
1706 if (f->status() == SS_FAILED)
1707 nq[nnq++] = i;
1708 else
1709 tight = true;
1710 delete f;
1711 }
1712 }
1713 }
1714 if (nnq) modified = true;
1715 while (nnq--) rel(*_current_space, ivar, IRT_NQ, nq[nnq]);
1716 if (_current_space->status() == SS_FAILED) return false;
1717 }
1718 } while (toFixedPoint && modified);
1719 return true;
1720}
1721
1722bool GecodeSolverInstance::presolve(Model* orig_model) {
1723 GCLock lock;
1724 if (_current_space->status() == SS_FAILED) return false;
1725 // run SAC?
1726 if (_run_sac || _run_shave) {
1727 unsigned int iters = _pre_passes;
1728 if (iters) {
1729 for (unsigned int i = 0; i < iters; i++) sac(false, _run_shave);
1730 } else {
1731 sac(true, _run_shave);
1732 }
1733 }
1734
1735 if (orig_model != NULL) {
1736 std::unordered_map<std::string, VarDecl*> vds;
1737 for (VarDeclIterator it = orig_model->begin_vardecls(); it != orig_model->end_vardecls();
1738 ++it) {
1739 VarDecl* vd = it->e();
1740 vds[vd->id()->str().str()] = vd;
1741 }
1742
1743 // TODO: Does not work for new SolverInstance
1744 // IdMap<GecodeVariable>::iterator it;
1745 // for(auto it = _variableMap.begin(); it != _variableMap.end(); it++) {
1746 // int vd = it->first->decl();
1747 // long long int old_domsize = 0;
1748 // bool holes = false;
1749
1750 // if(vd->ti()->domain()) {
1751 // if(vd->type().isint()) {
1752 // IntBounds old_bounds = compute_int_bounds(_env.envi(), vd->id());
1753 // long long int old_rangesize = abs(old_bounds.u.toInt() - old_bounds.l.toInt());
1754 // if(vd->ti()->domain()->isa<SetLit>())
1755 // old_domsize = arg2intset(_env.envi(), vd->ti()->domain()).size();
1756 // else
1757 // old_domsize = old_rangesize + 1;
1758 // holes = old_domsize < old_rangesize + 1;
1759 // }
1760 // }
1761
1762 // std::string name = it->first->str().str();
1763
1764 // if(vds.find(name) != vds.end()) {
1765 // VarDecl* nvd = vds[name];
1766 // Type::BaseType bt = vd->type().bt();
1767 // if(bt == Type::BaseType::BT_INT) {
1768 // IntVar intvar = it->second.intVar(_current_space);
1769 // const long long int l = intvar.min(), u = intvar.max();
1770
1771 // if(l==u) {
1772 // if(nvd->e()) {
1773 // nvd->ti()->domain(new SetLit(nvd->loc(), IntSetVal::a(l, u)));
1774 // } else {
1775 // nvd->type(Type::parint());
1776 // nvd->ti(new TypeInst(nvd->loc(), Type::parint()));
1777 // nvd->e(IntLit::a(l));
1778 // }
1779 // } else if(!(l == Gecode::Int::Limits::min || u == Gecode::Int::Limits::max)){
1780 // if(_only_range_domains && !holes) {
1781 // nvd->ti()->domain(new SetLit(nvd->loc(), IntSetVal::a(l, u)));
1782 // } else {
1783 // IntVarRanges ivr(intvar);
1784 // nvd->ti()->domain(new SetLit(nvd->loc(), IntSetVal::ai(ivr)));
1785 // }
1786 // }
1787 // } else if(bt == Type::BaseType::BT_BOOL) {
1788 // BoolVar boolvar = it->second.boolVar(_current_space);
1789 // int l = boolvar.min(),
1790 // u = boolvar.max();
1791 // if(l == u) {
1792 // if(nvd->e()) {
1793 // nvd->ti()->domain(constants().boollit(l));
1794 // } else {
1795 // nvd->type(Type::parbool());
1796 // nvd->ti(new TypeInst(nvd->loc(), Type::parbool()));
1797 // nvd->e(new BoolLit(nvd->loc(), l));
1798 // }
1799 // }
1800 // #ifdef GECODE_HAS_FLOAT_VAR
1801 // } else if(bt == Type::BaseType::BT_FLOAT) {
1802 // Gecode::FloatVar floatvar = it->second.floatVar(_current_space);
1803 // if(floatvar.assigned() && !nvd->e()) {
1804 // FloatNum l = floatvar.min();
1805 // nvd->type(Type::parfloat());
1806 // nvd->ti(new TypeInst(nvd->loc(), Type::parfloat()));
1807 // nvd->e(FloatLit::a(l));
1808 // } else {
1809 // FloatNum l = floatvar.min(),
1810 // u = floatvar.max();
1811 // nvd->ti()->domain(new SetLit(nvd->loc(), FloatSetVal::a(l, u)));
1812 // }
1813 // #endif
1814 // }
1815 // }
1816 // }
1817 }
1818 return true;
1819}
1820
1821void GecodeSolverInstance::setSearchStrategyFromAnnotation(
1822 std::vector<Expression*> flatAnn, std::vector<bool>& iv_searched,
1823 std::vector<bool>& bv_searched,
1824#ifdef GECODE_HAS_SET_VARS
1825 std::vector<bool>& sv_searched,
1826#endif
1827#ifdef GECODE_HAS_FLOAT_VARS
1828 std::vector<bool>& fv_searched,
1829#endif
1830 TieBreak<IntVarBranch>& def_int_varsel, IntValBranch& def_int_valsel,
1831 TieBreak<BoolVarBranch>& def_bool_varsel, BoolValBranch& def_bool_valsel,
1832#ifdef GECODE_HAS_SET_VARS
1833 SetVarBranch& def_set_varsel, SetValBranch& def_set_valsel,
1834#endif
1835#ifdef GECODE_HAS_FLOAT_VARS
1836 TieBreak<FloatVarBranch>& def_float_varsel, FloatValBranch& def_float_valsel,
1837#endif
1838 Rnd& rnd, double decay, bool ignoreUnknown, std::ostream& err) {
1839 for (unsigned int i = 0; i < flatAnn.size(); i++) {
1840 if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "gecode_search") {
1841 // Call* c = flatAnn[i]->cast<Call>();
1842 // branchWithPlugin(c->args);
1843 std::cerr << "WARNING: Not supporting search annotation \"gecode_search\" yet." << std::endl;
1844 return;
1845 } else if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "int_search") {
1846 Call* call = flatAnn[i]->cast<Call>();
1847 ArrayLit* vars = arg2arraylit(call->arg(0));
1848 if (vars->size() == 0) { // empty array
1849 std::cerr << "WARNING: trying to branch on empty array in search annotation: " << *call
1850 << std::endl;
1851 continue;
1852 }
1853 int k = vars->size();
1854 for (int i = vars->size(); i--;)
1855 if (!(*vars)[i]->type().isvarint()) k--;
1856 IntVarArgs va(k);
1857 std::vector<std::string> names;
1858 k = 0;
1859 for (unsigned int i = 0; i < vars->size(); i++) {
1860 if (!(*vars)[i]->type().isvarint()) {
1861 continue;
1862 }
1863 int idx = resolveVar(getVarDecl((*vars)[i])).index();
1864 va[k++] = _current_space->iv[idx];
1865 iv_searched[idx] = true;
1866 names.push_back(getVarDecl((*vars)[i])->id()->str().str());
1867 }
1868 std::string r0, r1;
1869 // BrancherHandle bh =
1870 branch(*_current_space, va, ann2ivarsel(call->arg(1)->cast<Id>()->str().str(), rnd, decay),
1871 ann2ivalsel(call->arg(2)->cast<Id>()->str().str(), r0, r1, rnd), NULL
1872 //,&varValPrint<IntVar>
1873 );
1874 // branchInfo.add(bh,r0,r1,names);
1875 } // end int_search
1876 else if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "int_assign") {
1877 Call* call = flatAnn[i]->dyn_cast<Call>();
1878 ArrayLit* vars = arg2arraylit(call->arg(0));
1879 int k = vars->size();
1880 for (int i = vars->size(); i--;)
1881 if (!((*vars)[i])->type().isvarint()) k--;
1882 IntVarArgs va(k);
1883 k = 0;
1884 for (unsigned int i = 0; i < vars->size(); i++) {
1885 if (!((*vars)[i])->type().isvarint()) continue;
1886 int idx = resolveVar(getVarDecl((*vars)[i])).index();
1887 va[k++] = _current_space->iv[idx];
1888 iv_searched[idx] = true;
1889 }
1890 assign(*_current_space, va, ann2asnivalsel(call->arg(1)->cast<Id>()->str().str(), rnd), NULL
1891 //&varValPrint<IntVar>
1892 );
1893 } else if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "bool_search") {
1894 Call* call = flatAnn[i]->dyn_cast<Call>();
1895 ArrayLit* vars = arg2arraylit(call->arg(0));
1896 int k = vars->size();
1897 for (int i = vars->size(); i--;)
1898 if (!((*vars)[i])->type().isvarbool()) k--;
1899 BoolVarArgs va(k);
1900 k = 0;
1901 std::vector<std::string> names;
1902 for (unsigned int i = 0; i < vars->size(); i++) {
1903 if (!((*vars)[i])->type().isvarbool()) continue;
1904 int idx = resolveVar(getVarDecl((*vars)[i])).index();
1905 va[k++] = _current_space->bv[idx];
1906 bv_searched[idx] = true;
1907 names.push_back(getVarDecl((*vars)[i])->id()->str().str());
1908 }
1909
1910 std::string r0, r1;
1911 // BrancherHandle bh =
1912 branch(*_current_space, va, ann2bvarsel(call->arg(1)->cast<Id>()->str().str(), rnd, decay),
1913 ann2bvalsel(call->arg(2)->cast<Id>()->str().str(), r0, r1, rnd), NULL //,
1914 //&varValPrint<BoolVar>
1915 );
1916 // branchInfo.add(bh,r0,r1,names);
1917 } else if (flatAnn[i]->isa<Call>() &&
1918 flatAnn[i]->cast<Call>()->id().str() == "int_default_search") {
1919 Call* call = flatAnn[i]->dyn_cast<Call>();
1920 def_int_varsel = ann2ivarsel(call->arg(0)->cast<Id>()->str().str(), rnd, decay);
1921 std::string r0;
1922 def_int_valsel = ann2ivalsel(call->arg(1)->cast<Id>()->str().str(), r0, r0, rnd);
1923 } else if (flatAnn[i]->isa<Call>() &&
1924 flatAnn[i]->cast<Call>()->id().str() == "bool_default_search") {
1925 Call* call = flatAnn[i]->dyn_cast<Call>();
1926 std::string r0;
1927 def_bool_varsel = ann2bvarsel(call->arg(0)->cast<Id>()->str().str(), rnd, decay);
1928 def_bool_valsel = ann2bvalsel(call->arg(1)->cast<Id>()->str().str(), r0, r0, rnd);
1929 } else if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "set_search") {
1930#ifdef GECODE_HAS_SET_VARS
1931 Call* call = flatAnn[i]->dyn_cast<Call>();
1932 ArrayLit* vars = arg2arraylit(call->arg(0));
1933 int k = vars->size();
1934 for (int i = vars->size(); i--;)
1935 if (!((*vars)[i])->type().is_set() || !((*vars)[i])->type().isvar()) k--;
1936 SetVarArgs va(k);
1937 k = 0;
1938 std::vector<std::string> names;
1939 for (unsigned int i = 0; i < vars->size(); i++) {
1940 if (!((*vars)[i])->type().is_set() || !((*vars)[i])->type().isvar()) continue;
1941 int idx = resolveVar(getVarDecl((*vars)[i])).index();
1942 va[k++] = _current_space->sv[idx];
1943 sv_searched[idx] = true;
1944 names.push_back(getVarDecl((*vars)[i])->id()->str().str());
1945 }
1946 std::string r0, r1;
1947 // BrancherHandle bh =
1948 branch(*_current_space, va, ann2svarsel(call->arg(1)->cast<Id>()->str().str(), rnd, decay),
1949 ann2svalsel(call->arg(2)->cast<Id>()->str().str(), r0, r1, rnd),
1950 NULL //,
1951 //&varValPrint<SetVar>
1952 );
1953 // branchInfo.add(bh,r0,r1,names);
1954#else
1955 if (!ignoreUnknown) {
1956 err << "Warning, ignored search annotation: ";
1957 // flatAnn[i]->print(err);
1958 err << std::endl;
1959 }
1960#endif
1961 } else if (flatAnn[i]->isa<Call>() &&
1962 flatAnn[i]->cast<Call>()->id().str() == "set_default_search") {
1963#ifdef GECODE_HAS_SET_VARS
1964 Call* call = flatAnn[i]->dyn_cast<Call>();
1965 def_set_varsel = ann2svarsel(call->arg(0)->cast<Id>()->str().str(), rnd, decay);
1966 std::string r0;
1967 def_set_valsel = ann2svalsel(call->arg(1)->cast<Id>()->str().str(), r0, r0, rnd);
1968#else
1969 if (!ignoreUnknown) {
1970 err << "Warning, ignored search annotation: ";
1971 // flatAnn[i]->print(err);
1972 err << std::endl;
1973 }
1974#endif
1975 } else if (flatAnn[i]->isa<Call>() &&
1976 flatAnn[i]->cast<Call>()->id().str() == "float_default_search") {
1977#ifdef GECODE_HAS_FLOAT_VARS
1978 Call* call = flatAnn[i]->dyn_cast<Call>();
1979 def_float_varsel = ann2fvarsel(call->arg(0)->cast<Id>()->str().str(), rnd, decay);
1980 std::string r0;
1981 def_float_valsel = ann2fvalsel(call->arg(1)->cast<Id>()->str().str(), r0, r0);
1982#else
1983 if (!ignoreUnknown) {
1984 err << "Warning, ignored search annotation: float_default_search" << std::endl;
1985 }
1986#endif
1987 } else if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "float_search") {
1988#ifdef GECODE_HAS_FLOAT_VARS
1989 Call* call = flatAnn[i]->dyn_cast<Call>();
1990 ArrayLit* vars = call->arg(0)->cast<ArrayLit>();
1991 int k = vars->size();
1992 for (int i = vars->size(); i--;)
1993 if (!((*vars)[i])->type().isvarfloat()) k--;
1994 FloatVarArgs va(k);
1995 k = 0;
1996 std::vector<std::string> names;
1997 for (unsigned int i = 0; i < vars->size(); i++) {
1998 if (!((*vars)[i])->type().isvarfloat()) continue;
1999 int idx = resolveVar(getVarDecl((*vars)[i])).index();
2000 va[k++] = _current_space->fv[idx];
2001 fv_searched[idx] = true;
2002 names.push_back(getVarDecl((*vars)[i])->id()->str().str());
2003 }
2004 std::string r0, r1;
2005 // BrancherHandle bh =
2006 branch(*_current_space, va, ann2fvarsel(call->arg(2)->cast<Id>()->str().str(), rnd, decay),
2007 ann2fvalsel(call->arg(3)->cast<Id>()->str().str(), r0, r1),
2008 NULL //,
2009 //&varValPrintF
2010 );
2011 // branchInfo.add(bh,r0,r1,names);
2012#else
2013 if (!ignoreUnknown) {
2014 err << "Warning, ignored search annotation: float_search" << std::endl;
2015 }
2016#endif
2017 } else {
2018 if (!ignoreUnknown) {
2019 err << "Warning, ignored search annotation: " << *flatAnn[i] << std::endl;
2020 }
2021 }
2022 } // end for all annotations
2023}
2024
2025void GecodeSolverInstance::createBranchers(Annotation& ann, Expression* additionalAnn, int seed,
2026 double decay, bool ignoreUnknown, std::ostream& err) {
2027 // default search heuristics
2028 Rnd rnd(static_cast<unsigned int>(seed));
2029 TieBreak<IntVarBranch> def_int_varsel = INT_VAR_AFC_SIZE_MAX(0.99);
2030 IntValBranch def_int_valsel = INT_VAL_MIN();
2031 TieBreak<BoolVarBranch> def_bool_varsel = BOOL_VAR_AFC_MAX(0.99);
2032 BoolValBranch def_bool_valsel = BOOL_VAL_MIN();
2033#ifdef GECODE_HAS_SET_VARS
2034 SetVarBranch def_set_varsel = SET_VAR_AFC_SIZE_MAX(0.99);
2035 SetValBranch def_set_valsel = SET_VAL_MIN_INC();
2036#endif
2037#ifdef GECODE_HAS_FLOAT_VARS
2038 TieBreak<FloatVarBranch> def_float_varsel = FLOAT_VAR_SIZE_MIN();
2039 FloatValBranch def_float_valsel = FLOAT_VAL_SPLIT_MIN();
2040#endif
2041
2042 std::vector<bool> iv_searched(_current_space->iv.size());
2043 for (unsigned int i = _current_space->iv.size(); i--;) iv_searched[i] = false;
2044 std::vector<bool> bv_searched(_current_space->bv.size());
2045 for (unsigned int i = _current_space->bv.size(); i--;) bv_searched[i] = false;
2046#ifdef GECODE_HAS_SET_VARS
2047 std::vector<bool> sv_searched(_current_space->sv.size());
2048 for (unsigned int i = _current_space->sv.size(); i--;) sv_searched[i] = false;
2049#endif
2050#ifdef GECODE_HAS_FLOAT_VARS
2051 std::vector<bool> fv_searched(_current_space->fv.size());
2052 for (unsigned int i = _current_space->fv.size(); i--;) fv_searched[i] = false;
2053#endif
2054
2055 // solving annotations
2056 std::vector<Expression*> flatAnn;
2057 if (!ann.isEmpty()) {
2058 flattenSearchAnnotations(ann, flatAnn);
2059 }
2060 if (additionalAnn != NULL) {
2061 flatAnn.push_back(additionalAnn);
2062 }
2063 if (flatAnn.size() > 0) {
2064 setSearchStrategyFromAnnotation(flatAnn, iv_searched, bv_searched,
2065#ifdef GECODE_HAS_SET_VARS
2066 sv_searched,
2067#endif
2068#ifdef GECODE_HAS_FLOAT_VARS
2069 fv_searched,
2070#endif
2071 def_int_varsel, def_int_valsel, def_bool_varsel,
2072 def_bool_valsel,
2073#ifdef GECODE_HAS_SET_VARS
2074 def_set_varsel, def_set_valsel,
2075#endif
2076#ifdef GECODE_HAS_FLOAT_VARS
2077 def_float_varsel, def_float_valsel,
2078#endif
2079 rnd, decay, ignoreUnknown, err);
2080 }
2081
2082 int introduced = 0;
2083 int funcdep = 0;
2084 int searched = 0;
2085 for (int i = _current_space->iv.size(); i--;) {
2086 if (iv_searched[i]) {
2087 searched++;
2088 } else if (_current_space->iv_introduced[i]) {
2089 if (_current_space->iv_defined[i]) {
2090 funcdep++;
2091 } else {
2092 introduced++;
2093 }
2094 }
2095 }
2096 IntVarArgs iv_sol(_current_space->iv.size() - (introduced + funcdep + searched));
2097 IntVarArgs iv_tmp(introduced);
2098 for (unsigned int i = _current_space->iv.size(), j = 0, k = 0; i--;) {
2099 if (iv_searched[i]) continue;
2100 if (_current_space->iv_introduced[i]) {
2101 if (_current_space->iv_introduced.size() >= i) {
2102 if (!_current_space->iv_defined[i]) {
2103 iv_tmp[j++] = _current_space->iv[i];
2104 }
2105 }
2106 } else {
2107 iv_sol[k++] = _current_space->iv[i];
2108 }
2109 }
2110 // Collecting Boolean variables
2111 introduced = 0;
2112 funcdep = 0;
2113 searched = 0;
2114 for (int i = _current_space->bv.size(); i--;) {
2115 if (bv_searched[i]) {
2116 searched++;
2117 } else if (_current_space->bv_introduced[i]) {
2118 if (_current_space->bv_defined[i]) {
2119 funcdep++;
2120 } else {
2121 introduced++;
2122 }
2123 }
2124 }
2125 BoolVarArgs bv_sol(_current_space->bv.size() - (introduced + funcdep + searched));
2126 BoolVarArgs bv_tmp(introduced);
2127 for (int i = _current_space->bv.size(), j = 0, k = 0; i--;) {
2128 if (bv_searched[i]) continue;
2129 if (_current_space->bv_introduced[i]) {
2130 if (!_current_space->bv_defined[i]) {
2131 bv_tmp[j++] = _current_space->bv[i];
2132 }
2133 } else {
2134 bv_sol[k++] = _current_space->bv[i];
2135 }
2136 }
2137
2138 if (iv_sol.size() > 0) branch(*this->_current_space, iv_sol, def_int_varsel, def_int_valsel);
2139 if (bv_sol.size() > 0) branch(*this->_current_space, bv_sol, def_bool_varsel, def_bool_valsel);
2140
2141 // std::cout << "DEBUG: branched over " << iv_sol.size() << " integer variables."<<
2142 // std::endl; std::cout << "DEBUG: branched over " << bv_sol.size() << " Boolean
2143 // variables."<< std::endl;
2144#ifdef GECODE_HAS_FLOAT_VARS
2145 introduced = 0;
2146 funcdep = 0;
2147 searched = 0;
2148 for (int i = _current_space->fv.size(); i--;) {
2149 if (fv_searched[i]) {
2150 searched++;
2151 } else if (_current_space->fv_introduced[i]) {
2152 if (_current_space->fv_defined[i]) {
2153 funcdep++;
2154 } else {
2155 introduced++;
2156 }
2157 }
2158 }
2159 FloatVarArgs fv_sol(_current_space->fv.size() - (introduced + funcdep + searched));
2160 FloatVarArgs fv_tmp(introduced);
2161 for (int i = _current_space->fv.size(), j = 0, k = 0; i--;) {
2162 if (fv_searched[i]) continue;
2163 if (_current_space->fv_introduced[i]) {
2164 if (!_current_space->fv_defined[i]) {
2165 fv_tmp[j++] = _current_space->fv[i];
2166 }
2167 } else {
2168 fv_sol[k++] = _current_space->fv[i];
2169 }
2170 }
2171
2172 if (fv_sol.size() > 0) branch(*this->_current_space, fv_sol, def_float_varsel, def_float_valsel);
2173#endif
2174#ifdef GECODE_HAS_SET_VARS
2175 introduced = 0;
2176 funcdep = 0;
2177 searched = 0;
2178 for (int i = _current_space->sv.size(); i--;) {
2179 if (sv_searched[i]) {
2180 searched++;
2181 } else if (_current_space->sv_introduced[i]) {
2182 if (_current_space->sv_defined[i]) {
2183 funcdep++;
2184 } else {
2185 introduced++;
2186 }
2187 }
2188 }
2189 SetVarArgs sv_sol(_current_space->sv.size() - (introduced + funcdep + searched));
2190 SetVarArgs sv_tmp(introduced);
2191 for (int i = _current_space->sv.size(), j = 0, k = 0; i--;) {
2192 if (sv_searched[i]) continue;
2193 if (_current_space->sv_introduced[i]) {
2194 if (!_current_space->sv_defined[i]) {
2195 sv_tmp[j++] = _current_space->sv[i];
2196 }
2197 } else {
2198 sv_sol[k++] = _current_space->sv[i];
2199 }
2200 }
2201
2202 if (sv_sol.size() > 0) branch(*this->_current_space, sv_sol, def_set_varsel, def_set_valsel);
2203#endif
2204
2205 // branching on auxiliary variables
2206 _current_space->iv_aux = IntVarArray(*this->_current_space, iv_tmp);
2207 _current_space->bv_aux = BoolVarArray(*this->_current_space, bv_tmp);
2208 int n_aux = _current_space->iv_aux.size() + _current_space->bv_aux.size();
2209#ifdef GECODE_HAS_SET_VARS
2210 _current_space->sv_aux = SetVarArray(*this->_current_space, sv_tmp);
2211 n_aux += _current_space->sv_aux.size();
2212#endif
2213#ifdef GECODE_HAS_FLOAT_VARS
2214 _current_space->fv_aux = FloatVarArray(*this->_current_space, fv_tmp);
2215 n_aux += _current_space->fv_aux.size();
2216#endif
2217 if (n_aux > 0) {
2218 AuxVarBrancher::post(*this->_current_space, def_int_varsel, def_int_valsel, def_bool_varsel,
2219 def_bool_valsel
2220#ifdef GECODE_HAS_SET_VARS
2221 ,
2222 def_set_varsel, def_set_valsel
2223#endif
2224#ifdef GECODE_HAS_FLOAT_VARS
2225 ,
2226 def_float_varsel, def_float_valsel
2227#endif
2228 ); // end post
2229 // std::cout << "DEBUG: Posted aux-var-brancher for " << n_aux << " aux-variables" <<
2230 // std::endl;
2231 } // end if n_aux > 0
2232 // else
2233 // std::cout << "DEBUG: No aux vars to branch on." << std::endl;
2234}
2235
2236TieBreak<IntVarBranch> GecodeSolverInstance::ann2ivarsel(std::string s, Rnd& rnd, double decay) {
2237 if (s == "input_order") return TieBreak<IntVarBranch>(INT_VAR_NONE());
2238 if (s == "first_fail") return TieBreak<IntVarBranch>(INT_VAR_SIZE_MIN());
2239 if (s == "anti_first_fail") return TieBreak<IntVarBranch>(INT_VAR_SIZE_MAX());
2240 if (s == "smallest") return TieBreak<IntVarBranch>(INT_VAR_MIN_MIN());
2241 if (s == "largest") return TieBreak<IntVarBranch>(INT_VAR_MAX_MAX());
2242 if (s == "occurrence") return TieBreak<IntVarBranch>(INT_VAR_DEGREE_MAX());
2243 if (s == "max_regret") return TieBreak<IntVarBranch>(INT_VAR_REGRET_MIN_MAX());
2244 if (s == "most_constrained")
2245 return TieBreak<IntVarBranch>(INT_VAR_SIZE_MIN(), INT_VAR_DEGREE_MAX());
2246 if (s == "random") {
2247 return TieBreak<IntVarBranch>(INT_VAR_RND(rnd));
2248 }
2249 if (s == "afc_min") return TieBreak<IntVarBranch>(INT_VAR_AFC_MIN(decay));
2250 if (s == "afc_max") return TieBreak<IntVarBranch>(INT_VAR_AFC_MAX(decay));
2251 if (s == "afc_size_min") return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MIN(decay));
2252 if (s == "afc_size_max" || s == "dom_w_deg") {
2253 return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MAX(decay));
2254 }
2255 if (s == "action_min") return TieBreak<IntVarBranch>(INT_VAR_ACTION_MIN(decay));
2256 if (s == "action_max") return TieBreak<IntVarBranch>(INT_VAR_ACTION_MAX(decay));
2257 if (s == "action_size_min") return TieBreak<IntVarBranch>(INT_VAR_ACTION_SIZE_MIN(decay));
2258 if (s == "action_size_max") return TieBreak<IntVarBranch>(INT_VAR_ACTION_SIZE_MAX(decay));
2259 std::cerr << "Warning, ignored search annotation: " << s << std::endl;
2260 return TieBreak<IntVarBranch>(INT_VAR_NONE());
2261}
2262
2263Gecode::IntValBranch GecodeSolverInstance::ann2ivalsel(std::string s, std::string& r0,
2264 std::string& r1, Rnd& rnd) {
2265 if (s == "indomain_min") {
2266 r0 = "=";
2267 r1 = "!=";
2268 return INT_VAL_MIN();
2269 }
2270 if (s == "indomain_max") {
2271 r0 = "=";
2272 r1 = "!=";
2273 return INT_VAL_MAX();
2274 }
2275 if (s == "indomain_median") {
2276 r0 = "=";
2277 r1 = "!=";
2278 return INT_VAL_MED();
2279 }
2280 if (s == "indomain_split") {
2281 r0 = "<=";
2282 r1 = ">";
2283 return INT_VAL_SPLIT_MIN();
2284 }
2285 if (s == "indomain_reverse_split") {
2286 r0 = ">";
2287 r1 = "<=";
2288 return INT_VAL_SPLIT_MAX();
2289 }
2290 if (s == "indomain_random") {
2291 r0 = "=";
2292 r1 = "!=";
2293 return INT_VAL_RND(rnd);
2294 }
2295 if (s == "indomain") {
2296 r0 = "=";
2297 r1 = "=";
2298 return INT_VALUES_MIN();
2299 }
2300 if (s == "indomain_middle") {
2301 std::cerr << "Warning, replacing unsupported annotation "
2302 << "indomain_middle with indomain_median" << std::endl;
2303 r0 = "=";
2304 r1 = "!=";
2305 return INT_VAL_MED();
2306 }
2307 if (s == "indomain_interval") {
2308 std::cerr << "Warning, replacing unsupported annotation "
2309 << "indomain_interval with indomain_split" << std::endl;
2310 r0 = "<=";
2311 r1 = ">";
2312 return INT_VAL_SPLIT_MIN();
2313 }
2314 std::cerr << "Warning, ignored search annotation: " << s << std::endl;
2315 r0 = "=";
2316 r1 = "!=";
2317 return INT_VAL_MIN();
2318}
2319
2320TieBreak<BoolVarBranch> GecodeSolverInstance::ann2bvarsel(std::string s, Rnd& rnd, double decay) {
2321 if ((s == "input_order") || (s == "first_fail") || (s == "anti_first_fail") ||
2322 (s == "smallest") || (s == "largest") || (s == "max_regret"))
2323 return TieBreak<BoolVarBranch>(BOOL_VAR_NONE());
2324 if ((s == "occurrence") || (s == "most_constrained"))
2325 return TieBreak<BoolVarBranch>(BOOL_VAR_DEGREE_MAX());
2326 if (s == "random") return TieBreak<BoolVarBranch>(BOOL_VAR_RND(rnd));
2327 if ((s == "afc_min") || (s == "afc_size_min"))
2328 return TieBreak<BoolVarBranch>(BOOL_VAR_AFC_MIN(decay));
2329 if ((s == "afc_max") || (s == "afc_size_max") || (s == "dom_w_deg"))
2330 return TieBreak<BoolVarBranch>(BOOL_VAR_AFC_MAX(decay));
2331 if ((s == "action_min") && (s == "action_size_min"))
2332 return TieBreak<BoolVarBranch>(BOOL_VAR_ACTION_MIN(decay));
2333 if ((s == "action_max") || (s == "action_size_max"))
2334 return TieBreak<BoolVarBranch>(BOOL_VAR_ACTION_MAX(decay));
2335 std::cerr << "Warning, ignored search annotation: " << s << std::endl;
2336 return TieBreak<BoolVarBranch>(BOOL_VAR_NONE());
2337}
2338
2339BoolValBranch GecodeSolverInstance::ann2bvalsel(std::string s, std::string& r0, std::string& r1,
2340 Rnd& rnd) {
2341 if (s == "indomain_min") {
2342 r0 = "=";
2343 r1 = "!=";
2344 return BOOL_VAL_MIN();
2345 }
2346 if (s == "indomain_max") {
2347 r0 = "=";
2348 r1 = "!=";
2349 return BOOL_VAL_MAX();
2350 }
2351 if (s == "indomain_median") {
2352 r0 = "=";
2353 r1 = "!=";
2354 return BOOL_VAL_MIN();
2355 }
2356 if (s == "indomain_split") {
2357 r0 = "<=";
2358 r1 = ">";
2359 return BOOL_VAL_MIN();
2360 }
2361 if (s == "indomain_reverse_split") {
2362 r0 = ">";
2363 r1 = "<=";
2364 return BOOL_VAL_MAX();
2365 }
2366 if (s == "indomain_random") {
2367 r0 = "=";
2368 r1 = "!=";
2369 return BOOL_VAL_RND(rnd);
2370 }
2371 if (s == "indomain") {
2372 r0 = "=";
2373 r1 = "=";
2374 return BOOL_VAL_MIN();
2375 }
2376 if (s == "indomain_middle") {
2377 std::cerr << "Warning, replacing unsupported annotation "
2378 << "indomain_middle with indomain_median" << std::endl;
2379 r0 = "=";
2380 r1 = "!=";
2381 return BOOL_VAL_MIN();
2382 }
2383 if (s == "indomain_interval") {
2384 std::cerr << "Warning, replacing unsupported annotation "
2385 << "indomain_interval with indomain_split" << std::endl;
2386 r0 = "<=";
2387 r1 = ">";
2388 return BOOL_VAL_MIN();
2389 }
2390 std::cerr << "Warning, ignored search annotation: " << s << "\n";
2391 r0 = "=";
2392 r1 = "!=";
2393 return BOOL_VAL_MIN();
2394}
2395
2396BoolAssign GecodeSolverInstance::ann2asnbvalsel(std::string s, Rnd& rnd) {
2397 if ((s == "indomain_min") || (s == "indomain_median")) return BOOL_ASSIGN_MIN();
2398 if (s == "indomain_max") return BOOL_ASSIGN_MAX();
2399 if (s == "indomain_random") {
2400 return BOOL_ASSIGN_RND(rnd);
2401 }
2402 std::cerr << "Warning, ignored search annotation: " << s << "\n";
2403 return BOOL_ASSIGN_MIN();
2404}
2405
2406IntAssign GecodeSolverInstance::ann2asnivalsel(std::string s, Rnd& rnd) {
2407 if (s == "indomain_min") return INT_ASSIGN_MIN();
2408 if (s == "indomain_max") return INT_ASSIGN_MAX();
2409 if (s == "indomain_median") return INT_ASSIGN_MED();
2410 if (s == "indomain_random") {
2411 return INT_ASSIGN_RND(rnd);
2412 }
2413 std::cerr << "Warning, ignored search annotation: " << s << std::endl;
2414 return INT_ASSIGN_MIN();
2415}
2416
2417void GecodeSolverInstance::pushState() {
2418 stack.push_back(_current_space);
2419 _variableMap.emplace_back();
2420 _current_space->status();
2421 _current_space = static_cast<FznSpace*>(_current_space->clone());
2422}
2423
2424void GecodeSolverInstance::popState() {
2425 delete _current_space;
2426 _current_space = stack.back();
2427 stack.pop_back();
2428 _variableMap.pop_back();
2429}
2430
2431#ifdef GECODE_HAS_SET_VARS
2432SetVarBranch GecodeSolverInstance::ann2svarsel(std::string s, Rnd& rnd, double decay) {
2433 if (s == "input_order") return SET_VAR_NONE();
2434 if (s == "first_fail") return SET_VAR_SIZE_MIN();
2435 if (s == "anti_first_fail") return SET_VAR_SIZE_MAX();
2436 if (s == "smallest") return SET_VAR_MIN_MIN();
2437 if (s == "largest") return SET_VAR_MAX_MAX();
2438 if (s == "afc_min") return SET_VAR_AFC_MIN(decay);
2439 if (s == "afc_max") return SET_VAR_AFC_MAX(decay);
2440 if (s == "afc_size_min") return SET_VAR_AFC_SIZE_MIN(decay);
2441 if (s == "afc_size_max") return SET_VAR_AFC_SIZE_MAX(decay);
2442 if (s == "action_min") return SET_VAR_ACTION_MIN(decay);
2443 if (s == "action_max") return SET_VAR_ACTION_MAX(decay);
2444 if (s == "action_size_min") return SET_VAR_ACTION_SIZE_MIN(decay);
2445 if (s == "action_size_max") return SET_VAR_ACTION_SIZE_MAX(decay);
2446 if (s == "random") {
2447 return SET_VAR_RND(rnd);
2448 }
2449 std::cerr << "Warning, ignored search annotation: " << s << std::endl;
2450 return SET_VAR_NONE();
2451}
2452
2453SetValBranch GecodeSolverInstance::ann2svalsel(std::string s, std::string r0, std::string r1,
2454 Rnd& rnd) {
2455 (void)rnd;
2456 if (s == "indomain_min") {
2457 r0 = "in";
2458 r1 = "not in";
2459 return SET_VAL_MIN_INC();
2460 }
2461 if (s == "indomain_max") {
2462 r0 = "in";
2463 r1 = "not in";
2464 return SET_VAL_MAX_INC();
2465 }
2466 if (s == "outdomain_min") {
2467 r1 = "in";
2468 r0 = "not in";
2469 return SET_VAL_MIN_EXC();
2470 }
2471 if (s == "outdomain_max") {
2472 r1 = "in";
2473 r0 = "not in";
2474 return SET_VAL_MAX_EXC();
2475 }
2476 std::cerr << "Warning, ignored search annotation: " << s << std::endl;
2477 r0 = "in";
2478 r1 = "not in";
2479 return SET_VAL_MIN_INC();
2480}
2481#endif
2482
2483#ifdef GECODE_HAS_FLOAT_VARS
2484TieBreak<FloatVarBranch> GecodeSolverInstance::ann2fvarsel(std::string s, Rnd& rnd, double decay) {
2485 if (s == "input_order") return TieBreak<FloatVarBranch>(FLOAT_VAR_NONE());
2486 if (s == "first_fail") return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MIN());
2487 if (s == "anti_first_fail") return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MAX());
2488 if (s == "smallest") return TieBreak<FloatVarBranch>(FLOAT_VAR_MIN_MIN());
2489 if (s == "largest") return TieBreak<FloatVarBranch>(FLOAT_VAR_MAX_MAX());
2490 if (s == "occurrence") return TieBreak<FloatVarBranch>(FLOAT_VAR_DEGREE_MAX());
2491 if (s == "most_constrained")
2492 return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MIN(), FLOAT_VAR_DEGREE_MAX());
2493 if (s == "random") {
2494 return TieBreak<FloatVarBranch>(FLOAT_VAR_RND(rnd));
2495 }
2496 if (s == "afc_min") return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_MIN(decay));
2497 if (s == "afc_max") return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_MAX(decay));
2498 if (s == "afc_size_min") return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_SIZE_MIN(decay));
2499 if (s == "afc_size_max") return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_SIZE_MAX(decay));
2500 if (s == "action_min") return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_MIN(decay));
2501 if (s == "action_max") return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_MAX(decay));
2502 if (s == "action_size_min") return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_SIZE_MIN(decay));
2503 if (s == "action_size_max") return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_SIZE_MAX(decay));
2504 std::cerr << "Warning, ignored search annotation: " << s << std::endl;
2505 return TieBreak<FloatVarBranch>(FLOAT_VAR_NONE());
2506}
2507
2508FloatValBranch GecodeSolverInstance::ann2fvalsel(std::string s, std::string r0, std::string r1) {
2509 if (s == "indomain_split") {
2510 r0 = "<=";
2511 r1 = ">";
2512 return FLOAT_VAL_SPLIT_MIN();
2513 }
2514 if (s == "indomain_reverse_split") {
2515 r1 = "<=";
2516 r0 = ">";
2517 return FLOAT_VAL_SPLIT_MAX();
2518 }
2519 std::cerr << "Warning, ignored search annotation: " << s << std::endl;
2520 r0 = "<=";
2521 r1 = ">";
2522 return FLOAT_VAL_SPLIT_MIN();
2523}
2524#endif
2525} // namespace MiniZinc