From: Andrew Reynolds Date: Fri, 15 Mar 2013 14:15:23 +0000 (-0500) Subject: changed default option for quantifier instantiation X-Git-Tag: cvc5-1.0.0~7392 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0891afc4553d43475643145e3c8687a7c2b1af49;p=cvc5.git changed default option for quantifier instantiation --- 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\