1// 2// Copyright (c) 2013-2017 Benjamin Kaufmann 3// 4// This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 5// 6// Permission is hereby granted, free of charge, to any person obtaining a copy 7// of this software and associated documentation files (the "Software"), to 8// deal in the Software without restriction, including without limitation the 9// rights to use, copy, modify, merge, publish, distribute, sublicense, and/or 10// sell copies of the Software, and to permit persons to whom the Software is 11// furnished to do so, subject to the following conditions: 12// 13// The above copyright notice and this permission notice shall be included in 14// all copies or substantial portions of the Software. 15// 16// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 17// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 18// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 19// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 20// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING 21// FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS 22// IN THE SOFTWARE. 23// 24/*! 25 * \file 26 * \brief Supermacros for describing clasp's options. 27 * \code 28 * OPTION(key, "ext", ARG(...), "help", set, get) 29 * \endcode 30 * An option consists of: 31 * - a key (valid and unique c identifier in 'snake_case') 32 * - a key extension ("[!][,<alias>][,@<level>]") as understood by ProgramOptions::OptionInitHelper 33 * - an arg description (ARG macro) as understood by ProgramOptions::Value 34 * - a description (string) 35 * - a set action to be executed when a value (string) for the option is found in a source 36 * - a get action to be executed when the current value for an option is requested 37 * . 38 * 39 * \note In the implementation of ClaspCliConfig, each key is mapped to an enumeration constant and 40 * the stringified version of key (i.e. \#key) is used to identify options. 41 * Furthermore, the key is also used for generating command-line option names. 42 * As a convention, compound keys using 'snake_case' to separate words 43 * are mapped to dash-separated command-line option names. 44 * E.g. an \<option_like_this\> is mapped to the command-line option "option-like-this". 45 * 46 * \note ClaspCliConfig assumes a certain option order. In particular, context options shall 47 * precede all solver/search options, which in turn shall precede global asp/solving options. 48 * 49 * \note The following set actions may be used: 50 * - STORE(obj): converts the string value to the type of obj and stores the result in obj. 51 * - STORE_U(E, n): converts the string value to type E and stores it as unsigned int in n. 52 * - STORE_LEQ(n, max): converts the string value to an unsinged int and stores the result in n if it is <= max. 53 * - STORE_FLAG(n): converts the string value to a bool and stores the result in n as either 0 or 1. 54 * - STORE_OR_FILL(n): converts the string value to an unsinged int t and sets n to std::min(t, maxValue(n)). 55 * - FUN(arg): anonymous function of type bool (ArgStream& arg), where arg provides the following interface: 56 * - arg.ok() : returns whether arg is still valid 57 * - arg.empty() : returns whether arg is empty (i.e. all tokens were extracted) 58 * - arg.off() : returns whether arg contains a single token representing a valid off value 59 * - arg >> x : extracts and converts the current token and stores it in x. Sets failbit if conversion fails. 60 * - arg >> opt(x): extracts an optional argument, shorthand for (!arg.empty() ? arg>>obj : arg) 61 * . 62 * 63 * \note The following get actions may be used: 64 * - GET_FUN(str) : anonymous function of type void (OutputStream& str) 65 * - GET(obj...) : shorthand for GET_FUN(str) { (str << obj)...; } 66 * - GET_IF(C, obj): shorthand for GET_FUN(str) { ITE(C, str << obj, str << off); } 67 * . 68 * 69 * \note The following primitives may be used in the set/get arguments: 70 * - off : singleton object representing a valid off value ("no", "off", "false", "0") 71 * - ITE(C, x, y) : if-then-else expression, i.e. behaves like (C ? x : y). 72 * - SET(x, y) : shorthand for (x=y) == y. 73 * - SET_LEQ(x, v, m) : shorthand for (x <= m && SET(x, v)). 74 * - SET_GEQ(x, v, m) : shorthand for (x >= m && SET(x, v)). 75 * - SET_OR_FILL(x, v) : behaves like SET(x, min(v, maxValue(x))) 76 * - SET_OR_ZERO(x,v) : behaves like ITE(v <= maxValue(x), SET(x, v), SET(x, 0)). 77 * . 78 */ 79#if !defined(OPTION) || defined(SELF) || !defined(CLASP_HAS_THREADS) 80#error Invalid include context 81#endif 82 83#if !defined(GROUP_BEGIN) 84#define GROUP_BEGIN(X) 85#endif 86 87#if !defined(GROUP_END) 88#define GROUP_END(X) 89#endif 90 91//! Options for configuring a SharedContext object stored in a Clasp::ContextParams object. 92#if defined(CLASP_CONTEXT_OPTIONS) 93#define SELF CLASP_CONTEXT_OPTIONS 94GROUP_BEGIN(SELF) 95OPTION(share, "!,@1", ARG_EXT(defaultsTo("auto")->state(Value::value_defaulted), DEFINE_ENUM_MAPPING(ContextParams::ShareMode, \ 96 MAP("no" , ContextParams::share_no) , MAP("all", ContextParams::share_all),\ 97 MAP("auto", ContextParams::share_auto), MAP("problem", ContextParams::share_problem),\ 98 MAP("learnt", ContextParams::share_learnt))),\ 99 "Configure physical sharing of constraints [%D]\n"\ 100 " %A: {auto|problem|learnt|all}", FUN(arg) {ContextParams::ShareMode x; return arg>>x && SET(SELF.shareMode, (uint32)x);}, GET((ContextParams::ShareMode)SELF.shareMode)) 101OPTION(learn_explicit, ",@2" , ARG(flag()), "Do not use Short Implication Graph for learning", STORE_FLAG(SELF.shortMode), GET(SELF.shortMode)) 102OPTION(sat_prepro , "!,@1", ARG(arg("<arg>")->implicit("2")), \ 103 "Run SatELite-like preprocessing (Implicit: %I)\n" \ 104 " %A: <level>[,<limit>...]\n" \ 105 " <level> : Set preprocessing level to <level {1..3}>\n" \ 106 " 1: Variable elimination with subsumption (VE)\n" \ 107 " 2: VE with limited blocked clause elimination (BCE)\n" \ 108 " 3: Full BCE followed by VE\n" \ 109 " <limit> : [<key {iter|occ|time|frozen|clause}>=]<n> (0=no limit)\n" \ 110 " iter : Set iteration limit to <n> [0]\n" \ 111 " occ : Set variable occurrence limit to <n> [0]\n" \ 112 " time : Set time limit to <n> seconds [0]\n" \ 113 " frozen: Set frozen variables limit to <n>%% [0]\n" \ 114 " size : Set size limit to <n>*1000 clauses [4000]", STORE(SELF.satPre), GET(SELF.satPre)) 115GROUP_END(SELF) 116#undef CLASP_CONTEXT_OPTIONS 117#undef SELF 118#endif 119 120//! Global options only valid in facade. 121#if defined(CLASP_GLOBAL_OPTIONS) 122#define SELF CLASP_GLOBAL_OPTIONS 123GROUP_BEGIN(SELF) 124OPTION(stats, ",s", ARG(implicit("1")->arg("<n>[,<t>]")), "Enable {1=basic|2=full} statistics (<t> for tester)",\ 125 FUN(arg) { uint32 s = 0; uint32 t = 0;\ 126 return (arg.off() || (arg >> s >> opt(t) && s > 0)) 127 && SET(SELF.stats, s) && ((!SELF.testerConfig() && t == 0) || SET(SELF.addTesterConfig()->stats, t)); 128 },\ 129 GET_FUN(str) { ITE(!SELF.testerConfig() || !SELF.testerConfig()->stats, str << SELF.stats, str << SELF.stats << SELF.testerConfig()->stats); }) 130OPTION(parse_ext, "!", ARG(flag()), "Enable extensions in non-aspif input",\ 131 FUN(arg) { bool b = false; return (arg.off() || arg >> b) && (SELF.parse.assign(ParserOptions::parse_full, b), true); }, \ 132 GET((SELF.parse.anyOf(ParserOptions::parse_full)))) 133OPTION(parse_maxsat, "!", ARG(flag()), "Treat dimacs input as MaxSAT problem", \ 134 FUN(arg) { bool b = false; return (arg.off() || arg >> b) && (SELF.parse.assign(ParserOptions::parse_maxsat, b), true); }, \ 135 GET(static_cast<bool>(SELF.parse.isEnabled(ParserOptions::parse_maxsat)))) 136GROUP_END(SELF) 137#undef CLASP_GLOBAL_OPTIONS 138#undef SELF 139#endif 140 141//! Solver options (see SolverParams). 142#if defined(CLASP_SOLVER_OPTIONS) 143#define SELF CLASP_SOLVER_OPTIONS 144GROUP_BEGIN(SELF) 145OPTION(opt_strategy , "" , ARG_EXT(arg("<arg>"),\ 146 DEFINE_ENUM_MAPPING(OptParams::Type, MAP("bb", OptParams::type_bb), MAP("usc", OptParams::type_usc))\ 147 DEFINE_ENUM_MAPPING(OptParams::BBAlgo, MAP("lin", OptParams::bb_lin), MAP("hier", OptParams::bb_hier), MAP("inc", OptParams::bb_inc), MAP("dec", OptParams::bb_dec))\ 148 DEFINE_ENUM_MAPPING(OptParams::UscAlgo, MAP("oll", OptParams::usc_oll), MAP("one", OptParams::usc_one), MAP("k", OptParams::usc_k), MAP("pmres", OptParams::usc_pmr))\ 149 DEFINE_ENUM_MAPPING(OptParams::UscOption, MAP("disjoint", OptParams::usc_disjoint), MAP("succinct", OptParams::usc_succinct), MAP("stratify", OptParams::usc_stratify))),\ 150 "Configure optimization strategy\n" \ 151 " %A: {bb|usc}[,<tactics>]\n" \ 152 " bb : Model-guided optimization with <tactics {lin|hier|inc|dec}> [lin]\n" \ 153 " lin : Basic lexicographical descent\n" \ 154 " hier: Hierarchical (highest priority criteria first) descent \n" \ 155 " inc : Hierarchical descent with exponentially increasing steps\n" \ 156 " dec : Hierarchical descent with exponentially decreasing steps\n" \ 157 " usc: Core-guided optimization with <tactics>: <relax>[,<opts>]\n" \ 158 " <relax>: Relaxation algorithm {oll|one|k|pmres} [oll]\n" \ 159 " oll : Use strategy from unclasp\n" \ 160 " one : Add one cardinality constraint per core\n" \ 161 " k[,<n>]: Add cardinality constraints of bounded size ([0]=dynamic)\n" \ 162 " pmres : Add clauses of size 3\n" \ 163 " <opts> : Tactics <list {disjoint|succinct|stratify}>|<mask {0..7}>\n" \ 164 " disjoint: Disjoint-core preprocessing (1)\n" \ 165 " succinct: No redundant (symmetry) constraints (2)\n" \ 166 " stratify: Stratification heuristic for handling weights (4)", \ 167 STORE(SELF.opt), GET(SELF.opt)) 168OPTION(opt_usc_shrink, "", ARG_EXT(arg("<arg>"), DEFINE_ENUM_MAPPING(OptParams::UscTrim, \ 169 MAP("lin", OptParams::usc_trim_lin), MAP("rgs", OptParams::usc_trim_rgs), MAP("min", OptParams::usc_trim_min),\ 170 MAP("exp", OptParams::usc_trim_exp), MAP("inv", OptParams::usc_trim_inv), MAP("bin", OptParams::usc_trim_bin))),\ 171 "Enable core-shrinking in core-guided optimization\n" \ 172 " %A: <algo>[,<limit> (0=no limit)]\n" \ 173 " <algo> : Use algorithm {lin|inv|bin|rgs|exp|min}\n" \ 174 " lin : Forward linear search unsat\n" \ 175 " inv : Inverse linear search not unsat\n" \ 176 " bin : Binary search\n" \ 177 " rgs : Repeated geometric sequence until unsat\n" \ 178 " exp : Exponential search until unsat\n" \ 179 " min : Linear search for subset minimal core\n" \ 180 " <limit>: Limit solve calls to 2^<n> conflicts [10]",\ 181 FUN(arg) {\ 182 OptParams::UscTrim t = (OptParams::UscTrim)0; uint32 n = 0; \ 183 return (arg.off() || arg >> t >> opt(n=10)) && SET(SELF.opt.trim, uint32(t)) && SET(SELF.opt.tLim, uint32(n)); },\ 184 GET_IF(SELF.opt.trim, (OptParams::UscTrim)SELF.opt.trim, SELF.opt.tLim)) 185OPTION(opt_heuristic, "", ARG_EXT(arg("<list>"), DEFINE_ENUM_MAPPING(OptParams::Heuristic, \ 186 MAP("sign", OptParams::heu_sign), MAP("model", OptParams::heu_model))),\ 187 "Use opt. in <list {sign|model}> heuristics",\ 188 FUN(arg) { Set<OptParams::Heuristic> h; return (arg.off() || arg >> h) && SET(SELF.opt.heus, h.value());},\ 189 GET(Set<OptParams::Heuristic>(SELF.opt.heus))) 190OPTION(restart_on_model, "!", ARG(flag()), "Restart after each model\n", STORE_FLAG(SELF.restartOnModel), GET(SELF.restartOnModel)) 191OPTION(lookahead , "!", ARG_EXT(implicit("atom"), DEFINE_ENUM_MAPPING(VarType, \ 192 MAP("atom", Var_t::Atom), MAP("body", Var_t::Body), MAP("hybrid", Var_t::Hybrid))),\ 193 "Configure failed-literal detection (fld)\n" \ 194 " %A: <type>[,<limit>] / Implicit: %I\n" \ 195 " <type> : Run fld via {atom|body|hybrid} lookahead\n" \ 196 " <limit>: Disable fld after <limit> applications ([0]=no limit)\n" \ 197 " --lookahead=atom is default if --no-lookback is used\n", FUN(arg) { \ 198 VarType type = Var_t::Atom; uint32 limit = (SELF.lookOps = 0u);\ 199 return ITE(arg.off(), SET(SELF.lookType, 0u), arg>>type>>opt(limit) && SET(SELF.lookType, (uint32)type)) && SET_OR_ZERO(SELF.lookOps, limit);},\ 200 GET_IF(SELF.lookType, (VarType)SELF.lookType, SELF.lookOps)) 201OPTION(heuristic, "", ARG_EXT(arg("<heu>"), DEFINE_ENUM_MAPPING(Heuristic_t::Type, \ 202 MAP("berkmin", Heuristic_t::Berkmin), MAP("vmtf" , Heuristic_t::Vmtf), \ 203 MAP("vsids" , Heuristic_t::Vsids) , MAP("domain", Heuristic_t::Domain), \ 204 MAP("unit" , Heuristic_t::Unit) , MAP("auto", Heuristic_t::Default), MAP("none" , Heuristic_t::None))), \ 205 "Configure decision heuristic\n" \ 206 " %A: {Berkmin|Vmtf|Vsids|Domain|Unit|None}[,<n>]\n" \ 207 " Berkmin: Use BerkMin-like heuristic (Check last <n> nogoods [0]=all)\n" \ 208 " Vmtf : Use Siege-like heuristic (Move <n> literals to the front [8])\n" \ 209 " Vsids : Use Chaff-like heuristic (Use 1.0/0.<n> as decay factor [95])\n"\ 210 " Domain : Use domain knowledge in Vsids-like heuristic\n"\ 211 " Unit : Use Smodels-like heuristic (Default if --no-lookback)\n" \ 212 " None : Select the first free variable", FUN(arg) { Heuristic_t::Type h = Heuristic_t::Berkmin; uint32 n = 0u; \ 213 return arg>>h>>opt(n) && SET(SELF.heuId, (uint32)h) && (Heuristic_t::isLookback(h) || !n) && SET_OR_FILL(SELF.heuristic.param, n);},\ 214 GET((Heuristic_t::Type)SELF.heuId, SELF.heuristic.param)) 215OPTION(init_moms , "!,@2", ARG(flag()) , "Initialize heuristic with MOMS-score", STORE_FLAG(SELF.heuristic.moms), GET(SELF.heuristic.moms)) 216OPTION(score_res , ",@2" , ARG_EXT(arg("<score>"), DEFINE_ENUM_MAPPING(HeuParams::Score, \ 217 MAP("auto", HeuParams::score_auto), MAP("min", HeuParams::score_min), MAP("set", HeuParams::score_set), MAP("multiset", HeuParams::score_multi_set))),\ 218 "Resolution score {auto|min|set|multiset}", STORE_U(HeuParams::Score, SELF.heuristic.score), GET(static_cast<HeuParams::Score>(SELF.heuristic.score))) 219OPTION(score_other, ",@2" , ARG_EXT(arg("<arg>"), DEFINE_ENUM_MAPPING(HeuParams::ScoreOther, \ 220 MAP("auto", HeuParams::other_auto), MAP("no", HeuParams::other_no), MAP("loop", HeuParams::other_loop), MAP("all", HeuParams::other_all))),\ 221 "Score other learnt nogoods: {auto|no|loop|all}", STORE_U(HeuParams::ScoreOther, SELF.heuristic.other), GET(static_cast<HeuParams::ScoreOther>(SELF.heuristic.other))) 222OPTION(sign_def , ",@1" , ARG_EXT(arg("<sign>"),\ 223 DEFINE_ENUM_MAPPING(SolverStrategies::SignHeu, MAP("asp", SolverStrategies::sign_atom), MAP("pos", SolverStrategies::sign_pos), MAP("neg", SolverStrategies::sign_neg), MAP("rnd", SolverStrategies::sign_rnd))),\ 224 "Default sign: {asp|pos|neg|rnd}", STORE_U(SolverStrategies::SignHeu, SELF.signDef), GET((SolverStrategies::SignHeu)SELF.signDef)) 225OPTION(sign_fix , "!,@2", ARG(flag()) , "Disable sign heuristics and use default signs only", STORE_FLAG(SELF.signFix), GET(SELF.signFix)) 226OPTION(berk_huang , "!,@2", ARG(flag()) , "Enable Huang-scoring in Berkmin", STORE_FLAG(SELF.heuristic.huang), GET(SELF.heuristic.huang)) 227OPTION(vsids_acids, "!,@2", ARG(flag()) , "Enable acids-scheme in Vsids/Domain", STORE_FLAG(SELF.heuristic.acids), GET(SELF.heuristic.acids)) 228OPTION(vsids_progress, ",@2", NO_ARG, "Enable dynamic decaying scheme in Vsids/Domain\n"\ 229 " %A: <n>[,<i {1..100}>][,<c>]|(0=disable)\n"\ 230 " <n> : Set initial decay factor to 1.0/0.<n>\n"\ 231 " <i> : Set decay update to <i>/100.0 [1]\n"\ 232 " <c> : Decrease decay every <c> conflicts [5000]", \ 233 FUN(arg) { uint32 n = 80; uint32 i = 1; uint32 c = 5000; \ 234 return ITE(arg.off(), SET(SELF.heuristic.decay.init, 0), (arg >> n >> opt(i) >> opt(c))\ 235 && SET(SELF.heuristic.decay.init, n) && SET_LEQ(SELF.heuristic.decay.bump, i, 100) && SET(SELF.heuristic.decay.freq, c));}, \ 236 GET_IF(SELF.heuristic.decay.init, SELF.heuristic.decay.init, SELF.heuristic.decay.bump, SELF.heuristic.decay.freq)) 237OPTION(nant , "!,@2", ARG(flag()) , "Prefer negative antecedents of P in heuristic", STORE_FLAG(SELF.heuristic.nant), GET(SELF.heuristic.nant)) 238OPTION(dom_mod , ",@1" , ARG_EXT(arg("<arg>"), DEFINE_ENUM_MAPPING(HeuParams::DomMod, \ 239 MAP("level", HeuParams::mod_level), MAP("pos", HeuParams::mod_spos), MAP("true", HeuParams::mod_true),\ 240 MAP("neg", HeuParams::mod_sneg), MAP("false", HeuParams::mod_false), MAP("init", HeuParams::mod_init), MAP("factor", HeuParams::mod_factor))\ 241 DEFINE_ENUM_MAPPING(HeuParams::DomPref, MAP("all", HeuParams::pref_atom), MAP("scc", HeuParams::pref_scc), MAP("hcc", HeuParams::pref_hcc),\ 242 MAP("disj", HeuParams::pref_disj), MAP("opt", HeuParams::pref_min), MAP("show", HeuParams::pref_show))),\ 243 "Default modification for domain heuristic\n"\ 244 " %A: (no|<mod>[,<pick>])\n"\ 245 " <mod> : Modifier {level|pos|true|neg|false|init|factor}\n"\ 246 " <pick> : Apply <mod> to (all | <list {scc|hcc|disj|opt|show}>) atoms", \ 247 FUN(arg) { HeuParams::DomMod modK; unsigned modN = 0; Set<HeuParams::DomPref> k; bool ok = true;\ 248 if (!arg.off()) { ok = ITE(arg.peek() >= 'A', arg >> modK && SET(modN, uint32(modK)), arg >> modN && modN > 0u && modN < 8u); }\ 249 return ok && (arg.off() || arg >> opt(k)) && SET(SELF.heuristic.domMod, modN) && SET(SELF.heuristic.domPref, k.value());},\ 250 GET_FUN(str) { Set<HeuParams::DomMod> mod(SELF.heuristic.domMod); Set<HeuParams::DomPref> pick(SELF.heuristic.domPref); \ 251 ITE(mod.value() && pick.value(), str << mod << pick, str << mod); }) 252OPTION(save_progress, "", ARG(implicit("1")->arg("<n>")), "Use RSat-like progress saving on backjumps > %A", STORE_OR_FILL(SELF.saveProgress), GET(SELF.saveProgress)) 253OPTION(init_watches , ",@2", ARG_EXT(arg("<arg>"), DEFINE_ENUM_MAPPING(SolverStrategies::WatchInit, \ 254 MAP("rnd", SolverStrategies::watch_rand), MAP("first", SolverStrategies::watch_first), MAP("least", SolverStrategies::watch_least))),\ 255 "Watched literal initialization: {rnd|first|least}", STORE_U(SolverStrategies::WatchInit, SELF.initWatches), GET(static_cast<SolverStrategies::WatchInit>(SELF.initWatches))) 256OPTION(update_mode , ",@2", ARG_EXT(arg("<mode>"), DEFINE_ENUM_MAPPING(SolverStrategies::UpdateMode, \ 257 MAP("propagate", SolverStrategies::update_on_propagate), MAP("conflict", SolverStrategies::update_on_conflict))),\ 258 "Process messages on {propagate|conflict}", STORE_U(SolverStrategies::UpdateMode, SELF.upMode), GET(static_cast<SolverStrategies::UpdateMode>(SELF.upMode))) 259OPTION(acyc_prop, ",@2", ARG(implicit("1")->arg("{0..1}")), "Use backward inference in acyc propagation", \ 260 FUN(arg) { uint32 x; return arg>>x && SET_LEQ(SELF.acycFwd, (1u-x), 1u); }, GET(1u-SELF.acycFwd)) 261OPTION(seed , "" , ARG(arg("<n>")),"Set random number generator's seed to %A", STORE(SELF.seed), GET(SELF.seed)) 262OPTION(no_lookback , "" , ARG(flag()), "Disable all lookback strategies\n", STORE_FLAG(SELF.search),GET(static_cast<bool>(SELF.search == SolverStrategies::no_learning))) 263OPTION(forget_on_step, "" , ARG_EXT(arg("<opts>"), DEFINE_ENUM_MAPPING(SolverParams::Forget, \ 264 MAP("varScores", SolverParams::forget_heuristic), MAP("signs", SolverParams::forget_signs), MAP("lemmaScores", SolverParams::forget_activities), MAP("lemmas", SolverParams::forget_learnts))),\ 265 "Configure forgetting on (incremental) step\n"\ 266 " %A: <list {varScores|signs|lemmaScores|lemmas}>|<mask {0..15}>\n",\ 267 FUN(arg) { Set<SolverParams::Forget> s; return (arg.off() || arg >> s) && SET(SELF.forgetSet, s.value()); },\ 268 GET(Set<SolverParams::Forget>(SELF.forgetSet))) 269OPTION(strengthen , "!" , ARG_EXT(arg("<X>"),\ 270 DEFINE_ENUM_MAPPING(SolverStrategies::CCMinType, MAP("local", SolverStrategies::cc_local), MAP("recursive", SolverStrategies::cc_recursive))\ 271 DEFINE_ENUM_MAPPING(SolverStrategies::CCMinAntes, MAP("all", SolverStrategies::all_antes), MAP("short", SolverStrategies::short_antes), MAP("binary", SolverStrategies::binary_antes))), \ 272 "Use MiniSAT-like conflict nogood strengthening\n" \ 273 " %A: <mode>[,<type>][,<bump {yes|no}>]\n" \ 274 " <mode>: Use {local|recursive} self-subsumption check\n" \ 275 " <type>: Follow {all|short|binary} antecedents [all]\n" \ 276 " <bump>: Bump activities of antecedents [yes]", FUN(arg) {\ 277 SolverStrategies::CCMinType m = SolverStrategies::cc_local; SolverStrategies::CCMinAntes t = SolverStrategies::no_antes; bool b = true; \ 278 return (arg.off() || arg>>m>>opt(t = SolverStrategies::all_antes)>>opt(b)) && SET(SELF.ccMinAntes, (uint32)t) && SET(SELF.ccMinRec, (uint32)m) && SET(SELF.ccMinKeepAct, uint32(!b)); }, \ 279 GET_IF(SELF.ccMinAntes != SolverStrategies::no_antes, (SolverStrategies::CCMinType)SELF.ccMinRec, (SolverStrategies::CCMinAntes)SELF.ccMinAntes, ITE(SELF.ccMinKeepAct, "no", "yes"))) 280OPTION(otfs , "" , ARG(implicit("1")->arg("{0..2}")), "Enable {1=partial|2=full} on-the-fly subsumption", STORE_LEQ(SELF.otfs, 2u), GET(SELF.otfs)) 281OPTION(update_lbd , "!,@2" , ARG_EXT(arg("<arg>"), DEFINE_ENUM_MAPPING(SolverStrategies::LbdMode, \ 282 MAP("less", SolverStrategies::lbd_updated_less), MAP("glucose", SolverStrategies::lbd_update_glucose), MAP("pseudo", SolverStrategies::lbd_update_pseudo))),\ 283 "Configure LBD updates during conflict resolution\n" \ 284 " %A: <mode {less|glucose|pseudo}>[,<n {0..127}>]\n" \ 285 " less : update to X = new LBD iff X < previous LBD\n" \ 286 " glucose: update to X = new LBD iff X+1 < previous LBD\n" \ 287 " pseudo : update to X = new LBD+1 iff X < previous LBD\n" \ 288 " <n> : Protect updated nogoods on next reduce if X <= <n>",\ 289 FUN(arg) { SolverStrategies::LbdMode n = SolverStrategies::lbd_fixed; uint32 m = 0; \ 290 return (arg.off() || (arg >> n >> opt(m) && n > 0)) && SET(SELF.updateLbd, uint32(n)) && SET_LEQ(search->reduce.strategy.protect, m, uint32(Clasp::LBD_MAX));},\ 291 GET_IF(SELF.updateLbd, (SolverStrategies::LbdMode)SELF.updateLbd, search->reduce.strategy.protect)) 292OPTION(update_act , ",@2", ARG(flag()), "Enable LBD-based activity bumping", STORE_FLAG(SELF.bumpVarAct), GET(SELF.bumpVarAct)) 293OPTION(reverse_arcs, "" , ARG(implicit("1")->arg("{0..3}")), "Enable ManySAT-like inverse-arc learning", STORE_LEQ(SELF.reverseArcs, 3u), GET(SELF.reverseArcs)) 294OPTION(contraction , "!,@2", ARG_EXT(arg("<arg>"),\ 295 DEFINE_ENUM_MAPPING(SolverStrategies::CCRepMode, MAP("no", SolverStrategies::cc_no_replace), MAP("decisionSeq", SolverStrategies::cc_rep_decision), MAP("allUIP", SolverStrategies::cc_rep_uip), MAP("dynamic", SolverStrategies::cc_rep_dynamic))),\ 296 "Configure handling of long learnt nogoods\n" 297 " %A: <n>[,<rep>]\n"\ 298 " <n> : Contract nogoods if size > <n> (0=disable)\n"\ 299 " <rep>: Nogood replacement {no|decisionSeq|allUIP|dynamic} [no]\n", FUN(arg) { uint32 n = 0; SolverStrategies::CCRepMode r = SolverStrategies::cc_no_replace;\ 300 return (arg.off() || (arg>>n>>opt(r) && n != 0u)) && SET_OR_FILL(SELF.compress, n) && SET(SELF.ccRepMode, uint32(r));},\ 301 GET_IF(SELF.compress, SELF.compress, (SolverStrategies::CCRepMode)SELF.ccRepMode)) 302OPTION(loops, "" , ARG_EXT(arg("<type>"), DEFINE_ENUM_MAPPING(DefaultUnfoundedCheck::ReasonStrategy,\ 303 MAP("common" , DefaultUnfoundedCheck::common_reason) , MAP("shared", DefaultUnfoundedCheck::shared_reason), \ 304 MAP("distinct", DefaultUnfoundedCheck::distinct_reason), MAP("no", DefaultUnfoundedCheck::only_reason))),\ 305 "Configure learning of loop nogoods\n" \ 306 " %A: {common|distinct|shared|no}\n" \ 307 " common : Create loop nogoods for atoms in an unfounded set\n" \ 308 " distinct: Create distinct loop nogood for each atom in an unfounded set\n" \ 309 " shared : Create loop formula for a whole unfounded set\n" \ 310 " no : Do not learn loop formulas\n", FUN(arg) {DefaultUnfoundedCheck::ReasonStrategy x; return arg>>x && SET(SELF.loopRep, (uint32)x);},\ 311 GET(static_cast<DefaultUnfoundedCheck::ReasonStrategy>(SELF.loopRep))) 312GROUP_END(SELF) 313#undef CLASP_SOLVER_OPTIONS 314#undef SELF 315#endif 316 317//! Search-related options (see SolveParams). 318#if defined(CLASP_SEARCH_OPTIONS) 319#define SELF CLASP_SEARCH_OPTIONS 320GROUP_BEGIN(SELF) 321OPTION(partial_check, "", ARG(implicit("50")), "Configure partial stability tests\n" \ 322 " %A: <p>[,<h>] / Implicit: %I\n" \ 323 " <p>: Partial check skip percentage\n" \ 324 " <h>: Init/update value for high bound ([0]=umax)", FUN(arg) {\ 325 uint32 p = 0; uint32 h = 0; \ 326 return (arg.off() || (arg>>p>>opt(h) && p)) && SET_LEQ(SELF.fwdCheck.highPct, p, 100u) && SET_OR_ZERO(SELF.fwdCheck.highStep, h);},\ 327 GET_IF(SELF.fwdCheck.highPct, SELF.fwdCheck.highPct, SELF.fwdCheck.highStep)) 328OPTION(sign_def_disj, ",@2", ARG(arg("<sign>")), "Default sign for atoms in disjunctions", STORE_U(SolverStrategies::SignHeu, SELF.fwdCheck.signDef), GET((SolverStrategies::SignHeu)SELF.fwdCheck.signDef)) 329OPTION(rand_freq, "!", ARG(arg("<p>")), "Make random decisions with probability %A", FUN(arg) {\ 330 double f = 0.0; \ 331 return (arg.off() || arg>>f) && SET_R(SELF.randProb, (float)f, 0.0f, 1.0f);}, GET(SELF.randProb)) 332OPTION(rand_prob, "", ARG(arg("<n>[,<m>]")), "Do <n> random searches with [<m>=100] conflicts",\ 333 FUN(arg) { uint32 n1 = 0; uint32 n2 = 100;\ 334 return (arg.off() || (arg>>n1>>opt(n2) && n1)) && SET_OR_FILL(SELF.randRuns, n1) && SET_OR_FILL(SELF.randConf, n2);},\ 335 GET_IF(SELF.randRuns, SELF.randRuns,SELF.randConf)) 336#undef SELF 337//! Options for configuring the restart strategy of a solver. 338#define SELF CLASP_SEARCH_RESTART_OPTIONS 339#if defined(NOTIFY_SUBGROUPS) 340GROUP_BEGIN(SELF) 341#endif 342OPTION(restarts, "!,r", ARG(arg("<sched>")), "Configure restart policy\n" \ 343 " %A: <type {D|F|L|x|+}>,<n {1..umax}>[,<args>][,<lim>]\n" \ 344 " F,<n> : Run fixed sequence of <n> conflicts\n" \ 345 " L,<n> : Run Luby et al.'s sequence with unit length <n>\n" \ 346 " x,<n>,<f>: Run geometric seq. of <n>*(<f>^i) conflicts (<f> >= 1.0)\n" \ 347 " +,<n>,<m>: Run arithmetic seq. of <n>+(<m>*i) conflicts (<m {0..umax}>)\n"\ 348 " ...,<lim>: Repeat seq. every <lim>+j restarts (<type> != F)\n" \ 349 " D,<n>,<f>: Restart based on moving LBD average over last <n> conflicts\n" \ 350 " Mavg(<n>,LBD)*<f> > avg(LBD)\n" \ 351 " use conflict level average if <lim> > 0 and avg(LBD) > <lim>\n"\ 352 " no|0 : Disable restarts", FUN(arg) { return ITE(arg.off(), (SELF.disable(),true), \ 353 arg>>SELF.sched && SET(SELF.dynRestart, uint32(SELF.sched.type == ScheduleStrategy::User)));}, GET(SELF.sched)) 354OPTION(reset_restarts , ",@2", ARG_EXT(arg("<arg>"), DEFINE_ENUM_MAPPING(RestartParams::SeqUpdate, \ 355 MAP("no",RestartParams::seq_continue), MAP("repeat", RestartParams::seq_repeat), MAP("disable", RestartParams::seq_disable))),\ 356 "Update restart seq. on model {no|repeat|disable}",\ 357 STORE_U(RestartParams::SeqUpdate, SELF.upRestart), GET(static_cast<RestartParams::SeqUpdate>(SELF.upRestart))) 358OPTION(local_restarts , "!" , ARG(flag()), "Use Ryvchin et al.'s local restarts", STORE_FLAG(SELF.cntLocal), GET(SELF.cntLocal)) 359OPTION(counter_restarts, "" , ARG(arg("<arg>")), "Use counter implication restarts\n" \ 360 " %A: (<rate>[,<bump>] | {0|no})\n" \ 361 " <rate>: Interval in number of restarts\n" \ 362 " <bump>: Bump factor applied to indegrees", \ 363 FUN(arg) { uint32 n = 0; uint32 m = SELF.counterBump; \ 364 return (arg.off() || (arg >> n >> opt(m) && n > 0)) && SET_OR_FILL(SELF.counterRestart, n) && SET_OR_FILL(SELF.counterBump, m); },\ 365 GET_IF(SELF.counterRestart, SELF.counterRestart, SELF.counterBump)) 366OPTION(block_restarts , "" , ARG(arg("<arg>")), "Use glucose-style blocking restarts\n" \ 367 " %A: <n>[,<R {1.0..5.0}>][,<c>]\n" \ 368 " <n>: Window size for moving average (0=disable blocking)\n" \ 369 " <R>: Block restart if assignment > average * <R> [1.4]\n" \ 370 " <c>: Disable blocking for the first <c> conflicts [10000]\n", FUN(arg) { \ 371 uint32 n = 0; double R = 0.0; uint32 x = 0;\ 372 return (arg.off() || (arg>>n>>opt(R = 1.4)>>opt(x = 10000) && n && R >= 1.0 && R <= 5.0))\ 373 && SET(SELF.blockWindow, n) && SET(SELF.blockScale, (float)R) && SET_OR_FILL(SELF.blockFirst, x);},\ 374 GET_IF(SELF.blockWindow, SELF.blockWindow, SELF.blockScale, SELF.blockFirst)) 375OPTION(shuffle , "!" , ARG(arg("<n1>,<n2>")), "Shuffle problem after <n1>+(<n2>*i) restarts\n", FUN(arg) { uint32 n1 = 0; uint32 n2 = 0;\ 376 return (arg.off() || (arg>>n1>>opt(n2) && n1)) && SET_OR_FILL(SELF.shuffle, n1) && SET_OR_FILL(SELF.shuffleNext, n2);},\ 377 GET_IF(SELF.shuffle, SELF.shuffle, SELF.shuffleNext)) 378#if defined(NOTIFY_SUBGROUPS) 379GROUP_END(SELF) 380#endif 381#undef SELF 382#undef CLASP_SEARCH_RESTART_OPTIONS 383//! Options for configuring the deletion strategy of a solver. 384#define SELF CLASP_SEARCH_REDUCE_OPTIONS 385#if defined(NOTIFY_SUBGROUPS) 386GROUP_BEGIN(SELF) 387#endif 388OPTION(deletion , "!,d", ARG_EXT(defaultsTo("basic,75,activity")->state(Value::value_defaulted), DEFINE_ENUM_MAPPING(ReduceStrategy::Algorithm,\ 389 MAP("basic", ReduceStrategy::reduce_linear), MAP("sort", ReduceStrategy::reduce_stable),\ 390 MAP("ipSort", ReduceStrategy::reduce_sort) , MAP("ipHeap", ReduceStrategy::reduce_heap))\ 391 DEFINE_ENUM_MAPPING(ReduceStrategy::Score, MAP("activity",ReduceStrategy::score_act), MAP("lbd", ReduceStrategy::score_lbd), MAP("mixed", ReduceStrategy::score_both))),\ 392 "Configure deletion algorithm [%D]\n" \ 393 " %A: <algo>[,<n {1..100}>][,<sc>]\n" \ 394 " <algo>: Use {basic|sort|ipSort|ipHeap} algorithm\n" \ 395 " <n> : Delete at most <n>%% of nogoods on reduction [75]\n" \ 396 " <sc> : Use {activity|lbd|mixed} nogood scores [activity]\n" \ 397 " no : Disable nogood deletion", FUN(arg){\ 398 ReduceStrategy::Algorithm algo = ReduceStrategy::reduce_linear; uint32 n; ReduceStrategy::Score sc;\ 399 return ITE(arg.off(), (SELF.disable(), true), arg>>algo>>opt(n = 75)>>opt(sc = ReduceStrategy::score_act)\ 400 && SET(SELF.strategy.algo, (uint32)algo) && SET_R(SELF.strategy.fReduce, n, 1, 100) && SET(SELF.strategy.score, (uint32)sc));},\ 401 GET_IF(SELF.strategy.fReduce, (ReduceStrategy::Algorithm)SELF.strategy.algo, SELF.strategy.fReduce,(ReduceStrategy::Score)SELF.strategy.score)) 402OPTION(del_grow , "!", NO_ARG, "Configure size-based deletion policy\n" \ 403 " %A: <f>[,<g>][,<sched>] (<f> >= 1.0)\n" \ 404 " <f> : Keep at most T = X*(<f>^i) learnt nogoods with X being the\n"\ 405 " initial limit and i the number of times <sched> fired\n" \ 406 " <g> : Stop growth once T > P*<g> (0=no limit) [3.0]\n" \ 407 " <sched> : Set grow schedule (<type {F|L|x|+}>) [grow on restart]", FUN(arg){ double f; double g; ScheduleStrategy sc = ScheduleStrategy::def();\ 408 return ITE(arg.off(), (SELF.growSched = ScheduleStrategy::none(), SELF.fGrow = 0.0f, true),\ 409 arg>>f>>opt(g = 3.0)>>opt(sc) && SET_R(SELF.fGrow, (float)f, 1.0f, FLT_MAX) && SET_R(SELF.fMax, (float)g, 0.0f, FLT_MAX)\ 410 && (sc.defaulted() || sc.type != ScheduleStrategy::User) && (SELF.growSched=sc, true));},\ 411 GET_FUN(str) { if (SELF.fGrow == 0.0f) str<<off; else { str<<SELF.fGrow<<SELF.fMax; if (!SELF.growSched.disabled()) str<<SELF.growSched;}}) 412OPTION(del_cfl , "!", ARG(arg("<sched>")), "Configure conflict-based deletion policy\n" \ 413 " %A: <type {F|L|x|+}>,<args>... (see restarts)", FUN(arg){\ 414 return ITE(arg.off(), (SELF.cflSched=ScheduleStrategy::none()).disabled(), arg>>SELF.cflSched && SELF.cflSched.type != ScheduleStrategy::User);}, GET(SELF.cflSched)) 415OPTION(del_init , "" , ARG(defaultsTo("3.0")->state(Value::value_defaulted)), "Configure initial deletion limit\n"\ 416 " %A: <f>[,<n>,<o>] (<f> > 0)\n" \ 417 " <f> : Set initial limit to P=estimated problem size/<f> [%D]\n" \ 418 " <n>,<o>: Clamp initial limit to the range [<n>,<n>+<o>]" , FUN(arg) { double f; uint32 lo = 10; uint32 hi = UINT32_MAX;\ 419 return arg>>f>>opt(lo)>>opt(hi) && f > 0.0 && (SELF.fInit = float(1.0 / f)) > 0 && SET_OR_FILL(SELF.initRange.lo, lo) && SET_OR_FILL(SELF.initRange.hi, (uint64(hi)+SELF.initRange.lo));},\ 420 GET_IF(SELF.fInit, 1.0/SELF.fInit, SELF.initRange.lo, SELF.initRange.hi - SELF.initRange.lo)) 421OPTION(del_estimate, "", ARG(arg("0..3")->implicit("1")), "Use estimated problem complexity in limits", STORE_LEQ(SELF.strategy.estimate, 3u), GET(SELF.strategy.estimate)) 422OPTION(del_max , "!", ARG(arg("<n>,<X>")), "Keep at most <n> learnt nogoods taking up to <X> MB", FUN(arg) { uint32 n = UINT32_MAX; uint32 mb = 0; \ 423 return (arg.off() || arg>>n>>opt(mb)) && SET_GEQ(SELF.maxRange, n, 1u) && SET(SELF.memMax, mb);}, GET(SELF.maxRange, SELF.memMax)) 424OPTION(del_glue , "", NO_ARG, "Configure glue clause handling\n" \ 425 " %A: <n {0..15}>[,<m {0|1}>]\n" \ 426 " <n>: Do not delete nogoods with LBD <= <n>\n" \ 427 " <m>: Count (0) or ignore (1) glue clauses in size limit [0]", FUN(arg) {uint32 lbd; uint32 m = 0; \ 428 return arg>>lbd>>opt(m) && SET(SELF.strategy.glue, lbd) && SET(SELF.strategy.noGlue, m);}, GET(SELF.strategy.glue, SELF.strategy.noGlue)) 429OPTION(del_on_restart, "", ARG(arg("<n>")), "Delete %A%% of learnt nogoods on each restart", STORE_LEQ(SELF.strategy.fRestart, 100u), GET(SELF.strategy.fRestart)) 430#if defined(NOTIFY_SUBGROUPS) 431GROUP_END(SELF) 432#endif 433#undef SELF 434#undef CLASP_SEARCH_REDUCE_OPTIONS 435GROUP_END(CLASP_SEARCH_OPTIONS) 436#undef CLASP_SEARCH_OPTIONS 437#endif 438 439//! ASP-front-end options stored in an Clasp::Asp::LogicProgram::AspOptions object. 440#if defined(CLASP_ASP_OPTIONS) 441#define SELF CLASP_ASP_OPTIONS 442GROUP_BEGIN(SELF) 443OPTION(trans_ext , "!", ARG_EXT(arg("<mode>"), DEFINE_ENUM_MAPPING(Asp::LogicProgram::ExtendedRuleMode,\ 444 MAP("no" , Asp::LogicProgram::mode_native) , MAP("all" , Asp::LogicProgram::mode_transform),\ 445 MAP("choice", Asp::LogicProgram::mode_transform_choice), MAP("card", Asp::LogicProgram::mode_transform_card),\ 446 MAP("weight", Asp::LogicProgram::mode_transform_weight), MAP("scc" , Asp::LogicProgram::mode_transform_scc),\ 447 MAP("integ" , Asp::LogicProgram::mode_transform_integ) , MAP("dynamic", Asp::LogicProgram::mode_transform_dynamic))),\ 448 "Configure handling of extended rules\n"\ 449 " %A: {all|choice|card|weight|integ|dynamic}\n"\ 450 " all : Transform all extended rules to basic rules\n"\ 451 " choice : Transform choice rules, but keep cardinality and weight rules\n"\ 452 " card : Transform cardinality rules, but keep choice and weight rules\n"\ 453 " weight : Transform cardinality and weight rules, but keep choice rules\n"\ 454 " scc : Transform \"recursive\" cardinality and weight rules\n"\ 455 " integ : Transform cardinality integrity constraints\n"\ 456 " dynamic: Transform \"simple\" extended rules, but keep more complex ones", STORE(SELF.erMode), GET((Asp::LogicProgram::ExtendedRuleMode)SELF.erMode)) 457OPTION(eq, "", ARG(arg("<n>")), "Configure equivalence preprocessing\n" \ 458 " Run for at most %A iterations (-1=run to fixpoint)", STORE_OR_FILL(SELF.iters), GET(SELF.iters)) 459OPTION(backprop ,"!,@1", ARG(flag()), "Use backpropagation in ASP-preprocessing", STORE_FLAG(SELF.backprop), GET(SELF.backprop)) 460OPTION(supp_models , ",@1", ARG(flag()), "Compute supported models", STORE_FLAG(SELF.suppMod), GET(SELF.suppMod)) 461OPTION(no_ufs_check, ",@1", ARG(flag()), "Disable unfounded set check", STORE_FLAG(SELF.noSCC), GET(SELF.noSCC)) 462OPTION(no_gamma , ",@1", ARG(flag()), "Do not add gamma rules for non-hcf disjunctions", STORE_FLAG(SELF.noGamma), GET(SELF.noGamma)) 463OPTION(eq_dfs , ",@2", ARG(flag()), "Enable df-order in eq-preprocessing", STORE_FLAG(SELF.dfOrder), GET(SELF.dfOrder)) 464OPTION(dlp_old_map , ",@3", ARG(flag()), "Enable old mapping for disjunctive LPs", STORE_FLAG(SELF.oldMap), GET(SELF.oldMap)) 465GROUP_END(SELF) 466#undef CLASP_ASP_OPTIONS 467#undef SELF 468#endif 469 470//! Options for the solving algorithm (see Clasp::SolveOptions) 471#if defined(CLASP_SOLVE_OPTIONS) 472#define SELF CLASP_SOLVE_OPTIONS 473GROUP_BEGIN(SELF) 474OPTION(solve_limit , ",@1", ARG(arg("<n>[,<m>]")), "Stop search after <n> conflicts or <m> restarts\n", FUN(arg) {\ 475 uint32 n = UINT32_MAX; uint32 m = UINT32_MAX;\ 476 return ((arg.off() && arg.peek() != '0') || arg>>n>>opt(m)) && (SELF.limit=SolveLimits(n == UINT32_MAX ? UINT64_MAX : n, m == UINT32_MAX ? UINT64_MAX : m), true);},\ 477 GET((uint32)Range<uint64>(0u,UINT32_MAX).clamp(SELF.limit.conflicts),(uint32)Range<uint64>(0u,UINT32_MAX).clamp(SELF.limit.restarts))) 478#if CLASP_HAS_THREADS 479OPTION(parallel_mode, ",t", ARG_EXT(arg("<arg>"), DEFINE_ENUM_MAPPING(SolveOptions::Algorithm::SearchMode,\ 480 MAP("compete", SolveOptions::Algorithm::mode_compete), MAP("split", SolveOptions::Algorithm::mode_split))),\ 481 "Run parallel search with given number of threads\n" \ 482 " %A: <n {1..64}>[,<mode {compete|split}>]\n" \ 483 " <n> : Number of threads to use in search\n"\ 484 " <mode>: Run competition or splitting based search [compete]\n", FUN(arg){\ 485 uint32 n; SolveOptions::Algorithm::SearchMode mode;\ 486 return arg>>n>>opt(mode = SolveOptions::Algorithm::mode_compete) && SET_R(SELF.algorithm.threads, n, 1u, 64u) && SET(SELF.algorithm.mode, mode);},\ 487 GET(SELF.algorithm.threads, (SolveOptions::Algorithm::SearchMode)SELF.algorithm.mode)) 488OPTION(global_restarts, ",@1", ARG(arg("<X>")), "Configure global restart policy\n" \ 489 " %A: <n>[,<sched>]\n" \ 490 " <n> : Maximal number of global restarts (0=disable)\n" \ 491 " <sched>: Restart schedule [x,100,1.5] (<type {F|L|x|+}>)\n", FUN(arg) {\ 492 return ITE(arg.off(), (SELF.restarts = SolveOptions::GRestarts(), true), arg>>SELF.restarts.maxR>>opt(SELF.restarts.sched = ScheduleStrategy())\ 493 && SELF.restarts.maxR && SELF.restarts.sched.type != ScheduleStrategy::User);},\ 494 GET_IF(SELF.restarts.maxR, SELF.restarts.maxR, SELF.restarts.sched)) 495OPTION(distribute, "!,@1", ARG_EXT(defaultsTo("conflict,global,4"), \ 496 DEFINE_ENUM_MAPPING(Distributor::Policy::Types, MAP("all", Distributor::Policy::all), MAP("short", Distributor::Policy::implicit), MAP("conflict", Distributor::Policy::conflict), MAP("loop" , Distributor::Policy::loop))\ 497 DEFINE_ENUM_MAPPING(SolveOptions::Distribution::Mode, MAP("global", SolveOptions::Distribution::mode_global), MAP("local", SolveOptions::Distribution::mode_local))),\ 498 "Configure nogood distribution [%D]\n" \ 499 " %A: <type>[,<mode>][,<lbd {0..127}>][,<size>]\n" \ 500 " <type> : Distribute {all|short|conflict|loop} nogoods\n" \ 501 " <mode> : Use {global|local} distribution [global]\n" \ 502 " <lbd> : Distribute only if LBD <= <lbd> [4]\n" \ 503 " <size> : Distribute only if size <= <size> [-1]", \ 504 FUN(arg) { Distributor::Policy::Types type; SolveOptions::Distribution::Mode mode = SolveOptions::Distribution::mode_global; uint32 lbd; uint32 size; \ 505 if (arg.off()) { SELF.distribute.policy() = Distributor::Policy(0, 0, 0); return true; } 506 return (arg >> type) && (arg.peek() < 'A' || arg >> opt(mode)) && arg >> opt(lbd = 4) >> opt(size = UINT32_MAX) 507 && SET(SELF.distribute.types, (uint32)type) && SET(SELF.distribute.mode, (uint32)mode) && SET(SELF.distribute.lbd, lbd) && SET_OR_FILL(SELF.distribute.size, size);},\ 508 GET_FUN(str) { ITE(!SELF.distribute.types, str << off,\ 509 str << (Distributor::Policy::Types)SELF.distribute.types << (SolveOptions::Distribution::Mode)SELF.distribute.mode << SELF.distribute.lbd << SELF.distribute.size); }) 510OPTION(integrate, ",@1", ARG_EXT(defaultsTo("gp")->state(Value::value_defaulted),\ 511 DEFINE_ENUM_MAPPING(SolveOptions::Integration::Filter, \ 512 MAP("all", SolveOptions::Integration::filter_no), MAP("gp", SolveOptions::Integration::filter_gp),\ 513 MAP("unsat", SolveOptions::Integration::filter_sat), MAP("active", SolveOptions::Integration::filter_heuristic))\ 514 DEFINE_ENUM_MAPPING(SolveOptions::Integration::Topology, \ 515 MAP("all" , SolveOptions::Integration::topo_all) , MAP("ring" , SolveOptions::Integration::topo_ring),\ 516 MAP("cube", SolveOptions::Integration::topo_cube), MAP("cubex", SolveOptions::Integration::topo_cubex))),\ 517 "Configure nogood integration [%D]\n" \ 518 " %A: <pick>[,<n>][,<topo>]\n" \ 519 " <pick>: Add {all|unsat|gp(unsat wrt guiding path)|active} nogoods\n" \ 520 " <n> : Always keep at least last <n> integrated nogoods [1024]\n" \ 521 " <topo>: Accept nogoods from {all|ring|cube|cubex} peers [all]\n", FUN(arg) {\ 522 SolveOptions::Integration::Filter pick = SolveOptions::Integration::filter_no; uint32 n; SolveOptions::Integration::Topology topo; 523 return arg>>pick>>opt(n = 1024)>>opt(topo = SolveOptions::Integration::topo_all) && SET(SELF.integrate.filter, (uint32)pick) && SET_OR_FILL(SELF.integrate.grace, n) && SET(SELF.integrate.topo, (uint32)topo);},\ 524 GET((SolveOptions::Integration::Filter)SELF.integrate.filter, SELF.integrate.grace, (SolveOptions::Integration::Topology)SELF.integrate.topo)) 525#endif 526OPTION(enum_mode , ",e", ARG_EXT(defaultsTo("auto")->state(Value::value_defaulted), DEFINE_ENUM_MAPPING(SolveOptions::EnumType,\ 527 MAP("bt", SolveOptions::enum_bt), MAP("record", SolveOptions::enum_record), MAP("domRec", SolveOptions::enum_dom_record),\ 528 MAP("brave", SolveOptions::enum_brave), MAP("cautious", SolveOptions::enum_cautious), MAP("query", SolveOptions::enum_query),\ 529 MAP("auto", SolveOptions::enum_auto), MAP("user", SolveOptions::enum_user))),\ 530 "Configure enumeration algorithm [%D]\n" \ 531 " %A: {bt|record|brave|cautious|auto}\n" \ 532 " bt : Backtrack decision literals from solutions\n" \ 533 " record : Add nogoods for computed solutions\n" \ 534 " domRec : Add nogoods over true domain atoms\n" \ 535 " brave : Compute brave consequences (union of models)\n" \ 536 " cautious: Compute cautious consequences (intersection of models)\n" \ 537 " auto : Use bt for enumeration and record for optimization", STORE(SELF.enumMode), GET(SELF.enumMode)) 538OPTION(project, "!", ARG_EXT(arg("<arg>")->implicit("auto,3"), DEFINE_ENUM_MAPPING(ProjectMode_t::Mode,\ 539 MAP("auto", ProjectMode_t::Implicit), MAP("show", ProjectMode_t::Output), MAP("project", ProjectMode_t::Explicit))),\ 540 "Enable projective solution enumeration\n" \ 541 " %A: {show|project|auto}[,<bt {0..3}>] (Implicit: %I)\n" \ 542 " Project to atoms in show or project directives, or\n" \ 543 " select depending on the existence of a project directive\n" \ 544 " <bt> : Additional options for enumeration algorithm 'bt'\n" \ 545 " Use activity heuristic (1) when selecting backtracking literal\n" \ 546 " and/or progress saving (2) when retracting solution literals", \ 547 FUN(arg) { ProjectMode m = ProjectMode_t::Implicit; uint32 p = 0; \ 548 return (arg.off() || (arg.peek() < '9' && arg >> p) || ((arg >> m >> opt(p)) && (p = (p<<1)|1) != 0u)) && SET(SELF.proMode, m) && SET_LEQ(SELF.project, p, 7u);},\ 549 GET_IF(SELF.project, SELF.proMode, SELF.project >> 1)) 550OPTION(models, ",n", ARG(arg("<n>")), "Compute at most %A models (0 for all)\n", STORE(SELF.numModels), GET(SELF.numModels)) 551OPTION(opt_mode , "", ARG_EXT(arg("<arg>"), DEFINE_ENUM_MAPPING(MinimizeMode_t::Mode,\ 552 MAP("opt" , MinimizeMode_t::optimize), MAP("enum" , MinimizeMode_t::enumerate),\ 553 MAP("optN", MinimizeMode_t::enumOpt) , MAP("ignore", MinimizeMode_t::ignore))),\ 554 "Configure optimization algorithm\n"\ 555 " %A: <mode {opt|enum|optN|ignore}>[,<bound>...]\n" \ 556 " opt : Find optimal model\n" \ 557 " enum : Find models with costs <= <bound>\n" \ 558 " optN : Find optimum, then enumerate optimal models\n"\ 559 " ignore: Ignore optimize statements\n" \ 560 " <bound> : Set initial bound for objective function(s)", \ 561 FUN(arg) { MinimizeMode_t::Mode m = MinimizeMode_t::optimize; SumVec B; return (arg >> m >> opt(B)) && SET(SELF.optMode, m) && (SELF.optBound.swap(B), true); }, \ 562 GET_FUN(str) { str << SELF.optMode; if (!SELF.optBound.empty()) str << SELF.optBound; }) 563GROUP_END(SELF) 564#undef CLASP_SOLVE_OPTIONS 565#undef SELF 566#endif 567 568#undef GROUP_BEGIN 569#undef GROUP_END 570#undef OPTION 571#undef NOTIFY_SUBGROUPS 572#undef ARG 573#undef ARG_EXT 574#undef NO_ARG 575