diff options
| -rw-r--r-- | src/theory/quantifiers/ematching/candidate_generator.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/equality_query.cpp | 118 | ||||
| -rw-r--r-- | src/theory/quantifiers/fmf/model_engine.cpp | 5 | ||||
| -rw-r--r-- | src/theory/quantifiers_engine.h | 11 |
4 files changed, 75 insertions, 61 deletions
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 2a123e59c..ee6291564 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -185,7 +185,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() { if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ nh = d_qe->getInternalRepresentative( nh, d_f, d_index ); //don't consider this if already the instantiation is ineligible - if (!tdb->isTermEligibleForInstantiation(nh, d_f)) + if (!nh.isNull() && !tdb->isTermEligibleForInstantiation(nh, d_f)) { nh = Node::null(); } 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(){ diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 4012f687f..3fff374a7 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -182,6 +182,11 @@ int ModelEngine::checkModel(){ Trace("model-engine-debug") << " Term reps : "; for( size_t i=0; i<it->second.size(); i++ ){ Node r = d_quantEngine->getInternalRepresentative( it->second[i], Node::null(), 0 ); + if (r.isNull()) + { + // there was an invalid equivalence class + d_incomplete_check = true; + } Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 5172c1554..5d4ff6afe 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -232,7 +232,16 @@ public: bool usingModelEqualityEngine() const { return d_useModelEe; } /** debug print equality engine */ void debugPrintEqualityEngine( const char * c ); - /** get internal representative */ + /** get internal representative + * + * Choose a term that is equivalent to a in the current context that is the + * best term for instantiating the index^th variable of quantified formula q. + * If no legal term can be found, we return null. This can occur if: + * - a's type is not a subtype of the type of the index^th variable of q, + * - a is in an equivalent class with all terms that are restricted not to + * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample + * guided instantiation. + */ Node getInternalRepresentative( Node a, Node q, int index ); public: |