diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-04 17:18:06 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-12-04 17:18:06 -0600 |
| commit | dd66d825a0e05b46690b0bb914da3b0aa2045654 (patch) | |
| tree | 7648d3693578c2dbf8b74216fe335990784b3380 /src/options/quantifiers_options.toml | |
| parent | 1741bb48e54f25ef4fd7776380deca1dd60a2201 (diff) | |
New grammar construction modes for SyGuS (#3486)
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 019b052bc..171af1e47 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1077,6 +1077,16 @@ header = "options/quantifiers_options.h" help = "embed sygus templates into grammars" [[option]] + name = "sygusGrammarConsMode" + category = "regular" + long = "sygus-grammar-cons=MODE" + type = "CVC4::theory::quantifiers::SygusGrammarConsMode" + default = "CVC4::theory::quantifiers::SYGUS_GCONS_SIMPLE" + handler = "stringToSygusGrammarConsMode" + includes = ["options/quantifiers_modes.h"] + help = "mode for SyGuS grammar construction" + +[[option]] name = "sygusInvTemplMode" category = "regular" long = "sygus-inv-templ=MODE" |