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