diff options
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index c555c37bf..d9d3e0d38 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1403,12 +1403,22 @@ header = "options/quantifiers_options.h" help = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen" [[option]] - name = "sygusSolFilterImplied" + name = "sygusFilterSolMode" category = "regular" - long = "sygus-sol-filter-implied" + long = "sygus-filter-sol=MODE" + type = "CVC4::theory::quantifiers::SygusFilterSolMode" + default = "CVC4::theory::quantifiers::SYGUS_FILTER_SOL_NONE" + handler = "stringToSygusFilterSolMode" + includes = ["options/quantifiers_modes.h"] + help = "mode for filtering sygus solutions" + +[[option]] + name = "sygusFilterSolRevSubsume" + category = "expert" + long = "sygus-filter-sol-rev" type = "bool" default = "false" - help = "use sygus to enumerate interesting satisfiability queries" + help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones" [[option]] name = "sygusExprMinerCheckUseExport" |