Make handling of illegal internal representatives in quantifiers engine more robust (#4034)

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.

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: