diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-09 11:54:59 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-09 11:54:59 -0500 |
| commit | 609a4c11eed577f127644006465d7e112139532d (patch) | |
| tree | a7fdcd05b759dfd235719d841d90761e3bc85b17 /src/options | |
| parent | df974e62c34f3e1b4f57feb64e439e1e791e87ce (diff) | |
Better option names for PBE (#1891)
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/datatypes_options.toml | 8 | ||||
| -rw-r--r-- | src/options/quantifiers_options.toml | 15 |
2 files changed, 11 insertions, 12 deletions
diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index ef736e913..8d6f0baf3 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -113,6 +113,14 @@ header = "options/datatypes_options.h" help = "dynamic sygus sym break lemmas" [[option]] + name = "sygusSymBreakPbe" + category = "regular" + long = "sygus-sym-break-pbe" + type = "bool" + default = "true" + help = "sygus sym break lemmas based on pbe conjectures" + +[[option]] name = "sygusOpt1" category = "regular" long = "sygus-opt1" diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 2f911bdd1..4c771c143 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -960,14 +960,6 @@ header = "options/quantifiers_options.h" help = "abort if synthesis conjecture is not single invocation" [[option]] - name = "sygusPbe" - category = "regular" - long = "sygus-pbe" - type = "bool" - default = "true" - help = "sygus advanced pruning based on examples" - -[[option]] name = "sygusUnif" category = "regular" long = "sygus-unif" @@ -1050,13 +1042,12 @@ header = "options/quantifiers_options.h" help = "enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems" [[option]] - name = "sygusUnifCondSol" + name = "sygusUnifPbe" category = "regular" - long = "sygus-unif-csol" + long = "sygus-pbe" type = "bool" default = "true" - read_only = true - help = "enable new approach which unifies conditional solutions" + help = "enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures" [[option]] name = "sygusDirectEval" |