diff options
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rwxr-xr-x | src/theory/quantifiers_engine.cpp | 26 |
1 files changed, 17 insertions, 9 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0fe50aad6..2ae5edb39 100755 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -632,8 +632,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, return r; }else{ int sortId = 0; - if( optInternalRepSortInference() ){ - //if( options::ufssSymBreak() ){ + if( optInternalRepSortInference() && !f.isNull() ){ sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( f, f[0][index] ); } if( d_int_rep[sortId].find( r )==d_int_rep[sortId].end() ){ @@ -646,12 +645,20 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, }else{ std::vector< Node > eqc; getEquivalenceClass( r, eqc ); + Trace("internal-rep-select") << "Choose representative for equivalence class : { "; + for( unsigned i=0; i<eqc.size(); i++ ){ + if( i>0 ) Trace("internal-rep-select") << ", "; + Trace("internal-rep-select") << eqc[i]; + } + Trace("internal-rep-select") << " } " << std::endl; int r_best_score = -1; for( size_t i=0; i<eqc.size(); i++ ){ - int score = getRepScore( eqc[i], f, index ); + //if cbqi is active, do not choose instantiation constant terms if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc[i]) ){ - if( optInternalRepSortInference() ){ - int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i]); + int score = getRepScore( eqc[i], f, index ); + //base it on sort information as well + if( sortId!=0 ){ + int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i] ); if( score>=0 && e_sortId!=sortId ){ score += 100; } @@ -661,12 +668,12 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, r_best = eqc[i]; r_best_score = score; } - } + } } if( r_best.isNull() ){ - Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index ); - r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); - } + Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index ); + r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); + } //now, make sure that no other member of the class is an instance if( !optInternalRepSortInference() ){ r_best = getInstance( r_best, eqc ); @@ -675,6 +682,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, if( d_rep_score.find( r_best )==d_rep_score.end() ){ d_rep_score[ r_best ] = d_reset_count; } + Trace("internal-rep-select") << "...Choose " << r_best << std::endl; } d_int_rep[sortId][r] = r_best; if( r_best!=a ){ |