1
2 /*
3 * File Options.cpp.
4 *
5 * This file is part of the source code of the software program
6 * Vampire. It is protected by applicable
7 * copyright laws.
8 *
9 * This source code is distributed under the licence found here
10 * https://vprover.github.io/license.html
11 * and in the source directory
12 *
13 * In summary, you are allowed to use Vampire for non-commercial
14 * purposes but not allowed to distribute, modify, copy, create derivatives,
15 * or use in competitions.
16 * For other uses of Vampire please contact developers for a different
17 * licence, which we will make an effort to provide.
18 */
19 /**
20 * @file Options.cpp
21 * Implements Vampire options.
22 *
23 * @since 06/06/2001 Manchester, completely rewritten
24 *
25 * @since Sep 14 rewritten by Giles
26 *
27 *
28 * IMPORTANT --> see .hpp file for instructions on how to add an option
29 */
30
31 // Visual does not know the round function
32 #include <cmath>
33
34 #include "Forwards.hpp"
35
36 #include "Debug/Tracer.hpp"
37 #include "Debug/Assertion.hpp"
38
39 #include "Lib/VString.hpp"
40 #include "Lib/Environment.hpp"
41 #include "Lib/Timer.hpp"
42 #include "Lib/Exception.hpp"
43 #include "Lib/Int.hpp"
44 #include "Lib/Random.hpp"
45 #include "Lib/Set.hpp"
46 #include "Lib/System.hpp"
47
48 #include "Shell/UIHelper.hpp"
49
50 #include "Kernel/Problem.hpp"
51 #include "Kernel/Signature.hpp"
52
53 #include "Options.hpp"
54 #include "Property.hpp"
55
56 using namespace Lib;
57 using namespace Shell;
58
59 /**
60 * Initialize options to the default values.
61 *
62 * Options are divided by the mode they are applicable to.
63 * We then divid by tags where appropriate.
64 * If an option is applicable to multiple modes but is not global it should be
65 * put in the most obvious mode - usually Vampire.
66 *
67 * IMPORTANT --> see .hpp file for instructions on how to add an option
68 *
69 * @since 10/07/2003 Manchester, _normalize added
70 */
Options()71 Options::Options ()
72
73 {
74 CALL("Options::Options");
75 init();
76 }
77
init()78 void Options::Options::init()
79 {
80 CALL("Options::init");
81
82 // some options that were not give names previously
83 _forceIncompleteness = BoolOptionValue("force_incompleteness","",false);
84 _equivalentVariableRemoval = BoolOptionValue("equivalentVariableRemoval","",true);
85 _bpCollapsingPropagation = BoolOptionValue("bp_collapsing_propagation","",false);
86 _backjumpTargetIsDecisionPoint = BoolOptionValue("backjump_target_is_decision_point","",true);
87 _selectUnusedVariablesFirst = BoolOptionValue("_selectUnusedVariablesFirst","",false);
88
89 //**********************************************************************
90 //*********************** GLOBAL, for all modes ***********************
91 //**********************************************************************
92
93 _memoryLimit = UnsignedOptionValue("memory_limit","m",
94 #if VDEBUG
95 1000
96 #else
97 3000
98 #endif
99 );
100 _memoryLimit.description="Memory limit in MB";
101 _lookup.insert(&_memoryLimit);
102 #if !__APPLE__ && !__CYGWIN__
103 _memoryLimit.addHardConstraint(lessThanEq((unsigned)Lib::System::getSystemMemory()));
104 #endif
105
106 _mode = ChoiceOptionValue<Mode>("mode","",Mode::VAMPIRE,
107 {"axiom_selection",
108 "casc",
109 "casc_sat",
110 "casc_ltb",
111 "clausify",
112 "consequence_elimination",
113 "grounding",
114 "model_check",
115 "output",
116 "portfolio",
117 "preprocess",
118 "preprocess2",
119 "profile",
120 "random_strategy",
121 "sat_solver",
122 "smtcomp",
123 "spider",
124 "tclausify",
125 "tpreprocess",
126 "vampire"});
127 _mode.description=
128 "Select the mode of operation. Choices are:\n"
129 " -vampire: the standard mode of operation for first-order theorem proving\n"
130 " -portfolio: a portfolio mode running a specified schedule (see schedule)\n"
131 " -casc, casc_sat, smtcomp - like portfolio mode, with competition specific\n presets for schedule, etc.\n"
132 " -preprocess,axiom_selection,clausify,grounding: modes for producing output\n for other solvers.\n"
133 " -tpreprocess,tclausify: output modes for theory input (clauses are quantified\n with sort information).\n"
134 " -output,profile: output information about the problem\n"
135 " -sat_solver: accepts problems in DIMACS and uses the internal sat solver\n directly\n"
136 "Some modes are not currently maintained (get in touch if interested):\n"
137 " -bpa: perform bound propagation\n"
138 " -consequence_elimination: perform consequence elimination\n"
139 " -random_strategy: attempts to randomize the option values\n";
140 _lookup.insert(&_mode);
141 _mode.addHardConstraint(If(equal(Mode::CONSEQUENCE_ELIMINATION)).then(_splitting.is(notEqual(true))));
142
143 _schedule = ChoiceOptionValue<Schedule>("schedule","sched",Schedule::CASC,
144 {"casc",
145 "casc_2014",
146 "casc_2014_epr",
147 "casc_2016",
148 "casc_2017",
149 "casc_2018",
150 "casc_2019",
151 "casc_sat",
152 "casc_sat_2014",
153 "casc_sat_2016",
154 "casc_sat_2017",
155 "casc_sat_2018",
156 "casc_sat_2019",
157 "ltb_2014",
158 "ltb_2014_mzr",
159 "ltb_default_2017",
160 "ltb_hh4_2015_fast",
161 "ltb_hh4_2015_midd",
162 "ltb_hh4_2015_slow",
163 "ltb_hh4_2017",
164 "ltb_hll_2015_fast",
165 "ltb_hll_2015_midd",
166 "ltb_hll_2015_slow",
167 "ltb_hll_2017",
168 "ltb_isa_2015_fast",
169 "ltb_isa_2015_midd",
170 "ltb_isa_2015_slow",
171 "ltb_isa_2017",
172 "ltb_mzr_2015_fast",
173 "ltb_mzr_2015_midd",
174 "ltb_mzr_2015_slow",
175 "ltb_mzr_2017",
176 "smtcomp",
177 "smtcomp_2016",
178 "smtcomp_2017",
179 "smtcomp_2018"});
180 _schedule.description = "Schedule to be run by the portfolio mode. casc and smtcomp usually point to the most recent schedule in that category. Note that some old schedules may contain option values that are no longer supported - see ignore_missing.";
181 _lookup.insert(&_schedule);
182 _schedule.reliesOnHard(Or(_mode.is(equal(Mode::CASC)),_mode.is(equal(Mode::CASC_SAT)),_mode.is(equal(Mode::SMTCOMP)),_mode.is(equal(Mode::PORTFOLIO))));
183
184 _multicore = UnsignedOptionValue("cores","",1);
185 _multicore.description = "When running in portfolio modes (including casc or smtcomp modes) specify the number of cores, set to 0 to use maximum";
186 _lookup.insert(&_multicore);
187 _multicore.reliesOnHard(Or(_mode.is(equal(Mode::CASC)),_mode.is(equal(Mode::CASC_SAT)),_mode.is(equal(Mode::SMTCOMP)),_mode.is(equal(Mode::PORTFOLIO))));
188
189 _ltbLearning = ChoiceOptionValue<LTBLearning>("ltb_learning","ltbl",LTBLearning::OFF,{"on","off","biased"});
190 _ltbLearning.description = "Perform learning in LTB mode";
191 _lookup.insert(&_ltbLearning);
192 _ltbLearning.setExperimental();
193
194 _ltbDirectory = StringOptionValue("ltb_directory","","");
195 _ltbDirectory.description = "Directory for output from LTB mode. Default is to put output next to problem.";
196 _lookup.insert(&_ltbDirectory);
197 _ltbDirectory.setExperimental();
198
199 _decode = DecodeOptionValue("decode","",this);
200 _decode.description="Decodes an encoded strategy. Can be used to replay a strategy. To make Vampire output an encoded version of the strategy use the encode option.";
201 _lookup.insert(&_decode);
202 _decode.tag(OptionTag::DEVELOPMENT);
203
204 _encode = BoolOptionValue("encode","",false);
205 _encode.description="Output an encoding of the strategy to be used with the decode option";
206 _lookup.insert(&_encode);
207 _encode.tag(OptionTag::DEVELOPMENT);
208
209 _randomStrategy = ChoiceOptionValue<RandomStrategy>("random_strategy","",RandomStrategy::OFF,{"on","off","sat","nocheck"});
210 _randomStrategy.description =
211 "Create a random strategy. Randomisation will occur after all other options have been "
212 "set, whatever order they have been given in. A random number of options will be selected "
213 " and set with a safe (possibly default) value.";
214 _lookup.insert(&_randomStrategy);
215 _randomStrategy.reliesOnHard(Or(_mode.is(equal(Mode::VAMPIRE)),_mode.is(equal(Mode::RANDOM_STRATEGY))));
216 _randomStrategy.tag(OptionTag::DEVELOPMENT);
217
218 _forbiddenOptions = StringOptionValue("forbidden_options","","");
219 _forbiddenOptions.description=
220 "If some of the specified options are set to a forbidden state, vampire will fail to start, or in portfolio modes it will skip such strategies. The expected syntax is <opt1>=<val1>:<opt2>:<val2>:...:<optn>=<valN>";
221 _lookup.insert(&_forbiddenOptions);
222 _forbiddenOptions.tag(OptionTag::INPUT);
223
224 _forcedOptions = StringOptionValue("forced_options","","");
225 _forcedOptions.description=
226 "Options in the format <opt1>=<val1>:<opt2>=<val2>:...:<optn>=<valN> that override the option values set by other means (also inside portfolio mode strategies)";
227 _lookup.insert(&_forcedOptions);
228 _forcedOptions.tag(OptionTag::INPUT);
229
230 _printAllTheoryAxioms = BoolOptionValue("print_theory_axioms","",false);
231 _printAllTheoryAxioms.description = "Just print all theory axioms and terminate";
232 _printAllTheoryAxioms.tag(OptionTag::DEVELOPMENT);
233 _lookup.insert(&_printAllTheoryAxioms);
234 _printAllTheoryAxioms.setExperimental();
235
236 _showHelp = BoolOptionValue("help","h",false);
237 _showHelp.description="Display the help message";
238 _lookup.insert(&_showHelp);
239 _showHelp.tag(OptionTag::HELP);
240
241 _showOptions = BoolOptionValue("show_options","",false);
242 _showOptions.description="List all available options";
243 _lookup.insert(&_showOptions);
244 _showOptions.tag(OptionTag::HELP);
245
246 _showOptionsLineWrap = BoolOptionValue("show_options_line_wrap","",true);
247 _showOptionsLineWrap.description="Line wrap in show options. Mainly used when options are read by another tool that applies its own line wrap.";
248 _lookup.insert(&_showOptionsLineWrap);
249 _showOptionsLineWrap.tag(OptionTag::HELP);
250 _showOptionsLineWrap.setExperimental();
251
252 _showExperimentalOptions = BoolOptionValue("show_experimental_options","",false);
253 _showExperimentalOptions.description="Include experimental options in showOption";
254 _lookup.insert(&_showExperimentalOptions);
255 _showExperimentalOptions.setExperimental(); // only we know about it!
256 _showExperimentalOptions.tag(OptionTag::HELP);
257
258 _explainOption = StringOptionValue("explain_option","explain","");
259 _explainOption.description = "Use to explain a single option i.e. -explain explain";
260 _lookup.insert(&_explainOption);
261 _explainOption.tag(OptionTag::HELP);
262
263 _ignoreMissing = ChoiceOptionValue<IgnoreMissing>("ignore_missing","",IgnoreMissing::OFF,{"on","off","warn"});
264 _ignoreMissing.description=
265 "Ignore any options that have been removed (useful in portfolio modes where this can cause strategies to be skipped). If set to warn "
266 "this will print a warning when ignoring. This is set to warn in CASC mode.";
267 _lookup.insert(&_ignoreMissing);
268 _ignoreMissing.tag(OptionTag::DEVELOPMENT);
269
270 _badOption = ChoiceOptionValue<BadOption>("bad_option","",BadOption::SOFT,{"hard","forced","off","soft"});
271 _badOption.description = "What should be done if a bad option value (wrt hard and soft constraints) is encountered:\n"
272 " - hard: will cause a user error\n"
273 " - soft: will only report the error (unless it is unsafe)\n"
274 " - forced: <under development> \n"
275 " - off: will ignore safe errors\n"
276 "Note that unsafe errors will aways lead to a user error";
277 _lookup.insert(&_badOption);
278 _badOption.tag(OptionTag::HELP);
279
280
281 /*
282 * TODO: Not currently used, bring back?
283 _namePrefix = StringOptionValue("name_prefix","","");
284 _namePrefix.description=
285 "Prefix for symbols introduced by Vampire (naming predicates, Skolem functions)";
286 _lookup.insert(&_namePrefix);
287 _namePrefix.tag(OptionTag::OUTPUT);
288 */
289
290 // Do we really need to be able to set this externally?
291 _problemName = StringOptionValue("problem_name","","");
292 _problemName.description="";
293 //_lookup.insert(&_problemName);
294
295 _proof = ChoiceOptionValue<Proof>("proof","p",Proof::ON,{"off","on","proofcheck","tptp","property"});
296 _proof.description=
297 "Specifies whether proof (or similar e.g. model/saturation) will be output and in which format:\n"
298 "- off gives no proof output\n"
299 "- on gives native Vampire proof output\n"
300 "- proofcheck will output proof as a sequence of TPTP problems to allow for proof-checking by external solvers\n"
301 "- tptp gives TPTP output\n"
302 "- property is a developmental option. It allows developers to output statistics about the proof using a ProofPrinter "
303 "object (see Kernel/InferenceStore::ProofPropertyPrinter\n";
304 _lookup.insert(&_proof);
305 _proof.tag(OptionTag::OUTPUT);
306
307 _minimizeSatProofs = BoolOptionValue("minimize_sat_proofs","",true);
308 _minimizeSatProofs.description="Perform unsat core minimization when a sat solver finds a clause set UNSAT\n"
309 "(such as with AVATAR proofs or with global subsumption).";
310 _lookup.insert(&_minimizeSatProofs);
311 _minimizeSatProofs.tag(OptionTag::OUTPUT);
312
313 _proofExtra = ChoiceOptionValue<ProofExtra>("proof_extra","",ProofExtra::OFF,{"off","free","full"});
314 _proofExtra.description="Add extra detail to proofs:\n "
315 "- free uses known information only\n"
316 "- full may perform expensive operations to acheive this so may"
317 " significantly impact on performance.\n"
318 " The option is still under development and the format of extra information (mainly from full) may change between minor releases";
319 _lookup.insert(&_proofExtra);
320 _proofExtra.tag(OptionTag::OUTPUT);
321
322 _proofChecking = BoolOptionValue("proof_checking","",false);
323 _proofChecking.description="";
324 _lookup.insert(&_proofChecking);
325 _proofChecking.setExperimental(); // don't think it works!
326
327 _protectedPrefix = StringOptionValue("protected_prefix","","");
328 _protectedPrefix.description="Symbols with this prefix are immune against elimination during preprocessing";
329 _lookup.insert(&_protectedPrefix);
330 _protectedPrefix.tag(OptionTag::PREPROCESSING);
331 _protectedPrefix.setExperimental(); // Does not work for all (any?) preprocessing steps currently
332
333 _statistics = ChoiceOptionValue<Statistics>("statistics","stat",Statistics::BRIEF,{"brief","full","none"});
334 _statistics.description="The level of statistics to report at the end of the run.";
335 _lookup.insert(&_statistics);
336 _statistics.tag(OptionTag::OUTPUT);
337
338 _testId = StringOptionValue("test_id","","unspecified_test");
339 _testId.description="";
340 _lookup.insert(&_testId);
341 _testId.setExperimental();
342
343 _outputMode = ChoiceOptionValue<Output>("output_mode","om",Output::SZS,{"smtcomp","spider","szs","vampire"});
344 _outputMode.description="Change how Vampire prints the final result. SZS uses TPTP's SZS ontology. smtcomp mode"
345 " supresses all output and just prints sat/unsat. vampire is the same as SZS just without the SZS."
346 " Spider prints out some profile information and extra error reports.";
347 _lookup.insert(&_outputMode);
348 _outputMode.tag(OptionTag::OUTPUT);
349
350 _thanks = StringOptionValue("thanks","","Tanya");
351 _thanks.description="";
352 _lookup.insert(&_thanks);
353 _thanks.setExperimental();
354
355 _timeLimitInDeciseconds = TimeLimitOptionValue("time_limit","t",600); // stores deciseconds, but reads seconds from the user by default
356 _timeLimitInDeciseconds.description="Time limit in wall clock seconds, you can use d,s,m,h,D suffixes also i.e. 60s, 5m. Setting it to 0 effectively gives no time limit.";
357 _lookup.insert(&_timeLimitInDeciseconds);
358
359 _timeStatistics = BoolOptionValue("time_statistics","tstat",false);
360 _timeStatistics.description="Show how much running time was spent in each part of Vampire";
361 _lookup.insert(&_timeStatistics);
362 _timeStatistics.tag(OptionTag::OUTPUT);
363
364 //*********************** Input ***********************
365
366 _include = StringOptionValue("include","","");
367 _include.description="Path prefix for the 'include' TPTP directive";
368 _lookup.insert(&_include);
369 _include.tag(OptionTag::INPUT);
370
371 _inputFile= InputFileOptionValue("input_file","","",this);
372 _inputFile.description="Problem file to be solved (if not specified, standard input is used)";
373 _lookup.insert(&_inputFile);
374 _inputFile.tag(OptionTag::INPUT);
375 _inputFile.setExperimental();
376
377 _inputSyntax= ChoiceOptionValue<InputSyntax>("input_syntax","",
378 //in case we compile vampire with bpa, then the default input syntax is smtlib
379 InputSyntax::TPTP,
380 //{"simplify","smtlib","smtlib2","tptp"});//,"xhuman","xmps","xnetlib"});
381 {"smtlib2","tptp"});//,"xhuman","xmps","xnetlib"});
382 _inputSyntax.description=
383 "Input syntax. Historic input syntaxes have been removed as they are not actively maintained. Contact developers for help with these.";
384 _lookup.insert(&_inputSyntax);
385 _inputSyntax.tag(OptionTag::INPUT);
386
387 _smtlibConsiderIntsReal = BoolOptionValue("smtlib_consider_ints_real","",false);
388 _smtlibConsiderIntsReal.description="All integers will be considered to be reals by the SMTLIB parser";
389 _lookup.insert(&_smtlibConsiderIntsReal);
390 _smtlibConsiderIntsReal.tag(OptionTag::INPUT);
391
392 _smtlibFletAsDefinition = BoolOptionValue("smtlib_flet_as_definition","",false);
393 _smtlibFletAsDefinition.description="";
394 _lookup.insert(&_smtlibFletAsDefinition);
395 _smtlibFletAsDefinition.setExperimental();
396 _smtlibFletAsDefinition.tag(OptionTag::INPUT);
397
398 _guessTheGoal = ChoiceOptionValue<GoalGuess>("guess_the_goal","gtg",GoalGuess::OFF,{"off","all","exists_top","exists_all","exists_sym","position"});
399 _guessTheGoal.description = "Use heuristics to guess formulas that correspond to the goal. Doesn't "
400 "really make sense if there is already a goal but it will still do something. "
401 "This is really designed for use with SMTLIB problems that don't have goals";
402 _lookup.insert(&_guessTheGoal);
403 _guessTheGoal.tag(OptionTag::INPUT);
404
405 _guessTheGoalLimit = UnsignedOptionValue("guess_the_goal_limit","gtgl",1);
406 _guessTheGoalLimit.description = "The maximum number of input units a symbol appears for it to be considered in a goal";
407 _guessTheGoalLimit.tag(OptionTag::INPUT);
408 _guessTheGoalLimit.reliesOn(_guessTheGoal.is(notEqual(GoalGuess::OFF)));
409 _lookup.insert(&_guessTheGoalLimit);
410
411
412 //*********************** Preprocessing ***********************
413
414 _ignoreConjectureInPreprocessing = BoolOptionValue("ignore_conjecture_in_preprocessing","icip",false);
415 _ignoreConjectureInPreprocessing.description="Make sure we do not delete the conjecture in preprocessing even if it can be deleted.";
416 _lookup.insert(&_ignoreConjectureInPreprocessing);
417 _ignoreConjectureInPreprocessing.tag(OptionTag::PREPROCESSING);
418
419 _inequalitySplitting = IntOptionValue("inequality_splitting","ins",0);
420 _inequalitySplitting.description=
421 "Defines a weight threshold w such that any clause C \\/ s!=t where s (or conversely t) is ground "
422 "and has weight less than w is replaced by C \\/ p(s) with the additional unit clause ~p(t) being added "
423 "for fresh predicate p.";
424 _lookup.insert(&_inequalitySplitting);
425 _inequalitySplitting.tag(OptionTag::PREPROCESSING);
426
427 _sos = ChoiceOptionValue<Sos>("sos","sos",Sos::OFF,{"all","off","on","theory"});
428 _sos.description=
429 "Set of support strategy. All formulas annotated as axioms are put directly among active clauses, without performing any inferences between them."
430 " If all, select all literals of set-of-support clauses, otherwise use the default literal selector. If theory then only apply to theory"
431 " axioms introduced by vampire (all literals are selected).";
432 _lookup.insert(&_sos);
433 _sos.tag(OptionTag::PREPROCESSING);
434 _sos.setRandomChoices(And(isRandSat(),saNotInstGen()),{"on","off","off","off","off"});
435 _sos.setRandomChoices(And(isRandOn(),hasNonUnits()),{"on","off","off","off","off"});
436 _sos.setRandomChoices(isRandOn(),{"all","off","on"});
437
438 _sosTheoryLimit = UnsignedOptionValue("sos_theory_limit","sstl",0);
439 _sosTheoryLimit.description="When sos=theory, limit the depth of descendants a theory axiom can have.";
440 _lookup.insert(&_sosTheoryLimit);
441 _sosTheoryLimit.tag(OptionTag::PREPROCESSING);
442 _sosTheoryLimit.reliesOn(_sos.is(equal(Sos::THEORY)));
443
444
445
446 _equalityProxy = ChoiceOptionValue<EqualityProxy>( "equality_proxy","ep",EqualityProxy::OFF,{"R","RS","RST","RSTC","off"});
447 _equalityProxy.description="Applies the equality proxy transformation to the problem. It works as follows:\n"
448 " - All literals s=t are replaced by E(s,t)\n"
449 " - All literals s!=t are replaced by ~E(s,t)\n"
450 " - If S the symmetry clause ~E(x,y) \\/ E(y,x) is added\n"
451 " - If T the transitivity clause ~E(x,y) \\/ ~E(y,z) \\/ E(x,z) is added\n"
452 " - If C the congruence clauses are added as follows:\n"
453 " for predicates p that are not E or equality add\n"
454 " ~E(x1,y1) \\/ ... \\/ ~E(xN,yN) \\/ ~p(x1,...,xN) \\/ p(y1,...,yN)\n"
455 " for non-constant functions f add\n"
456 " ~E(x1,y1) \\/ ... \\/ ~E(xN,yN) \\/ E(f(x1,...,xN),f(y1,...,yN))\n"
457 " R stands for reflexivity";
458 _lookup.insert(&_equalityProxy);
459 _equalityProxy.tag(OptionTag::PREPROCESSING);
460 _equalityProxy.addProblemConstraint(hasEquality());
461 _equalityProxy.setRandomChoices(isRandOn(),{"R","RS","RST","RSTC","off","off","off","off","off"}); // wasn't tested, make off more likely
462
463
464 _equalityResolutionWithDeletion = ChoiceOptionValue<RuleActivity>( "equality_resolution_with_deletion","erd",
465 RuleActivity::INPUT_ONLY,{"input_only","off","on"});
466 _equalityResolutionWithDeletion.description="Perform equality resolution with deletion. Only input_only and off are valid options.";
467 _lookup.insert(&_equalityResolutionWithDeletion);
468 _equalityResolutionWithDeletion.tag(OptionTag::PREPROCESSING);
469 _equalityResolutionWithDeletion.addConstraint(notEqual(RuleActivity::ON));
470 //TODO does this depend on anything?
471 //TODO is there a problemConstraint?
472 _equalityResolutionWithDeletion.setRandomChoices({"input_only","off"});
473
474
475 _arityCheck = BoolOptionValue("arity_check","",false);
476 _arityCheck.description="Enforce the condition that the same symbol name cannot be used with multiple arities."
477 "This also ensures a symbol is not used as a function and predicate.";
478 _lookup.insert(&_arityCheck);
479 _arityCheck.tag(OptionTag::DEVELOPMENT);
480
481 _functionDefinitionElimination = ChoiceOptionValue<FunctionDefinitionElimination>("function_definition_elimination","fde",
482 FunctionDefinitionElimination::ALL,{"all","none","unused"});
483 _functionDefinitionElimination.description=
484 "Attempts to eliminate function definitions. A function definition is a unit clause of the form f(x1,..,xn) = t where x1,..,xn are the pairwise distinct free variables of t and f does not appear in t. If 'all', definitions are eliminated by replacing every occurence of f(s1,..,sn) by t{x1 -> s1, .., xn -> sn}. If 'unused' only unused definitions are removed.";
485 _lookup.insert(&_functionDefinitionElimination);
486 _functionDefinitionElimination.tag(OptionTag::PREPROCESSING);
487 _functionDefinitionElimination.addProblemConstraint(hasEquality());
488 _functionDefinitionElimination.setRandomChoices({"all","none"});
489
490 _generalSplitting = ChoiceOptionValue<RuleActivity>("general_splitting","gsp",RuleActivity::OFF,{"input_only","off","on"});
491 _generalSplitting.description=
492 "Splits clauses in order to reduce number of different variables in each clause. "
493 "A clause C[X] \\/ D[Y] with subclauses C and D over non-equal sets of variables X and Y can be split into S(Z) \\/ C[X] and ~S(Z) \\/ D[Y] where Z is the intersection of X and Y. "
494 " Only input_only and off are valid values.";
495 _lookup.insert(&_generalSplitting);
496 _generalSplitting.tag(OptionTag::PREPROCESSING);
497 _generalSplitting.addConstraint(notEqual(RuleActivity::ON));
498 _generalSplitting.addProblemConstraint(hasNonUnits());
499 _generalSplitting.setRandomChoices({"off","input_only"});
500
501 _unusedPredicateDefinitionRemoval = BoolOptionValue("unused_predicate_definition_removal","updr",true);
502 _unusedPredicateDefinitionRemoval.description="Attempt to remove predicate definitions. A predicate definition is a formula of the form ![X1,..,Xn] : (p(X1,..,XN) <=> F) where p is not equality and does not occur in F and X1,..,XN are the free variables of F. If p has only positive (negative) occurences then <=> in the definition can be replaced by => (<=). If p does not occur in the rest of the problem the definition can be removed.";
503 _lookup.insert(&_unusedPredicateDefinitionRemoval);
504 _unusedPredicateDefinitionRemoval.tag(OptionTag::PREPROCESSING);
505 _unusedPredicateDefinitionRemoval.addProblemConstraint(notWithCat(Property::UEQ));
506 _unusedPredicateDefinitionRemoval.setRandomChoices({"on","off"});
507
508 _blockedClauseElimination = BoolOptionValue("blocked_clause_elimination","bce",false);
509 _blockedClauseElimination.description="Eliminate blocked clauses after clausification.";
510 _lookup.insert(&_blockedClauseElimination);
511 _blockedClauseElimination.tag(OptionTag::PREPROCESSING);
512 _blockedClauseElimination.addProblemConstraint(notWithCat(Property::UEQ));
513 _blockedClauseElimination.setRandomChoices({"on","off"});
514
515 _theoryAxioms = ChoiceOptionValue<TheoryAxiomLevel>("theory_axioms","tha",TheoryAxiomLevel::ON,{"on","off","some"});
516 _theoryAxioms.description="Include theory axioms for detected interpreted symbols";
517 _lookup.insert(&_theoryAxioms);
518 _theoryAxioms.tag(OptionTag::PREPROCESSING);
519
520 _theoryFlattening = BoolOptionValue("theory_flattening","thf",false);
521 _theoryFlattening.description = "Flatten clauses to separate theory and non-theory parts in the input. This is often quickly undone in proof search.";
522 _lookup.insert(&_theoryFlattening);
523 _theoryFlattening.tag(OptionTag::PREPROCESSING);
524
525 _sineDepth = UnsignedOptionValue("sine_depth","sd",0);
526 _sineDepth.description=
527 "Limit number of iterations of the transitive closure algorithm that selects formulas based on SInE's D-relation (see SInE description). 0 means no limit, 1 is a maximal limit (least selected axioms), 2 allows two iterations, etc...";
528 _lookup.insert(&_sineDepth);
529 _sineDepth.tag(OptionTag::PREPROCESSING);
530 // Captures that if the value is not default then sineSelection must be on
531 _sineDepth.reliesOn(_sineSelection.is(notEqual(SineSelection::OFF)));
532 _sineDepth.setRandomChoices({"0","1","2","3","4","5","7","10"});
533
534 _sineGeneralityThreshold = UnsignedOptionValue("sine_generality_threshold","sgt",0);
535 _sineGeneralityThreshold.description=
536 "Generality of a symbol is the number of input formulas in which a symbol appears. If the generality of a symbol is smaller than the threshold, it is always added into the D-relation with formulas in which it appears.";
537 _lookup.insert(&_sineGeneralityThreshold);
538 _sineGeneralityThreshold.tag(OptionTag::PREPROCESSING);
539 // Captures that if the value is not default then sineSelection must be on
540 _sineGeneralityThreshold.reliesOn(_sineSelection.is(notEqual(SineSelection::OFF)));
541
542 _sineSelection = ChoiceOptionValue<SineSelection>("sine_selection","ss",SineSelection::OFF,{"axioms","included","off"});
543 _sineSelection.description=
544 "If 'axioms', all formulas that are not annotated as 'axiom' (i.e. conjectures and hypotheses) are initially selected, and the SInE selection is performed on those annotated as 'axiom'. If 'included', all formulas that are directly in the problem file are initially selected, and the SInE selection is performed on formulas from included files. The 'included' value corresponds to the behaviour of the original SInE implementation.";
545 _lookup.insert(&_sineSelection);
546 _sineSelection.tag(OptionTag::PREPROCESSING);
547 _sineSelection.setRandomChoices(atomsMoreThan(100000),{"axioms","axioms","off"});
548 _sineSelection.setRandomChoices(atomsMoreThan(30000),{"axioms","off"});
549 _sineSelection.setRandomChoices(atomsMoreThan(10000),{"axioms","off","off","off"});
550 _sineSelection.setRandomChoices(atomsMoreThan(3000),{"axioms","off","off","off","off","off"});
551 _sineSelection.setRandomChoices(atomsMoreThan(1000),{"axioms","off","off","off","off","off","off","off"});
552
553 _sineTolerance = FloatOptionValue("sine_tolerance","st",1.0);
554 _sineTolerance.description="SInE tolerance parameter (sometimes referred to as 'benevolence')";
555 _lookup.insert(&_sineTolerance);
556 _sineTolerance.tag(OptionTag::PREPROCESSING);
557 _sineTolerance.addConstraint(Or(equal(0.0f),greaterThanEq(1.0f) ));
558 // Captures that if the value is not 1.0 then sineSelection must be on
559 _sineTolerance.reliesOn(_sineSelection.is(notEqual(SineSelection::OFF)));
560 _sineTolerance.setRandomChoices({"1.0","1.2","1.5","2.0","3.0","5.0"});
561
562 _naming = IntOptionValue("naming","nm",8);
563 _naming.description="Introduce names for subformulas. Given a subformula F(x1,..,xk) of formula G a new predicate symbol is introduced as a name for F(x1,..,xk) by adding the axiom n(x1,..,xk) <=> F(x1,..,xk) and replacing F(x1,..,xk) with n(x1,..,xk) in G. The value indicates how many times a subformula must be used before it is named.";
564 _lookup.insert(&_naming);
565 _naming.tag(OptionTag::PREPROCESSING);
566 _naming.addHardConstraint(lessThan(32768));
567 _naming.addHardConstraint(greaterThan(-1));
568 _naming.addHardConstraint(notEqual(1));
569
570 _newCNF = BoolOptionValue("newcnf","newcnf",false);
571 _newCNF.description="Use NewCNF algorithm to do naming, preprecess3 and clausificiation.";
572 _lookup.insert(&_newCNF);
573 _newCNF.tag(OptionTag::PREPROCESSING);
574
575 _iteInliningThreshold = IntOptionValue("ite_inlining_threshold","", 0);
576 _iteInliningThreshold.description="Threashold of inlining of if-then-else expressions. "
577 "0 means that all expressions are named. "
578 "<0 means that all expressions are inlined.";
579 _lookup.insert(&_iteInliningThreshold);
580 _iteInliningThreshold.tag(OptionTag::PREPROCESSING);
581
582 _inlineLet = BoolOptionValue("inline_let","ile",false);
583 _inlineLet.description="Always inline let-expressions.";
584 _lookup.insert(&_inlineLet);
585 _inlineLet.tag(OptionTag::PREPROCESSING);
586
587
588 //*********************** Output ***********************
589
590 // how is this used?
591 _logFile = StringOptionValue("log_file","","off");
592 _logFile.description="";
593 //_lookup.insert(&_logFile);
594 _logFile.tag(OptionTag::OUTPUT);
595
596 //used?
597 _xmlOutput = StringOptionValue("xml_output","","off");
598 _xmlOutput.description="File to put XML output in.";
599 //_lookup.insert(&_xmlOutput);
600 _xmlOutput.tag(OptionTag::OUTPUT);
601
602 _latexOutput = StringOptionValue("latex_output","","off");
603 _latexOutput.description="File that will contain proof in the LaTeX format.";
604 _lookup.insert(&_latexOutput);
605 _latexOutput.tag(OptionTag::OUTPUT);
606
607 _latexUseDefaultSymbols = BoolOptionValue("latex_use_default_symbols","",true);
608 _latexUseDefaultSymbols.description="Interpretted symbols such as product have default LaTeX symbols"
609 " that can be used. They can be overriden in the normal way. This option can turn them off";
610 _latexUseDefaultSymbols.tag(OptionTag::OUTPUT);
611 _lookup.insert(&_latexUseDefaultSymbols);
612
613 _outputAxiomNames = BoolOptionValue("output_axiom_names","",false);
614 _outputAxiomNames.description="Preserve names of axioms from the problem file in the proof output";
615 _lookup.insert(&_outputAxiomNames);
616 _outputAxiomNames.tag(OptionTag::OUTPUT);
617
618
619 _printClausifierPremises = BoolOptionValue("print_clausifier_premises","",false);
620 _printClausifierPremises.description="Output how the clausified problem was derived.";
621 _lookup.insert(&_printClausifierPremises);
622 _printClausifierPremises.tag(OptionTag::OUTPUT);
623
624 _showAll = BoolOptionValue("show_everything","",false);
625 _showAll.description="Turn (almost) all of the showX commands on";
626 _lookup.insert(&_showAll);
627 _showAll.tag(OptionTag::DEVELOPMENT);
628
629 _showActive = BoolOptionValue("show_active","",false);
630 _showActive.description="Print activated clauses.";
631 _lookup.insert(&_showActive);
632 _showActive.tag(OptionTag::DEVELOPMENT);
633
634 _showBlocked = BoolOptionValue("show_blocked","",false);
635 _showBlocked.description="Show generating inferences blocked due to coloring of symbols";
636 _lookup.insert(&_showBlocked);
637 _showBlocked.tag(OptionTag::DEVELOPMENT);
638
639 _showDefinitions = BoolOptionValue("show_definitions","",false);
640 _showDefinitions.description="Show definition introductions.";
641 _lookup.insert(&_showDefinitions);
642 _showDefinitions.tag(OptionTag::DEVELOPMENT);
643
644 _showNew = BoolOptionValue("show_new","",false);
645 _showNew.description="Show new (generated) clauses";
646 _lookup.insert(&_showNew);
647 _showNew.tag(OptionTag::DEVELOPMENT);
648
649 _sineToAge = BoolOptionValue("sine_to_age","s2a",false);
650 _lookup.insert(&_sineToAge);
651 _sineToAge.tag(OptionTag::DEVELOPMENT);
652
653 _sineToPredLevels = ChoiceOptionValue<PredicateSineLevels>("sine_to_pred_levels","s2pl",PredicateSineLevels::OFF,{"no","off","on"});
654 _sineToPredLevels.description = "Assign levels to predicate symbols as they are used to trigger axioms during SInE computation. "
655 "Then used then as predicateLevels determining the ordering. on means conjecture symbols are larger, no means the opposite. (equality keeps its standard lowest level).";
656 _lookup.insert(&_sineToPredLevels);
657 _sineToPredLevels.tag(OptionTag::DEVELOPMENT);
658 _sineToPredLevels.addHardConstraint(If(notEqual(PredicateSineLevels::OFF)).then(_literalComparisonMode.is(notEqual(LiteralComparisonMode::PREDICATE))));
659 _sineToPredLevels.addHardConstraint(If(notEqual(PredicateSineLevels::OFF)).then(_literalComparisonMode.is(notEqual(LiteralComparisonMode::REVERSE))));
660
661 // Like generality threshold for SiNE, except used by the sine2age trick
662 _sineToAgeGeneralityThreshold = UnsignedOptionValue("sine_to_age_generality_threshold","s2agt",0);
663 _lookup.insert(&_sineToAgeGeneralityThreshold);
664 _sineToAgeGeneralityThreshold.tag(OptionTag::DEVELOPMENT);
665 _sineToAgeGeneralityThreshold.reliesOn(Or(_sineToAge.is(equal(true)),_sineToPredLevels.is(notEqual(PredicateSineLevels::OFF))));
666
667 // Like generality threshold for SiNE, except used by the sine2age trick
668 _sineToAgeTolerance = FloatOptionValue("sine_to_age_tolerance","s2at",1.0);
669 _lookup.insert(&_sineToAgeTolerance);
670 _sineToAgeTolerance.tag(OptionTag::DEVELOPMENT);
671 _sineToAgeTolerance.addConstraint(Or(equal(0.0f),greaterThanEq(1.0f)));
672 // Captures that if the value is not 1.0 then sineSelection must be on
673 _sineToAgeTolerance.reliesOn(Or(_sineToAge.is(equal(true)),_sineToPredLevels.is(notEqual(PredicateSineLevels::OFF))));
674 _sineToAgeTolerance.setRandomChoices({"1.0","1.2","1.5","2.0","3.0","5.0"});
675
676 _showSplitting = BoolOptionValue("show_splitting","",false);
677 _showSplitting.description="Show updates within AVATAR";
678 _lookup.insert(&_showSplitting);
679 _showSplitting.tag(OptionTag::DEVELOPMENT);
680
681 _showNewPropositional = BoolOptionValue("show_new_propositional","",false);
682 _showNewPropositional.description="";
683 //_lookup.insert(&_showNewPropositional);
684 _showNewPropositional.tag(OptionTag::DEVELOPMENT);
685
686 _showNonconstantSkolemFunctionTrace = BoolOptionValue("show_nonconstant_skolem_function_trace","",false);
687 _showNonconstantSkolemFunctionTrace.description="Show introduction of non-constant skolem functions.";
688 _lookup.insert(&_showNonconstantSkolemFunctionTrace);
689 _showNonconstantSkolemFunctionTrace.tag(OptionTag::DEVELOPMENT);
690
691
692 _showPassive = BoolOptionValue("show_passive","",false);
693 _showPassive.description="Show clauses added to the passive set.";
694 _lookup.insert(&_showPassive);
695 _showPassive.tag(OptionTag::DEVELOPMENT);
696
697 _showReductions = BoolOptionValue("show_reductions","",false);
698 _showReductions.description="Show reductions.";
699 _showReductions.tag(OptionTag::DEVELOPMENT);
700 _lookup.insert(&_showReductions);
701
702 _showPreprocessing = BoolOptionValue("show_preprocessing","",false);
703 _showPreprocessing.description="Show preprocessing.";
704 _lookup.insert(&_showPreprocessing);
705 _showPreprocessing.tag(OptionTag::DEVELOPMENT);
706
707 _showSkolemisations = BoolOptionValue("show_skolemisations","",false);
708 _showSkolemisations.description="Show Skolemisations.";
709 _lookup.insert(&_showSkolemisations);
710 _showSkolemisations.tag(OptionTag::DEVELOPMENT);
711
712 _showSymbolElimination = BoolOptionValue("show_symbol_elimination","",false);
713 _showSymbolElimination.description="Show symbol elimination.";
714 _lookup.insert(&_showSymbolElimination);
715 _showSymbolElimination.tag(OptionTag::DEVELOPMENT);
716
717 _showTheoryAxioms = BoolOptionValue("show_theory_axioms","",false);
718 _showTheoryAxioms.description="Show the added theory axioms.";
719 _lookup.insert(&_showTheoryAxioms);
720 _showTheoryAxioms.tag(OptionTag::DEVELOPMENT);
721
722 #if VZ3
723 _showZ3 = BoolOptionValue("show_z3","",false);
724 _showZ3.description="Print the clauses being added to Z3";
725 _lookup.insert(&_showZ3);
726 _showZ3.tag(OptionTag::DEVELOPMENT);
727 #endif
728
729 _showFOOL = BoolOptionValue("show_fool","",false);
730 _showFOOL.description="Reveal the internal representation of FOOL terms";
731 _lookup.insert(&_showFOOL);
732 _showFOOL.tag(OptionTag::OUTPUT);
733
734 _showFMBsortInfo = BoolOptionValue("show_fmb_sort_info","",false);
735 _showFMBsortInfo.description = "Print information about sorts in FMB";
736 _lookup.insert(&_showFMBsortInfo);
737 _showFMBsortInfo.tag(OptionTag::OUTPUT);
738
739 _showInduction = BoolOptionValue("show_induction","",false);
740 _showInduction.description = "Print information about induction";
741 _lookup.insert(&_showInduction);
742 _showInduction.tag(OptionTag::OUTPUT);
743
744 _manualClauseSelection = BoolOptionValue("manual_cs","",false);
745 _manualClauseSelection.description="Run Vampire interactively by manually picking the clauses to be selected";
746 _lookup.insert(&_manualClauseSelection);
747 _manualClauseSelection.tag(OptionTag::DEVELOPMENT);
748
749 //************************************************************************
750 //*********************** VAMPIRE (includes CASC) ***********************
751 //************************************************************************
752
753 //*********************** Saturation ***********************
754
755 _saturationAlgorithm = ChoiceOptionValue<SaturationAlgorithm>("saturation_algorithm","sa",SaturationAlgorithm::LRS,
756 {"discount","fmb","inst_gen","lrs","otter"
757 #if VZ3
758 ,"z3"
759 #endif
760 });
761 _saturationAlgorithm.description=
762 "Select the saturation algorithm:\n"
763 " - discount:\n"
764 " - otter:\n"
765 " - limited resource:\n"
766 " - instance generation: a simple implementation of instantiation calculus\n"
767 " (global_subsumption, unit_resulting_resolution and age_weight_ratio)\n"
768 " - fmb : finite model building for satisfiable problems.\n"
769 " -z3 : pass the preprocessed problem to z3, will terminate if the resulting problem is not ground.\n"
770 "inst_gen, z3 and fmb aren't influenced by options for the saturation algorithm, apart from those under the relevant heading";
771 _lookup.insert(&_saturationAlgorithm);
772 _saturationAlgorithm.tag(OptionTag::SATURATION);
773 // Captures that if the saturation algorithm is InstGen then splitting must be off
774 _saturationAlgorithm.addHardConstraint(If(equal(SaturationAlgorithm::INST_GEN)).then(_splitting.is(notEqual(true))));
775 // Note order of adding constraints matters (we assume previous gaurds are false)
776 _saturationAlgorithm.setRandomChoices(isRandSat(),{"discount","otter","inst_gen","fmb"});
777 _saturationAlgorithm.setRandomChoices(Or(hasCat(Property::UEQ),atomsLessThan(4000)),{"lrs","discount","otter","inst_gen"});
778 _saturationAlgorithm.setRandomChoices({"discount","inst_gen","lrs","otter"});
779
780 #if VZ3
781 _smtForGround = BoolOptionValue("smt_for_ground","smtfg",true);
782 _smtForGround.description = "When a (theory) problem is ground after preprocessing pass it to Z3. In this case we can return sat if Z3 does.";
783 _lookup.insert(&_smtForGround);
784 #endif
785
786
787 _fmbNonGroundDefs = BoolOptionValue("fmb_nonground_defs","fmbngd",false);
788 _fmbNonGroundDefs.description = "Introduce definitions for non ground terms in preprocessing for fmb";
789 //_lookup.insert(&_fmbNonGroundDefs);
790 _fmbNonGroundDefs.setExperimental();
791 _fmbNonGroundDefs.setRandomChoices({"on","off"});
792
793 _fmbStartSize = UnsignedOptionValue("fmb_start_size","fmbss",1);
794 _fmbStartSize.description = "Set the initial model size for finite model building";
795 _lookup.insert(&_fmbStartSize);
796 _fmbStartSize.tag(OptionTag::FMB);
797
798 _fmbSymmetryRatio = FloatOptionValue("fmb_symmetry_ratio","fmbsr",1.0);
799 _fmbSymmetryRatio.description = "Usually we use at most n principal terms for symmetry avoidance where n is the current model size. This option allows us to supply a multiplier for that n. See Symmetry Avoidance in MACE-Style Finite Model Finding.";
800 _lookup.insert(&_fmbSymmetryRatio);
801 _fmbSymmetryRatio.tag(OptionTag::FMB);
802
803 _fmbSymmetryOrderSymbols = ChoiceOptionValue<FMBSymbolOrders>("fmb_symmetry_symbol_order","fmbsso",
804 FMBSymbolOrders::OCCURENCE,
805 {"occurence","input_usage","preprocessed_usage"});
806 _fmbSymmetryOrderSymbols.description = "The order of symbols considered for symmetry avoidance. See Symmetry Avoidance in MACE-Style Finite Model Finding.";
807 _lookup.insert(&_fmbSymmetryOrderSymbols);
808 _fmbSymmetryOrderSymbols.tag(OptionTag::FMB);
809
810 _fmbSymmetryWidgetOrders = ChoiceOptionValue<FMBWidgetOrders>("fmb_symmetry_widget_order","fmbswo",
811 FMBWidgetOrders::FUNCTION_FIRST,
812 {"function_first","argument_first","diagonal"});
813 _fmbSymmetryWidgetOrders.description = "The order of constructed principal terms used in symmetry avoidance. See Symmetry Avoidance in MACE-Style Finite Model Finding.";
814 _lookup.insert(&_fmbSymmetryWidgetOrders);
815 _fmbSymmetryWidgetOrders.tag(OptionTag::FMB);
816
817 _fmbAdjustSorts = ChoiceOptionValue<FMBAdjustSorts>("fmb_adjust_sorts","fmbas",
818 FMBAdjustSorts::GROUP,
819 {"off","expand","group","predicate","function"});
820 _fmbAdjustSorts.description = "Detect monotonic sorts. If <expand> then expand monotonic subsorts into proper sorts. If <group> then collapse monotonic sorts into a single sort. If <predicate> then introduce sort predicates for non-monotonic sorts and collapse all sorts into one. If <function> then introduce sort functions for non-monotonic sorts and collapse all sorts into one";
821 _lookup.insert(&_fmbAdjustSorts);
822 _fmbAdjustSorts.addHardConstraint(
823 If(equal(FMBAdjustSorts::EXPAND)).then(_fmbEnumerationStrategy.is(notEqual(FMBEnumerationStrategy::CONTOUR))));
824 _fmbAdjustSorts.tag(OptionTag::FMB);
825
826 _fmbDetectSortBounds = BoolOptionValue("fmb_detect_sort_bounds","fmbdsb",false);
827 _fmbDetectSortBounds.description = "Use a saturation loop to detect sort bounds introduced by (for example) injective functions";
828 _lookup.insert(&_fmbDetectSortBounds);
829 _fmbDetectSortBounds.addHardConstraint(If(equal(true)).then(_fmbAdjustSorts.is(notEqual(FMBAdjustSorts::PREDICATE))));
830 _fmbDetectSortBounds.addHardConstraint(If(equal(true)).then(_fmbAdjustSorts.is(notEqual(FMBAdjustSorts::FUNCTION))));
831 _fmbDetectSortBounds.tag(OptionTag::FMB);
832
833 _fmbDetectSortBoundsTimeLimit = UnsignedOptionValue("fmb_detect_sort_bounds_time_limit","fmbdsbt",1);
834 _fmbDetectSortBoundsTimeLimit.description = "The time limit (in seconds) for performing sort bound detection";
835 _lookup.insert(&_fmbDetectSortBoundsTimeLimit);
836 _fmbDetectSortBoundsTimeLimit.tag(OptionTag::FMB);
837
838 _fmbSizeWeightRatio = UnsignedOptionValue("fmb_size_weight_ratio","fmbswr",1);
839 _fmbSizeWeightRatio.description = "Controls the priority the next sort size vector is given based on a ratio. 0 is size only, 1 means 1:1, 2 means 1:2, etc.";
840 _fmbSizeWeightRatio.reliesOn(_fmbEnumerationStrategy.is(equal(FMBEnumerationStrategy::CONTOUR)));
841 _lookup.insert(&_fmbSizeWeightRatio);
842 _fmbSizeWeightRatio.tag(OptionTag::FMB);
843
844 _fmbEnumerationStrategy = ChoiceOptionValue<FMBEnumerationStrategy>("fmb_enumeration_strategy","fmbes",FMBEnumerationStrategy::SBMEAM,{"sbeam",
845 #if VZ3
846 "smt",
847 #endif
848 "contour"});
849 _fmbEnumerationStrategy.description = "How model sizes assignments are enumerated in the multi-sorted setting. (Only smt and contour are known to be finite model complete and can therefore return UNSAT.)";
850 _lookup.insert(&_fmbEnumerationStrategy);
851 _fmbEnumerationStrategy.tag(OptionTag::FMB);
852
853 _selection = SelectionOptionValue("selection","s",10);
854 _selection.description=
855 "Selection methods 2,3,4,10,11 are complete by virtue of extending Maximal i.e. they select the best among maximal. Methods 1002,1003,1004,1010,1011 relax this restriction and are therefore not complete.\n"
856 " 0 - Total (select everything)\n"
857 " 1 - Maximal\n"
858 " 2 - ColoredFirst, MaximalSize then Lexigraphical\n"
859 " 3 - ColoredFirst, NoPositiveEquality, LeastTopLevelVariables,\n LeastDistinctVariables then Lexigraphical\n"
860 " 4 - ColoredFirst, NoPositiveEquality, LeastTopLevelVariables,\n LeastVariables, MaximalSize then Lexigraphical\n"
861 " 10 - ColoredFirst, NegativeEquality, MaximalSize, Negative then Lexigraphical\n"
862 " 11 - Lookahead\n"
863 " 1002 - Incomplete version of 2\n"
864 " 1003 - Incomplete version of 3\n"
865 " 1004 - Incomplete version of 4\n"
866 " 1010 - Incomplete version of 10\n"
867 " 1011 - Incomplete version of 11\n"
868 "Or negated, which means that reversePolarity is true i.e. for selection we treat all negative non-equalty literals as "
869 "positive and vice versa (can only apply to non-equality literals).\n";
870
871 _lookup.insert(&_selection);
872 _selection.tag(OptionTag::SATURATION);
873 _selection.reliesOn(Or(_saturationAlgorithm.is(notEqual(SaturationAlgorithm::INST_GEN)),_instGenWithResolution.is(equal(true))));
874 _selection.setRandomChoices(And(isRandSat(),saNotInstGen()),{"0","1","2","3","4","10","11","-1","-2","-3","-4","-10","-11"});
875 _selection.setRandomChoices({"0","1","2","3","4","10","11","1002","1003","1004","1010","1011","-1","-2","-3","-4","-10","-11","-1002","-1003","-1004","-1010"});
876
877 _lookaheadDelay = IntOptionValue("lookahaed_delay","lsd",0);
878 _lookaheadDelay.description = "Delay the use of lookahead selection by this many selections"
879 " the idea is that lookahead selection may behave erratically"
880 " at the start";
881 _lookaheadDelay.tag(OptionTag::SATURATION);
882 _lookup.insert(&_lookaheadDelay);
883 _lookaheadDelay.reliesOn(_selection.isLookAheadSelection());
884
885 _ageWeightRatio = RatioOptionValue("age_weight_ratio","awr",1,1,':');
886 _ageWeightRatio.description=
887 "Ratio in which clauses are being selected for activation i.e. a:w means that for every a clauses selected based on age "
888 "there will be w selected based on weight.";
889 _lookup.insert(&_ageWeightRatio);
890 _ageWeightRatio.tag(OptionTag::SATURATION);
891 _ageWeightRatio.reliesOn(Or(_saturationAlgorithm.is(notEqual(SaturationAlgorithm::INST_GEN)),_instGenWithResolution.is(equal(true))));
892 _ageWeightRatio.setRandomChoices({"8:1","5:1","4:1","3:1","2:1","3:2","5:4","1","2:3","2","3","4","5","6","7","8","10","12","14","16","20","24","28","32","40","50","64","128","1024"});
893
894
895 _ageWeightRatioShape = ChoiceOptionValue<AgeWeightRatioShape>("age_weight_ratio_shape","awrs",AgeWeightRatioShape::CONSTANT,{"constant","decay", "converge"});
896 _ageWeightRatioShape.description = "How to change the age/weight ratio during proof search.";
897 _lookup.insert(&_ageWeightRatioShape);
898 _ageWeightRatioShape.tag(OptionTag::SATURATION);
899
900 _ageWeightRatioShapeFrequency = UnsignedOptionValue("age_weight_ratio_shape_frequency","awrsf",100);
901 _ageWeightRatioShapeFrequency.description = "How frequently the age/weight ratio shape is to change: i.e. if set to 'decay' at a frequency of 100, the age/weight ratio will change every 100 age/weight choices.";
902 _lookup.insert(&_ageWeightRatioShapeFrequency);
903 _ageWeightRatioShapeFrequency.tag(OptionTag::SATURATION);
904
905 _useTheorySplitQueues = BoolOptionValue("theory_split_queue","thsq",false);
906 _useTheorySplitQueues.description = "Turn on clause selection using multiple queues containing different clauses (split by amount of theory reasoning)";
907 _lookup.insert(&_useTheorySplitQueues);
908 _useTheorySplitQueues.tag(OptionTag::SATURATION);
909
910 _theorySplitQueueExpectedRatioDenom = IntOptionValue("theory_split_queue_expected_ratio_denom","thsqd", 8);
911 _theorySplitQueueExpectedRatioDenom.description = "The denominator n such that we expect the final proof to have a ratio of theory-axioms to all-axioms of 1/n.";
912 _lookup.insert(&_theorySplitQueueExpectedRatioDenom);
913 _theorySplitQueueExpectedRatioDenom.reliesOn(_useTheorySplitQueues.is(equal(true)));
914 _theorySplitQueueExpectedRatioDenom.tag(OptionTag::SATURATION);
915
916 _theorySplitQueueCutoffs = StringOptionValue("theory_split_queue_cutoffs", "thsqc", "0,32,80");
917 _theorySplitQueueCutoffs.description = "The cutoff-values for the split-queues (the cutoff value for the last queue has to be omitted, as it is always infinity). Any split-queue contains all clauses which are assigned a feature-value less or equal to the cutoff-value of the queue. If no custom value for this option is set, the implementation will use cutoffs 0,4*d,10*d,infinity (where d denotes the theory split queue expected ratio denominator).";
918 _lookup.insert(&_theorySplitQueueCutoffs);
919 _theorySplitQueueCutoffs.reliesOn(_useTheorySplitQueues.is(equal(true)));
920 _theorySplitQueueCutoffs.tag(OptionTag::SATURATION);
921
922 _theorySplitQueueRatios = StringOptionValue("theory_split_queue_ratios", "thsqr", "20,10,10,1");
923 _theorySplitQueueRatios.description = "The ratios for picking clauses from the split-queues using weighted round robin. If a queue is empty, the clause will be picked from the next non-empty queue to the right. Note that this option implicitly also sets the number of queues.";
924 _lookup.insert(&_theorySplitQueueRatios);
925 _theorySplitQueueRatios.reliesOn(_useTheorySplitQueues.is(equal(true)));
926 _theorySplitQueueRatios.tag(OptionTag::SATURATION);
927
928 _theorySplitQueueLayeredArrangement = BoolOptionValue("theory_split_queue_layered_arrangement","thsql",true);
929 _theorySplitQueueLayeredArrangement.description = "If turned on, use a layered arrangement to split clauses into queues. Otherwise use a tammet-style-arrangement.";
930 _lookup.insert(&_theorySplitQueueLayeredArrangement);
931 _theorySplitQueueLayeredArrangement.reliesOn(_useTheorySplitQueues.is(equal(true)));
932 _theorySplitQueueLayeredArrangement.tag(OptionTag::SATURATION);
933
934 _useAvatarSplitQueues = BoolOptionValue("avatar_split_queue","avsq",false);
935 _useAvatarSplitQueues.description = "Turn on experiments: clause selection with multiple queues containing different clauses (split by amount of avatar-split-set-size)";
936 _lookup.insert(&_useAvatarSplitQueues);
937 _useAvatarSplitQueues.tag(OptionTag::AVATAR);
938 _avatarSplitQueueCutoffs.reliesOn(_splitting.is(equal(true)));
939
940 _avatarSplitQueueCutoffs = StringOptionValue("avatar_split_queue_cutoffs", "avsqc", "0");
941 _avatarSplitQueueCutoffs.description = "The cutoff-values for the avatar-split-queues (the cutoff value for the last queue is omitted, since it has to be infinity).";
942 _lookup.insert(&_avatarSplitQueueCutoffs);
943 _avatarSplitQueueCutoffs.reliesOn(_useAvatarSplitQueues.is(equal(true)));
944 _avatarSplitQueueCutoffs.tag(OptionTag::AVATAR);
945
946 _avatarSplitQueueRatios = StringOptionValue("avatar_split_queue_ratios", "avsqr", "1,1");
947 _avatarSplitQueueRatios.description = "The ratios for picking clauses from the split-queues using weighted round robin. If a queue is empty, the clause will be picked from the next non-empty queue to the right. Note that this option implicitly also sets the number of queues.";
948 _lookup.insert(&_avatarSplitQueueRatios);
949 _avatarSplitQueueRatios.reliesOn(_useAvatarSplitQueues.is(equal(true)));
950 _avatarSplitQueueRatios.tag(OptionTag::AVATAR);
951
952 _avatarSplitQueueLayeredArrangement = BoolOptionValue("avatar_split_queue_layered_arrangement","avsql",false);
953 _avatarSplitQueueLayeredArrangement.description = "If turned on, use a layered arrangement to split clauses into queues. Otherwise use a tammet-style-arrangement.";
954 _lookup.insert(&_avatarSplitQueueLayeredArrangement);
955 _avatarSplitQueueLayeredArrangement.reliesOn(_useAvatarSplitQueues.is(equal(true)));
956 _avatarSplitQueueLayeredArrangement.tag(OptionTag::AVATAR);
957
958 _useSineLevelSplitQueues = BoolOptionValue("sine_level_split_queue","slsq",false);
959 _useSineLevelSplitQueues.description = "Turn on experiments: clause selection with multiple queues containing different clauses (split by sine-level of clause)";
960 _lookup.insert(&_useSineLevelSplitQueues);
961 _useSineLevelSplitQueues.tag(OptionTag::SATURATION);
962
963 _sineLevelSplitQueueCutoffs = StringOptionValue("sine_level_split_queue_cutoffs", "slsqc", "0,1");
964 _sineLevelSplitQueueCutoffs.description = "The cutoff-values for the sine-level-split-queues (the cutoff value for the last queue is omitted, since it has to be infinity).";
965 _lookup.insert(&_sineLevelSplitQueueCutoffs);
966 _sineLevelSplitQueueCutoffs.reliesOn(_useSineLevelSplitQueues.is(equal(true)));
967 _sineLevelSplitQueueCutoffs.tag(OptionTag::SATURATION);
968
969 _sineLevelSplitQueueRatios = StringOptionValue("sine_level_split_queue_ratios", "slsqr", "1,2,3");
970 _sineLevelSplitQueueRatios.description = "The ratios for picking clauses from the sine-level-split-queues using weighted round robin. If a queue is empty, the clause will be picked from the next non-empty queue to the right. Note that this option implicitly also sets the number of queues.";
971 _lookup.insert(&_sineLevelSplitQueueRatios);
972 _sineLevelSplitQueueRatios.reliesOn(_useSineLevelSplitQueues.is(equal(true)));
973 _sineLevelSplitQueueRatios.tag(OptionTag::SATURATION);
974
975 _sineLevelSplitQueueLayeredArrangement = BoolOptionValue("sine_level_split_queue_layered_arrangement","slsql",true);
976 _sineLevelSplitQueueLayeredArrangement.description = "If turned on, use a layered arrangement to split clauses into queues. Otherwise use a tammet-style-arrangement.";
977 _lookup.insert(&_sineLevelSplitQueueLayeredArrangement);
978 _sineLevelSplitQueueLayeredArrangement.reliesOn(_useSineLevelSplitQueues.is(equal(true)));
979 _sineLevelSplitQueueLayeredArrangement.tag(OptionTag::SATURATION);
980
981 _usePositiveLiteralSplitQueues = BoolOptionValue("positive_literal_split_queue","plsq",false);
982 _usePositiveLiteralSplitQueues.description = "Turn on experiments: clause selection with multiple queues containing different clauses (split by number of positive literals in clause)";
983 _lookup.insert(&_usePositiveLiteralSplitQueues);
984 _usePositiveLiteralSplitQueues.tag(OptionTag::SATURATION);
985
986 _positiveLiteralSplitQueueCutoffs = StringOptionValue("positive_literal_split_queue_cutoffs", "plsqc", "0");
987 _positiveLiteralSplitQueueCutoffs.description = "The cutoff-values for the positive-literal-split-queues (the cutoff value for the last queue is omitted, since it has to be infinity).";
988 _lookup.insert(&_positiveLiteralSplitQueueCutoffs);
989 _positiveLiteralSplitQueueCutoffs.reliesOn(_usePositiveLiteralSplitQueues.is(equal(true)));
990 _positiveLiteralSplitQueueCutoffs.tag(OptionTag::SATURATION);
991
992 _positiveLiteralSplitQueueRatios = StringOptionValue("positive_literal_split_queue_ratios", "plsqr", "1,4");
993 _positiveLiteralSplitQueueRatios.description = "The ratios for picking clauses from the positive-literal-split-queues using weighted round robin. If a queue is empty, the clause will be picked from the next non-empty queue to the right. Note that this option implicitly also sets the number of queues.";
994 _lookup.insert(&_positiveLiteralSplitQueueRatios);
995 _positiveLiteralSplitQueueRatios.reliesOn(_usePositiveLiteralSplitQueues.is(equal(true)));
996 _positiveLiteralSplitQueueRatios.tag(OptionTag::SATURATION);
997
998 _positiveLiteralSplitQueueLayeredArrangement = BoolOptionValue("positive_literal_split_queue_layered_arrangement","plsql",false);
999 _positiveLiteralSplitQueueLayeredArrangement.description = "If turned on, use a layered arrangement to split clauses into queues. Otherwise use a tammet-style-arrangement.";
1000 _lookup.insert(&_positiveLiteralSplitQueueLayeredArrangement);
1001 _positiveLiteralSplitQueueLayeredArrangement.reliesOn(_usePositiveLiteralSplitQueues.is(equal(true)));
1002 _positiveLiteralSplitQueueLayeredArrangement.tag(OptionTag::SATURATION);
1003
1004 _literalMaximalityAftercheck = BoolOptionValue("literal_maximality_aftercheck","lma",false);
1005 _literalMaximalityAftercheck.description =
1006 "For efficiency we perform maximality checks before applying substitutions. Sometimes this can "
1007 "lead to generating more clauses than needed for completeness. Set this on to add the checks "
1008 "afterwards as well.";
1009 _lookup.insert(&_literalMaximalityAftercheck);
1010 _literalMaximalityAftercheck.tag(OptionTag::SATURATION);
1011
1012 _lrsFirstTimeCheck = IntOptionValue("lrs_first_time_check","",5);
1013 _lrsFirstTimeCheck.description=
1014 "Percentage of time limit at which the LRS algorithm will for the first time estimate the number of reachable clauses.";
1015 _lookup.insert(&_lrsFirstTimeCheck);
1016 _lrsFirstTimeCheck.tag(OptionTag::LRS);
1017 _lrsFirstTimeCheck.addConstraint(greaterThanEq(0));
1018 _lrsFirstTimeCheck.addConstraint(lessThan(100));
1019
1020 _lrsWeightLimitOnly = BoolOptionValue("lrs_weight_limit_only","lwlo",false);
1021 _lrsWeightLimitOnly.description=
1022 "If off, the lrs sets both age and weight limit according to clause reachability, otherwise it sets the age limit to 0 and only the weight limit reflects reachable clauses";
1023 _lookup.insert(&_lrsWeightLimitOnly);
1024 _lrsWeightLimitOnly.tag(OptionTag::LRS);
1025
1026 _simulatedTimeLimit = TimeLimitOptionValue("simulated_time_limit","stl",0);
1027 _simulatedTimeLimit.description=
1028 "Time limit in seconds for the purpose of reachability estimations of the LRS saturation algorithm (if 0, the actual time limit is used)";
1029 _lookup.insert(&_simulatedTimeLimit);
1030 _simulatedTimeLimit.tag(OptionTag::LRS);
1031
1032
1033 //*********************** Inferences ***********************
1034
1035 #if VZ3
1036
1037 _theoryInstAndSimp = ChoiceOptionValue<TheoryInstSimp>("theory_instantiation","thi",
1038 TheoryInstSimp::OFF,{"off","all","strong","overlap","full","new"});
1039 _theoryInstAndSimp.description = "";
1040 _theoryInstAndSimp.tag(OptionTag::INFERENCES);
1041 _lookup.insert(&_theoryInstAndSimp);
1042 #endif
1043 _unificationWithAbstraction = ChoiceOptionValue<UnificationWithAbstraction>("unification_with_abstraction","uwa",
1044 UnificationWithAbstraction::OFF,
1045 {"off","interpreted_only","one_side_interpreted","one_side_constant","all","ground"});
1046 _unificationWithAbstraction.description=
1047 "During unification, if two terms s and t fail to unify we will introduce a constraint s!=t and carry on. For example, "
1048 "resolving p(1) \\/ C with ~p(a+2) would produce C \\/ 1 !=a+2. This is controlled by a check on the terms. The expected "
1049 "use case is in theory reasoning. The possible values are:"
1050 "- off: do not introduce a constraint\n"
1051 "- interpreted_only: only if s and t have interpreted top symbols\n"
1052 "- one_side_interpreted: only if one of s or t have interpreted top symbols\n"
1053 "- one_side_constant: only if one of s or t is an interpreted constant (e.g. a number)\n"
1054 "- all: always apply\n"
1055 "- ground: only if both s and t are ground\n"
1056 "See Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning for further details.";
1057 _unificationWithAbstraction.tag(OptionTag::INFERENCES);
1058 _lookup.insert(&_unificationWithAbstraction);
1059
1060 _useACeval = BoolOptionValue("use_ac_eval","uace",true);
1061 _useACeval.description="Evaluate associative and commutative operators e.g. + and *.";
1062 _useACeval.tag(OptionTag::INFERENCES);
1063 _lookup.insert(&_useACeval);
1064
1065 _inequalityNormalization = BoolOptionValue("normalize_inequalities","norm_ineq",false);
1066 _inequalityNormalization.description="Enable normalizing of inequalities like s < t ==> 0 < t - s.";
1067 _lookup.insert(&_inequalityNormalization);
1068 _inequalityNormalization.tag(OptionTag::INFERENCES);
1069
1070 _gaussianVariableElimination = BoolOptionValue("gaussian_variable_elimination","gve",false);
1071 _gaussianVariableElimination.description=
1072 "Enable the immideate simplification \"Gaussian Variable Elimination\":\n"
1073 "\n"
1074 "s != t | C[X] \n"
1075 "------------- if s != t can be rewritten to X != r \n"
1076 " C[r] \n"
1077 "\n"
1078 "example:\n"
1079 "\n"
1080 "6 * X0 != 2 * X1 | p(X0, X1)\n"
1081 "-------------------------------\n"
1082 " p(2 * X1 / 6, X1)";
1083
1084 _lookup.insert(&_gaussianVariableElimination);
1085 _gaussianVariableElimination.tag(OptionTag::INFERENCES);
1086
1087
1088 _induction = ChoiceOptionValue<Induction>("induction","ind",Induction::NONE,
1089 {"none","struct","math","both"});
1090 _induction.description = "Apply structural and/or mathematical induction on datatypes and integers.";
1091 _induction.tag(OptionTag::INFERENCES);
1092 _lookup.insert(&_induction);
1093 //_induction.setRandomChoices
1094
1095 _structInduction = ChoiceOptionValue<StructuralInductionKind>("structural_induction_kind","sik",
1096 StructuralInductionKind::ONE,{"one","two","three","all"});
1097 _structInduction.description="The kind of structural induction applied";
1098 _structInduction.tag(OptionTag::INFERENCES);
1099 _structInduction.reliesOn(Or(_induction.is(equal(Induction::STRUCTURAL)),_induction.is(equal(Induction::BOTH))));
1100 _lookup.insert(&_structInduction);
1101
1102 _mathInduction = ChoiceOptionValue<MathInductionKind>("math_induction_kind","mik",
1103 MathInductionKind::ONE,{"one","two","all"});
1104 _mathInduction.description="The kind of mathematical induction applied";
1105 _mathInduction.tag(OptionTag::INFERENCES);
1106 _mathInduction.reliesOn(Or(_induction.is(equal(Induction::MATHEMATICAL)),_induction.is(equal(Induction::BOTH))));
1107 //_lookup.insert(&_mathInduction);
1108
1109 _inductionChoice = ChoiceOptionValue<InductionChoice>("induction_choice","indc",InductionChoice::ALL,
1110 {"all","goal","goal_plus"});
1111 _inductionChoice.description="Where to apply induction. Goal only applies to constants in goal, goal_plus"
1112 " extends this with skolem constants introduced by induction. Consider using"
1113 " guess_the_goal for problems in SMTLIB as they do not come with a conjecture";
1114 _inductionChoice.tag(OptionTag::INFERENCES);
1115 _lookup.insert(&_inductionChoice);
1116 _inductionChoice.reliesOn(_induction.is(notEqual(Induction::NONE)));
1117 //_inductionChoice.addHardConstraint(If(equal(InductionChoice::GOAL)->Or(equal(InductionChoice::GOAL_PLUS))).then(
1118 // _inputSyntax.is(equal(InputSyntax::TPTP))->Or<InductionChoice>(_guessTheGoal.is(equal(true)))));
1119
1120
1121 _maxInductionDepth = UnsignedOptionValue("induction_max_depth","indmd",0);
1122 _maxInductionDepth.description = "Set maximum depth of induction where 0 means no max.";
1123 _maxInductionDepth.tag(OptionTag::INFERENCES);
1124 _maxInductionDepth.reliesOn(_induction.is(notEqual(Induction::NONE)));
1125 _maxInductionDepth.addHardConstraint(lessThan(33u));
1126 _lookup.insert(&_maxInductionDepth);
1127
1128 _inductionNegOnly = BoolOptionValue("induction_neg_only","indn",true);
1129 _inductionNegOnly.description = "Only apply induction to negative literals";
1130 _inductionNegOnly.tag(OptionTag::INFERENCES);
1131 _inductionNegOnly.reliesOn(_induction.is(notEqual(Induction::NONE)));
1132 _lookup.insert(&_inductionNegOnly);
1133
1134 _inductionUnitOnly = BoolOptionValue("induction_unit_only","indu",true);
1135 _inductionUnitOnly.description = "Only apply induction to unit clauses";
1136 _inductionUnitOnly.tag(OptionTag::INFERENCES);
1137 _inductionUnitOnly.reliesOn(_induction.is(notEqual(Induction::NONE)));
1138 _lookup.insert(&_inductionUnitOnly);
1139
1140 _inductionGen = BoolOptionValue("induction_gen","indgen",false);
1141 _inductionGen.description = "Apply induction with generalization (on both all & selected occurrences)";
1142 _inductionGen.tag(OptionTag::INFERENCES);
1143 _inductionGen.reliesOn(_induction.is(notEqual(Induction::NONE)));
1144 _lookup.insert(&_inductionGen);
1145
1146 _maxInductionGenSubsetSize = UnsignedOptionValue("max_induction_gen_subset_size","indgenss",3);
1147 _maxInductionGenSubsetSize.description = "Set maximum number of occurrences of the induction term to be"
1148 " generalized, where 0 means no max. (Regular induction will"
1149 " be applied without this restriction.)";
1150 _maxInductionGenSubsetSize.tag(OptionTag::INFERENCES);
1151 _maxInductionGenSubsetSize.reliesOn(_inductionGen.is(equal(true)));
1152 _maxInductionGenSubsetSize.addHardConstraint(lessThan(10u));
1153 _lookup.insert(&_maxInductionGenSubsetSize);
1154
1155 _inductionOnComplexTerms = BoolOptionValue("induction_on_complex_terms","indoct",false);
1156 _inductionOnComplexTerms.description = "Apply induction on complex (ground) terms vs. only on constants";
1157 _inductionOnComplexTerms.tag(OptionTag::INFERENCES);
1158 _inductionOnComplexTerms.reliesOn(_induction.is(notEqual(Induction::NONE)));
1159 _lookup.insert(&_inductionOnComplexTerms);
1160
1161 _instantiation = ChoiceOptionValue<Instantiation>("instantiation","inst",Instantiation::OFF,{"off","on"});
1162 _instantiation.description = "Heuristically instantiate variables. Often wastes a lot of effort. Consider using thi instead.";
1163 _instantiation.tag(OptionTag::INFERENCES);
1164 _lookup.insert(&_instantiation);
1165 _instantiation.setRandomChoices({"off","on"}); // Turn this on rarely
1166
1167 _backwardDemodulation = ChoiceOptionValue<Demodulation>("backward_demodulation","bd",
1168 Demodulation::ALL,
1169 {"all","off","preordered"});
1170 _backwardDemodulation.description=
1171 "Oriented rewriting of kept clauses by newly derived unit equalities\n"
1172 "s = t L[sθ] \\/ C\n"
1173 "--------------------- where sθ > tθ (replaces RHS)\n"
1174 " L[tθ] \\/ C\n";
1175 _lookup.insert(&_backwardDemodulation);
1176 _backwardDemodulation.tag(OptionTag::INFERENCES);
1177 _backwardDemodulation.addProblemConstraint(hasEquality());
1178 _backwardDemodulation.reliesOn(Or(_saturationAlgorithm.is(notEqual(SaturationAlgorithm::INST_GEN)),_instGenWithResolution.is(equal(true))));
1179 _backwardDemodulation.setRandomChoices({"all","off"});
1180
1181 _backwardSubsumption = ChoiceOptionValue<Subsumption>("backward_subsumption","bs",
1182 Subsumption::OFF,{"off","on","unit_only"});
1183 _backwardSubsumption.description=
1184 "Perform subsumption deletion of kept clauses by newly derived clauses. Unit_only means that the subsumption will be performed only by unit clauses";
1185 _lookup.insert(&_backwardSubsumption);
1186 _backwardSubsumption.tag(OptionTag::INFERENCES);
1187 _backwardSubsumption.reliesOn(Or(_saturationAlgorithm.is(notEqual(SaturationAlgorithm::INST_GEN)),_instGenWithResolution.is(equal(true))));
1188 _backwardSubsumption.setRandomChoices({"on","off"});
1189
1190 _backwardSubsumptionResolution = ChoiceOptionValue<Subsumption>("backward_subsumption_resolution","bsr",
1191 Subsumption::OFF,{"off","on","unit_only"});
1192 _backwardSubsumptionResolution.description=
1193 "Perform subsumption resolution on kept clauses using newly derived clauses. Unit_only means that the subsumption resolution will be performed only by unit clauses";
1194 _lookup.insert(&_backwardSubsumptionResolution);
1195 _backwardSubsumptionResolution.tag(OptionTag::INFERENCES);
1196 _backwardSubsumptionResolution.reliesOn(Or(_saturationAlgorithm.is(notEqual(SaturationAlgorithm::INST_GEN)),_instGenWithResolution.is(equal(true))));
1197 _backwardSubsumptionResolution.setRandomChoices({"on","off"});
1198
1199 _backwardSubsumptionDemodulation = BoolOptionValue("backward_subsumption_demodulation", "bsd", false);
1200 _backwardSubsumptionDemodulation.description = "Perform backward subsumption demodulation.";
1201 _lookup.insert(&_backwardSubsumptionDemodulation);
1202 _backwardSubsumptionDemodulation.tag(OptionTag::INFERENCES);
1203 _backwardSubsumptionDemodulation.addProblemConstraint(hasEquality());
1204 _backwardSubsumptionDemodulation.setRandomChoices({"on","off"});
1205
1206 _backwardSubsumptionDemodulationMaxMatches = UnsignedOptionValue("backward_subsumption_demodulation_max_matches", "bsdmm", 0);
1207 _backwardSubsumptionDemodulationMaxMatches.description = "Maximum number of multi-literal matches to consider in backward subsumption demodulation. 0 means to try all matches (until first success).";
1208 _lookup.insert(&_backwardSubsumptionDemodulationMaxMatches);
1209 _backwardSubsumptionDemodulationMaxMatches.tag(OptionTag::INFERENCES);
1210 _backwardSubsumptionDemodulationMaxMatches.setRandomChoices({"0", "1", "3"});
1211
1212 _binaryResolution = BoolOptionValue("binary_resolution","br",true);
1213 _binaryResolution.description=
1214 "Standard binary resolution i.e.\n"
1215 "C \\/ t D \\/ s\n"
1216 "---------------------\n"
1217 "(C \\/ D)θ\n"
1218 "where θ = mgu(t,-s) and t selected";
1219 _lookup.insert(&_binaryResolution);
1220 _binaryResolution.tag(OptionTag::INFERENCES);
1221 // If urr is off then binary resolution should be on
1222 _binaryResolution.addConstraint(
1223 If(equal(false)).then(_unitResultingResolution.is(notEqual(URResolution::OFF))));
1224 _binaryResolution.setRandomChoices(And(isRandSat(),saNotInstGen(),Or(hasEquality(),isBfnt(),hasCat(Property::HNE))),{"on"});
1225 _binaryResolution.setRandomChoices({"on","off"});
1226
1227
1228 _condensation = ChoiceOptionValue<Condensation>("condensation","cond",Condensation::OFF,{"fast","off","on"});
1229 _condensation.description=
1230 "Perform condensation. If 'fast' is specified, we only perform condensations that are easy to check for.";
1231 _lookup.insert(&_condensation);
1232 _condensation.tag(OptionTag::INFERENCES);
1233 _condensation.reliesOn(Or(_saturationAlgorithm.is(notEqual(SaturationAlgorithm::INST_GEN)),_instGenWithResolution.is(equal(true))));
1234 _condensation.setRandomChoices({"on","off","fast"});
1235
1236 _demodulationRedundancyCheck = BoolOptionValue("demodulation_redundancy_check","drc",true);
1237 _demodulationRedundancyCheck.description=
1238 "Avoids the following cases of backward and forward demodulation, as they do not preserve completeness:\n"
1239 "s = t s = t1 \\/ C \t s = t s != t1 \\/ C\n"
1240
1241 "--------------------- \t ---------------------\n"
1242 "t = t1 \\/ C \t\t t != t1 \\/ C\n"
1243 "where t > t1 and s = t > C (RHS replaced)";
1244 _lookup.insert(&_demodulationRedundancyCheck);
1245 _demodulationRedundancyCheck.tag(OptionTag::INFERENCES);
1246 _demodulationRedundancyCheck.reliesOn(Or(_saturationAlgorithm.is(notEqual(SaturationAlgorithm::INST_GEN)),_instGenWithResolution.is(equal(true))));
1247 _demodulationRedundancyCheck.addProblemConstraint(hasEquality());
1248 _demodulationRedundancyCheck.setRandomChoices({"on","off"});
1249
1250
1251 _extensionalityAllowPosEq = BoolOptionValue( "extensionality_allow_pos_eq","",false);
1252 _extensionalityAllowPosEq.description="If extensionality resolution equals filter, this dictates"
1253 " whether we allow other positive equalities when recognising extensionality clauses";
1254 _lookup.insert(&_extensionalityAllowPosEq);
1255 _extensionalityAllowPosEq.tag(OptionTag::INFERENCES);
1256 _extensionalityAllowPosEq.reliesOn(_extensionalityResolution.is(equal(ExtensionalityResolution::FILTER)));
1257 _extensionalityAllowPosEq.setRandomChoices({"on","off","off"}); // Prefer off
1258
1259 _extensionalityMaxLength = UnsignedOptionValue("extensionality_max_length","",0);
1260 _extensionalityMaxLength.description="Sets the maximum length (number of literals) an extensionality"
1261 " clause can have when doing recognition for extensionality resolution. If zero there is no maximum.";
1262 _lookup.insert(&_extensionalityMaxLength);
1263 _extensionalityMaxLength.tag(OptionTag::INFERENCES);
1264 // 0 means infinity, so it is intentionally not if (unsignedValue < 2).
1265 _extensionalityMaxLength.addConstraint(notEqual(1u));
1266 _extensionalityMaxLength.reliesOn(_extensionalityResolution.is(notEqual(ExtensionalityResolution::OFF)));
1267 //TODO does this depend on anything?
1268 _extensionalityMaxLength.setRandomChoices({"0","0","0","2","3"}); // TODO what are good values?
1269
1270 _extensionalityResolution = ChoiceOptionValue<ExtensionalityResolution>("extensionality_resolution","er",
1271 ExtensionalityResolution::OFF,{"filter","known","tagged","off"});
1272 _extensionalityResolution.description=
1273 "Turns on the following inference rule:\n"
1274 " x=y \\/ C s != t \\/ D\n"
1275 " -----------------------\n"
1276 " C{x → s, y → t} \\/ D\n"
1277 "Where s!=t is selected in s!=t \\/D and x=y \\/ C is a recognised as an extensionality clause - how clauses are recognised depends on the value of this option.\n"
1278 "If filter we attempt to recognise all extensionality clauses i.e. those that have exactly one X=Y, no inequality of the same sort as X-Y (and optionally no equality except X=Y, see extensionality_allow_pos_eq).\n"
1279 "If known we only recognise a known set of extensionality clauses. At the moment this includes the standard and subset-based formulations of the set extensionality axiom, as well as the array extensionality axiom.\n"
1280 "If tagged we only use formulas tagged as extensionality clauses.";
1281 _lookup.insert(&_extensionalityResolution);
1282 _extensionalityResolution.tag(OptionTag::INFERENCES);
1283 // Captures that if ExtensionalityResolution is not off then inequality splitting must be 0
1284 _extensionalityResolution.reliesOn(_inequalitySplitting.is(equal(0)));
1285 _extensionalityResolution.setRandomChoices({"filter","known","off","off"});
1286
1287 _FOOLParamodulation = BoolOptionValue("fool_paramodulation","foolp",false);
1288 _FOOLParamodulation.description=
1289 "Turns on the following inference rule:\n"
1290 " C[s]\n"
1291 "--------------------,\n"
1292 "C[true] \\/ s = false\n"
1293 "where s is a boolean term that is not a variable, true or false, C[true] is "
1294 "the C clause with s substituted by true. This rule is needed for effecient "
1295 "treatment of boolean terms.";
1296 _lookup.insert(&_FOOLParamodulation);
1297 _FOOLParamodulation.tag(OptionTag::INFERENCES);
1298
1299 _termAlgebraInferences = BoolOptionValue("term_algebra_rules","tar",true);
1300 _termAlgebraInferences.description=
1301 "Activates some rules that improve reasoning with term algebras (such as algebraic datatypes in SMT-LIB):\n"
1302 "If the problem does not contain any term algebra symbols, activating this options has no effect\n"
1303 "- distinctness rule:\n"
1304 "f(...) = g(...) \\/ A\n"
1305 "--------------------\n"
1306 " A \n"
1307 "where f and g are distinct term algebra constructors\n"
1308 "- distinctness tautology deletion: clauses of the form f(...) ~= g(...) \\/ A are deleted\n"
1309 "- injectivity rule:\n"
1310 "f(s1 ... sn) = f(t1 ... tn) \\/ A\n"
1311 "--------------------------------\n"
1312 " s1 = t1 \\/ A\n"
1313 " ...\n"
1314 " sn = tn \\/ A";
1315 _lookup.insert(&_termAlgebraInferences);
1316 _termAlgebraInferences.tag(OptionTag::INFERENCES);
1317
1318 _termAlgebraCyclicityCheck = ChoiceOptionValue<TACyclicityCheck>("term_algebra_acyclicity","tac",
1319 TACyclicityCheck::OFF,{"off","axiom","rule","light"});
1320 _termAlgebraCyclicityCheck.description=
1321 "Activates the cyclicity rule for term algebras (such as algebraic datatypes in SMT-LIB):\n"
1322 "- off : the cyclicity rule is not enforced (this is sound but incomplete)\n"
1323 "- axiom : the cyclicity rule is axiomatized with a transitive predicate describing the subterm relation over terms\n"
1324 "- rule : the cyclicity rule is enforced by a specific hyper-resolution rule\n"
1325 "- light : the cyclicity rule is enforced by rule generating disequality between a term and its known subterms";
1326 _lookup.insert(&_termAlgebraCyclicityCheck);
1327 _termAlgebraCyclicityCheck.tag(OptionTag::INFERENCES);
1328
1329 _forwardDemodulation = ChoiceOptionValue<Demodulation>("forward_demodulation","fd",Demodulation::ALL,{"all","off","preordered"});
1330 _forwardDemodulation.description=
1331 "Oriented rewriting of newly derived clauses by kept unit equalities\n"
1332 "s = t L[sθ] \\/ C\n"
1333 "--------------------- where sθ > tθ\n"
1334 " L[tθ] \\/ C\n"
1335 "If 'preordered' is set, only equalities s = t where s > t are used for rewriting.";
1336 _lookup.insert(&_forwardDemodulation);
1337 _forwardDemodulation.tag(OptionTag::INFERENCES);
1338 _forwardDemodulation.setRandomChoices({"all","all","all","off","preordered"});
1339
1340 _forwardLiteralRewriting = BoolOptionValue("forward_literal_rewriting","flr",false);
1341 _forwardLiteralRewriting.description="Perform forward literal rewriting.";
1342 _lookup.insert(&_forwardLiteralRewriting);
1343 _forwardLiteralRewriting.tag(OptionTag::INFERENCES);
1344 _forwardLiteralRewriting.addProblemConstraint(hasNonUnits());
1345 _forwardLiteralRewriting.reliesOn(Or(_saturationAlgorithm.is(notEqual(SaturationAlgorithm::INST_GEN)),_instGenWithResolution.is(equal(true))));
1346 _forwardLiteralRewriting.setRandomChoices({"on","off"});
1347
1348 _forwardSubsumption = BoolOptionValue("forward_subsumption","fs",true);
1349 _forwardSubsumption.description="Perform forward subsumption deletion.";
1350 _lookup.insert(&_forwardSubsumption);
1351 _forwardSubsumption.tag(OptionTag::INFERENCES);
1352 _forwardSubsumption.setRandomChoices({"on","on","on","on","on","on","on","on","on","off"}); // turn this off rarely
1353
1354 _forwardSubsumptionResolution = BoolOptionValue("forward_subsumption_resolution","fsr",true);
1355 _forwardSubsumptionResolution.description="Perform forward subsumption resolution.";
1356 _lookup.insert(&_forwardSubsumptionResolution);
1357 _forwardSubsumptionResolution.tag(OptionTag::INFERENCES);
1358
1359 _forwardSubsumptionResolution.reliesOn(Or(_saturationAlgorithm.is(notEqual(SaturationAlgorithm::INST_GEN)),_instGenWithResolution.is(equal(true))));
1360 _forwardSubsumptionResolution.setRandomChoices({"on","off"});
1361
1362 _forwardSubsumptionDemodulation = BoolOptionValue("forward_subsumption_demodulation", "fsd", false);
1363 _forwardSubsumptionDemodulation.description = "Perform forward subsumption demodulation.";
1364 _lookup.insert(&_forwardSubsumptionDemodulation);
1365 _forwardSubsumptionDemodulation.tag(OptionTag::INFERENCES);
1366 _forwardSubsumptionDemodulation.addProblemConstraint(hasEquality());
1367 _forwardSubsumptionDemodulation.setRandomChoices({"off","on"});
1368
1369 _forwardSubsumptionDemodulationMaxMatches = UnsignedOptionValue("forward_subsumption_demodulation_max_matches", "fsdmm", 0);
1370 _forwardSubsumptionDemodulationMaxMatches.description = "Maximum number of multi-literal matches to consider in forward subsumption demodulation. 0 means to try all matches (until first success).";
1371 _lookup.insert(&_forwardSubsumptionDemodulationMaxMatches);
1372 _forwardSubsumptionDemodulationMaxMatches.tag(OptionTag::INFERENCES);
1373 _forwardSubsumptionDemodulationMaxMatches.setRandomChoices({"0", "1", "3"});
1374
1375 _hyperSuperposition = BoolOptionValue("hyper_superposition","",false);
1376 _hyperSuperposition.description=
1377 "Simplifying inference that attempts to do several rewritings at once if it will eliminate literals of the original clause (now we aim just for elimination by equality resolution)";
1378 _lookup.insert(&_hyperSuperposition);
1379 _hyperSuperposition.tag(OptionTag::INFERENCES);
1380
1381 _simultaneousSuperposition = BoolOptionValue("simultaneous_superposition","sims",true);
1382 _simultaneousSuperposition.description="Rewrite the whole RHS clause during superposition, not just the target literal.";
1383 _lookup.insert(&_simultaneousSuperposition);
1384 _simultaneousSuperposition.tag(OptionTag::INFERENCES);
1385
1386 _innerRewriting = BoolOptionValue("inner_rewriting","irw",false);
1387 _innerRewriting.description="C[t_1] | t1 != t2 ==> C[t_2] | t1 != t2 when t1>t2";
1388 _lookup.insert(&_innerRewriting);
1389 _innerRewriting.tag(OptionTag::INFERENCES);
1390
1391 _equationalTautologyRemoval = BoolOptionValue("equational_tautology_removal","etr",false);
1392 _equationalTautologyRemoval.description="A reduction which uses congruence closure to remove logically valid clauses.";
1393 _lookup.insert(&_equationalTautologyRemoval);
1394 _equationalTautologyRemoval.tag(OptionTag::INFERENCES);
1395
1396 _unitResultingResolution = ChoiceOptionValue<URResolution>("unit_resulting_resolution","urr",URResolution::OFF,{"ec_only","off","on"});
1397 _unitResultingResolution.description=
1398 "Uses unit resulting resolution only to derive empty clauses (may be useful for splitting)";
1399 _lookup.insert(&_unitResultingResolution);
1400 _unitResultingResolution.tag(OptionTag::INFERENCES);
1401 // Wrong, should instead suggest that urr is always used with inst_gen
1402 //_unitResultingResolution.reliesOn(
1403 // _saturationAlgorithm.is(notEqual(SaturationAlgorithm::INST_GEN))->And<URResolution,bool>(
1404 // _instGenWithResolution.is(notEqual(true))));
1405 _unitResultingResolution.addProblemConstraint(hasPredicates());
1406 // If br has already been set off then this will be forced on, if br has not yet been set
1407 // then setting this to off will force br on
1408 _unitResultingResolution.setRandomChoices(And(isRandSat(),saNotInstGen(),Or(hasEquality(),isBfnt(),hasCat(Property::HNE))),{"on","off"});
1409 _unitResultingResolution.setRandomChoices(isRandSat(),{});
1410 _unitResultingResolution.setRandomChoices({"on","on","off"});
1411
1412
1413 _superpositionFromVariables = BoolOptionValue("superposition_from_variables","sfv",true);
1414 _superpositionFromVariables.description="Perform superposition from variables.";
1415 _lookup.insert(&_superpositionFromVariables);
1416 _superpositionFromVariables.tag(OptionTag::INFERENCES);
1417 _superpositionFromVariables.addProblemConstraint(hasEquality());
1418 _superpositionFromVariables.reliesOn(Or(_saturationAlgorithm.is(notEqual(SaturationAlgorithm::INST_GEN)),_instGenWithResolution.is(equal(true))));
1419 _superpositionFromVariables.setRandomChoices({"on","off"});
1420
1421 //*********************** InstGen ***********************
1422
1423 _globalSubsumption = BoolOptionValue("global_subsumption","gs",false);
1424 _globalSubsumption.description="Perform global subsumption. Use a set of groundings of generated clauses G to replace C \\/ L by C if the grounding of C is implied by G. A SAT solver is used for ground reasoning.";
1425 _lookup.insert(&_globalSubsumption);
1426 _globalSubsumption.tag(OptionTag::INFERENCES);
1427 _globalSubsumption.addProblemConstraint(hasNonUnits());
1428 _globalSubsumption.setRandomChoices({"off","on"});
1429
1430 _globalSubsumptionSatSolverPower = ChoiceOptionValue<GlobalSubsumptionSatSolverPower>("global_subsumption_sat_solver_power","gsssp",
1431 GlobalSubsumptionSatSolverPower::PROPAGATION_ONLY,{"propagation_only","full"});
1432 _globalSubsumptionSatSolverPower.description="";
1433 _lookup.insert(&_globalSubsumptionSatSolverPower);
1434 _globalSubsumptionSatSolverPower.tag(OptionTag::INFERENCES);
1435 _globalSubsumptionSatSolverPower.reliesOn(_globalSubsumption.is(equal(true)));
1436 _globalSubsumptionSatSolverPower.setRandomChoices({"propagation_only","full"});
1437
1438 _globalSubsumptionExplicitMinim = ChoiceOptionValue<GlobalSubsumptionExplicitMinim>("global_subsumption_explicit_minim","gsem",
1439 GlobalSubsumptionExplicitMinim::RANDOMIZED,{"off","on","randomized"});
1440 _globalSubsumptionSatSolverPower.description="Explicitly minimize the result of global sumsumption reduction.";
1441 _lookup.insert(&_globalSubsumptionExplicitMinim);
1442 _globalSubsumptionExplicitMinim.tag(OptionTag::INFERENCES);
1443 _globalSubsumptionExplicitMinim.reliesOn(_globalSubsumption.is(equal(true)));
1444 _globalSubsumptionExplicitMinim.setRandomChoices({"off","on","randomized"});
1445
1446 _globalSubsumptionAvatarAssumptions = ChoiceOptionValue<GlobalSubsumptionAvatarAssumptions>("global_subsumption_avatar_assumptions","gsaa",
1447 GlobalSubsumptionAvatarAssumptions::OFF,{"off","from_current","full_model"});
1448 _globalSubsumptionAvatarAssumptions.description=
1449 "When running global subsumption and AVATAR at the same time we need to include information about the current AVATAR model. When this is off "
1450 "we ignore clauses with AVATAR assumptions for GS. When it is from_current we assume the assumptions in the current clause. When it is "
1451 "full_model we assume the full model from AVATAR. See paper Global Subsumption Revisited (Briefly).";
1452 _lookup.insert(&_globalSubsumptionAvatarAssumptions);
1453 _globalSubsumptionAvatarAssumptions.tag(OptionTag::INFERENCES);
1454 _globalSubsumptionAvatarAssumptions.reliesOn(_globalSubsumption.is(equal(true)));
1455 _globalSubsumptionAvatarAssumptions.reliesOn(_splitting.is(equal(true)));
1456 _globalSubsumptionAvatarAssumptions.setRandomChoices({"off","from_current","full_model"});
1457
1458 _instGenBigRestartRatio = FloatOptionValue("inst_gen_big_restart_ratio","igbrr",0.0);
1459 _instGenBigRestartRatio.description=
1460 "Determines how often a big restart (instance generation starts from input clauses) will be performed. Small restart means all clauses generated so far are processed again.";
1461 _lookup.insert(&_instGenBigRestartRatio);
1462 _instGenBigRestartRatio.tag(OptionTag::INST_GEN);
1463 _instGenBigRestartRatio.addConstraint(And(greaterThanEq(0.0f),lessThanEq(1.0f)));
1464 // Captures that this is only non-default when saturationAlgorithm is instgen
1465 _instGenBigRestartRatio.reliesOn(_saturationAlgorithm.is(equal(SaturationAlgorithm::INST_GEN)));
1466 _instGenBigRestartRatio.setRandomChoices({"0.0","0.1","0.2","0.3","0.4","0.5","0.6","0.7","0.8","0.9","1.0"});
1467
1468 _instGenPassiveReactivation = BoolOptionValue("inst_gen_passive_reactivation","igpr",false);
1469 _instGenPassiveReactivation.description="When the model describing the selection function changes some active clauses may become lazily deselected. If passive reaction is selected these clauses are added into the passive set before recomputing the next model, otherwise they are added back to active.";
1470 _lookup.insert(&_instGenPassiveReactivation);
1471 _instGenPassiveReactivation.tag(OptionTag::INST_GEN);
1472 _instGenPassiveReactivation.reliesOn(_saturationAlgorithm.is(equal(SaturationAlgorithm::INST_GEN)));
1473
1474 _instGenResolutionInstGenRatio = RatioOptionValue("inst_gen_resolution_ratio","igrr",1,1,'/');
1475 _instGenResolutionInstGenRatio.description=
1476 "Ratio of resolution and instantiation steps (applies only if inst_gen_with_resolution is on)";
1477 _lookup.insert(&_instGenResolutionInstGenRatio);
1478 _instGenResolutionInstGenRatio.tag(OptionTag::INST_GEN);
1479 _instGenResolutionInstGenRatio.reliesOn(_saturationAlgorithm.is(equal(SaturationAlgorithm::INST_GEN)));
1480 _instGenResolutionInstGenRatio.reliesOn(_instGenWithResolution.is(equal(true)));
1481 _instGenResolutionInstGenRatio.setRandomChoices({"128/1","64/1","32/1","16/1","8/1","4/1","2/1","1/1","1/2","1/4","1/8","1/16","1/32","1/64","1/128"});
1482
1483 _instGenRestartPeriod = IntOptionValue("inst_gen_restart_period","igrp",1000);
1484 _instGenRestartPeriod.description="How many clauses are processed before restart. The size of the restart depends on inst_gen_big_restart_ratio.";
1485 _lookup.insert(&_instGenRestartPeriod);
1486 _instGenRestartPeriod.tag(OptionTag::INST_GEN);
1487 _instGenRestartPeriod.reliesOn(_saturationAlgorithm.is(equal(SaturationAlgorithm::INST_GEN)));
1488 _instGenRestartPeriod.setRandomChoices({"100","200","400","700","1000","1400","2000","4000"});
1489
1490 _instGenRestartPeriodQuotient = FloatOptionValue("inst_gen_restart_period_quotient","igrpq",1.0);
1491 _instGenRestartPeriodQuotient.description="Restart period is multiplied by this number after each restart.";
1492 _lookup.insert(&_instGenRestartPeriodQuotient);
1493 _instGenRestartPeriodQuotient.tag(OptionTag::INST_GEN);
1494 _instGenRestartPeriodQuotient.addConstraint(greaterThanEq(1.0f));
1495 _instGenRestartPeriodQuotient.reliesOn(_saturationAlgorithm.is(equal(SaturationAlgorithm::INST_GEN)));
1496 _instGenRestartPeriodQuotient.setRandomChoices({"1.0","1.05","1.1","1.2","1.3","1.5","2.0"});
1497
1498 _instGenSelection = SelectionOptionValue("inst_gen_selection","igs",0);
1499 _instGenSelection.description=
1500 "Selection function for InstGen. This is applied *after* model-based selection is applied. "
1501 "For consistency the value 1011 is used to denote look-ahead selection.";
1502 _instGenSelection.addHardConstraint(notEqual(11)); // Use 1011 for look-ahead in InstGen instead.
1503 _lookup.insert(&_instGenSelection);
1504 _instGenSelection.tag(OptionTag::INST_GEN);
1505 _instGenSelection.reliesOn(_saturationAlgorithm.is(equal(SaturationAlgorithm::INST_GEN)));
1506
1507 _instGenWithResolution = BoolOptionValue("inst_gen_with_resolution","igwr",false);
1508 _instGenWithResolution.description=
1509 "Performs instantiation together with resolution (global subsumption index is shared, also clauses generated by the resolution are added to the instance SAT problem)";
1510 _lookup.insert(&_instGenWithResolution);
1511 _instGenWithResolution.tag(OptionTag::INST_GEN);
1512 _instGenWithResolution.reliesOn(_saturationAlgorithm.is(equal(SaturationAlgorithm::INST_GEN)));
1513 _instGenWithResolution.setRandomChoices({"on","off"});
1514
1515 _useHashingVariantIndex = BoolOptionValue("use_hashing_clause_variant_index","uhcvi",false);
1516 _useHashingVariantIndex.description= "Use clause variant index based on hashing for clause variant detection (affects inst_gen and avatar).";
1517 _lookup.insert(&_useHashingVariantIndex);
1518 _useHashingVariantIndex.tag(OptionTag::OTHER);
1519 _useHashingVariantIndex.setRandomChoices({"on","off"});
1520
1521 /*
1522 _use_dm = BoolOptionValue("use_dismatching","dm",false);
1523 _use_dm.description="Use dismatching constraints.";
1524 // Dismatching constraints didn't work and are being discontinued ...
1525 // _lookup.insert(&_use_dm);
1526 _use_dm.tag(OptionTag::INST_GEN);
1527 //_use_dm.setExperimental();
1528 _use_dm.setRandomChoices({"on","off"});
1529 _use_dm.reliesOn(_saturationAlgorithm.is(equal(SaturationAlgorithm::INST_GEN)));
1530 */
1531
1532 _nicenessOption = ChoiceOptionValue<Niceness>("niceness_option","none",Niceness::NONE,{"average","none","sum","top"});
1533 _nicenessOption.description="";
1534 _lookup.insert(&_nicenessOption);
1535 _nicenessOption.tag(OptionTag::INST_GEN);
1536 _nicenessOption.setExperimental();
1537 _nicenessOption.reliesOn(_saturationAlgorithm.is(equal(SaturationAlgorithm::INST_GEN)));
1538 _nicenessOption.reliesOn(_satSolver.is(equal(SatSolver::VAMPIRE)));
1539 _nicenessOption.setRandomChoices({"none","none","none","none","none","average","sum","top"});
1540
1541 //*********************** AVATAR ***********************
1542
1543 _splitting = BoolOptionValue("avatar","av",true);
1544 _splitting.description="Use AVATAR splitting.";
1545 _lookup.insert(&_splitting);
1546 _splitting.tag(OptionTag::AVATAR);
1547 //_splitting.addProblemConstraint(hasNonUnits());
1548 _splitting.setRandomChoices({"on","off"}); //TODO change balance?
1549
1550 _splitAtActivation = BoolOptionValue("split_at_activation","sac",false);
1551 _splitAtActivation.description="Split a clause when it is activated, default is to split when it is processed";
1552 _lookup.insert(&_splitAtActivation);
1553 _splitAtActivation.reliesOn(_splitting.is(equal(true)));
1554 _splitAtActivation.tag(OptionTag::AVATAR);
1555 _splitAtActivation.setRandomChoices({"on","off"});
1556
1557 _splittingAddComplementary = ChoiceOptionValue<SplittingAddComplementary>("avatar_add_complementary","aac",
1558 SplittingAddComplementary::GROUND,{"ground","none"});
1559 _splittingAddComplementary.description="";
1560 _lookup.insert(&_splittingAddComplementary);
1561 _splittingAddComplementary.tag(OptionTag::AVATAR);
1562 _splittingAddComplementary.reliesOn(_splitting.is(equal(true)));
1563 _splittingAddComplementary.setRandomChoices({"ground","none"});
1564
1565
1566 _splittingCongruenceClosure = ChoiceOptionValue<SplittingCongruenceClosure>("avatar_congruence_closure","acc",
1567 SplittingCongruenceClosure::OFF,{"model","off","on"});
1568 _splittingCongruenceClosure.description="Use a congruence closure decision procedure on top of the AVATAR SAT solver. This ensures that models produced by AVATAR satisfy the theory of uninterprted functions.";
1569 _lookup.insert(&_splittingCongruenceClosure);
1570 _splittingCongruenceClosure.tag(OptionTag::AVATAR);
1571 _splittingCongruenceClosure.reliesOn(_splitting.is(equal(true)));
1572 #if VZ3
1573 _splittingCongruenceClosure.reliesOn(_satSolver.is(notEqual(SatSolver::Z3)));
1574 #endif
1575 _splittingCongruenceClosure.addProblemConstraint(hasEquality());
1576 _splittingCongruenceClosure.setRandomChoices({"model","off","on"});
1577 _splittingCongruenceClosure.addHardConstraint(If(equal(SplittingCongruenceClosure::MODEL)).
1578 then(_splittingMinimizeModel.is(notEqual(SplittingMinimizeModel::SCO))));
1579
1580 _ccUnsatCores = ChoiceOptionValue<CCUnsatCores>("cc_unsat_cores","ccuc",CCUnsatCores::ALL,
1581 {"first", "small_ones", "all"});
1582 _ccUnsatCores.description="";
1583 _lookup.insert(&_ccUnsatCores);
1584 _ccUnsatCores.tag(OptionTag::AVATAR);
1585 _ccUnsatCores.reliesOn(_splittingCongruenceClosure.is(notEqual(SplittingCongruenceClosure::OFF)));
1586 _ccUnsatCores.setRandomChoices({"first", "small_ones", "all"});
1587
1588 _splittingLiteralPolarityAdvice = ChoiceOptionValue<SplittingLiteralPolarityAdvice>(
1589 "avatar_literal_polarity_advice","alpa",
1590 SplittingLiteralPolarityAdvice::NONE,
1591 {"false","true","none"});
1592 _splittingLiteralPolarityAdvice.description="Override SAT-solver's default polarity/phase setting for variables abstracting clause components.";
1593 _lookup.insert(&_splittingLiteralPolarityAdvice);
1594 _splittingLiteralPolarityAdvice.tag(OptionTag::AVATAR);
1595 _splittingLiteralPolarityAdvice.reliesOn(_splitting.is(equal(true)));
1596
1597 _splittingMinimizeModel = ChoiceOptionValue<SplittingMinimizeModel>("avatar_minimize_model","amm",
1598 SplittingMinimizeModel::ALL,{"off","sco","all"});
1599
1600 _splittingMinimizeModel.description="Minimize the SAT-solver model by replacing concrete values with don't-cares"
1601 " provided <all> the sat clauses (or only the split clauses with <sco>) remain provably satisfied"
1602 " by the partial model.";
1603 _lookup.insert(&_splittingMinimizeModel);
1604 _splittingMinimizeModel.tag(OptionTag::AVATAR);
1605 _splittingMinimizeModel.reliesOn(_splitting.is(equal(true)));
1606 _splittingMinimizeModel.setRandomChoices({"off","sco","all"});
1607
1608 _splittingEagerRemoval = BoolOptionValue("avatar_eager_removal","aer",true);
1609 _splittingEagerRemoval.description="If a component was in the model and then becomes 'don't care' eagerly remove that component from the first-order solver. Note: only has any impact when smm is used.";
1610 _lookup.insert(&_splittingEagerRemoval);
1611 _splittingEagerRemoval.tag(OptionTag::AVATAR);
1612 _splittingEagerRemoval.reliesOn(_splitting.is(equal(true)));
1613 // if minimize is off then makes no difference
1614 // if minimize is sco then we could have a conflict clause added infinitely often
1615 _splittingEagerRemoval.reliesOn(_splittingMinimizeModel.is(equal(SplittingMinimizeModel::ALL)));
1616 _splittingEagerRemoval.setRandomChoices({"on","off"});
1617
1618 _splittingFastRestart = BoolOptionValue("avatar_fast_restart","afr",false);
1619 _splittingFastRestart.description="";
1620 _lookup.insert(&_splittingFastRestart);
1621 _splittingFastRestart.tag(OptionTag::AVATAR);
1622 _splittingFastRestart.reliesOn(_splitting.is(equal(true)));
1623 _splittingFastRestart.setRandomChoices({"on","off"});
1624
1625 _splittingBufferedSolver = BoolOptionValue("avatar_buffered_solver","abs",false);
1626 _splittingBufferedSolver.description="Added buffering funcitonality to the SAT solver used in AVATAR.";
1627 _lookup.insert(&_splittingBufferedSolver);
1628 _splittingBufferedSolver.tag(OptionTag::AVATAR);
1629 _splittingBufferedSolver.reliesOn(_splitting.is(equal(true)));
1630 _splittingBufferedSolver.setRandomChoices({"on","off"});
1631
1632 _splittingDeleteDeactivated = ChoiceOptionValue<SplittingDeleteDeactivated>("avatar_delete_deactivated","add",
1633 SplittingDeleteDeactivated::ON,{"on","large","off"});
1634
1635 _splittingDeleteDeactivated.description="";
1636 _lookup.insert(&_splittingDeleteDeactivated);
1637 _splittingDeleteDeactivated.tag(OptionTag::AVATAR);
1638 _splittingDeleteDeactivated.reliesOn(_splitting.is(equal(true)));
1639 _splittingDeleteDeactivated.setRandomChoices({"on","large","off"});
1640
1641
1642 _splittingFlushPeriod = UnsignedOptionValue("avatar_flush_period","afp",0);
1643 _splittingFlushPeriod.description=
1644 "after given number of generated clauses without deriving an empty clause, the splitting component selection is shuffled. If equal to zero, shuffling is never performed.";
1645 _lookup.insert(&_splittingFlushPeriod);
1646 _splittingFlushPeriod.tag(OptionTag::AVATAR);
1647 _splittingFlushPeriod.reliesOn(_splitting.is(equal(true)));
1648 _splittingFlushPeriod.setRandomChoices({"0","1000","4000","10000","40000","100000"});
1649
1650 _splittingFlushQuotient = FloatOptionValue("avatar_flush_quotient","afq",1.5);
1651 _splittingFlushQuotient.description=
1652 "after each flush, the avatar_flush_period is multiplied by the quotient";
1653 _lookup.insert(&_splittingFlushQuotient);
1654 _splittingFlushQuotient.tag(OptionTag::AVATAR);
1655 _splittingFlushQuotient.addConstraint(greaterThanEq(1.0f));
1656 _splittingFlushQuotient.reliesOn(_splitting.is(equal(true)));
1657 _splittingFlushQuotient.setRandomChoices({"1.0","1.1","1.2","1.4","2.0"});
1658
1659 _splittingNonsplittableComponents = ChoiceOptionValue<SplittingNonsplittableComponents>("avatar_nonsplittable_components","anc",
1660 SplittingNonsplittableComponents::KNOWN,
1661 {"all","all_dependent","known","none"});
1662 _splittingNonsplittableComponents.description=
1663 "Decide what to do with a nonsplittable component:\n"
1664 " -known: SAT clauses will be learnt from non-splittable clauses that have corresponding components (if there is a component C with name SAT l, clause C | {l1,..ln} will give SAT clause ~l1 \\/ … \\/ ~ln \\/ l). When we add the sat clause, we discard the original FO clause C | {l1,..ln} and let the component selection update model, possibly adding the component clause C | {l}.\n"
1665 " -all: like known, except when we see a non-splittable clause that doesn't have a name, we introduce the name for it.\n"
1666 " -all_dependent: like all, but we don't introduce names for non-splittable clauses that don't depend on any components";
1667 _lookup.insert(&_splittingNonsplittableComponents);
1668 _splittingNonsplittableComponents.tag(OptionTag::AVATAR);
1669 _splittingNonsplittableComponents.reliesOn(_splitting.is(equal(true)));
1670 _splittingNonsplittableComponents.setRandomChoices({"all","all_dependent","known","none"});
1671
1672
1673 _nonliteralsInClauseWeight = BoolOptionValue("nonliterals_in_clause_weight","nicw",false);
1674 _nonliteralsInClauseWeight.description=
1675 "Non-literal parts of clauses (such as its split history) will also contribute to the weight";
1676 _lookup.insert(&_nonliteralsInClauseWeight);
1677 _nonliteralsInClauseWeight.tag(OptionTag::AVATAR);
1678 _nonliteralsInClauseWeight.reliesOn(_saturationAlgorithm.is(notEqual(SaturationAlgorithm::INST_GEN)));
1679 _nonliteralsInClauseWeight.reliesOn(_splitting.is(notEqual(false)));
1680 _nonliteralsInClauseWeight.addProblemConstraint(hasNonUnits());
1681 _nonliteralsInClauseWeight.setRandomChoices({"on","off"});
1682
1683 //*********************** SAT solver (used in various places) ***********************
1684
1685 _satClauseActivityDecay = FloatOptionValue("sat_clause_activity_decay","",1.001f);
1686 _satClauseActivityDecay.description="";
1687 _lookup.insert(&_satClauseActivityDecay);
1688 _satClauseActivityDecay.tag(OptionTag::SAT);
1689 _satClauseActivityDecay.addConstraint(greaterThan(1.0f));
1690 _satClauseActivityDecay.setExperimental();
1691
1692 _satClauseDisposer = ChoiceOptionValue<SatClauseDisposer>("sat_clause_disposer","",SatClauseDisposer::MINISAT,
1693 {"growing","minisat"});
1694 _satClauseDisposer.description="";
1695 _lookup.insert(&_satClauseDisposer);
1696 _satClauseDisposer.tag(OptionTag::SAT);
1697 _satClauseDisposer.setExperimental();
1698
1699 _satLearntMinimization = BoolOptionValue("sat_learnt_minimization","",true);
1700 _satLearntMinimization.description="";
1701 _lookup.insert(&_satLearntMinimization);
1702 _satLearntMinimization.tag(OptionTag::SAT);
1703 _satLearntMinimization.setExperimental();
1704
1705 _satLearntSubsumptionResolution = BoolOptionValue("sat_learnt_subsumption_resolution","",true);
1706 _satLearntSubsumptionResolution.description="";
1707 _lookup.insert(&_satLearntSubsumptionResolution);
1708 _satLearntSubsumptionResolution.tag(OptionTag::SAT);
1709 _satLearntSubsumptionResolution.setExperimental();
1710
1711 _satRestartFixedCount = IntOptionValue("sat_restart_fixed_count","",16000);
1712 _satRestartFixedCount.description="";
1713 _lookup.insert(&_satRestartFixedCount);
1714 _satRestartFixedCount.tag(OptionTag::SAT);
1715 _satRestartFixedCount.setExperimental();
1716
1717 _satRestartGeometricIncrease = FloatOptionValue("sat_restart_geometric_increase","",1.1);
1718 _satRestartGeometricIncrease.description="";
1719 _lookup.insert(&_satRestartGeometricIncrease);
1720 _satRestartGeometricIncrease.tag(OptionTag::SAT);
1721 _satRestartGeometricIncrease.addConstraint(greaterThan(1.0f));
1722 _satRestartGeometricIncrease.setExperimental();
1723
1724 _satRestartGeometricInit = IntOptionValue("sat_restart_geometric_init","",32);
1725 _satRestartGeometricInit.description="";
1726 _lookup.insert(&_satRestartGeometricInit);
1727 _satRestartGeometricInit.tag(OptionTag::SAT);
1728 _satRestartGeometricInit.setExperimental();
1729
1730 _satRestartLubyFactor = IntOptionValue("sat_restart_luby_factor","",100);
1731 _satRestartLubyFactor.description="";
1732 _lookup.insert(&_satRestartLubyFactor);
1733 _satRestartLubyFactor.tag(OptionTag::SAT);
1734 _satRestartLubyFactor.setExperimental();
1735
1736 _satRestartMinisatIncrease = FloatOptionValue("sat_restart_minisat_increase","",1.1);
1737 _satRestartMinisatIncrease.description="";
1738 _lookup.insert(&_satRestartMinisatIncrease);
1739 _satRestartMinisatIncrease.tag(OptionTag::SAT);
1740 _satRestartMinisatIncrease.addConstraint(greaterThan(1.0f));
1741 _satRestartMinisatIncrease.setExperimental();
1742
1743 _satRestartMinisatInit = IntOptionValue("sat_restart_minisat_init","",100);
1744 _satRestartMinisatInit.description="";
1745 _lookup.insert(&_satRestartMinisatInit);
1746 _satRestartMinisatInit.tag(OptionTag::SAT);
1747 _satRestartMinisatInit.setExperimental();
1748
1749 _satRestartStrategy = ChoiceOptionValue<SatRestartStrategy>("sat_restart_strategy","",SatRestartStrategy::LUBY,
1750 {"fixed","geometric","luby","minisat"});
1751 _satRestartStrategy.description="";
1752 _lookup.insert(&_satRestartStrategy);
1753 _satRestartStrategy.tag(OptionTag::SAT);
1754 _satRestartStrategy.setExperimental();
1755
1756 _satSolver = ChoiceOptionValue<SatSolver>("sat_solver","sas",SatSolver::MINISAT,
1757 #if VZ3
1758 {"minisat","vampire","z3"});
1759 #else
1760 {"minisat","vampire"});
1761 #endif
1762 _satSolver.description=
1763 "Select the SAT solver to be used throughout the solver. This will be used in AVATAR (for splitting) when the saturation algorithm is discount,lrs or otter and in instance generation for selection and global subsumption.";
1764 _lookup.insert(&_satSolver);
1765 _satSolver.tag(OptionTag::SAT);
1766 _satSolver.setRandomChoices(
1767 #if VZ3
1768 {"minisat","vampire","z3"});
1769 #else
1770 {"minisat","vampire"});
1771 #endif
1772
1773 #if VZ3
1774 _satFallbackForSMT = BoolOptionValue("sat_fallback_for_smt","sffsmt",false);
1775 _satFallbackForSMT.description="If using z3 run a sat solver alongside to use if the smt"
1776 " solver returns unknown at any point";
1777 _lookup.insert(&_satFallbackForSMT);
1778 _satFallbackForSMT.tag(OptionTag::SAT);
1779 _satFallbackForSMT.reliesOn(_satSolver.is(equal(SatSolver::Z3)));
1780
1781 _z3UnsatCores = BoolOptionValue("z3_unsat_core","z3uc",false);
1782 _z3UnsatCores.description="";
1783 _lookup.insert(&_z3UnsatCores);
1784 _z3UnsatCores.tag(OptionTag::SAT);
1785 #endif
1786
1787 _satVarActivityDecay = FloatOptionValue("sat_var_activity_decay","",1.05f);
1788 _satVarActivityDecay.description="";
1789 _lookup.insert(&_satVarActivityDecay);
1790 _satVarActivityDecay.tag(OptionTag::SAT);
1791 _satVarActivityDecay.addConstraint(greaterThan(1.0f));
1792 _satVarActivityDecay.setExperimental();
1793
1794 _satVarSelector = ChoiceOptionValue<SatVarSelector>("sat_var_selector","svs",SatVarSelector::ACTIVE,
1795 {"active","niceness","recently_learnt"});
1796 _satVarSelector.description="";
1797 _lookup.insert(&_satVarSelector);
1798 _satVarSelector.tag(OptionTag::SAT);
1799 _satVarSelector.setExperimental();
1800
1801 //*************************************************************
1802 //*********************** which mode or tag? ************************
1803 //*************************************************************
1804
1805 _bfnt = BoolOptionValue("bfnt","bfnt",false);
1806 _bfnt.description="";
1807 _lookup.insert(&_bfnt);
1808 _bfnt.tag(OptionTag::SATURATION);
1809 // This is checked in checkGlobal
1810 //_bfnt.addConstraint(new OnAnd(new RequiresCompleteForNonHorn<bool>()));
1811 _bfnt.addProblemConstraint(notWithCat(Property::EPR));
1812 _bfnt.setRandomChoices({},{"on","off","off","off","off","off"});
1813 _bfnt.setExperimental();
1814
1815 _increasedNumeralWeight = BoolOptionValue("increased_numeral_weight","inw",false);
1816 _increasedNumeralWeight.description=
1817 "This option only applies if the problem has interpreted numbers. The weight of integer constants depends on the logarithm of their absolute value (instead of being 1)";
1818 _lookup.insert(&_increasedNumeralWeight);
1819 _increasedNumeralWeight.tag(OptionTag::SATURATION);
1820
1821
1822 _interpretedSimplification = BoolOptionValue("interpreted_simplification","",false);
1823 _interpretedSimplification.description=
1824 "Performs simplifications of interpreted functions. This option requires interpreted_evaluation to be enabled as well. IMPORTANT - Currently not supported";
1825 _lookup.insert(&_interpretedSimplification);
1826 _interpretedSimplification.tag(OptionTag::OTHER);
1827 _interpretedSimplification.setExperimental();
1828
1829
1830 _literalComparisonMode = ChoiceOptionValue<LiteralComparisonMode>("literal_comparison_mode","lcm",
1831 LiteralComparisonMode::STANDARD,
1832 {"predicate","reverse","standard"});
1833 _literalComparisonMode.description="Vampire uses term orderings which use an ordering of predicates. Standard places equality (and certain other special predicates) first and all others second. Predicate depends on symbol precedence (see symbol_precedence). Reverse reverses the order.";
1834 _lookup.insert(&_literalComparisonMode);
1835 _literalComparisonMode.tag(OptionTag::SATURATION);
1836 _literalComparisonMode.addProblemConstraint(hasNonUnits());
1837 _literalComparisonMode.addProblemConstraint(hasPredicates());
1838 // TODO: if sat then should not use reverse
1839 _literalComparisonMode.setRandomChoices({"predicate","reverse","standard"});
1840
1841
1842 _maxActive = LongOptionValue("max_active","",0);
1843 _maxActive.description="";
1844 //_lookup.insert(&_maxActive);
1845 _maxActive.tag(OptionTag::OTHER);
1846
1847 _maxAnswers = IntOptionValue("max_answers","",1);
1848 _maxAnswers.description="";
1849 //_lookup.insert(&_maxAnswers);
1850 _maxAnswers.tag(OptionTag::OTHER);
1851
1852 _maxInferenceDepth = IntOptionValue("max_inference_depth","",0);
1853 _maxInferenceDepth.description="";
1854 //_lookup.insert(&_maxInferenceDepth);
1855 _maxInferenceDepth.tag(OptionTag::OTHER);
1856
1857 _maxPassive = LongOptionValue("max_passive","",0);
1858 _maxPassive.description="";
1859 //_lookup.insert(&_maxPassive);
1860 _maxPassive.tag(OptionTag::OTHER);
1861
1862 _nonGoalWeightCoefficient = NonGoalWeightOptionValue("nongoal_weight_coefficient","nwc",1.0);
1863 _nonGoalWeightCoefficient.description=
1864 "coefficient that will multiply the weight of theory clauses (those marked as 'axiom' in TPTP)";
1865 _lookup.insert(&_nonGoalWeightCoefficient);
1866 _nonGoalWeightCoefficient.tag(OptionTag::SATURATION);
1867 _nonGoalWeightCoefficient.setRandomChoices({"1","1.1","1.2","1.3","1.5","1.7","2","2.5","3","4","5","10"});
1868
1869 _restrictNWCtoGC = BoolOptionValue("restrict_nwc_to_goal_constants","rnwc",false);
1870 _restrictNWCtoGC.description = "restrict nongoal_weight_coefficient to those containing goal constants";
1871 _lookup.insert(&_restrictNWCtoGC);
1872 _restrictNWCtoGC.tag(OptionTag::SATURATION);
1873 _restrictNWCtoGC.reliesOn(_nonGoalWeightCoefficient.is(notEqual(1.0f)));
1874
1875
1876 _normalize = BoolOptionValue("normalize","norm",false);
1877 _normalize.description="Normalize the problem so that the ordering of clauses etc does not effect proof search.";
1878 _lookup.insert(&_normalize);
1879 _normalize.tag(OptionTag::PREPROCESSING);
1880
1881 _questionAnswering = ChoiceOptionValue<QuestionAnsweringMode>("question_answering","qa",QuestionAnsweringMode::OFF,
1882 {"answer_literal","from_proof","off"});
1883 _questionAnswering.description="Determines whether (and how) we attempt to answer questions";
1884 _questionAnswering.addHardConstraint(If(notEqual(QuestionAnsweringMode::OFF)).then(_splitting.is(notEqual(true))));
1885 _lookup.insert(&_questionAnswering);
1886 _questionAnswering.tag(OptionTag::OTHER);
1887
1888 _randomSeed = IntOptionValue("random_seed","",Random::seed());
1889 _randomSeed.description="Some parts of vampire use random numbers. This seed allows for reproducability of results. By default the seed is not changed.";
1890 _lookup.insert(&_randomSeed);
1891 _randomSeed.tag(OptionTag::INPUT);
1892
1893 _activationLimit = IntOptionValue("activation_limit","al",0);
1894 _activationLimit.description="Terminate saturation after this many iterations of the main loop. 0 means no limit.";
1895 _lookup.insert(&_activationLimit);
1896 _activationLimit.tag(OptionTag::SATURATION);
1897
1898 _termOrdering = ChoiceOptionValue<TermOrdering>("term_ordering","to", TermOrdering::KBO,
1899 {"kbo","lpo"});
1900 _termOrdering.description="The term ordering used by Vampire to orient equations and order literals";
1901 _termOrdering.tag(OptionTag::SATURATION);
1902 _lookup.insert(&_termOrdering);
1903
1904 _symbolPrecedence = ChoiceOptionValue<SymbolPrecedence>("symbol_precedence","sp",SymbolPrecedence::ARITY,
1905 {"arity","occurrence","reverse_arity","scramble",
1906 "frequency","reverse_frequency",
1907 "weighted_frequency","reverse_weighted_frequency"});
1908 _symbolPrecedence.description="Vampire uses term orderings which require a precedence relation between symbols. Arity orders symbols by their arity (and reverse_arity takes the reverse of this) and occurence orders symbols by the order they appear in the problem.";
1909 _lookup.insert(&_symbolPrecedence);
1910 _symbolPrecedence.tag(OptionTag::SATURATION);
1911 _symbolPrecedence.setRandomChoices({"arity","occurence","reverse_arity","frequency"});
1912
1913 _introducedSymbolPrecedence = ChoiceOptionValue<IntroducedSymbolPrecedence>("introduced_symbol_precedence","isp",
1914 IntroducedSymbolPrecedence::TOP,
1915 {"top","bottom"});
1916 _introducedSymbolPrecedence.description="Decides where to place symbols introduced during proof search in the symbol precedence";
1917 _lookup.insert(&_introducedSymbolPrecedence);
1918 _introducedSymbolPrecedence.tag(OptionTag::SATURATION);
1919
1920 _functionPrecedence = StringOptionValue("function_precendence","fp","");
1921 _functionPrecedence.description = "A name of a file with an explicit user specified precedence on function symbols.";
1922 _functionPrecedence.setExperimental();
1923 _lookup.insert(&_functionPrecedence);
1924
1925 _predicatePrecedence = StringOptionValue("predicate_precendence","pp","");
1926 _predicatePrecedence.description = "A name of a file with an explicit user specified precedence on predicate symbols.";
1927 _predicatePrecedence.setExperimental();
1928 _lookup.insert(&_predicatePrecedence);
1929
1930 _symbolPrecedenceBoost = ChoiceOptionValue<SymbolPrecedenceBoost>("symbol_precedence_boost","spb",SymbolPrecedenceBoost::NONE,
1931 {"none","goal","units","goal_then_units"});
1932 _symbolPrecedenceBoost.description = "Boost the symbol precedence of symbols occuring in certain kinds of clauses in the input.";
1933 _symbolPrecedenceBoost.tag(OptionTag::SATURATION);
1934 _lookup.insert(&_symbolPrecedenceBoost);
1935
1936 _weightIncrement = BoolOptionValue("weight_increment","",false);
1937 _weightIncrement.description="";
1938 //_lookup.insert(&_weightIncrement);
1939 _weightIncrement.tag(OptionTag::OTHER);
1940
1941
1942 //******************************************************************
1943 //*********************** Vinter??? *******************************
1944 //******************************************************************
1945
1946
1947 _colorUnblocking = BoolOptionValue("color_unblocking","",false);
1948 _colorUnblocking.description="";
1949 _lookup.insert(&_colorUnblocking);
1950 _colorUnblocking.setExperimental();
1951 _colorUnblocking.tag(OptionTag::OTHER);
1952
1953
1954 _showInterpolant = ChoiceOptionValue<InterpolantMode>("show_interpolant","",InterpolantMode::OFF,
1955 {"new_heur","new_opt","off", "old", "old_opt"});
1956 _lookup.insert(&_showInterpolant);
1957 _showInterpolant.tag(OptionTag::OTHER);
1958 _showInterpolant.setExperimental();
1959
1960 //******************************************************************
1961 //*********************** Bound Propagation ***********************
1962 //******************************************************************
1963
1964 /*
1965 _whileNumber = IntOptionValue("while_number","",1);
1966 _whileNumber.description="";
1967 _lookup.insert(&_whileNumber);
1968 _whileNumber.tag(Mode::BOUND_PROP);
1969
1970 _functionNumber = IntOptionValue("function_number","",1);
1971 _functionNumber.description="";
1972 _lookup.insert(&_functionNumber);
1973 _functionNumber.tag(Mode::BOUND_PROP);
1974 _functionNumber.tag(OptionTag::PREPROCESSING);
1975
1976 _bpCollapsingPropagation = BoolOptionValue("bp_add_collapsing_inequalities","",false); // ASSUMED default, wasn't in Options
1977 _bpCollapsingPropagation.description="";
1978 _lookup.insert(&_bpCollapsingPropagation);
1979 _bpCollapsingPropagation.tag(Mode::BOUND_PROP);
1980 _bpCollapsingPropagation.reliesOn(_mode.is(equal(Mode::BOUND_PROP)));
1981
1982 _bpAllowedFMBalance = UnsignedOptionValue("bp_allowed_fm_balance","",0);
1983 _bpAllowedFMBalance.description="";
1984 _lookup.insert(&_bpAllowedFMBalance);
1985 _bpAllowedFMBalance.tag(Mode::BOUND_PROP);
1986 _bpAllowedFMBalance.reliesOn(_mode.is(equal(Mode::BOUND_PROP)));
1987
1988 _bpAlmostHalfBoundingRemoval= ChoiceOptionValue<BPAlmostHalfBoundingRemoval>("bp_almost_half_bounding_removal","",
1989 BPAlmostHalfBoundingRemoval::ON,{"bounds_on","off","on"});
1990 _bpAlmostHalfBoundingRemoval.description="";
1991 _lookup.insert(&_bpAlmostHalfBoundingRemoval);
1992 _bpAlmostHalfBoundingRemoval.tag(Mode::BOUND_PROP);
1993 _bpAlmostHalfBoundingRemoval.reliesOn(_mode.is(equal(Mode::BOUND_PROP)));
1994
1995 _bpAssignmentSelector = ChoiceOptionValue<BPAssignmentSelector>("bp_assignment_selector","",
1996 BPAssignmentSelector::RANDOM,
1997 {"alternating","bmp","lower_bound",
1998 "middle","random","rational","smallest",
1999 "tight","tightish","upper_bound"});
2000 _bpAssignmentSelector.description="";
2001 _lookup.insert(&_bpAssignmentSelector);
2002 _bpAssignmentSelector.tag(Mode::BOUND_PROP);
2003 _bpAssignmentSelector.reliesOn(_mode.is(equal(Mode::BOUND_PROP)));
2004
2005 _updatesByOneConstraint= UnsignedOptionValue("bp_bound_improvement_limit","",3);
2006 _updatesByOneConstraint.description="";
2007 _lookup.insert(&_updatesByOneConstraint);
2008 _updatesByOneConstraint.tag(Mode::BOUND_PROP);
2009 _updatesByOneConstraint.reliesOn(_mode.is(equal(Mode::BOUND_PROP)));
2010
2011 _bpConflictSelector = ChoiceOptionValue<BPConflictSelector>("bp_conflict_selector","",
2012 BPConflictSelector::MOST_RECENT,{"least_recent","most_recent","shortest"});
2013 _bpConflictSelector.description="";
2014 _lookup.insert(&_bpConflictSelector);
2015 _bpConflictSelector.tag(Mode::BOUND_PROP);
2016 _bpConflictSelector.reliesOn(_mode.is(equal(Mode::BOUND_PROP)));
2017
2018 _bpConservativeAssignmentSelection = BoolOptionValue("bp_conservative_assignment_selection","",true);
2019 _bpConservativeAssignmentSelection.description="";
2020 _lookup.insert(&_bpConservativeAssignmentSelection);
2021 _bpConservativeAssignmentSelection.tag(Mode::BOUND_PROP);
2022 _bpConservativeAssignmentSelection.reliesOn(_mode.is(equal(Mode::BOUND_PROP)));
2023
2024 _bpFmElimination= BoolOptionValue("bp_fm_elimination","",true);
2025 _bpFmElimination.description="";
2026 _lookup.insert(&_bpFmElimination);
2027 _bpFmElimination.tag(Mode::BOUND_PROP);
2028 _bpFmElimination.reliesOn(_mode.is(equal(Mode::BOUND_PROP)));
2029
2030 _maximalPropagatedEqualityLength = UnsignedOptionValue("bp_max_prop_length","",5);
2031 _maximalPropagatedEqualityLength.description="";
2032 _lookup.insert(&_maximalPropagatedEqualityLength);
2033 _maximalPropagatedEqualityLength.tag(Mode::BOUND_PROP);
2034 _maximalPropagatedEqualityLength.reliesOn(_mode.is(equal(Mode::BOUND_PROP)));
2035
2036 _bpPropagateAfterConflict = BoolOptionValue("bp_propagate_after_conflict","",true);
2037 _bpPropagateAfterConflict.description="";
2038 _lookup.insert(&_bpPropagateAfterConflict);
2039 _bpPropagateAfterConflict.tag(Mode::BOUND_PROP);
2040 _bpPropagateAfterConflict.reliesOn(_mode.is(equal(Mode::BOUND_PROP)));
2041
2042 _bpStartWithPrecise = BoolOptionValue("bp_start_with_precise","",false);
2043 _bpStartWithPrecise.description="";
2044 _lookup.insert(&_bpStartWithPrecise);
2045 _bpStartWithPrecise.tag(Mode::BOUND_PROP);
2046 _bpStartWithPrecise.reliesOn(_mode.is(equal(Mode::BOUND_PROP)));
2047
2048 _bpStartWithRational = BoolOptionValue("bp_start_with_rational","",false);
2049 _bpStartWithRational.description="";
2050 _lookup.insert(&_bpStartWithRational);
2051 _bpStartWithRational.tag(Mode::BOUND_PROP);
2052 _bpStartWithRational.reliesOn(_mode.is(equal(Mode::BOUND_PROP)));
2053
2054 _bpVariableSelector = ChoiceOptionValue<BPVariableSelector>("bp_variable_selector","",
2055 BPVariableSelector::TIGHTEST_BOUND,
2056 {"conflicting","conflicting_and_collapsing",
2057 "first","look_ahead","random","recent_collapsing",
2058 "recent_conflicting","tightest_bound"});
2059 _bpVariableSelector.description="";
2060 _lookup.insert(&_bpVariableSelector);
2061 _bpVariableSelector.tag(Mode::BOUND_PROP);
2062 _bpVariableSelector.reliesOn(_mode.is(equal(Mode::BOUND_PROP)));
2063 */
2064
2065
2066 // Declare tag names
2067
2068 _tagNames = {
2069 "Unused",
2070 "Other",
2071 "Development",
2072 "Output",
2073 "Instance Generation",
2074 "SAT Solving",
2075 "Finite Model Building",
2076 "AVATAR",
2077 "Inferences",
2078 "LRS Specific",
2079 "Saturation",
2080 "Preprocessing",
2081 "Input",
2082 "Help",
2083 "Global"
2084 };
2085
2086 } // Options::init
2087
copyValuesFrom(const Options & that)2088 void Options::copyValuesFrom(const Options& that)
2089 {
2090 //copy across the actual values in that
2091 VirtualIterator<AbstractOptionValue*> options = _lookup.values();
2092
2093 while(options.hasNext()){
2094 AbstractOptionValue* opt = options.next();
2095 if(opt->shouldCopy()){
2096 AbstractOptionValue* other = that.getOptionValueByName(opt->longName);
2097 ASS(opt!=other);
2098 bool status = opt -> set(other->getStringOfActual());
2099 ASS(status);
2100 }
2101 }
2102 }
Options(const Options & that)2103 Options::Options(const Options& that)
2104 {
2105 init();
2106 copyValuesFrom(that);
2107 }
2108
operator =(const Options & that)2109 Options& Options::operator=(const Options& that)
2110 {
2111 if(this==&that) return *this;
2112 copyValuesFrom(that);
2113 return *this;
2114 }
2115
2116
2117 /**
2118 * Set option by its name and value.
2119 * @since 13/11/2004 Manchester
2120 * @since 18/01/2014 Manchester, changed to use _ignoreMissing
2121 * @since 14/09/2014 updated to use _lookup
2122 * @author Andrei Voronkov
2123 */
set(const char * name,const char * value,bool longOpt)2124 void Options::set(const char* name,const char* value, bool longOpt)
2125 {
2126 CALL ("Options::set/3");
2127
2128 try {
2129 if((longOpt && !_lookup.findLong(name)->set(value)) ||
2130 (!longOpt && !_lookup.findShort(name)->set(value))) {
2131 switch (ignoreMissing()) {
2132 case IgnoreMissing::OFF:
2133 USER_ERROR((vstring) value +" is an invalid value for "+(vstring)name+"\nSee help or use explain i.e. vampire -explain mode");
2134 break;
2135 case IgnoreMissing::WARN:
2136 if (outputAllowed()) {
2137 env.beginOutput();
2138 addCommentSignForSZS(env.out());
2139 env.out() << "WARNING: invalid value "<< value << " for option " << name << endl;
2140 env.endOutput();
2141 }
2142 break;
2143 case IgnoreMissing::ON:
2144 break;
2145 }
2146 }
2147 }
2148 catch (const ValueNotFoundException&) {
2149 if (_ignoreMissing.actualValue != IgnoreMissing::ON) {
2150 vstring msg = (vstring)name + (longOpt ? " is not a valid option" : " is not a valid short option (did you mean --?)");
2151 if (_ignoreMissing.actualValue == IgnoreMissing::WARN) {
2152 if (outputAllowed()) {
2153 env.beginOutput();
2154 addCommentSignForSZS(env.out());
2155 env.out() << "WARNING: " << msg << endl;
2156 env.endOutput();
2157 }
2158 return;
2159 } // else:
2160 Stack<vstring> sim = getSimilarOptionNames(name,false);
2161 Stack<vstring>::Iterator sit(sim);
2162 if(sit.hasNext()){
2163 vstring first = sit.next();
2164 msg += "\n\tMaybe you meant ";
2165 if(sit.hasNext()) msg += "one of:\n\t\t";
2166 msg += first;
2167 while(sit.hasNext()){ msg+="\n\t\t"+sit.next();}
2168 msg+="\n\tYou can use -explain <option> to explain an option";
2169 }
2170 USER_ERROR(msg);
2171 }
2172 }
2173 } // Options::set/2
2174
2175 /**
2176 * Set option by its name and value.
2177 * @since 06/04/2005 Torrevieja
2178 */
set(const vstring & name,const vstring & value)2179 void Options::set(const vstring& name,const vstring& value)
2180 {
2181 CALL ("Options::set/2");
2182 set(name.c_str(),value.c_str(),true);
2183 } // Options::set/2
2184
check(Property * p)2185 bool Options::OptionHasValue::check(Property*p){
2186 CALL("Options::OptionHasValue::check");
2187 AbstractOptionValue* opt = env.options->getOptionValueByName(option_value);
2188 ASS(opt);
2189 return opt->getStringOfActual()==value;
2190 }
2191
2192 /**
2193 * Static functions to help specify random choice values
2194 */
2195
isRandOn()2196 Options::OptionProblemConstraintUP Options::isRandOn(){
2197 return OptionProblemConstraintUP(new OptionHasValue("random_strategy","on"));
2198 }
isRandSat()2199 Options::OptionProblemConstraintUP Options::isRandSat(){
2200 return OptionProblemConstraintUP(new OptionHasValue("random_strategy","sat"));
2201 }
saNotInstGen()2202 Options::OptionProblemConstraintUP Options::saNotInstGen(){
2203 return OptionProblemConstraintUP(new OptionHasValue("sa","inst_gen"));
2204 }
isBfnt()2205 Options::OptionProblemConstraintUP Options::isBfnt(){
2206 return OptionProblemConstraintUP(new OptionHasValue("bfnt","on"));
2207 }
2208
2209 /**
2210 * Return the include file name using its relative name.
2211 *
2212 * @param relativeName the relative name, must begin and end with "'"
2213 * because of the TPTP syntax
2214 * @since 16/10/2003 Manchester, relativeName changed to string from char*
2215 * @since 07/08/2014 Manchester, relativeName changed to vstring
2216 */
includeFileName(const vstring & relativeName)2217 vstring Options::includeFileName (const vstring& relativeName)
2218 {
2219 CALL("Options::includeFileName");
2220
2221 if (relativeName[0] == '/') { // absolute name
2222 return relativeName;
2223 }
2224
2225 if (System::fileExists(relativeName)) {
2226 return relativeName;
2227 }
2228
2229 // truncatedRelativeName is relative.
2230 // Use the conventions of Vampire:
2231 // (a) first search the value of "include"
2232 vstring dir = include();
2233
2234 if (dir == "") { // include undefined
2235 // (b) search in the directory of the 'current file'
2236 // i.e. the input file
2237 vstring currentFile = inputFile();
2238 System::extractDirNameFromPath(currentFile,dir);
2239 if(System::fileExists(dir+"/"+relativeName)){
2240 return dir + "/" + relativeName;
2241 }
2242
2243 // (c) search the value of the environment variable TPTP_DIR
2244 char* env = getenv("TPTP");
2245 if (env) {
2246 dir = env;
2247 }
2248 else {
2249 // (d) use the current directory
2250 dir = ".";
2251 }
2252 // we do not check (c) or (d) - an error will occur later
2253 // if the file does not exist here
2254 }
2255 // now dir is the directory to search
2256 return dir + "/" + relativeName;
2257 } // Options::includeFileName
2258
2259
2260 /**
2261 * Output options to a stream.
2262 *
2263 * @param str the stream
2264 * @since 02/01/2003 Manchester
2265 * @since 28/06/2003 Manchester, changed to treat XML output as well
2266 * @since 10/07/2003 Manchester, "normalize" added.
2267 * @since 27/11/2003 Manchester, changed using new XML routines and iterator
2268 * of options
2269 */
output(ostream & str) const2270 void Options::output (ostream& str) const
2271 {
2272 CALL("Options::output");
2273
2274 if(printAllTheoryAxioms()){
2275 cout << "Sorry, not implemented yet!" << endl;
2276
2277 return;
2278 }
2279
2280 if(!explainOption().empty()){
2281
2282 //We bypass the allocator here because of the use of vstringstream
2283 BYPASSING_ALLOCATOR;
2284
2285 AbstractOptionValue* option;
2286 vstring name = explainOption();
2287 try{
2288 option = _lookup.findLong(name);
2289 }
2290 catch(const ValueNotFoundException&){
2291 try{
2292 option = _lookup.findShort(name);
2293 }
2294 catch(const ValueNotFoundException&){
2295 option = 0;
2296 }
2297 }
2298 if(!option){
2299 str << name << " not a known option" << endl;
2300 Stack<vstring> sim_s = getSimilarOptionNames(name,true);
2301 Stack<vstring> sim_l = getSimilarOptionNames(name,false);
2302 VirtualIterator<vstring> sit = pvi(getConcatenatedIterator(
2303 Stack<vstring>::Iterator(sim_s),Stack<vstring>::Iterator(sim_l)));
2304 if(sit.hasNext()){
2305 vstring first = sit.next();
2306 str << "\tMaybe you meant ";
2307 if(sit.hasNext()) str << "one of:\n\t\t";
2308 str << first;
2309 while(sit.hasNext()){ str << "\n\t\t"+sit.next();}
2310 str << endl;
2311 }
2312 }
2313 else{
2314 vstringstream vs;
2315 option->output(vs,lineWrapInShowOptions());
2316 str << vs.str();
2317 }
2318
2319 }
2320
2321 if (showHelp()){
2322 str << "=========== Usage ==========\n";
2323 str << "Call vampire using\n";
2324 str << " vampire [options] [problem]\n";
2325 str << "For example,\n";
2326 str << " vampire --mode casc --include ~/TPTP ~/TPTP/Problems/ALG/ALG150+1.p\n";
2327
2328 str << "=========== Hints ==========\n";
2329
2330
2331 str << "=========== Options ==========\n";
2332 str << "To see a list of all options use\n --show_options on\n";
2333 str << "Options will only be displayed for the current mode (Vampire by default)\n";
2334 str << " use --mode to change mode\n";
2335 //str << "By default experimental options will not be shown. To show ";
2336 //str << "these options use\n --show_experimental_options on\n";
2337 str << "=========== End ==========\n";
2338 }
2339
2340 bool normalshow = showOptions();
2341 bool experimental = showExperimentalOptions();
2342
2343 if(normalshow || experimental) {
2344
2345 //We bypass the allocator here because of the use of vstringstream
2346 BYPASSING_ALLOCATOR;
2347
2348 Mode this_mode = _mode.actualValue;
2349 //str << "=========== Options ==========\n";
2350
2351 VirtualIterator<AbstractOptionValue*> options = _lookup.values();
2352
2353 //Stack<vstringstream*> groups;
2354 int num_tags = static_cast<int>(OptionTag::LAST_TAG);
2355 Stack<Stack<AbstractOptionValue*>> groups;
2356 for(int i=0; i<=num_tags;i++){
2357 // groups.push(new vstringstream);
2358 Stack<AbstractOptionValue*> stack;
2359 groups.push(stack);
2360 }
2361
2362
2363 while(options.hasNext()){
2364 AbstractOptionValue* option = options.next();
2365 if(option->inMode(this_mode) &&
2366 ((experimental && option->experimental) ||
2367 (normalshow && !option->experimental) )){
2368 unsigned tag = static_cast<unsigned>(option->getTag());
2369 //option->output(*groups[tag]);
2370 (groups[tag]).push(option);
2371 }
2372 }
2373
2374 //output them in reverse order
2375 for(int i=num_tags;i>=0;i--){
2376 if(groups[i].isEmpty()) continue;
2377 vstring label = " "+_tagNames[i]+" ";
2378 ASS(label.length() < 40);
2379 vstring br = "******************************";
2380 vstring br_gap = br.substr(0,(br.length()-(label.length()/2)));
2381 str << endl << br << br << endl;
2382 str << br_gap << label << br_gap << endl;
2383 str << br << br << endl << endl;
2384
2385 // Sort
2386 Stack<AbstractOptionValue*> os = groups[i];
2387 DArray<AbstractOptionValue*> osa;
2388 osa.initFromIterator(Stack<AbstractOptionValue*>::Iterator(os));
2389 osa.sort(AbstractOptionValueCompatator());
2390 DArray<AbstractOptionValue*>::Iterator oit(osa);
2391 while(oit.hasNext()){
2392 oit.next()->output(str,lineWrapInShowOptions());
2393 }
2394 //str << (*groups[i]).str();
2395 //BYPASSING_ALLOCATOR;
2396 //delete groups[i];
2397 }
2398
2399 //str << "======= End of options =======\n";
2400 }
2401
2402 } // Options::output (ostream& str) const
2403
2404
2405 // * Convert options to an XML element.
2406 // *
2407 // * @since 15/11/2004 Manchester
2408 // */
2409 // XMLElement Options::toXML () const
2410 // {
2411 // CALL("Options::toXML");
2412
2413 // XMLElement options("options");
2414 // for (int i = 0;i < Constants::optionNames.length;i++) {
2415 // ostringstream str;
2416 // outputValue(str,i);
2417 // XMLElement OptionValue("option",true);
2418 // options.addChild(option);
2419 // option.addAttribute("name",Constants::optionNames[i]);
2420 // option.addAttribute("value",str.str());
2421 // }
2422 // return options;
2423 // } // Options::toXML
2424
2425 template<typename T>
randomize(Property * prop)2426 bool Options::OptionValue<T>::randomize(Property* prop){
2427 CALL("Options::OptionValue::randomize()");
2428
2429 DArray<vstring>* choices = nullptr;
2430 if(env.options->randomStrategy()==RandomStrategy::NOCHECK) prop=0;
2431
2432 // Only randomize if we have a property and need it or don't have one and don't need it!
2433 if( env.options->randomStrategy()!=RandomStrategy::NOCHECK &&
2434 ((prop && !hasProblemConstraints()) || (!prop && hasProblemConstraints()))
2435 ){
2436 return false;
2437 }
2438 // Note that if we suppressed the problem constraints
2439 // the checks will be skipped
2440
2441 //Search for the first set of random choices that is valid
2442 Stack<RandEntry>::BottomFirstIterator entry_it(rand_choices);
2443 while(entry_it.hasNext()){
2444 auto& entry = entry_it.next();
2445 if(!entry.first || (prop && entry.first->check(prop))){
2446 choices = entry.second.get();
2447 break;
2448 }
2449 }
2450 if(!choices || choices->size()==0) return false; // no valid choices
2451
2452 //Pick a random option from the available choices
2453 int index = Random::getInteger(choices->size());
2454 set((*choices)[index]);
2455 return true;
2456 }
2457
2458 //TODO should not use cout, should use env.out
2459 template<typename T>
checkConstraints()2460 bool Options::OptionValue<T>::checkConstraints(){
2461 CALL("Options::OptionValue::checkConstraints");
2462 typename Lib::Stack<OptionValueConstraintUP<T>>::Iterator it(_constraints);
2463 while(it.hasNext()){
2464 const OptionValueConstraintUP<T>& con = it.next();
2465 if(!con->check(*this)){
2466
2467 if(env.options->mode()==Mode::SPIDER){
2468 reportSpiderFail();
2469 USER_ERROR("\nBroken Constraint: "+con->msg(*this));
2470 }
2471
2472 if(con->isHard()){
2473 if(env.options->randomStrategy()!=RandomStrategy::OFF)
2474 return false; // Skip warning for Hard
2475 USER_ERROR("\nBroken Constraint: "+con->msg(*this));
2476 }
2477 switch(env.options->getBadOptionChoice()){
2478 case BadOption::HARD :
2479 USER_ERROR("\nBroken Constraint: "+con->msg(*this));
2480 case BadOption::SOFT :
2481 cout << "WARNING Broken Constraint: "+con->msg(*this) << endl;
2482 return false;
2483 case BadOption::FORCED :
2484 if(con->force(this)){
2485 cout << "Forced constraint " + con->msg(*this) << endl;
2486 break;
2487 }else{
2488 USER_ERROR("\nCould not force Constraint: "+con->msg(*this));
2489 }
2490 case BadOption::OFF:
2491 return false;
2492 default: ASSERTION_VIOLATION;
2493 }
2494 }
2495 }
2496 return true;
2497 }
2498
2499 template<typename T>
checkProblemConstraints(Property * prop)2500 bool Options::OptionValue<T>::checkProblemConstraints(Property* prop){
2501 CALL("Options::OptionValue::checkProblemConstraints");
2502
2503 Lib::Stack<OptionProblemConstraintUP>::Iterator it(_prob_constraints);
2504 while(it.hasNext()){
2505 OptionProblemConstraintUP& con = it.next();
2506 // Constraint should hold whenever the option is set
2507 if(is_set && !con->check(prop)){
2508
2509 if(env.options->mode()==Mode::SPIDER){
2510 reportSpiderFail();
2511 USER_ERROR("WARNING: " + longName + con->msg());
2512 }
2513
2514 switch(env.options->getBadOptionChoice()){
2515 case BadOption::OFF: break;
2516 default:
2517 cout << "WARNING: " << longName << con->msg() << endl;
2518 }
2519 return false;
2520 }
2521 }
2522 return true;
2523 }
2524
2525 template<typename T>
is(OptionValueConstraintUP<T> c)2526 Options::AbstractWrappedConstraintUP Options::OptionValue<T>::is(OptionValueConstraintUP<T> c)
2527 {
2528 return AbstractWrappedConstraintUP(new WrappedConstraint<T>(*this,std::move(c)));
2529 }
2530
2531 /**
2532 * Read age-weight ratio from a string. The string can be an integer
2533 * or an expression "a:w", where a,w are integers.
2534 *
2535 * @since 25/05/2004 Manchester
2536 */
readRatio(const char * val,char separator)2537 bool Options::RatioOptionValue::readRatio(const char* val, char separator)
2538 {
2539 CALL("RatioOptionValue::readRatio");
2540
2541 // search the string for ":"
2542 bool found = false;
2543 int colonIndex = 0;
2544 while (val[colonIndex]) {
2545 if (val[colonIndex] == separator) {
2546 found = true;
2547 break;
2548 }
2549 colonIndex++;
2550 }
2551
2552 if (found) {
2553 if (strlen(val) > 127) {
2554 return false;
2555 }
2556 char copy[128];
2557 strcpy(copy,val);
2558 copy[colonIndex] = 0;
2559 int age;
2560 if (! Int::stringToInt(copy,age)) {
2561 return false;
2562 }
2563 actualValue = age;
2564 int weight;
2565 if (! Int::stringToInt(copy+colonIndex+1,weight)) {
2566 return false;
2567 }
2568 otherValue = weight;
2569
2570 // don't allow ratios 0:0
2571 if (actualValue == 0 && otherValue == 0) {
2572 return false;
2573 }
2574
2575 return true;
2576 }
2577 actualValue = 1;
2578 int weight;
2579 if (! Int::stringToInt(val,weight)) {
2580 return false;
2581 }
2582 otherValue = weight;
2583 return true;
2584 }
2585
setValue(const vstring & value)2586 bool Options::NonGoalWeightOptionValue::setValue(const vstring& value)
2587 {
2588 CALL("NonGoalWeightOptionValue::setValue");
2589
2590 float newValue;
2591 if(!Int::stringToFloat(value.c_str(),newValue)) return false;
2592
2593 if(newValue <= 0.0) return false;
2594
2595 actualValue=newValue;
2596
2597 // actualValue contains numerator
2598 numerator=static_cast<int>(newValue*100);
2599 // otherValue contains denominator
2600 denominator=100;
2601
2602 return true;
2603
2604
2605 }
2606
setValue(const vstring & value)2607 bool Options::SelectionOptionValue::setValue(const vstring& value)
2608 {
2609 CALL("SelectionOptionValue::setValue");
2610
2611 int sel;
2612 if(!Int::stringToInt(value,sel)) return false;
2613 switch (sel) {
2614 case 0:
2615 case 1:
2616 case 2:
2617 case 3:
2618 case 4:
2619 case 10:
2620 case 11:
2621 case 20:
2622 case 21:
2623 case 22:
2624
2625 case 30:
2626 case 31:
2627 case 32:
2628 case 33:
2629 case 34:
2630 case 35:
2631
2632 case 1002:
2633 case 1003:
2634 case 1004:
2635 case 1010:
2636 case 1011:
2637 case -1:
2638 case -2:
2639 case -3:
2640 case -4:
2641 case -10:
2642 case -11:
2643 case -20: // almost same as 20 (but factoring will be on negative and not positive literals)
2644 case -21:
2645 case -22:
2646 case -30: // almost same as 30 (but factoring will be on negative and not positive literals)
2647 case -31:
2648 case -32:
2649 case -33:
2650 case -34:
2651 case -35:
2652
2653 case -1002:
2654 case -1003:
2655 case -1004:
2656 case -1010:
2657 case -1011: // almost same as 1011 (but factoring will be on negative and not positive literals)
2658 actualValue = sel;
2659 return true;
2660 default:
2661 return false;
2662 }
2663 }
2664
setValue(const vstring & value)2665 bool Options::InputFileOptionValue::setValue(const vstring& value)
2666 {
2667 CALL("InputFileOptionValue::setValue");
2668
2669 actualValue=value;
2670 if(value.empty()) return true;
2671
2672 //update the problem name
2673
2674 int length = value.length();
2675 const char* name = value.c_str();
2676
2677 int b = length - 1;
2678 while (b >= 0 && name[b] != '/') {
2679 b--;
2680 }
2681 b++;
2682
2683 int e = length - 1;
2684 while (e >= b && name[e] != '.') {
2685 e--;
2686 }
2687 if (e < b) {
2688 e = length;
2689 }
2690
2691 parent->_problemName.actualValue=value.substr(b,e-b);
2692
2693 return true;
2694
2695 }
2696
2697
setValue(const vstring & value)2698 bool Options::TimeLimitOptionValue::setValue(const vstring& value)
2699 {
2700 CALL("Options::readTimeLimit");
2701
2702 int length = value.size();
2703 if (length == 0 || length > 127) {
2704 USER_ERROR((vstring)"wrong value for time limit: " + value);
2705 }
2706
2707 char copy[128];
2708 strcpy(copy,value.c_str());
2709 char* end = copy;
2710 // search for the end of the string for
2711 while (*end) {
2712 end++;
2713 }
2714 end--;
2715 float multiplier = 10.0; // by default assume seconds
2716 switch (*end) {
2717 case 'd': // deciseconds
2718 multiplier = 1.0;
2719 *end = 0;
2720 break;
2721 case 's': // seconds
2722 multiplier = 10.0;
2723 *end = 0;
2724 break;
2725 case 'm': // minutes
2726 multiplier = 600.0;
2727 *end = 0;
2728 break;
2729 case 'h': // minutes
2730 multiplier = 36000.0;
2731 *end = 0;
2732 break;
2733 case 'D': // days
2734 multiplier = 864000.0;
2735 *end = 0;
2736 break;
2737 default:
2738 break;
2739 }
2740
2741 float number;
2742 if (! Int::stringToFloat(copy,number)) {
2743 USER_ERROR((vstring)"wrong value for time limit: " + value);
2744 }
2745
2746 #ifdef _MSC_VER
2747 // Visual C++ does not know the round function
2748 actualValue= (int)floor(number * multiplier);
2749 #else
2750 actualValue= (int)round(number * multiplier);
2751 #endif
2752
2753 return true;
2754 } // Options::readTimeLimit(const char* val)
2755
randomizeStrategy(Property * prop)2756 void Options::randomizeStrategy(Property* prop)
2757 {
2758 CALL("Options::randomizeStrategy");
2759 if(_randomStrategy.actualValue==RandomStrategy::OFF) return;
2760
2761 TimeCounter tc(TC_RAND_OPT);
2762
2763 // The pseudo random sequence is deterministic given a seed.
2764 // By default the seed is 1
2765 // For this randomisation we get save the seed and try and randomize it
2766 int saved_seed = Random::seed();
2767 Random::setSeed(time(NULL)); // TODO is this the best choice of seed?
2768
2769 // We randomize options that have setRandomChoices
2770 // TODO: randomize order in which options are selected
2771 // (not order of insertion but probably deterministic)
2772
2773 // We define some options that should be set before the rest
2774 // Note this is a stack!
2775 Stack<AbstractOptionValue*> do_first;
2776 do_first.push(&_saturationAlgorithm);
2777 do_first.push(&_bfnt);
2778
2779 auto options = getConcatenatedIterator(Stack<AbstractOptionValue*>::Iterator(do_first),_lookup.values());
2780
2781 // whilst doing this don't report any bad options
2782 BadOption saved_bad_option = _badOption.actualValue;
2783 _badOption.actualValue=BadOption::OFF;
2784
2785 bool skipChecks = _randomStrategy.actualValue == RandomStrategy::NOCHECK;
2786
2787 while(options.hasNext()){
2788 AbstractOptionValue* option = options.next();
2789 if(!option->is_set){
2790 // try 5 random values before giving up
2791 vstring def = option->getStringOfActual();
2792
2793 // This is where we check the NoProperty condition if prop=0
2794 bool can_rand = option->randomize(prop);
2795 // If we cannot randomize then skip (invariant, if this is false value is unchanged)
2796 if(can_rand){
2797 // We need to check ALL constraints - rather inefficient
2798 bool valid = skipChecks || (checkGlobalOptionConstraints(true) && (!prop || checkProblemOptionConstraints(prop,true)));
2799 unsigned i=4;
2800 while(!valid && i-- > 0){
2801 option->randomize(prop);
2802 valid = checkGlobalOptionConstraints(true) && (!prop || checkProblemOptionConstraints(prop,true));
2803 }
2804 if(!valid){
2805 //cout << "Failed for " << option->longName << endl;
2806 option->set(def);
2807 option->is_set=false;
2808 }
2809 //else cout << "Randomized " << option->longName << endl;
2810 }// else cout << "cannot randomize " << option->longName << endl;
2811 }
2812 }
2813
2814 // Reset saved things
2815 _badOption.actualValue = saved_bad_option;
2816 Random::setSeed(saved_seed);
2817
2818 //When we reach this place all constraints should be holding
2819 //However, there is one we haven't checked yet: bfnt completeness
2820 //If this fails we restart this with bfnt set to off... only if it was on before
2821 if(!checkGlobalOptionConstraints() && _bfnt.actualValue){
2822 _bfnt.set("off");
2823 randomizeStrategy(prop);
2824 }
2825 else{
2826 if(prop) cout << "Random strategy: " + generateEncodedOptions() << endl;
2827 }
2828 }
2829
2830 /**
2831 * Assign option values as encoded in the option vstring if assign=true, otherwise check that
2832 * the option values are not currently set to those values.
2833 * according to the argument in the format
2834 * opt1=val1:opt2=val2:...:optn=valN,
2835 * for example bs=off:cond=on:drc=off:nwc=1.5:nicw=on:sos=on:sio=off:spl=sat:ssnc=none
2836 */
readOptionsString(vstring optionsString,bool assign)2837 void Options::readOptionsString(vstring optionsString,bool assign)
2838 {
2839 CALL("Options::readOptionsString");
2840
2841 // repeatedly look for param=value
2842 while (optionsString != "") {
2843 size_t index1 = optionsString.find('=');
2844 if (index1 == vstring::npos) {
2845 error: USER_ERROR("bad option specification '" + optionsString+"'");
2846 }
2847 size_t index = optionsString.find(':');
2848 if (index!=vstring::npos && index1 > index) {
2849 goto error;
2850 }
2851
2852 vstring param = optionsString.substr(0,index1);
2853 vstring value;
2854 if (index==vstring::npos) {
2855 value = optionsString.substr(index1+1);
2856 }
2857 else {
2858 value = optionsString.substr(index1+1,index-index1-1);
2859 }
2860 AbstractOptionValue* opt = getOptionValueByName(param);
2861 if(opt){
2862 if(assign){
2863 if (!opt->set(value)) {
2864 switch (ignoreMissing()) {
2865 case IgnoreMissing::OFF:
2866 USER_ERROR("value "+value+" for option "+ param +" not known");
2867 break;
2868 case IgnoreMissing::WARN:
2869 env.beginOutput();
2870 if (outputAllowed()) {
2871 env.beginOutput();
2872 addCommentSignForSZS(env.out());
2873 env.out() << "WARNING: value " << value << " for option "<< param <<" not known" << endl;
2874 env.endOutput();
2875 }
2876 break;
2877 case IgnoreMissing::ON:
2878 break;
2879 }
2880 }
2881 }
2882 else{
2883 vstring current = opt->getStringOfActual();
2884 if(value==current){
2885 USER_ERROR("option "+param+" uses forbidden value "+value);
2886 }
2887 }
2888 }
2889 else{
2890 switch (ignoreMissing()) {
2891 case IgnoreMissing::OFF:
2892 USER_ERROR("option "+param+" not known");
2893 break;
2894 case IgnoreMissing::WARN:
2895 env.beginOutput();
2896 if (outputAllowed()) {
2897 env.beginOutput();
2898 addCommentSignForSZS(env.out());
2899 env.out() << "WARNING: option "<< param << " not known." << endl;
2900 env.endOutput();
2901 }
2902 break;
2903 case IgnoreMissing::ON:
2904 break;
2905 }
2906 }
2907
2908 if (index==vstring::npos) {
2909 return;
2910 }
2911 optionsString = optionsString.substr(index+1);
2912 }
2913 } // readOptionsString/1
2914
2915 /**
2916 * Build options from a Spider test id.
2917 * @since 30/05/2004 Manchester
2918 * @since 21/06/2005 Manchester time limit in the test id must be
2919 * in deciseconds
2920 * @throws UserErrorException if the test id is incorrect
2921 */
readFromEncodedOptions(vstring testId)2922 void Options::readFromEncodedOptions (vstring testId)
2923 {
2924 CALL("Options::readFromTestId");
2925
2926 _normalize.actualValue = true;
2927 _testId.actualValue = testId;
2928
2929 vstring ma(testId,0,3); // the first 3 characters
2930 if (ma == "dis") {
2931 _saturationAlgorithm.actualValue = SaturationAlgorithm::DISCOUNT;
2932 }
2933 else if (ma == "lrs") {
2934 _saturationAlgorithm.actualValue = SaturationAlgorithm::LRS;
2935 }
2936 else if (ma == "ott") {
2937 _saturationAlgorithm.actualValue = SaturationAlgorithm::OTTER;
2938 }
2939 else if (ma == "ins") {
2940 _saturationAlgorithm.actualValue = SaturationAlgorithm::INST_GEN;
2941 }
2942 else if (ma == "fmb") {
2943 _saturationAlgorithm.actualValue = SaturationAlgorithm::FINITE_MODEL_BUILDING;
2944 }
2945 else {
2946 error: USER_ERROR("bad test id " + _testId.actualValue);
2947 }
2948
2949 // after last '_' we have time limit
2950 size_t index = testId.find_last_of('_');
2951 if (index == vstring::npos) { // not found
2952 goto error;
2953 }
2954 vstring timeString = testId.substr(index+1);
2955 _timeLimitInDeciseconds.set(timeString);
2956 // setting assumes seconds as default, but encoded strings use deciseconds
2957 _timeLimitInDeciseconds.actualValue = _timeLimitInDeciseconds.actualValue/10;
2958
2959 testId = testId.substr(3,index-3);
2960 switch (testId[0]) {
2961 case '+':
2962 testId = testId.substr(1);
2963 break;
2964 case '-':
2965 break;
2966 default:
2967 goto error;
2968 }
2969
2970 index = testId.find('_');
2971 vstring sel = testId.substr(0,index);
2972 _selection.set(sel);
2973 testId = testId.substr(index+1);
2974
2975 if (testId == "") {
2976 goto error;
2977 }
2978
2979 index = testId.find('_');
2980 vstring awr = testId.substr(0,index);
2981 _ageWeightRatio.set(awr.c_str());
2982 if (index==string::npos) {
2983 //there are no extra options
2984 return;
2985 }
2986 testId = testId.substr(index+1);
2987 //now read the rest of the options
2988 readOptionsString(testId);
2989 } // Options::readFromTestId
2990
setForcedOptionValues()2991 void Options::setForcedOptionValues()
2992 {
2993 CALL("Options::setForcedOptionValues");
2994
2995 if(_forcedOptions.actualValue.empty()) return;
2996 readOptionsString(_forcedOptions.actualValue);
2997 }
2998
2999 /**
3000 * Return testId vstring that represents current values of the options
3001 */
generateEncodedOptions() const3002 vstring Options::generateEncodedOptions() const
3003 {
3004 CALL("Options::generateEncodedOptions");
3005
3006 BYPASSING_ALLOCATOR;
3007 vostringstream res;
3008 //saturation algorithm
3009 vstring sat;
3010 switch(_saturationAlgorithm.actualValue){
3011 case SaturationAlgorithm::LRS : sat="lrs"; break;
3012 case SaturationAlgorithm::DISCOUNT : sat="dis"; break;
3013 case SaturationAlgorithm::OTTER : sat="ott"; break;
3014 case SaturationAlgorithm::INST_GEN : sat="ins"; break;
3015 case SaturationAlgorithm::FINITE_MODEL_BUILDING : sat="fmb"; break;
3016 default : ASSERTION_VIOLATION;
3017 }
3018
3019 res << sat;
3020
3021 //selection function
3022 res << (selection() < 0 ? "-" : "+") << abs(selection());
3023 res << "_";
3024
3025 //age-weight ratio
3026 if (ageRatio()!=1) {
3027 res << ageRatio() << ":";
3028 }
3029 res << weightRatio();
3030 res << "_";
3031
3032 Options cur=*this;
3033
3034 // Record options that do not want to be in encoded string
3035 static Set<const AbstractOptionValue*> forbidden;
3036 //we initialize the set if there's nothing inside
3037 if (forbidden.size()==0) {
3038 //things we output elsewhere
3039 forbidden.insert(&_saturationAlgorithm);
3040 forbidden.insert(&_selection);
3041 forbidden.insert(&_ageWeightRatio);
3042 forbidden.insert(&_timeLimitInDeciseconds);
3043
3044 //things we don't want to output (showHelp etc won't get to here anyway)
3045 forbidden.insert(&_mode);
3046 forbidden.insert(&_testId); // is this old version of decode?
3047 forbidden.insert(&_include);
3048 forbidden.insert(&_problemName);
3049 forbidden.insert(&_inputFile);
3050 forbidden.insert(&_randomStrategy);
3051 forbidden.insert(&_decode);
3052 forbidden.insert(&_ignoreMissing); // or maybe we do!
3053 }
3054
3055 VirtualIterator<AbstractOptionValue*> options = _lookup.values();
3056
3057 bool first=true;
3058 while(options.hasNext()){
3059 AbstractOptionValue* option = options.next();
3060 // TODO do we want to also filter by !isDefault?
3061 if(!forbidden.contains(option) && option->is_set && !option->isDefault()){
3062 vstring name = option->shortName;
3063 if(name.empty()) name = option->longName;
3064 if(!first){ res<<":";}else{first=false;}
3065 res << name << "=" << option->getStringOfActual();
3066 }
3067 }
3068
3069 if(!first){ res << "_"; }
3070 res << Lib::Int::toString(_timeLimitInDeciseconds.actualValue);
3071
3072 return res.str();
3073
3074 }
3075
3076
3077 /**
3078 * True if the options are complete.
3079 * @since 23/07/2011 Manchester
3080 */
complete(const Problem & prb) const3081 bool Options::complete(const Problem& prb) const
3082 {
3083 CALL("Options::complete");
3084
3085 if (_showInterpolant.actualValue != InterpolantMode::OFF) {
3086 return false;
3087 }
3088
3089 //we did some transformation that made us lose completeness
3090 //(e.g. equality proxy replacing equality for reflexive predicate)
3091 if (prb.hadIncompleteTransformation()) {
3092 return false;
3093 }
3094
3095 Property& prop = *prb.getProperty();
3096
3097 // general properties causing incompleteness
3098 if (prop.hasInterpretedOperations()
3099 || prop.hasProp(Property::PR_HAS_INTEGERS)
3100 || prop.hasProp(Property::PR_HAS_REALS)
3101 || prop.hasProp(Property::PR_HAS_RATS)
3102 || prop.hasProp(Property::PR_HAS_ARRAYS)
3103 || (!prop.onlyFiniteDomainDatatypes() && prop.hasProp(Property::PR_HAS_DT_CONSTRUCTORS))
3104 || (!prop.onlyFiniteDomainDatatypes() && prop.hasProp(Property::PR_HAS_CDT_CONSTRUCTORS))) {
3105 return false;
3106 }
3107
3108 // preprocessing
3109 if (env.signature->hasDistinctGroups()) {
3110 return false;
3111 }
3112
3113 switch (_saturationAlgorithm.actualValue) {
3114 case SaturationAlgorithm::INST_GEN: return true; // !!! Implies InstGen is always complete
3115 default: break;
3116 }
3117
3118 // preprocessing for resolution-based algorithms
3119 if (_sos.actualValue != Sos::OFF) return false;
3120 // run-time rule causing incompleteness
3121 if (_forwardLiteralRewriting.actualValue) return false;
3122
3123 bool unitEquality = prop.category() == Property::UEQ;
3124 bool hasEquality = (prop.equalityAtoms() != 0);
3125
3126 if (!unitEquality) {
3127 if (_selection.actualValue <= -100 || _selection.actualValue >= 100) return false;
3128 if (_literalComparisonMode.actualValue == LiteralComparisonMode::REVERSE) return false;
3129 }
3130
3131 if (!hasEquality) {
3132 if (_binaryResolution.actualValue) return true;
3133 if (_unitResultingResolution.actualValue!=URResolution::ON) return false;
3134 // binary resolution is off
3135 return prop.category() == Property::HNE; // URR is complete for Horn problems
3136 }
3137
3138 if (!_demodulationRedundancyCheck.actualValue) return false;
3139 if (!_superpositionFromVariables.actualValue) return false;
3140
3141 // only checking resolution rules remain
3142 bool pureEquality = (prop.atoms() == prop.equalityAtoms());
3143 if (pureEquality) return true;
3144 return (_binaryResolution.actualValue); // MS: we are in the equality case, so URR cannot help here even for horn problems
3145 } // Options::complete
3146
3147 /**
3148 * True if the options are complete for non-Horn problems without equality.
3149 * @since 02/08/2011 Wroclaw
3150 */
completeForNNE() const3151 bool Options::completeForNNE() const
3152 {
3153 CALL("Options::completeForNNE");
3154
3155 // preprocessing
3156 if (_sineSelection.actualValue != SineSelection::OFF) return false;
3157
3158 switch (_saturationAlgorithm.actualValue) {
3159 case SaturationAlgorithm::INST_GEN: return true; // !!!
3160 default: break;
3161 }
3162
3163 // preprocessing for resolution-based algorithms
3164 if (_sos.actualValue != Sos::OFF) return false;
3165 // run-time rule causing incompleteness
3166 if (_forwardLiteralRewriting.actualValue) return false;
3167
3168 if (_selection.actualValue <= -100 || _selection.actualValue >= 100) return false;
3169
3170 return _binaryResolution.actualValue;
3171 } // Options::completeForNNE
3172
3173
3174 /**
3175 * Check constraints necessary for options to make sense
3176 *
3177 * The function is called after all options are parsed.
3178 */
checkGlobalOptionConstraints(bool fail_early)3179 bool Options::checkGlobalOptionConstraints(bool fail_early)
3180 {
3181 CALL("Options::checkGlobalOptionsConstraints");
3182
3183 //Check forbidden options
3184 readOptionsString(_forbiddenOptions.actualValue,false);
3185
3186 //if we're not in mid-randomisation then check bfnt completeness
3187 //this assumes that fail_early is only on when being called from randomizeStrategy
3188 if(!fail_early && env.options->bfnt() && !completeForNNE()){
3189 return false;
3190 }
3191
3192 bool result = true;
3193
3194 // Check recorded option constraints
3195 VirtualIterator<AbstractOptionValue*> options = _lookup.values();
3196 while(options.hasNext()){
3197 result = options.next()->checkConstraints() && result;
3198 if(fail_early && !result) return result;
3199 }
3200
3201 return result;
3202 }
3203
3204 /**
3205 * Check whether the option values make sense with respect to the given problem
3206 **/
checkProblemOptionConstraints(Property * prop,bool fail_early)3207 bool Options::checkProblemOptionConstraints(Property* prop,bool fail_early)
3208 {
3209 CALL("Options::checkProblemOptionConstraints");
3210
3211 bool result = true;
3212
3213 VirtualIterator<AbstractOptionValue*> options = _lookup.values();
3214 while(options.hasNext()){
3215 result = options.next()->checkProblemConstraints(prop) && result;
3216 if(fail_early && !result) return result;
3217 }
3218
3219 return result;
3220 }
3221
theorySplitQueueRatios() const3222 Lib::vvector<int> Options::theorySplitQueueRatios() const
3223 {
3224 CALL("Options::theorySplitQueueRatios");
3225 vstringstream inputRatiosStream(_theorySplitQueueRatios.actualValue);
3226 Lib::vvector<int> inputRatios;
3227 std::string currentRatio;
3228 while (std::getline(inputRatiosStream, currentRatio, ',')) {
3229 inputRatios.push_back(std::stoi(currentRatio));
3230 }
3231
3232 // sanity checks
3233 if (inputRatios.size() < 2) {
3234 USER_ERROR("Wrong usage of option '-thsqr'. Needs to have at least two values (e.g. '10,1')");
3235 }
3236 for (unsigned i = 0; i < inputRatios.size(); i++) {
3237 if(inputRatios[i] <= 0) {
3238 USER_ERROR("Wrong usage of option '-thsqr'. Each ratio needs to be a positive integer");
3239 }
3240 }
3241
3242 return inputRatios;
3243 }
3244
theorySplitQueueCutoffs() const3245 Lib::vvector<float> Options::theorySplitQueueCutoffs() const
3246 {
3247 CALL("Options::theorySplitQueueCutoffs");
3248 // initialize cutoffs
3249 Lib::vvector<float> cutoffs;
3250 if (_theorySplitQueueCutoffs.isDefault()) {
3251 // if no custom cutoffs are set, use heuristics: (0,4*d,10*d,infinity)
3252 auto d = _theorySplitQueueExpectedRatioDenom.actualValue;
3253 cutoffs.push_back(0.0f);
3254 cutoffs.push_back(4.0f * d);
3255 cutoffs.push_back(10.0f * d);
3256 cutoffs.push_back(std::numeric_limits<float>::max());
3257 } else {
3258 // if custom cutoffs are set, parse them and add float-max as last value
3259 vstringstream cutoffsStream(_theorySplitQueueCutoffs.actualValue);
3260 std::string currentCutoff;
3261 while (std::getline(cutoffsStream, currentCutoff, ','))
3262 {
3263 cutoffs.push_back(std::stof(currentCutoff));
3264 }
3265 cutoffs.push_back(std::numeric_limits<float>::max());
3266 }
3267
3268 // sanity checks
3269 for (unsigned i = 0; i < cutoffs.size(); i++)
3270 {
3271 auto cutoff = cutoffs[i];
3272
3273 if (i > 0 && cutoff <= cutoffs[i-1])
3274 {
3275 USER_ERROR("Wrong usage of option '-thsqc'. The cutoff values must be strictly increasing");
3276 }
3277 }
3278
3279 return cutoffs;
3280 }
3281
avatarSplitQueueRatios() const3282 Lib::vvector<int> Options::avatarSplitQueueRatios() const
3283 {
3284 CALL("Options::avatarSplitQueueRatios");
3285 vstringstream inputRatiosStream(_avatarSplitQueueRatios.actualValue);
3286 Lib::vvector<int> inputRatios;
3287 std::string currentRatio;
3288 while (std::getline(inputRatiosStream, currentRatio, ',')) {
3289 inputRatios.push_back(std::stoi(currentRatio));
3290 }
3291
3292 // sanity checks
3293 if (inputRatios.size() < 2) {
3294 USER_ERROR("Wrong usage of option '-avsqr'. Needs to have at least two values (e.g. '10,1')");
3295 }
3296 for (unsigned i = 0; i < inputRatios.size(); i++) {
3297 if(inputRatios[i] <= 0) {
3298 USER_ERROR("Each ratio (supplied by option '-avsqr') needs to be a positive integer");
3299 }
3300 }
3301
3302 return inputRatios;
3303 }
3304
avatarSplitQueueCutoffs() const3305 Lib::vvector<float> Options::avatarSplitQueueCutoffs() const
3306 {
3307 CALL("Options::avatarSplitQueueCutoffs");
3308 // initialize cutoffs and add float-max as last value
3309 Lib::vvector<float> cutoffs;
3310 vstringstream cutoffsStream(_avatarSplitQueueCutoffs.actualValue);
3311 std::string currentCutoff;
3312 while (std::getline(cutoffsStream, currentCutoff, ','))
3313 {
3314 cutoffs.push_back(std::stof(currentCutoff));
3315 }
3316 cutoffs.push_back(std::numeric_limits<float>::max());
3317
3318 // sanity checks
3319 for (unsigned i = 0; i < cutoffs.size(); i++)
3320 {
3321 auto cutoff = cutoffs[i];
3322
3323 if (i > 0 && cutoff <= cutoffs[i-1])
3324 {
3325 USER_ERROR("The cutoff values (supplied by option '-avsqc') must be strictly increasing");
3326 }
3327 }
3328
3329 return cutoffs;
3330 }
3331
sineLevelSplitQueueRatios() const3332 Lib::vvector<int> Options::sineLevelSplitQueueRatios() const
3333 {
3334 CALL("Options::sineLevelSplitQueueRatios");
3335 vstringstream inputRatiosStream(_sineLevelSplitQueueRatios.actualValue);
3336 Lib::vvector<int> inputRatios;
3337 std::string currentRatio;
3338 while (std::getline(inputRatiosStream, currentRatio, ',')) {
3339 inputRatios.push_back(std::stoi(currentRatio));
3340 }
3341
3342 // sanity checks
3343 if (inputRatios.size() < 2) {
3344 USER_ERROR("Wrong usage of option '-slsqr'. Needs to have at least two values (e.g. '1,3')");
3345 }
3346 for (unsigned i = 0; i < inputRatios.size(); i++) {
3347 if(inputRatios[i] <= 0) {
3348 USER_ERROR("Each ratio (supplied by option '-slsqr') needs to be a positive integer");
3349 }
3350 }
3351
3352 return inputRatios;
3353 }
3354
sineLevelSplitQueueCutoffs() const3355 Lib::vvector<float> Options::sineLevelSplitQueueCutoffs() const
3356 {
3357 CALL("Options::sineLevelSplitQueueCutoffs");
3358 // initialize cutoffs and add float-max as last value
3359 Lib::vvector<float> cutoffs;
3360 vstringstream cutoffsStream(_sineLevelSplitQueueCutoffs.actualValue);
3361 std::string currentCutoff;
3362 while (std::getline(cutoffsStream, currentCutoff, ','))
3363 {
3364 cutoffs.push_back(std::stof(currentCutoff));
3365 }
3366 cutoffs.push_back(std::numeric_limits<float>::max());
3367
3368 // sanity checks
3369 for (unsigned i = 0; i < cutoffs.size(); i++)
3370 {
3371 auto cutoff = cutoffs[i];
3372
3373 if (i > 0 && cutoff <= cutoffs[i-1])
3374 {
3375 USER_ERROR("The cutoff values (supplied by option '-slsqc') must be strictly increasing");
3376 }
3377 }
3378
3379 return cutoffs;
3380 }
3381
positiveLiteralSplitQueueRatios() const3382 Lib::vvector<int> Options::positiveLiteralSplitQueueRatios() const
3383 {
3384 CALL("Options::positiveLiteralSplitQueueRatios");
3385 vstringstream inputRatiosStream(_positiveLiteralSplitQueueRatios.actualValue);
3386 Lib::vvector<int> inputRatios;
3387 std::string currentRatio;
3388 while (std::getline(inputRatiosStream, currentRatio, ',')) {
3389 inputRatios.push_back(std::stoi(currentRatio));
3390 }
3391
3392 // sanity checks
3393 if (inputRatios.size() < 2) {
3394 USER_ERROR("Wrong usage of option '-plsqr'. Needs to have at least two values (e.g. '1,3')");
3395 }
3396 for (unsigned i = 0; i < inputRatios.size(); i++) {
3397 if(inputRatios[i] <= 0) {
3398 USER_ERROR("Each ratio (supplied by option '-plsqr') needs to be a positive integer");
3399 }
3400 }
3401
3402 return inputRatios;
3403 }
3404
positiveLiteralSplitQueueCutoffs() const3405 Lib::vvector<float> Options::positiveLiteralSplitQueueCutoffs() const
3406 {
3407 CALL("Options::positiveLiteralSplitQueueCutoffs");
3408 // initialize cutoffs and add float-max as last value
3409 Lib::vvector<float> cutoffs;
3410 vstringstream cutoffsStream(_positiveLiteralSplitQueueCutoffs.actualValue);
3411 std::string currentCutoff;
3412 while (std::getline(cutoffsStream, currentCutoff, ','))
3413 {
3414 cutoffs.push_back(std::stof(currentCutoff));
3415 }
3416 cutoffs.push_back(std::numeric_limits<float>::max());
3417
3418 // sanity checks
3419 for (unsigned i = 0; i < cutoffs.size(); i++)
3420 {
3421 auto cutoff = cutoffs[i];
3422
3423 if (i > 0 && cutoff <= cutoffs[i-1])
3424 {
3425 USER_ERROR("The cutoff values (supplied by option '-plsqc') must be strictly increasing");
3426 }
3427 }
3428
3429 return cutoffs;
3430 }
3431