diff options
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index dad173ff5..cac78af46 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -41,7 +41,7 @@ option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true option cnfQuant --cnf-quant bool :default false apply CNF conversion to quantified formulas # Whether to NNF quantifier bodies -option nnfQuant --nnf-quant bool :default false +option nnfQuant --nnf-quant bool :default true apply NNF conversion to quantified formulas option clauseSplit --clause-split bool :default false @@ -88,7 +88,7 @@ option fmfFunWellDefined --fmf-fun bool :default false option registerQuantBodyTerms --register-quant-body-terms bool :default false consider ground terms within bodies of quantified formulas for matching -option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" +option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" when to apply instantiation option instMaxLevel --inst-max-level=N int :read-write :default -1 maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) @@ -127,7 +127,7 @@ option finiteModelFind finite-model-find --finite-model-find bool :default false option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" choose mode for model-based quantifier instantiation -option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false +option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default false only add one instantiation per quantifier per round for mbqi option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false only add instantiations for one quantifier per round for mbqi @@ -196,5 +196,7 @@ option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMo option localTheoryExt --local-t-ext bool :default false do instantiation based on local theory extensions +option termDbInstClosure --term-db-inst-closure bool :default false + only consider inst closure terms for E-matching endmodule |