[[option]]
name = "arithUnateLemmaMode"
- category = "regular"
+ category = "expert"
long = "unate-lemmas=MODE"
type = "ArithUnateLemmaMode"
default = "ALL"
[[option]]
name = "arithPropagationMode"
- category = "regular"
+ category = "expert"
long = "arith-prop=MODE"
type = "ArithPropagationMode"
default = "BOTH_PROP"
# defaults.
[[option]]
name = "arithHeuristicPivots"
- category = "regular"
+ category = "expert"
long = "heuristic-pivots=N"
type = "int64_t"
default = "0"
[[option]]
name = "arithErrorSelectionRule"
- category = "regular"
+ category = "expert"
long = "error-selection-rule=RULE"
type = "ErrorSelectionRule"
default = "MINIMUM_AMOUNT"
# The number of pivots before simplex rechecks every basic variable for a conflict
[[option]]
name = "arithSimplexCheckPeriod"
- category = "regular"
+ category = "expert"
long = "simplex-check-period=N"
type = "uint64_t"
default = "200"
# defaults.
[[option]]
name = "arithPivotThreshold"
- category = "regular"
+ category = "expert"
long = "pivot-threshold=N"
type = "uint64_t"
default = "2"
[[option]]
name = "arithPropagateMaxLength"
- category = "regular"
+ category = "expert"
long = "prop-row-length=N"
type = "uint64_t"
default = "16"
[[option]]
name = "arithDioSolver"
- category = "regular"
+ category = "expert"
long = "dio-solver"
type = "bool"
default = "true"
[[option]]
name = "arithMLTrick"
- category = "regular"
+ category = "expert"
long = "miplib-trick"
type = "bool"
default = "false"
[[option]]
name = "arithMLTrickSubstitutions"
- category = "regular"
+ category = "expert"
long = "miplib-trick-subs=N"
type = "uint64_t"
default = "1"
[[option]]
name = "doCutAllBounded"
- category = "regular"
+ category = "expert"
long = "cut-all-bounded"
type = "bool"
default = "false"
[[option]]
name = "maxCutsInContext"
- category = "regular"
+ category = "expert"
long = "maxCutsInContext=N"
type = "uint64_t"
default = "65535"
[[option]]
name = "revertArithModels"
- category = "regular"
+ category = "expert"
long = "revert-arith-models-on-unsat"
type = "bool"
default = "false"
[[option]]
name = "havePenalties"
- category = "regular"
+ category = "expert"
long = "fc-penalties"
type = "bool"
default = "false"
[[option]]
name = "useFC"
- category = "regular"
+ category = "expert"
long = "use-fcsimplex"
type = "bool"
default = "false"
[[option]]
name = "useSOI"
- category = "regular"
+ category = "expert"
long = "use-soi"
type = "bool"
default = "false"
[[option]]
name = "restrictedPivots"
- category = "regular"
+ category = "expert"
long = "restrict-pivots"
type = "bool"
default = "true"
[[option]]
name = "collectPivots"
- category = "regular"
+ category = "expert"
long = "collect-pivot-stats"
type = "bool"
default = "false"
[[option]]
name = "useApprox"
- category = "regular"
+ category = "expert"
long = "use-approx"
type = "bool"
default = "false"
[[option]]
name = "maxApproxDepth"
- category = "regular"
+ category = "expert"
long = "approx-branch-depth=N"
type = "int64_t"
default = "200"
[[option]]
name = "exportDioDecompositions"
- category = "regular"
+ category = "expert"
long = "dio-decomps"
type = "bool"
default = "false"
[[option]]
name = "newProp"
- category = "regular"
+ category = "expert"
long = "new-prop"
type = "bool"
default = "true"
[[option]]
name = "arithPropAsLemmaLength"
- category = "regular"
+ category = "expert"
long = "arith-prop-clauses=N"
type = "uint64_t"
default = "8"
[[option]]
name = "soiQuickExplain"
- category = "regular"
+ category = "expert"
long = "soi-qe"
type = "bool"
default = "false"
[[option]]
name = "trySolveIntStandardEffort"
- category = "regular"
+ category = "expert"
long = "se-solve-int"
type = "bool"
default = "false"
[[option]]
name = "replayFailureLemma"
- category = "regular"
+ category = "expert"
long = "lemmas-on-replay-failure"
type = "bool"
default = "false"
[[option]]
name = "dioSolverTurns"
- category = "regular"
+ category = "expert"
long = "dio-turns=N"
type = "int64_t"
default = "10"
[[option]]
name = "rrTurns"
- category = "regular"
+ category = "expert"
long = "rr-turns=N"
type = "int64_t"
default = "3"
[[option]]
name = "replayEarlyCloseDepths"
- category = "regular"
+ category = "expert"
long = "replay-early-close-depth=N"
type = "int64_t"
default = "1"
[[option]]
name = "replayNumericFailurePenalty"
- category = "regular"
+ category = "expert"
long = "replay-num-err-penalty=N"
type = "int64_t"
default = "4194304"
[[option]]
name = "replayRejectCutSize"
- category = "regular"
+ category = "expert"
long = "replay-reject-cut=N"
type = "uint64_t"
default = "25500"
[[option]]
name = "lemmaRejectCutSize"
- category = "regular"
+ category = "expert"
long = "replay-lemma-reject-cut=N"
type = "uint64_t"
default = "25500"
[[option]]
name = "ppAssertMaxSubSize"
- category = "regular"
+ category = "expert"
long = "pp-assert-max-sub-size=N"
type = "uint64_t"
default = "2"
[[option]]
name = "arithNoPartialFun"
- category = "regular"
+ category = "expert"
long = "arith-no-partial-fun"
type = "bool"
default = "false"
[[option]]
name = "pbRewrites"
- category = "regular"
+ category = "expert"
long = "pb-rewrites"
type = "bool"
default = "false"
[[option]]
name = "nlRlvAssertBounds"
- category = "regular"
+ category = "expert"
long = "nl-rlv-assert-bounds"
type = "bool"
default = "false"
[[option]]
name = "nlExtResBound"
- category = "regular"
+ category = "expert"
long = "nl-ext-rbound"
type = "bool"
default = "false"
[[option]]
name = "nlExtEntailConflicts"
- category = "regular"
+ category = "expert"
long = "nl-ext-ent-conf"
type = "bool"
default = "false"
[[option]]
name = "nlExtPurify"
- category = "regular"
+ category = "expert"
long = "nl-ext-purify"
type = "bool"
default = "false"
[[option]]
name = "nlExtSplitZero"
- category = "regular"
+ category = "expert"
long = "nl-ext-split-zero"
type = "bool"
default = "false"
[[option]]
name = "nlExtTfTaylorDegree"
- category = "regular"
+ category = "expert"
long = "nl-ext-tf-taylor-deg=N"
type = "int64_t"
default = "4"
[[option]]
name = "nlExtIncPrecision"
- category = "regular"
+ category = "expert"
long = "nl-ext-inc-prec"
type = "bool"
default = "true"
[[option]]
name = "nlRlvMode"
- category = "regular"
+ category = "expert"
long = "nl-rlv=MODE"
type = "NlRlvMode"
default = "NONE"
[[option]]
name = "nlCovVarElim"
- category = "regular"
+ category = "expert"
long = "nl-cov-var-elim"
type = "bool"
default = "true"
[[option]]
name = "nlCovPrune"
- category = "regular"
+ category = "expert"
long = "nl-cov-prune"
type = "bool"
default = "false"
[[option]]
name = "arithEqSolver"
- category = "regular"
+ category = "expert"
long = "arith-eq-solver"
type = "bool"
default = "false"
[[option]]
name = "arithCongMan"
- category = "regular"
+ category = "expert"
long = "arith-cong-man"
type = "bool"
default = "true"
[[option]]
name = "arraysOptimizeLinear"
- category = "regular"
+ category = "expert"
long = "arrays-optimize-linear"
type = "bool"
default = "true"
[[option]]
name = "arraysWeakEquivalence"
- category = "regular"
+ category = "expert"
long = "arrays-weak-equiv"
type = "bool"
default = "false"
[[option]]
name = "arraysEagerLemmas"
- category = "regular"
+ category = "expert"
long = "arrays-eager-lemmas"
type = "bool"
default = "false"
[[option]]
name = "arraysReduceSharing"
- category = "regular"
+ category = "expert"
long = "arrays-reduce-sharing"
type = "bool"
default = "false"
[[option]]
name = "arraysPropagate"
- category = "regular"
+ category = "expert"
long = "arrays-prop=N"
type = "int64_t"
default = "2"
[[option]]
name = "err"
- category = "regular"
+ category = "expert"
long = "err=erroutput"
type = "ManagedErr"
default = '{}'
[[option]]
name = "in"
- category = "regular"
+ category = "expert"
long = "in=input"
type = "ManagedIn"
default = '{}'
[[option]]
name = "out"
- category = "regular"
+ category = "expert"
long = "out=output"
type = "ManagedOut"
default = '{}'
[[option]]
name = "verbosity"
long = "verbosity=N"
- category = "regular"
+ category = "common"
type = "int64_t"
default = "0"
predicates = ["setVerbosity"]
[[option]]
name = "parseOnly"
- category = "regular"
+ category = "common"
long = "parse-only"
type = "bool"
default = "false"
[[option]]
name = "preprocessOnly"
- category = "regular"
+ category = "common"
long = "preprocess-only"
type = "bool"
default = "false"
[[option]]
short = "o"
+ category = "common"
long = "output=TAG"
type = "OutputTag"
default = "NONE"
predicates = ["enableOutputTag"]
- category = "regular"
help = "Enable output tag."
help_mode = "Output tags."
[[option.mode.NONE]]
[[option]]
name = "printSuccess"
- category = "regular"
+ category = "common"
long = "print-success"
type = "bool"
default = "false"
[[option]]
name = "bvSatSolver"
- category = "expert"
+ category = "regular"
long = "bv-sat-solver=MODE"
type = "SatSolverMode"
default = "CADICAL"
[[option]]
name = "bitvectorPropagate"
- category = "regular"
+ category = "expert"
long = "bv-propagate"
type = "bool"
default = "true"
[[option]]
name = "bvAssertInput"
- category = "regular"
+ category = "expert"
long = "bv-assert-input"
type = "bool"
default = "false"
[[option]]
name = "dtBinarySplit"
- category = "regular"
+ category = "expert"
long = "dt-binary-split"
type = "bool"
default = "false"
[[option]]
name = "cdtBisimilar"
- category = "regular"
+ category = "expert"
long = "cdt-bisimilar"
type = "bool"
default = "true"
[[option]]
name = "dtCyclic"
- category = "regular"
+ category = "expert"
long = "dt-cyclic"
type = "bool"
default = "true"
[[option]]
name = "dtInferAsLemmas"
- category = "regular"
+ category = "expert"
long = "dt-infer-as-lemmas"
type = "bool"
default = "false"
[[option]]
name = "dtBlastSplits"
- category = "regular"
+ category = "expert"
long = "dt-blast-splits"
type = "bool"
default = "false"
[[option]]
name = "dtNestedRec"
- category = "regular"
+ category = "expert"
long = "dt-nested-rec"
type = "bool"
default = "false"
[[option]]
name = "sygusSymBreakLazy"
- category = "regular"
+ category = "expert"
long = "sygus-sym-break-lazy"
type = "bool"
default = "true"
[[option]]
name = "sygusSymBreakRlv"
- category = "regular"
+ category = "expert"
long = "sygus-sym-break-rlv"
type = "bool"
default = "true"
[[option]]
name = "sygusFairMax"
- category = "regular"
+ category = "expert"
long = "sygus-fair-max"
type = "bool"
default = "true"
[[option]]
name = "defaultExprDepth"
- category = "regular"
+ category = "expert"
long = "expr-depth=N"
type = "int64_t"
default = "-1"
[[option]]
name = "defaultDagThresh"
- category = "regular"
+ category = "common"
long = "dag-thresh=N"
type = "int64_t"
default = "1"
[[option]]
name = "typeChecking"
- category = "regular"
+ category = "expert"
long = "type-checking"
type = "bool"
default = "DO_SEMANTIC_CHECKS_BY_DEFAULT"
[[option]]
name = "wellFormedChecking"
- category = "regular"
+ category = "expert"
long = "wf-checking"
type = "bool"
default = "true"
[[option]]
name = "fpExp"
- category = "regular"
+ category = "expert"
long = "fp-exp"
type = "bool"
default = "false"
[[option]]
name = "showDebugTags"
- category = "regular"
+ category = "expert"
long = "show-debug-tags"
type = "bool"
default = "false"
[[option]]
name = "showTraceTags"
- category = "regular"
+ category = "expert"
long = "show-trace-tags"
type = "bool"
default = "false"
[[option]]
name = "interactive"
- category = "regular"
+ category = "common"
long = "interactive"
type = "bool"
default = "false"
[[option]]
name = "segvSpin"
- category = "regular"
+ category = "expert"
long = "segv-spin"
type = "bool"
default = "false"
[[option]]
name = "dumpInstantiationsDebug"
- category = "regular"
+ category = "expert"
long = "dump-instantiations-debug"
type = "bool"
default = "false"
[[option]]
name = "forceNoLimitCpuWhileDump"
- category = "regular"
+ category = "expert"
long = "force-no-limit-cpu-while-dump"
type = "bool"
default = "false"
[[option]]
name = "semanticChecks"
long = "semantic-checks"
- category = "regular"
+ category = "expert"
type = "bool"
default = "DO_SEMANTIC_CHECKS_BY_DEFAULT"
help = "enable semantic checks, including type checks"
[[option]]
name = "forceLogicString"
- category = "expert"
+ category = "common"
long = "force-logic=LOGIC"
type = "std::string"
default = '""'
id = "PRINTER"
name = "Printing"
-[[option]]
- name = "flattenHOChains"
- category = "regular"
- long = "flatten-ho-chains"
- type = "bool"
- default = "false"
- help = "print (binary) application chains in a flattened way, e.g. (a b c) rather than ((a b) c)"
-
[[option]]
name = "printInstMode"
- category = "regular"
+ category = "common"
long = "print-inst=MODE"
type = "PrintInstMode"
default = "LIST"
type = "bool"
default = "false"
help = "when printing unsat cores, include unlabeled assertions"
+
+[[option]]
+ name = "flattenHOChains"
+ category = "expert"
+ long = "flatten-ho-chains"
+ type = "bool"
+ default = "false"
+ help = "print (binary) application chains in a flattened way, e.g. (a b c) rather than ((a b) c)"
+
+[[option]]
+ name = "modelUninterpPrint"
+ category = "regular"
+ long = "model-u-print=MODE"
+ type = "ModelUninterpPrintMode"
+ default = "None"
+ help = "determines how to print uninterpreted elements in models"
+ help_mode = "uninterpreted elements in models printing modes."
+[[option.mode.DeclSortAndFun]]
+ name = "decl-sort-and-fun"
+ help = "print uninterpreted elements declare-fun, and also include a declare-sort for the sort"
+[[option.mode.DeclFun]]
+ name = "decl-fun"
+ help = "print uninterpreted elements declare-fun, but don't include a declare-sort for the sort"
+[[option.mode.None]]
+ name = "none"
+ help = "(default) do not print declarations of uninterpreted elements in models."
[[option]]
name = "proofPrintConclusion"
- category = "regular"
+ category = "expert"
long = "proof-print-conclusion"
type = "bool"
default = "false"
[[option]]
name = "proofPedantic"
- category = "regular"
+ category = "expert"
long = "proof-pedantic=N"
type = "uint64_t"
default = "0"
[[option]]
name = "proofCheck"
- category = "regular"
+ category = "expert"
long = "proof-check=MODE"
type = "ProofCheckMode"
default = "LAZY"
[[option]]
name = "proofPpMerge"
- category = "regular"
+ category = "expert"
long = "proof-pp-merge"
type = "bool"
default = "true"
[[option]]
name = "proofAnnotate"
- category = "regular"
+ category = "expert"
long = "proof-annotate"
type = "bool"
default = "false"
[[option]]
name = "proofPruneInput"
- category = "regular"
+ category = "expert"
long = "proof-prune-input"
type = "bool"
default = "false"
[[option]]
name = "proofAletheResPivots"
- category = "regular"
+ category = "expert"
long = "proof-alethe-res-pivots"
type = "bool"
default = "false"
[[option]]
name = "proofDotDAG"
- category = "regular"
+ category = "expert"
long = "proof-dot-dag"
type = "bool"
default = "false"
[[option]]
name = "satRandomFreq"
alias = ["random-frequency"]
- category = "regular"
+ category = "expert"
long = "random-freq=P"
type = "double"
default = "0.0"
[[option]]
name = "satRandomSeed"
category = "regular"
- long = "random-seed=S"
+ long = "sat-random-seed=N"
type = "uint64_t"
default = "0"
help = "sets the random seed for the sat solver"
[[option]]
name = "satVarDecay"
- category = "regular"
+ category = "expert"
type = "double"
default = "0.95"
minimum = "0.0"
[[option]]
name = "satClauseDecay"
- category = "regular"
+ category = "expert"
type = "double"
default = "0.999"
minimum = "0.0"
[[option]]
name = "satRestartFirst"
- category = "regular"
+ category = "expert"
long = "restart-int-base=N"
type = "uint64_t"
default = "25"
[[option]]
name = "satRestartInc"
- category = "regular"
+ category = "expert"
long = "restart-int-inc=F"
type = "double"
default = "3.0"
[[option]]
name = "minisatSimpMode"
- category = "regular"
+ category = "expert"
long = "minisat-simplification=MODE"
type = "MinisatSimpMode"
default = "ALL"
[[option]]
name = "minisatDumpDimacs"
- category = "regular"
+ category = "expert"
long = "minisat-dump-dimacs"
type = "bool"
default = "false"
[[option]]
name = "dtVarExpandQuant"
- category = "regular"
+ category = "expert"
long = "dt-var-exp-quant"
type = "bool"
default = "true"
[[option]]
name = "condVarSplitQuant"
- category = "regular"
+ category = "expert"
long = "cond-var-split-quant=MODE"
type = "CondVarSplitQuantMode"
default = "ON"
# forall x. P( x ) => f( S( x ) ) = x
[[option]]
name = "preSkolemQuantNested"
- category = "regular"
+ category = "expert"
long = "pre-skolem-quant-nested"
type = "bool"
default = "true"
[[option]]
name = "globalNegate"
- category = "regular"
+ category = "expert"
long = "global-negate"
type = "bool"
default = "false"
[[option]]
name = "relevantTriggers"
- category = "expert"
+ category = "regular"
long = "relevant-triggers"
type = "bool"
default = "false"
[[option]]
name = "multiTriggerWhenSingle"
- category = "expert"
+ category = "regular"
long = "multi-trigger-when-single"
type = "bool"
default = "false"
[[option]]
name = "multiTriggerPriority"
- category = "expert"
+ category = "regular"
long = "multi-trigger-priority"
type = "bool"
default = "false"
[[option]]
name = "multiTriggerCache"
- category = "expert"
+ category = "regular"
long = "multi-trigger-cache"
type = "bool"
default = "false"
[[option]]
name = "multiTriggerLinear"
- category = "expert"
+ category = "regular"
long = "multi-trigger-linear"
type = "bool"
default = "true"
[[option]]
name = "triggerActiveSelMode"
- category = "regular"
+ category = "expert"
long = "trigger-active-sel=MODE"
type = "TriggerActiveSelMode"
default = "ALL"
[[option]]
name = "enumInstSum"
- category = "expert"
+ category = "regular"
long = "enum-inst-sum"
type = "bool"
default = "false"
[[option]]
name = "fmfOneInstPerRound"
- category = "expert"
+ category = "regular"
long = "mbqi-one-inst-per-round"
type = "bool"
default = "false"
[[option]]
name = "fmfTypeCompletionThresh"
- category = "expert"
+ category = "regular"
long = "fmf-type-completion-thresh=N"
type = "int64_t"
default = "1000"
[[option]]
name = "cbqiAllConflict"
- category = "expert"
+ category = "regular"
long = "cbqi-all-conflict"
type = "bool"
default = "false"
[[option]]
name = "sygusInference"
- category = "regular"
+ category = "expert"
long = "sygus-inference"
type = "bool"
default = "false"
help = "attempt to preprocess arbitrary inputs to sygus conjectures"
+# this is set to true for sygus inputs
[[option]]
name = "sygus"
category = "regular"
long = "sygus"
type = "bool"
default = "false"
- help = "use sygus solver (default is true for sygus inputs)"
+ help = "support SyGuS commands"
[[option]]
name = "cegqiSingleInvMode"
[[option]]
name = "cegqiSingleInvReconstructLimit"
- category = "regular"
+ category = "expert"
long = "sygus-si-rcons-limit=N"
type = "int64_t"
default = "10000"
[[option]]
name = "sygusConstRepairAbort"
- category = "regular"
+ category = "expert"
long = "sygus-crepair-abort"
type = "bool"
default = "false"
[[option]]
name = "sygusRepairConstTimeout"
- category = "regular"
+ category = "expert"
long = "sygus-repair-const-timeout=N"
type = "uint64_t"
default = "0"
[[option]]
name = "sygusInvTemplWhenSyntax"
- category = "regular"
+ category = "expert"
long = "sygus-inv-templ-when-sg"
type = "bool"
default = "false"
[[option]]
name = "cegisSample"
- category = "expert"
+ category = "regular"
long = "cegis-sample=MODE"
type = "CegisSampleMode"
default = "NONE"
[[option]]
name = "sygusRewVerify"
- category = "regular"
+ category = "expert"
long = "sygus-rr-verify"
type = "bool"
default = "false"
[[option]]
name = "sygusExprMinerCheckTimeout"
- category = "regular"
+ category = "expert"
long = "sygus-expr-miner-check-timeout=N"
type = "uint64_t"
default = "0"
[[option]]
name = "sygusQueryGen"
- category = "regular"
+ category = "expert"
long = "sygus-query-gen=MODE"
type = "SygusQueryGenMode"
default = "NONE"
[[option]]
name = "sygusQueryGenDumpFiles"
- category = "regular"
+ category = "expert"
long = "sygus-query-gen-dump-files=MODE"
type = "SygusQueryDumpFilesMode"
default = "NONE"
[[option]]
name = "cegqiInnermost"
- category = "expert"
+ category = "regular"
long = "cegqi-innermost"
type = "bool"
default = "true"
[[option]]
name = "cegqiNestedQE"
- category = "expert"
+ category = "regular"
long = "cegqi-nested-qe"
type = "bool"
default = "false"
[[option]]
name = "cegqiUseInfInt"
- category = "expert"
- long = "cegqi-use-inf-int"
+ category = "regular"
+ long = "cegqi-inf-int"
type = "bool"
default = "false"
help = "use integer infinity for vts in counterexample-based quantifier instantiation"
[[option]]
name = "cegqiUseInfReal"
- category = "expert"
- long = "cegqi-use-inf-real"
+ category = "regular"
+ long = "cegqi-inf-real"
type = "bool"
default = "false"
help = "use real infinity for vts in counterexample-based quantifier instantiation"
[[option]]
name = "cegqiMidpoint"
- category = "expert"
+ category = "regular"
long = "cegqi-midpoint"
type = "bool"
default = "false"
[[option]]
name = "quantDynamicSplit"
category = "regular"
- long = "quant-dsplit-mode=MODE"
+ long = "quant-dsplit=MODE"
type = "QuantDSplitMode"
default = "DEFAULT"
help = "mode for dynamic quantifiers splitting"
[[option]]
name = "hoElim"
- category = "expert"
+ category = "regular"
long = "ho-elim"
type = "bool"
default = "false"
[[option]]
name = "hoElimStoreAx"
- category = "expert"
+ category = "regular"
long = "ho-elim-store-ax"
type = "bool"
default = "true"
[[option]]
name = "sepMinimalRefine"
- category = "regular"
+ category = "expert"
long = "sep-min-refine"
type = "bool"
default = "false"
[[option]]
name = "sepPreSkolemEmp"
- category = "regular"
+ category = "expert"
long = "sep-pre-skolem-emp"
type = "bool"
default = "false"
[[option]]
name = "setsExt"
- category = "expert"
+ category = "regular"
long = "sets-ext"
type = "bool"
default = "false"
default = "false"
help = "rewrite the input based on learned literals"
-[[option]]
- name = "expandDefinitions"
- long = "expand-definitions"
- category = "regular"
- type = "bool"
- default = "false"
- help = "always expand symbol definitions in output"
-
[[option]]
name = "produceModels"
category = "common"
[[option]]
name = "checkModels"
- category = "regular"
+ category = "common"
long = "check-models"
type = "bool"
default = "false"
[[option]]
name = "debugCheckModels"
- category = "regular"
+ category = "expert"
long = "debug-check-models"
type = "bool"
default = "false"
[[option]]
name = "blockModelsMode"
- category = "regular"
+ category = "expert"
long = "block-models=MODE"
type = "BlockModelsMode"
default = "NONE"
[[option]]
name = "unsatCoresMode"
- category = "regular"
+ category = "expert"
long = "unsat-cores-mode=MODE"
type = "UnsatCoresMode"
default = "OFF"
[[option]]
name = "minimalUnsatCores"
- category = "regular"
+ category = "expert"
long = "minimal-unsat-cores"
type = "bool"
default = "false"
[[option]]
name = "difficultyMode"
- category = "regular"
+ category = "expert"
long = "difficulty-mode=MODE"
type = "DifficultyMode"
default = "LEMMA_LITERAL"
[[option]]
name = "produceAssertions"
- category = "common"
+ category = "regular"
long = "produce-assertions"
type = "bool"
alias = ["interactive-mode"]
[[option]]
name = "extRewPrep"
- category = "expert"
+ category = "regular"
long = "ext-rew-prep=MODE"
type = "ExtRewPrepMode"
default = "OFF"
default = "false"
help = "in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard"
-[[option]]
- name = "modelUninterpPrint"
- alias = ["model-uninterp-print"]
- category = "regular"
- long = "model-u-print=MODE"
- type = "ModelUninterpPrintMode"
- default = "None"
- help = "determines how to print uninterpreted elements in models"
- help_mode = "uninterpreted elements in models printing modes."
-[[option.mode.DeclSortAndFun]]
- name = "decl-sort-and-fun"
- help = "print uninterpreted elements declare-fun, and also include a declare-sort for the sort"
-[[option.mode.DeclFun]]
- name = "decl-fun"
- help = "print uninterpreted elements declare-fun, but don't include a declare-sort for the sort"
-[[option.mode.None]]
- name = "none"
- help = "(default) do not print declarations of uninterpreted elements in models."
-
[[option]]
name = "foreignTheoryRewrite"
category = "expert"
[[option]]
name = "solveBVAsInt"
- category = "expert"
+ category = "regular"
long = "solve-bv-as-int=MODE"
type = "SolveBVAsIntMode"
default = "OFF"
[[option]]
name = "solveIntAsBV"
- category = "expert"
+ category = "regular"
long = "solve-int-as-bv=N"
type = "uint64_t"
default = "0"
[[option]]
name = "solveRealAsInt"
- category = "expert"
+ category = "regular"
long = "solve-real-as-int"
type = "bool"
default = "false"
[[option]]
name = "stringEager"
- category = "regular"
+ category = "expert"
long = "strings-eager"
type = "bool"
default = "false"
[[option]]
name = "stringLenNorm"
- category = "regular"
+ category = "expert"
long = "strings-len-norm"
type = "bool"
default = "true"
[[option]]
name = "stringInferSym"
- category = "regular"
+ category = "expert"
long = "strings-infer-sym"
type = "bool"
default = "true"
[[option]]
name = "stringEagerLen"
- category = "regular"
+ category = "expert"
long = "strings-eager-len"
type = "bool"
default = "true"
[[option]]
name = "stringProcessLoopMode"
- category = "expert"
+ category = "regular"
long = "strings-process-loop-mode=MODE"
type = "ProcessLoopMode"
default = "FULL"
[[option]]
name = "stringInferAsLemmas"
- category = "regular"
+ category = "expert"
long = "strings-infer-as-lemmas"
type = "bool"
default = "false"
[[option]]
name = "stringRExplainLemmas"
- category = "regular"
+ category = "expert"
long = "strings-rexplain-lemmas"
type = "bool"
default = "true"
[[option]]
name = "stringMinPrefixExplain"
- category = "regular"
+ category = "expert"
long = "strings-min-prefix-explain"
type = "bool"
default = "true"
[[option]]
name = "stringFlatForms"
- category = "regular"
+ category = "expert"
long = "strings-ff"
type = "bool"
default = "true"
[[option]]
name = "stringRegExpInterMode"
- category = "expert"
+ category = "regular"
long = "re-inter-mode=MODE"
type = "RegExpInterMode"
default = "CONSTANT"
[[option]]
name = "stringUnifiedVSpt"
- category = "regular"
+ category = "expert"
long = "strings-unified-vspt"
type = "bool"
default = "true"
[[option]]
name = "stringsAlphaCard"
- category = "regular"
+ category = "expert"
long = "strings-alpha-card=N"
type = "uint64_t"
default = "196608"
[[option]]
name = "stringsModelMaxLength"
- category = "regular"
+ category = "expert"
long = "strings-model-max-len=N"
type = "uint64_t"
default = "65536"
[[option]]
name = "assignFunctionValues"
- category = "regular"
+ category = "expert"
long = "assign-function-values"
type = "bool"
default = "true"
[[option]]
name = "condenseFunctionValues"
- category = "regular"
+ category = "expert"
long = "condense-function-values"
type = "bool"
default = "true"
[[option]]
name = "relevanceFilter"
- category = "regular"
+ category = "expert"
long = "relevance-filter"
type = "bool"
default = "false"
[[option]]
name = "ufSymmetryBreaker"
- alias = ["uf-symmetry-breaker"]
- category = "regular"
+ category = "expert"
long = "symmetry-breaker"
type = "bool"
default = "true"
[[option]]
name = "ufssFairnessMonotone"
- category = "regular"
+ category = "expert"
long = "uf-ss-fair-monotone"
type = "bool"
default = "false"
; EXPECT: 2
; EXPECT: sat
; EXPECT: 0
-; EXPECT: (error "Invalid call to 'setOption' for option 'random-seed', solver is already fully initialized")
+; EXPECT: (error "Invalid call to 'setOption' for option 'sat-random-seed', solver is already fully initialized")
; EXIT: 1
(get-option :verbosity)
(set-option :verbosity 1)
(get-option :verbosity)
(set-option :verbosity 0)
-(get-option :random-seed)
-(set-option :random-seed 2)
-(get-option :random-seed)
+(get-option :sat-random-seed)
+(set-option :sat-random-seed 2)
+(get-option :sat-random-seed)
(set-logic QF_UF)
(declare-fun x () Bool)
(set-option :verbosity 0)
(get-option :verbosity)
-(set-option :random-seed 1)
\ No newline at end of file
+(set-option :sat-random-seed 1)
(set-logic LIRA)
(set-info :status unsat)
-(set-option :cegqi-use-inf-int true)
-(set-option :cegqi-use-inf-real true)
+(set-option :cegqi-inf-int true)
+(set-option :cegqi-inf-real true)
(set-option :var-ineq-elim-quant false)
(assert (forall (( b Real )) (forall (( c Int )) (and (> c (* b 2 ))))))
(check-sat)
-; COMMAND-LINE: --cegqi-use-inf-int --cegqi-use-inf-real
+; COMMAND-LINE: --cegqi-inf-int --cegqi-inf-real
; EXPECT: unsat
(set-info :smt-lib-version 2.6)
(set-logic LRA)
projects / cvc5.git / commitdiff