diff options
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 48 |
1 files changed, 27 insertions, 21 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 94bc475d0..bc1a6929d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -640,32 +640,38 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( f, f[0][index] ); } if( d_int_rep[sortId].find( r )==d_int_rep[sortId].end() ){ - std::vector< Node > eqc; - getEquivalenceClass( r, eqc ); //find best selection for representative Node r_best; - int r_best_score = -1; - for( size_t i=0; i<eqc.size(); i++ ){ - int score = getRepScore( eqc[i], f, index ); - if( optInternalRepSortInference() ){ - int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i]); - if( score>=0 && e_sortId!=sortId ){ - score += 100; + if( options::fmfRelevantDomain() ){ + Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl; + r_best = d_qe->getModelEngine()->getRelevantDomain()->getRelevantTerm( f, index, r ); + Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl; + }else{ + std::vector< Node > eqc; + getEquivalenceClass( r, eqc ); + int r_best_score = -1; + for( size_t i=0; i<eqc.size(); i++ ){ + int score = getRepScore( eqc[i], f, index ); + if( optInternalRepSortInference() ){ + int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i]); + if( score>=0 && e_sortId!=sortId ){ + score += 100; + } + } + //score prefers earliest use of this term as a representative + if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){ + r_best = eqc[i]; + r_best_score = score; } } - //score prefers earliest use of this term as a representative - if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){ - r_best = eqc[i]; - r_best_score = score; + //now, make sure that no other member of the class is an instance + if( !optInternalRepSortInference() ){ + r_best = getInstance( r_best, eqc ); + } + //store that this representative was chosen at this point + if( d_rep_score.find( r_best )==d_rep_score.end() ){ + d_rep_score[ r_best ] = d_reset_count; } - } - //now, make sure that no other member of the class is an instance - if( !optInternalRepSortInference() ){ - r_best = getInstance( r_best, eqc ); - } - //store that this representative was chosen at this point - if( d_rep_score.find( r_best )==d_rep_score.end() ){ - d_rep_score[ r_best ] = d_reset_count; } d_int_rep[sortId][r] = r_best; if( r_best!=a ){ |