diff options
Diffstat (limited to 'src/options/arith_options.toml')
-rw-r--r-- | src/options/arith_options.toml | 46 |
1 files changed, 39 insertions, 7 deletions
diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 80403ee0d..ab8164130 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -7,11 +7,21 @@ header = "options/arith_options.h" category = "regular" long = "unate-lemmas=MODE" type = "ArithUnateLemmaMode" - default = "ALL_PRESOLVE_LEMMAS" - handler = "stringToArithUnateLemmaMode" - includes = ["options/arith_unate_lemma_mode.h"] + default = "ALL" read_only = true help = "determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)" + help_mode = "Unate lemmas are generated before SAT search begins using the relationship of constant terms and polynomials." +[[option.mode.ALL]] + name = "all" + help = "A combination of inequalities and equalities." +[[option.mode.EQUALITY]] + name = "eqs" + help = "Outputs lemmas of the general forms (= p c) implies (<= p d) for c < d, or (= p c) implies (not (= p d)) for c != d." +[[option.mode.INEQUALITY]] + name = "ineqs" + help = "Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d." +[[option.mode.NO]] + name = "none" [[option]] name = "arithPropagationMode" @@ -19,10 +29,22 @@ header = "options/arith_options.h" long = "arith-prop=MODE" type = "ArithPropagationMode" default = "BOTH_PROP" - handler = "stringToArithPropagationMode" - includes = ["options/arith_propagation_mode.h"] read_only = true help = "turns on arithmetic propagation (default is 'old', see --arith-prop=help)" + help_mode = "This decides on kind of propagation arithmetic attempts to do during the search." +[[option.mode.NO_PROP]] + name = "none" +[[option.mode.UNATE_PROP]] + name = "unate" + help = "Use constraints to do unate propagation." +[[option.mode.BOUND_INFERENCE_PROP]] + name = "bi" + help = "(Bounds Inference) infers bounds on basic variables using the upper and lower bounds of the non-basic variables in the tableau." +[[option.mode.BOTH_PROP]] + name = "both" + help = "Use bounds inference and unate." + + # The maximum number of difference pivots to do per invocation of simplex. # If this is negative, the number of pivots done is the number of variables. @@ -55,10 +77,20 @@ header = "options/arith_options.h" long = "error-selection-rule=RULE" type = "ErrorSelectionRule" default = "MINIMUM_AMOUNT" - handler = "stringToErrorSelectionRule" - includes = ["options/arith_heuristic_pivot_rule.h"] read_only = true help = "change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)" + help_mode = "This decides on the rule used by simplex during heuristic rounds for deciding the next basic variable to select." +[[option.mode.MINIMUM_AMOUNT]] + name = "min" + help = "The minimum abs() value of the variable's violation of its bound." +[[option.mode.VAR_ORDER]] + name = "varord" + help = "The variable order." +[[option.mode.MAXIMUM_AMOUNT]] + name = "max" + help = "The maximum violation the bound." +[[option.mode.SUM_METRIC]] + name = "sum" # The number of pivots before simplex rechecks every basic variable for a conflict [[option]] |