diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-03-15 09:15:23 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-03-15 09:15:32 -0500 |
| commit | 0891afc4553d43475643145e3c8687a7c2b1af49 (patch) | |
| tree | 3be0dc50ef7b921eeeea7d6a2cc58f9b080499f8 /src/theory/quantifiers | |
| parent | d1a8a1854d9a71d409f6af23a1f52471fc34deb0 (diff) | |
changed default option for quantifier instantiation
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/options | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/options_handlers.h | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 222fc4425..e12a7d70f 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -56,7 +56,7 @@ option relevantTriggers /--disable-relevant-triggers bool :default true 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_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" +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 eagerInstQuant --eager-inst-quant bool :default false diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 312261d3c..01538d8cb 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -29,10 +29,10 @@ namespace quantifiers { static const std::string instWhenHelp = "\ Modes currently supported by the --inst-when option:\n\ \n\ -full\n\ +full (default)\n\ + Run instantiation round at full effort, before theory combination.\n\ \n\ -full-last-call (default)\n\ +full-last-call\n\ + Alternate running instantiation rounds at full effort and last\n\ call. In other words, interleave instantiation and theory combination.\n\ \n\ |