diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-12 15:18:30 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-12 15:18:30 -0500 |
| commit | 093d5ffdfa5c1656309da6b9cbdfbbf28574a8a0 (patch) | |
| tree | 96c76652c60e286223523cf08f599b4cd84fb687 /src/options | |
| parent | ec8ea8a9c993435c4c5e671b1beea45ac088de64 (diff) | |
Add option --sygus-rr-synth-rec for considering all grammar types recursively (#2270)
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options.toml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index d9d3e0d38..4deb5565d 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1240,7 +1240,7 @@ header = "options/quantifiers_options.h" type = "bool" default = "false" read_only = true - help = "use sygus to enumerate and verify correctness of rewrite rules via sampling" + help = "use sygus to enumerate and verify correctness of rewrite rules" [[option]] name = "sygusRewSynth" @@ -1248,7 +1248,7 @@ header = "options/quantifiers_options.h" long = "sygus-rr-synth" type = "bool" default = "false" - help = "use sygus to enumerate candidate rewrite rules via sampling" + help = "use sygus to enumerate candidate rewrite rules" [[option]] name = "sygusRewSynthFilterOrder" @@ -1369,6 +1369,14 @@ header = "options/quantifiers_options.h" long = "sygus-expr-miner-check-timeout=N" type = "unsigned long" help = "timeout (in milliseconds) for satisfiability checks in expression miners" + +[[option]] + name = "sygusRewSynthRec" + category = "regular" + long = "sygus-rr-synth-rec" + type = "bool" + default = "false" + help = "synthesize rewrite rules over all sygus grammar types recursively" [[option]] name = "sygusQueryGen" |