Make handling of illegal internal representatives in quantifiers engine more robust...

Fixes #4002 (that benchmark is now unknown).

The experimental option --cbqi-all previously had some issues when combined with finite model finding. When these two options are used simultaneously, it may be the case that certain equivalence classes are "illegal" since they contain only terms that are ineligible for instantiation.

The previous code threw a warning when this occurred which in extreme cases allowed for potentially ineligible terms for instantiation. The new code is more conservative: we never choose illegal internal representatives and instead set the incomplete flag in finite model finding when this occurs.

A block of code changed indentation in this PR, which was updated to the new standards.

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 2a123e59cc04e0caa27b66d495c9335a3d89c3d6..ee629156492c1b445901974cfcacf3fc2fc9e47f 100644 (file)
--- 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 13e7b2eb7eaad3787dfdac266053dd5196ef63e4..355375d064df0155113033cc6d179e792765e18c 100644 (file)
--- 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 4012f687fa4b0af03f0ae8b35cdbc4d7fe75e911..3fff374a7de73d65c9662f719aa0f8c1bc850b59 100644 (file)
--- 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 5172c155464eaa2e759d5389a5b2ee4a33f45ac4..5d4ff6afed6631ff5f20ab1b453352d0ea6c34c4 100644 (file)
--- 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: