diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index abb84ccd7..c4b10eb6f 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -907,7 +907,8 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) { } } -bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) { +bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f) +{ if( options::lteRestrictInstClosure() ){ //has to be both in inst closure and in ground assertions if( !isInstClosure( n ) ){ @@ -937,7 +938,9 @@ bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) { } } } - return true; + // it cannot have instantiation constants, which originate from + // counterexample-guided instantiation strategies. + return !TermUtil::hasInstConstAttr(n); } Node TermDb::getEligibleTermInEqc( TNode r ) { @@ -949,11 +952,14 @@ Node TermDb::getEligibleTermInEqc( TNode r ) { Node h; eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); - while( h.isNull() && !eqc_i.isFinished() ){ + while (!eqc_i.isFinished()) + { TNode n = (*eqc_i); ++eqc_i; - if( hasTermCurrent( n ) ){ + if (isTermEligibleForInstantiation(n, TNode::null())) + { h = n; + break; } } d_term_elig_eqc[r] = h; |