diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-26 13:03:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-26 13:03:08 -0500 |
| commit | 6bdc464d5f2e2dac39230dfef8da1049e0b317d1 (patch) | |
| tree | 7e8d7c6cdc8295f9a4ee39adb22eedb00b1b346b /src/options/quantifiers_options.toml | |
| parent | 5a669e6ed1c51cc80cc1dd313906ca47345abccd (diff) | |
Synth-check and accelerate options for sygus-rr (#1691)
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index c40491a40..ad05aa5cd 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1147,6 +1147,21 @@ header = "options/quantifiers_options.h" read_only = true help = "when applicable, use grammar for choosing sample points" +[[option]] + name = "sygusRewSynthAccel" + category = "regular" + long = "sygus-rr-synth-accel" + type = "bool" + default = "false" + help = "add dynamic symmetry breaking clauses based on candidate rewrites" + +[[option]] + name = "sygusRewSynthCheck" + category = "regular" + long = "sygus-rr-synth-check" + type = "bool" + default = "false" + help = "use satisfiability check to verify correctness of candidate rewrites" # CEGQI applied to general quantified formulas |