diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-10-01 13:48:37 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-01 13:48:37 -0700 |
| commit | 776ee02237b06eb3130e56af4d98d9ff36667d8b (patch) | |
| tree | 56d55c26003f2dfa3ef23c0cf4ae32e7af2e5e11 /src/options | |
| parent | cd91768f52349bd14399e49b2fbc4e59bb659ded (diff) | |
Add additional ground terms to SyGuS instantiation grammar (#5167)
This PR adds options to add additional ground terms to the SyGuS instantiation grammars.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options.toml | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 4b130158c..724a2ef2b 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1995,3 +1995,39 @@ header = "options/quantifiers_options.h" type = "bool" default = "false" help = "Enable SyGuS instantiation quantifiers module" + +[[option]] + name = "sygusInstScope" + category = "regular" + long = "sygus-inst-scope=MODE" + type = "SygusInstScope" + default = "IN" + help = "select scope of ground terms" + help_mode = "scope for collecting ground terms for the grammar." +[[option.mode.IN]] + name = "in" + help = "use ground terms inside given quantified formula only." +[[option.mode.OUT]] + name = "out" + help = "use ground terms outside of quantified formulas only." +[[option.mode.BOTH]] + name = "both" + help = "combines inside and outside." + +[[option]] + name = "sygusInstTermSel" + category = "regular" + long = "sygus-inst-term-sel=MODE" + type = "SygusInstTermSelMode" + default = "MIN" + help = "granularity for ground terms" + help_mode = "Ground term selection modes." +[[option.mode.MIN]] + name = "min" + help = "collect minimal ground terms only." +[[option.mode.MAX]] + name = "max" + help = "collect maximal ground terms only." +[[option.mode.BOTH]] + name = "both" + help = "combines minimal and maximal ." |