diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-24 19:42:21 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-24 19:42:21 +0100 |
commit | 79ad2d6ec3ebd5c45dce4e13e895d0bed0a6f525 (patch) | |
tree | 7524e1376337c2b3d6544eeda832f8f3d574b409 /src/theory/quantifiers/term_database.cpp | |
parent | 73cecf65a750b9ee59486083af5ee55734da0a6a (diff) |
Variable patterns only look at eligible terms. Minor refactoring of quantifiers check for sat.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 73 |
1 files changed, 50 insertions, 23 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index fb28974a9..0f0329a93 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -338,33 +338,60 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) { } } -Node TermDb::getHasTermEqc( Node r ) { - if( hasTermCurrent( r ) ){ +bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) { + if( options::lteRestrictInstClosure() ){ + //has to be both in inst closure and in ground assertions + if( !isInstClosure( n ) ){ + Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl; + return false; + } + // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this + if( !hasTermCurrent( n, false ) ){ + Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl; + return false; + } + } + if( options::instMaxLevel()!=-1 ){ + if( n.hasAttribute(InstLevelAttribute()) ){ + int fml = f.isNull() ? -1 : getQAttrQuantInstLevel( f ); + unsigned ml = fml>=0 ? fml : options::instMaxLevel(); + + if( n.getAttribute(InstLevelAttribute())>ml ){ + Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute()); + Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl; + return false; + } + }else{ + if( options::instLevelInputOnly() ){ + Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl; + return false; + } + } + } + return true; +} + +Node TermDb::getEligibleTermInEqc( TNode r ) { + if( isTermEligibleForInstantiation( r, TNode::null() ) ){ return r; }else{ - /* - if( options::termDbInstClosure() ){ - std::map< Node, Node >::iterator it = d_has_eqc.find( r ); - if( it==d_has_eqc.end() ){ - Node h; - eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); - while( h.isNull() && !eqc_i.isFinished() ){ - TNode n = (*eqc_i); - ++eqc_i; - if( hasTermCurrent( n ) ){ - h = n; - } + std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r ); + if( it==d_term_elig_eqc.end() ){ + Node h; + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( h.isNull() && !eqc_i.isFinished() ){ + TNode n = (*eqc_i); + ++eqc_i; + if( hasTermCurrent( n ) ){ + h = n; } - d_has_eqc[r] = h; - return h; - }else{ - return it->second; } + d_term_elig_eqc[r] = h; + return h; + }else{ + return it->second; } - */ - //if not using inst closure, then either all are relevant, or it is a singleton irrelevant eqc - return Node::null(); } } @@ -404,7 +431,7 @@ void TermDb::reset( Theory::Effort effort ){ //compute has map if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){ d_has_map.clear(); - d_has_eqc.clear(); + d_term_elig_eqc.clear(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); while( !eqcs_i.isFinished() ){ TNode r = (*eqcs_i); |