From: Gereon Kremer Date: Wed, 15 Sep 2021 17:06:51 +0000 (+0200) Subject: remove options that are no longer used (#7197) X-Git-Tag: cvc5-1.0.0~1207 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f416c8803e4af59a99823a76bb8279a303ab2efb;p=cvc5.git remove options that are no longer used (#7197) This PR removes a handful of options that are no longer used anywhere. --- diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 97fab52a0..6eb67d6d7 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -295,14 +295,6 @@ name = "Arithmetic Theory" default = "3" help = "round robin turn" -[[option]] - name = "dioRepeat" - category = "regular" - long = "dio-repeat" - type = "bool" - default = "false" - help = "handle dio solver constraints in mass or one at a time" - [[option]] name = "replayEarlyCloseDepths" category = "regular" @@ -311,14 +303,6 @@ name = "Arithmetic Theory" default = "1" help = "multiples of the depths to try to close the approx log eagerly" -[[option]] - name = "replayFailurePenalty" - category = "regular" - long = "replay-failure-penalty=N" - type = "int64_t" - default = "100" - help = "number of solve integer attempts to skips after a numeric failure" - [[option]] name = "replayNumericFailurePenalty" category = "regular" @@ -343,38 +327,6 @@ name = "Arithmetic Theory" default = "25500" help = "maximum complexity of any coefficient while outputting replaying cut lemmas" -[[option]] - name = "soiApproxMajorFailure" - category = "regular" - long = "replay-soi-major-threshold=T" - type = "double" - default = ".01" - help = "threshold for a major tolerance failure by the approximate solver" - -[[option]] - name = "soiApproxMajorFailurePen" - category = "regular" - long = "replay-soi-major-threshold-pen=N" - type = "int64_t" - default = "50" - help = "threshold for a major tolerance failure by the approximate solver" - -[[option]] - name = "soiApproxMinorFailure" - category = "regular" - long = "replay-soi-minor-threshold=T" - type = "double" - default = ".0001" - help = "threshold for a minor tolerance failure by the approximate solver" - -[[option]] - name = "soiApproxMinorFailurePen" - category = "regular" - long = "replay-soi-minor-threshold-pen=N" - type = "int64_t" - default = "10" - help = "threshold for a minor tolerance failure by the approximate solver" - [[option]] name = "ppAssertMaxSubSize" category = "regular" diff --git a/src/options/arrays_options.toml b/src/options/arrays_options.toml index 9892b3fad..9681ea132 100644 --- a/src/options/arrays_options.toml +++ b/src/options/arrays_options.toml @@ -17,14 +17,6 @@ name = "Arrays Theory" default = "false" help = "use algorithm from Christ/Hoenicke (SMT 2014)" -[[option]] - name = "arraysModelBased" - category = "regular" - long = "arrays-model-based" - type = "bool" - default = "false" - help = "turn on model-based array solver" - [[option]] name = "arraysEagerIndexSplitting" category = "regular" @@ -41,14 +33,6 @@ name = "Arrays Theory" default = "false" help = "turn on eager lemma generation for arrays" -[[option]] - name = "arraysConfig" - category = "regular" - long = "arrays-config=N" - type = "int64_t" - default = "0" - help = "set different array option configurations - for developers only" - [[option]] name = "arraysReduceSharing" category = "regular" diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 2457645d1..17c65c290 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -190,14 +190,6 @@ name = "Bitvector Theory" default = "false" help = "simplify formula via Gaussian Elimination if applicable" -[[option]] - name = "bvAlgExtf" - category = "regular" - long = "bv-alg-extf" - type = "bool" - default = "true" - help = "algebraic inferences for extended functions" - [[option]] name = "bvPrintConstsAsIndexedSymbols" category = "regular" diff --git a/src/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp index b9528b93c..9da20ce86 100644 --- a/src/options/didyoumean_test.cpp +++ b/src/options/didyoumean_test.cpp @@ -530,7 +530,6 @@ set getOptionStrings() { "dio-repeat", "no-dio-repeat", "replay-early-close-depth", - "replay-failure-penalty", "replay-num-err-penalty", "replay-reject-cut", "replay-lemma-reject-cut", diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml index a8b11c197..cc9847469 100644 --- a/src/options/printer_options.toml +++ b/src/options/printer_options.toml @@ -1,21 +1,6 @@ id = "PRINTER" name = "Printing" -[[option]] - name = "modelFormatMode" - category = "regular" - long = "model-format=MODE" - type = "ModelFormatMode" - default = "DEFAULT" - help = "print format mode for models, see --model-format=help" - help_mode = "Model format modes." -[[option.mode.DEFAULT]] - name = "default" - help = "Print model as expressions in the output language format." -[[option.mode.TABLE]] - name = "table" - help = "Print functional expressions over finite domains in a table format." - [[option]] name = "flattenHOChains" category = "regular" diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 1bd29684a..106161305 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -941,14 +941,6 @@ name = "Quantifiers" name = "all" help = "Always use single invocation techniques." -[[option]] - name = "cegqiSingleInvPartial" - category = "regular" - long = "sygus-si-partial" - type = "bool" - default = "false" - help = "combined techniques for synthesis conjectures that are partially single invocation" - # Solution reconstruction modes for single invocation conjectures # # These modes indicate the policy when cvc5 solves a synthesis conjecture using @@ -984,14 +976,6 @@ name = "Quantifiers" default = "10000" help = "number of rounds of enumeration to use during solution reconstruction (negative means unlimited)" -[[option]] - name = "cegqiSingleInvReconstructConst" - category = "regular" - long = "sygus-si-reconstruct-const" - type = "bool" - default = "true" - help = "include constants when reconstruct solutions for single invocation conjectures in original grammar" - [[option]] name = "cegqiSingleInvAbort" category = "regular" diff --git a/src/options/sep_options.toml b/src/options/sep_options.toml index 7185a35df..ff5ac1af6 100644 --- a/src/options/sep_options.toml +++ b/src/options/sep_options.toml @@ -9,14 +9,6 @@ name = "Separation Logic Theory" default = "true" help = "check negated spatial assertions" -[[option]] - name = "sepExp" - category = "regular" - long = "sep-exp" - type = "bool" - default = "false" - help = "experimental flag for sep" - [[option]] name = "sepMinimalRefine" category = "regular" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 26af86ca2..95cc79a0d 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -161,14 +161,6 @@ name = "SMT Layer" name = "sygus-standard" help = "Print based on SyGuS standard." -[[option]] - name = "sygusPrintCallbacks" - category = "regular" - long = "sygus-print-callbacks" - type = "bool" - default = "true" - help = "use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging)" - [[option]] name = "unsatCores" category = "regular" diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 8ee25c265..90e363f28 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -122,14 +122,6 @@ name = "Strings Theory" default = "false" help = "use model guessing to avoid string extended function reductions" -[[option]] - name = "stringLenPropCsp" - category = "regular" - long = "strings-lprop-csp" - type = "bool" - default = "false" - help = "do length propagation based on constant splits" - [[option]] name = "regExpElim" category = "regular" diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml index d90d8f693..239628e28 100644 --- a/src/options/uf_options.toml +++ b/src/options/uf_options.toml @@ -10,22 +10,6 @@ name = "Uninterpreted Functions Theory" default = "true" help = "use UF symmetry breaker (Deharbe et al., CADE 2011)" -[[option]] - name = "ufssTotalityLimited" - category = "regular" - long = "uf-ss-totality-limited=N" - type = "int64_t" - default = "-1" - help = "apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)" - -[[option]] - name = "ufssTotalitySymBreak" - category = "regular" - long = "uf-ss-totality-sym-break" - type = "bool" - default = "false" - help = "apply symmetry breaking for totality axioms" - [[option]] name = "ufssAbortCardinality" category = "regular"