remove options that are no longer used (#7197)

This PR removes a handful of options that are no longer used anywhere.

10 files changed, 0 insertions, 144 deletions

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
@@ -296,14 +296,6 @@ name   = "Arithmetic Theory"
   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"
   long       = "replay-early-close-depth=N"
@@ -312,14 +304,6 @@ name   = "Arithmetic Theory"
   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"
   long       = "replay-num-err-penalty=N"
@@ -344,38 +328,6 @@ name   = "Arithmetic Theory"
   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"
   long       = "pp-assert-max-sub-size=N"
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
@@ -18,14 +18,6 @@ name   = "Arrays Theory"
   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"
   long       = "arrays-eager-index"
@@ -42,14 +34,6 @@ name   = "Arrays Theory"
   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"
   long       = "arrays-reduce-sharing"
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
@@ -191,14 +191,6 @@ name   = "Bitvector Theory"
   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"
   long       = "bv-print-consts-as-indexed-symbols"
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<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 a8b11c197..cc9847469 100644
--- a/src/options/printer_options.toml
+++ b/src/options/printer_options.toml
@@ -2,21 +2,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"
   long       = "flatten-ho-chains"
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
@@ -985,14 +977,6 @@ name   = "Quantifiers"
   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"
   long       = "sygus-si-abort"
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
@@ -10,14 +10,6 @@ name   = "Separation Logic Theory"
   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"
   long       = "sep-min-refine"
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
@@ -162,14 +162,6 @@ name   = "SMT Layer"
   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"
   long       = "produce-unsat-cores"
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
@@ -123,14 +123,6 @@ name   = "Strings Theory"
   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"
   long       = "re-elim"
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
@@ -11,22 +11,6 @@ name   = "Uninterpreted Functions Theory"
   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"
   long       = "uf-ss-abort-card=N"