diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-23 12:20:23 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-23 12:20:23 -0500 |
| commit | d95e5257f452d765aa67931f0b2af7b178f2e986 (patch) | |
| tree | f67100dedc9b9a3c7eb477dd66664b31f7f15d73 /src/options | |
| parent | d3528b6db31f9bdff56bc519bbf427b2533c43b8 (diff) | |
Enable post-condition strenghtening by default for non-syntax restricted invariant synthesis (#1703)
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options.toml | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 8f07384d6..ab74fbc79 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1017,11 +1017,20 @@ header = "options/quantifiers_options.h" category = "regular" long = "sygus-inv-templ=MODE" type = "CVC4::theory::quantifiers::SygusInvTemplMode" - default = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE" + default = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST" handler = "stringToSygusInvTemplMode" includes = ["options/quantifiers_modes.h"] read_only = true - help = "template mode for sygus invariant synthesis" + help = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)" + +[[option]] + name = "sygusInvTemplWhenSyntax" + category = "regular" + long = "sygus-inv-templ-when-sg" + type = "bool" + default = "false" + read_only = false + help = "use invariant templates (with solution reconstruction) for syntax guided problems" [[option]] name = "sygusInvAutoUnfold" |