diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-20 09:02:25 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-10-20 09:02:25 -0500 |
| commit | 9d9a8bbd4465efd0860b185889fae89e4693d2a2 (patch) | |
| tree | ec42e3da1ce7d790ece4e1e1df6e35f65c782041 /src/options/quantifiers_options.toml | |
| parent | f25f227eb4a4df388160cdf62795f7f684b224ea (diff) | |
| parent | 1d4324bf87a35e36d9cc1e856d74ffbaf912a848 (diff) | |
Merge branch 'master' into strRewritesstrRewrites
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 1c2405449..0762622f0 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1094,7 +1094,6 @@ header = "options/quantifiers_options.h" 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 (weaken pre-condition, strengthen post-condition, or none)" [[option]] @@ -1396,6 +1395,14 @@ header = "options/quantifiers_options.h" help = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen" [[option]] + name = "sygusSolFilterImplied" + category = "regular" + long = "sygus-sol-filter-implied" + type = "bool" + default = "false" + help = "use sygus to enumerate interesting satisfiability queries" + +[[option]] name = "sygusExprMinerCheckUseExport" category = "expert" long = "sygus-expr-miner-check-use-export" |