From 0891afc4553d43475643145e3c8687a7c2b1af49 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 15 Mar 2013 09:15:23 -0500 Subject: [PATCH] changed default option for quantifier instantiation --- src/theory/quantifiers/options | 2 +- 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\ -- 2.30.2