diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-21 13:40:00 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-22 12:58:36 -0600 |
| commit | 3da57075e8f810773ae95aadadc5408e0a537f02 (patch) | |
| tree | 6a91448ed48cecfe69ffa0a571ef45d83bf97661 /src/theory/quantifiers | |
| parent | 02efc4635cc200deb7884e55bf62feb7f19248b8 (diff) | |
Smarter options, but still have a bug
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/options | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 4a853b6cd..bfb1d6f65 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -91,7 +91,7 @@ option flipDecision --flip-decision/ bool :default false option internalReps /--disable-quant-internal-reps bool :default true disables instantiating with representatives chosen by quantifiers engine -option finiteModelFind --finite-model-find bool :default false +option finiteModelFind --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" @@ -113,7 +113,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 +option fmfBoundInt --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" |