diff options
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 1eb98e7b7..f485b981c 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -95,11 +95,9 @@ option internalReps /--disable-quant-internal-reps bool :default true option finiteModelFind --finite-model-find bool :default false use finite model finding heuristic for quantifier instantiation -option fmfModelBasedInst /--disable-fmf-mbqi bool :default true - disable model-based quantifier instantiation for finite model finding +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" + choose mode for model-based quantifier instantiation -option fmfFullModelCheck --fmf-fmc bool :default false :read-write - enable full model check for finite model finding option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding option fmfFmcCoverSimplify /--disable-fmf-fmc-cover-simplify bool :default true @@ -115,8 +113,6 @@ option fmfInstEngine --fmf-inst-engine bool :default false use instantiation engine in conjunction with finite model finding option fmfRelevantDomain --fmf-relevant-domain bool :default false use relevant domain computation, similar to complete instantiation (Ge, deMoura 09) -option fmfNewInstGen --fmf-new-inst-gen bool :default false - use new inst gen technique for answering sat without exhaustive instantiation option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true enable Inst-Gen instantiation techniques for finite model finding (default) /disable Inst-Gen instantiation techniques for finite model finding |