From 59e78c5cab0da7973c76c67818dac6154f5ff1b0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 24 Mar 2022 20:56:48 -0500 Subject: [PATCH] Recategorize options (#8386) --- src/options/arith_options.toml | 94 +++++++++---------- src/options/arrays_options.toml | 10 +- src/options/base_options.toml | 16 ++-- src/options/bv_options.toml | 6 +- src/options/datatypes_options.toml | 18 ++-- src/options/expr_options.toml | 8 +- src/options/fp_options.toml | 2 +- src/options/main_options.toml | 12 +-- src/options/parser_options.toml | 4 +- src/options/printer_options.toml | 36 +++++-- src/options/proof_options.toml | 16 ++-- src/options/prop_options.toml | 16 ++-- src/options/quantifiers_options.toml | 71 +++++++------- src/options/sep_options.toml | 4 +- src/options/sets_options.toml | 2 +- src/options/smt_options.toml | 49 +++------- src/options/strings_options.toml | 26 ++--- src/options/theory_options.toml | 6 +- src/options/uf_options.toml | 5 +- .../cli/regress0/options/set-after-init.smt2 | 10 +- .../regress0/quantifiers/issue4086-infs.smt2 | 4 +- .../cli/regress1/quantifiers/lra-vts-inf.smt2 | 2 +- 22 files changed, 204 insertions(+), 213 deletions(-) diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 63b065880..74a2caa06 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -3,7 +3,7 @@ name = "Arithmetic Theory" [[option]] name = "arithUnateLemmaMode" - category = "regular" + category = "expert" long = "unate-lemmas=MODE" type = "ArithUnateLemmaMode" default = "ALL" @@ -24,7 +24,7 @@ name = "Arithmetic Theory" [[option]] name = "arithPropagationMode" - category = "regular" + category = "expert" long = "arith-prop=MODE" type = "ArithPropagationMode" default = "BOTH_PROP" @@ -50,7 +50,7 @@ name = "Arithmetic Theory" # defaults. [[option]] name = "arithHeuristicPivots" - category = "regular" + category = "expert" long = "heuristic-pivots=N" type = "int64_t" default = "0" @@ -71,7 +71,7 @@ name = "Arithmetic Theory" [[option]] name = "arithErrorSelectionRule" - category = "regular" + category = "expert" long = "error-selection-rule=RULE" type = "ErrorSelectionRule" default = "MINIMUM_AMOUNT" @@ -92,7 +92,7 @@ name = "Arithmetic Theory" # 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" @@ -104,7 +104,7 @@ name = "Arithmetic Theory" # defaults. [[option]] name = "arithPivotThreshold" - category = "regular" + category = "expert" long = "pivot-threshold=N" type = "uint64_t" default = "2" @@ -112,7 +112,7 @@ name = "Arithmetic Theory" [[option]] name = "arithPropagateMaxLength" - category = "regular" + category = "expert" long = "prop-row-length=N" type = "uint64_t" default = "16" @@ -120,7 +120,7 @@ name = "Arithmetic Theory" [[option]] name = "arithDioSolver" - category = "regular" + category = "expert" long = "dio-solver" type = "bool" default = "true" @@ -138,7 +138,7 @@ name = "Arithmetic Theory" [[option]] name = "arithMLTrick" - category = "regular" + category = "expert" long = "miplib-trick" type = "bool" default = "false" @@ -146,7 +146,7 @@ name = "Arithmetic Theory" [[option]] name = "arithMLTrickSubstitutions" - category = "regular" + category = "expert" long = "miplib-trick-subs=N" type = "uint64_t" default = "1" @@ -154,7 +154,7 @@ name = "Arithmetic Theory" [[option]] name = "doCutAllBounded" - category = "regular" + category = "expert" long = "cut-all-bounded" type = "bool" default = "false" @@ -162,7 +162,7 @@ name = "Arithmetic Theory" [[option]] name = "maxCutsInContext" - category = "regular" + category = "expert" long = "maxCutsInContext=N" type = "uint64_t" default = "65535" @@ -170,7 +170,7 @@ name = "Arithmetic Theory" [[option]] name = "revertArithModels" - category = "regular" + category = "expert" long = "revert-arith-models-on-unsat" type = "bool" default = "false" @@ -178,7 +178,7 @@ name = "Arithmetic Theory" [[option]] name = "havePenalties" - category = "regular" + category = "expert" long = "fc-penalties" type = "bool" default = "false" @@ -186,7 +186,7 @@ name = "Arithmetic Theory" [[option]] name = "useFC" - category = "regular" + category = "expert" long = "use-fcsimplex" type = "bool" default = "false" @@ -194,7 +194,7 @@ name = "Arithmetic Theory" [[option]] name = "useSOI" - category = "regular" + category = "expert" long = "use-soi" type = "bool" default = "false" @@ -202,7 +202,7 @@ name = "Arithmetic Theory" [[option]] name = "restrictedPivots" - category = "regular" + category = "expert" long = "restrict-pivots" type = "bool" default = "true" @@ -210,7 +210,7 @@ name = "Arithmetic Theory" [[option]] name = "collectPivots" - category = "regular" + category = "expert" long = "collect-pivot-stats" type = "bool" default = "false" @@ -218,7 +218,7 @@ name = "Arithmetic Theory" [[option]] name = "useApprox" - category = "regular" + category = "expert" long = "use-approx" type = "bool" default = "false" @@ -226,7 +226,7 @@ name = "Arithmetic Theory" [[option]] name = "maxApproxDepth" - category = "regular" + category = "expert" long = "approx-branch-depth=N" type = "int64_t" default = "200" @@ -234,7 +234,7 @@ name = "Arithmetic Theory" [[option]] name = "exportDioDecompositions" - category = "regular" + category = "expert" long = "dio-decomps" type = "bool" default = "false" @@ -242,7 +242,7 @@ name = "Arithmetic Theory" [[option]] name = "newProp" - category = "regular" + category = "expert" long = "new-prop" type = "bool" default = "true" @@ -250,7 +250,7 @@ name = "Arithmetic Theory" [[option]] name = "arithPropAsLemmaLength" - category = "regular" + category = "expert" long = "arith-prop-clauses=N" type = "uint64_t" default = "8" @@ -258,7 +258,7 @@ name = "Arithmetic Theory" [[option]] name = "soiQuickExplain" - category = "regular" + category = "expert" long = "soi-qe" type = "bool" default = "false" @@ -266,7 +266,7 @@ name = "Arithmetic Theory" [[option]] name = "trySolveIntStandardEffort" - category = "regular" + category = "expert" long = "se-solve-int" type = "bool" default = "false" @@ -274,7 +274,7 @@ name = "Arithmetic Theory" [[option]] name = "replayFailureLemma" - category = "regular" + category = "expert" long = "lemmas-on-replay-failure" type = "bool" default = "false" @@ -282,7 +282,7 @@ name = "Arithmetic Theory" [[option]] name = "dioSolverTurns" - category = "regular" + category = "expert" long = "dio-turns=N" type = "int64_t" default = "10" @@ -290,7 +290,7 @@ name = "Arithmetic Theory" [[option]] name = "rrTurns" - category = "regular" + category = "expert" long = "rr-turns=N" type = "int64_t" default = "3" @@ -298,7 +298,7 @@ name = "Arithmetic Theory" [[option]] name = "replayEarlyCloseDepths" - category = "regular" + category = "expert" long = "replay-early-close-depth=N" type = "int64_t" default = "1" @@ -306,7 +306,7 @@ name = "Arithmetic Theory" [[option]] name = "replayNumericFailurePenalty" - category = "regular" + category = "expert" long = "replay-num-err-penalty=N" type = "int64_t" default = "4194304" @@ -314,7 +314,7 @@ name = "Arithmetic Theory" [[option]] name = "replayRejectCutSize" - category = "regular" + category = "expert" long = "replay-reject-cut=N" type = "uint64_t" default = "25500" @@ -322,7 +322,7 @@ name = "Arithmetic Theory" [[option]] name = "lemmaRejectCutSize" - category = "regular" + category = "expert" long = "replay-lemma-reject-cut=N" type = "uint64_t" default = "25500" @@ -330,7 +330,7 @@ name = "Arithmetic Theory" [[option]] name = "ppAssertMaxSubSize" - category = "regular" + category = "expert" long = "pp-assert-max-sub-size=N" type = "uint64_t" default = "2" @@ -338,7 +338,7 @@ name = "Arithmetic Theory" [[option]] name = "arithNoPartialFun" - category = "regular" + category = "expert" long = "arith-no-partial-fun" type = "bool" default = "false" @@ -346,7 +346,7 @@ name = "Arithmetic Theory" [[option]] name = "pbRewrites" - category = "regular" + category = "expert" long = "pb-rewrites" type = "bool" default = "false" @@ -372,7 +372,7 @@ name = "Arithmetic Theory" [[option]] name = "nlRlvAssertBounds" - category = "regular" + category = "expert" long = "nl-rlv-assert-bounds" type = "bool" default = "false" @@ -380,7 +380,7 @@ name = "Arithmetic Theory" [[option]] name = "nlExtResBound" - category = "regular" + category = "expert" long = "nl-ext-rbound" type = "bool" default = "false" @@ -420,7 +420,7 @@ name = "Arithmetic Theory" [[option]] name = "nlExtEntailConflicts" - category = "regular" + category = "expert" long = "nl-ext-ent-conf" type = "bool" default = "false" @@ -436,7 +436,7 @@ name = "Arithmetic Theory" [[option]] name = "nlExtPurify" - category = "regular" + category = "expert" long = "nl-ext-purify" type = "bool" default = "false" @@ -444,7 +444,7 @@ name = "Arithmetic Theory" [[option]] name = "nlExtSplitZero" - category = "regular" + category = "expert" long = "nl-ext-split-zero" type = "bool" default = "false" @@ -452,7 +452,7 @@ name = "Arithmetic Theory" [[option]] name = "nlExtTfTaylorDegree" - category = "regular" + category = "expert" long = "nl-ext-tf-taylor-deg=N" type = "int64_t" default = "4" @@ -460,7 +460,7 @@ name = "Arithmetic Theory" [[option]] name = "nlExtIncPrecision" - category = "regular" + category = "expert" long = "nl-ext-inc-prec" type = "bool" default = "true" @@ -468,7 +468,7 @@ name = "Arithmetic Theory" [[option]] name = "nlRlvMode" - category = "regular" + category = "expert" long = "nl-rlv=MODE" type = "NlRlvMode" default = "NONE" @@ -502,7 +502,7 @@ name = "Arithmetic Theory" [[option]] name = "nlCovVarElim" - category = "regular" + category = "expert" long = "nl-cov-var-elim" type = "bool" default = "true" @@ -510,7 +510,7 @@ name = "Arithmetic Theory" [[option]] name = "nlCovPrune" - category = "regular" + category = "expert" long = "nl-cov-prune" type = "bool" default = "false" @@ -577,7 +577,7 @@ name = "Arithmetic Theory" [[option]] name = "arithEqSolver" - category = "regular" + category = "expert" long = "arith-eq-solver" type = "bool" default = "false" @@ -585,7 +585,7 @@ name = "Arithmetic Theory" [[option]] name = "arithCongMan" - category = "regular" + category = "expert" long = "arith-cong-man" type = "bool" default = "true" diff --git a/src/options/arrays_options.toml b/src/options/arrays_options.toml index 9681ea132..e213718a4 100644 --- a/src/options/arrays_options.toml +++ b/src/options/arrays_options.toml @@ -3,7 +3,7 @@ name = "Arrays Theory" [[option]] name = "arraysOptimizeLinear" - category = "regular" + category = "expert" long = "arrays-optimize-linear" type = "bool" default = "true" @@ -11,7 +11,7 @@ name = "Arrays Theory" [[option]] name = "arraysWeakEquivalence" - category = "regular" + category = "expert" long = "arrays-weak-equiv" type = "bool" default = "false" @@ -27,7 +27,7 @@ name = "Arrays Theory" [[option]] name = "arraysEagerLemmas" - category = "regular" + category = "expert" long = "arrays-eager-lemmas" type = "bool" default = "false" @@ -35,7 +35,7 @@ name = "Arrays Theory" [[option]] name = "arraysReduceSharing" - category = "regular" + category = "expert" long = "arrays-reduce-sharing" type = "bool" default = "false" @@ -43,7 +43,7 @@ name = "Arrays Theory" [[option]] name = "arraysPropagate" - category = "regular" + category = "expert" long = "arrays-prop=N" type = "int64_t" default = "2" diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 4bf13ec25..13aa1020b 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -3,7 +3,7 @@ name = "Base" [[option]] name = "err" - category = "regular" + category = "expert" long = "err=erroutput" type = "ManagedErr" default = '{}' @@ -14,7 +14,7 @@ name = "Base" [[option]] name = "in" - category = "regular" + category = "expert" long = "in=input" type = "ManagedIn" default = '{}' @@ -23,7 +23,7 @@ name = "Base" [[option]] name = "out" - category = "regular" + category = "expert" long = "out=output" type = "ManagedOut" default = '{}' @@ -59,7 +59,7 @@ name = "Base" [[option]] name = "verbosity" long = "verbosity=N" - category = "regular" + category = "common" type = "int64_t" default = "0" predicates = ["setVerbosity"] @@ -130,7 +130,7 @@ name = "Base" [[option]] name = "parseOnly" - category = "regular" + category = "common" long = "parse-only" type = "bool" default = "false" @@ -138,7 +138,7 @@ name = "Base" [[option]] name = "preprocessOnly" - category = "regular" + category = "common" long = "preprocess-only" type = "bool" default = "false" @@ -162,11 +162,11 @@ name = "Base" [[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]] @@ -227,7 +227,7 @@ name = "Base" [[option]] name = "printSuccess" - category = "regular" + category = "common" long = "print-success" type = "bool" default = "false" diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 00835e719..a4bed7c4a 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -3,7 +3,7 @@ name = "Bitvector Theory" [[option]] name = "bvSatSolver" - category = "expert" + category = "regular" long = "bv-sat-solver=MODE" type = "SatSolverMode" default = "CADICAL" @@ -36,7 +36,7 @@ name = "Bitvector Theory" [[option]] name = "bitvectorPropagate" - category = "regular" + category = "expert" long = "bv-propagate" type = "bool" default = "true" @@ -125,7 +125,7 @@ name = "Bitvector Theory" [[option]] name = "bvAssertInput" - category = "regular" + category = "expert" long = "bv-assert-input" type = "bool" default = "false" diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index 58c20c618..b1d38b525 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -11,7 +11,7 @@ name = "Datatypes Theory" [[option]] name = "dtBinarySplit" - category = "regular" + category = "expert" long = "dt-binary-split" type = "bool" default = "false" @@ -19,7 +19,7 @@ name = "Datatypes Theory" [[option]] name = "cdtBisimilar" - category = "regular" + category = "expert" long = "cdt-bisimilar" type = "bool" default = "true" @@ -27,7 +27,7 @@ name = "Datatypes Theory" [[option]] name = "dtCyclic" - category = "regular" + category = "expert" long = "dt-cyclic" type = "bool" default = "true" @@ -35,7 +35,7 @@ name = "Datatypes Theory" [[option]] name = "dtInferAsLemmas" - category = "regular" + category = "expert" long = "dt-infer-as-lemmas" type = "bool" default = "false" @@ -43,7 +43,7 @@ name = "Datatypes Theory" [[option]] name = "dtBlastSplits" - category = "regular" + category = "expert" long = "dt-blast-splits" type = "bool" default = "false" @@ -51,7 +51,7 @@ name = "Datatypes Theory" [[option]] name = "dtNestedRec" - category = "regular" + category = "expert" long = "dt-nested-rec" type = "bool" default = "false" @@ -111,7 +111,7 @@ name = "Datatypes Theory" [[option]] name = "sygusSymBreakLazy" - category = "regular" + category = "expert" long = "sygus-sym-break-lazy" type = "bool" default = "true" @@ -119,7 +119,7 @@ name = "Datatypes Theory" [[option]] name = "sygusSymBreakRlv" - category = "regular" + category = "expert" long = "sygus-sym-break-rlv" type = "bool" default = "true" @@ -151,7 +151,7 @@ name = "Datatypes Theory" [[option]] name = "sygusFairMax" - category = "regular" + category = "expert" long = "sygus-fair-max" type = "bool" default = "true" diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml index 6f2174a4f..cc237c9c3 100644 --- a/src/options/expr_options.toml +++ b/src/options/expr_options.toml @@ -3,7 +3,7 @@ name = "Expression" [[option]] name = "defaultExprDepth" - category = "regular" + category = "expert" long = "expr-depth=N" type = "int64_t" default = "-1" @@ -13,7 +13,7 @@ name = "Expression" [[option]] name = "defaultDagThresh" - category = "regular" + category = "common" long = "dag-thresh=N" type = "int64_t" default = "1" @@ -23,7 +23,7 @@ name = "Expression" [[option]] name = "typeChecking" - category = "regular" + category = "expert" long = "type-checking" type = "bool" default = "DO_SEMANTIC_CHECKS_BY_DEFAULT" @@ -31,7 +31,7 @@ name = "Expression" [[option]] name = "wellFormedChecking" - category = "regular" + category = "expert" long = "wf-checking" type = "bool" default = "true" diff --git a/src/options/fp_options.toml b/src/options/fp_options.toml index 2ed61effe..bebac4be3 100644 --- a/src/options/fp_options.toml +++ b/src/options/fp_options.toml @@ -3,7 +3,7 @@ name = "Floating-Point" [[option]] name = "fpExp" - category = "regular" + category = "expert" long = "fp-exp" type = "bool" default = "false" diff --git a/src/options/main_options.toml b/src/options/main_options.toml index 0dbe2899f..fe3224716 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -53,7 +53,7 @@ name = "Driver" [[option]] name = "showDebugTags" - category = "regular" + category = "expert" long = "show-debug-tags" type = "bool" default = "false" @@ -63,7 +63,7 @@ name = "Driver" [[option]] name = "showTraceTags" - category = "regular" + category = "expert" long = "show-trace-tags" type = "bool" default = "false" @@ -81,7 +81,7 @@ name = "Driver" [[option]] name = "interactive" - category = "regular" + category = "common" long = "interactive" type = "bool" default = "false" @@ -97,7 +97,7 @@ name = "Driver" [[option]] name = "segvSpin" - category = "regular" + category = "expert" long = "segv-spin" type = "bool" default = "false" @@ -129,7 +129,7 @@ name = "Driver" [[option]] name = "dumpInstantiationsDebug" - category = "regular" + category = "expert" long = "dump-instantiations-debug" type = "bool" default = "false" @@ -153,7 +153,7 @@ name = "Driver" [[option]] name = "forceNoLimitCpuWhileDump" - category = "regular" + category = "expert" long = "force-no-limit-cpu-while-dump" type = "bool" default = "false" diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml index 4dccd4c2e..83cbcb7bf 100644 --- a/src/options/parser_options.toml +++ b/src/options/parser_options.toml @@ -12,7 +12,7 @@ name = "Parser" [[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" @@ -47,7 +47,7 @@ name = "Parser" [[option]] name = "forceLogicString" - category = "expert" + category = "common" long = "force-logic=LOGIC" type = "std::string" default = '""' diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml index e6806823d..210803dbb 100644 --- a/src/options/printer_options.toml +++ b/src/options/printer_options.toml @@ -1,17 +1,9 @@ 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" @@ -39,3 +31,29 @@ name = "Printing" 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." diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index e6c2386b7..c014cc310 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -27,7 +27,7 @@ name = "Proof" [[option]] name = "proofPrintConclusion" - category = "regular" + category = "expert" long = "proof-print-conclusion" type = "bool" default = "false" @@ -35,7 +35,7 @@ name = "Proof" [[option]] name = "proofPedantic" - category = "regular" + category = "expert" long = "proof-pedantic=N" type = "uint64_t" default = "0" @@ -44,7 +44,7 @@ name = "Proof" [[option]] name = "proofCheck" - category = "regular" + category = "expert" long = "proof-check=MODE" type = "ProofCheckMode" default = "LAZY" @@ -65,7 +65,7 @@ name = "Proof" [[option]] name = "proofPpMerge" - category = "regular" + category = "expert" long = "proof-pp-merge" type = "bool" default = "true" @@ -94,7 +94,7 @@ name = "Proof" [[option]] name = "proofAnnotate" - category = "regular" + category = "expert" long = "proof-annotate" type = "bool" default = "false" @@ -102,7 +102,7 @@ name = "Proof" [[option]] name = "proofPruneInput" - category = "regular" + category = "expert" long = "proof-prune-input" type = "bool" default = "false" @@ -110,7 +110,7 @@ name = "Proof" [[option]] name = "proofAletheResPivots" - category = "regular" + category = "expert" long = "proof-alethe-res-pivots" type = "bool" default = "false" @@ -118,7 +118,7 @@ name = "Proof" [[option]] name = "proofDotDAG" - category = "regular" + category = "expert" long = "proof-dot-dag" type = "bool" default = "false" diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml index 84fea44d0..7e2c93954 100644 --- a/src/options/prop_options.toml +++ b/src/options/prop_options.toml @@ -4,7 +4,7 @@ name = "SAT Layer" [[option]] name = "satRandomFreq" alias = ["random-frequency"] - category = "regular" + category = "expert" long = "random-freq=P" type = "double" default = "0.0" @@ -15,14 +15,14 @@ name = "SAT Layer" [[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" @@ -31,7 +31,7 @@ name = "SAT Layer" [[option]] name = "satClauseDecay" - category = "regular" + category = "expert" type = "double" default = "0.999" minimum = "0.0" @@ -40,7 +40,7 @@ name = "SAT Layer" [[option]] name = "satRestartFirst" - category = "regular" + category = "expert" long = "restart-int-base=N" type = "uint64_t" default = "25" @@ -48,7 +48,7 @@ name = "SAT Layer" [[option]] name = "satRestartInc" - category = "regular" + category = "expert" long = "restart-int-inc=F" type = "double" default = "3.0" @@ -57,7 +57,7 @@ name = "SAT Layer" [[option]] name = "minisatSimpMode" - category = "regular" + category = "expert" long = "minisat-simplification=MODE" type = "MinisatSimpMode" default = "ALL" @@ -75,7 +75,7 @@ name = "SAT Layer" [[option]] name = "minisatDumpDimacs" - category = "regular" + category = "expert" long = "minisat-dump-dimacs" type = "bool" default = "false" diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index d78ea82ef..36f49836e 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -81,7 +81,7 @@ name = "Quantifiers" [[option]] name = "dtVarExpandQuant" - category = "regular" + category = "expert" long = "dt-var-exp-quant" type = "bool" default = "true" @@ -107,7 +107,7 @@ name = "Quantifiers" [[option]] name = "condVarSplitQuant" - category = "regular" + category = "expert" long = "cond-var-split-quant=MODE" type = "CondVarSplitQuantMode" default = "ON" @@ -154,7 +154,7 @@ name = "Quantifiers" # forall x. P( x ) => f( S( x ) ) = x [[option]] name = "preSkolemQuantNested" - category = "regular" + category = "expert" long = "pre-skolem-quant-nested" type = "bool" default = "true" @@ -178,7 +178,7 @@ name = "Quantifiers" [[option]] name = "globalNegate" - category = "regular" + category = "expert" long = "global-negate" type = "bool" default = "false" @@ -227,7 +227,7 @@ name = "Quantifiers" [[option]] name = "relevantTriggers" - category = "expert" + category = "regular" long = "relevant-triggers" type = "bool" default = "false" @@ -267,7 +267,7 @@ name = "Quantifiers" [[option]] name = "multiTriggerWhenSingle" - category = "expert" + category = "regular" long = "multi-trigger-when-single" type = "bool" default = "false" @@ -275,7 +275,7 @@ name = "Quantifiers" [[option]] name = "multiTriggerPriority" - category = "expert" + category = "regular" long = "multi-trigger-priority" type = "bool" default = "false" @@ -283,7 +283,7 @@ name = "Quantifiers" [[option]] name = "multiTriggerCache" - category = "expert" + category = "regular" long = "multi-trigger-cache" type = "bool" default = "false" @@ -291,7 +291,7 @@ name = "Quantifiers" [[option]] name = "multiTriggerLinear" - category = "expert" + category = "regular" long = "multi-trigger-linear" type = "bool" default = "true" @@ -357,7 +357,7 @@ name = "Quantifiers" [[option]] name = "triggerActiveSelMode" - category = "regular" + category = "expert" long = "trigger-active-sel=MODE" type = "TriggerActiveSelMode" default = "ALL" @@ -524,7 +524,7 @@ name = "Quantifiers" [[option]] name = "enumInstSum" - category = "expert" + category = "regular" long = "enum-inst-sum" type = "bool" default = "false" @@ -613,7 +613,7 @@ name = "Quantifiers" [[option]] name = "fmfOneInstPerRound" - category = "expert" + category = "regular" long = "mbqi-one-inst-per-round" type = "bool" default = "false" @@ -653,7 +653,7 @@ name = "Quantifiers" [[option]] name = "fmfTypeCompletionThresh" - category = "expert" + category = "regular" long = "fmf-type-completion-thresh=N" type = "int64_t" default = "1000" @@ -694,7 +694,7 @@ name = "Quantifiers" [[option]] name = "cbqiAllConflict" - category = "expert" + category = "regular" long = "cbqi-all-conflict" type = "bool" default = "false" @@ -834,19 +834,20 @@ name = "Quantifiers" [[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" @@ -895,7 +896,7 @@ name = "Quantifiers" [[option]] name = "cegqiSingleInvReconstructLimit" - category = "regular" + category = "expert" long = "sygus-si-rcons-limit=N" type = "int64_t" default = "10000" @@ -911,7 +912,7 @@ name = "Quantifiers" [[option]] name = "sygusConstRepairAbort" - category = "regular" + category = "expert" long = "sygus-crepair-abort" type = "bool" default = "false" @@ -991,7 +992,7 @@ name = "Quantifiers" [[option]] name = "sygusRepairConstTimeout" - category = "regular" + category = "expert" long = "sygus-repair-const-timeout=N" type = "uint64_t" default = "0" @@ -1104,7 +1105,7 @@ name = "Quantifiers" [[option]] name = "sygusInvTemplWhenSyntax" - category = "regular" + category = "expert" long = "sygus-inv-templ-when-sg" type = "bool" default = "false" @@ -1173,7 +1174,7 @@ name = "Quantifiers" [[option]] name = "cegisSample" - category = "expert" + category = "regular" long = "cegis-sample=MODE" type = "CegisSampleMode" default = "NONE" @@ -1273,7 +1274,7 @@ name = "Quantifiers" [[option]] name = "sygusRewVerify" - category = "regular" + category = "expert" long = "sygus-rr-verify" type = "bool" default = "false" @@ -1345,7 +1346,7 @@ name = "Quantifiers" [[option]] name = "sygusExprMinerCheckTimeout" - category = "regular" + category = "expert" long = "sygus-expr-miner-check-timeout=N" type = "uint64_t" default = "0" @@ -1361,7 +1362,7 @@ name = "Quantifiers" [[option]] name = "sygusQueryGen" - category = "regular" + category = "expert" long = "sygus-query-gen=MODE" type = "SygusQueryGenMode" default = "NONE" @@ -1390,7 +1391,7 @@ name = "Quantifiers" [[option]] name = "sygusQueryGenDumpFiles" - category = "regular" + category = "expert" long = "sygus-query-gen-dump-files=MODE" type = "SygusQueryDumpFilesMode" default = "NONE" @@ -1468,7 +1469,7 @@ name = "Quantifiers" [[option]] name = "cegqiInnermost" - category = "expert" + category = "regular" long = "cegqi-innermost" type = "bool" default = "true" @@ -1476,7 +1477,7 @@ name = "Quantifiers" [[option]] name = "cegqiNestedQE" - category = "expert" + category = "regular" long = "cegqi-nested-qe" type = "bool" default = "false" @@ -1486,16 +1487,16 @@ name = "Quantifiers" [[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" @@ -1518,7 +1519,7 @@ name = "Quantifiers" [[option]] name = "cegqiMidpoint" - category = "expert" + category = "regular" long = "cegqi-midpoint" type = "bool" default = "false" @@ -1639,7 +1640,7 @@ name = "Quantifiers" [[option]] name = "quantDynamicSplit" category = "regular" - long = "quant-dsplit-mode=MODE" + long = "quant-dsplit=MODE" type = "QuantDSplitMode" default = "DEFAULT" help = "mode for dynamic quantifiers splitting" @@ -1674,7 +1675,7 @@ name = "Quantifiers" [[option]] name = "hoElim" - category = "expert" + category = "regular" long = "ho-elim" type = "bool" default = "false" @@ -1682,7 +1683,7 @@ name = "Quantifiers" [[option]] name = "hoElimStoreAx" - category = "expert" + category = "regular" long = "ho-elim-store-ax" type = "bool" default = "true" diff --git a/src/options/sep_options.toml b/src/options/sep_options.toml index be347502c..22dd62b29 100644 --- a/src/options/sep_options.toml +++ b/src/options/sep_options.toml @@ -3,7 +3,7 @@ name = "Separation Logic Theory" [[option]] name = "sepMinimalRefine" - category = "regular" + category = "expert" long = "sep-min-refine" type = "bool" default = "false" @@ -11,7 +11,7 @@ name = "Separation Logic Theory" [[option]] name = "sepPreSkolemEmp" - category = "regular" + category = "expert" long = "sep-pre-skolem-emp" type = "bool" default = "false" diff --git a/src/options/sets_options.toml b/src/options/sets_options.toml index ba0a9ad1d..bc0f6c367 100644 --- a/src/options/sets_options.toml +++ b/src/options/sets_options.toml @@ -19,7 +19,7 @@ name = "Sets Theory" [[option]] name = "setsExt" - category = "expert" + category = "regular" long = "sets-ext" type = "bool" default = "false" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 8dee79cd3..3b3f9e240 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -41,14 +41,6 @@ name = "SMT Layer" 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" @@ -60,7 +52,7 @@ name = "SMT Layer" [[option]] name = "checkModels" - category = "regular" + category = "common" long = "check-models" type = "bool" default = "false" @@ -68,7 +60,7 @@ name = "SMT Layer" [[option]] name = "debugCheckModels" - category = "regular" + category = "expert" long = "debug-check-models" type = "bool" default = "false" @@ -102,7 +94,7 @@ name = "SMT Layer" [[option]] name = "blockModelsMode" - category = "regular" + category = "expert" long = "block-models=MODE" type = "BlockModelsMode" default = "NONE" @@ -190,7 +182,7 @@ name = "SMT Layer" [[option]] name = "unsatCoresMode" - category = "regular" + category = "expert" long = "unsat-cores-mode=MODE" type = "UnsatCoresMode" default = "OFF" @@ -208,7 +200,7 @@ name = "SMT Layer" [[option]] name = "minimalUnsatCores" - category = "regular" + category = "expert" long = "minimal-unsat-cores" type = "bool" default = "false" @@ -240,7 +232,7 @@ name = "SMT Layer" [[option]] name = "difficultyMode" - category = "regular" + category = "expert" long = "difficulty-mode=MODE" type = "DifficultyMode" default = "LEMMA_LITERAL" @@ -274,7 +266,7 @@ name = "SMT Layer" [[option]] name = "produceAssertions" - category = "common" + category = "regular" long = "produce-assertions" type = "bool" alias = ["interactive-mode"] @@ -299,7 +291,7 @@ name = "SMT Layer" [[option]] name = "extRewPrep" - category = "expert" + category = "regular" long = "ext-rew-prep=MODE" type = "ExtRewPrepMode" default = "OFF" @@ -371,25 +363,6 @@ name = "SMT Layer" 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" @@ -400,7 +373,7 @@ name = "SMT Layer" [[option]] name = "solveBVAsInt" - category = "expert" + category = "regular" long = "solve-bv-as-int=MODE" type = "SolveBVAsIntMode" default = "OFF" @@ -458,7 +431,7 @@ name = "SMT Layer" [[option]] name = "solveIntAsBV" - category = "expert" + category = "regular" long = "solve-int-as-bv=N" type = "uint64_t" default = "0" @@ -466,7 +439,7 @@ name = "SMT Layer" [[option]] name = "solveRealAsInt" - category = "expert" + category = "regular" long = "solve-real-as-int" type = "bool" default = "false" diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 52fec34af..350348927 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -19,7 +19,7 @@ name = "Strings Theory" [[option]] name = "stringEager" - category = "regular" + category = "expert" long = "strings-eager" type = "bool" default = "false" @@ -35,7 +35,7 @@ name = "Strings Theory" [[option]] name = "stringLenNorm" - category = "regular" + category = "expert" long = "strings-len-norm" type = "bool" default = "true" @@ -43,7 +43,7 @@ name = "Strings Theory" [[option]] name = "stringInferSym" - category = "regular" + category = "expert" long = "strings-infer-sym" type = "bool" default = "true" @@ -51,7 +51,7 @@ name = "Strings Theory" [[option]] name = "stringEagerLen" - category = "regular" + category = "expert" long = "strings-eager-len" type = "bool" default = "true" @@ -67,7 +67,7 @@ name = "Strings Theory" [[option]] name = "stringProcessLoopMode" - category = "expert" + category = "regular" long = "strings-process-loop-mode=MODE" type = "ProcessLoopMode" default = "FULL" @@ -91,7 +91,7 @@ name = "Strings Theory" [[option]] name = "stringInferAsLemmas" - category = "regular" + category = "expert" long = "strings-infer-as-lemmas" type = "bool" default = "false" @@ -99,7 +99,7 @@ name = "Strings Theory" [[option]] name = "stringRExplainLemmas" - category = "regular" + category = "expert" long = "strings-rexplain-lemmas" type = "bool" default = "true" @@ -107,7 +107,7 @@ name = "Strings Theory" [[option]] name = "stringMinPrefixExplain" - category = "regular" + category = "expert" long = "strings-min-prefix-explain" type = "bool" default = "true" @@ -141,7 +141,7 @@ name = "Strings Theory" [[option]] name = "stringFlatForms" - category = "regular" + category = "expert" long = "strings-ff" type = "bool" default = "true" @@ -149,7 +149,7 @@ name = "Strings Theory" [[option]] name = "stringRegExpInterMode" - category = "expert" + category = "regular" long = "re-inter-mode=MODE" type = "RegExpInterMode" default = "CONSTANT" @@ -170,7 +170,7 @@ name = "Strings Theory" [[option]] name = "stringUnifiedVSpt" - category = "regular" + category = "expert" long = "strings-unified-vspt" type = "bool" default = "true" @@ -186,7 +186,7 @@ name = "Strings Theory" [[option]] name = "stringsAlphaCard" - category = "regular" + category = "expert" long = "strings-alpha-card=N" type = "uint64_t" default = "196608" @@ -245,7 +245,7 @@ name = "Strings Theory" [[option]] name = "stringsModelMaxLength" - category = "regular" + category = "expert" long = "strings-model-max-len=N" type = "uint64_t" default = "65536" diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml index 87869beb3..46123ded6 100644 --- a/src/options/theory_options.toml +++ b/src/options/theory_options.toml @@ -18,7 +18,7 @@ name = "Theory Layer" [[option]] name = "assignFunctionValues" - category = "regular" + category = "expert" long = "assign-function-values" type = "bool" default = "true" @@ -26,7 +26,7 @@ name = "Theory Layer" [[option]] name = "condenseFunctionValues" - category = "regular" + category = "expert" long = "condense-function-values" type = "bool" default = "true" @@ -34,7 +34,7 @@ name = "Theory Layer" [[option]] name = "relevanceFilter" - category = "regular" + category = "expert" long = "relevance-filter" type = "bool" default = "false" diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml index a289132fc..c6907a83d 100644 --- a/src/options/uf_options.toml +++ b/src/options/uf_options.toml @@ -3,8 +3,7 @@ name = "Uninterpreted Functions Theory" [[option]] name = "ufSymmetryBreaker" - alias = ["uf-symmetry-breaker"] - category = "regular" + category = "expert" long = "symmetry-breaker" type = "bool" default = "true" @@ -46,7 +45,7 @@ name = "Uninterpreted Functions Theory" [[option]] name = "ufssFairnessMonotone" - category = "regular" + category = "expert" long = "uf-ss-fair-monotone" type = "bool" default = "false" diff --git a/test/regress/cli/regress0/options/set-after-init.smt2 b/test/regress/cli/regress0/options/set-after-init.smt2 index 5c1fce9a7..51bb1e78e 100644 --- a/test/regress/cli/regress0/options/set-after-init.smt2 +++ b/test/regress/cli/regress0/options/set-after-init.smt2 @@ -4,16 +4,16 @@ ; 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) @@ -22,4 +22,4 @@ (set-option :verbosity 0) (get-option :verbosity) -(set-option :random-seed 1) \ No newline at end of file +(set-option :sat-random-seed 1) diff --git a/test/regress/cli/regress0/quantifiers/issue4086-infs.smt2 b/test/regress/cli/regress0/quantifiers/issue4086-infs.smt2 index faad2cf18..432218e73 100644 --- a/test/regress/cli/regress0/quantifiers/issue4086-infs.smt2 +++ b/test/regress/cli/regress0/quantifiers/issue4086-infs.smt2 @@ -1,7 +1,7 @@ (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) diff --git a/test/regress/cli/regress1/quantifiers/lra-vts-inf.smt2 b/test/regress/cli/regress1/quantifiers/lra-vts-inf.smt2 index 80315edaf..9fb4f7b44 100644 --- a/test/regress/cli/regress1/quantifiers/lra-vts-inf.smt2 +++ b/test/regress/cli/regress1/quantifiers/lra-vts-inf.smt2 @@ -1,4 +1,4 @@ -; 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) -- 2.30.2