Removing a few deprecated options (#4052)

1 files changed, 0 insertions, 63 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 6e0460ae9..12549152d 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -677,15 +677,6 @@ header = "options/quantifiers_options.h"
   help       = "only add one instantiation per quantifier per round for mbqi"
 
 [[option]]
-  name       = "fmfOneQuantPerRound"
-  category   = "regular"
-  long       = "mbqi-one-quant-per-round"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "only add instantiations for one quantifier per round for mbqi"
-
-[[option]]
   name       = "mbqiInterleave"
   category   = "regular"
   long       = "mbqi-interleave"
@@ -703,24 +694,6 @@ header = "options/quantifiers_options.h"
   help       = "use instantiation engine in conjunction with finite model finding"
 
 [[option]]
-  name       = "fmfInstGen"
-  category   = "regular"
-  long       = "fmf-inst-gen"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "enable Inst-Gen instantiation techniques for finite model finding"
-
-[[option]]
-  name       = "fmfInstGenOneQuantPerRound"
-  category   = "regular"
-  long       = "fmf-inst-gen-one-quant-per-round"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "only perform Inst-Gen instantiation techniques on one quantifier per round"
-
-[[option]]
   name       = "fmfFreshDistConst"
   category   = "regular"
   long       = "fmf-fresh-dc"
@@ -871,14 +844,6 @@ header = "options/quantifiers_options.h"
   help       = "do not consider instances of quantified formulas that are currently true in model, if it is available"
 
 [[option]]
-  name       = "instPropagate"
-  category   = "regular"
-  long       = "inst-prop"
-  type       = "bool"
-  default    = "false"
-  help       = "internal propagation for instantiations for selecting relevant instances"
-
-[[option]]
   name       = "qcfEagerTest"
   category   = "regular"
   long       = "qcf-eager-test"
@@ -905,17 +870,6 @@ header = "options/quantifiers_options.h"
   read_only  = true
   help       = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
 
-### Rewrite rules options
-
-[[option]]
-  name       = "rrOneInstPerRound"
-  category   = "regular"
-  long       = "rr-one-inst-per-round"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "add one instance of rewrite rule per round"
-
 ### Induction options
 
 [[option]]
@@ -1378,15 +1332,6 @@ header = "options/quantifiers_options.h"
   help       = "do unfolding of Boolean evaluation functions that appear in refinement lemmas"
 
 [[option]]
-  name       = "sygusRefEval"
-  category   = "regular"
-  long       = "sygus-ref-eval"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "direct evaluation of refinement lemmas for conflict analysis"
-
-[[option]]
   name       = "sygusStream"
   category   = "regular"
   long       = "sygus-stream"
@@ -1429,14 +1374,6 @@ header = "options/quantifiers_options.h"
   help = "Trust that when a solution for a conjecture is always true under sampling, then it is indeed a solution. Note this option may print out spurious solutions for synthesis conjectures."
 
 [[option]]
-  name       = "minSynthSol"
-  category   = "regular"
-  long       = "min-synth-sol"
-  type       = "bool"
-  default    = "true"
-  help       = "Minimize synthesis solutions"
-
-[[option]]
   name       = "sygusEvalOpt"
   category   = "regular"
   long       = "sygus-eval-opt"