diff options
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 74ce3cc6c..a31fbe6e7 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -110,9 +110,6 @@ option fullSaturateQuantRd --full-saturate-quant-rd bool :default true 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 -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" - policy for instantiating axioms - ### finite model finding options option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write @@ -120,8 +117,10 @@ option finiteModelFind finite-model-find --finite-model-find bool :default false option quantFunWellDefined --quant-fun-wd bool :default false assume that function defined by quantifiers are well defined -option fmfFunWellDefined --fmf-fun bool :default false - find models for finite runs of defined functions, assumes functions are well-defined +option fmfFunWellDefined --fmf-fun bool :default false :read-write + find models for recursively defined functions, assumes functions are admissible +option fmfFunWellDefinedRelevant --fmf-fun-rlv bool :default false + find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant 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 |