diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-13 14:53:00 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-13 12:53:00 -0700 |
commit | 442ab0cdd8578631974318c17dd8ace59d145839 (patch) | |
tree | 047f130c44c21c84fb461e5df2e998e475fd0936 /src/options | |
parent | 5fe737f9513ef4c9c6f582d08bd8cd644a9e012c (diff) |
Removing a few deprecated options (#4052)
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/datatypes_options.toml | 9 | ||||
-rw-r--r-- | src/options/quantifiers_options.toml | 63 | ||||
-rw-r--r-- | src/options/strings_options.toml | 20 |
3 files changed, 0 insertions, 92 deletions
diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index 7eb9d30c5..82e833506 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -119,15 +119,6 @@ header = "options/datatypes_options.h" type = "bool" default = "true" help = "sygus symmetry breaking lemmas based on pbe conjectures" - -[[option]] - name = "sygusOpt1" - category = "regular" - long = "sygus-opt1" - type = "bool" - default = "false" - read_only = true - help = "sygus experimental option" [[option]] name = "sygusSymBreakLazy" 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" diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index f51c4ce67..49c304bab 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -11,17 +11,6 @@ header = "options/strings_options.h" help = "experimental features in the theory of strings" [[option]] - name = "stringLB" - smt_name = "strings-lb" - category = "regular" - long = "strings-lb=N" - type = "unsigned" - default = "0" - predicates = ["unsignedLessEqual2"] - read_only = true - help = "the strategy of LB rule application: 0-lazy, 1-eager, 2-no" - -[[option]] name = "stdPrintASCII" category = "regular" long = "strings-print-ascii" @@ -48,15 +37,6 @@ header = "options/strings_options.h" help = "strings eager check" [[option]] - name = "stringEIT" - category = "regular" - long = "strings-eit" - type = "bool" - default = "false" - read_only = true - help = "the eager intersection used by the theory of strings" - -[[option]] name = "stringIgnNegMembership" category = "regular" long = "strings-inm" |