diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-24 03:35:08 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-24 03:35:08 -0500 |
commit | bd3a86055008e692ac4e5e6fa5dfce9e78660d8a (patch) | |
tree | 59950b0d965b84bc55158013bbddaabbd1be05df /src/theory | |
parent | 766859010a5ca2cc94ffe69908dfe2606df2af28 (diff) |
Add --inst-max-level=N option for Kshitij. Support define-const command in Smt2.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/options | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 35 |
2 files changed, 24 insertions, 13 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 32e65438e..e733764f0 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -67,6 +67,8 @@ option registerQuantBodyTerms --register-quant-body-terms bool :default false 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 instMaxLevel --inst-max-level=N int :default -1 + maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index eaf5e8228..63697f5e7 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -319,7 +319,6 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std Trace("inst") << " " << terms[i]; Trace("inst") << std::endl; } - //uint64_t maxInstLevel = 0; if( options::cbqi() ){ for( int i=0; i<(int)terms.size(); i++ ){ if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){ @@ -328,22 +327,21 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std Debug("inst") << " " << terms[i] << std::endl; } Unreachable("Bad instantiation"); - }else{ - Trace("inst") << " " << terms[i]; - //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute()); - Trace("inst") << std::endl; - //if( terms[i].hasAttribute(InstLevelAttribute()) ){ - //if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ - // maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); - //} - //}else{ - //setInstantiationLevelAttr( terms[i], 0 ); - //} } } } + if( options::instMaxLevel()!=-1 ){ + uint64_t maxInstLevel = 0; + for( int i=0; i<(int)terms.size(); i++ ){ + if( terms[i].hasAttribute(InstLevelAttribute()) ){ + if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ + maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); + } + } + } + setInstantiationLevelAttr( body, maxInstLevel+1 ); + } Trace("inst-debug") << "*** Lemma is " << lem << std::endl; - //setInstantiationLevelAttr( body, maxInstLevel+1 ); ++(d_statistics.d_instantiations); return true; }else{ @@ -504,6 +502,17 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo } Trace("inst-add-debug") << std::endl; + if( options::instMaxLevel()!=-1 ){ + for( unsigned i=0; i<terms.size(); i++ ){ + if( terms[i].hasAttribute(InstLevelAttribute()) && + (int)terms[i].getAttribute(InstLevelAttribute())>options::instMaxLevel() ){ + Trace("inst-add-debug") << "Term " << terms[i] << " has instantiation level " << terms[i].getAttribute(InstLevelAttribute()); + Trace("inst-add-debug") << ", which is more than maximum allowed level " << options::instMaxLevel() << std::endl; + return false; + } + } + } + //check for duplication ///* bool alreadyExists = false; |