Something went wrong. Try again.
This repository has no description
Something went wrong. Try again.
102 kB · 2525 lines
C++
at develop
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900901902903904905906907908909910911912913914915916917918919920921922923924925926927928929930931932933934935936937938939940941942943944945946947948949950951952953954955956957958959960961962963964965966967968969970971972973974975976977978979980981982983984985986987988989990991992993994995996997998999100010011002100310041005100610071008100910101011101210131014101510161017101810191020102110221023102410251026102710281029103010311032103310341035103610371038103910401041104210431044104510461047104810491050105110521053105410551056105710581059106010611062106310641065106610671068106910701071107210731074107510761077107810791080108110821083108410851086108710881089109010911092109310941095109610971098109911001101110211031104110511061107110811091110111111121113111411151116111711181119112011211122112311241125112611271128112911301131113211331134113511361137113811391140114111421143114411451146114711481149115011511152115311541155115611571158115911601161116211631164116511661167116811691170117111721173117411751176117711781179118011811182118311841185118611871188118911901191119211931194119511961197119811991200120112021203120412051206120712081209121012111212121312141215121612171218121912201221122212231224122512261227122812291230123112321233123412351236123712381239124012411242124312441245124612471248124912501251125212531254125512561257125812591260126112621263126412651266126712681269127012711272127312741275127612771278127912801281128212831284128512861287128812891290129112921293129412951296129712981299130013011302130313041305130613071308130913101311131213131314131513161317131813191320132113221323132413251326132713281329133013311332133313341335133613371338133913401341134213431344134513461347134813491350135113521353135413551356135713581359136013611362136313641365136613671368136913701371137213731374137513761377137813791380138113821383138413851386138713881389139013911392139313941395139613971398139914001401140214031404140514061407140814091410141114121413141414151416141714181419142014211422142314241425142614271428142914301431143214331434143514361437143814391440144114421443144414451446144714481449145014511452145314541455145614571458145914601461146214631464146514661467146814691470147114721473147414751476147714781479148014811482148314841485148614871488148914901491149214931494149514961497149814991500150115021503150415051506150715081509151015111512151315141515151615171518151915201521152215231524152515261527152815291530153115321533153415351536153715381539154015411542154315441545154615471548154915501551155215531554155515561557155815591560156115621563156415651566156715681569157015711572157315741575157615771578157915801581158215831584158515861587158815891590159115921593159415951596159715981599160016011602160316041605160616071608160916101611161216131614161516161617161816191620162116221623162416251626162716281629163016311632163316341635163616371638163916401641164216431644164516461647164816491650165116521653165416551656165716581659166016611662166316641665166616671668166916701671167216731674167516761677167816791680168116821683168416851686168716881689169016911692169316941695169616971698169917001701170217031704170517061707170817091710171117121713171417151716171717181719172017211722172317241725172617271728172917301731173217331734173517361737173817391740174117421743174417451746174717481749175017511752175317541755175617571758175917601761176217631764176517661767176817691770177117721773177417751776177717781779178017811782178317841785178617871788178917901791179217931794179517961797179817991800180118021803180418051806180718081809181018111812181318141815181618171818181918201821182218231824182518261827182818291830183118321833183418351836183718381839184018411842184318441845184618471848184918501851185218531854185518561857185818591860186118621863186418651866186718681869187018711872187318741875187618771878187918801881188218831884188518861887188818891890189118921893189418951896189718981899190019011902190319041905190619071908190919101911191219131914191519161917191819191920192119221923192419251926192719281929193019311932193319341935193619371938193919401941194219431944194519461947194819491950195119521953195419551956195719581959196019611962196319641965196619671968196919701971197219731974197519761977197819791980198119821983198419851986198719881989199019911992199319941995199619971998199920002001200220032004200520062007200820092010201120122013201420152016201720182019202020212022202320242025202620272028202920302031203220332034203520362037203820392040204120422043204420452046204720482049205020512052205320542055205620572058205920602061206220632064206520662067206820692070207120722073207420752076207720782079208020812082208320842085208620872088208920902091209220932094209520962097209820992100210121022103210421052106210721082109211021112112211321142115211621172118211921202121212221232124212521262127212821292130213121322133213421352136213721382139214021412142214321442145214621472148214921502151215221532154215521562157215821592160216121622163216421652166216721682169217021712172217321742175217621772178217921802181218221832184218521862187218821892190219121922193219421952196219721982199220022012202220322042205220622072208220922102211221222132214221522162217221822192220222122222223222422252226222722282229223022312232223322342235223622372238223922402241224222432244224522462247224822492250225122522253225422552256225722582259226022612262226322642265226622672268226922702271227222732274227522762277227822792280228122822283228422852286228722882289229022912292229322942295229622972298229923002301230223032304230523062307230823092310231123122313231423152316231723182319232023212322232323242325232623272328232923302331233223332334233523362337233823392340234123422343234423452346234723482349235023512352235323542355235623572358235923602361236223632364236523662367236823692370237123722373237423752376237723782379238023812382238323842385238623872388238923902391239223932394239523962397239823992400240124022403240424052406240724082409241024112412241324142415241624172418241924202421242224232424242524262427242824292430243124322433243424352436243724382439244024412442244324442445244624472448244924502451245224532454245524562457245824592460246124622463246424652466246724682469247024712472247324742475247624772478247924802481248224832484248524862487248824892490249124922493249424952496249724982499250025012502250325042505250625072508250925102511251225132514251525162517251825192520252125222523252425252526/* * Main authors: * Kevin Leo <kevin.leo@monash.edu> * Andrea Rendl <andrea.rendl@nicta.com.au> * Guido Tack <guido.tack@monash.edu> */
/* This Source Code Form is subject to the terms of the Mozilla Public * License, v. 2.0. If a copy of the MPL was not distributed with this * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
#include <minizinc/ast.hh>#include <minizinc/eval_par.hh>#include <minizinc/exception.hh>#include <minizinc/solvers/gecode/fzn_space.hh>#include <minizinc/solvers/gecode/gecode_constraints.hh>#include <minizinc/solvers/gecode_solverinstance.hh>
#include "aux_brancher.hh"
using namespace std;using namespace Gecode;
namespace MiniZinc {
Gecode_SolverFactory::Gecode_SolverFactory(void) { SolverConfig sc("org.minizinc.gecode_presolver", GECODE_VERSION); sc.name("Presolver"); sc.mznlib("-Ggecode_presolver"); sc.mznlibVersion(1); sc.supportsMzn(false); sc.description("Internal Gecode presolver plugin"); sc.tags({"cp", "float", "api", "set", "gecode_presolver", "__internal__"}); sc.stdFlags({"-a", "-n"}); SolverConfigs::registerBuiltinSolver(sc);}
SolverInstanceBase::Options* Gecode_SolverFactory::createOptions(void) { return new GecodeOptions; }
SolverInstanceBase* Gecode_SolverFactory::doCreateSI(std::ostream& log, SolverInstanceBase::Options* opt) { return new GecodeSolverInstance(log, opt);}
string Gecode_SolverFactory::getDescription(SolverInstanceBase::Options*) { string v = "Gecode solver plugin, compiled " __DATE__ ", using: Gecode version " + string(GECODE_VERSION); return v;}
string Gecode_SolverFactory::getVersion(SolverInstanceBase::Options*) { return string(GECODE_VERSION);}
bool Gecode_SolverFactory::processOption(SolverInstanceBase::Options* opt, int& i, std::vector<std::string>& argv) { GecodeOptions& _opt = static_cast<GecodeOptions&>(*opt); if (string(argv[i]) == "--allow-unbounded-vars") { _opt.allow_unbounded_vars = true; } else if (string(argv[i]) == "--only-range-domains") { _opt.only_range_domains = true; } else if (string(argv[i]) == "--sac") { _opt.sac = true; } else if (string(argv[i]) == "--shave") { _opt.shave = true; } else if (string(argv[i]) == "--pre-passes") { if (++i == argv.size()) return false; int passes = atoi(argv[i].c_str()); if (passes >= 0) _opt.pre_passes = passes; } else if (string(argv[i]) == "-a" || string(argv[i]) == "--all-solutions") { _opt.all_solutions = true; } else if (string(argv[i]) == "-n") { if (++i == argv.size()) return false; int n = atoi(argv[i].c_str()); if (n >= 0) _opt.n_solutions = n; } else if (string(argv[i]) == "--node") { if (++i == argv.size()) return false; int nodes = atoi(argv[i].c_str()); if (nodes >= 0) _opt.nodes = nodes; } else if (string(argv[i]) == "--fail") { if (++i == argv.size()) return false; int fails = atoi(argv[i].c_str()); if (fails >= 0) _opt.fails = fails; } else if (argv[i] == "--solver-time-limit" || argv[i] == "-t") { if (++i == argv.size()) return false; int time = atoi(argv[i].c_str()); if (time >= 0) _opt.time = time; } else if (string(argv[i]) == "-v" || string(argv[i]) == "--verbose-solving") { _opt.verbose = true; } else if (string(argv[i]) == "-s" || string(argv[i]) == "--solver-statistics") { _opt.statistics = true; } else { return false; } return true;}
void Gecode_SolverFactory::printHelp(ostream& os) { os << "Gecode solver plugin options:" << std::endl << " --allow-unbounded-vars" << std::endl << " give unbounded variables maximum bounds (this may lead to incorrect behaviour)" << std::endl << " --only-range-domains" << std::endl << " only tighten bounds" << std::endl << " --sac" << std ::endl << " singleton arc consistency" << std::endl << " --shave" << std::endl << " shave domains" << std::endl << " --pre-passes <n>" << std::endl << " n passes of sac/shaving, 0 for fixed point" << std::endl << " --node <n>" << std::endl << " node cutoff (0 = none, solution mode)" << std::endl << " --fail <f>" << std::endl << " failure cutoff (0 = none, solution mode)" << std::endl << " --time <ms>" << std::endl << " time (in ms) cutoff (0 = none, solution mode)" << std::endl << " -a, --all-solutions" << std::endl << " print intermediate solutions" << std::endl << " -n <sols>" << std::endl << " number of solutions" << std::endl << std::endl;}
class GecodeEngine {public: virtual FznSpace* next(void) = 0; virtual bool stopped(void) = 0; virtual ~GecodeEngine(void) {} virtual Gecode::Search::Statistics statistics(void) = 0;};
template <template <class> class Engine, template <class, template <class> class> class Meta>class MetaEngine : public GecodeEngine { Meta<FznSpace, Engine> e;
public: MetaEngine(FznSpace* s, Search::Options& o) : e(s, o) {} virtual FznSpace* next(void) { return e.next(); } virtual bool stopped(void) { return e.stopped(); } virtual Gecode::Search::Statistics statistics(void) { return e.statistics(); }};
GecodeSolverInstance::GecodeSolverInstance(std::ostream& log, SolverInstanceBase::Options* opt) : SolverInstanceImpl<GecodeSolver>(log, opt), _n_found_solutions(0), _current_space(new FznSpace()), _solution(NULL), engine(NULL) { registerConstraints(); _current_space->_solveType = MiniZinc::SolveI::SolveType::ST_SAT; // _flat = env.flat();}
GecodeSolverInstance::~GecodeSolverInstance(void) { delete engine; // delete _current_space; // delete _solution; // TODO: is this necessary?}
void GecodeSolverInstance::registerConstraint(std::string name, poster p) { std::stringstream ss; ss << "gecode_" << name; _constraintRegistry.add(ss.str(), p); std::stringstream ss2; ss2 << "fzn_" << name; _constraintRegistry.add(ss2.str(), p); // TODO: DO NOT USE global names directly _constraintRegistry.add(name, p);}
void GecodeSolverInstance::registerConstraints(void) { GCLock lock; registerConstraint("all_different_int", GecodeConstraints::p_distinct); registerConstraint("all_different_offset", GecodeConstraints::p_distinctOffset); registerConstraint("all_equal_int", GecodeConstraints::p_all_equal); registerConstraint("int_eq", GecodeConstraints::p_int_eq); registerConstraint("int_ne", GecodeConstraints::p_int_ne); registerConstraint("int_ge", GecodeConstraints::p_int_ge); registerConstraint("int_gt", GecodeConstraints::p_int_gt); registerConstraint("int_le", GecodeConstraints::p_int_le); registerConstraint("int_lt", GecodeConstraints::p_int_lt); registerConstraint("int_eq_reif", GecodeConstraints::p_int_eq_reif); registerConstraint("int_ne_reif", GecodeConstraints::p_int_ne_reif); registerConstraint("int_ge_reif", GecodeConstraints::p_int_ge_reif); registerConstraint("int_gt_reif", GecodeConstraints::p_int_gt_reif); registerConstraint("int_le_reif", GecodeConstraints::p_int_le_reif); registerConstraint("int_lt_reif", GecodeConstraints::p_int_lt_reif); registerConstraint("int_eq_imp", GecodeConstraints::p_int_eq_imp); registerConstraint("int_ne_imp", GecodeConstraints::p_int_ne_imp); registerConstraint("int_ge_imp", GecodeConstraints::p_int_ge_imp); registerConstraint("int_gt_imp", GecodeConstraints::p_int_gt_imp); registerConstraint("int_le_imp", GecodeConstraints::p_int_le_imp); registerConstraint("int_lt_imp", GecodeConstraints::p_int_lt_imp); registerConstraint("int_lin_eq", GecodeConstraints::p_int_lin_eq); registerConstraint("int_lin_eq_reif", GecodeConstraints::p_int_lin_eq_reif); registerConstraint("int_lin_eq_imp", GecodeConstraints::p_int_lin_eq_imp); registerConstraint("int_lin_le", GecodeConstraints::p_int_lin_le); registerConstraint("int_lin_le_reif", GecodeConstraints::p_int_lin_le_reif); registerConstraint("int_lin_le_imp", GecodeConstraints::p_int_lin_le_imp); registerConstraint("int_lin_lt", GecodeConstraints::p_int_lin_lt); registerConstraint("int_lin_lt_reif", GecodeConstraints::p_int_lin_lt_reif); registerConstraint("int_lin_lt_imp", GecodeConstraints::p_int_lin_lt_imp); registerConstraint("int_lin_ge", GecodeConstraints::p_int_lin_ge); registerConstraint("int_lin_ge_reif", GecodeConstraints::p_int_lin_ge_reif); registerConstraint("int_lin_ge_imp", GecodeConstraints::p_int_lin_ge_imp); registerConstraint("int_lin_gt", GecodeConstraints::p_int_lin_gt); registerConstraint("int_lin_gt_reif", GecodeConstraints::p_int_lin_gt_reif); registerConstraint("int_lin_gt_imp", GecodeConstraints::p_int_lin_gt_imp); // registerConstraint("int_plus", GecodeConstraints::p_int_plus); registerConstraint("int_sum", GecodeConstraints::p_int_sum); // registerConstraint("int_minus", GecodeConstraints::p_int_minus); registerConstraint("int_times", GecodeConstraints::p_int_times); registerConstraint("int_div", GecodeConstraints::p_int_div); registerConstraint("int_mod", GecodeConstraints::p_int_mod); registerConstraint("int_min", GecodeConstraints::p_int_min); registerConstraint("int_max", GecodeConstraints::p_int_max); registerConstraint("int_abs", GecodeConstraints::p_abs); registerConstraint("int_negate", GecodeConstraints::p_int_negate); registerConstraint("bool_eq", GecodeConstraints::p_bool_eq); registerConstraint("bool_eq_reif", GecodeConstraints::p_bool_eq_reif); registerConstraint("bool_eq_imp", GecodeConstraints::p_bool_eq_imp); registerConstraint("bool_not", GecodeConstraints::p_bool_ne); registerConstraint("bool_ne", GecodeConstraints::p_bool_ne); registerConstraint("bool_ne_reif", GecodeConstraints::p_bool_ne_reif); registerConstraint("bool_ne_imp", GecodeConstraints::p_bool_ne_imp); registerConstraint("bool_ge", GecodeConstraints::p_bool_ge); registerConstraint("bool_ge_reif", GecodeConstraints::p_bool_ge_reif); registerConstraint("bool_ge_imp", GecodeConstraints::p_bool_ge_imp); registerConstraint("bool_le", GecodeConstraints::p_bool_le); registerConstraint("bool_le_reif", GecodeConstraints::p_bool_le_reif); registerConstraint("bool_le_imp", GecodeConstraints::p_bool_le_imp); registerConstraint("bool_gt", GecodeConstraints::p_bool_gt); registerConstraint("bool_gt_reif", GecodeConstraints::p_bool_gt_reif); registerConstraint("bool_gt_imp", GecodeConstraints::p_bool_gt_imp); registerConstraint("bool_lt", GecodeConstraints::p_bool_lt); registerConstraint("bool_lt_reif", GecodeConstraints::p_bool_lt_reif); registerConstraint("bool_lt_imp", GecodeConstraints::p_bool_lt_imp); registerConstraint("bool_or", GecodeConstraints::p_bool_or); registerConstraint("bool_or_imp", GecodeConstraints::p_bool_or_imp); registerConstraint("bool_and", GecodeConstraints::p_bool_and); registerConstraint("forall", GecodeConstraints::p_forall); registerConstraint("bool_and_imp", GecodeConstraints::p_bool_and_imp); registerConstraint("bool_xor", GecodeConstraints::p_bool_xor); registerConstraint("bool_xor_imp", GecodeConstraints::p_bool_xor_imp); registerConstraint("array_bool_and", GecodeConstraints::p_array_bool_and); registerConstraint("array_bool_and_imp", GecodeConstraints::p_array_bool_and_imp); registerConstraint("array_bool_or", GecodeConstraints::p_array_bool_or); // registerConstraint("exists", GecodeConstraints::p_exists); registerConstraint("array_bool_or_imp", GecodeConstraints::p_array_bool_or_imp); registerConstraint("array_bool_xor", GecodeConstraints::p_array_bool_xor); registerConstraint("array_bool_xor_imp", GecodeConstraints::p_array_bool_xor_imp); registerConstraint("bool_clause", GecodeConstraints::p_array_bool_clause); registerConstraint("bool_clause_reif", GecodeConstraints::p_array_bool_clause_reif); registerConstraint("bool_clause_imp", GecodeConstraints::p_array_bool_clause_imp); registerConstraint("bool_left_imp", GecodeConstraints::p_bool_l_imp); registerConstraint("bool_right_imp", GecodeConstraints::p_bool_r_imp); // registerConstraint("bool_not", GecodeConstraints::p_bool_not); registerConstraint("array_int_element", GecodeConstraints::p_array_int_element); registerConstraint("array_var_int_element", GecodeConstraints::p_array_int_element); registerConstraint("array_bool_element", GecodeConstraints::p_array_bool_element); registerConstraint("array_var_bool_element", GecodeConstraints::p_array_bool_element); registerConstraint("bool2int", GecodeConstraints::p_bool2int); registerConstraint("int_in", GecodeConstraints::p_int_in); registerConstraint("int_in_reif", GecodeConstraints::p_int_in_reif); registerConstraint("int_in_imp", GecodeConstraints::p_int_in_imp); //#ifndef GECODE_HAS_SET_VARS registerConstraint("set_in", GecodeConstraints::p_int_in); registerConstraint("set_in_reif", GecodeConstraints::p_int_in_reif); registerConstraint("set_in_imp", GecodeConstraints::p_int_in_imp); //#endif
registerConstraint("array_int_lt", GecodeConstraints::p_array_int_lt); registerConstraint("array_int_lq", GecodeConstraints::p_array_int_lq); registerConstraint("array_bool_lt", GecodeConstraints::p_array_bool_lt); registerConstraint("array_bool_lq", GecodeConstraints::p_array_bool_lq); registerConstraint("count", GecodeConstraints::p_count); registerConstraint("count_reif", GecodeConstraints::p_count_reif); registerConstraint("count_imp", GecodeConstraints::p_count_imp); registerConstraint("at_least_int", GecodeConstraints::p_at_least); registerConstraint("at_most_int", GecodeConstraints::p_at_most); registerConstraint("bin_packing_load", GecodeConstraints::p_bin_packing_load); registerConstraint("global_cardinality", GecodeConstraints::p_global_cardinality); registerConstraint("global_cardinality_closed", GecodeConstraints::p_global_cardinality_closed); registerConstraint("global_cardinality_low_up", GecodeConstraints::p_global_cardinality_low_up); registerConstraint("global_cardinality_low_up_closed", GecodeConstraints::p_global_cardinality_low_up_closed); registerConstraint("array_int_minimum", GecodeConstraints::p_minimum); registerConstraint("array_int_maximum", GecodeConstraints::p_maximum); registerConstraint("minimum_arg_int", GecodeConstraints::p_minimum_arg); registerConstraint("maximum_arg_int", GecodeConstraints::p_maximum_arg); registerConstraint("regular", GecodeConstraints::p_regular); registerConstraint("sort", GecodeConstraints::p_sort); registerConstraint("inverse_offsets", GecodeConstraints::p_inverse_offsets); registerConstraint("increasing_int", GecodeConstraints::p_increasing_int); registerConstraint("increasing_bool", GecodeConstraints::p_increasing_bool); registerConstraint("decreasing_int", GecodeConstraints::p_decreasing_int); registerConstraint("decreasing_bool", GecodeConstraints::p_decreasing_bool); registerConstraint("table_int", GecodeConstraints::p_table_int); registerConstraint("table_bool", GecodeConstraints::p_table_bool); registerConstraint("cumulatives", GecodeConstraints::p_cumulatives); registerConstraint("among_seq_int", GecodeConstraints::p_among_seq_int); registerConstraint("among_seq_bool", GecodeConstraints::p_among_seq_bool);
registerConstraint("bool_lin_eq", GecodeConstraints::p_bool_lin_eq); registerConstraint("bool_lin_ne", GecodeConstraints::p_bool_lin_ne); registerConstraint("bool_lin_le", GecodeConstraints::p_bool_lin_le); registerConstraint("bool_lin_lt", GecodeConstraints::p_bool_lin_lt); registerConstraint("bool_lin_ge", GecodeConstraints::p_bool_lin_ge); registerConstraint("bool_lin_gt", GecodeConstraints::p_bool_lin_gt);
registerConstraint("bool_lin_eq_reif", GecodeConstraints::p_bool_lin_eq_reif); registerConstraint("bool_lin_eq_imp", GecodeConstraints::p_bool_lin_eq_imp); registerConstraint("bool_lin_ne_reif", GecodeConstraints::p_bool_lin_ne_reif); registerConstraint("bool_lin_ne_imp", GecodeConstraints::p_bool_lin_ne_imp); registerConstraint("bool_lin_le_reif", GecodeConstraints::p_bool_lin_le_reif); registerConstraint("bool_lin_le_imp", GecodeConstraints::p_bool_lin_le_imp); registerConstraint("bool_lin_lt_reif", GecodeConstraints::p_bool_lin_lt_reif); registerConstraint("bool_lin_lt_imp", GecodeConstraints::p_bool_lin_lt_imp); registerConstraint("bool_lin_ge_reif", GecodeConstraints::p_bool_lin_ge_reif); registerConstraint("bool_lin_ge_imp", GecodeConstraints::p_bool_lin_ge_imp); registerConstraint("bool_lin_gt_reif", GecodeConstraints::p_bool_lin_gt_reif); registerConstraint("bool_lin_gt_imp", GecodeConstraints::p_bool_lin_gt_imp);
registerConstraint("schedule_unary", GecodeConstraints::p_schedule_unary); registerConstraint("schedule_unary_optional", GecodeConstraints::p_schedule_unary_optional); registerConstraint("schedule_cumulative_optional", GecodeConstraints::p_cumulative_opt);
registerConstraint("circuit", GecodeConstraints::p_circuit); registerConstraint("circuit_cost_array", GecodeConstraints::p_circuit_cost_array); registerConstraint("circuit_cost", GecodeConstraints::p_circuit_cost); registerConstraint("nooverlap", GecodeConstraints::p_nooverlap); registerConstraint("precede", GecodeConstraints::p_precede); registerConstraint("nvalue", GecodeConstraints::p_nvalue); registerConstraint("among", GecodeConstraints::p_among); registerConstraint("member_int", GecodeConstraints::p_member_int); registerConstraint("member_int_reif", GecodeConstraints::p_member_int_reif); registerConstraint("member_bool", GecodeConstraints::p_member_bool); registerConstraint("member_bool_reif", GecodeConstraints::p_member_bool_reif);
#ifdef GECODE_HAS_FLOAT_VARS registerConstraint("int2float", GecodeConstraints::p_int2float); registerConstraint("float_abs", GecodeConstraints::p_float_abs); registerConstraint("float_sqrt", GecodeConstraints::p_float_sqrt); registerConstraint("float_eq", GecodeConstraints::p_float_eq); registerConstraint("float_eq_reif", GecodeConstraints::p_float_eq_reif); registerConstraint("float_le", GecodeConstraints::p_float_le); registerConstraint("float_le_reif", GecodeConstraints::p_float_le_reif); registerConstraint("float_lt", GecodeConstraints::p_float_lt); registerConstraint("float_lt_reif", GecodeConstraints::p_float_lt_reif); registerConstraint("float_ne", GecodeConstraints::p_float_ne); registerConstraint("float_times", GecodeConstraints::p_float_times); registerConstraint("float_div", GecodeConstraints::p_float_div); registerConstraint("float_plus", GecodeConstraints::p_float_plus); registerConstraint("float_max", GecodeConstraints::p_float_max); registerConstraint("float_min", GecodeConstraints::p_float_min); registerConstraint("float_lin_eq", GecodeConstraints::p_float_lin_eq); registerConstraint("float_lin_eq_reif", GecodeConstraints::p_float_lin_eq_reif); registerConstraint("float_lin_le", GecodeConstraints::p_float_lin_le); registerConstraint("float_lin_le_reif", GecodeConstraints::p_float_lin_le_reif);#endif#ifdef GECODE_HAS_MPFR registerConstraint("float_acos", GecodeConstraints::p_float_acos); registerConstraint("float_asin", GecodeConstraints::p_float_asin); registerConstraint("float_atan", GecodeConstraints::p_float_atan); registerConstraint("float_cos", GecodeConstraints::p_float_cos); registerConstraint("float_exp", GecodeConstraints::p_float_exp); registerConstraint("float_ln", GecodeConstraints::p_float_ln); registerConstraint("float_log10", GecodeConstraints::p_float_log10); registerConstraint("float_log2", GecodeConstraints::p_float_log2); registerConstraint("float_sin", GecodeConstraints::p_float_sin); registerConstraint("float_tan", GecodeConstraints::p_float_tan);#endif#ifdef GECODE_HAS_SET_VARS registerConstraint("set_eq", GecodeConstraints::p_set_eq); registerConstraint("set_le", GecodeConstraints::p_set_le); registerConstraint("set_lt", GecodeConstraints::p_set_lt); registerConstraint("equal", GecodeConstraints::p_set_eq); registerConstraint("set_ne", GecodeConstraints::p_set_ne); registerConstraint("set_union", GecodeConstraints::p_set_union); registerConstraint("array_set_element", GecodeConstraints::p_array_set_element); registerConstraint("array_var_set_element", GecodeConstraints::p_array_set_element); registerConstraint("set_intersect", GecodeConstraints::p_set_intersect); registerConstraint("set_diff", GecodeConstraints::p_set_diff); registerConstraint("set_symdiff", GecodeConstraints::p_set_symdiff); registerConstraint("set_subset", GecodeConstraints::p_set_subset); registerConstraint("set_superset", GecodeConstraints::p_set_superset); registerConstraint("set_card", GecodeConstraints::p_set_card); registerConstraint("set_in", GecodeConstraints::p_set_in); registerConstraint("set_eq_reif", GecodeConstraints::p_set_eq_reif); registerConstraint("set_le_reif", GecodeConstraints::p_set_le_reif); registerConstraint("set_lt_reif", GecodeConstraints::p_set_lt_reif); registerConstraint("equal_reif", GecodeConstraints::p_set_eq_reif); registerConstraint("set_ne_reif", GecodeConstraints::p_set_ne_reif); registerConstraint("set_subset_reif", GecodeConstraints::p_set_subset_reif); registerConstraint("set_superset_reif", GecodeConstraints::p_set_superset_reif); registerConstraint("set_in_reif", GecodeConstraints::p_set_in_reif); registerConstraint("set_in_imp", GecodeConstraints::p_set_in_imp); registerConstraint("disjoint", GecodeConstraints::p_set_disjoint); registerConstraint("link_set_to_booleans", GecodeConstraints::p_link_set_to_booleans); registerConstraint("array_set_union", GecodeConstraints::p_array_set_union); registerConstraint("array_set_partition", GecodeConstraints::p_array_set_partition); registerConstraint("set_convex", GecodeConstraints::p_set_convex); registerConstraint("array_set_seq", GecodeConstraints::p_array_set_seq); registerConstraint("array_set_seq_union", GecodeConstraints::p_array_set_seq_union); registerConstraint("array_set_element_union", GecodeConstraints::p_array_set_element_union); registerConstraint("array_set_element_intersect", GecodeConstraints::p_array_set_element_intersect); registerConstraint("array_set_element_intersect_in", GecodeConstraints::p_array_set_element_intersect_in); registerConstraint("array_set_element_partition", GecodeConstraints::p_array_set_element_partition); registerConstraint("int_set_channel", GecodeConstraints::p_int_set_channel); registerConstraint("range", GecodeConstraints::p_range); registerConstraint("set_weights", GecodeConstraints::p_weights); registerConstraint("inverse_set", GecodeConstraints::p_inverse_set); registerConstraint("precede_set", GecodeConstraints::p_precede_set);#endif}
inline bool GecodeSolverInstance::valueWithinBounds(double b) { long long int bo = round_to_longlong(b); return bo >= Gecode::Int::Limits::min && bo <= Gecode::Int::Limits::max;}
void GecodeSolverInstance::addConstraint(const std::vector<BytecodeProc>& bs, Constraint* c) { const std::string& name = bs[c->pred()].name;
if (name == "solve_this") { IntVal solve_mode = c->arg(0).toIntVal(); Val obj = c->arg(1); SolveI* si; if (solve_mode != 1) { _current_space->_optVarIsInt = true; _current_space->_solveType = solve_mode == 1 ? MiniZinc::SolveI::SolveType::ST_MIN : MiniZinc::SolveI::SolveType::ST_MAX; GecodeVariable var = resolveVar(obj.toVar()); IntVar intVar = var.intVar(_current_space); for (unsigned int i = 0; i < _current_space->iv.size(); i++) { if (_current_space->iv[i].varimp() == intVar.varimp()) { _current_space->_optVarIdx = i; break; } } GCLock lock; solveExpr = new Id(Location().introduce(), obj.timestamp(), nullptr); } // TODO: Use correct search heuristic /* if (c->size() == 5) { Val search_a = c->arg(2); IntVal var_sel = c->arg(3).toIntVal(); IntVal val_sel = c->arg(4).toIntVal(); if (search_a.isVec() && search_a.size() > 0 && var_sel > 0 && val_sel > 0) { Expression* search_vars = val_to_expr(Type::varint(1), search_a); ASTString var_sel_s(var_sel == 1 ? "input_order" : "first_fail"); ASTString val_sel_s(val_sel == 1 ? "indomain_min" : "indomain_max"); Id* var_sel_id = new Id(Location().introduce(), var_sel_s, nullptr); Id* val_sel_id = new Id(Location().introduce(), val_sel_s, nullptr); Id* complete_id = new Id(Location().introduce(), "complete", nullptr); si->ann().add(new Call(Location().introduce(), ASTString("int_search"), {search_vars, var_sel_id, val_sel_id, complete_id})); } */ return; } _constraintRegistry.post(name, c);}void GecodeSolverInstance::addVariable(Variable* var, bool isOutput) { GecodeConstraints::p_mk_intvar(*this, var, isOutput);}
void GecodeSolverInstance::processFlatZinc(void) { return; assert(false); // GecodeOptions& _opt = static_cast<GecodeOptions&>(*_options); // _only_range_domains = _opt.only_range_domains; // _run_sac = _opt.sac; // _run_shave = _opt.shave; // _pre_passes = _opt.pre_passes; // _print_stats = _opt.statistics; // _all_solutions = _opt.all_solutions; // _n_max_solutions = _opt.n_solutions; // _allow_unbounded_vars = _opt.allow_unbounded_vars; // _current_space = new FznSpace();
// // iterate over VarDecls of the flat model and create variables // for (VarDeclIterator it = _flat->begin_vardecls(); it != _flat->end_vardecls(); ++it) { // if (!it->removed() && it->e()->type().isvar()) { // // check if it has an output-annotation // VarDecl* vd = it->e(); // if(!vd->ann().isEmpty()) { // if(vd->ann().containsCall(constants().ann.output_array.aststr())) { // ArrayLit* al = vd->e()->dyn_cast<ArrayLit>(); // if(!al) { // std::stringstream ssm; // ssm << "GecodeSolverInstance::processFlatZinc: Error: Array without right hand // side: " << *vd->id() << std::endl; throw InternalError(ssm.str()); // } // for(int i=0; i<al->size(); i++) { // if(Id* id = (*al)[i]->dyn_cast<Id>()) { // GecodeVariable var = resolveVar(id); // if(var.isint()) { // _current_space->iv_introduced[var.index()] = false; // } else if(var.isbool()) { // _current_space->bv_introduced[var.index()] = false; // } else if(var.isfloat()) { // _current_space->fv_introduced[var.index()] = false; // } else if(var.isset()) { // _current_space->sv_introduced[var.index()] = false; // } // } // } // _varsWithOutput.push_back(vd); // } else if (vd->ann().contains(constants().ann.output_var)) { // _varsWithOutput.push_back(vd); // } // }
// if (it->e()->type().dim() != 0) { // // we ignore arrays - all their elements are defined // continue; // } // MiniZinc::TypeInst* ti = it->e()->ti(); // bool isDefined, isIntroduced = false;
// if(vd->type().isint()) { // if(!it->e()->e()) { // if there is no initialisation expression // Expression* domain = ti->domain(); // if(domain) { // IntVar intVar(*this->_current_space, arg2intset(_env.envi(), domain)); // _current_space->iv.push_back(intVar); // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::INT_TYPE, // _current_space->iv.size()-1)); // } else { // if(_allow_unbounded_vars) { // IntVar intVar(*this->_current_space, Gecode::Int::Limits::min, // Gecode::Int::Limits::max); _current_space->iv.push_back(intVar); // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::INT_TYPE, // _current_space->iv.size()-1)); std::cerr << "% // GecodeSolverInstance::processFlatZinc: Warning: Unbounded variable " << // *vd->id() << " given maximum integer bounds, this may be incorrect: " << // std::endl; // } else { // std::stringstream ssm; // ssm << "GecodeSolverInstance::processFlatZinc: Error: Unbounded variable: " // << *vd->id() << ", rerun with --allow-unbounded-vars to add arbitrary // bounds."<< std::endl; throw InternalError(ssm.str()); // } // } // } else { // there is an initialisation expression // Expression* init = it->e()->e(); // if (init->isa<Id>() || init->isa<ArrayAccess>()) { // // root->iv[root->intVarCount++] = root->iv[*(int*)resolveVar(init)]; // GecodeVariable var = resolveVar(init); // assert(var.isint()); // _current_space->iv.push_back(var.intVar(_current_space)); // insertVar(it->e()->id(), var); // } else { // double il = init->cast<IntLit>()->v().toInt(); // if(valueWithinBounds(il)) { // IntVar intVar(*this->_current_space, il, il); // _current_space->iv.push_back(intVar); // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::INT_TYPE, // _current_space->iv.size()-1)); // } else { // std::stringstream ssm; // ssm << "GecodeSolverInstance::processFlatZinc: Error: Unsafe value for // Gecode: " << il << std::endl; throw InternalError(ssm.str()); // } // } // } // isIntroduced = it->e()->introduced() || (MiniZinc::getAnnotation(it->e()->ann(), // constants().ann.is_introduced.str()) != NULL); // _current_space->iv_introduced.push_back(isIntroduced); // isDefined = MiniZinc::getAnnotation(it->e()->ann(), // constants().ann.is_defined_var->str().str()) != NULL; // _current_space->iv_defined.push_back(isDefined);
// } else if(vd->type().isbool()) { // double lb=0, ub=1; // if(!it->e()->e()) { // there is NO initialisation expression // Expression* domain = ti->domain(); // if(domain) { // IntBounds ib = compute_int_bounds(_env.envi(), domain); // lb = ib.l.toInt(); // ub = ib.u.toInt(); // } else { // lb = 0; // ub = 1; // } // BoolVar boolVar(*this->_current_space, lb, ub); // _current_space->bv.push_back(boolVar); // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::BOOL_TYPE, // _current_space->bv.size()-1)); // } else { // there is an initialisation expression // Expression* init = it->e()->e(); // if (init->isa<Id>() || init->isa<ArrayAccess>()) { // // root->bv[root->boolVarCount++] = root->bv[*(int*)resolveVar(init)]; // //int index = *(int*) resolveVar(init); // GecodeVariable var = resolveVar(init); // assert(var.isbool()); // _current_space->bv.push_back(var.boolVar(_current_space)); // insertVar(it->e()->id(), var); // } else { // double b = (double) init->cast<BoolLit>()->v(); // BoolVar boolVar(*this->_current_space, b, b); // _current_space->bv.push_back(boolVar); // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::BOOL_TYPE, // _current_space->bv.size()-1)); // } // } // isIntroduced = it->e()->introduced() || (MiniZinc::getAnnotation(it->e()->ann(), // constants().ann.is_introduced.str()) != NULL); // _current_space->bv_introduced.push_back(isIntroduced); // isDefined = MiniZinc::getAnnotation(it->e()->ann(), // constants().ann.is_defined_var->str().str()) != NULL; // _current_space->bv_defined.push_back(isDefined); // #ifdef GECODE_HAS_FLOAT_VARS // } else if(vd->type().isfloat()) { // if(it->e()->e() == NULL) { // there is NO initialisation expression // Expression* domain = ti->domain(); // double lb, ub; // if (domain) { // FloatBounds fb = compute_float_bounds(_env.envi(), vd->id()); // lb = fb.l.toDouble(); // ub = fb.u.toDouble(); // } else { // if(_allow_unbounded_vars) { // lb = Gecode::Float::Limits::min; // ub = Gecode::Float::Limits::max; // std::cerr << "%% GecodeSolverInstance::processFlatZinc: Warning: Unbounded // variable " << *vd->id() << " given maximum float bounds, this may be // incorrect: " << std::endl; // } else { // std::stringstream ssm; // ssm << "GecodeSolverInstance::processFlatZinc: Error: Unbounded variable: " // << *vd->id() << ", rerun with --allow-unbounded-vars to add arbitrary // bounds."<< std::endl; throw InternalError(ssm.str()); // } // } // FloatVar floatVar(*this->_current_space, lb, ub); // _current_space->fv.push_back(floatVar); // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::FLOAT_TYPE, // _current_space->fv.size()-1)); // } else { // Expression* init = it->e()->e(); // if (init->isa<Id>() || init->isa<ArrayAccess>()) { // // root->fv[root->floatVarCount++] = root->fv[*(int*)resolveVar(init)]; // GecodeVariable var = resolveVar(init); // assert(var.isfloat()); // _current_space->fv.push_back(var.floatVar(_current_space)); // insertVar(it->e()->id(), var); // } else { // double il = init->cast<FloatLit>()->v().toDouble(); // FloatVar floatVar(*this->_current_space, il, il); // _current_space->fv.push_back(floatVar); // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::FLOAT_TYPE, // _current_space->fv.size()-1)); // } // } // isIntroduced = it->e()->introduced() || (MiniZinc::getAnnotation(it->e()->ann(), // constants().ann.is_introduced.str()) != NULL); // _current_space->fv_introduced.push_back(isIntroduced); // isDefined = MiniZinc::getAnnotation(it->e()->ann(), // constants().ann.is_defined_var->str().str()) != NULL; // _current_space->fv_defined.push_back(isDefined); // #endif // #ifdef GECODE_HAS_SET_VARS // } else if(vd->type().isintset()) { // Expression* domain = ti->domain(); // auto d = arg2intset(_env.envi(), domain); // SetVar setVar(*this->_current_space, Gecode::IntSet::empty, d); // _current_space->sv.push_back(setVar); // isIntroduced = it->e()->introduced() || (MiniZinc::getAnnotation(it->e()->ann(), // constants().ann.is_introduced.str()) != NULL); // _current_space->sv_introduced.push_back(isIntroduced); // isDefined = MiniZinc::getAnnotation(it->e()->ann(), // constants().ann.is_defined_var->str().str()) != NULL; // _current_space->sv_defined.push_back(isDefined); // insertVar(it->e()->id(), GecodeVariable(GecodeVariable::SET_TYPE, // _current_space->sv.size()-1)); // #endif // } else { // std::stringstream ssm; // ssm << "Type " << *ti << " is currently not supported by Gecode." << std::endl; // throw InternalError(ssm.str()); // } // } // end if it is a variable // } // end for all var decls
// // post the constraints // for (ConstraintIterator it = _flat->begin_constraints(); it != _flat->end_constraints(); // ++it) { // if(!it->removed()) { // if (Call* c = it->e()->dyn_cast<Call>()) { // // _constraintRegistry.post(c); // } // } // }
// // objective // SolveI* si = _flat->solveItem(); // _current_space->_solveType = si->st(); // if(si->e()) { // _current_space->_optVarIsInt = (si->e()->type().isvarint()); // if(Id* id = si->e()->dyn_cast<Id>()) { // if (si->e()->type().isvar()) { // GecodeVariable var = resolveVar(id->decl()); // if(_current_space->_optVarIsInt) { // IntVar intVar = var.intVar(_current_space); // for(unsigned int i=0; i<_current_space->iv.size(); i++) { // if(_current_space->iv[i].varimp()==intVar.varimp()) { // _current_space->_optVarIdx = i; // break; // } // } // assert(_current_space->_optVarIdx >= 0); // #ifdef GECODE_HAS_FLOAT_VARS // } else { // FloatVar floatVar = var.floatVar(_current_space); // for(unsigned int i=0; i<_current_space->fv.size(); i++) { // if(_current_space->fv[i].varimp()==floatVar.varimp()) { // _current_space->_optVarIdx = i; // break; // } // } // assert(_current_space->_optVarIdx >= 0); // #endif // } // } // } // else { // the solve expression has to be a variable/id // assert(false); // }
// }
// //std::cout << "DEBUG: at end of processFlatZinc: " << std::endl // // << "iv has " << _current_space->iv.size() << " variables " << std::endl // // << "bv has " << _current_space->bv.size() << " variables " << std::endl // // << "fv has " << _current_space->fv.size() << " variables " << std::endl // // << "sv has " << _current_space->sv.size() << " variables " << std::endl;}
Gecode::IntArgs GecodeSolverInstance::arg2intargs(Expression* arg, int offset) { if (!arg->isa<Id>() && !arg->isa<ArrayLit>()) { std::stringstream ssm; ssm << "Invalid argument in arg2intargs: " << *arg; ssm << ". Expected Id or ArrayLit."; throw InternalError(ssm.str()); } ArrayLit* a = arg->isa<Id>() ? arg->cast<Id>()->decl()->e()->cast<ArrayLit>() : arg->cast<ArrayLit>(); IntArgs ia(a->size() + offset); for (int i = offset; i--;) ia[i] = 0; for (int i = a->size(); i--;) { ia[i + offset] = (*a)[i]->cast<IntLit>()->v().toInt(); } return ia;}
Gecode::IntArgs GecodeSolverInstance::arg2intargs(const Val& vec, int offset) { if (!vec.isVec()) { std::stringstream ssm; ssm << "Invalid argument in arg2intargs: " << vec.toString(); ssm << ". Expected Array."; throw InternalError(ssm.str()); } assert(!vec.toVec()->hasIndexSet()); IntArgs ia(vec.size() + offset); for (int i = offset; i--;) ia[i] = 0; for (int i = vec.size(); i--;) { ia[i + offset] = vec[i].toInt(); } return ia;}
Gecode::IntArgs GecodeSolverInstance::arg2boolargs(Expression* arg, int offset) { if (!arg->isa<Id>() && !arg->isa<ArrayLit>()) { std::stringstream ssm; ssm << "Invalid argument in arg2boolargs: " << *arg; ssm << ". Expected Id or ArrayLit."; throw InternalError(ssm.str()); } ArrayLit* a = arg->isa<Id>() ? arg->cast<Id>()->decl()->e()->cast<ArrayLit>() : arg->cast<ArrayLit>(); IntArgs ia(a->size() + offset); for (int i = offset; i--;) ia[i] = 0; for (int i = a->size(); i--;) ia[i + offset] = (*a)[i]->cast<BoolLit>()->v(); return ia;}
Gecode::IntArgs GecodeSolverInstance::arg2boolargs(const Val& vec, int offset) { if (!vec.isVec()) { std::stringstream ssm; ssm << "Invalid argument in arg2intargs: " << vec.toString(); ssm << ". Expected Vec."; throw InternalError(ssm.str()); } assert(!vec.toVec()->hasIndexSet()); IntArgs ia(vec.size() + offset); for (int i = offset; i--;) ia[i] = 0; for (int i = vec.size(); i--;) { ia[i + offset] = vec[i].toInt(); } return ia;}
class GecodeRangeIter {public: GecodeSolverInstance& si; IntSetRanges& isr; GecodeRangeIter(GecodeSolverInstance& gsi, IntSetRanges& isr0) : si(gsi), isr(isr0) {} int min(void) const { long long int val = isr.min().toInt(); if (si.valueWithinBounds(val)) { return (int)val; } else { std::stringstream ssm; ssm << "GecodeRangeIter::min: Error: " << val << " outside 32-bit int." << std::endl; throw InternalError(ssm.str()); } } int max(void) const { long long int val = isr.max().toInt(); if (si.valueWithinBounds(val)) { return (int)val; } else { std::stringstream ssm; ssm << "GecodeRangeIter::max: Error: " << val << " outside 32-bit int." << std::endl; throw InternalError(ssm.str()); } } int width(void) const { return isr.width().toInt(); } bool operator()(void) { return isr(); } void operator++(void) { ++isr; }};
Gecode::IntSet GecodeSolverInstance::arg2intset(EnvI& envi, Expression* arg) { GCLock lock; IntSetVal* isv = eval_intset(envi, arg); IntSetRanges isr(isv); GecodeRangeIter isr_g(*this, isr); IntSet d(isr_g); return d;}Gecode::IntSet GecodeSolverInstance::arg2intset(const Val& sl) { GCLock lock; assert(sl.isVec()); assert(sl.size() >= 2 && sl.size() % 2 == 0); std::vector<IntSetVal::Range> ranges; for (int i = 0; i < sl.size(); i += 2) { ranges.emplace_back(sl[i].toIntVal(), sl[i + 1].toIntVal()); } IntSetVal* isv = IntSetVal::a(ranges); IntSetRanges isr(isv); GecodeRangeIter isr_g(*this, isr); IntSet d(isr_g); return d;}IntSetArgs GecodeSolverInstance::arg2intsetargs(EnvI& envi, Expression* arg, int offset) { ArrayLit* a = arg2arraylit(arg); if (a->size() == 0) { IntSetArgs emptyIa(0); return emptyIa; } IntSetArgs ia(a->size() + offset); for (int i = offset; i--;) ia[i] = IntSet::empty; for (int i = a->size(); i--;) { ia[i + offset] = arg2intset(envi, (*a)[i]); } return ia;}
Gecode::IntVarArgs GecodeSolverInstance::arg2intvarargs(const Val& vec, int offset) { assert(!vec.toVec()->hasIndexSet()); if (vec.size() == 0) { IntVarArgs emptyIa(0); return emptyIa; } IntVarArgs ia(vec.size() + offset); for (int i = offset; i--;) ia[i] = IntVar(*this->_current_space, 0, 0); for (int i = vec.size(); i--;) { const Val& val = Val::follow_alias(vec[i]); if (val.isVar()) { // ia[i+offset] = _current_space->iv[*(int*)resolveVar(getVarDecl(e))]; GecodeSolver::Variable var = resolveVar(val.toVar()); if (var.isbool()) { // TODO: We should cache the channeling IntVar intVar(*_current_space, 0, 1); _current_space->iv.push_back(intVar); // insertVar(def, GecodeVariable(GecodeVariable::INT_TYPE, // _current_space->iv.size()-1)); _current_space->iv_introduced.push_back(true); _current_space->iv_defined.push_back(true); channel(*_current_space, intVar, var.boolVar(_current_space), MZ_ICL_DEF); ia[i + offset] = intVar; } else { assert(var.isint()); Gecode::IntVar v = var.intVar(_current_space); ia[i + offset] = v; } } else { long long int value = val.toInt(); if (valueWithinBounds(value)) { IntVar iv(*this->_current_space, value, value); ia[i + offset] = iv; } else { std::stringstream ssm; ssm << "GecodeSolverInstance::arg2intvarargs Error: " << value << " outside 32-bit int." << std::endl; throw InternalError(ssm.str()); } } } return ia;}Gecode::IntVarArgs GecodeSolverInstance::arg2intvarargs(Expression* arg, int offset) { ArrayLit* a = arg2arraylit(arg); if (a->size() == 0) { IntVarArgs emptyIa(0); return emptyIa; } IntVarArgs ia(a->size() + offset); for (int i = offset; i--;) ia[i] = IntVar(*this->_current_space, 0, 0); for (int i = a->size(); i--;) { Expression* e = (*a)[i]; if (e->type().isvar()) { // ia[i+offset] = _current_space->iv[*(int*)resolveVar(getVarDecl(e))]; GecodeSolver::Variable var = resolveVar(getVarDecl(e)); assert(var.isint()); Gecode::IntVar v = var.intVar(_current_space); ia[i + offset] = v; } else { long long int value = e->cast<IntLit>()->v().toInt(); if (valueWithinBounds(value)) { IntVar iv(*this->_current_space, value, value); ia[i + offset] = iv; } else { std::stringstream ssm; ssm << "GecodeSolverInstance::arg2intvarargs Error: " << value << " outside 32-bit int." << std::endl; throw InternalError(ssm.str()); } } } return ia;}
Gecode::BoolVarArgs GecodeSolverInstance::arg2boolvarargs(const Val& vec, int offset, int siv) { assert(!vec.toVec()->hasIndexSet()); if (vec.size() == 0) { BoolVarArgs emptyIa(0); return emptyIa; } BoolVarArgs ia(vec.size() + offset - ((siv < 0 || siv >= vec.size()) ? 0 : 1)); for (int i = offset; i--;) ia[i] = BoolVar(*this->_current_space, 0, 0); for (int i = 0; i < static_cast<int>(vec.size()); i++) { if (i == siv) continue; const Val& v = Val::follow_alias(vec[i]); if (v.isVar()) { GecodeVariable var = resolveVar(v.toVar()); if (var.isbool()) { // assert(var.isbool()); ia[offset++] = var.boolVar(_current_space); } else if (var.hasBoolAlias()) { ia[offset++] = _current_space->bv[var.boolAliasIndex()]; } else { std::stringstream ssm; ssm << "expected bool-var or alias int var instead of " << v.toString(); throw InternalError(ssm.str()); } } else { long long int i = v.toInt(); if (i >= 0 && i <= 1) { BoolVar iv(*this->_current_space, i, i); ia[offset++] = iv; } else { std::stringstream ssm; ssm << "Expected bool literal instead of: " << v.toString(); throw new InternalError(ssm.str()); } } } return ia;}Gecode::BoolVarArgs GecodeSolverInstance::arg2boolvarargs(Expression* arg, int offset, int siv) { ArrayLit* a = arg2arraylit(arg); if (a->length() == 0) { BoolVarArgs emptyIa(0); return emptyIa; } BoolVarArgs ia(a->length() + offset - (siv == -1 ? 0 : 1)); for (int i = offset; i--;) ia[i] = BoolVar(*this->_current_space, 0, 0); for (int i = 0; i < static_cast<int>(a->length()); i++) { if (i == siv) continue; Expression* e = (*a)[i]; if (e->type().isvar()) { GecodeVariable var = resolveVar(getVarDecl(e)); if (e->type().isvarbool()) { assert(var.isbool()); ia[offset++] = var.boolVar(_current_space); } else if (e->type().isvarint() && var.hasBoolAlias()) { ia[offset++] = _current_space->bv[var.boolAliasIndex()]; } else { std::stringstream ssm; ssm << "expected bool-var or alias int var instead of " << *e << " with type " << e->type().toString(env().envi()); throw InternalError(ssm.str()); } } else { if (BoolLit* bl = e->dyn_cast<BoolLit>()) { bool value = bl->v(); BoolVar iv(*this->_current_space, value, value); ia[offset++] = iv; } else { std::stringstream ssm; ssm << "Expected bool literal instead of: " << *e; throw new InternalError(ssm.str()); } } } return ia;}
Gecode::BoolVar GecodeSolverInstance::reifyVar(const Variable* var) { BoolVar boolVar(*_current_space, 0, 1); _current_space->bv.push_back(boolVar); insertVar(var, GecodeVariable(GecodeVariable::BOOL_TYPE, _current_space->bv.size() - 1)); _current_space->bv_introduced.push_back(true); _current_space->bv_defined.push_back(true); return boolVar;}
Gecode::BoolVar GecodeSolverInstance::arg2boolvar(const Val& v) { Val _v = Val::follow_alias(v); BoolVar x0; if (_v.isVar()) { // x0 = _current_space->bv[*(int*)resolveVar(getVarDecl(e))]; GecodeVariable var = resolveVar(_v.toVar()); assert(var.isbool()); x0 = var.boolVar(_current_space); } else { long long int i = _v.toInt(); if (i < 0 || i > 1) { std::stringstream ssm; ssm << "Expected bool literal instead of: " << _v.toString(); throw new InternalError(ssm.str()); } else { x0 = BoolVar(*this->_current_space, i, i); } } return x0;}Gecode::BoolVar GecodeSolverInstance::arg2boolvar(Expression* e) { BoolVar x0; if (e->type().isvar()) { // x0 = _current_space->bv[*(int*)resolveVar(getVarDecl(e))]; GecodeVariable var = resolveVar(getVarDecl(e)); assert(var.isbool()); x0 = var.boolVar(_current_space); } else { if (BoolLit* bl = e->dyn_cast<BoolLit>()) { x0 = BoolVar(*this->_current_space, bl->v(), bl->v()); } else { std::stringstream ssm; ssm << "Expected bool literal instead of: " << *e; throw new InternalError(ssm.str()); } } return x0;}
Gecode::IntVar GecodeSolverInstance::arg2intvar(Expression* e) { IntVar x0; if (e->type().isvar()) { // x0 = _current_space->iv[*(int*)resolveVar(getVarDecl(e))]; GecodeVariable var = resolveVar(getVarDecl(e)); assert(var.isint()); x0 = var.intVar(_current_space); } else { IntVal i; if (IntLit* il = e->dyn_cast<IntLit>()) i = il->v().toInt(); else if (BoolLit* bl = e->dyn_cast<BoolLit>()) i = bl->v(); else { std::stringstream ssm; ssm << "Expected bool or int literal instead of: " << *e; throw InternalError(ssm.str()); } x0 = IntVar(*this->_current_space, i.toInt(), i.toInt()); } return x0;}Gecode::IntVar GecodeSolverInstance::arg2intvar(const Val& val) { IntVar x0; Val _val = Val::follow_alias(val); if (_val.isVar()) { Variable* v = _val.toVar(); // x0 = _current_space->iv[*(int*)resolveVar(getVarDecl(e))]; GecodeVariable var = resolveVar(v); if (var.isbool()) { // TODO: We should cache the channeling IntVar intVar(*_current_space, 0, 1); _current_space->iv.push_back(intVar); // insertVar(def, GecodeVariable(GecodeVariable::INT_TYPE, // _current_space->iv.size()-1)); _current_space->iv_introduced.push_back(true); _current_space->iv_defined.push_back(true); channel(*_current_space, intVar, var.boolVar(_current_space), MZ_ICL_DEF); x0 = intVar; } else { assert(var.isint()); x0 = var.intVar(_current_space); } } else { IntVal i = _val.toIntVal(); x0 = IntVar(*this->_current_space, i.toInt(), i.toInt()); } return x0;}
ArrayLit* GecodeSolverInstance::arg2arraylit(Expression* arg) { ArrayLit* a; if (Id* id = arg->dyn_cast<Id>()) { VarDecl* vd = id->decl(); if (vd->e()) { a = vd->e()->cast<ArrayLit>(); } else { std::vector<Expression*>* array = arrayMap[vd]; std::vector<Expression*> ids; for (unsigned int i = 0; i < array->size(); i++) ids.push_back(((*array)[i])->cast<VarDecl>()->id()); a = new ArrayLit(vd->loc(), ids); } } else if (ArrayLit* al = arg->dyn_cast<ArrayLit>()) { a = al; } else { std::stringstream ssm; ssm << "Invalid argument in arg2arrayLit: " << *arg; ssm << ". Expected Id or ArrayLit."; throw new InternalError(ssm.str()); } return a;}
bool GecodeSolverInstance::isBoolArray(const Val& arr, int& singleInt) { assert(!arr.toVec()->hasIndexSet()); singleInt = -1; if (arr.size() == 0) return true; for (int i = arr.size(); i--;) { const Val& val = Val::follow_alias(arr[i]); if (val.isInt() && val >= 0 && val <= 1) { continue; } else if (val.isVar()) { if (val.lb() >= Val(int(0)) && val.ub() <= Val(int(1))) { continue; } return false; // TODO: Check variable domain // GecodeVariable var = resolveVar(getVarDecl((*a)[i])); // if (var.hasBoolAlias()) { // singleInt = var.boolAliasIndex(); // } // else { // } } else { return false; } } return singleInt == -1 || arr.size() > 1;}bool GecodeSolverInstance::isBoolArray(ArrayLit* a, int& singleInt) { singleInt = -1; if (a->length() == 0) return true; for (int i = a->length(); i--;) { if ((*a)[i]->type().isbool()) { continue; } else if (((*a)[i])->type().isvarint()) { GecodeVariable var = resolveVar(getVarDecl((*a)[i])); if (var.hasBoolAlias()) { if (singleInt != -1) { return false; } singleInt = var.boolAliasIndex(); } else return false; } else { return false; } } return singleInt == -1 || a->length() > 1;}#ifdef GECODE_HAS_SET_VARSSetVar GecodeSolverInstance::arg2setvar(Expression* e) { SetVar x0; if (!e->type().isvar()) { Gecode::IntSet d = arg2intset(_env.envi(), e); x0 = SetVar(*this->_current_space, d, d); } else { GecodeVariable var = resolveVar(getVarDecl(e)); assert(var.isset()); x0 = var.setVar(_current_space); } return x0;}Gecode::SetVarArgs GecodeSolverInstance::arg2setvarargs(Expression* arg, int offset, int doffset, const Gecode::IntSet& od) { ArrayLit* a = arg2arraylit(arg); SetVarArgs ia(a->size() + offset); for (int i = offset; i--;) { Gecode::IntSet d = i < doffset ? od : Gecode::IntSet::empty; ia[i] = SetVar(*this->_current_space, d, d); } for (int i = a->size(); i--;) { ia[i + offset] = arg2setvar((*a)[i]); } return ia;}#endif#ifdef GECODE_HAS_FLOAT_VARSGecode::FloatValArgs GecodeSolverInstance::arg2floatargs(Expression* arg, int offset) { assert(arg->isa<Id>() || arg->isa<ArrayLit>()); ArrayLit* a = arg->isa<Id>() ? arg->cast<Id>()->decl()->e()->cast<ArrayLit>() : arg->cast<ArrayLit>(); FloatValArgs fa(a->size() + offset); for (int i = offset; i--;) fa[i] = 0.0; for (int i = a->size(); i--;) fa[i + offset] = (*a)[i]->cast<FloatLit>()->v().toDouble(); return fa;}
Gecode::FloatVar GecodeSolverInstance::arg2floatvar(Expression* e) { FloatVar x0; if (e->type().isvar()) { GecodeVariable var = resolveVar(getVarDecl(e)); assert(var.isfloat()); x0 = var.floatVar(_current_space); } else { FloatVal i; if (IntLit* il = e->dyn_cast<IntLit>()) i = il->v().toInt(); else if (BoolLit* bl = e->dyn_cast<BoolLit>()) i = bl->v(); else if (FloatLit* fl = e->dyn_cast<FloatLit>()) i = fl->v(); else { std::stringstream ssm; ssm << "Expected bool, int or float literal instead of: " << *e; throw InternalError(ssm.str()); } x0 = FloatVar(*this->_current_space, i.toDouble(), i.toDouble()); } return x0;}
Gecode::FloatVarArgs GecodeSolverInstance::arg2floatvarargs(Expression* arg, int offset) { ArrayLit* a = arg2arraylit(arg); if (a->size() == 0) { FloatVarArgs emptyFa(0); return emptyFa; } FloatVarArgs fa(a->size() + offset); for (int i = offset; i--;) fa[i] = FloatVar(*this->_current_space, 0.0, 0.0); for (int i = a->size(); i--;) { Expression* e = (*a)[i]; if (e->type().isvar()) { GecodeVariable var = resolveVar(getVarDecl(e)); assert(var.isfloat()); fa[i + offset] = var.floatVar(_current_space); } else { if (FloatLit* fl = e->dyn_cast<FloatLit>()) { double value = fl->v().toDouble(); FloatVar fv(*this->_current_space, value, value); fa[i + offset] = fv; } else { std::stringstream ssm; ssm << "Expected float literal instead of: " << *e; throw InternalError(ssm.str()); } } } return fa;}#endif
MZ_IntConLevel GecodeSolverInstance::ann2icl(const Annotation& ann) { if (!ann.isEmpty()) { if (getAnnotation(ann, "val")) return MZ_ICL_VAL; if (getAnnotation(ann, "domain")) return MZ_ICL_DOM; if (getAnnotation(ann, "bounds") || getAnnotation(ann, "boundsR") || getAnnotation(ann, "boundsD") || getAnnotation(ann, "boundsZ")) return MZ_ICL_BND; } return MZ_ICL_DEF;}
VarDecl* GecodeSolverInstance::getVarDecl(Expression* expr) { VarDecl* vd = NULL; if ((vd = expr->dyn_cast<VarDecl>())) { vd = expr->cast<VarDecl>(); } else if (Id* id = expr->dyn_cast<Id>()) { vd = id->decl(); } else if (ArrayAccess* aa = expr->dyn_cast<ArrayAccess>()) { vd = resolveArrayAccess(aa); } else { std::stringstream ssm; ssm << "Can not extract vardecl from " << *expr; throw new InternalError(ssm.str()); } return vd;}
VarDecl* GecodeSolverInstance::resolveArrayAccess(ArrayAccess* aa) { VarDecl* vd = aa->v()->cast<Id>()->decl(); int idx = aa->idx()[0]->cast<IntLit>()->v().toInt(); return resolveArrayAccess(vd, idx);}
VarDecl* GecodeSolverInstance::resolveArrayAccess(VarDecl* vd, int index) { std::unordered_map<VarDecl*, std::vector<Expression*>*>::iterator it = arrayMap.find(vd); if (it != arrayMap.end()) { std::vector<Expression*>* exprs = it->second; Expression* expr = (*exprs)[index - 1]; return expr->cast<VarDecl>(); } else { std::stringstream ssm; ssm << "Unknown array: " << vd->id(); throw new InternalError(ssm.str()); }}
GecodeSolver::Variable GecodeSolverInstance::resolveVar(Expression* e) { std::stringstream ssm; ssm << "USING OLD SOLVER INTERFACE THINGS!"; throw InternalError(ssm.str()); // if (Id* id = e->dyn_cast<Id>()) { // return _variableMap.get(id->decl()->id()); //lookupVar(id->decl()); // } else if (VarDecl* vd = e->dyn_cast<VarDecl>()) { // return _variableMap.get(vd->id()->decl()->id()); // } else if (ArrayAccess* aa = e->dyn_cast<ArrayAccess>()) { // return _variableMap.get(resolveArrayAccess(aa)->id()->decl()->id()); // } else { // std::stringstream ssm; // ssm << "Expected Id, VarDecl or ArrayAccess instead of \"" << *e << "\""; // throw InternalError(ssm.str()); // }}
GecodeSolver::Variable GecodeSolverInstance::resolveVar(Variable* v) { int i = _variableMap.size() - 1; std::unordered_map<int, VarId>::iterator it; while (i >= 0) { it = _variableMap[i].find(v->timestamp()); if (it != _variableMap[i].end()) { break; } i--; } assert(it != _variableMap[0].end()); return it->second; // lookupVar(id->decl());}
SolverInstance::Status GecodeSolverInstance::next(void) { GCLock lock; prepareEngine();
_solution = engine->next();
if (_solution) { assignSolutionToOutput(); return SolverInstance::SAT; } else if (engine->stopped()) { return SolverInstance::UNKNOWN; } else { return SolverInstance::UNSAT; }}
void GecodeSolverInstance::resetSolver(void) { assert(false); // TODO: implement}
Expression* GecodeSolverInstance::getSolutionValue(Id* id) { id = id->decl()->id(); if (id->type().isvar()) { GecodeVariable var = resolveVar(id->decl()->id());#ifdef GECODE_HAS_SET_VARS if (id->type().is_set()) { SetVar& sv = var.setVar(_solution); assert(sv.assigned()); SetVarGlbRanges svr(sv); assert(svr());
IntVal mi = svr.min(); IntVal ma = svr.max(); ++svr; vector<IntVal> vals; if (svr()) { SetVarGlbValues svv(sv); IntVal i = svv.val(); vals.push_back(i); ++svv; for (; svv(); ++svv) vals.push_back(svv.val()); return new SetLit(Location().introduce(), IntSetVal::a(vals)); } else { return new SetLit(Location().introduce(), IntSetVal::a(mi, ma)); } }#endif switch (id->type().bt()) { case Type::BT_INT: assert(var.intVar(_solution).assigned()); return IntLit::a(var.intVar(_solution).val()); case Type::BT_BOOL: assert(var.boolVar(_solution).assigned()); return constants().boollit(var.boolVar(_solution).val());#ifdef GECODE_HAS_FLOAT_VARS case Type::BT_FLOAT: assert(var.floatVar(_solution).assigned()); return FloatLit::a(var.floatVar(_solution).val().med());#endif default: return NULL; } } else { return id->decl()->e(); }}
Val GecodeSolverInstance::getSolutionValue(Variable* v) { GecodeVariable var = resolveVar(v);
if (var.isbool()) { assert(var.boolVar(_solution).assigned()); return Val(var.boolVar(_solution).val()); } else { assert(var.intVar(_solution).assigned()); return Val(var.intVar(_solution).val()); }}
void GecodeSolverInstance::prepareEngine(void) { GCLock lock; GecodeOptions& _opt = static_cast<GecodeOptions&>(*_options); delete engine; engine = nullptr; if (engine == NULL) { // TODO: check what we need to do options-wise std::vector<Expression*> branch_vars; std::vector<Expression*> solve_args; Expression* optSearch = NULL;
switch (_current_space->_solveType) { case MiniZinc::SolveI::SolveType::ST_MIN: assert(solveExpr != NULL); branch_vars.push_back(solveExpr); solve_args.push_back(new ArrayLit(Location(), branch_vars)); if (!_current_space->_optVarIsInt) // TODO: why?? solve_args.push_back(FloatLit::a(0.0)); solve_args.push_back(new Id(Location(), "input_order", NULL)); solve_args.push_back(new Id( Location(), _current_space->_optVarIsInt ? "indomain_min" : "indomain_split", NULL)); solve_args.push_back(new Id(Location(), "complete", NULL)); optSearch = new Call( Location(), _current_space->_optVarIsInt ? "int_search" : "float_search", solve_args); break; case MiniZinc::SolveI::SolveType::ST_MAX: branch_vars.push_back(solveExpr); solve_args.push_back(new ArrayLit(Location(), branch_vars)); if (!_current_space->_optVarIsInt) solve_args.push_back(FloatLit::a(0.0)); solve_args.push_back(new Id(Location(), "input_order", NULL)); solve_args.push_back( new Id(Location(), _current_space->_optVarIsInt ? "indomain_max" : "indomain_split_reverse", NULL)); solve_args.push_back(new Id(Location(), "complete", NULL)); optSearch = new Call( Location(), _current_space->_optVarIsInt ? "int_search" : "float_search", solve_args); break; case MiniZinc::SolveI::SolveType::ST_SAT: break; default: assert(false); }
int seed = _opt.seed; double decay = _opt.decay;
Annotation search_ann; createBranchers(search_ann, optSearch, seed, decay, false, /* ignoreUnknown */ std::cerr);
int nodeStop = _opt.nodes; int failStop = _opt.fails; int timeStop = _opt.time;
engine_options.stop = Driver::CombinedStop::create(nodeStop, failStop, timeStop, false); // TODO: add presolving part if (_current_space->_solveType == MiniZinc::SolveI::SolveType::ST_SAT) { engine = new MetaEngine<DFS, Driver::EngineToMeta>(this->_current_space, engine_options); } else { engine = new MetaEngine<BAB, Driver::EngineToMeta>(this->_current_space, engine_options); } }}
void GecodeSolverInstance::print_stats() { Gecode::Search::Statistics stat = engine->statistics(); std::cerr << "%% variables: " << (_current_space->iv.size() + _current_space->bv.size() /*+ _current_space->sv.size()*/) << std::endl << "%% propagators: " << Gecode::PropagatorGroup::all.size(*_current_space) << endl << "%% propagations: " << stat.propagate << std::endl << "%% nodes: " << stat.node << std::endl << "%% failures: " << stat.fail << std::endl << "%% restarts: " << stat.restart << std::endl << "%% peak depth: " << stat.depth << std::endl << std::endl;}
void GecodeSolverInstance::processSolution(bool last_sol) { if (_solution) { assignSolutionToOutput(); printSolution(); if (_current_space->_solveType == MiniZinc::SolveI::SolveType::ST_SAT) { if (engine->stopped() || !last_sol) { _status = SolverInstance::SAT; } else { _status = SolverInstance::OPT; } } else { if (engine->stopped()) { Gecode::Search::Statistics stat = engine->statistics(); Driver::CombinedStop* cs = static_cast<Driver::CombinedStop*>(engine_options.stop); std::cerr << "% GecodeSolverInstance: "; int r = cs->reason(stat, engine_options); if (r & Driver::CombinedStop::SR_INT) std::cerr << "user interrupt " << std::endl; else { if (r & Driver::CombinedStop::SR_NODE) { _status_reason = SolverInstance::SR_LIMIT; std::cerr << "node "; } if (r & Driver::CombinedStop::SR_FAIL) { _status_reason = SolverInstance::SR_LIMIT; std::cerr << "failure "; } if (r & Driver::CombinedStop::SR_TIME) { _status_reason = SolverInstance::SR_LIMIT; std::cerr << "time "; } std::cerr << "limit reached" << std::endl << std::endl; } if (_n_found_solutions > 0) { _status = SolverInstance::SAT; } else { _status = SolverInstance::UNKNOWN; } } else { _status = last_sol ? SolverInstance::OPT : SolverInstance::SAT; } } } else { if (engine->stopped()) { _status = SolverInstance::UNKNOWN; } else { _status = SolverInstance::UNSAT; } }}
SolverInstanceBase::Status GecodeSolverInstance::solve(void) { GCLock lock; SolverInstanceBase::Status ret; // Reset solutions previously found _n_found_solutions = 0; delete _solution; _solution = nullptr;
GecodeOptions& _opt = static_cast<GecodeOptions&>(*_options); _only_range_domains = _opt.only_range_domains; _run_sac = _opt.sac; _run_shave = _opt.shave; _pre_passes = _opt.pre_passes; _print_stats = _opt.statistics; _all_solutions = _opt.all_solutions; _n_max_solutions = _opt.n_solutions; _allow_unbounded_vars = _opt.allow_unbounded_vars;
prepareEngine();
if (_run_sac || _run_shave) { presolve(); }
int n_max_solutions = _n_max_solutions; if (n_max_solutions == -1) { if (_all_solutions) { n_max_solutions = 0; } else if (_current_space->_solveType == MiniZinc::SolveI::SolveType::ST_SAT) { n_max_solutions = 1; } }
FznSpace* next_sol = engine->next(); while (next_sol) { delete _solution; _solution = next_sol; _n_found_solutions++;
if (n_max_solutions == 0 || _n_found_solutions <= n_max_solutions) { // processSolution(); if (_print_stats) print_stats(); } if (_n_found_solutions == n_max_solutions) { break; } next_sol = engine->next(); } if (_current_space->_solveType != MiniZinc::SolveI::SolveType::ST_SAT) { if (n_max_solutions == -1) { // Print last solution // processSolution(next_sol == NULL); if (_print_stats) print_stats(); } } if (next_sol == NULL) { if (_solution) { ret = engine->stopped() ? SolverInstance::SAT : SolverInstance::OPT; } else { ret = engine->stopped() ? SolverInstance::UNKNOWN : SolverInstance::UNSAT; } } else { ret = SolverInstance::SAT; } delete engine; engine = nullptr; return ret;}
class IntVarComp {public: std::vector<Gecode::IntVar> iv; IntVarComp(std::vector<Gecode::IntVar> b) { iv = b; } int operator()(int a, int b) { return iv[a].size() < iv[b].size(); }};
class IntVarRangesBwd : public Int::IntVarImpBwd {public: IntVarRangesBwd(void) {} IntVarRangesBwd(const IntVar& x) : Int::IntVarImpBwd(x.varimp()) {} void init(const IntVar& x) { Int::IntVarImpBwd(x.varimp()); }};
bool GecodeSolverInstance::sac(bool toFixedPoint = false, bool shaving = false) { if (_current_space->status() == SS_FAILED) return false; bool modified; std::vector<int> sorted_iv;
for (unsigned int i = 0; i < _current_space->iv.size(); i++) if (!_current_space->iv[i].assigned()) sorted_iv.push_back(i); IntVarComp ivc(_current_space->iv); sort(sorted_iv.begin(), sorted_iv.end(), ivc);
do { modified = false; for (unsigned int idx = 0; idx < _current_space->bv.size(); idx++) { BoolVar bvar = _current_space->bv[idx]; if (!bvar.assigned()) { for (int val = bvar.min(); val <= bvar.max(); ++val) { FznSpace* f = static_cast<FznSpace*>(_current_space->clone()); rel(*f, f->bv[idx], IRT_EQ, val); if (f->status() == SS_FAILED) { rel(*_current_space, bvar, IRT_NQ, val); modified = true; if (_current_space->status() == SS_FAILED) return false; } delete f; } } }
for (unsigned int i = 0; i < sorted_iv.size(); i++) { unsigned int idx = sorted_iv[i]; IntVar ivar = _current_space->iv[idx]; bool tight = false; unsigned int nnq = 0; int fwd_min; IntArgs nq(ivar.size()); for (IntVarValues vv(ivar); vv() && !tight; ++vv) { FznSpace* f = static_cast<FznSpace*>(_current_space->clone()); rel(*f, f->iv[idx], IRT_EQ, vv.val()); if (f->status() == SS_FAILED) { nq[nnq++] = vv.val(); } else { fwd_min = vv.val(); tight = shaving; } delete f; } if (shaving) { tight = false; for (IntVarRangesBwd vr(ivar); vr() && !tight; ++vr) { for (int i = vr.max(); i >= vr.min() && i >= fwd_min; i--) { FznSpace* f = static_cast<FznSpace*>(_current_space->clone()); rel(*f, f->iv[idx], IRT_EQ, i); if (f->status() == SS_FAILED) nq[nnq++] = i; else tight = true; delete f; } } } if (nnq) modified = true; while (nnq--) rel(*_current_space, ivar, IRT_NQ, nq[nnq]); if (_current_space->status() == SS_FAILED) return false; } } while (toFixedPoint && modified); return true;}
bool GecodeSolverInstance::presolve(Model* orig_model) { GCLock lock; if (_current_space->status() == SS_FAILED) return false; // run SAC? if (_run_sac || _run_shave) { unsigned int iters = _pre_passes; if (iters) { for (unsigned int i = 0; i < iters; i++) sac(false, _run_shave); } else { sac(true, _run_shave); } }
if (orig_model != NULL) { std::unordered_map<std::string, VarDecl*> vds; for (VarDeclIterator it = orig_model->begin_vardecls(); it != orig_model->end_vardecls(); ++it) { VarDecl* vd = it->e(); vds[vd->id()->str().str()] = vd; }
// TODO: Does not work for new SolverInstance // IdMap<GecodeVariable>::iterator it; // for(auto it = _variableMap.begin(); it != _variableMap.end(); it++) { // int vd = it->first->decl(); // long long int old_domsize = 0; // bool holes = false;
// if(vd->ti()->domain()) { // if(vd->type().isint()) { // IntBounds old_bounds = compute_int_bounds(_env.envi(), vd->id()); // long long int old_rangesize = abs(old_bounds.u.toInt() - old_bounds.l.toInt()); // if(vd->ti()->domain()->isa<SetLit>()) // old_domsize = arg2intset(_env.envi(), vd->ti()->domain()).size(); // else // old_domsize = old_rangesize + 1; // holes = old_domsize < old_rangesize + 1; // } // }
// std::string name = it->first->str().str();
// if(vds.find(name) != vds.end()) { // VarDecl* nvd = vds[name]; // Type::BaseType bt = vd->type().bt(); // if(bt == Type::BaseType::BT_INT) { // IntVar intvar = it->second.intVar(_current_space); // const long long int l = intvar.min(), u = intvar.max();
// if(l==u) { // if(nvd->e()) { // nvd->ti()->domain(new SetLit(nvd->loc(), IntSetVal::a(l, u))); // } else { // nvd->type(Type::parint()); // nvd->ti(new TypeInst(nvd->loc(), Type::parint())); // nvd->e(IntLit::a(l)); // } // } else if(!(l == Gecode::Int::Limits::min || u == Gecode::Int::Limits::max)){ // if(_only_range_domains && !holes) { // nvd->ti()->domain(new SetLit(nvd->loc(), IntSetVal::a(l, u))); // } else { // IntVarRanges ivr(intvar); // nvd->ti()->domain(new SetLit(nvd->loc(), IntSetVal::ai(ivr))); // } // } // } else if(bt == Type::BaseType::BT_BOOL) { // BoolVar boolvar = it->second.boolVar(_current_space); // int l = boolvar.min(), // u = boolvar.max(); // if(l == u) { // if(nvd->e()) { // nvd->ti()->domain(constants().boollit(l)); // } else { // nvd->type(Type::parbool()); // nvd->ti(new TypeInst(nvd->loc(), Type::parbool())); // nvd->e(new BoolLit(nvd->loc(), l)); // } // } // #ifdef GECODE_HAS_FLOAT_VAR // } else if(bt == Type::BaseType::BT_FLOAT) { // Gecode::FloatVar floatvar = it->second.floatVar(_current_space); // if(floatvar.assigned() && !nvd->e()) { // FloatNum l = floatvar.min(); // nvd->type(Type::parfloat()); // nvd->ti(new TypeInst(nvd->loc(), Type::parfloat())); // nvd->e(FloatLit::a(l)); // } else { // FloatNum l = floatvar.min(), // u = floatvar.max(); // nvd->ti()->domain(new SetLit(nvd->loc(), FloatSetVal::a(l, u))); // } // #endif // } // } // } } return true;}
void GecodeSolverInstance::setSearchStrategyFromAnnotation( std::vector<Expression*> flatAnn, std::vector<bool>& iv_searched, std::vector<bool>& bv_searched,#ifdef GECODE_HAS_SET_VARS std::vector<bool>& sv_searched,#endif#ifdef GECODE_HAS_FLOAT_VARS std::vector<bool>& fv_searched,#endif TieBreak<IntVarBranch>& def_int_varsel, IntValBranch& def_int_valsel, TieBreak<BoolVarBranch>& def_bool_varsel, BoolValBranch& def_bool_valsel,#ifdef GECODE_HAS_SET_VARS SetVarBranch& def_set_varsel, SetValBranch& def_set_valsel,#endif#ifdef GECODE_HAS_FLOAT_VARS TieBreak<FloatVarBranch>& def_float_varsel, FloatValBranch& def_float_valsel,#endif Rnd& rnd, double decay, bool ignoreUnknown, std::ostream& err) { for (unsigned int i = 0; i < flatAnn.size(); i++) { if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "gecode_search") { // Call* c = flatAnn[i]->cast<Call>(); // branchWithPlugin(c->args); std::cerr << "WARNING: Not supporting search annotation \"gecode_search\" yet." << std::endl; return; } else if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "int_search") { Call* call = flatAnn[i]->cast<Call>(); ArrayLit* vars = arg2arraylit(call->arg(0)); if (vars->size() == 0) { // empty array std::cerr << "WARNING: trying to branch on empty array in search annotation: " << *call << std::endl; continue; } int k = vars->size(); for (int i = vars->size(); i--;) if (!(*vars)[i]->type().isvarint()) k--; IntVarArgs va(k); std::vector<std::string> names; k = 0; for (unsigned int i = 0; i < vars->size(); i++) { if (!(*vars)[i]->type().isvarint()) { continue; } int idx = resolveVar(getVarDecl((*vars)[i])).index(); va[k++] = _current_space->iv[idx]; iv_searched[idx] = true; names.push_back(getVarDecl((*vars)[i])->id()->str().str()); } std::string r0, r1; // BrancherHandle bh = branch(*_current_space, va, ann2ivarsel(call->arg(1)->cast<Id>()->str().str(), rnd, decay), ann2ivalsel(call->arg(2)->cast<Id>()->str().str(), r0, r1, rnd), NULL //,&varValPrint<IntVar> ); // branchInfo.add(bh,r0,r1,names); } // end int_search else if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "int_assign") { Call* call = flatAnn[i]->dyn_cast<Call>(); ArrayLit* vars = arg2arraylit(call->arg(0)); int k = vars->size(); for (int i = vars->size(); i--;) if (!((*vars)[i])->type().isvarint()) k--; IntVarArgs va(k); k = 0; for (unsigned int i = 0; i < vars->size(); i++) { if (!((*vars)[i])->type().isvarint()) continue; int idx = resolveVar(getVarDecl((*vars)[i])).index(); va[k++] = _current_space->iv[idx]; iv_searched[idx] = true; } assign(*_current_space, va, ann2asnivalsel(call->arg(1)->cast<Id>()->str().str(), rnd), NULL //&varValPrint<IntVar> ); } else if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "bool_search") { Call* call = flatAnn[i]->dyn_cast<Call>(); ArrayLit* vars = arg2arraylit(call->arg(0)); int k = vars->size(); for (int i = vars->size(); i--;) if (!((*vars)[i])->type().isvarbool()) k--; BoolVarArgs va(k); k = 0; std::vector<std::string> names; for (unsigned int i = 0; i < vars->size(); i++) { if (!((*vars)[i])->type().isvarbool()) continue; int idx = resolveVar(getVarDecl((*vars)[i])).index(); va[k++] = _current_space->bv[idx]; bv_searched[idx] = true; names.push_back(getVarDecl((*vars)[i])->id()->str().str()); }
std::string r0, r1; // BrancherHandle bh = branch(*_current_space, va, ann2bvarsel(call->arg(1)->cast<Id>()->str().str(), rnd, decay), ann2bvalsel(call->arg(2)->cast<Id>()->str().str(), r0, r1, rnd), NULL //, //&varValPrint<BoolVar> ); // branchInfo.add(bh,r0,r1,names); } else if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "int_default_search") { Call* call = flatAnn[i]->dyn_cast<Call>(); def_int_varsel = ann2ivarsel(call->arg(0)->cast<Id>()->str().str(), rnd, decay); std::string r0; def_int_valsel = ann2ivalsel(call->arg(1)->cast<Id>()->str().str(), r0, r0, rnd); } else if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "bool_default_search") { Call* call = flatAnn[i]->dyn_cast<Call>(); std::string r0; def_bool_varsel = ann2bvarsel(call->arg(0)->cast<Id>()->str().str(), rnd, decay); def_bool_valsel = ann2bvalsel(call->arg(1)->cast<Id>()->str().str(), r0, r0, rnd); } else if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "set_search") {#ifdef GECODE_HAS_SET_VARS Call* call = flatAnn[i]->dyn_cast<Call>(); ArrayLit* vars = arg2arraylit(call->arg(0)); int k = vars->size(); for (int i = vars->size(); i--;) if (!((*vars)[i])->type().is_set() || !((*vars)[i])->type().isvar()) k--; SetVarArgs va(k); k = 0; std::vector<std::string> names; for (unsigned int i = 0; i < vars->size(); i++) { if (!((*vars)[i])->type().is_set() || !((*vars)[i])->type().isvar()) continue; int idx = resolveVar(getVarDecl((*vars)[i])).index(); va[k++] = _current_space->sv[idx]; sv_searched[idx] = true; names.push_back(getVarDecl((*vars)[i])->id()->str().str()); } std::string r0, r1; // BrancherHandle bh = branch(*_current_space, va, ann2svarsel(call->arg(1)->cast<Id>()->str().str(), rnd, decay), ann2svalsel(call->arg(2)->cast<Id>()->str().str(), r0, r1, rnd), NULL //, //&varValPrint<SetVar> ); // branchInfo.add(bh,r0,r1,names);#else if (!ignoreUnknown) { err << "Warning, ignored search annotation: "; // flatAnn[i]->print(err); err << std::endl; }#endif } else if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "set_default_search") {#ifdef GECODE_HAS_SET_VARS Call* call = flatAnn[i]->dyn_cast<Call>(); def_set_varsel = ann2svarsel(call->arg(0)->cast<Id>()->str().str(), rnd, decay); std::string r0; def_set_valsel = ann2svalsel(call->arg(1)->cast<Id>()->str().str(), r0, r0, rnd);#else if (!ignoreUnknown) { err << "Warning, ignored search annotation: "; // flatAnn[i]->print(err); err << std::endl; }#endif } else if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "float_default_search") {#ifdef GECODE_HAS_FLOAT_VARS Call* call = flatAnn[i]->dyn_cast<Call>(); def_float_varsel = ann2fvarsel(call->arg(0)->cast<Id>()->str().str(), rnd, decay); std::string r0; def_float_valsel = ann2fvalsel(call->arg(1)->cast<Id>()->str().str(), r0, r0);#else if (!ignoreUnknown) { err << "Warning, ignored search annotation: float_default_search" << std::endl; }#endif } else if (flatAnn[i]->isa<Call>() && flatAnn[i]->cast<Call>()->id().str() == "float_search") {#ifdef GECODE_HAS_FLOAT_VARS Call* call = flatAnn[i]->dyn_cast<Call>(); ArrayLit* vars = call->arg(0)->cast<ArrayLit>(); int k = vars->size(); for (int i = vars->size(); i--;) if (!((*vars)[i])->type().isvarfloat()) k--; FloatVarArgs va(k); k = 0; std::vector<std::string> names; for (unsigned int i = 0; i < vars->size(); i++) { if (!((*vars)[i])->type().isvarfloat()) continue; int idx = resolveVar(getVarDecl((*vars)[i])).index(); va[k++] = _current_space->fv[idx]; fv_searched[idx] = true; names.push_back(getVarDecl((*vars)[i])->id()->str().str()); } std::string r0, r1; // BrancherHandle bh = branch(*_current_space, va, ann2fvarsel(call->arg(2)->cast<Id>()->str().str(), rnd, decay), ann2fvalsel(call->arg(3)->cast<Id>()->str().str(), r0, r1), NULL //, //&varValPrintF ); // branchInfo.add(bh,r0,r1,names);#else if (!ignoreUnknown) { err << "Warning, ignored search annotation: float_search" << std::endl; }#endif } else { if (!ignoreUnknown) { err << "Warning, ignored search annotation: " << *flatAnn[i] << std::endl; } } } // end for all annotations}
void GecodeSolverInstance::createBranchers(Annotation& ann, Expression* additionalAnn, int seed, double decay, bool ignoreUnknown, std::ostream& err) { // default search heuristics Rnd rnd(static_cast<unsigned int>(seed)); TieBreak<IntVarBranch> def_int_varsel = INT_VAR_AFC_SIZE_MAX(0.99); IntValBranch def_int_valsel = INT_VAL_MIN(); TieBreak<BoolVarBranch> def_bool_varsel = BOOL_VAR_AFC_MAX(0.99); BoolValBranch def_bool_valsel = BOOL_VAL_MIN();#ifdef GECODE_HAS_SET_VARS SetVarBranch def_set_varsel = SET_VAR_AFC_SIZE_MAX(0.99); SetValBranch def_set_valsel = SET_VAL_MIN_INC();#endif#ifdef GECODE_HAS_FLOAT_VARS TieBreak<FloatVarBranch> def_float_varsel = FLOAT_VAR_SIZE_MIN(); FloatValBranch def_float_valsel = FLOAT_VAL_SPLIT_MIN();#endif
std::vector<bool> iv_searched(_current_space->iv.size()); for (unsigned int i = _current_space->iv.size(); i--;) iv_searched[i] = false; std::vector<bool> bv_searched(_current_space->bv.size()); for (unsigned int i = _current_space->bv.size(); i--;) bv_searched[i] = false;#ifdef GECODE_HAS_SET_VARS std::vector<bool> sv_searched(_current_space->sv.size()); for (unsigned int i = _current_space->sv.size(); i--;) sv_searched[i] = false;#endif#ifdef GECODE_HAS_FLOAT_VARS std::vector<bool> fv_searched(_current_space->fv.size()); for (unsigned int i = _current_space->fv.size(); i--;) fv_searched[i] = false;#endif
// solving annotations std::vector<Expression*> flatAnn; if (!ann.isEmpty()) { flattenSearchAnnotations(ann, flatAnn); } if (additionalAnn != NULL) { flatAnn.push_back(additionalAnn); } if (flatAnn.size() > 0) { setSearchStrategyFromAnnotation(flatAnn, iv_searched, bv_searched,#ifdef GECODE_HAS_SET_VARS sv_searched,#endif#ifdef GECODE_HAS_FLOAT_VARS fv_searched,#endif def_int_varsel, def_int_valsel, def_bool_varsel, def_bool_valsel,#ifdef GECODE_HAS_SET_VARS def_set_varsel, def_set_valsel,#endif#ifdef GECODE_HAS_FLOAT_VARS def_float_varsel, def_float_valsel,#endif rnd, decay, ignoreUnknown, err); }
int introduced = 0; int funcdep = 0; int searched = 0; for (int i = _current_space->iv.size(); i--;) { if (iv_searched[i]) { searched++; } else if (_current_space->iv_introduced[i]) { if (_current_space->iv_defined[i]) { funcdep++; } else { introduced++; } } } IntVarArgs iv_sol(_current_space->iv.size() - (introduced + funcdep + searched)); IntVarArgs iv_tmp(introduced); for (unsigned int i = _current_space->iv.size(), j = 0, k = 0; i--;) { if (iv_searched[i]) continue; if (_current_space->iv_introduced[i]) { if (_current_space->iv_introduced.size() >= i) { if (!_current_space->iv_defined[i]) { iv_tmp[j++] = _current_space->iv[i]; } } } else { iv_sol[k++] = _current_space->iv[i]; } } // Collecting Boolean variables introduced = 0; funcdep = 0; searched = 0; for (int i = _current_space->bv.size(); i--;) { if (bv_searched[i]) { searched++; } else if (_current_space->bv_introduced[i]) { if (_current_space->bv_defined[i]) { funcdep++; } else { introduced++; } } } BoolVarArgs bv_sol(_current_space->bv.size() - (introduced + funcdep + searched)); BoolVarArgs bv_tmp(introduced); for (int i = _current_space->bv.size(), j = 0, k = 0; i--;) { if (bv_searched[i]) continue; if (_current_space->bv_introduced[i]) { if (!_current_space->bv_defined[i]) { bv_tmp[j++] = _current_space->bv[i]; } } else { bv_sol[k++] = _current_space->bv[i]; } }
if (iv_sol.size() > 0) branch(*this->_current_space, iv_sol, def_int_varsel, def_int_valsel); if (bv_sol.size() > 0) branch(*this->_current_space, bv_sol, def_bool_varsel, def_bool_valsel);
// std::cout << "DEBUG: branched over " << iv_sol.size() << " integer variables."<< // std::endl; std::cout << "DEBUG: branched over " << bv_sol.size() << " Boolean // variables."<< std::endl;#ifdef GECODE_HAS_FLOAT_VARS introduced = 0; funcdep = 0; searched = 0; for (int i = _current_space->fv.size(); i--;) { if (fv_searched[i]) { searched++; } else if (_current_space->fv_introduced[i]) { if (_current_space->fv_defined[i]) { funcdep++; } else { introduced++; } } } FloatVarArgs fv_sol(_current_space->fv.size() - (introduced + funcdep + searched)); FloatVarArgs fv_tmp(introduced); for (int i = _current_space->fv.size(), j = 0, k = 0; i--;) { if (fv_searched[i]) continue; if (_current_space->fv_introduced[i]) { if (!_current_space->fv_defined[i]) { fv_tmp[j++] = _current_space->fv[i]; } } else { fv_sol[k++] = _current_space->fv[i]; } }
if (fv_sol.size() > 0) branch(*this->_current_space, fv_sol, def_float_varsel, def_float_valsel);#endif#ifdef GECODE_HAS_SET_VARS introduced = 0; funcdep = 0; searched = 0; for (int i = _current_space->sv.size(); i--;) { if (sv_searched[i]) { searched++; } else if (_current_space->sv_introduced[i]) { if (_current_space->sv_defined[i]) { funcdep++; } else { introduced++; } } } SetVarArgs sv_sol(_current_space->sv.size() - (introduced + funcdep + searched)); SetVarArgs sv_tmp(introduced); for (int i = _current_space->sv.size(), j = 0, k = 0; i--;) { if (sv_searched[i]) continue; if (_current_space->sv_introduced[i]) { if (!_current_space->sv_defined[i]) { sv_tmp[j++] = _current_space->sv[i]; } } else { sv_sol[k++] = _current_space->sv[i]; } }
if (sv_sol.size() > 0) branch(*this->_current_space, sv_sol, def_set_varsel, def_set_valsel);#endif
// branching on auxiliary variables _current_space->iv_aux = IntVarArray(*this->_current_space, iv_tmp); _current_space->bv_aux = BoolVarArray(*this->_current_space, bv_tmp); int n_aux = _current_space->iv_aux.size() + _current_space->bv_aux.size();#ifdef GECODE_HAS_SET_VARS _current_space->sv_aux = SetVarArray(*this->_current_space, sv_tmp); n_aux += _current_space->sv_aux.size();#endif#ifdef GECODE_HAS_FLOAT_VARS _current_space->fv_aux = FloatVarArray(*this->_current_space, fv_tmp); n_aux += _current_space->fv_aux.size();#endif if (n_aux > 0) { AuxVarBrancher::post(*this->_current_space, def_int_varsel, def_int_valsel, def_bool_varsel, def_bool_valsel#ifdef GECODE_HAS_SET_VARS , def_set_varsel, def_set_valsel#endif#ifdef GECODE_HAS_FLOAT_VARS , def_float_varsel, def_float_valsel#endif ); // end post // std::cout << "DEBUG: Posted aux-var-brancher for " << n_aux << " aux-variables" << // std::endl; } // end if n_aux > 0 // else // std::cout << "DEBUG: No aux vars to branch on." << std::endl;}
TieBreak<IntVarBranch> GecodeSolverInstance::ann2ivarsel(std::string s, Rnd& rnd, double decay) { if (s == "input_order") return TieBreak<IntVarBranch>(INT_VAR_NONE()); if (s == "first_fail") return TieBreak<IntVarBranch>(INT_VAR_SIZE_MIN()); if (s == "anti_first_fail") return TieBreak<IntVarBranch>(INT_VAR_SIZE_MAX()); if (s == "smallest") return TieBreak<IntVarBranch>(INT_VAR_MIN_MIN()); if (s == "largest") return TieBreak<IntVarBranch>(INT_VAR_MAX_MAX()); if (s == "occurrence") return TieBreak<IntVarBranch>(INT_VAR_DEGREE_MAX()); if (s == "max_regret") return TieBreak<IntVarBranch>(INT_VAR_REGRET_MIN_MAX()); if (s == "most_constrained") return TieBreak<IntVarBranch>(INT_VAR_SIZE_MIN(), INT_VAR_DEGREE_MAX()); if (s == "random") { return TieBreak<IntVarBranch>(INT_VAR_RND(rnd)); } if (s == "afc_min") return TieBreak<IntVarBranch>(INT_VAR_AFC_MIN(decay)); if (s == "afc_max") return TieBreak<IntVarBranch>(INT_VAR_AFC_MAX(decay)); if (s == "afc_size_min") return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MIN(decay)); if (s == "afc_size_max" || s == "dom_w_deg") { return TieBreak<IntVarBranch>(INT_VAR_AFC_SIZE_MAX(decay)); } if (s == "action_min") return TieBreak<IntVarBranch>(INT_VAR_ACTION_MIN(decay)); if (s == "action_max") return TieBreak<IntVarBranch>(INT_VAR_ACTION_MAX(decay)); if (s == "action_size_min") return TieBreak<IntVarBranch>(INT_VAR_ACTION_SIZE_MIN(decay)); if (s == "action_size_max") return TieBreak<IntVarBranch>(INT_VAR_ACTION_SIZE_MAX(decay)); std::cerr << "Warning, ignored search annotation: " << s << std::endl; return TieBreak<IntVarBranch>(INT_VAR_NONE());}
Gecode::IntValBranch GecodeSolverInstance::ann2ivalsel(std::string s, std::string& r0, std::string& r1, Rnd& rnd) { if (s == "indomain_min") { r0 = "="; r1 = "!="; return INT_VAL_MIN(); } if (s == "indomain_max") { r0 = "="; r1 = "!="; return INT_VAL_MAX(); } if (s == "indomain_median") { r0 = "="; r1 = "!="; return INT_VAL_MED(); } if (s == "indomain_split") { r0 = "<="; r1 = ">"; return INT_VAL_SPLIT_MIN(); } if (s == "indomain_reverse_split") { r0 = ">"; r1 = "<="; return INT_VAL_SPLIT_MAX(); } if (s == "indomain_random") { r0 = "="; r1 = "!="; return INT_VAL_RND(rnd); } if (s == "indomain") { r0 = "="; r1 = "="; return INT_VALUES_MIN(); } if (s == "indomain_middle") { std::cerr << "Warning, replacing unsupported annotation " << "indomain_middle with indomain_median" << std::endl; r0 = "="; r1 = "!="; return INT_VAL_MED(); } if (s == "indomain_interval") { std::cerr << "Warning, replacing unsupported annotation " << "indomain_interval with indomain_split" << std::endl; r0 = "<="; r1 = ">"; return INT_VAL_SPLIT_MIN(); } std::cerr << "Warning, ignored search annotation: " << s << std::endl; r0 = "="; r1 = "!="; return INT_VAL_MIN();}
TieBreak<BoolVarBranch> GecodeSolverInstance::ann2bvarsel(std::string s, Rnd& rnd, double decay) { if ((s == "input_order") || (s == "first_fail") || (s == "anti_first_fail") || (s == "smallest") || (s == "largest") || (s == "max_regret")) return TieBreak<BoolVarBranch>(BOOL_VAR_NONE()); if ((s == "occurrence") || (s == "most_constrained")) return TieBreak<BoolVarBranch>(BOOL_VAR_DEGREE_MAX()); if (s == "random") return TieBreak<BoolVarBranch>(BOOL_VAR_RND(rnd)); if ((s == "afc_min") || (s == "afc_size_min")) return TieBreak<BoolVarBranch>(BOOL_VAR_AFC_MIN(decay)); if ((s == "afc_max") || (s == "afc_size_max") || (s == "dom_w_deg")) return TieBreak<BoolVarBranch>(BOOL_VAR_AFC_MAX(decay)); if ((s == "action_min") && (s == "action_size_min")) return TieBreak<BoolVarBranch>(BOOL_VAR_ACTION_MIN(decay)); if ((s == "action_max") || (s == "action_size_max")) return TieBreak<BoolVarBranch>(BOOL_VAR_ACTION_MAX(decay)); std::cerr << "Warning, ignored search annotation: " << s << std::endl; return TieBreak<BoolVarBranch>(BOOL_VAR_NONE());}
BoolValBranch GecodeSolverInstance::ann2bvalsel(std::string s, std::string& r0, std::string& r1, Rnd& rnd) { if (s == "indomain_min") { r0 = "="; r1 = "!="; return BOOL_VAL_MIN(); } if (s == "indomain_max") { r0 = "="; r1 = "!="; return BOOL_VAL_MAX(); } if (s == "indomain_median") { r0 = "="; r1 = "!="; return BOOL_VAL_MIN(); } if (s == "indomain_split") { r0 = "<="; r1 = ">"; return BOOL_VAL_MIN(); } if (s == "indomain_reverse_split") { r0 = ">"; r1 = "<="; return BOOL_VAL_MAX(); } if (s == "indomain_random") { r0 = "="; r1 = "!="; return BOOL_VAL_RND(rnd); } if (s == "indomain") { r0 = "="; r1 = "="; return BOOL_VAL_MIN(); } if (s == "indomain_middle") { std::cerr << "Warning, replacing unsupported annotation " << "indomain_middle with indomain_median" << std::endl; r0 = "="; r1 = "!="; return BOOL_VAL_MIN(); } if (s == "indomain_interval") { std::cerr << "Warning, replacing unsupported annotation " << "indomain_interval with indomain_split" << std::endl; r0 = "<="; r1 = ">"; return BOOL_VAL_MIN(); } std::cerr << "Warning, ignored search annotation: " << s << "\n"; r0 = "="; r1 = "!="; return BOOL_VAL_MIN();}
BoolAssign GecodeSolverInstance::ann2asnbvalsel(std::string s, Rnd& rnd) { if ((s == "indomain_min") || (s == "indomain_median")) return BOOL_ASSIGN_MIN(); if (s == "indomain_max") return BOOL_ASSIGN_MAX(); if (s == "indomain_random") { return BOOL_ASSIGN_RND(rnd); } std::cerr << "Warning, ignored search annotation: " << s << "\n"; return BOOL_ASSIGN_MIN();}
IntAssign GecodeSolverInstance::ann2asnivalsel(std::string s, Rnd& rnd) { if (s == "indomain_min") return INT_ASSIGN_MIN(); if (s == "indomain_max") return INT_ASSIGN_MAX(); if (s == "indomain_median") return INT_ASSIGN_MED(); if (s == "indomain_random") { return INT_ASSIGN_RND(rnd); } std::cerr << "Warning, ignored search annotation: " << s << std::endl; return INT_ASSIGN_MIN();}
void GecodeSolverInstance::pushState() { stack.push_back(_current_space); _variableMap.emplace_back(); _current_space->status(); _current_space = static_cast<FznSpace*>(_current_space->clone());}
void GecodeSolverInstance::popState() { delete _current_space; _current_space = stack.back(); stack.pop_back(); _variableMap.pop_back();}
#ifdef GECODE_HAS_SET_VARSSetVarBranch GecodeSolverInstance::ann2svarsel(std::string s, Rnd& rnd, double decay) { if (s == "input_order") return SET_VAR_NONE(); if (s == "first_fail") return SET_VAR_SIZE_MIN(); if (s == "anti_first_fail") return SET_VAR_SIZE_MAX(); if (s == "smallest") return SET_VAR_MIN_MIN(); if (s == "largest") return SET_VAR_MAX_MAX(); if (s == "afc_min") return SET_VAR_AFC_MIN(decay); if (s == "afc_max") return SET_VAR_AFC_MAX(decay); if (s == "afc_size_min") return SET_VAR_AFC_SIZE_MIN(decay); if (s == "afc_size_max") return SET_VAR_AFC_SIZE_MAX(decay); if (s == "action_min") return SET_VAR_ACTION_MIN(decay); if (s == "action_max") return SET_VAR_ACTION_MAX(decay); if (s == "action_size_min") return SET_VAR_ACTION_SIZE_MIN(decay); if (s == "action_size_max") return SET_VAR_ACTION_SIZE_MAX(decay); if (s == "random") { return SET_VAR_RND(rnd); } std::cerr << "Warning, ignored search annotation: " << s << std::endl; return SET_VAR_NONE();}
SetValBranch GecodeSolverInstance::ann2svalsel(std::string s, std::string r0, std::string r1, Rnd& rnd) { (void)rnd; if (s == "indomain_min") { r0 = "in"; r1 = "not in"; return SET_VAL_MIN_INC(); } if (s == "indomain_max") { r0 = "in"; r1 = "not in"; return SET_VAL_MAX_INC(); } if (s == "outdomain_min") { r1 = "in"; r0 = "not in"; return SET_VAL_MIN_EXC(); } if (s == "outdomain_max") { r1 = "in"; r0 = "not in"; return SET_VAL_MAX_EXC(); } std::cerr << "Warning, ignored search annotation: " << s << std::endl; r0 = "in"; r1 = "not in"; return SET_VAL_MIN_INC();}#endif
#ifdef GECODE_HAS_FLOAT_VARSTieBreak<FloatVarBranch> GecodeSolverInstance::ann2fvarsel(std::string s, Rnd& rnd, double decay) { if (s == "input_order") return TieBreak<FloatVarBranch>(FLOAT_VAR_NONE()); if (s == "first_fail") return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MIN()); if (s == "anti_first_fail") return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MAX()); if (s == "smallest") return TieBreak<FloatVarBranch>(FLOAT_VAR_MIN_MIN()); if (s == "largest") return TieBreak<FloatVarBranch>(FLOAT_VAR_MAX_MAX()); if (s == "occurrence") return TieBreak<FloatVarBranch>(FLOAT_VAR_DEGREE_MAX()); if (s == "most_constrained") return TieBreak<FloatVarBranch>(FLOAT_VAR_SIZE_MIN(), FLOAT_VAR_DEGREE_MAX()); if (s == "random") { return TieBreak<FloatVarBranch>(FLOAT_VAR_RND(rnd)); } if (s == "afc_min") return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_MIN(decay)); if (s == "afc_max") return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_MAX(decay)); if (s == "afc_size_min") return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_SIZE_MIN(decay)); if (s == "afc_size_max") return TieBreak<FloatVarBranch>(FLOAT_VAR_AFC_SIZE_MAX(decay)); if (s == "action_min") return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_MIN(decay)); if (s == "action_max") return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_MAX(decay)); if (s == "action_size_min") return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_SIZE_MIN(decay)); if (s == "action_size_max") return TieBreak<FloatVarBranch>(FLOAT_VAR_ACTION_SIZE_MAX(decay)); std::cerr << "Warning, ignored search annotation: " << s << std::endl; return TieBreak<FloatVarBranch>(FLOAT_VAR_NONE());}
FloatValBranch GecodeSolverInstance::ann2fvalsel(std::string s, std::string r0, std::string r1) { if (s == "indomain_split") { r0 = "<="; r1 = ">"; return FLOAT_VAL_SPLIT_MIN(); } if (s == "indomain_reverse_split") { r1 = "<="; r0 = ">"; return FLOAT_VAL_SPLIT_MAX(); } std::cerr << "Warning, ignored search annotation: " << s << std::endl; r0 = "<="; r1 = ">"; return FLOAT_VAL_SPLIT_MIN();}#endif} // namespace MiniZinc