diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-10-11 11:10:16 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-11 13:10:16 -0500 |
| commit | 3d49a4413c819f6dee337ac7c53b6f6c6b510377 (patch) | |
| tree | 005dba213df89927ffcdf9c0bdf3776609c855ca /src/options/quantifiers_options.toml | |
| parent | 0f834b9622947ad1f6405c83a43df88c98c05c55 (diff) | |
SyGuS instantiation modes (#5228)
This PR adds three instantiation modes to the SyGuS instantiation module.
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 2a5faf9f7..d29052042 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -2023,3 +2023,21 @@ header = "options/quantifiers_options.h" [[option.mode.BOTH]] name = "both" help = "combines minimal and maximal ." + +[[option]] + name = "sygusInstMode" + category = "regular" + long = "sygus-inst-mode=MODE" + type = "SygusInstMode" + default = "PRIORITY_INST" + help = "select instantiation lemma mode" + help_mode = "SyGuS instantiation lemma modes." +[[option.mode.PRIORITY_INST]] + name = "priority-inst" + help = "add instantiation lemmas first, add evaluation unfolding if instantiation fails." +[[option.mode.PRIORITY_EVAL]] + name = "priority-eval" + help = "add evaluation unfolding lemma first, add instantiation lemma if unfolding lemmas already added." +[[option.mode.INTERLEAVE]] + name = "interleave" + help = "add instantiation and evaluation unfolding lemmas in the same step." |