From d5987a99361f227cf2ea1404fec594f4a998be70 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 10 May 2021 23:37:12 +0200 Subject: [PATCH] Remove read_only from options. (#6513) This PR removes the possibility of declaring options read_only. It's only effect is making an attempts to disallow changing the respective option from within our internal code (by not providing a setter method). However, a "read-only" option can still be set via the setOption() methods that is also used by the API, and by SMT-LIB's set-option. --- src/options/README | 4 -- src/options/arith_options.toml | 34 ----------- src/options/base_options.toml | 10 ---- src/options/bv_options.toml | 3 - src/options/datatypes_options.toml | 16 ----- src/options/decision_options.toml | 4 -- src/options/expr_options.toml | 3 - src/options/main_options.toml | 11 ---- src/options/mkoptions.py | 23 ++------ src/options/parser_options.toml | 6 -- src/options/proof_options.toml | 2 - src/options/prop_options.toml | 5 -- src/options/quantifiers_options.toml | 71 ----------------------- src/options/resource_manager_options.toml | 1 - src/options/sep_options.toml | 6 -- src/options/sets_options.toml | 3 - src/options/smt_options.toml | 26 --------- src/options/strings_options.toml | 14 ----- src/options/theory_options.toml | 1 - src/options/uf_options.toml | 5 -- 20 files changed, 6 insertions(+), 242 deletions(-) diff --git a/src/options/README b/src/options/README index 5467d20c4..868690b85 100644 --- a/src/options/README +++ b/src/options/README @@ -41,9 +41,6 @@ Options predicates ... (list) functions that check whether given option value is valid includes ... (list) header files required by handler/predicates - read_only ... (bool) true: option should not provide a ::set method, - false (default): option should provide a ::set - method to set the option value alternate ... (bool) true (default): add --no- alternative option false: omit --no- alternative option help ... (string) documentation (required if category is not @@ -71,7 +68,6 @@ Options handler = "stringToOutputLanguage" predicates = [] includes = ["options/language.h"] - read_only = false help = "force output language (default is \"auto\"; see --output-lang help)" diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 20ae73fce..2afe92ccd 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -8,7 +8,6 @@ header = "options/arith_options.h" long = "unate-lemmas=MODE" type = "ArithUnateLemmaMode" 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]] @@ -29,7 +28,6 @@ header = "options/arith_options.h" long = "arith-prop=MODE" type = "ArithPropagationMode" default = "BOTH_PROP" - 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]] @@ -77,7 +75,6 @@ header = "options/arith_options.h" long = "error-selection-rule=RULE" type = "ErrorSelectionRule" default = "MINIMUM_AMOUNT" - 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]] @@ -99,7 +96,6 @@ header = "options/arith_options.h" long = "simplex-check-period=N" type = "uint16_t" default = "200" - read_only = true help = "the number of pivots to do in simplex before rechecking for a conflict on all variables" # This is the pivots per basic variable that can be done using heuristic choices @@ -120,7 +116,6 @@ header = "options/arith_options.h" long = "prop-row-length=N" type = "uint16_t" default = "16" - read_only = true help = "sets the maximum row length to be used in propagation" [[option]] @@ -129,7 +124,6 @@ header = "options/arith_options.h" long = "dio-solver" type = "bool" default = "true" - read_only = true help = "turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)" # Whether to split (= x y) into (and (<= x y) (>= x y)) in @@ -158,7 +152,6 @@ header = "options/arith_options.h" long = "miplib-trick-subs=N" type = "unsigned" default = "1" - read_only = true help = "do substitution for miplib 'tmp' vars if defined in <= N eliminated vars" [[option]] @@ -175,7 +168,6 @@ header = "options/arith_options.h" long = "maxCutsInContext=N" type = "unsigned" default = "65535" - read_only = true help = "maximum cuts in a given context before signalling a restart" [[option]] @@ -184,7 +176,6 @@ header = "options/arith_options.h" long = "revert-arith-models-on-unsat" type = "bool" default = "false" - read_only = true help = "revert the arithmetic model to a known safe model on unsat if one is cached" [[option]] @@ -281,7 +272,6 @@ header = "options/arith_options.h" long = "se-solve-int" type = "bool" default = "false" - read_only = true help = "attempt to use the approximate solve integer method on standard effort" [[option]] @@ -290,7 +280,6 @@ header = "options/arith_options.h" long = "lemmas-on-replay-failure" type = "bool" default = "false" - read_only = true help = "attempt to use external lemmas if approximate solve integer failed" [[option]] @@ -299,7 +288,6 @@ header = "options/arith_options.h" long = "dio-turns=N" type = "int" default = "10" - read_only = true help = "turns in a row dio solver cutting gets" [[option]] @@ -308,7 +296,6 @@ header = "options/arith_options.h" long = "rr-turns=N" type = "int" default = "3" - read_only = true help = "round robin turn" [[option]] @@ -317,7 +304,6 @@ header = "options/arith_options.h" long = "dio-repeat" type = "bool" default = "false" - read_only = true help = "handle dio solver constraints in mass or one at a time" [[option]] @@ -326,7 +312,6 @@ header = "options/arith_options.h" long = "replay-early-close-depth=N" type = "int" default = "1" - read_only = true help = "multiples of the depths to try to close the approx log eagerly" [[option]] @@ -335,7 +320,6 @@ header = "options/arith_options.h" long = "replay-failure-penalty=N" type = "int" default = "100" - read_only = true help = "number of solve integer attempts to skips after a numeric failure" [[option]] @@ -344,7 +328,6 @@ header = "options/arith_options.h" long = "replay-num-err-penalty=N" type = "int" default = "4194304" - read_only = true help = "number of solve integer attempts to skips after a numeric failure" [[option]] @@ -353,7 +336,6 @@ header = "options/arith_options.h" long = "replay-reject-cut=N" type = "unsigned" default = "25500" - read_only = true help = "maximum complexity of any coefficient while replaying cuts" [[option]] @@ -362,7 +344,6 @@ header = "options/arith_options.h" long = "replay-lemma-reject-cut=N" type = "unsigned" default = "25500" - read_only = true help = "maximum complexity of any coefficient while outputting replaying cut lemmas" [[option]] @@ -371,7 +352,6 @@ header = "options/arith_options.h" long = "replay-soi-major-threshold=T" type = "double" default = ".01" - read_only = true help = "threshold for a major tolerance failure by the approximate solver" [[option]] @@ -380,7 +360,6 @@ header = "options/arith_options.h" long = "replay-soi-major-threshold-pen=N" type = "int" default = "50" - read_only = true help = "threshold for a major tolerance failure by the approximate solver" [[option]] @@ -389,7 +368,6 @@ header = "options/arith_options.h" long = "replay-soi-minor-threshold=T" type = "double" default = ".0001" - read_only = true help = "threshold for a minor tolerance failure by the approximate solver" [[option]] @@ -398,7 +376,6 @@ header = "options/arith_options.h" long = "replay-soi-minor-threshold-pen=N" type = "int" default = "10" - read_only = true help = "threshold for a minor tolerance failure by the approximate solver" [[option]] @@ -407,7 +384,6 @@ header = "options/arith_options.h" long = "pp-assert-max-sub-size=N" type = "unsigned" default = "2" - read_only = true help = "threshold for substituting an equality in ppAssert" [[option]] @@ -416,7 +392,6 @@ header = "options/arith_options.h" long = "arith-no-partial-fun" type = "bool" default = "false" - read_only = true help = "do not use partial function semantics for arithmetic (not SMT LIB compliant)" [[option]] @@ -441,7 +416,6 @@ header = "options/arith_options.h" long = "nl-ext-rbound" type = "bool" default = "false" - read_only = true help = "use resolution-style inference for inferring new bounds in non-linear incremental linearization solver" [[option]] @@ -450,7 +424,6 @@ header = "options/arith_options.h" long = "nl-ext-factor" type = "bool" default = "true" - read_only = true help = "use factoring inference in non-linear incremental linearization solver" [[option]] @@ -475,7 +448,6 @@ header = "options/arith_options.h" long = "nl-ext-tf-tplanes" type = "bool" default = "true" - read_only = true help = "use non-terminating tangent plane strategy for transcendental functions for non-linear incremental linearization solver" [[option]] @@ -484,7 +456,6 @@ header = "options/arith_options.h" long = "nl-ext-ent-conf" type = "bool" default = "false" - read_only = true help = "check for entailed conflicts in non-linear solver" [[option]] @@ -493,7 +464,6 @@ header = "options/arith_options.h" long = "nl-ext-rewrite" type = "bool" default = "true" - read_only = true help = "do context-dependent simplification based on rewrites in non-linear solver" [[option]] @@ -502,7 +472,6 @@ header = "options/arith_options.h" long = "nl-ext-purify" type = "bool" default = "false" - read_only = true help = "purify non-linear terms at preprocess" [[option]] @@ -511,7 +480,6 @@ header = "options/arith_options.h" long = "nl-ext-split-zero" type = "bool" default = "false" - read_only = true help = "initial splits on zero for all variables" [[option]] @@ -528,7 +496,6 @@ header = "options/arith_options.h" long = "nl-ext-inc-prec" type = "bool" default = "true" - read_only = true help = "whether to increment the precision for irrational function constraints" [[option]] @@ -555,7 +522,6 @@ header = "options/arith_options.h" long = "arith-brab" type = "bool" default = "true" - read_only = true help = "whether to use simple rounding, similar to a unit-cube test, for integers" [[option]] diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 75e33e551..eb3a13778 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -71,7 +71,6 @@ header = "options/base_options.h" long = "verbose" type = "void" handler = "increaseVerbosity" - read_only = true help = "increase verbosity (may be repeated)" [[option]] @@ -80,7 +79,6 @@ header = "options/base_options.h" long = "quiet" type = "void" handler = "decreaseVerbosity" - read_only = true help = "decrease verbosity (may be repeated)" [[option]] @@ -90,7 +88,6 @@ header = "options/base_options.h" category = "common" type = "bool" predicates = ["setStats"] - read_only = true help = "give statistics on exit" [[option]] @@ -100,7 +97,6 @@ header = "options/base_options.h" category = "expert" type = "bool" predicates = ["setStats"] - read_only = true help = "print unchanged (defaulted) statistics as well" [[option]] @@ -110,7 +106,6 @@ header = "options/base_options.h" category = "expert" type = "bool" predicates = ["setStats"] - read_only = true help = "print expert (non-public) statistics as well" [[option]] @@ -121,7 +116,6 @@ header = "options/base_options.h" type = "bool" predicates = ["setStats"] default = "false" - read_only = true help = "in incremental mode, print stats after every satisfiability or validity query" [[option]] @@ -136,7 +130,6 @@ header = "options/base_options.h" category = "regular" long = "preprocess-only" type = "bool" - read_only = true help = "exit after preprocessing input" [[option]] @@ -146,7 +139,6 @@ header = "options/base_options.h" long = "trace=TAG" type = "std::string" handler = "enableTraceTag" - read_only = true help = "trace something (e.g. -t pushpop), can repeat" [[option]] @@ -156,7 +148,6 @@ header = "options/base_options.h" long = "debug=TAG" type = "std::string" handler = "enableDebugTag" - read_only = true help = "debug something (e.g. -d arith), can repeat" [[option]] @@ -164,5 +155,4 @@ header = "options/base_options.h" category = "regular" long = "print-success" type = "bool" - read_only = true help = "print the \"success\" output required of SMT-LIBv2" diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 18f190ff1..e6ef18311 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -160,7 +160,6 @@ header = "options/bv_options.h" long = "bv-num-func=N" type = "unsigned" default = "1" - read_only = true help = "number of function symbols in conflicts that are generalized" [[option]] @@ -177,7 +176,6 @@ header = "options/bv_options.h" long = "bv-quick-xplain" type = "bool" default = "false" - read_only = true help = "minimize bv conflicts using the QuickXplain algorithm" [[option]] @@ -194,7 +192,6 @@ header = "options/bv_options.h" long = "bv-gauss-elim" type = "bool" default = "false" - read_only = true help = "simplify formula via Gaussian Elimination if applicable" [[option]] diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index 164dd736b..cf1ac5f49 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -29,7 +29,6 @@ header = "options/datatypes_options.h" long = "dt-polite-optimize" type = "bool" default = "true" - read_only = true help = "turn on optimization for polite combination" [[option]] @@ -38,7 +37,6 @@ header = "options/datatypes_options.h" long = "dt-binary-split" type = "bool" default = "false" - read_only = true help = "do binary splits for datatype constructor types" [[option]] @@ -47,7 +45,6 @@ header = "options/datatypes_options.h" long = "cdt-bisimilar" type = "bool" default = "true" - read_only = true help = "do bisimilarity check for co-datatypes" [[option]] @@ -56,7 +53,6 @@ header = "options/datatypes_options.h" long = "dt-cyclic" type = "bool" default = "true" - read_only = true help = "do cyclicity check for datatypes" [[option]] @@ -65,7 +61,6 @@ header = "options/datatypes_options.h" long = "dt-infer-as-lemmas" type = "bool" default = "false" - read_only = true help = "always send lemmas out instead of making internal inferences" [[option]] @@ -74,7 +69,6 @@ header = "options/datatypes_options.h" long = "dt-blast-splits" type = "bool" default = "false" - read_only = true help = "when applicable, blast splitting lemmas for all variables at once" [[option]] @@ -83,7 +77,6 @@ header = "options/datatypes_options.h" long = "dt-nested-rec" type = "bool" default = "false" - read_only = true help = "allow nested recursion in datatype definitions" [[option]] @@ -92,7 +85,6 @@ header = "options/datatypes_options.h" long = "dt-share-sel" type = "bool" default = "true" - read_only = true help = "internally use shared selectors across multiple constructors" [[option]] @@ -101,7 +93,6 @@ header = "options/datatypes_options.h" long = "sygus-sym-break" type = "bool" default = "true" - read_only = true help = "simple sygus symmetry breaking lemmas" [[option]] @@ -110,7 +101,6 @@ header = "options/datatypes_options.h" long = "sygus-sym-break-agg" type = "bool" default = "true" - read_only = true help = "use aggressive checks for simple sygus symmetry breaking lemmas" [[option]] @@ -119,7 +109,6 @@ header = "options/datatypes_options.h" long = "sygus-sym-break-dynamic" type = "bool" default = "true" - read_only = true help = "dynamic sygus symmetry breaking lemmas" [[option]] @@ -136,7 +125,6 @@ header = "options/datatypes_options.h" long = "sygus-sym-break-lazy" type = "bool" default = "true" - read_only = true help = "lazily add symmetry breaking lemmas for terms" [[option]] @@ -145,7 +133,6 @@ header = "options/datatypes_options.h" long = "sygus-sym-break-rlv" type = "bool" default = "true" - read_only = true help = "add relevancy conditions to symmetry breaking lemmas" [[option]] @@ -154,7 +141,6 @@ header = "options/datatypes_options.h" long = "sygus-fair=MODE" type = "SygusFairMode" default = "DT_SIZE" - read_only = true help = "if and how to apply fairness for sygus" help_mode = "Modes for enforcing fairness for counterexample guided quantifier instantion." [[option.mode.DIRECT]] @@ -179,7 +165,6 @@ header = "options/datatypes_options.h" long = "sygus-fair-max" type = "bool" default = "true" - read_only = true help = "use max instead of sum for multi-function sygus conjectures" [[option]] @@ -188,5 +173,4 @@ header = "options/datatypes_options.h" long = "sygus-abort-size=N" type = "int" default = "-1" - read_only = true help = "tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)" diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml index c614ab3db..68698b3a1 100644 --- a/src/options/decision_options.toml +++ b/src/options/decision_options.toml @@ -34,7 +34,6 @@ header = "options/decision_options.h" type = "decision::DecisionWeight" default = "0" includes = ["options/decision_weight.h"] - read_only = true help = "ignore all nodes greater than threshold in first attempt to pick decision" [[option]] @@ -43,7 +42,6 @@ header = "options/decision_options.h" long = "decision-use-weight" type = "bool" default = "false" - read_only = true help = "use the weight nodes (locally, by looking at children) to direct recursive search" @@ -53,7 +51,6 @@ header = "options/decision_options.h" long = "decision-random-weight=N" type = "int" default = "0" - read_only = true help = "assign random weights to nodes between 0 and N-1 (0: disable)" [[option]] @@ -62,7 +59,6 @@ header = "options/decision_options.h" long = "decision-weight-internal=HOW" type = "DecisionWeightInternal" default = "OFF" - read_only = true help = "compute weights of internal nodes using children: off, max, sum, usr1" help_mode = "Decision weight internal mode." [[option.mode.OFF]] diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml index 368fb34e4..34a4fb979 100644 --- a/src/options/expr_options.toml +++ b/src/options/expr_options.toml @@ -9,7 +9,6 @@ header = "options/expr_options.h" type = "int" default = "0" predicates = ["setDefaultExprDepthPredicate"] - read_only = true help = "print exprs to depth N (0 == default, -1 == no limit)" [[option]] @@ -20,7 +19,6 @@ header = "options/expr_options.h" type = "int" default = "1" predicates = ["setDefaultDagThreshPredicate"] - read_only = true help = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)" [[option]] @@ -29,5 +27,4 @@ header = "options/expr_options.h" long = "type-checking" type = "bool" default = "DO_SEMANTIC_CHECKS_BY_DEFAULT" - read_only = true help = "type check expressions" diff --git a/src/options/main_options.toml b/src/options/main_options.toml index f0d767276..f014068f3 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -8,7 +8,6 @@ header = "options/main_options.h" short = "V" long = "version" type = "bool" - read_only = true alternate = false help = "identify this cvc5 binary" @@ -18,7 +17,6 @@ header = "options/main_options.h" short = "h" long = "help" type = "bool" - read_only = true alternate = false help = "full command line reference" @@ -27,7 +25,6 @@ header = "options/main_options.h" long = "show-config" type = "void" handler = "showConfiguration" - read_only = true help = "show cvc5 static configuration" [[option]] @@ -35,7 +32,6 @@ header = "options/main_options.h" long = "copyright" type = "void" handler = "copyright" - read_only = true help = "show cvc5 copyright information" [[option]] @@ -45,7 +41,6 @@ header = "options/main_options.h" long = "seed=N" type = "uint64_t" default = "0" - read_only = true help = "seed for random number generator" [[option]] @@ -53,7 +48,6 @@ header = "options/main_options.h" long = "show-debug-tags" type = "void" handler = "showDebugTags" - read_only = true help = "show all available tags for debugging" [[option]] @@ -61,7 +55,6 @@ header = "options/main_options.h" long = "show-trace-tags" type = "void" handler = "showTraceTags" - read_only = true help = "show all available tags for tracing" [[option]] @@ -70,7 +63,6 @@ header = "options/main_options.h" long = "early-exit" type = "bool" default = "true" - read_only = true help = "do not run destructors at exit; default on except in debug builds" [[option]] @@ -86,7 +78,6 @@ header = "options/main_options.h" long = "interactive-prompt" type = "bool" default = "true" - read_only = true help = "interactive prompting while in interactive mode" [[option]] @@ -95,7 +86,6 @@ header = "options/main_options.h" long = "segv-spin" type = "bool" default = "false" - read_only = true help = "spin on segfault/other crash waiting for gdb" [[option]] @@ -104,5 +94,4 @@ header = "options/main_options.h" long = "tear-down-incremental=N" type = "int" default = "0" - read_only = true help = "implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N queries" diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index e2c138490..b632b3384 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -56,7 +56,7 @@ MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['option'] OPTION_ATTR_REQ = ['category', 'type'] OPTION_ATTR_ALL = OPTION_ATTR_REQ + [ 'name', 'help', 'help_mode', 'smt_name', 'short', 'long', 'default', - 'includes', 'handler', 'predicates', 'read_only', + 'includes', 'handler', 'predicates', 'alternate', 'mode' ] @@ -134,15 +134,6 @@ TPL_OPTION_STRUCT_RW = \ static constexpr const char* name = "{long_name}"; }} thread_local {name};""" -TPL_OPTION_STRUCT_RO = \ -"""extern struct {name}__option_t -{{ - typedef {type} type; - type operator()() const; - static constexpr const char* name = "{long_name}"; -}} thread_local {name};""" - - TPL_DECL_SET = \ """template <> options::{name}__option_t::type& Options::ref( options::{name}__option_t);""" @@ -260,12 +251,11 @@ class Option(object): self.__dict__ = dict((k, None) for k in OPTION_ATTR_ALL) self.includes = [] self.predicates = [] - self.read_only = False self.alternate = True # add --no- alternative long option for bool self.filename = None for (attr, val) in d.items(): assert attr in self.__dict__ - if attr in ['read_only', 'alternate'] or val: + if attr == 'alternate' or val: self.__dict__[attr] = val @@ -274,6 +264,7 @@ def die(msg): def perr(filename, msg, option = None): + msg_suffix = '' if option: if option.name: msg_suffix = "option '{}' ".format(option.name) @@ -461,7 +452,7 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): holder_specs.append(TPL_HOLDER_MACRO_ATTR.format(name=option.name)) # Generate module declaration - tpl_decl = TPL_OPTION_STRUCT_RO if option.read_only else TPL_OPTION_STRUCT_RW + tpl_decl = TPL_OPTION_STRUCT_RW if option.long: long_name = option.long.split('=')[0] else: @@ -469,8 +460,7 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): decls.append(tpl_decl.format(name=option.name, type=option.type, long_name = long_name)) # Generate module specialization - if not option.read_only: - specs.append(TPL_DECL_SET.format(name=option.name)) + specs.append(TPL_DECL_SET.format(name=option.name)) specs.append(TPL_DECL_OP_BRACKET.format(name=option.name)) specs.append(TPL_DECL_WAS_SET_BY_USER.format(name=option.name)) @@ -492,8 +482,7 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): ### Generate code for {module.name}_options.cpp # Accessors - if not option.read_only: - accs.append(TPL_IMPL_SET.format(name=option.name)) + accs.append(TPL_IMPL_SET.format(name=option.name)) accs.append(TPL_IMPL_OP_BRACKET.format(name=option.name)) accs.append(TPL_IMPL_WAS_SET_BY_USER.format(name=option.name)) diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml index 1a4b75429..56568bc0c 100644 --- a/src/options/parser_options.toml +++ b/src/options/parser_options.toml @@ -7,7 +7,6 @@ header = "options/parser_options.h" category = "common" long = "strict-parsing" type = "bool" - read_only = true help = "be less tolerant of non-conforming inputs" [[option]] @@ -15,7 +14,6 @@ header = "options/parser_options.h" category = "regular" long = "mmap" type = "bool" - read_only = true help = "memory map file input" [[option]] @@ -24,7 +22,6 @@ header = "options/parser_options.h" category = "regular" type = "bool" default = "DO_SEMANTIC_CHECKS_BY_DEFAULT" - read_only = true help = "enable semantic checks, including type checks" [[option]] @@ -33,7 +30,6 @@ header = "options/parser_options.h" category = "regular" type = "bool" default = "false" - read_only = true help = "force all declarations and definitions to be global" # this is to support security in the online version, and in other similar @@ -54,7 +50,6 @@ header = "options/parser_options.h" long = "filesystem-access" type = "bool" default = "true" - read_only = true [[option]] name = "forceLogicString" @@ -62,5 +57,4 @@ header = "options/parser_options.h" category = "expert" long = "force-logic=LOGIC" type = "std::string" - read_only = true help = "set the logic, and override all further user attempts to change it" diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index f6a39e0fe..177307918 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -26,7 +26,6 @@ header = "options/proof_options.h" long = "proof-print-conclusion" type = "bool" default = "false" - read_only = true help = "Print conclusion of proof steps when printing AST" [[option]] @@ -35,7 +34,6 @@ header = "options/proof_options.h" long = "proof-pedantic=N" type = "uint32_t" default = "0" - read_only = true help = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof" [[option]] diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml index 5ad691e62..0670bb7da 100644 --- a/src/options/prop_options.toml +++ b/src/options/prop_options.toml @@ -10,7 +10,6 @@ header = "options/prop_options.h" type = "double" default = "0.0" predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"] - read_only = true help = "sets the frequency of random decisions in the sat solver (P=0.0 by default)" [[option]] @@ -44,7 +43,6 @@ header = "options/prop_options.h" long = "restart-int-base=N" type = "unsigned" default = "25" - read_only = true help = "sets the base restart interval for the sat solver (N=25 by default)" [[option]] @@ -54,7 +52,6 @@ header = "options/prop_options.h" type = "double" default = "3.0" predicates = ["doubleGreaterOrEqual0"] - read_only = true help = "sets the restart interval increase factor for the sat solver (F=3.0 by default)" [[option]] @@ -63,7 +60,6 @@ header = "options/prop_options.h" long = "refine-conflicts" type = "bool" default = "false" - read_only = true help = "refine theory conflict clauses (default false)" [[option]] @@ -80,5 +76,4 @@ header = "options/prop_options.h" long = "minisat-dump-dimacs" type = "bool" default = "false" - read_only = true help = "instead of solving minisat dumps the asserted clauses in Dimacs format" diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 076d26553..ce2e1ab32 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -67,7 +67,6 @@ header = "options/quantifiers_options.h" long = "var-elim-quant" type = "bool" default = "true" - read_only = true help = "enable simple variable elimination for quantified formulas" [[option]] @@ -76,7 +75,6 @@ header = "options/quantifiers_options.h" long = "var-ineq-elim-quant" type = "bool" default = "true" - read_only = true help = "enable variable elimination based on infinite projection of unbound arithmetic variables" [[option]] @@ -85,7 +83,6 @@ header = "options/quantifiers_options.h" long = "dt-var-exp-quant" type = "bool" default = "true" - read_only = true help = "expand datatype variables bound to one constructor in quantifiers" [[option]] @@ -112,7 +109,6 @@ header = "options/quantifiers_options.h" long = "cond-var-split-quant" type = "bool" default = "true" - read_only = true help = "split quantified formulas that lead to variable eliminations" [[option]] @@ -121,7 +117,6 @@ header = "options/quantifiers_options.h" long = "cond-var-split-agg-quant" type = "bool" default = "false" - read_only = true help = "aggressive split quantified formulas that lead to variable eliminations" [[option]] @@ -165,7 +160,6 @@ header = "options/quantifiers_options.h" long = "ag-miniscope-quant" type = "bool" default = "false" - read_only = true help = "perform aggressive miniscoping for quantifiers" [[option]] @@ -174,7 +168,6 @@ header = "options/quantifiers_options.h" long = "elim-taut-quant" type = "bool" default = "true" - read_only = true help = "eliminate tautological disjuncts of quantified formulas" [[option]] @@ -183,7 +176,6 @@ header = "options/quantifiers_options.h" long = "ext-rewrite-quant" type = "bool" default = "false" - read_only = true help = "apply extended rewriting to bodies of quantified formulas" [[option]] @@ -233,7 +225,6 @@ header = "options/quantifiers_options.h" long = "register-quant-body-terms" type = "bool" default = "false" - read_only = true help = "consider ground terms within bodies of quantified formulas for matching" [[option]] @@ -242,7 +233,6 @@ header = "options/quantifiers_options.h" long = "strict-triggers" type = "bool" default = "false" - read_only = true help = "only instantiate quantifiers with user patterns based on triggers" [[option]] @@ -251,7 +241,6 @@ header = "options/quantifiers_options.h" long = "relevant-triggers" type = "bool" default = "false" - read_only = true help = "prefer triggers that are more relevant based on SInE style analysis" [[option]] @@ -260,7 +249,6 @@ header = "options/quantifiers_options.h" long = "relational-triggers" type = "bool" default = "false" - read_only = true help = "choose relational triggers such as x = f(y), x >= f(y)" [[option]] @@ -285,7 +273,6 @@ header = "options/quantifiers_options.h" long = "multi-trigger-when-single" type = "bool" default = "false" - read_only = true help = "select multi triggers when single triggers exist" [[option]] @@ -294,7 +281,6 @@ header = "options/quantifiers_options.h" long = "multi-trigger-priority" type = "bool" default = "false" - read_only = true help = "only try multi triggers if single triggers give no instantiations" [[option]] @@ -303,7 +289,6 @@ header = "options/quantifiers_options.h" long = "multi-trigger-cache" type = "bool" default = "false" - read_only = true help = "caching version of multi triggers" [[option]] @@ -312,7 +297,6 @@ header = "options/quantifiers_options.h" long = "multi-trigger-linear" type = "bool" default = "true" - read_only = true help = "implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms" # Trigger selection mode. @@ -421,7 +405,6 @@ header = "options/quantifiers_options.h" long = "increment-triggers" type = "bool" default = "true" - read_only = true help = "generate additional triggers as needed during search" [[option]] @@ -490,7 +473,6 @@ header = "options/quantifiers_options.h" long = "inst-level-input-only" type = "bool" default = "true" - read_only = true help = "only input terms are assigned instantiation level zero" [[option]] @@ -525,7 +507,6 @@ header = "options/quantifiers_options.h" long = "full-saturate-quant-rd" type = "bool" default = "true" - read_only = true help = "whether to use relevant domain first for enumerative instantiation strategy" [[option]] @@ -534,7 +515,6 @@ header = "options/quantifiers_options.h" long = "full-saturate-quant-limit=N" type = "int" default = "-1" - read_only = true help = "maximum number of rounds of enumerative instantiation to apply (-1 means no limit)" [[option]] @@ -543,7 +523,6 @@ header = "options/quantifiers_options.h" long = "fs-interleave" type = "bool" default = "false" - read_only = true help = "interleave enumerative instantiation with other techniques" [[option]] @@ -552,7 +531,6 @@ header = "options/quantifiers_options.h" long = "fs-stratify" type = "bool" default = "false" - read_only = true help = "stratify effort levels in enumerative instantiation, which favors speed over fairness" [[option]] @@ -561,7 +539,6 @@ header = "options/quantifiers_options.h" long = "fs-sum" type = "bool" default = "false" - read_only = true help = "enumerating tuples of quantifiers by increasing the sum of indices, rather than the maximum" [[option]] @@ -570,7 +547,6 @@ header = "options/quantifiers_options.h" long = "literal-matching=MODE" type = "LiteralMatchMode" default = "USE" - read_only = true help = "choose literal matching mode" help_mode = "Literal match modes." [[option.mode.NONE]] @@ -610,7 +586,6 @@ header = "options/quantifiers_options.h" long = "quant-fun-wd" type = "bool" default = "false" - read_only = true help = "assume that function defined by quantifiers are well defined" [[option]] @@ -627,7 +602,6 @@ header = "options/quantifiers_options.h" long = "fmf-fun-rlv" type = "bool" default = "false" - read_only = true help = "find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant" [[option]] @@ -662,7 +636,6 @@ header = "options/quantifiers_options.h" long = "mbqi-interleave" type = "bool" default = "false" - read_only = true help = "interleave model-based quantifier instantiation with other techniques" [[option]] @@ -679,7 +652,6 @@ header = "options/quantifiers_options.h" long = "fmf-fresh-dc" type = "bool" default = "false" - read_only = true help = "use fresh distinguished representative when applying Inst-Gen techniques" [[option]] @@ -688,7 +660,6 @@ header = "options/quantifiers_options.h" long = "fmf-fmc-simple" type = "bool" default = "true" - read_only = true help = "simple models in full model check for finite model finding" [[option]] @@ -721,7 +692,6 @@ header = "options/quantifiers_options.h" long = "fmf-type-completion-thresh=N" type = "int" default = "1000" - read_only = true help = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted" [[option]] @@ -738,7 +708,6 @@ header = "options/quantifiers_options.h" long = "quant-cf-mode=MODE" type = "QcfMode" default = "PROP_EQ" - read_only = true help = "what effort to apply conflict find mechanism" help_mode = "Quantifier conflict find modes." [[option.mode.CONFLICT_ONLY]] @@ -757,7 +726,6 @@ header = "options/quantifiers_options.h" long = "quant-cf-when=MODE" type = "QcfWhenMode" default = "DEFAULT" - read_only = true help = "when to invoke conflict find mechanism for quantifiers" help_mode = "Quantifier conflict find modes." [[option.mode.DEFAULT]] @@ -795,7 +763,6 @@ header = "options/quantifiers_options.h" long = "qcf-nested-conflict" type = "bool" default = "false" - read_only = true help = "consider conflicts for nested quantifiers" [[option]] @@ -804,7 +771,6 @@ header = "options/quantifiers_options.h" long = "qcf-vo-exp" type = "bool" default = "false" - read_only = true help = "qcf experimental variable ordering" [[option]] @@ -821,7 +787,6 @@ header = "options/quantifiers_options.h" long = "qcf-eager-test" type = "bool" default = "true" - read_only = true help = "optimization, test qcf instances eagerly" [[option]] @@ -830,7 +795,6 @@ header = "options/quantifiers_options.h" long = "qcf-eager-check-rd" type = "bool" default = "true" - read_only = true help = "optimization, eagerly check relevant domain of matched position" [[option]] @@ -839,7 +803,6 @@ header = "options/quantifiers_options.h" long = "qcf-skip-rd" type = "bool" default = "false" - read_only = true help = "optimization, skip instances based on possibly irrelevant portions of quantified formulas" ### Induction options @@ -850,7 +813,6 @@ header = "options/quantifiers_options.h" long = "quant-ind" type = "bool" default = "false" - read_only = true help = "use all available techniques for inductive reasoning" [[option]] @@ -883,7 +845,6 @@ header = "options/quantifiers_options.h" long = "conjecture-gen-per-round=N" type = "int" default = "1" - read_only = true help = "number of conjectures to generate per instantiation round" [[option]] @@ -892,7 +853,6 @@ header = "options/quantifiers_options.h" long = "conjecture-no-filter" type = "bool" default = "false" - read_only = true help = "do not filter conjectures" [[option]] @@ -925,7 +885,6 @@ header = "options/quantifiers_options.h" long = "conjecture-gen-gt-enum=N" type = "int" default = "50" - read_only = true help = "number of ground terms to generate for model filtering" [[option]] @@ -934,7 +893,6 @@ header = "options/quantifiers_options.h" long = "conjecture-gen-uee-intro" type = "bool" default = "false" - read_only = true help = "more aggressive merging for universal equality engine, introduces terms" [[option]] @@ -943,7 +901,6 @@ header = "options/quantifiers_options.h" long = "conjecture-gen-max-depth=N" type = "int" default = "3" - read_only = true help = "maximum depth of terms to consider for conjectures" ### Synthesis options @@ -954,7 +911,6 @@ header = "options/quantifiers_options.h" long = "sygus-inference" type = "bool" default = "false" - read_only = false help = "attempt to preprocess arbitrary inputs to sygus conjectures" [[option]] @@ -989,7 +945,6 @@ header = "options/quantifiers_options.h" long = "sygus-si-partial" type = "bool" default = "false" - read_only = true help = "combined techniques for synthesis conjectures that are partially single invocation" # Solution reconstruction modes for single invocation conjectures @@ -1025,7 +980,6 @@ header = "options/quantifiers_options.h" long = "sygus-si-rcons-limit=N" type = "int" default = "10000" - read_only = true help = "number of rounds of enumeration to use during solution reconstruction (negative means unlimited)" [[option]] @@ -1034,7 +988,6 @@ header = "options/quantifiers_options.h" long = "sygus-si-reconstruct-const" type = "bool" default = "true" - read_only = true help = "include constants when reconstruct solutions for single invocation conjectures in original grammar" [[option]] @@ -1043,7 +996,6 @@ header = "options/quantifiers_options.h" long = "sygus-si-abort" type = "bool" default = "false" - read_only = true help = "abort if synthesis conjecture is not single invocation" [[option]] @@ -1052,7 +1004,6 @@ header = "options/quantifiers_options.h" long = "sygus-crepair-abort" type = "bool" default = "false" - read_only = true help = "abort if constant repair techniques are not applicable" # Modes for piecewise-independent unification for synthesis (see Barbosa et al @@ -1109,7 +1060,6 @@ header = "options/quantifiers_options.h" long = "sygus-qe-preproc" type = "bool" default = "false" - read_only = true help = "use quantifier elimination as a preprocessing step for sygus" [[option]] @@ -1141,7 +1091,6 @@ header = "options/quantifiers_options.h" long = "sygus-active-gen=MODE" type = "SygusActiveGenMode" default = "AUTO" - read_only = true help = "mode for actively-generated sygus enumerators" help_mode = "Modes for actively-generated sygus enumerators." [[option.mode.NONE]] @@ -1174,7 +1123,6 @@ header = "options/quantifiers_options.h" long = "sygus-min-grammar" type = "bool" default = "true" - read_only = true help = "statically minimize sygus grammars" [[option]] @@ -1183,7 +1131,6 @@ header = "options/quantifiers_options.h" long = "sygus-add-const-grammar" type = "bool" default = "false" - read_only = true help = "statically add constants appearing in conjecture to grammars" [[option]] @@ -1192,7 +1139,6 @@ header = "options/quantifiers_options.h" long = "sygus-grammar-norm" type = "bool" default = "false" - read_only = true help = "statically normalize sygus grammars based on flattening (linearization)" [[option]] @@ -1201,7 +1147,6 @@ header = "options/quantifiers_options.h" long = "sygus-templ-embed-grammar" type = "bool" default = "false" - read_only = true help = "embed sygus templates into grammars" [[option]] @@ -1249,7 +1194,6 @@ header = "options/quantifiers_options.h" long = "sygus-inv-templ-when-sg" type = "bool" default = "false" - read_only = false help = "use invariant templates (with solution reconstruction) for syntax guided problems" [[option]] @@ -1258,7 +1202,6 @@ header = "options/quantifiers_options.h" long = "sygus-auto-unfold" type = "bool" default = "true" - read_only = true help = "enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems" [[option]] @@ -1291,7 +1234,6 @@ header = "options/quantifiers_options.h" long = "sygus-eval-unfold" type = "bool" default = "true" - read_only = true help = "do unfolding of sygus evaluation functions" [[option]] @@ -1300,7 +1242,6 @@ header = "options/quantifiers_options.h" long = "sygus-eval-unfold-bool" type = "bool" default = "true" - read_only = true help = "do unfolding of Boolean evaluation functions that appear in refinement lemmas" [[option]] @@ -1377,7 +1318,6 @@ header = "options/quantifiers_options.h" long = "sygus-rr" type = "bool" default = "false" - read_only = true help = "use sygus to enumerate and verify correctness of rewrite rules" [[option]] @@ -1450,7 +1390,6 @@ header = "options/quantifiers_options.h" long = "sygus-sample-grammar" type = "bool" default = "true" - read_only = true help = "when applicable, use grammar for choosing sample points" [[option]] @@ -1690,7 +1629,6 @@ header = "options/quantifiers_options.h" long = "cegqi-min-bounds" type = "bool" default = "false" - read_only = true help = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation" [[option]] @@ -1699,7 +1637,6 @@ header = "options/quantifiers_options.h" long = "cegqi-round-up-lia" type = "bool" default = "false" - read_only = true help = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation" [[option]] @@ -1716,7 +1653,6 @@ header = "options/quantifiers_options.h" long = "cegqi-nopt" type = "bool" default = "true" - read_only = true help = "non-optimal bounds for counterexample-based quantifier instantiation" # CEGQI for BV @@ -1795,7 +1731,6 @@ header = "options/quantifiers_options.h" long = "quant-alpha-equiv" type = "bool" default = "true" - read_only = true help = "infer alpha equivalence between quantified formulas" [[option]] @@ -1812,7 +1747,6 @@ header = "options/quantifiers_options.h" long = "macros-quant-mode=MODE" type = "MacrosQuantMode" default = "GROUND_UF" - read_only = true help = "mode for quantifiers macro expansion" help_mode = "Modes for quantifiers macro expansion." [[option.mode.ALL]] @@ -1851,7 +1785,6 @@ header = "options/quantifiers_options.h" long = "ho-matching" type = "bool" default = "true" - read_only = true help = "do higher-order matching algorithm for triggers with variable operators" [[option]] @@ -1860,7 +1793,6 @@ header = "options/quantifiers_options.h" long = "ho-matching-var-priority" type = "bool" default = "true" - read_only = true help = "give priority to variable arguments over constant arguments" [[option]] @@ -1869,7 +1801,6 @@ header = "options/quantifiers_options.h" long = "ho-merge-term-db" type = "bool" default = "true" - read_only = true help = "merge term indices modulo equality" [[option]] @@ -1878,7 +1809,6 @@ header = "options/quantifiers_options.h" long = "ho-elim" type = "bool" default = "false" - read_only = true help = "eagerly eliminate higher-order constraints" [[option]] @@ -1887,7 +1817,6 @@ header = "options/quantifiers_options.h" long = "ho-elim-store-ax" type = "bool" default = "true" - read_only = false help = "use store axiom during ho-elim" ### Output options diff --git a/src/options/resource_manager_options.toml b/src/options/resource_manager_options.toml index 05dd613f1..8f1c28ca5 100644 --- a/src/options/resource_manager_options.toml +++ b/src/options/resource_manager_options.toml @@ -47,7 +47,6 @@ header = "options/resource_manager_options.h" long = "rweight=VAL=N" type = "std::string" handler = "setResourceWeight" - read_only = true help = "set a single resource weight" [[option]] diff --git a/src/options/sep_options.toml b/src/options/sep_options.toml index e19790d7b..9e808df98 100644 --- a/src/options/sep_options.toml +++ b/src/options/sep_options.toml @@ -8,7 +8,6 @@ header = "options/sep_options.h" long = "sep-check-neg" type = "bool" default = "true" - read_only = true help = "check negated spatial assertions" [[option]] @@ -17,7 +16,6 @@ header = "options/sep_options.h" long = "sep-exp" type = "bool" default = "false" - read_only = true help = "experimental flag for sep" [[option]] @@ -26,7 +24,6 @@ header = "options/sep_options.h" long = "sep-min-refine" type = "bool" default = "false" - read_only = true help = "only add refinement lemmas for minimal (innermost) assertions" [[option]] @@ -35,7 +32,6 @@ header = "options/sep_options.h" long = "sep-deq-c" type = "bool" default = "true" - read_only = true help = "assume cardinality elements are distinct" [[option]] @@ -44,7 +40,6 @@ header = "options/sep_options.h" long = "sep-pre-skolem-emp" type = "bool" default = "false" - read_only = true help = "eliminate emp constraint at preprocess time" [[option]] @@ -53,5 +48,4 @@ header = "options/sep_options.h" long = "sep-child-refine" type = "bool" default = "false" - read_only = true help = "child-specific refinements of negated star, positive wand" diff --git a/src/options/sets_options.toml b/src/options/sets_options.toml index 766da793a..0f206f980 100644 --- a/src/options/sets_options.toml +++ b/src/options/sets_options.toml @@ -8,7 +8,6 @@ header = "options/sets_options.h" long = "sets-proxy-lemmas" type = "bool" default = "false" - read_only = true help = "introduce proxy variables eagerly to shorten lemmas" [[option]] @@ -17,7 +16,6 @@ header = "options/sets_options.h" long = "sets-infer-as-lemmas" type = "bool" default = "true" - read_only = true help = "send inferences as lemmas" [[option]] @@ -26,5 +24,4 @@ header = "options/sets_options.h" long = "sets-ext" type = "bool" default = "false" - read_only = true help = "enable extended symbols such as complement and universe in theory of sets" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 24ae162da..3d0cb6d8d 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -8,7 +8,6 @@ header = "options/smt_options.h" category = "common" long = "dump=MODE" type = "std::string" - read_only = true help = "dump preprocessed assertions, etc., see --dump=help" [[option]] @@ -17,7 +16,6 @@ header = "options/smt_options.h" category = "common" long = "dump-to=FILE" type = "std::string" - read_only = true help = "all dumping goes to FILE (instead of stdout)" [[option]] @@ -50,7 +48,6 @@ header = "options/smt_options.h" long = "static-learning" type = "bool" default = "true" - read_only = true help = "use static learning (on by default)" [[option]] @@ -59,7 +56,6 @@ header = "options/smt_options.h" category = "regular" type = "bool" default = "false" - read_only = true help = "always expand symbol definitions in output" [[option]] @@ -91,7 +87,6 @@ header = "options/smt_options.h" long = "dump-models" type = "bool" default = "false" - read_only = true help = "output models after every SAT/INVALID/UNKNOWN response" [[option]] @@ -144,7 +139,6 @@ header = "options/smt_options.h" long = "dump-proofs" type = "bool" default = "false" - read_only = true help = "output proofs after every UNSAT/VALID response" [[option]] @@ -160,7 +154,6 @@ header = "options/smt_options.h" long = "dump-instantiations" type = "bool" default = "false" - read_only = true help = "output instantiations of quantified formulas after every UNSAT/VALID response" [[option]] @@ -190,7 +183,6 @@ header = "options/smt_options.h" long = "sygus-print-callbacks" type = "bool" default = "true" - read_only = true help = "use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging)" [[option]] @@ -246,7 +238,6 @@ header = "options/smt_options.h" long = "dump-unsat-cores-full" type = "bool" default = "false" - read_only = true help = "dump the full unsat core, including unlabeled assertions" [[option]] @@ -255,7 +246,6 @@ header = "options/smt_options.h" long = "produce-unsat-assumptions" type = "bool" default = "false" - read_only = true help = "turn on unsat assumptions generation" [[option]] @@ -366,7 +356,6 @@ header = "options/smt_options.h" long = "simp-ite-hunt-zombies=N" type = "uint32_t" default = "524288" - read_only = true help = "post ite compression enables zombie removal while the number of nodes is above this threshold" [[option]] @@ -392,7 +381,6 @@ header = "options/smt_options.h" long = "abstract-values" type = "bool" default = "false" - read_only = true help = "in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard" [[option]] @@ -402,7 +390,6 @@ header = "options/smt_options.h" long = "model-u-print=MODE" type = "ModelUninterpPrintMode" default = "None" - read_only = true help = "determines how to print uninterpreted elements in models" help_mode = "uninterpreted elements in models printing modes." [[option.mode.DtEnum]] @@ -425,7 +412,6 @@ header = "options/smt_options.h" long = "model-witness-value" type = "bool" default = "false" - read_only = true help = "in models, use a witness constant for choice functions" [[option]] @@ -433,7 +419,6 @@ header = "options/smt_options.h" smt_name = "regular-output-channel" category = "regular" type = "std::string" - read_only = true help = "set the regular output channel of the solver" [[option]] @@ -441,7 +426,6 @@ header = "options/smt_options.h" smt_name = "diagnostic-output-channel" category = "regular" type = "std::string" - read_only = true help = "set the diagnostic output channel of the solver" [[option]] @@ -450,7 +434,6 @@ header = "options/smt_options.h" long = "force-no-limit-cpu-while-dump" type = "bool" default = "false" - read_only = true help = "Force no CPU limit when dumping models and proofs" [[option]] @@ -459,7 +442,6 @@ header = "options/smt_options.h" long = "foreign-theory-rewrite" type = "bool" default = "false" - read_only = true help = "Cross-theory rewrites" [[option]] @@ -489,7 +471,6 @@ header = "options/smt_options.h" long = "bvand-integer-granularity=N" type = "uint32_t" default = "1" - read_only = true help = "granularity to use in --solve-bv-as-int mode and for iand operator (experimental)" [[option]] @@ -498,7 +479,6 @@ header = "options/smt_options.h" long = "iand-mode=mode" type = "IandMode" default = "VALUE" - read_only = true help = "Set the refinement scheme for integer AND" help_mode = "Refinement modes for integer AND" [[option.mode.VALUE]] @@ -517,7 +497,6 @@ header = "options/smt_options.h" long = "solve-int-as-bv=N" type = "uint32_t" default = "0" - read_only = true help = "attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)" [[option]] @@ -526,7 +505,6 @@ header = "options/smt_options.h" long = "solve-real-as-int" type = "bool" default = "false" - read_only = true help = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)" [[option]] @@ -535,7 +513,6 @@ header = "options/smt_options.h" long = "produce-interpols=MODE" type = "ProduceInterpols" default = "NONE" - read_only = true help = "support the get-interpol command" help_mode = "Interpolants grammar mode" [[option.mode.NONE]] @@ -563,7 +540,6 @@ header = "options/smt_options.h" long = "produce-abducts" type = "bool" default = "false" - read_only = true help = "support the get-abduct command" [[option]] @@ -572,7 +548,6 @@ header = "options/smt_options.h" long = "check-interpols" type = "bool" default = "false" - read_only = true help = "checks whether produced solutions to get-interpol are correct" [[option]] @@ -581,5 +556,4 @@ header = "options/smt_options.h" long = "check-abducts" type = "bool" default = "false" - read_only = true help = "checks whether produced solutions to get-abduct are correct" diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 208b4483f..4672bbb6e 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -24,7 +24,6 @@ header = "options/strings_options.h" long = "strings-eager" type = "bool" default = "false" - read_only = true help = "strings eager check" [[option]] @@ -33,7 +32,6 @@ header = "options/strings_options.h" long = "strings-inm" type = "bool" default = "false" - read_only = true help = "internal for strings: ignore negative membership constraints (fragment checking is needed, left to users for now)" [[option]] @@ -42,7 +40,6 @@ header = "options/strings_options.h" long = "strings-lazy-pp" type = "bool" default = "true" - read_only = true help = "perform string preprocessing lazily" [[option]] @@ -51,7 +48,6 @@ header = "options/strings_options.h" long = "strings-len-norm" type = "bool" default = "true" - read_only = true help = "strings length normalization lemma" [[option]] @@ -60,7 +56,6 @@ header = "options/strings_options.h" long = "strings-infer-sym" type = "bool" default = "true" - read_only = true help = "strings split on empty string" [[option]] @@ -69,7 +64,6 @@ header = "options/strings_options.h" long = "strings-eager-len" type = "bool" default = "true" - read_only = true help = "strings eager length lemmas" [[option]] @@ -78,7 +72,6 @@ header = "options/strings_options.h" long = "strings-check-entail-len" type = "bool" default = "true" - read_only = true help = "check entailment between length terms to reduce splitting" [[option]] @@ -112,7 +105,6 @@ header = "options/strings_options.h" long = "strings-infer-as-lemmas" type = "bool" default = "false" - read_only = true help = "always send lemmas out instead of making internal inferences" [[option]] @@ -121,7 +113,6 @@ header = "options/strings_options.h" long = "strings-rexplain-lemmas" type = "bool" default = "true" - read_only = true help = "regression explanations for string lemmas" [[option]] @@ -130,7 +121,6 @@ header = "options/strings_options.h" long = "strings-min-prefix-explain" type = "bool" default = "true" - read_only = true help = "minimize explanations for prefix of normal forms in strings" [[option]] @@ -139,7 +129,6 @@ header = "options/strings_options.h" long = "strings-guess-model" type = "bool" default = "false" - read_only = true help = "use model guessing to avoid string extended function reductions" [[option]] @@ -148,7 +137,6 @@ header = "options/strings_options.h" long = "strings-lprop-csp" type = "bool" default = "false" - read_only = true help = "do length propagation based on constant splits" [[option]] @@ -173,7 +161,6 @@ header = "options/strings_options.h" long = "strings-ff" type = "bool" default = "true" - read_only = true help = "do flat form inferences" [[option]] @@ -203,7 +190,6 @@ header = "options/strings_options.h" long = "strings-unified-vspt" type = "bool" default = "true" - read_only = true help = "use a single skolem for the variable splitting rule" [[option]] diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml index 388333124..a0f769684 100644 --- a/src/options/theory_options.toml +++ b/src/options/theory_options.toml @@ -32,7 +32,6 @@ header = "options/theory_options.h" long = "condense-function-values" type = "bool" default = "true" - read_only = true help = "condense values for functions in models rather than explicitly representing them" [[option]] diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml index a098061f8..bd0027fb4 100644 --- a/src/options/uf_options.toml +++ b/src/options/uf_options.toml @@ -17,7 +17,6 @@ header = "options/uf_options.h" long = "uf-ss-totality-limited=N" type = "int" default = "-1" - read_only = true help = "apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)" [[option]] @@ -26,7 +25,6 @@ header = "options/uf_options.h" long = "uf-ss-totality-sym-break" type = "bool" default = "false" - read_only = true help = "apply symmetry breaking for totality axioms" [[option]] @@ -35,7 +33,6 @@ header = "options/uf_options.h" long = "uf-ss-abort-card=N" type = "int" default = "-1" - read_only = true help = "tells the uf with cardinality to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)" [[option]] @@ -44,7 +41,6 @@ header = "options/uf_options.h" long = "uf-ss=MODE" type = "UfssMode" default = "FULL" - read_only = true help = "mode of operation for uf with cardinality solver." help_mode = "UF with cardinality options currently supported by the --uf-ss option when combined with finite model finding." [[option.mode.FULL]] @@ -63,7 +59,6 @@ header = "options/uf_options.h" long = "uf-ss-fair" type = "bool" default = "true" - read_only = true help = "use fair strategy for finite model finding multiple sorts" [[option]] -- 2.30.2