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.
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-<long> alternative option
false: omit --no-<long> alternative option
help ... (string) documentation (required if category is not
handler = "stringToOutputLanguage"
predicates = []
includes = ["options/language.h"]
- read_only = false
help = "force output language (default is \"auto\"; see --output-lang help)"
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]]
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]]
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]]
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
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]]
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
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]]
long = "maxCutsInContext=N"
type = "unsigned"
default = "65535"
- read_only = true
help = "maximum cuts in a given context before signalling a restart"
[[option]]
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]]
long = "se-solve-int"
type = "bool"
default = "false"
- read_only = true
help = "attempt to use the approximate solve integer method on standard effort"
[[option]]
long = "lemmas-on-replay-failure"
type = "bool"
default = "false"
- read_only = true
help = "attempt to use external lemmas if approximate solve integer failed"
[[option]]
long = "dio-turns=N"
type = "int"
default = "10"
- read_only = true
help = "turns in a row dio solver cutting gets"
[[option]]
long = "rr-turns=N"
type = "int"
default = "3"
- read_only = true
help = "round robin turn"
[[option]]
long = "dio-repeat"
type = "bool"
default = "false"
- read_only = true
help = "handle dio solver constraints in mass or one at a time"
[[option]]
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]]
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]]
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]]
long = "replay-reject-cut=N"
type = "unsigned"
default = "25500"
- read_only = true
help = "maximum complexity of any coefficient while replaying cuts"
[[option]]
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]]
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]]
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]]
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]]
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]]
long = "pp-assert-max-sub-size=N"
type = "unsigned"
default = "2"
- read_only = true
help = "threshold for substituting an equality in ppAssert"
[[option]]
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]]
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]]
long = "nl-ext-factor"
type = "bool"
default = "true"
- read_only = true
help = "use factoring inference in non-linear incremental linearization solver"
[[option]]
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]]
long = "nl-ext-ent-conf"
type = "bool"
default = "false"
- read_only = true
help = "check for entailed conflicts in non-linear solver"
[[option]]
long = "nl-ext-rewrite"
type = "bool"
default = "true"
- read_only = true
help = "do context-dependent simplification based on rewrites in non-linear solver"
[[option]]
long = "nl-ext-purify"
type = "bool"
default = "false"
- read_only = true
help = "purify non-linear terms at preprocess"
[[option]]
long = "nl-ext-split-zero"
type = "bool"
default = "false"
- read_only = true
help = "initial splits on zero for all variables"
[[option]]
long = "nl-ext-inc-prec"
type = "bool"
default = "true"
- read_only = true
help = "whether to increment the precision for irrational function constraints"
[[option]]
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]]
long = "verbose"
type = "void"
handler = "increaseVerbosity"
- read_only = true
help = "increase verbosity (may be repeated)"
[[option]]
long = "quiet"
type = "void"
handler = "decreaseVerbosity"
- read_only = true
help = "decrease verbosity (may be repeated)"
[[option]]
category = "common"
type = "bool"
predicates = ["setStats"]
- read_only = true
help = "give statistics on exit"
[[option]]
category = "expert"
type = "bool"
predicates = ["setStats"]
- read_only = true
help = "print unchanged (defaulted) statistics as well"
[[option]]
category = "expert"
type = "bool"
predicates = ["setStats"]
- read_only = true
help = "print expert (non-public) statistics as well"
[[option]]
type = "bool"
predicates = ["setStats"]
default = "false"
- read_only = true
help = "in incremental mode, print stats after every satisfiability or validity query"
[[option]]
category = "regular"
long = "preprocess-only"
type = "bool"
- read_only = true
help = "exit after preprocessing input"
[[option]]
long = "trace=TAG"
type = "std::string"
handler = "enableTraceTag"
- read_only = true
help = "trace something (e.g. -t pushpop), can repeat"
[[option]]
long = "debug=TAG"
type = "std::string"
handler = "enableDebugTag"
- read_only = true
help = "debug something (e.g. -d arith), can repeat"
[[option]]
category = "regular"
long = "print-success"
type = "bool"
- read_only = true
help = "print the \"success\" output required of SMT-LIBv2"
long = "bv-num-func=N"
type = "unsigned"
default = "1"
- read_only = true
help = "number of function symbols in conflicts that are generalized"
[[option]]
long = "bv-quick-xplain"
type = "bool"
default = "false"
- read_only = true
help = "minimize bv conflicts using the QuickXplain algorithm"
[[option]]
long = "bv-gauss-elim"
type = "bool"
default = "false"
- read_only = true
help = "simplify formula via Gaussian Elimination if applicable"
[[option]]
long = "dt-polite-optimize"
type = "bool"
default = "true"
- read_only = true
help = "turn on optimization for polite combination"
[[option]]
long = "dt-binary-split"
type = "bool"
default = "false"
- read_only = true
help = "do binary splits for datatype constructor types"
[[option]]
long = "cdt-bisimilar"
type = "bool"
default = "true"
- read_only = true
help = "do bisimilarity check for co-datatypes"
[[option]]
long = "dt-cyclic"
type = "bool"
default = "true"
- read_only = true
help = "do cyclicity check for datatypes"
[[option]]
long = "dt-infer-as-lemmas"
type = "bool"
default = "false"
- read_only = true
help = "always send lemmas out instead of making internal inferences"
[[option]]
long = "dt-blast-splits"
type = "bool"
default = "false"
- read_only = true
help = "when applicable, blast splitting lemmas for all variables at once"
[[option]]
long = "dt-nested-rec"
type = "bool"
default = "false"
- read_only = true
help = "allow nested recursion in datatype definitions"
[[option]]
long = "dt-share-sel"
type = "bool"
default = "true"
- read_only = true
help = "internally use shared selectors across multiple constructors"
[[option]]
long = "sygus-sym-break"
type = "bool"
default = "true"
- read_only = true
help = "simple sygus symmetry breaking lemmas"
[[option]]
long = "sygus-sym-break-agg"
type = "bool"
default = "true"
- read_only = true
help = "use aggressive checks for simple sygus symmetry breaking lemmas"
[[option]]
long = "sygus-sym-break-dynamic"
type = "bool"
default = "true"
- read_only = true
help = "dynamic sygus symmetry breaking lemmas"
[[option]]
long = "sygus-sym-break-lazy"
type = "bool"
default = "true"
- read_only = true
help = "lazily add symmetry breaking lemmas for terms"
[[option]]
long = "sygus-sym-break-rlv"
type = "bool"
default = "true"
- read_only = true
help = "add relevancy conditions to symmetry breaking lemmas"
[[option]]
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]]
long = "sygus-fair-max"
type = "bool"
default = "true"
- read_only = true
help = "use max instead of sum for multi-function sygus conjectures"
[[option]]
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)"
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]]
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"
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]]
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]]
type = "int"
default = "0"
predicates = ["setDefaultExprDepthPredicate"]
- read_only = true
help = "print exprs to depth N (0 == default, -1 == no limit)"
[[option]]
type = "int"
default = "1"
predicates = ["setDefaultDagThreshPredicate"]
- read_only = true
help = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)"
[[option]]
long = "type-checking"
type = "bool"
default = "DO_SEMANTIC_CHECKS_BY_DEFAULT"
- read_only = true
help = "type check expressions"
short = "V"
long = "version"
type = "bool"
- read_only = true
alternate = false
help = "identify this cvc5 binary"
short = "h"
long = "help"
type = "bool"
- read_only = true
alternate = false
help = "full command line reference"
long = "show-config"
type = "void"
handler = "showConfiguration"
- read_only = true
help = "show cvc5 static configuration"
[[option]]
long = "copyright"
type = "void"
handler = "copyright"
- read_only = true
help = "show cvc5 copyright information"
[[option]]
long = "seed=N"
type = "uint64_t"
default = "0"
- read_only = true
help = "seed for random number generator"
[[option]]
long = "show-debug-tags"
type = "void"
handler = "showDebugTags"
- read_only = true
help = "show all available tags for debugging"
[[option]]
long = "show-trace-tags"
type = "void"
handler = "showTraceTags"
- read_only = true
help = "show all available tags for tracing"
[[option]]
long = "early-exit"
type = "bool"
default = "true"
- read_only = true
help = "do not run destructors at exit; default on except in debug builds"
[[option]]
long = "interactive-prompt"
type = "bool"
default = "true"
- read_only = true
help = "interactive prompting while in interactive mode"
[[option]]
long = "segv-spin"
type = "bool"
default = "false"
- read_only = true
help = "spin on segfault/other crash waiting for gdb"
[[option]]
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"
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'
]
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);"""
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
def perr(filename, msg, option = None):
+ msg_suffix = ''
if option:
if option.name:
msg_suffix = "option '{}' ".format(option.name)
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:
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))
### 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))
category = "common"
long = "strict-parsing"
type = "bool"
- read_only = true
help = "be less tolerant of non-conforming inputs"
[[option]]
category = "regular"
long = "mmap"
type = "bool"
- read_only = true
help = "memory map file input"
[[option]]
category = "regular"
type = "bool"
default = "DO_SEMANTIC_CHECKS_BY_DEFAULT"
- read_only = true
help = "enable semantic checks, including type checks"
[[option]]
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
long = "filesystem-access"
type = "bool"
default = "true"
- read_only = true
[[option]]
name = "forceLogicString"
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"
long = "proof-print-conclusion"
type = "bool"
default = "false"
- read_only = true
help = "Print conclusion of proof steps when printing AST"
[[option]]
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]]
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]]
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]]
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]]
long = "refine-conflicts"
type = "bool"
default = "false"
- read_only = true
help = "refine theory conflict clauses (default false)"
[[option]]
long = "minisat-dump-dimacs"
type = "bool"
default = "false"
- read_only = true
help = "instead of solving minisat dumps the asserted clauses in Dimacs format"
long = "var-elim-quant"
type = "bool"
default = "true"
- read_only = true
help = "enable simple variable elimination for quantified formulas"
[[option]]
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]]
long = "dt-var-exp-quant"
type = "bool"
default = "true"
- read_only = true
help = "expand datatype variables bound to one constructor in quantifiers"
[[option]]
long = "cond-var-split-quant"
type = "bool"
default = "true"
- read_only = true
help = "split quantified formulas that lead to variable eliminations"
[[option]]
long = "cond-var-split-agg-quant"
type = "bool"
default = "false"
- read_only = true
help = "aggressive split quantified formulas that lead to variable eliminations"
[[option]]
long = "ag-miniscope-quant"
type = "bool"
default = "false"
- read_only = true
help = "perform aggressive miniscoping for quantifiers"
[[option]]
long = "elim-taut-quant"
type = "bool"
default = "true"
- read_only = true
help = "eliminate tautological disjuncts of quantified formulas"
[[option]]
long = "ext-rewrite-quant"
type = "bool"
default = "false"
- read_only = true
help = "apply extended rewriting to bodies of quantified formulas"
[[option]]
long = "register-quant-body-terms"
type = "bool"
default = "false"
- read_only = true
help = "consider ground terms within bodies of quantified formulas for matching"
[[option]]
long = "strict-triggers"
type = "bool"
default = "false"
- read_only = true
help = "only instantiate quantifiers with user patterns based on triggers"
[[option]]
long = "relevant-triggers"
type = "bool"
default = "false"
- read_only = true
help = "prefer triggers that are more relevant based on SInE style analysis"
[[option]]
long = "relational-triggers"
type = "bool"
default = "false"
- read_only = true
help = "choose relational triggers such as x = f(y), x >= f(y)"
[[option]]
long = "multi-trigger-when-single"
type = "bool"
default = "false"
- read_only = true
help = "select multi triggers when single triggers exist"
[[option]]
long = "multi-trigger-priority"
type = "bool"
default = "false"
- read_only = true
help = "only try multi triggers if single triggers give no instantiations"
[[option]]
long = "multi-trigger-cache"
type = "bool"
default = "false"
- read_only = true
help = "caching version of multi triggers"
[[option]]
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.
long = "increment-triggers"
type = "bool"
default = "true"
- read_only = true
help = "generate additional triggers as needed during search"
[[option]]
long = "inst-level-input-only"
type = "bool"
default = "true"
- read_only = true
help = "only input terms are assigned instantiation level zero"
[[option]]
long = "full-saturate-quant-rd"
type = "bool"
default = "true"
- read_only = true
help = "whether to use relevant domain first for enumerative instantiation strategy"
[[option]]
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]]
long = "fs-interleave"
type = "bool"
default = "false"
- read_only = true
help = "interleave enumerative instantiation with other techniques"
[[option]]
long = "fs-stratify"
type = "bool"
default = "false"
- read_only = true
help = "stratify effort levels in enumerative instantiation, which favors speed over fairness"
[[option]]
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]]
long = "literal-matching=MODE"
type = "LiteralMatchMode"
default = "USE"
- read_only = true
help = "choose literal matching mode"
help_mode = "Literal match modes."
[[option.mode.NONE]]
long = "quant-fun-wd"
type = "bool"
default = "false"
- read_only = true
help = "assume that function defined by quantifiers are well defined"
[[option]]
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]]
long = "mbqi-interleave"
type = "bool"
default = "false"
- read_only = true
help = "interleave model-based quantifier instantiation with other techniques"
[[option]]
long = "fmf-fresh-dc"
type = "bool"
default = "false"
- read_only = true
help = "use fresh distinguished representative when applying Inst-Gen techniques"
[[option]]
long = "fmf-fmc-simple"
type = "bool"
default = "true"
- read_only = true
help = "simple models in full model check for finite model finding"
[[option]]
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]]
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]]
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]]
long = "qcf-nested-conflict"
type = "bool"
default = "false"
- read_only = true
help = "consider conflicts for nested quantifiers"
[[option]]
long = "qcf-vo-exp"
type = "bool"
default = "false"
- read_only = true
help = "qcf experimental variable ordering"
[[option]]
long = "qcf-eager-test"
type = "bool"
default = "true"
- read_only = true
help = "optimization, test qcf instances eagerly"
[[option]]
long = "qcf-eager-check-rd"
type = "bool"
default = "true"
- read_only = true
help = "optimization, eagerly check relevant domain of matched position"
[[option]]
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
long = "quant-ind"
type = "bool"
default = "false"
- read_only = true
help = "use all available techniques for inductive reasoning"
[[option]]
long = "conjecture-gen-per-round=N"
type = "int"
default = "1"
- read_only = true
help = "number of conjectures to generate per instantiation round"
[[option]]
long = "conjecture-no-filter"
type = "bool"
default = "false"
- read_only = true
help = "do not filter conjectures"
[[option]]
long = "conjecture-gen-gt-enum=N"
type = "int"
default = "50"
- read_only = true
help = "number of ground terms to generate for model filtering"
[[option]]
long = "conjecture-gen-uee-intro"
type = "bool"
default = "false"
- read_only = true
help = "more aggressive merging for universal equality engine, introduces terms"
[[option]]
long = "conjecture-gen-max-depth=N"
type = "int"
default = "3"
- read_only = true
help = "maximum depth of terms to consider for conjectures"
### Synthesis options
long = "sygus-inference"
type = "bool"
default = "false"
- read_only = false
help = "attempt to preprocess arbitrary inputs to sygus conjectures"
[[option]]
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
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]]
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]]
long = "sygus-si-abort"
type = "bool"
default = "false"
- read_only = true
help = "abort if synthesis conjecture is not single invocation"
[[option]]
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
long = "sygus-qe-preproc"
type = "bool"
default = "false"
- read_only = true
help = "use quantifier elimination as a preprocessing step for sygus"
[[option]]
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]]
long = "sygus-min-grammar"
type = "bool"
default = "true"
- read_only = true
help = "statically minimize sygus grammars"
[[option]]
long = "sygus-add-const-grammar"
type = "bool"
default = "false"
- read_only = true
help = "statically add constants appearing in conjecture to grammars"
[[option]]
long = "sygus-grammar-norm"
type = "bool"
default = "false"
- read_only = true
help = "statically normalize sygus grammars based on flattening (linearization)"
[[option]]
long = "sygus-templ-embed-grammar"
type = "bool"
default = "false"
- read_only = true
help = "embed sygus templates into grammars"
[[option]]
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]]
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]]
long = "sygus-eval-unfold"
type = "bool"
default = "true"
- read_only = true
help = "do unfolding of sygus evaluation functions"
[[option]]
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]]
long = "sygus-rr"
type = "bool"
default = "false"
- read_only = true
help = "use sygus to enumerate and verify correctness of rewrite rules"
[[option]]
long = "sygus-sample-grammar"
type = "bool"
default = "true"
- read_only = true
help = "when applicable, use grammar for choosing sample points"
[[option]]
long = "cegqi-min-bounds"
type = "bool"
default = "false"
- read_only = true
help = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation"
[[option]]
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]]
long = "cegqi-nopt"
type = "bool"
default = "true"
- read_only = true
help = "non-optimal bounds for counterexample-based quantifier instantiation"
# CEGQI for BV
long = "quant-alpha-equiv"
type = "bool"
default = "true"
- read_only = true
help = "infer alpha equivalence between quantified formulas"
[[option]]
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]]
long = "ho-matching"
type = "bool"
default = "true"
- read_only = true
help = "do higher-order matching algorithm for triggers with variable operators"
[[option]]
long = "ho-matching-var-priority"
type = "bool"
default = "true"
- read_only = true
help = "give priority to variable arguments over constant arguments"
[[option]]
long = "ho-merge-term-db"
type = "bool"
default = "true"
- read_only = true
help = "merge term indices modulo equality"
[[option]]
long = "ho-elim"
type = "bool"
default = "false"
- read_only = true
help = "eagerly eliminate higher-order constraints"
[[option]]
long = "ho-elim-store-ax"
type = "bool"
default = "true"
- read_only = false
help = "use store axiom during ho-elim"
### Output options
long = "rweight=VAL=N"
type = "std::string"
handler = "setResourceWeight"
- read_only = true
help = "set a single resource weight"
[[option]]
long = "sep-check-neg"
type = "bool"
default = "true"
- read_only = true
help = "check negated spatial assertions"
[[option]]
long = "sep-exp"
type = "bool"
default = "false"
- read_only = true
help = "experimental flag for sep"
[[option]]
long = "sep-min-refine"
type = "bool"
default = "false"
- read_only = true
help = "only add refinement lemmas for minimal (innermost) assertions"
[[option]]
long = "sep-deq-c"
type = "bool"
default = "true"
- read_only = true
help = "assume cardinality elements are distinct"
[[option]]
long = "sep-pre-skolem-emp"
type = "bool"
default = "false"
- read_only = true
help = "eliminate emp constraint at preprocess time"
[[option]]
long = "sep-child-refine"
type = "bool"
default = "false"
- read_only = true
help = "child-specific refinements of negated star, positive wand"
long = "sets-proxy-lemmas"
type = "bool"
default = "false"
- read_only = true
help = "introduce proxy variables eagerly to shorten lemmas"
[[option]]
long = "sets-infer-as-lemmas"
type = "bool"
default = "true"
- read_only = true
help = "send inferences as lemmas"
[[option]]
long = "sets-ext"
type = "bool"
default = "false"
- read_only = true
help = "enable extended symbols such as complement and universe in theory of sets"
category = "common"
long = "dump=MODE"
type = "std::string"
- read_only = true
help = "dump preprocessed assertions, etc., see --dump=help"
[[option]]
category = "common"
long = "dump-to=FILE"
type = "std::string"
- read_only = true
help = "all dumping goes to FILE (instead of stdout)"
[[option]]
long = "static-learning"
type = "bool"
default = "true"
- read_only = true
help = "use static learning (on by default)"
[[option]]
category = "regular"
type = "bool"
default = "false"
- read_only = true
help = "always expand symbol definitions in output"
[[option]]
long = "dump-models"
type = "bool"
default = "false"
- read_only = true
help = "output models after every SAT/INVALID/UNKNOWN response"
[[option]]
long = "dump-proofs"
type = "bool"
default = "false"
- read_only = true
help = "output proofs after every UNSAT/VALID response"
[[option]]
long = "dump-instantiations"
type = "bool"
default = "false"
- read_only = true
help = "output instantiations of quantified formulas after every UNSAT/VALID response"
[[option]]
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]]
long = "dump-unsat-cores-full"
type = "bool"
default = "false"
- read_only = true
help = "dump the full unsat core, including unlabeled assertions"
[[option]]
long = "produce-unsat-assumptions"
type = "bool"
default = "false"
- read_only = true
help = "turn on unsat assumptions generation"
[[option]]
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]]
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]]
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]]
long = "model-witness-value"
type = "bool"
default = "false"
- read_only = true
help = "in models, use a witness constant for choice functions"
[[option]]
smt_name = "regular-output-channel"
category = "regular"
type = "std::string"
- read_only = true
help = "set the regular output channel of the solver"
[[option]]
smt_name = "diagnostic-output-channel"
category = "regular"
type = "std::string"
- read_only = true
help = "set the diagnostic output channel of the solver"
[[option]]
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]]
long = "foreign-theory-rewrite"
type = "bool"
default = "false"
- read_only = true
help = "Cross-theory rewrites"
[[option]]
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]]
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]]
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]]
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]]
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]]
long = "produce-abducts"
type = "bool"
default = "false"
- read_only = true
help = "support the get-abduct command"
[[option]]
long = "check-interpols"
type = "bool"
default = "false"
- read_only = true
help = "checks whether produced solutions to get-interpol are correct"
[[option]]
long = "check-abducts"
type = "bool"
default = "false"
- read_only = true
help = "checks whether produced solutions to get-abduct are correct"
long = "strings-eager"
type = "bool"
default = "false"
- read_only = true
help = "strings eager check"
[[option]]
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]]
long = "strings-lazy-pp"
type = "bool"
default = "true"
- read_only = true
help = "perform string preprocessing lazily"
[[option]]
long = "strings-len-norm"
type = "bool"
default = "true"
- read_only = true
help = "strings length normalization lemma"
[[option]]
long = "strings-infer-sym"
type = "bool"
default = "true"
- read_only = true
help = "strings split on empty string"
[[option]]
long = "strings-eager-len"
type = "bool"
default = "true"
- read_only = true
help = "strings eager length lemmas"
[[option]]
long = "strings-check-entail-len"
type = "bool"
default = "true"
- read_only = true
help = "check entailment between length terms to reduce splitting"
[[option]]
long = "strings-infer-as-lemmas"
type = "bool"
default = "false"
- read_only = true
help = "always send lemmas out instead of making internal inferences"
[[option]]
long = "strings-rexplain-lemmas"
type = "bool"
default = "true"
- read_only = true
help = "regression explanations for string lemmas"
[[option]]
long = "strings-min-prefix-explain"
type = "bool"
default = "true"
- read_only = true
help = "minimize explanations for prefix of normal forms in strings"
[[option]]
long = "strings-guess-model"
type = "bool"
default = "false"
- read_only = true
help = "use model guessing to avoid string extended function reductions"
[[option]]
long = "strings-lprop-csp"
type = "bool"
default = "false"
- read_only = true
help = "do length propagation based on constant splits"
[[option]]
long = "strings-ff"
type = "bool"
default = "true"
- read_only = true
help = "do flat form inferences"
[[option]]
long = "strings-unified-vspt"
type = "bool"
default = "true"
- read_only = true
help = "use a single skolem for the variable splitting rule"
[[option]]
long = "condense-function-values"
type = "bool"
default = "true"
- read_only = true
help = "condense values for functions in models rather than explicitly representing them"
[[option]]
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]]
long = "uf-ss-totality-sym-break"
type = "bool"
default = "false"
- read_only = true
help = "apply symmetry breaking for totality axioms"
[[option]]
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]]
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]]
long = "uf-ss-fair"
type = "bool"
default = "true"
- read_only = true
help = "use fair strategy for finite model finding multiple sorts"
[[option]]
projects / cvc5.git / commitdiff