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 0865f2c0b..e733764f0 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -67,11 +67,13 @@ option registerQuantBodyTerms --register-quant-body-terms bool :default false 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" when to apply instantiation +option instMaxLevel --inst-max-level=N int :default -1 + maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly -option fullSaturateQuant --full-saturate-quant bool :default true +option fullSaturateQuant --full-saturate-quant bool :default false 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" @@ -95,7 +97,7 @@ option internalReps /--disable-quant-internal-reps bool :default true option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write use finite model finding heuristic for quantifier instantiation -option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :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" +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 only add one instantiation per quantifier per round for mbqi @@ -112,7 +114,7 @@ option fmfFreshDistConst --fmf-fresh-dc bool :default false use fresh distinguished representative when applying Inst-Gen techniques option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding -option fmfBoundInt --fmf-bound-int bool :default false :read-write +option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write finite model finding on bounded integer quantification option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h" |