1
2 /*
3 * File Options.hpp.
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.hpp
21 * Defines Vampire options.
22 *
23 * INSTRUCTIONS on Adding a new Option
24 *
25 * Firstly, the easiest thing to do is copy what's been done for an existing option
26 *
27 * In Options.hpp
28 * - Add an OptionValue object (see NOTE on OptionValues below)
29 * - Add enum for choices if ChoiceOptionValue
30 * - Add getter for OptionValue
31 * - Only if necessary (usually not), add setter for OptionValue
32 *
33 * In Options.cpp
34 * - Initialise the OptionValue member, to do this you need to
35 * -- Call the constructor with at least a long name, short name and default value
36 * -- Provide a description
37 * -- Insert the option into lookup (this is essential)
38 * -- Tag the option, otherwise it will not appear nicely in showOptions
39 * -- Add value constraints, they can be soft or hard (see NOTE on OptionValueConstraints below)
40 * -- Add problem constraints (see NOTE on OptionProblemConstraints)
41 *
42 */
43
44 #ifndef __Options__
45 #define __Options__
46
47 #include <type_traits>
48 #include <cstring>
49 #include <memory>
50
51 #include "Forwards.hpp"
52
53 #include "Debug/Assertion.hpp"
54
55 #include "Lib/VString.hpp"
56 #include "Lib/VirtualIterator.hpp"
57 #include "Lib/DHMap.hpp"
58 #include "Lib/DArray.hpp"
59 #include "Lib/Stack.hpp"
60 #include "Lib/Int.hpp"
61 #include "Lib/Allocator.hpp"
62 #include "Lib/XML.hpp"
63 #include "Lib/Comparison.hpp"
64 #include "Lib/STL.hpp"
65
66 #include "Property.hpp"
67
68 namespace Shell {
69
70 using namespace Lib;
71 using namespace Kernel;
72
73 class Property;
74
75 /**
76 * Let us define a similarity measure for strings, used to compare option names
77 *
78 * This is a Levenshtein (edit) distance and therefore gives the number
79 * of edits needed to change s1 into s2
80 *
81 * TODO does not really belong here!
82 *
83 * @author Giles
84 */
distance(const vstring & s1,const vstring & s2)85 static size_t distance(const vstring &s1, const vstring &s2)
86 {
87 const size_t m(s1.size());
88 const size_t n(s2.size());
89
90 if( m==0 ) return n;
91 if( n==0 ) return m;
92
93 DArray<size_t> costs = DArray<size_t>(n+1);
94
95 for( size_t k=0; k<=n; k++ ) costs[k] = k;
96
97 size_t i = 0;
98 for ( vstring::const_iterator it1 = s1.begin(); it1 != s1.end(); ++it1, ++i )
99 {
100 costs[0] = i+1;
101 size_t corner = i;
102
103 size_t j = 0;
104 for ( vstring::const_iterator it2 = s2.begin(); it2 != s2.end(); ++it2, ++j )
105 {
106 size_t upper = costs[j+1];
107 if( *it1 == *it2 ){costs[j+1] = corner;}
108 else{
109 size_t t(upper<corner?upper:corner);
110 costs[j+1] = (costs[j]<t?costs[j]:t)+1;
111 }
112 corner = upper;
113 }
114 }
115
116 return costs[n];
117 }
118
119
120 /**
121 * Class that represents Vampire's options.
122 * 11/11/2004 Shrigley Hall, completely reimplemented
123 *
124 * @since Sep 14 reimplemented by Giles
125 */
126 class Options
127 {
128 public:
129
130 Options ();
131 // It is important that we can safely copy Options for use in CASC mode
132 void init();
133 void copyValuesFrom(const Options& that);
134 Options(const Options& that);
135 Options& operator=(const Options& that);
136
137 // used to print help and options
138 void output (ostream&) const;
139
140 // Dealing with encoded options. Used by --decode option
141 void readFromEncodedOptions (vstring testId);
142 void readOptionsString (vstring testId,bool assign=true);
143 vstring generateEncodedOptions() const;
144
145 // deal with completeness
146 bool complete(const Problem&) const;
147 bool completeForNNE() const;
forceIncompleteness()148 void forceIncompleteness() { _forceIncompleteness.actualValue=true; }
149
150 // deal with constraints
151 void setForcedOptionValues(); // not currently used effectively
152 bool checkGlobalOptionConstraints(bool fail_early=false);
153 bool checkProblemOptionConstraints(Property*, bool fail_early=false);
154
155 // Randomize strategy (will only work if randomStrategy=on)
156 // should only be called after all other options are set
157 //
158 // The usage is overloaded. If prop=0 then this function will randomize
159 // options that do not require a Property (no ProblemConstraints)
160 // (note it is possible to supress the requirement, see Options.cpp)
161 // Otherwise all other options will be randomized.
162 //
163 // This dual usage is required as the property object is created during
164 // the preprocessing stage. This means that in vampire.cpp we call this twice
165 void randomizeStrategy(Property* prop);
166
167 /**
168 * Return the problem name
169 *
170 * The problem name is computed from the input file name in
171 * the @b setInputFile function. If the input file is not set,
172 * the problem name is equal to "unknown". The problem name can
173 * be set to a specific value using setProblemName().
174 */
problemName() const175 const vstring& problemName () const { return _problemName.actualValue; }
setProblemName(vstring str)176 void setProblemName(vstring str) { _problemName.actualValue = str; }
177
setInputFile(const vstring & newVal)178 void setInputFile(const vstring& newVal){ _inputFile.set(newVal); }
179 vstring includeFileName (const vstring& relativeName);
180
181 CLASS_NAME(Options);
182 USE_ALLOCATOR(Options);
183
184 // standard ways of creating options
185 void set(const vstring& name, const vstring& value); // implicitly the long version used here
186 void set(const char* name, const char* value, bool longOpt);
187
188 public:
189 //==========================================================
190 // The Enums for Option Values
191 //==========================================================
192 //
193 // If you create a ChoiceOptionValue you will also need to create an enum
194
195
196 /**
197 * Possible tags to group options by
198 * Update _tagNames at the end of Options constructor if you add a tag
199 * @author Giles
200 */
201 enum class OptionTag: unsigned int {
202 UNUSED,
203 OTHER,
204 DEVELOPMENT,
205 OUTPUT,
206 INST_GEN,
207 FMB,
208 SAT,
209 AVATAR,
210 INFERENCES,
211 LRS,
212 SATURATION,
213 PREPROCESSING,
214 INPUT,
215 HELP,
216 LAST_TAG // Used for counting the number of tags
217 };
218 // update _tagNames at the end of Options constructor if you add a tag
219
220 enum class TheoryInstSimp : unsigned int {
221 OFF,
222 ALL, // select all interpreted
223 STRONG, // select strong only
224 OVERLAP, // select strong and weak which overlap with strong
225 FULL, // perform full abstraction
226 NEW
227 };
228 enum class UnificationWithAbstraction : unsigned int {
229 OFF,
230 INTERP_ONLY,
231 ONE_INTERP,
232 CONSTANT,
233 ALL,
234 GROUND
235 };
236
237 enum class Induction : unsigned int {
238 NONE,
239 STRUCTURAL,
240 MATHEMATICAL,
241 BOTH
242 };
243 enum class StructuralInductionKind : unsigned int {
244 ONE,
245 TWO,
246 THREE,
247 ALL
248 };
249 enum class MathInductionKind : unsigned int {
250 ONE,
251 TWO,
252 ALL
253 };
254
255 enum class PredicateSineLevels : unsigned int {
256 NO, // no means 1) the reverse of "on", 2) use with caution, it is predicted to be the worse value
257 OFF,
258 ON
259 };
260
261
262 enum class InductionChoice : unsigned int {
263 ALL,
264 GOAL, // only apply induction to goal constants
265 // a goal constant is one appearing in an explicit goal, or if gtg is used
266 // a constant that is used to lift a clause to a goal (uniqueness or Skolem)
267 GOAL_PLUS, // above plus skolem terms introduced in induction inferences
268 };
269
270 enum class TheoryAxiomLevel : unsigned int {
271 ON, // all of them
272 OFF, // none of them
273 CHEAP
274 };
275
276 enum class ProofExtra : unsigned int {
277 OFF,
278 FREE,
279 FULL
280 };
281 enum class FMBWidgetOrders : unsigned int {
282 FUNCTION_FIRST, // f(1) f(2) f(3) ... g(1) g(2) ...
283 ARGUMENT_FIRST, // f(1) g(1) h(1) ... f(2) g(2) ...
284 DIAGONAL, // f(1) g(2) h(3) f(2) g(3) h(1) f(3) g(1) h(2)
285 };
286 enum class FMBSymbolOrders : unsigned int {
287 OCCURENCE,
288 INPUT_USAGE,
289 PREPROCESSED_USAGE
290 };
291 enum class FMBAdjustSorts : unsigned int {
292 OFF,
293 EXPAND,
294 GROUP,
295 PREDICATE,
296 FUNCTION
297 };
298 enum class FMBEnumerationStrategy : unsigned int {
299 SBMEAM,
300 #if VZ3
301 SMT,
302 #endif
303 CONTOUR
304 };
305
306 enum class RandomStrategy : unsigned int {
307 ON,
308 OFF,
309 SAT,
310 NOCHECK
311 };
312
313 enum class BadOption : unsigned int {
314 HARD,
315 FORCED,
316 OFF,
317 SOFT
318 };
319
320 enum class LTBLearning : unsigned int {
321 ON,
322 OFF,
323 BIASED
324 };
325
326 enum class IgnoreMissing : unsigned int {
327 ON,
328 OFF,
329 WARN
330 };
331
332 //enums for the bound propagation purpose
333 enum class BPAlmostHalfBoundingRemoval : unsigned int {
334 BOUNDS_ONLY = 0,
335 OFF = 1,
336 ON = 2
337 };
338
339 enum class BPAssignmentSelector: unsigned int {
340 ALTERNATIVE = 0,
341 BMP = 1,
342 LOWER = 2,
343 MIDDLE = 3,
344 RANDOM = 4,
345 RATIONAL = 5,
346 SMALLEST = 6,
347 TIGHT = 7,
348 TIGHTISH = 8,
349 UPPER = 9
350 };
351
352 enum class BPConflictSelector: unsigned int {
353 LEAST_RECENT = 0,
354 MOST_RECENT = 1,
355 SHORTEST_CONSTRAINT = 2
356 };
357
358 enum class BPVariableSelector: unsigned int {
359 CONFLICTING = 0,
360 CONFLICTING_AND_COLLAPSING = 1,
361 FIRST = 2,
362 LOOK_AHEAD =3,
363 RANDOM = 4,
364 RECENTLY_CONFLICTING = 5,
365 RECENTLY_COLLAPSING = 6,
366 TIGHTEST_BOUND = 7
367
368 };
369 /**
370 * Possible values for function_definition_elimination.
371 * @since 29/05/2004 Manchester
372 */
373 enum class FunctionDefinitionElimination : unsigned int {
374 ALL = 0,
375 NONE = 1,
376 UNUSED = 2
377 };
378
379 /**
380 *
381 *
382 */
383 enum class Instantiation : unsigned int {
384 OFF = 0,
385 ON = 1
386 };
387
388 /**
389 * Possible values for the input syntax
390 * @since 26/08/2009 Redmond
391 */
392 enum class InputSyntax : unsigned int {
393 /** syntax of the Simplify prover */
394 //SIMPLIFY = 0,
395 /** syntax of SMTLIB1.2 */
396 //SMTLIB = 1,
397 SMTLIB2 = 0,
398 /** syntax of the TPTP prover */
399 TPTP = 1,
400 //HUMAN = 4,
401 //MPS = 5,
402 //NETLIB = 6
403 };
404
405
406 /**
407 * Possible values for mode_name.
408 * @since 06/05/2007 Manchester
409 */
410 enum class Mode : unsigned int {
411 AXIOM_SELECTION,
412 CASC,
413 CASC_SAT,
414 CASC_LTB,
415 CLAUSIFY,
416 CONSEQUENCE_ELIMINATION,
417 GROUNDING,
418 MODEL_CHECK,
419 /** this mode only outputs the input problem, without any preprocessing */
420 OUTPUT,
421 PORTFOLIO,
422 PREPROCESS,
423 PREPROCESS2,
424 PROFILE,
425 RANDOM_STRATEGY,
426 SAT,
427 SMTCOMP,
428 SPIDER,
429 TCLAUSIFY,
430 TPREPROCESS,
431 VAMPIRE
432 };
433
434 enum class Schedule : unsigned int {
435 CASC,
436 CASC_2014,
437 CASC_2014_EPR,
438 CASC_2016,
439 CASC_2017,
440 CASC_2018,
441 CASC_2019,
442 CASC_SAT,
443 CASC_SAT_2014,
444 CASC_SAT_2016,
445 CASC_SAT_2017,
446 CASC_SAT_2018,
447 CASC_SAT_2019,
448 LTB_2014,
449 LTB_2014_MZR,
450 LTB_DEFAULT_2017,
451
452 LTB_HH4_2015_FAST,
453 LTB_HH4_2015_MIDD,
454 LTB_HH4_2015_SLOW,
455 LTB_HH4_2017,
456
457 LTB_HLL_2015_FAST,
458 LTB_HLL_2015_MIDD,
459 LTB_HLL_2015_SLOW,
460 LTB_HLL_2017,
461
462 LTB_ISA_2015_FAST,
463 LTB_ISA_2015_MIDD,
464 LTB_ISA_2015_SLOW,
465 LTB_ISA_2017,
466
467 LTB_MZR_2015_FAST,
468 LTB_MZR_2015_MIDD,
469 LTB_MZR_2015_SLOW,
470 LTB_MZR_2017,
471
472 SMTCOMP,
473 SMTCOMP_2016,
474 SMTCOMP_2017,
475 SMTCOMP_2018
476 };
477
478
479 /* TODO: use an enum for Selection. The current issue is the way these values are manipulated as ints
480 *
481 enum class Selection : unsigned int {
482 TOTAL,
483 MAXIMAL,
484 TWO,
485 THREE,
486 FOUR,
487 TEN,
488 LOOKAHEAD,
489 BEST_TWO,
490 BEST_THREE,
491 BEST_FOUR,
492 BEST_TEN,
493 BEST_LOOKAHED
494 }
495 */
496
497 /** Various options for the output of statistics in Vampire */
498 enum class Statistics : unsigned int {
499 /** changed by the option "--statistics brief" */
500 BRIEF = 0,
501 /** changed by the option "--statistics full */
502 FULL = 1,
503 /** changed by the option "--statistics off" */
504 NONE = 2
505 };
506
507 /** how much we want vampire talking and in what language */
508 enum class Output : unsigned int {
509 SMTCOMP,
510 SPIDER,
511 SZS,
512 VAMPIRE
513 };
514
515 /** Possible values for sat_solver */
516 enum class SatSolver : unsigned int {
517 MINISAT = 0,
518 VAMPIRE = 1
519 #if VZ3
520 ,Z3 = 2
521 #endif
522 };
523
524 /** Possible values for saturation_algorithm */
525 enum class SaturationAlgorithm : unsigned int {
526 DISCOUNT = 0,
527 FINITE_MODEL_BUILDING = 1,
528 INST_GEN = 2,
529 LRS = 3,
530 OTTER = 4,
531 Z3 = 5,
532 };
533
534 /** Possible values for activity of some inference rules */
535 enum class RuleActivity : unsigned int {
536 INPUT_ONLY = 0,
537 OFF = 1,
538 ON = 2
539 };
540
541 enum class QuestionAnsweringMode : unsigned int {
542 ANSWER_LITERAL = 0,
543 FROM_PROOF = 1,
544 OFF = 2
545 };
546
547 enum class InterpolantMode : unsigned int {
548 NEW_HEUR = 0,
549 NEW_OPT = 1,
550 OFF = 2,
551 OLD = 3,
552 OLD_OPT = 4
553 };
554
555 enum class LiteralComparisonMode : unsigned int {
556 PREDICATE = 0,
557 REVERSE = 1,
558 STANDARD = 2
559 };
560
561 enum class Condensation : unsigned int {
562 FAST = 0,
563 OFF = 1,
564 ON = 2
565 };
566
567 enum class Demodulation : unsigned int {
568 ALL = 0,
569 OFF = 1,
570 PREORDERED = 2
571 };
572
573 enum class Subsumption : unsigned int {
574 OFF = 0,
575 ON = 1,
576 UNIT_ONLY = 2
577 };
578
579 enum class URResolution : unsigned int {
580 EC_ONLY = 0,
581 OFF = 1,
582 ON = 2
583 };
584
585 enum class TermOrdering : unsigned int {
586 KBO = 0,
587 LPO = 1,
588 };
589
590 enum class SymbolPrecedence : unsigned int {
591 ARITY = 0,
592 OCCURRENCE = 1,
593 REVERSE_ARITY = 2,
594 SCRAMBLE = 3,
595 FREQUENCY = 4,
596 REVERSE_FREQUENCY = 5,
597 WEIGHTED_FREQUENCY = 6,
598 REVERSE_WEIGHTED_FREQUENCY = 7
599 };
600 enum class SymbolPrecedenceBoost : unsigned int {
601 NONE = 0,
602 GOAL = 1,
603 UNIT = 2,
604 GOAL_UNIT = 3
605 };
606 enum class IntroducedSymbolPrecedence : unsigned int {
607 TOP = 0,
608 BOTTOM = 1
609 };
610
611 enum class SineSelection : unsigned int {
612 AXIOMS = 0,
613 INCLUDED = 1,
614 OFF = 2
615 };
616
617 enum class Proof : unsigned int {
618 OFF = 0,
619 ON = 1,
620 PROOFCHECK = 2,
621 TPTP = 3,
622 PROPERTY = 4
623 };
624
625 /** Values for --equality_proxy */
626 enum class EqualityProxy : unsigned int {
627 R = 0,
628 RS = 1,
629 RST = 2,
630 RSTC = 3,
631 OFF = 4,
632 };
633
634 /** Values for --extensionality_resolution */
635 enum class ExtensionalityResolution : unsigned int {
636 FILTER = 0,
637 KNOWN = 1,
638 TAGGED = 2,
639 OFF = 3
640 };
641
642 enum class SatRestartStrategy : unsigned int {
643 FIXED = 0,
644 GEOMETRIC = 1,
645 LUBY = 2,
646 MINISAT = 3,
647 };
648
649 enum class SatVarSelector : unsigned int {
650 ACTIVE = 0,
651 NICENESS = 1,
652 RECENTLY_LEARNT = 2,
653 };
654
655 enum class Niceness: unsigned int {
656 AVERAGE = 0,
657 NONE=1,
658 SUM = 2,
659 TOP = 3,
660 };
661
662 enum class SatClauseDisposer : unsigned int {
663 GROWING = 0,
664 MINISAT = 1,
665 };
666
667 enum class SplittingLiteralPolarityAdvice : unsigned int {
668 FALSE,
669 TRUE,
670 NONE
671 };
672
673 enum class SplittingMinimizeModel : unsigned int {
674 OFF = 0,
675 SCO = 1,
676 ALL = 2
677 };
678
679 enum class SplittingDeleteDeactivated : unsigned int {
680 ON,
681 LARGE_ONLY,
682 OFF
683 };
684
685 enum class SplittingAddComplementary : unsigned int {
686 GROUND = 0,
687 NONE = 1
688 };
689
690 enum class SplittingCongruenceClosure : unsigned int {
691 MODEL = 0,
692 OFF = 1,
693 ON = 2
694 };
695
696 enum class SplittingNonsplittableComponents : unsigned int {
697 ALL = 0,
698 ALL_DEPENDENT = 1,
699 KNOWN = 2,
700 NONE = 3
701 };
702
703 enum class CCUnsatCores : unsigned int {
704 FIRST = 0,
705 SMALL_ONES = 1,
706 ALL = 2
707 };
708
709 enum class GlobalSubsumptionSatSolverPower : unsigned int {
710 PROPAGATION_ONLY,
711 FULL
712 };
713
714 enum class GlobalSubsumptionExplicitMinim : unsigned int {
715 OFF,
716 ON,
717 RANDOMIZED
718 };
719
720 enum class GlobalSubsumptionAvatarAssumptions : unsigned int {
721 OFF,
722 FROM_CURRENT,
723 FULL_MODEL
724 };
725
726 enum class Sos : unsigned int{
727 ALL = 0,
728 OFF = 1,
729 ON = 2,
730 THEORY = 3
731 };
732
733 enum class TARules : unsigned int {
734 OFF = 0,
735 INJECTGEN = 1,
736 INJECTSIMPL = 2,
737 INJECTOPT = 2,
738 FULL = 3
739 };
740
741 enum class TACyclicityCheck : unsigned int {
742 OFF = 0,
743 AXIOM = 1,
744 RULE = 2,
745 RULELIGHT = 3
746 };
747
748 enum class GoalGuess : unsigned int {
749 OFF = 0,
750 ALL = 1,
751 EXISTS_TOP = 2,
752 EXISTS_ALL = 3,
753 EXISTS_SYM = 4,
754 POSITION = 5
755 };
756
757 enum class AgeWeightRatioShape {
758 CONSTANT,
759 DECAY,
760 CONVERGE
761 };
762
763 //==========================================================
764 // The Internals
765 //==========================================================
766 // Here I define the internal structures used to specify Options
767 // Normally these are not modified, see below for getters and values
768 //
769 // The internals consist of
770 // - OptionChoiceValues: to store the names of a option choice
771 // - OptionValue: stores an options value and meta-data
772 // - OptionValueConstraint: to give a constraint on an option
773 // - OptionProblemConstraint: to give a constraint on an option wrt the problem
774 //
775 // The details are explained in comments below
776 private:
777
778 /**
779 * These store the names of the choices for an option.
780 * They can be declared using initializer lists i.e. {"on","off","half_on"}
781 *
782 * TODO: this uses a linear search, for alternative see NameArray
783 *
784 * @author Giles
785 * @since 30/07/14
786 */
787 struct OptionChoiceValues{
788
OptionChoiceValuesShell::Options::OptionChoiceValues789 OptionChoiceValues(){ };
OptionChoiceValuesShell::Options::OptionChoiceValues790 OptionChoiceValues(std::initializer_list<vstring> list){
791 for(std::initializer_list<vstring>::iterator it = list.begin();
792 it!=list.end();++it){
793 names.push(*it);
794 ASS((*it).size()<70); // or else cannot be printed on a line
795 }
796 }
797
findShell::Options::OptionChoiceValues798 int find(vstring value) const {
799 for(unsigned i=0;i<names.length();i++){
800 if(value.compare(names[i])==0) return i;
801 }
802 return -1;
803 }
lengthShell::Options::OptionChoiceValues804 const int length() const { return names.length(); }
operator []Shell::Options::OptionChoiceValues805 const vstring operator[](int i) const{ return names[i];}
806
807 private:
808 Stack<vstring> names;
809 };
810
811 // Declare constraints here so they can be referred to, but define them below
812 template<typename T>
813 struct OptionValueConstraint;
814 template<typename T>
815 using OptionValueConstraintUP = std::unique_ptr<OptionValueConstraint<T>>;
816 struct AbstractWrappedConstraint;
817 typedef std::unique_ptr<AbstractWrappedConstraint> AbstractWrappedConstraintUP;
818 struct OptionProblemConstraint;
819 typedef std::unique_ptr<OptionProblemConstraint> OptionProblemConstraintUP;
820
821 /**
822 * An AbstractOptionValue includes all the information and functionality that does not
823 * depend on the type of the stored option. This is inherited by the templated OptionValue.
824 *
825 * The main purpose of the AbstractOptionValue is to allow us to have a collection of pointers
826 * to OptionValue objects
827 *
828 * @author Giles
829 */
830 struct AbstractOptionValue {
831
832 CLASS_NAME(AbstractOptionValue);
833 USE_ALLOCATOR(AbstractOptionValue);
834
AbstractOptionValueShell::Options::AbstractOptionValue835 AbstractOptionValue(){}
AbstractOptionValueShell::Options::AbstractOptionValue836 AbstractOptionValue(vstring l,vstring s) :
837 longName(l), shortName(s), experimental(false), is_set(false),_should_copy(true), _tag(OptionTag::LAST_TAG), supress_problemconstraints(false) {}
838
839 // Never copy an OptionValue... the Constraint system would break
840 AbstractOptionValue(const AbstractOptionValue&) = delete;
841 AbstractOptionValue& operator=(const AbstractOptionValue&) = delete;
842
843 // however move-assigment is needed for all the assigns in Options::init()
844 AbstractOptionValue(AbstractOptionValue&&) = default;
845 AbstractOptionValue& operator= (AbstractOptionValue && ) = default;
846
847 virtual ~AbstractOptionValue() = default;
848
849 // This is the main method, it sets the value of the option using an input string
850 // Returns false if we cannot set (will cause a UserError in Options::set)
851 virtual bool setValue(const vstring& value) = 0;
852
setShell::Options::AbstractOptionValue853 bool set(const vstring& value){
854 bool okay = setValue(value);
855 if(okay) is_set=true;
856 return okay;
857 }
858
859 // Set to a random value
860 virtual bool randomize(Property* P) = 0;
861
862 // Experimental options are not included in help
setExperimentalShell::Options::AbstractOptionValue863 void setExperimental(){experimental=true;}
864
865 // Meta-data
866 vstring longName;
867 vstring shortName;
868 vstring description;
869 bool experimental;
870 bool is_set;
871
872 // Checking constraits
873 virtual bool checkConstraints() = 0;
874 virtual bool checkProblemConstraints(Property* prop) = 0;
875
876 // Tagging: options can be filtered by mode and are organised by Tag in showOptions
tagShell::Options::AbstractOptionValue877 void tag(OptionTag tag){ ASS(_tag==OptionTag::LAST_TAG);_tag=tag; }
tagShell::Options::AbstractOptionValue878 void tag(Options::Mode mode){ _modes.push(mode); }
879
getTagShell::Options::AbstractOptionValue880 OptionTag getTag(){ return _tag;}
inModeShell::Options::AbstractOptionValue881 bool inMode(Options::Mode mode){
882 if(_modes.isEmpty()) return true;
883 else return _modes.find(mode);
884 }
885
886 // This allows us to get the actual value in string form
887 virtual vstring getStringOfActual() const = 0;
888 // Check if default value
889 virtual bool isDefault() const = 0;
890
891 // For use in showOptions and explainOption
892 //virtual void output(vstringstream& out) const {
outputShell::Options::AbstractOptionValue893 virtual void output(ostream& out,bool linewrap) const {
894 CALL("Options::AbstractOptionValue::output");
895 out << "--" << longName;
896 if(!shortName.empty()){ out << " (-"<<shortName<<")"; }
897 out << endl;
898
899 if (experimental) {
900 out << "\t[experimental]" << endl;
901 }
902
903
904 if(!description.empty()){
905 // Break a the description into lines where there have been at least 70 characters
906 // on the line at the next space
907 out << "\t";
908 int count=0;
909 for(const char* p = description.c_str();*p;p++){
910 out << *p;
911 count++;
912 if(linewrap && count>70 && *p==' '){
913 out << endl << '\t';
914 count=0;
915 }
916 if(*p=='\n'){ count=0; out << '\t'; }
917 }
918 out << endl;
919 }
920 else{ out << "\tno description provided!" << endl; }
921 }
922
923 // Used to determine wheter the value of an option should be copied when
924 // the Options object is copied.
925 bool _should_copy;
shouldCopyShell::Options::AbstractOptionValue926 bool shouldCopy() const { return _should_copy; }
927
928 typedef std::unique_ptr<DArray<vstring>> vstringDArrayUP;
929
930 typedef pair<OptionProblemConstraintUP,vstringDArrayUP> RandEntry;
931
setRandomChoicesShell::Options::AbstractOptionValue932 void setRandomChoices(std::initializer_list<vstring> list){
933 rand_choices.push(RandEntry(OptionProblemConstraintUP(),toArray(list)));
934 }
setRandomChoicesShell::Options::AbstractOptionValue935 void setRandomChoices(std::initializer_list<vstring> list,
936 std::initializer_list<vstring> list_sat){
937 rand_choices.push(RandEntry(isRandOn(),toArray(list)));
938 rand_choices.push(RandEntry(isRandSat(),toArray(list_sat)));
939 }
setRandomChoicesShell::Options::AbstractOptionValue940 void setRandomChoices(OptionProblemConstraintUP c,
941 std::initializer_list<vstring> list){
942 rand_choices.push(RandEntry(std::move(c),toArray(list)));
943 }
setNoPropertyRandomChoicesShell::Options::AbstractOptionValue944 void setNoPropertyRandomChoices(std::initializer_list<vstring> list){
945 rand_choices.push(RandEntry(OptionProblemConstraintUP(),toArray(list)));
946 supress_problemconstraints=true;
947 }
948
949
950 private:
951 // Tag state
952 OptionTag _tag;
953 Lib::Stack<Options::Mode> _modes;
954
toArrayShell::Options::AbstractOptionValue955 vstringDArrayUP toArray(std::initializer_list<vstring>& list){
956 DArray<vstring>* array = new DArray<vstring>(list.size());
957 unsigned index=0;
958 for(typename std::initializer_list<vstring>::iterator it = list.begin();
959 it!=list.end();++it){ (*array)[index++] =*it; }
960 return vstringDArrayUP(array);
961 }
962 protected:
963 // Note has LIFO semantics so use BottomFirstIterator
964 Stack<RandEntry> rand_choices;
965 bool supress_problemconstraints;
966 };
967
968 struct AbstractOptionValueCompatator{
compareShell::Options::AbstractOptionValueCompatator969 Comparison compare(AbstractOptionValue* o1, AbstractOptionValue* o2)
970 {
971 int value = strcmp(o1->longName.c_str(),o2->longName.c_str());
972 return value < 0 ? LESS : (value==0 ? EQUAL : GREATER);
973 }
974 };
975
976 /**
977 * The templated OptionValue is used to store default and actual values for options
978 *
979 * There are also type-related helper functions
980 *
981 * @author Giles
982 */
983 template<typename T>
984 struct OptionValue : public AbstractOptionValue {
985
986 CLASS_NAME(OptionValue);
987 USE_ALLOCATOR(OptionValue);
988
989 // We need to include an empty constructor as all the OptionValue objects need to be initialized
990 // with something when the Options object is created. They should then all be reconstructed
991 // This is annoying but preferable to the alternative in my opinion
OptionValueShell::Options::OptionValue992 OptionValue(){}
OptionValueShell::Options::OptionValue993 OptionValue(vstring l, vstring s,T def) : AbstractOptionValue(l,s),
994 defaultValue(def), actualValue(def){}
995
996 // We store the defaultValue separately so that we can check if the actualValue is non-default
997 T defaultValue;
998 T actualValue;
999
isDefaultShell::Options::OptionValue1000 virtual bool isDefault() const { return defaultValue==actualValue;}
1001
1002 // Getting the string versions of values, useful for output
getStringOfValueShell::Options::OptionValue1003 virtual vstring getStringOfValue(T value) const{ ASSERTION_VIOLATION;}
getStringOfActualShell::Options::OptionValue1004 virtual vstring getStringOfActual() const { return getStringOfValue(actualValue); }
1005
1006 // Adding and checking constraints
1007 // By default constraints are soft and reaction to them is controlled by the bad_option option
1008 // But a constraint can be added as Hard, meaning that it always causes a UserError
addConstraintShell::Options::OptionValue1009 void addConstraint(OptionValueConstraintUP<T> c){ _constraints.push(std::move(c)); }
addHardConstraintShell::Options::OptionValue1010 void addHardConstraint(OptionValueConstraintUP<T> c){ c->setHard();addConstraint(std::move(c)); }
1011
1012 // A reliesOn constraint gives a constraint that must be true if a non-default value is used
1013 // For example, split_at_activation relies on splitting being on
1014 // These are defined for OptionValueConstraints and WrappedConstraints - see below for explanation
reliesOnShell::Options::OptionValue1015 void reliesOn(AbstractWrappedConstraintUP c){
1016 _constraints.push(If(getNotDefault()).then(unwrap<T>(c)));
1017 }
reliesOnShell::Options::OptionValue1018 void reliesOn(OptionValueConstraintUP<T> c){
1019 _constraints.push(If(getNotDefault()).then(std::move(c)));
1020 }
getNotDefaultShell::Options::OptionValue1021 virtual OptionValueConstraintUP<T> getNotDefault(){ return isNotDefault<T>(); }
reliesOnHardShell::Options::OptionValue1022 void reliesOnHard(AbstractWrappedConstraintUP c){
1023 OptionValueConstraintUP<T> tc = If(getNotDefault()).then(unwrap<T>(c));
1024 tc->setHard();
1025 _constraints.push(std::move(tc));
1026 }
reliesOnHardShell::Options::OptionValue1027 void reliesOnHard(OptionValueConstraintUP<T> c){
1028 OptionValueConstraintUP<T> tc = If(getNotDefault()).then(c);
1029 tc->setHard();
1030 _constraints.push(std::move(tc));
1031 }
1032 // This checks the constraints and may cause a UserError
1033 bool checkConstraints();
1034
1035 // Produces a separate constraint object based on this option
1036 /// Useful for IfThen constraints and reliesOn i.e. _splitting.is(equal(true))
1037 AbstractWrappedConstraintUP is(OptionValueConstraintUP<T> c);
1038
1039 // Problem constraints place a restriction on problem properties and option values
addProblemConstraintShell::Options::OptionValue1040 void addProblemConstraint(OptionProblemConstraintUP c){ _prob_constraints.push(std::move(c)); }
hasProblemConstraintsShell::Options::OptionValue1041 bool hasProblemConstraints(){
1042 return !supress_problemconstraints && !_prob_constraints.isEmpty();
1043 }
1044 virtual bool checkProblemConstraints(Property* prop);
1045
outputShell::Options::OptionValue1046 virtual void output(ostream& out, bool linewrap) const {
1047 CALL("Options::OptionValue::output");
1048 AbstractOptionValue::output(out,linewrap);
1049 out << "\tdefault: " << getStringOfValue(defaultValue) << endl;
1050 }
1051
1052 // This is where actual randomisation happens
1053 bool randomize(Property* p);
1054
1055 private:
1056 Lib::Stack<OptionValueConstraintUP<T>> _constraints;
1057 Lib::Stack<OptionProblemConstraintUP> _prob_constraints;
1058 };
1059
1060 /**
1061 * We now define particular OptionValues, see NOTE on OptionValues for high level usage
1062 */
1063
1064 /**
1065 * A ChoiceOptionValue is templated by an enum, which must be defined above
1066 *
1067 * It is then necessary to provide names for the enum values.
1068 * We do not check that those names have the same length as the enum but this is very important.
1069 * The names must also be in the same order!
1070 *
1071 * @author Giles
1072 */
1073 template<typename T >
1074 struct ChoiceOptionValue : public OptionValue<T> {
1075
1076 CLASS_NAME(ChoiceOptionValue);
1077 USE_ALLOCATOR(ChoiceOptionValue);
1078
ChoiceOptionValueShell::Options::ChoiceOptionValue1079 ChoiceOptionValue(){}
ChoiceOptionValueShell::Options::ChoiceOptionValue1080 ChoiceOptionValue(vstring l, vstring s,T def,OptionChoiceValues c) :
1081 OptionValue<T>(l,s,def), choices(c) {}
1082
setValueShell::Options::ChoiceOptionValue1083 bool setValue(const vstring& value){
1084 // makes reasonable assumption about ordering of every enum
1085 int index = choices.find(value.c_str());
1086 if(index<0) return false;
1087 this->actualValue = static_cast<T>(index);
1088 return true;
1089 }
1090
outputShell::Options::ChoiceOptionValue1091 virtual void output(ostream& out,bool linewrap) const {
1092 AbstractOptionValue::output(out,linewrap);
1093 out << "\tdefault: " << choices[static_cast<unsigned>(this->defaultValue)];
1094 out << endl;
1095 string values_header = "values: ";
1096 out << "\t" << values_header;
1097 // Again we restrict line length to 70 characters
1098 int count=0;
1099 for(int i=0;i<choices.length();i++){
1100 if(i==0){
1101 out << choices[i];
1102 }
1103 else{
1104 out << ",";
1105 vstring next = choices[i];
1106 if(linewrap && next.size()+count>60){ // next.size() will be <70, how big is a tab?
1107 out << endl << "\t";
1108 for(unsigned j=0;j<values_header.size();j++){out << " ";}
1109 count = 0;
1110 }
1111 out << next;
1112 count += next.size();
1113 }
1114 }
1115 out << endl;
1116 }
1117
getStringOfValueShell::Options::ChoiceOptionValue1118 vstring getStringOfValue(T value) const {
1119 unsigned i = static_cast<unsigned>(value);
1120 return choices[i];
1121 }
1122
1123 private:
1124 OptionChoiceValues choices;
1125 };
1126 /**
1127 * For Booleans - we use on/off rather than true/false
1128 * @author Giles
1129 */
1130 struct BoolOptionValue : public OptionValue<bool> {
BoolOptionValueShell::Options::BoolOptionValue1131 BoolOptionValue(){}
BoolOptionValueShell::Options::BoolOptionValue1132 BoolOptionValue(vstring l,vstring s, bool d) : OptionValue(l,s,d){}
setValueShell::Options::BoolOptionValue1133 bool setValue(const vstring& value){
1134 if (! value.compare("on") || ! value.compare("true")) {
1135 actualValue=true;
1136
1137 }
1138 else if (! value.compare("off") || ! value.compare("false")) {
1139 actualValue=false;
1140 }
1141 else return false;
1142
1143 return true;
1144 }
1145
getStringOfValueShell::Options::BoolOptionValue1146 vstring getStringOfValue(bool value) const { return (value ? "on" : "off"); }
1147 };
1148 struct IntOptionValue : public OptionValue<int> {
IntOptionValueShell::Options::IntOptionValue1149 IntOptionValue(){}
IntOptionValueShell::Options::IntOptionValue1150 IntOptionValue(vstring l,vstring s, int d) : OptionValue(l,s,d){}
setValueShell::Options::IntOptionValue1151 bool setValue(const vstring& value){
1152 return Int::stringToInt(value.c_str(),actualValue);
1153 }
getStringOfValueShell::Options::IntOptionValue1154 vstring getStringOfValue(int value) const{ return Lib::Int::toString(value); }
1155 };
1156
1157 struct UnsignedOptionValue : public OptionValue<unsigned> {
UnsignedOptionValueShell::Options::UnsignedOptionValue1158 UnsignedOptionValue(){}
UnsignedOptionValueShell::Options::UnsignedOptionValue1159 UnsignedOptionValue(vstring l,vstring s, unsigned d) : OptionValue(l,s,d){}
1160
setValueShell::Options::UnsignedOptionValue1161 bool setValue(const vstring& value){
1162 return Int::stringToUnsignedInt(value.c_str(),actualValue);
1163 }
getStringOfValueShell::Options::UnsignedOptionValue1164 vstring getStringOfValue(unsigned value) const{ return Lib::Int::toString(value); }
1165 };
1166
1167 struct StringOptionValue : public OptionValue<vstring> {
StringOptionValueShell::Options::StringOptionValue1168 StringOptionValue(){}
StringOptionValueShell::Options::StringOptionValue1169 StringOptionValue(vstring l,vstring s, vstring d) : OptionValue(l,s,d){}
setValueShell::Options::StringOptionValue1170 bool setValue(const vstring& value){
1171 actualValue = (value=="<empty>") ? "" : value;
1172 return true;
1173 }
getStringOfValueShell::Options::StringOptionValue1174 vstring getStringOfValue(vstring value) const{
1175 if(value.empty()) return "<empty>";
1176 return value;
1177 }
1178 };
1179
1180 struct LongOptionValue : public OptionValue<long> {
LongOptionValueShell::Options::LongOptionValue1181 LongOptionValue(){}
LongOptionValueShell::Options::LongOptionValue1182 LongOptionValue(vstring l,vstring s, long d) : OptionValue(l,s,d){}
setValueShell::Options::LongOptionValue1183 bool setValue(const vstring& value){
1184 return Int::stringToLong(value.c_str(),actualValue);
1185 }
getStringOfValueShell::Options::LongOptionValue1186 vstring getStringOfValue(long value) const{ return Lib::Int::toString(value); }
1187 };
1188
1189 struct FloatOptionValue : public OptionValue<float>{
FloatOptionValueShell::Options::FloatOptionValue1190 FloatOptionValue(){}
FloatOptionValueShell::Options::FloatOptionValue1191 FloatOptionValue(vstring l,vstring s, float d) : OptionValue(l,s,d){}
setValueShell::Options::FloatOptionValue1192 bool setValue(const vstring& value){
1193 return Int::stringToFloat(value.c_str(),actualValue);
1194 }
getStringOfValueShell::Options::FloatOptionValue1195 vstring getStringOfValue(float value) const{ return Lib::Int::toString(value); }
1196 };
1197
1198 /**
1199 * Ratios have two actual values and two default values
1200 * Therefore, we often need to tread them specially
1201 * @author Giles
1202 */
1203 struct RatioOptionValue : public OptionValue<int> {
1204
1205 CLASS_NAME(RatioOptionValue);
1206 USE_ALLOCATOR(RatioOptionValue);
1207
RatioOptionValueShell::Options::RatioOptionValue1208 RatioOptionValue(){}
RatioOptionValueShell::Options::RatioOptionValue1209 RatioOptionValue(vstring l, vstring s, int def, int other, char sp=':') :
1210 OptionValue(l,s,def), sep(sp), defaultOtherValue(other), otherValue(other) {};
1211
getNotDefaultShell::Options::RatioOptionValue1212 virtual OptionValueConstraintUP<int> getNotDefault() override { return isNotDefaultRatio(); }
1213
addConstraintIfNotDefaultShell::Options::RatioOptionValue1214 void addConstraintIfNotDefault(AbstractWrappedConstraintUP c){
1215 addConstraint(If(isNotDefaultRatio()).then(unwrap<int>(c)));
1216 }
1217
1218 bool readRatio(const char* val,char seperator);
setValueShell::Options::RatioOptionValue1219 bool setValue(const vstring& value) override {
1220 return readRatio(value.c_str(),sep);
1221 }
1222
1223 char sep;
1224 int defaultOtherValue;
1225 int otherValue;
1226
outputShell::Options::RatioOptionValue1227 virtual void output(ostream& out,bool linewrap) const override {
1228 AbstractOptionValue::output(out,linewrap);
1229 out << "\tdefault left: " << defaultValue << endl;
1230 out << "\tdefault right: " << defaultOtherValue << endl;
1231 }
1232
getStringOfValueShell::Options::RatioOptionValue1233 virtual vstring getStringOfValue(int value) const override { ASSERTION_VIOLATION;}
getStringOfActualShell::Options::RatioOptionValue1234 virtual vstring getStringOfActual() const override {
1235 return Lib::Int::toString(actualValue)+sep+Lib::Int::toString(otherValue);
1236 }
1237
1238 };
1239
1240 // We now have a number of option-specific values
1241 // These are necessary when the option needs to be read in a special way
1242
1243 /**
1244 * Oddly gets set with a float value and then creates a ratio of value*100/100
1245 * @author Giles
1246 */
1247 struct NonGoalWeightOptionValue : public OptionValue<float>{
1248
1249 CLASS_NAME(NonGoalWeightOptionValue);
1250 USE_ALLOCATOR(NonGoalWeightOptionValue);
1251
NonGoalWeightOptionValueShell::Options::NonGoalWeightOptionValue1252 NonGoalWeightOptionValue(){}
NonGoalWeightOptionValueShell::Options::NonGoalWeightOptionValue1253 NonGoalWeightOptionValue(vstring l, vstring s, float def) :
1254 OptionValue(l,s,def), numerator(1), denominator(1) {};
1255
1256 bool setValue(const vstring& value);
1257
1258 // output does not output numerator and denominator as they
1259 // are produced from defaultValue
1260 int numerator;
1261 int denominator;
1262
getStringOfValueShell::Options::NonGoalWeightOptionValue1263 virtual vstring getStringOfValue(float value) const{ return Lib::Int::toString(value); }
1264 };
1265
1266 /**
1267 * Selection is defined by a set of integers (TODO: make enum)
1268 * For now we need to check the integer is a valid one
1269 * @author Giles
1270 */
1271 struct SelectionOptionValue : public OptionValue<int>{
SelectionOptionValueShell::Options::SelectionOptionValue1272 SelectionOptionValue(){}
SelectionOptionValueShell::Options::SelectionOptionValue1273 SelectionOptionValue(vstring l,vstring s, int def):
1274 OptionValue(l,s,def){};
1275
1276 bool setValue(const vstring& value);
1277
outputShell::Options::SelectionOptionValue1278 virtual void output(ostream& out,bool linewrap) const {
1279 AbstractOptionValue::output(out,linewrap);
1280 out << "\tdefault: " << defaultValue << endl;;
1281 }
1282
getStringOfValueShell::Options::SelectionOptionValue1283 virtual vstring getStringOfValue(int value) const{ return Lib::Int::toString(value); }
1284
isLookAheadSelectionShell::Options::SelectionOptionValue1285 AbstractWrappedConstraintUP isLookAheadSelection(){
1286 return AbstractWrappedConstraintUP(new WrappedConstraint<int>(*this,OptionValueConstraintUP<int>(new isLookAheadSelectionConstraint())));
1287 }
1288 };
1289
1290 /**
1291 * This also updates problemName
1292 * @author Giles
1293 */
1294 struct InputFileOptionValue : public OptionValue<vstring>{
InputFileOptionValueShell::Options::InputFileOptionValue1295 InputFileOptionValue(){}
InputFileOptionValueShell::Options::InputFileOptionValue1296 InputFileOptionValue(vstring l,vstring s, vstring def,Options* p):
1297 OptionValue(l,s,def), parent(p){};
1298
1299 bool setValue(const vstring& value);
1300
outputShell::Options::InputFileOptionValue1301 virtual void output(ostream& out,bool linewrap) const {
1302 AbstractOptionValue::output(out,linewrap);
1303 out << "\tdefault: " << defaultValue << endl;;
1304 }
getStringOfValueShell::Options::InputFileOptionValue1305 virtual vstring getStringOfValue(vstring value) const{ return value; }
1306 private:
1307 Options* parent;
1308
1309 };
1310 /**
1311 * We need to decode the encoded option string
1312 * @author Giles
1313 */
1314 struct DecodeOptionValue : public OptionValue<vstring>{
DecodeOptionValueShell::Options::DecodeOptionValue1315 DecodeOptionValue(){ AbstractOptionValue::_should_copy=false;}
DecodeOptionValueShell::Options::DecodeOptionValue1316 DecodeOptionValue(vstring l,vstring s,Options* p):
1317 OptionValue(l,s,""), parent(p){ AbstractOptionValue::_should_copy=false;}
1318
setValueShell::Options::DecodeOptionValue1319 bool setValue(const vstring& value){
1320 parent->readFromEncodedOptions(value);
1321 return true;
1322 }
getStringOfValueShell::Options::DecodeOptionValue1323 virtual vstring getStringOfValue(vstring value) const{ return value; }
1324
1325 private:
1326 Options* parent;
1327
1328 };
1329 /**
1330 * Need to read the time limit. By default it assumes seconds (and stores deciseconds) but you can give
1331 * a multiplier i.e. d,s,m,h,D for deciseconds,seconds,minutes,hours,Days
1332 * @author Giles
1333 */
1334 struct TimeLimitOptionValue : public OptionValue<int>{
TimeLimitOptionValueShell::Options::TimeLimitOptionValue1335 TimeLimitOptionValue(){}
TimeLimitOptionValueShell::Options::TimeLimitOptionValue1336 TimeLimitOptionValue(vstring l, vstring s, float def) :
1337 OptionValue(l,s,def) {};
1338
1339 bool setValue(const vstring& value);
1340
outputShell::Options::TimeLimitOptionValue1341 virtual void output(ostream& out,bool linewrap) const {
1342 CALL("Options::TimeLimitOptionValue::output");
1343 AbstractOptionValue::output(out,linewrap);
1344 out << "\tdefault: " << defaultValue << "d" << endl;
1345 }
getStringOfValueShell::Options::TimeLimitOptionValue1346 virtual vstring getStringOfValue(int value) const{ return Lib::Int::toString(value)+"d"; }
1347 };
1348
1349 /**
1350 * NOTE on OptionValueConstraints
1351 *
1352 * OptionValueConstraints are used to declare constraints on and between option values
1353 * these are checked in checkGlobalOptionConstraints, which should be called after
1354 * Options is updated
1355 *
1356 * As usual, see Options.cpp for examples.
1357 *
1358 * There are two kinds of ValueConstraints (see below for ProblemConstraints)
1359 *
1360 * - Unary constraints such as greaterThan, equals, ...
1361 * - If-then constraints that capture dependencies
1362 *
1363 * In both cases an attempt has been made to make the declaration of constraints
1364 * in Options.cpp as readable as possible. For example, an If-then constraint is
1365 * written as follows
1366 *
1367 * If(equals(0)).then(_otherOption.is(lessThan(5)))
1368 *
1369 * Note that the equals(0) will apply to the OptionValue that the constraint belongs to
1370 *
1371 * WrappedConstraints are produced by OptionValue.is and are used to provide constraints
1372 * on other OptionValues, as seen in the example above. Most functions work with both
1373 * OptionValueConstraint and WrappedConstraint but in some cases one of these options
1374 * may need to be added. In this case see examples from AndWrapper below.
1375 *
1376 * MS: While OptionValueConstraints are expressions which wait for a concrete value to be evaluated against:
1377 * as in \lambda value. expression(value),
1378 * WrappedConstraints have already been "closed" by providing a concrete value:
1379 * as in (\lambda value. expression(value))[concrete_value]
1380 * Finally, we can at anytime "unwrap" a WrappedConstraint by providing a "fake" lambda again on top, to turn it into a OptionValueConstraints again:
1381 * as in \lambda value. expression_ignoring_value
1382 *
1383 * The tricky part (C++-technology-wise) here is that unwrapping needs to get a type for the value
1384 * and this type is indepedent form the expression_ignoring_value for obvious reasons.
1385 * So virous overloads of things are needed until we get to the point, where the type is known and can be supplied.
1386 * (e.g. there needs to be a separate hierarchy of Wrapped expressions along the one for OptionValueConstraint ones).
1387 */
1388
1389 template<typename T>
1390 struct OptionValueConstraint{
1391 CLASS_NAME(OptionValueConstraint);
1392 USE_ALLOCATOR(OptionValueConstraint);
OptionValueConstraintShell::Options::OptionValueConstraint1393 OptionValueConstraint() : _hard(false) {}
1394
~OptionValueConstraintShell::Options::OptionValueConstraint1395 virtual ~OptionValueConstraint() {} // virtual methods present -> there should be virtual destructor
1396
1397 virtual bool check(const OptionValue<T>& value) = 0;
1398 virtual vstring msg(const OptionValue<T>& value) = 0;
1399
1400 // By default cannot force constraint
forceShell::Options::OptionValueConstraint1401 virtual bool force(OptionValue<T>* value){ return false;}
1402 // TODO - allow for hard constraints
isHardShell::Options::OptionValueConstraint1403 bool isHard(){ return _hard; }
setHardShell::Options::OptionValueConstraint1404 void setHard(){ _hard=true;}
1405 bool _hard;
1406 };
1407
1408 // A Wrapped Constraint takes an OptionValue and a Constraint
1409 // It allows us to supply a constraint on another OptionValue in an If constraint for example
1410 struct AbstractWrappedConstraint {
1411 virtual bool check() = 0;
1412 virtual vstring msg() = 0;
~AbstractWrappedConstraintShell::Options::AbstractWrappedConstraint1413 virtual ~AbstractWrappedConstraint() {};
1414 };
1415
1416 template<typename T>
1417 struct WrappedConstraint : AbstractWrappedConstraint {
1418 CLASS_NAME(WrappedConstraint);
1419 USE_ALLOCATOR(WrappedConstraint);
1420
WrappedConstraintShell::Options::WrappedConstraint1421 WrappedConstraint(const OptionValue<T>& v, OptionValueConstraintUP<T> c) : value(v), con(std::move(c)) {}
1422
checkShell::Options::WrappedConstraint1423 bool check() override {
1424 return con->check(value);
1425 }
msgShell::Options::WrappedConstraint1426 vstring msg() override {
1427 return con->msg(value);
1428 }
1429
1430 const OptionValue<T>& value;
1431 OptionValueConstraintUP<T> con;
1432 };
1433
1434 struct WrappedConstraintOrWrapper : public AbstractWrappedConstraint {
1435 CLASS_NAME(WrappedConstraintOrWrapper);
1436 USE_ALLOCATOR(WrappedConstraintOrWrapper);
WrappedConstraintOrWrapperShell::Options::WrappedConstraintOrWrapper1437 WrappedConstraintOrWrapper(AbstractWrappedConstraintUP l, AbstractWrappedConstraintUP r) : left(std::move(l)),right(std::move(r)) {}
checkShell::Options::WrappedConstraintOrWrapper1438 bool check() override {
1439 return left->check() || right->check();
1440 }
msgShell::Options::WrappedConstraintOrWrapper1441 vstring msg() override { return left->msg() + " or " + right->msg(); }
1442
1443 AbstractWrappedConstraintUP left;
1444 AbstractWrappedConstraintUP right;
1445 };
1446
1447 struct WrappedConstraintAndWrapper : public AbstractWrappedConstraint {
1448 CLASS_NAME(WrappedConstraintAndWrapper);
1449 USE_ALLOCATOR(WrappedConstraintAndWrapper);
WrappedConstraintAndWrapperShell::Options::WrappedConstraintAndWrapper1450 WrappedConstraintAndWrapper(AbstractWrappedConstraintUP l, AbstractWrappedConstraintUP r) : left(std::move(l)),right(std::move(r)) {}
checkShell::Options::WrappedConstraintAndWrapper1451 bool check() override {
1452 return left->check() && right->check();
1453 }
msgShell::Options::WrappedConstraintAndWrapper1454 vstring msg() override { return left->msg() + " and " + right->msg(); }
1455
1456 AbstractWrappedConstraintUP left;
1457 AbstractWrappedConstraintUP right;
1458 };
1459
1460 template<typename T>
1461 struct OptionValueConstraintOrWrapper : public OptionValueConstraint<T>{
1462 CLASS_NAME(OptionValueConstraintOrWrapper);
1463 USE_ALLOCATOR(OptionValueConstraintOrWrapper);
OptionValueConstraintOrWrapperShell::Options::OptionValueConstraintOrWrapper1464 OptionValueConstraintOrWrapper(OptionValueConstraintUP<T> l, OptionValueConstraintUP<T> r) : left(std::move(l)),right(std::move(r)) {}
checkShell::Options::OptionValueConstraintOrWrapper1465 bool check(const OptionValue<T>& value){
1466 return left->check(value) || right->check(value);
1467 }
msgShell::Options::OptionValueConstraintOrWrapper1468 vstring msg(const OptionValue<T>& value){ return left->msg(value) + " or " + right->msg(value); }
1469
1470 OptionValueConstraintUP<T> left;
1471 OptionValueConstraintUP<T> right;
1472 };
1473
1474 template<typename T>
1475 struct OptionValueConstraintAndWrapper : public OptionValueConstraint<T>{
1476 CLASS_NAME(OptionValueConstraintAndWrapper);
1477 USE_ALLOCATOR(OptionValueConstraintAndWrapper);
OptionValueConstraintAndWrapperShell::Options::OptionValueConstraintAndWrapper1478 OptionValueConstraintAndWrapper(OptionValueConstraintUP<T> l, OptionValueConstraintUP<T> r) : left(std::move(l)),right(std::move(r)) {}
checkShell::Options::OptionValueConstraintAndWrapper1479 bool check(const OptionValue<T>& value){
1480 return left->check(value) && right->check(value);
1481 }
msgShell::Options::OptionValueConstraintAndWrapper1482 vstring msg(const OptionValue<T>& value){ return left->msg(value) + " and " + right->msg(value); }
1483
1484 OptionValueConstraintUP<T> left;
1485 OptionValueConstraintUP<T> right;
1486 };
1487
1488 template<typename T>
1489 struct UnWrappedConstraint : public OptionValueConstraint<T>{
1490 CLASS_NAME(UnWrappedConstraint);
1491 USE_ALLOCATOR(UnWrappedConstraint);
1492
UnWrappedConstraintShell::Options::UnWrappedConstraint1493 UnWrappedConstraint(AbstractWrappedConstraintUP c) : con(std::move(c)) {}
1494
checkShell::Options::UnWrappedConstraint1495 bool check(const OptionValue<T>&){ return con->check(); }
msgShell::Options::UnWrappedConstraint1496 vstring msg(const OptionValue<T>&){ return con->msg(); }
1497
1498 AbstractWrappedConstraintUP con;
1499 };
1500
1501 template <typename T>
maybe_unwrap(OptionValueConstraintUP<T> c)1502 static OptionValueConstraintUP<T> maybe_unwrap(OptionValueConstraintUP<T> c) { return c; }
1503
1504 template <typename T>
unwrap(AbstractWrappedConstraintUP & c)1505 static OptionValueConstraintUP<T> unwrap(AbstractWrappedConstraintUP& c) { return OptionValueConstraintUP<T>(new UnWrappedConstraint<T>(std::move(c))); }
1506
1507 template <typename T>
maybe_unwrap(AbstractWrappedConstraintUP & c)1508 static OptionValueConstraintUP<T> maybe_unwrap(AbstractWrappedConstraintUP& c) { return unwrap<T>(c); }
1509
1510 /*
1511 * To avoid too many cases a certain discipline is required from the user.
1512 * Namely, OptionValueConstraints need to precede WrappedConstraints in the arguments of Or and And
1513 **/
1514
1515 // the base case (the unary Or)
1516 template <typename T>
Or(OptionValueConstraintUP<T> a)1517 OptionValueConstraintUP<T> Or(OptionValueConstraintUP<T> a) { return a; }
Or(AbstractWrappedConstraintUP a)1518 AbstractWrappedConstraintUP Or(AbstractWrappedConstraintUP a) { return a; }
1519
1520 template<typename T, typename... Args>
Or(OptionValueConstraintUP<T> a,Args...args)1521 OptionValueConstraintUP<T> Or(OptionValueConstraintUP<T> a, Args... args)
1522 {
1523 OptionValueConstraintUP<T> r = maybe_unwrap<T>(Or(std::move(args)...));
1524 return OptionValueConstraintUP<T>(new OptionValueConstraintOrWrapper<T>(std::move(a),std::move(r)));
1525 }
1526
1527 template<typename... Args>
Or(AbstractWrappedConstraintUP a,Args...args)1528 AbstractWrappedConstraintUP Or(AbstractWrappedConstraintUP a, Args... args)
1529 {
1530 AbstractWrappedConstraintUP r = Or(std::move(args)...);
1531 return AbstractWrappedConstraintUP(new WrappedConstraintOrWrapper(std::move(a),std::move(r)));
1532 }
1533
1534 // the base case (the unary And)
1535 template <typename T>
And(OptionValueConstraintUP<T> a)1536 OptionValueConstraintUP<T> And(OptionValueConstraintUP<T> a) { return a; }
And(AbstractWrappedConstraintUP a)1537 AbstractWrappedConstraintUP And(AbstractWrappedConstraintUP a) { return a; }
1538
1539 template<typename T, typename... Args>
And(OptionValueConstraintUP<T> a,Args...args)1540 OptionValueConstraintUP<T> And(OptionValueConstraintUP<T> a, Args... args)
1541 {
1542 OptionValueConstraintUP<T> r = maybe_unwrap<T>(And(std::move(args)...));
1543 return OptionValueConstraintUP<T>(new OptionValueConstraintAndWrapper<T>(std::move(a),std::move(r)));
1544 }
1545
1546 template<typename... Args>
And(AbstractWrappedConstraintUP a,Args...args)1547 AbstractWrappedConstraintUP And(AbstractWrappedConstraintUP a, Args... args)
1548 {
1549 AbstractWrappedConstraintUP r = And(std::move(args)...);
1550 return AbstractWrappedConstraintUP(new WrappedConstraintAndWrapper(std::move(a),std::move(r)));
1551 }
1552
1553 template<typename T>
1554 struct Equal : public OptionValueConstraint<T>{
1555 CLASS_NAME(Equal);
1556 USE_ALLOCATOR(Equal);
EqualShell::Options::Equal1557 Equal(T gv) : _goodvalue(gv) {}
checkShell::Options::Equal1558 bool check(const OptionValue<T>& value){
1559 return value.actualValue == _goodvalue;
1560 }
msgShell::Options::Equal1561 vstring msg(const OptionValue<T>& value){
1562 return value.longName+"("+value.getStringOfActual()+") is equal to " + value.getStringOfValue(_goodvalue);
1563 }
1564 T _goodvalue;
1565 };
1566 template<typename T>
equal(T bv)1567 static OptionValueConstraintUP<T> equal(T bv){
1568 return OptionValueConstraintUP<T>(new Equal<T>(bv));
1569 }
1570
1571 template<typename T>
1572 struct NotEqual : public OptionValueConstraint<T>{
1573 CLASS_NAME(NotEqual);
1574 USE_ALLOCATOR(NotEqual);
NotEqualShell::Options::NotEqual1575 NotEqual(T bv) : _badvalue(bv) {}
checkShell::Options::NotEqual1576 bool check(const OptionValue<T>& value){
1577 return value.actualValue != _badvalue;
1578 }
msgShell::Options::NotEqual1579 vstring msg(const OptionValue<T>& value){ return value.longName+"("+value.getStringOfActual()+") is not equal to " + value.getStringOfValue(_badvalue); }
1580 T _badvalue;
1581 };
1582 template<typename T>
notEqual(T bv)1583 static OptionValueConstraintUP<T> notEqual(T bv){
1584 return OptionValueConstraintUP<T>(new NotEqual<T>(bv));
1585 }
1586
1587 // Constraint that the value should be less than a given value
1588 // optionally we can allow it be equal to that value also
1589 template<typename T>
1590 struct LessThan : public OptionValueConstraint<T>{
1591 CLASS_NAME(LessThan);
1592 USE_ALLOCATOR(LessThan);
LessThanShell::Options::LessThan1593 LessThan(T gv,bool eq=false) : _goodvalue(gv), _orequal(eq) {}
checkShell::Options::LessThan1594 bool check(const OptionValue<T>& value){
1595 return (value.actualValue < _goodvalue || (_orequal && value.actualValue==_goodvalue));
1596 }
msgShell::Options::LessThan1597 vstring msg(const OptionValue<T>& value){
1598 if(_orequal) return value.longName+"("+value.getStringOfActual()+") is less than or equal to " + value.getStringOfValue(_goodvalue);
1599 return value.longName+"("+value.getStringOfActual()+") is less than "+ value.getStringOfValue(_goodvalue);
1600 }
1601
1602 T _goodvalue;
1603 bool _orequal;
1604 };
1605 template<typename T>
lessThan(T bv)1606 static OptionValueConstraintUP<T> lessThan(T bv){
1607 return OptionValueConstraintUP<T>(new LessThan<T>(bv,false));
1608 }
1609 template<typename T>
lessThanEq(T bv)1610 static OptionValueConstraintUP<T> lessThanEq(T bv){
1611 return OptionValueConstraintUP<T>(new LessThan<T>(bv,true));
1612 }
1613
1614 // Constraint that the value should be greater than a given value
1615 // optionally we can allow it be equal to that value also
1616 template<typename T>
1617 struct GreaterThan : public OptionValueConstraint<T>{
1618 CLASS_NAME(GreaterThan);
1619 USE_ALLOCATOR(GreaterThan);
GreaterThanShell::Options::GreaterThan1620 GreaterThan(T gv,bool eq=false) : _goodvalue(gv), _orequal(eq) {}
checkShell::Options::GreaterThan1621 bool check(const OptionValue<T>& value){
1622 return (value.actualValue > _goodvalue || (_orequal && value.actualValue==_goodvalue));
1623 }
1624
msgShell::Options::GreaterThan1625 vstring msg(const OptionValue<T>& value){
1626 if(_orequal) return value.longName+"("+value.getStringOfActual()+") is greater than or equal to " + value.getStringOfValue(_goodvalue);
1627 return value.longName+"("+value.getStringOfActual()+") is greater than "+ value.getStringOfValue(_goodvalue);
1628 }
1629
1630 T _goodvalue;
1631 bool _orequal;
1632 };
1633 template<typename T>
greaterThan(T bv)1634 static OptionValueConstraintUP<T> greaterThan(T bv){
1635 return OptionValueConstraintUP<T>(new GreaterThan<T>(bv,false));
1636 }
1637 template<typename T>
greaterThanEq(T bv)1638 static OptionValueConstraintUP<T> greaterThanEq(T bv){
1639 return OptionValueConstraintUP<T>(new GreaterThan<T>(bv,true));
1640 }
1641
1642 /**
1643 * If constraints
1644 */
1645
1646 template<typename T>
1647 struct IfConstraint;
1648
1649 template<typename T>
1650 struct IfThenConstraint : public OptionValueConstraint<T>{
1651 CLASS_NAME(IfThenConstraint);
1652 USE_ALLOCATOR(IfThenConstraint);
1653
IfThenConstraintShell::Options::IfThenConstraint1654 IfThenConstraint(OptionValueConstraintUP<T> ic, OptionValueConstraintUP<T> c) :
1655 if_con(std::move(ic)), then_con(std::move(c)) {}
1656
checkShell::Options::IfThenConstraint1657 bool check(const OptionValue<T>& value){
1658 ASS(then_con);
1659 return !if_con->check(value) || then_con->check(value);
1660 }
1661
msgShell::Options::IfThenConstraint1662 vstring msg(const OptionValue<T>& value){
1663 return "if "+if_con->msg(value)+" then "+ then_con->msg(value);
1664 }
1665
1666 OptionValueConstraintUP<T> if_con;
1667 OptionValueConstraintUP<T> then_con;
1668 };
1669
1670 template<typename T>
1671 struct IfConstraint {
1672 CLASS_NAME(IfConstraint);
1673 USE_ALLOCATOR(IfConstraint);
IfConstraintShell::Options::IfConstraint1674 IfConstraint(OptionValueConstraintUP<T> c) :if_con(std::move(c)) {}
1675
thenShell::Options::IfConstraint1676 OptionValueConstraintUP<T> then(OptionValueConstraintUP<T> c){
1677 return OptionValueConstraintUP<T>(new IfThenConstraint<T>(std::move(if_con),std::move(c)));
1678 }
thenShell::Options::IfConstraint1679 OptionValueConstraintUP<T> then(AbstractWrappedConstraintUP c){
1680 return OptionValueConstraintUP<T>(new IfThenConstraint<T>(std::move(if_con),unwrap<T>(c)));
1681 }
1682
1683 OptionValueConstraintUP<T> if_con;
1684 };
1685
1686 template<typename T>
If(OptionValueConstraintUP<T> c)1687 static IfConstraint<T> If(OptionValueConstraintUP<T> c){
1688 return IfConstraint<T>(std::move(c));
1689 }
1690 template<typename T>
If(AbstractWrappedConstraintUP c)1691 static IfConstraint<T> If(AbstractWrappedConstraintUP c){
1692 return IfConstraint<T>(unwrap<T>(c));
1693 }
1694
1695 /**
1696 * Default Value constraints
1697 */
1698
1699 template<typename T>
1700 struct NotDefaultConstraint : public OptionValueConstraint<T> {
NotDefaultConstraintShell::Options::NotDefaultConstraint1701 NotDefaultConstraint() {}
1702
checkShell::Options::NotDefaultConstraint1703 bool check(const OptionValue<T>& value){
1704 return value.defaultValue != value.actualValue;
1705 }
msgShell::Options::NotDefaultConstraint1706 vstring msg(const OptionValue<T>& value) { return value.longName+"("+value.getStringOfActual()+") is not default("+value.getStringOfValue(value.defaultValue)+")";}
1707 };
1708 struct NotDefaultRatioConstraint : public OptionValueConstraint<int> {
NotDefaultRatioConstraintShell::Options::NotDefaultRatioConstraint1709 NotDefaultRatioConstraint() {}
1710
checkShell::Options::NotDefaultRatioConstraint1711 bool check(const OptionValue<int>& value){
1712 const RatioOptionValue& rvalue = static_cast<const RatioOptionValue&>(value);
1713 return (rvalue.defaultValue != rvalue.actualValue ||
1714 rvalue.defaultOtherValue != rvalue.otherValue);
1715 }
msgShell::Options::NotDefaultRatioConstraint1716 vstring msg(const OptionValue<int>& value) { return value.longName+"("+value.getStringOfActual()+") is not default";}
1717
1718 };
1719
1720 // You will need to provide the type, optionally use addConstraintIfNotDefault
1721 template<typename T>
isNotDefault()1722 static OptionValueConstraintUP<T> isNotDefault(){
1723 return OptionValueConstraintUP<T>(new NotDefaultConstraint<T>());
1724 }
1725 // You will need to provide the type, optionally use addConstraintIfNotDefault
isNotDefaultRatio()1726 static OptionValueConstraintUP<int> isNotDefaultRatio(){
1727 return OptionValueConstraintUP<int>(new NotDefaultRatioConstraint());
1728 }
1729
1730 struct isLookAheadSelectionConstraint : public OptionValueConstraint<int>{
1731 CLASS_NAME(isLookAheadSelectionConstraint);
1732 USE_ALLOCATOR(isLookAheadSelectionConstraint);
isLookAheadSelectionConstraintShell::Options::isLookAheadSelectionConstraint1733 isLookAheadSelectionConstraint() {}
checkShell::Options::isLookAheadSelectionConstraint1734 bool check(const OptionValue<int>& value){
1735 return value.actualValue == 11 || value.actualValue == 1011 || value.actualValue == -11 || value.actualValue == -1011;
1736 }
msgShell::Options::isLookAheadSelectionConstraint1737 vstring msg(const OptionValue<int>& value){
1738 return value.longName+"("+value.getStringOfActual()+") is not lookahead selection";
1739 }
1740 };
1741
1742
1743 /**
1744 * NOTE on OptionProblemConstraint
1745 *
1746 * OptionProblemConstraints are used to capture properties of a problem that
1747 * should be present when an option is used. The idea being that a warning will
1748 * be emitted if an option is used for an inappropriate problem.
1749 *
1750 * TODO - this element of Options is still under development
1751 */
1752
1753 struct OptionProblemConstraint{
1754 virtual bool check(Property* p) = 0;
1755 virtual vstring msg() = 0;
~OptionProblemConstraintShell::Options::OptionProblemConstraint1756 virtual ~OptionProblemConstraint() {};
1757 };
1758
1759 struct CategoryCondition : OptionProblemConstraint{
CategoryConditionShell::Options::CategoryCondition1760 CategoryCondition(Property::Category c,bool h) : cat(c), has(h) {}
checkShell::Options::CategoryCondition1761 bool check(Property*p){
1762 CALL("Options::CategoryCondition::check");
1763 ASS(p);
1764 return has ? p->category()==cat : p->category()!=cat;
1765 }
msgShell::Options::CategoryCondition1766 vstring msg(){
1767 vstring m =" not useful for property ";
1768 if(has) m+="not";
1769 return m+" in category "+Property::categoryToString(cat);
1770 }
1771 Property::Category cat;
1772 bool has;
1773 };
1774 struct UsesEquality : OptionProblemConstraint{
checkShell::Options::UsesEquality1775 bool check(Property*p){
1776 CALL("Options::UsesEquality::check");
1777 ASS(p)
1778 return (p->equalityAtoms() != 0);
1779 }
msgShell::Options::UsesEquality1780 vstring msg(){ return " only useful with equality"; }
1781 };
1782 struct HasNonUnits : OptionProblemConstraint{
checkShell::Options::HasNonUnits1783 bool check(Property*p){
1784 CALL("Options::HasNonUnits::check");
1785 return (p->clauses()-p->unitClauses())!=0;
1786 }
msgShell::Options::HasNonUnits1787 vstring msg(){ return " only useful with non-unit clauses"; }
1788 };
1789 struct HasPredicates : OptionProblemConstraint{
checkShell::Options::HasPredicates1790 bool check(Property*p){
1791 CALL("Options::HasPredicates::check");
1792 return (p->category()==Property::PEQ || p->category()==Property::UEQ);
1793 }
msgShell::Options::HasPredicates1794 vstring msg(){ return " only useful with predicates"; }
1795 };
1796 struct AtomConstraint : OptionProblemConstraint{
AtomConstraintShell::Options::AtomConstraint1797 AtomConstraint(int a,bool g) : atoms(a),greater(g) {}
1798 int atoms;
1799 bool greater;
checkShell::Options::AtomConstraint1800 bool check(Property*p){
1801 CALL("Options::AtomConstraint::check");
1802 return greater ? p->atoms()>atoms : p->atoms()<atoms;
1803 }
1804
msgShell::Options::AtomConstraint1805 vstring msg(){
1806 vstring m = " not with ";
1807 if(greater){ m+="more";}else{m+="less";}
1808 return m+" than "+Lib::Int::toString(atoms)+" atoms";
1809 }
1810 };
1811
1812 // Factory methods
notWithCat(Property::Category c)1813 static OptionProblemConstraintUP notWithCat(Property::Category c){
1814 return OptionProblemConstraintUP(new CategoryCondition(c,false));
1815 }
hasCat(Property::Category c)1816 static OptionProblemConstraintUP hasCat(Property::Category c){
1817 return OptionProblemConstraintUP(new CategoryCondition(c,true));
1818 }
hasEquality()1819 static OptionProblemConstraintUP hasEquality(){ return OptionProblemConstraintUP(new UsesEquality); }
hasNonUnits()1820 static OptionProblemConstraintUP hasNonUnits(){ return OptionProblemConstraintUP(new HasNonUnits); }
hasPredicates()1821 static OptionProblemConstraintUP hasPredicates(){ return OptionProblemConstraintUP(new HasPredicates); }
atomsMoreThan(int a)1822 static OptionProblemConstraintUP atomsMoreThan(int a){
1823 return OptionProblemConstraintUP(new AtomConstraint(a,true));
1824 }
atomsLessThan(int a)1825 static OptionProblemConstraintUP atomsLessThan(int a){
1826 return OptionProblemConstraintUP(new AtomConstraint(a,false));
1827 }
1828
1829
1830 //Cheating - we refer to env.options to ask about option values
1831 // There is an assumption that the option values used have been
1832 // set to their final values
1833 // These are used in randomisation where we guarantee a certain
1834 // set of options will not be randomized and some will be randomized first
1835
1836 struct OptionHasValue : OptionProblemConstraint{
OptionHasValueShell::Options::OptionHasValue1837 OptionHasValue(vstring ov,vstring v) : option_value(ov),value(v) {}
1838 bool check(Property*p);
msgShell::Options::OptionHasValue1839 vstring msg(){ return option_value+" has value "+value; }
1840 vstring option_value;
1841 vstring value;
1842 };
1843
1844 struct ManyOptionProblemConstraints : OptionProblemConstraint {
ManyOptionProblemConstraintsShell::Options::ManyOptionProblemConstraints1845 ManyOptionProblemConstraints(bool a) : is_and(a) {}
1846
checkShell::Options::ManyOptionProblemConstraints1847 bool check(Property*p){
1848 CALL("Options::ManyOptionProblemConstraints::check");
1849 bool res = is_and;
1850 Stack<OptionProblemConstraintUP>::Iterator it(cons);
1851 while(it.hasNext()){
1852 bool n=it.next()->check(p);res = is_and ? (res && n) : (res || n);}
1853 return res;
1854 }
1855
msgShell::Options::ManyOptionProblemConstraints1856 vstring msg(){
1857 vstring res="";
1858 Stack<OptionProblemConstraintUP>::Iterator it(cons);
1859 if(it.hasNext()){ res=it.next()->msg();}
1860 while(it.hasNext()){ res+=",and\n"+it.next()->msg();}
1861 return res;
1862 }
1863
addShell::Options::ManyOptionProblemConstraints1864 void add(OptionProblemConstraintUP& c){ cons.push(std::move(c));}
1865 Stack<OptionProblemConstraintUP> cons;
1866 bool is_and;
1867 };
1868
And(OptionProblemConstraintUP left,OptionProblemConstraintUP right)1869 static OptionProblemConstraintUP And(OptionProblemConstraintUP left,
1870 OptionProblemConstraintUP right){
1871 ManyOptionProblemConstraints* c = new ManyOptionProblemConstraints(true);
1872 c->add(left);c->add(right);
1873 return OptionProblemConstraintUP(c);
1874 }
And(OptionProblemConstraintUP left,OptionProblemConstraintUP mid,OptionProblemConstraintUP right)1875 static OptionProblemConstraintUP And(OptionProblemConstraintUP left,
1876 OptionProblemConstraintUP mid,
1877 OptionProblemConstraintUP right){
1878 ManyOptionProblemConstraints* c = new ManyOptionProblemConstraints(true);
1879 c->add(left);c->add(mid);c->add(right);
1880 return OptionProblemConstraintUP(c);
1881 }
Or(OptionProblemConstraintUP left,OptionProblemConstraintUP right)1882 static OptionProblemConstraintUP Or(OptionProblemConstraintUP left,
1883 OptionProblemConstraintUP right){
1884 ManyOptionProblemConstraints* c = new ManyOptionProblemConstraints(false);
1885 c->add(left);c->add(right);
1886 return OptionProblemConstraintUP(c);
1887 }
Or(OptionProblemConstraintUP left,OptionProblemConstraintUP mid,OptionProblemConstraintUP right)1888 static OptionProblemConstraintUP Or(OptionProblemConstraintUP left,
1889 OptionProblemConstraintUP mid,
1890 OptionProblemConstraintUP right){
1891 ManyOptionProblemConstraints* c = new ManyOptionProblemConstraints(false);
1892 c->add(left);c->add(mid);c->add(right);
1893 return OptionProblemConstraintUP(c);
1894 }
1895
1896 static OptionProblemConstraintUP isRandOn();
1897 static OptionProblemConstraintUP isRandSat();
1898 static OptionProblemConstraintUP saNotInstGen();
1899 static OptionProblemConstraintUP isBfnt();
1900
1901 //==========================================================
1902 // Getter functions
1903 // -currently disabled all unnecessary setter functions
1904 //==========================================================
1905 //
1906 // This is how options are accessed so if you add a new option you should add a getter
1907 public:
encodeStrategy() const1908 bool encodeStrategy() const{ return _encode.actualValue;}
randomStrategy() const1909 RandomStrategy randomStrategy() const {return _randomStrategy.actualValue; }
setRandomStrategy(RandomStrategy newVal)1910 void setRandomStrategy(RandomStrategy newVal){ _randomStrategy.actualValue=newVal;}
getBadOptionChoice() const1911 BadOption getBadOptionChoice() const { return _badOption.actualValue; }
setBadOptionChoice(BadOption newVal)1912 void setBadOptionChoice(BadOption newVal) { _badOption.actualValue = newVal; }
forcedOptions() const1913 vstring forcedOptions() const { return _forcedOptions.actualValue; }
forbiddenOptions() const1914 vstring forbiddenOptions() const { return _forbiddenOptions.actualValue; }
testId() const1915 vstring testId() const { return _testId.actualValue; }
protectedPrefix() const1916 vstring protectedPrefix() const { return _protectedPrefix.actualValue; }
statistics() const1917 Statistics statistics() const { return _statistics.actualValue; }
setStatistics(Statistics newVal)1918 void setStatistics(Statistics newVal) { _statistics.actualValue=newVal; }
proof() const1919 Proof proof() const { return _proof.actualValue; }
minimizeSatProofs() const1920 bool minimizeSatProofs() const { return _minimizeSatProofs.actualValue; }
proofExtra() const1921 ProofExtra proofExtra() const { return _proofExtra.actualValue; }
proofChecking() const1922 bool proofChecking() const { return _proofChecking.actualValue; }
naming() const1923 int naming() const { return _naming.actualValue; }
1924
fmbNonGroundDefs() const1925 bool fmbNonGroundDefs() const { return _fmbNonGroundDefs.actualValue; }
fmbStartSize() const1926 unsigned fmbStartSize() const { return _fmbStartSize.actualValue;}
fmbSymmetryRatio() const1927 float fmbSymmetryRatio() const { return _fmbSymmetryRatio.actualValue; }
fmbSymmetryWidgetOrders()1928 FMBWidgetOrders fmbSymmetryWidgetOrders() { return _fmbSymmetryWidgetOrders.actualValue;}
fmbSymmetryOrderSymbols() const1929 FMBSymbolOrders fmbSymmetryOrderSymbols() const {return _fmbSymmetryOrderSymbols.actualValue; }
fmbAdjustSorts() const1930 FMBAdjustSorts fmbAdjustSorts() const {return _fmbAdjustSorts.actualValue; }
fmbDetectSortBounds() const1931 bool fmbDetectSortBounds() const { return _fmbDetectSortBounds.actualValue; }
fmbDetectSortBoundsTimeLimit() const1932 unsigned fmbDetectSortBoundsTimeLimit() const { return _fmbDetectSortBoundsTimeLimit.actualValue; }
fmbSizeWeightRatio() const1933 unsigned fmbSizeWeightRatio() const { return _fmbSizeWeightRatio.actualValue; }
fmbEnumerationStrategy() const1934 FMBEnumerationStrategy fmbEnumerationStrategy() const { return _fmbEnumerationStrategy.actualValue; }
1935
flattenTopLevelConjunctions() const1936 bool flattenTopLevelConjunctions() const { return _flattenTopLevelConjunctions.actualValue; }
ltbLearning() const1937 LTBLearning ltbLearning() const { return _ltbLearning.actualValue; }
ltbDirectory() const1938 vstring ltbDirectory() const { return _ltbDirectory.actualValue; }
mode() const1939 Mode mode() const { return _mode.actualValue; }
schedule() const1940 Schedule schedule() const { return _schedule.actualValue; }
scheduleName() const1941 vstring scheduleName() const { return _schedule.getStringOfValue(_schedule.actualValue); }
setSchedule(Schedule newVal)1942 void setSchedule(Schedule newVal) { _schedule.actualValue = newVal; }
multicore() const1943 unsigned multicore() const { return _multicore.actualValue; }
setMulticore(unsigned newVal)1944 void setMulticore(unsigned newVal) { _multicore.actualValue = newVal; }
inputSyntax() const1945 InputSyntax inputSyntax() const { return _inputSyntax.actualValue; }
setInputSyntax(InputSyntax newVal)1946 void setInputSyntax(InputSyntax newVal) { _inputSyntax.actualValue = newVal; }
normalize() const1947 bool normalize() const { return _normalize.actualValue; }
setNormalize(bool normalize)1948 void setNormalize(bool normalize) { _normalize.actualValue = normalize; }
guessTheGoal() const1949 GoalGuess guessTheGoal() const { return _guessTheGoal.actualValue; }
gtgLimit() const1950 unsigned gtgLimit() const { return _guessTheGoalLimit.actualValue; }
1951
setNaming(int n)1952 void setNaming(int n){ _naming.actualValue = n;} //TODO: ensure global constraints
include() const1953 vstring include() const { return _include.actualValue; }
setInclude(vstring val)1954 void setInclude(vstring val) { _include.actualValue = val; }
logFile() const1955 vstring logFile() const { return _logFile.actualValue; }
inputFile() const1956 vstring inputFile() const { return _inputFile.actualValue; }
activationLimit() const1957 int activationLimit() const { return _activationLimit.actualValue; }
randomSeed() const1958 int randomSeed() const { return _randomSeed.actualValue; }
printClausifierPremises() const1959 bool printClausifierPremises() const { return _printClausifierPremises.actualValue; }
1960
1961 // IMPORTANT, if you add a showX command then include showAll
showAll() const1962 bool showAll() const { return _showAll.actualValue; }
showActive() const1963 bool showActive() const { return showAll() || _showActive.actualValue; }
showBlocked() const1964 bool showBlocked() const { return showAll() || _showBlocked.actualValue; }
showDefinitions() const1965 bool showDefinitions() const { return showAll() || _showDefinitions.actualValue; }
showNew() const1966 bool showNew() const { return showAll() || _showNew.actualValue; }
sineToAge() const1967 bool sineToAge() const { return _sineToAge.actualValue; }
sineToPredLevels() const1968 PredicateSineLevels sineToPredLevels() const { return _sineToPredLevels.actualValue; }
showSplitting() const1969 bool showSplitting() const { return showAll() || _showSplitting.actualValue; }
showNewPropositional() const1970 bool showNewPropositional() const { return showAll() || _showNewPropositional.actualValue; }
showPassive() const1971 bool showPassive() const { return showAll() || _showPassive.actualValue; }
showReductions() const1972 bool showReductions() const { return showAll() || _showReductions.actualValue; }
showPreprocessing() const1973 bool showPreprocessing() const { return showAll() || _showPreprocessing.actualValue; }
showSkolemisations() const1974 bool showSkolemisations() const { return showAll() || _showSkolemisations.actualValue; }
showSymbolElimination() const1975 bool showSymbolElimination() const { return showAll() || _showSymbolElimination.actualValue; }
showTheoryAxioms() const1976 bool showTheoryAxioms() const { return showAll() || _showTheoryAxioms.actualValue; }
showFOOL() const1977 bool showFOOL() const { return showAll() || _showFOOL.actualValue; }
showFMBsortInfo() const1978 bool showFMBsortInfo() const { return showAll() || _showFMBsortInfo.actualValue; }
showInduction() const1979 bool showInduction() const { return showAll() || _showInduction.actualValue; }
1980 #if VZ3
showZ3() const1981 bool showZ3() const { return showAll() || _showZ3.actualValue; }
1982 #endif
1983
1984 // end of show commands
1985
showNonconstantSkolemFunctionTrace() const1986 bool showNonconstantSkolemFunctionTrace() const { return _showNonconstantSkolemFunctionTrace.actualValue; }
setShowNonconstantSkolemFunctionTrace(bool newVal)1987 void setShowNonconstantSkolemFunctionTrace(bool newVal) { _showNonconstantSkolemFunctionTrace.actualValue = newVal; }
showInterpolant() const1988 InterpolantMode showInterpolant() const { return _showInterpolant.actualValue; }
showOptions() const1989 bool showOptions() const { return _showOptions.actualValue; }
lineWrapInShowOptions() const1990 bool lineWrapInShowOptions() const { return _showOptionsLineWrap.actualValue; }
showExperimentalOptions() const1991 bool showExperimentalOptions() const { return _showExperimentalOptions.actualValue; }
showHelp() const1992 bool showHelp() const { return _showHelp.actualValue; }
explainOption() const1993 vstring explainOption() const { return _explainOption.actualValue; }
1994
printAllTheoryAxioms() const1995 bool printAllTheoryAxioms() const { return _printAllTheoryAxioms.actualValue; }
1996
1997 #if VZ3
z3UnsatCores() const1998 bool z3UnsatCores() const { return _z3UnsatCores.actualValue;}
satFallbackForSMT() const1999 bool satFallbackForSMT() const { return _satFallbackForSMT.actualValue; }
smtForGround() const2000 bool smtForGround() const { return _smtForGround.actualValue; }
theoryInstAndSimp() const2001 TheoryInstSimp theoryInstAndSimp() const { return _theoryInstAndSimp.actualValue; }
2002 #endif
unificationWithAbstraction() const2003 UnificationWithAbstraction unificationWithAbstraction() const { return _unificationWithAbstraction.actualValue; }
setUWA(UnificationWithAbstraction value)2004 void setUWA(UnificationWithAbstraction value){ _unificationWithAbstraction.actualValue = value; }
fixUWA() const2005 bool fixUWA() const { return _fixUWA.actualValue; }
useACeval() const2006 bool useACeval() const { return _useACeval.actualValue;}
2007
unusedPredicateDefinitionRemoval() const2008 bool unusedPredicateDefinitionRemoval() const { return _unusedPredicateDefinitionRemoval.actualValue; }
blockedClauseElimination() const2009 bool blockedClauseElimination() const { return _blockedClauseElimination.actualValue; }
setUnusedPredicateDefinitionRemoval(bool newVal)2010 void setUnusedPredicateDefinitionRemoval(bool newVal) { _unusedPredicateDefinitionRemoval.actualValue = newVal; }
weightIncrement() const2011 bool weightIncrement() const { return _weightIncrement.actualValue; }
2012 // bool useDM() const { return _use_dm.actualValue; }
satSolver() const2013 SatSolver satSolver() const { return _satSolver.actualValue; }
2014 //void setSatSolver(SatSolver newVal) { _satSolver = newVal; }
saturationAlgorithm() const2015 SaturationAlgorithm saturationAlgorithm() const { return _saturationAlgorithm.actualValue; }
setSaturationAlgorithm(SaturationAlgorithm newVal)2016 void setSaturationAlgorithm(SaturationAlgorithm newVal) { _saturationAlgorithm.actualValue = newVal; }
selection() const2017 int selection() const { return _selection.actualValue; }
setSelection(int v)2018 void setSelection(int v) { _selection.actualValue=v;}
latexOutput() const2019 vstring latexOutput() const { return _latexOutput.actualValue; }
latexUseDefault() const2020 bool latexUseDefault() const { return _latexUseDefaultSymbols.actualValue; }
literalComparisonMode() const2021 LiteralComparisonMode literalComparisonMode() const { return _literalComparisonMode.actualValue; }
forwardSubsumptionResolution() const2022 bool forwardSubsumptionResolution() const { return _forwardSubsumptionResolution.actualValue; }
2023 //void setForwardSubsumptionResolution(bool newVal) { _forwardSubsumptionResolution = newVal; }
forwardSubsumptionDemodulation() const2024 bool forwardSubsumptionDemodulation() const { return _forwardSubsumptionDemodulation.actualValue; }
forwardSubsumptionDemodulationMaxMatches() const2025 unsigned forwardSubsumptionDemodulationMaxMatches() const { return _forwardSubsumptionDemodulationMaxMatches.actualValue; }
forwardDemodulation() const2026 Demodulation forwardDemodulation() const { return _forwardDemodulation.actualValue; }
binaryResolution() const2027 bool binaryResolution() const { return _binaryResolution.actualValue; }
bfnt() const2028 bool bfnt() const { return _bfnt.actualValue; }
setBfnt(bool newVal)2029 void setBfnt(bool newVal) { _bfnt.actualValue = newVal; }
unitResultingResolution() const2030 URResolution unitResultingResolution() const { return _unitResultingResolution.actualValue; }
hyperSuperposition() const2031 bool hyperSuperposition() const { return _hyperSuperposition.actualValue; }
simulatenousSuperposition() const2032 bool simulatenousSuperposition() const { return _simultaneousSuperposition.actualValue; }
innerRewriting() const2033 bool innerRewriting() const { return _innerRewriting.actualValue; }
equationalTautologyRemoval() const2034 bool equationalTautologyRemoval() const { return _equationalTautologyRemoval.actualValue; }
arityCheck() const2035 bool arityCheck() const { return _arityCheck.actualValue; }
2036 //void setArityCheck(bool newVal) { _arityCheck=newVal; }
backwardDemodulation() const2037 Demodulation backwardDemodulation() const { return _backwardDemodulation.actualValue; }
demodulationRedundancyCheck() const2038 bool demodulationRedundancyCheck() const { return _demodulationRedundancyCheck.actualValue; }
2039 //void setBackwardDemodulation(Demodulation newVal) { _backwardDemodulation = newVal; }
backwardSubsumption() const2040 Subsumption backwardSubsumption() const { return _backwardSubsumption.actualValue; }
2041 //void setBackwardSubsumption(Subsumption newVal) { _backwardSubsumption = newVal; }
backwardSubsumptionResolution() const2042 Subsumption backwardSubsumptionResolution() const { return _backwardSubsumptionResolution.actualValue; }
backwardSubsumptionDemodulation() const2043 bool backwardSubsumptionDemodulation() const { return _backwardSubsumptionDemodulation.actualValue; }
backwardSubsumptionDemodulationMaxMatches() const2044 unsigned backwardSubsumptionDemodulationMaxMatches() const { return _backwardSubsumptionDemodulationMaxMatches.actualValue; }
forwardSubsumption() const2045 bool forwardSubsumption() const { return _forwardSubsumption.actualValue; }
forwardLiteralRewriting() const2046 bool forwardLiteralRewriting() const { return _forwardLiteralRewriting.actualValue; }
lrsFirstTimeCheck() const2047 int lrsFirstTimeCheck() const { return _lrsFirstTimeCheck.actualValue; }
lrsWeightLimitOnly() const2048 int lrsWeightLimitOnly() const { return _lrsWeightLimitOnly.actualValue; }
lookaheadDelay() const2049 int lookaheadDelay() const { return _lookaheadDelay.actualValue; }
simulatedTimeLimit() const2050 int simulatedTimeLimit() const { return _simulatedTimeLimit.actualValue; }
setSimulatedTimeLimit(int newVal)2051 void setSimulatedTimeLimit(int newVal) { _simulatedTimeLimit.actualValue = newVal; }
maxInferenceDepth() const2052 int maxInferenceDepth() const { return _maxInferenceDepth.actualValue; }
termOrdering() const2053 TermOrdering termOrdering() const { return _termOrdering.actualValue; }
symbolPrecedence() const2054 SymbolPrecedence symbolPrecedence() const { return _symbolPrecedence.actualValue; }
symbolPrecedenceBoost() const2055 SymbolPrecedenceBoost symbolPrecedenceBoost() const { return _symbolPrecedenceBoost.actualValue; }
introducedSymbolPrecedence() const2056 IntroducedSymbolPrecedence introducedSymbolPrecedence() const { return _introducedSymbolPrecedence.actualValue; }
functionPrecedence() const2057 const vstring& functionPrecedence() const { return _functionPrecedence.actualValue; }
predicatePrecedence() const2058 const vstring& predicatePrecedence() const { return _predicatePrecedence.actualValue; }
2059 // Return time limit in deciseconds, or 0 if there is no time limit
timeLimitInDeciseconds() const2060 int timeLimitInDeciseconds() const { return _timeLimitInDeciseconds.actualValue; }
memoryLimit() const2061 size_t memoryLimit() const { return _memoryLimit.actualValue; }
inequalitySplitting() const2062 int inequalitySplitting() const { return _inequalitySplitting.actualValue; }
maxActive() const2063 long maxActive() const { return _maxActive.actualValue; }
maxAnswers() const2064 long maxAnswers() const { return _maxAnswers.actualValue; }
2065 //void setMaxAnswers(int newVal) { _maxAnswers = newVal; }
maxPassive() const2066 long maxPassive() const { return _maxPassive.actualValue; }
ageRatio() const2067 int ageRatio() const { return _ageWeightRatio.actualValue; }
setAgeRatio(int v)2068 void setAgeRatio(int v){ _ageWeightRatio.actualValue = v; }
weightRatio() const2069 int weightRatio() const { return _ageWeightRatio.otherValue; }
useTheorySplitQueues() const2070 bool useTheorySplitQueues() const { return _useTheorySplitQueues.actualValue; }
2071 Lib::vvector<int> theorySplitQueueRatios() const;
2072 Lib::vvector<float> theorySplitQueueCutoffs() const;
theorySplitQueueExpectedRatioDenom() const2073 int theorySplitQueueExpectedRatioDenom() const { return _theorySplitQueueExpectedRatioDenom.actualValue; }
theorySplitQueueLayeredArrangement() const2074 bool theorySplitQueueLayeredArrangement() const { return _theorySplitQueueLayeredArrangement.actualValue; }
useAvatarSplitQueues() const2075 bool useAvatarSplitQueues() const { return _useAvatarSplitQueues.actualValue; }
2076 Lib::vvector<int> avatarSplitQueueRatios() const;
2077 Lib::vvector<float> avatarSplitQueueCutoffs() const;
avatarSplitQueueLayeredArrangement() const2078 bool avatarSplitQueueLayeredArrangement() const { return _avatarSplitQueueLayeredArrangement.actualValue; }
useSineLevelSplitQueues() const2079 bool useSineLevelSplitQueues() const { return _useSineLevelSplitQueues.actualValue; }
2080 Lib::vvector<int> sineLevelSplitQueueRatios() const;
2081 Lib::vvector<float> sineLevelSplitQueueCutoffs() const;
sineLevelSplitQueueLayeredArrangement() const2082 bool sineLevelSplitQueueLayeredArrangement() const { return _sineLevelSplitQueueLayeredArrangement.actualValue; }
usePositiveLiteralSplitQueues() const2083 bool usePositiveLiteralSplitQueues() const { return _usePositiveLiteralSplitQueues.actualValue; }
2084 Lib::vvector<int> positiveLiteralSplitQueueRatios() const;
2085 Lib::vvector<float> positiveLiteralSplitQueueCutoffs() const;
positiveLiteralSplitQueueLayeredArrangement() const2086 bool positiveLiteralSplitQueueLayeredArrangement() const { return _positiveLiteralSplitQueueLayeredArrangement.actualValue; }
setWeightRatio(int v)2087 void setWeightRatio(int v){ _ageWeightRatio.otherValue = v; }
ageWeightRatioShape() const2088 AgeWeightRatioShape ageWeightRatioShape() const { return _ageWeightRatioShape.actualValue; }
ageWeightRatioShapeFrequency() const2089 int ageWeightRatioShapeFrequency() const { return _ageWeightRatioShapeFrequency.actualValue; }
literalMaximalityAftercheck() const2090 bool literalMaximalityAftercheck() const { return _literalMaximalityAftercheck.actualValue; }
superpositionFromVariables() const2091 bool superpositionFromVariables() const { return _superpositionFromVariables.actualValue; }
equalityProxy() const2092 EqualityProxy equalityProxy() const { return _equalityProxy.actualValue; }
equalityResolutionWithDeletion() const2093 RuleActivity equalityResolutionWithDeletion() const { return _equalityResolutionWithDeletion.actualValue; }
extensionalityResolution() const2094 ExtensionalityResolution extensionalityResolution() const { return _extensionalityResolution.actualValue; }
FOOLParamodulation() const2095 bool FOOLParamodulation() const { return _FOOLParamodulation.actualValue; }
termAlgebraInferences() const2096 bool termAlgebraInferences() const { return _termAlgebraInferences.actualValue; }
termAlgebraCyclicityCheck() const2097 TACyclicityCheck termAlgebraCyclicityCheck() const { return _termAlgebraCyclicityCheck.actualValue; }
extensionalityMaxLength() const2098 unsigned extensionalityMaxLength() const { return _extensionalityMaxLength.actualValue; }
extensionalityAllowPosEq() const2099 bool extensionalityAllowPosEq() const { return _extensionalityAllowPosEq.actualValue; }
nongoalWeightCoefficientNumerator() const2100 unsigned nongoalWeightCoefficientNumerator() const { return _nonGoalWeightCoefficient.numerator; }
nongoalWeightCoefficientDenominator() const2101 unsigned nongoalWeightCoefficientDenominator() const { return _nonGoalWeightCoefficient.denominator; }
restrictNWCtoGC() const2102 bool restrictNWCtoGC() const { return _restrictNWCtoGC.actualValue; }
sos() const2103 Sos sos() const { return _sos.actualValue; }
sosTheoryLimit() const2104 unsigned sosTheoryLimit() const { return _sosTheoryLimit.actualValue; }
2105 //void setSos(Sos newVal) { _sos = newVal; }
2106
ignoreConjectureInPreprocessing() const2107 bool ignoreConjectureInPreprocessing() const {return _ignoreConjectureInPreprocessing.actualValue;}
2108
functionDefinitionElimination() const2109 FunctionDefinitionElimination functionDefinitionElimination() const { return _functionDefinitionElimination.actualValue; }
outputAxiomNames() const2110 bool outputAxiomNames() const { return _outputAxiomNames.actualValue; }
setOutputAxiomNames(bool newVal)2111 void setOutputAxiomNames(bool newVal) { _outputAxiomNames.actualValue = newVal; }
questionAnswering() const2112 QuestionAnsweringMode questionAnswering() const { return _questionAnswering.actualValue; }
xmlOutput() const2113 vstring xmlOutput() const { return _xmlOutput.actualValue; }
outputMode() const2114 Output outputMode() const { return _outputMode.actualValue; }
setOutputMode(Output newVal)2115 void setOutputMode(Output newVal) { _outputMode.actualValue = newVal; }
thanks() const2116 vstring thanks() const { return _thanks.actualValue; }
setQuestionAnswering(QuestionAnsweringMode newVal)2117 void setQuestionAnswering(QuestionAnsweringMode newVal) { _questionAnswering.actualValue = newVal; }
globalSubsumption() const2118 bool globalSubsumption() const { return _globalSubsumption.actualValue; }
globalSubsumptionSatSolverPower() const2119 GlobalSubsumptionSatSolverPower globalSubsumptionSatSolverPower() const { return _globalSubsumptionSatSolverPower.actualValue; }
globalSubsumptionExplicitMinim() const2120 GlobalSubsumptionExplicitMinim globalSubsumptionExplicitMinim() const { return _globalSubsumptionExplicitMinim.actualValue; }
globalSubsumptionAvatarAssumptions() const2121 GlobalSubsumptionAvatarAssumptions globalSubsumptionAvatarAssumptions() const { return _globalSubsumptionAvatarAssumptions.actualValue; }
2122
2123 /** true if calling set() on non-existing options does not result in a user error */
ignoreMissing() const2124 IgnoreMissing ignoreMissing() const { return _ignoreMissing.actualValue; }
setIgnoreMissing(IgnoreMissing newVal)2125 void setIgnoreMissing(IgnoreMissing newVal) { _ignoreMissing.actualValue = newVal; }
increasedNumeralWeight() const2126 bool increasedNumeralWeight() const { return _increasedNumeralWeight.actualValue; }
theoryAxioms() const2127 TheoryAxiomLevel theoryAxioms() const { return _theoryAxioms.actualValue; }
2128 //void setTheoryAxioms(bool newValue) { _theoryAxioms = newValue; }
interpretedSimplification() const2129 bool interpretedSimplification() const { return _interpretedSimplification.actualValue; }
2130 //void setInterpretedSimplification(bool val) { _interpretedSimplification = val; }
condensation() const2131 Condensation condensation() const { return _condensation.actualValue; }
generalSplitting() const2132 RuleActivity generalSplitting() const { return _generalSplitting.actualValue; }
2133 //vstring namePrefix() const { return _namePrefix.actualValue; }
timeStatistics() const2134 bool timeStatistics() const { return _timeStatistics.actualValue; }
splitting() const2135 bool splitting() const { return _splitting.actualValue; }
setSplitting(bool value)2136 void setSplitting(bool value){ _splitting.actualValue=value; }
nonliteralsInClauseWeight() const2137 bool nonliteralsInClauseWeight() const { return _nonliteralsInClauseWeight.actualValue; }
sineDepth() const2138 unsigned sineDepth() const { return _sineDepth.actualValue; }
sineGeneralityThreshold() const2139 unsigned sineGeneralityThreshold() const { return _sineGeneralityThreshold.actualValue; }
sineToAgeGeneralityThreshold() const2140