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 97fab52a0bc662850203d8b9f39dfa91fec419f2..6eb67d6d753f0bd77f5511b2ecd4ae3db562dfc1 100644 (file)
--- 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 9892b3fadbf081456a081fc531e8f84e6d78e295..9681ea132d2d07a6f84598b12ecce738124c463a 100644 (file)
--- 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 2457645d1af9e5e93e3da066df5be8cf7353043d..17c65c2902d4a352df133a831bba76e57ce9786c 100644 (file)
--- 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 b9528b93cd53aea3d83e8db71da66542e9666026..9da20ce86c34b84237eb12f4d7093b3fb88d08e9 100644 (file)
--- a/src/options/didyoumean_test.cpp
+++ b/src/options/didyoumean_test.cpp
@@ -530,7 +530,6 @@ set<string> 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 a8b11c1979c6e36aee96341691d97027bd374396..cc9847469661d755eb590f6737e35e9a594049b5 100644 (file)
--- 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 1bd29684a3975e9de13a19199d6a97901064a109..106161305c2236498d0cbdab3031b30a25586964 100644 (file)
--- 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 7185a35df9ca885be880b6d7b27908c46c371ee3..ff5ac1af66d64b55f025a34a46697cd293bcd8e4 100644 (file)
--- 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 26af86ca2fdc3bc2797acb594e09f2448a1ab06e..95cc79a0d1f63a83d1efe0166cde0aca2756547b 100644 (file)
--- 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 8ee25c26520c9223d4d804d915f827788812512b..90e363f28f25a99ca8aed4d940bbe3d6f9a3b7d0 100644 (file)
--- 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 d90d8f69302fcbc18fe8770dc8bbefde3498055d..239628e283f5c391419cd889099323885a847ca2 100644 (file)
--- 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"