diff options
Diffstat (limited to 'src/theory/quantifiers/equality_query.cpp')
| -rw-r--r-- | src/theory/quantifiers/equality_query.cpp | 118 |
1 files changed, 59 insertions, 59 deletions
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 13e7b2eb7..355375d06 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -111,74 +111,74 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, } } } + TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType(); if (options::quantRepMode() == options::QuantRepMode::EE) { - return r; + int score = getRepScore(r, q, index, v_tn); + if (score >= 0) + { + return r; + } + // if we are not a valid representative, try to select one below + } + std::map<Node, Node>& v_int_rep = d_int_rep[v_tn]; + std::map<Node, Node>::const_iterator itir = v_int_rep.find(r); + if (itir != v_int_rep.end()) + { + return itir->second; } - else + // find best selection for representative + Node r_best; + std::vector<Node> eqc; + getEquivalenceClass(r, eqc); + Trace("internal-rep-select") + << "Choose representative for equivalence class : " << eqc + << ", type = " << v_tn << std::endl; + int r_best_score = -1; + for (const Node& n : eqc) { - TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType(); - std::map<Node, Node>& v_int_rep = d_int_rep[v_tn]; - std::map<Node, Node>::const_iterator itir = v_int_rep.find(r); - if (itir != v_int_rep.end()) + int score = getRepScore(n, q, index, v_tn); + if (score != -2) { - return itir->second; + if (r_best.isNull() + || (score >= 0 && (r_best_score < 0 || score < r_best_score))) + { + r_best = n; + r_best_score = score; + } } - else + } + if (r_best.isNull()) + { + Trace("internal-rep-warn") + << "No valid choice for representative in eqc class " << eqc + << std::endl; + return Node::null(); + } + // now, make sure that no other member of the class is an instance + std::unordered_map<TNode, Node, TNodeHashFunction> cache; + r_best = getInstance(r_best, eqc, cache); + // 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; + } + Trace("internal-rep-select") + << "...Choose " << r_best << " with score " << r_best_score + << " and type " << r_best.getType() << std::endl; + Assert(r_best.getType().isSubtypeOf(v_tn)); + v_int_rep[r] = r_best; + if (Trace.isOn("internal-rep-debug")) + { + if (r_best != a) { - //find best selection for representative - Node r_best; - // if( options::fmfRelevantDomain() && !q.isNull() ){ - // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << - // r << std::endl; - // r_best = d_qe->getRelevantDomain()->getRelevantTerm( q, index, r ); - // Trace("internal-rep-debug") << "Returned " << r_best << " " << r << - // std::endl; - //} - 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") << " }, type = " << v_tn << std::endl; - int r_best_score = -1; - for( size_t i=0; i<eqc.size(); i++ ){ - int score = getRepScore(eqc[i], q, index, v_tn); - if( score!=-2 ){ - if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){ - r_best = eqc[i]; - r_best_score = score; - } - } - } - if( r_best.isNull() ){ - Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl; - r_best = r; - } - //now, make sure that no other member of the class is an instance - std::unordered_map<TNode, Node, TNodeHashFunction> cache; - r_best = getInstance( r_best, eqc, cache ); - //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; - } - Trace("internal-rep-select") - << "...Choose " << r_best << " with score " << r_best_score - << " and type " << r_best.getType() << std::endl; - Assert(r_best.getType().isSubtypeOf(v_tn)); - v_int_rep[r] = r_best; - if( r_best!=a ){ - Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl; - Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl; - } - return r_best; + Trace("internal-rep-debug") + << "rep( " << a << " ) = " << r << ", " << std::endl; + Trace("internal-rep-debug") + << "int_rep( " << a << " ) = " << r_best << ", " << std::endl; } } + return r_best; } eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ |