From 442ab0cdd8578631974318c17dd8ace59d145839 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 13 Mar 2020 14:53:00 -0500
Subject: Removing a few deprecated options (#4052)

---
 src/options/quantifiers_options.toml | 63 ------------------------------------
 1 file changed, 63 deletions(-)

(limited to 'src/options/quantifiers_options.toml')

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
@@ -676,15 +676,6 @@ header = "options/quantifiers_options.h"
   default    = "false"
   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"
@@ -702,24 +693,6 @@ header = "options/quantifiers_options.h"
   default    = "false"
   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"
@@ -870,14 +843,6 @@ header = "options/quantifiers_options.h"
   default    = "false"
   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"
@@ -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]]
@@ -1377,15 +1331,6 @@ header = "options/quantifiers_options.h"
   read_only  = true
   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"
@@ -1428,14 +1373,6 @@ header = "options/quantifiers_options.h"
   name = "trust"
   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"
-- 
cgit v1.2.3