From ccc301aa495153b3a2bd1b3958cc49cef65b09cc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 19 Oct 2018 20:59:51 -0500 Subject: Sygus streaming non-implied predicates (#2660) --- src/options/quantifiers_options.toml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'src/options') 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]] @@ -1395,6 +1394,14 @@ header = "options/quantifiers_options.h" default = "false" 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" -- cgit v1.2.3