diff options
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 2041a91b8..f9cabe62b 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -72,6 +72,9 @@ option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :de option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly + +option fullSaturateQuant --full-saturate-quant bool :default true + when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" choose literal matching mode |