Make candidate rewrite match filtering handle polymorphic operators properly (#2236)

Currently, the discrimination tree index used for candidate rewrite rule filtering based on matching does not properly distinguish polymorphic operators, which leads to type errors. This makes the index handle them correctly.

Fixes #1923.

4 files changed, 66 insertions, 25 deletions

diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp
index 118c073a0..bf2248e25 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp
@@ -219,15 +219,12 @@ void CandidateRewriteFilter::initialize(SygusSampler* ss,
   // initialize members of this class
   d_match_trie.clear();
   d_pairs.clear();
-  if (options::sygusRewSynthFilterCong())
-  {
-    // initialize the dynamic rewriter
-    std::stringstream ss;
-    ss << "_dyn_rewriter_" << drewrite_counter;
-    drewrite_counter++;
-    d_drewrite = std::unique_ptr<DynamicRewriter>(
-        new DynamicRewriter(ss.str(), &d_fake_context));
-  }
+  // (re)initialize the dynamic rewriter
+  std::stringstream ssn;
+  ssn << "_dyn_rewriter_" << drewrite_counter;
+  drewrite_counter++;
+  d_drewrite = std::unique_ptr<DynamicRewriter>(
+      new DynamicRewriter(ssn.str(), &d_fake_context));
 }
 
 bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)
@@ -285,7 +282,7 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)
   }
 
   // ----- check rewriting redundancy
-  if (keep && d_drewrite != nullptr)
+  if (keep && options::sygusRewSynthFilterCong())
   {
     Trace("cr-filter-debug") << "Check equal rewrite pair..." << std::endl;
     if (d_drewrite->areEqual(bn, beq_n))
@@ -296,14 +293,15 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)
     }
   }
 
-  if (options::sygusRewSynthFilterMatch())
+  if (keep && options::sygusRewSynthFilterMatch())
   {
     // ----- check matchable
     // check whether the pair is matchable with a previous one
     d_curr_pair_rhs = beq_n;
     Trace("crf-match") << "CRF check matches : " << bn << " [rhs = " << beq_n
                        << "]..." << std::endl;
-    if (!d_match_trie.getMatches(bn, &d_ssenm))
+    Node bni = d_drewrite->toInternal(bn);
+    if (!d_match_trie.getMatches(bni, &d_ssenm))
     {
       keep = false;
       Trace("cr-filter") << "...redundant (matchable)" << std::endl;
@@ -340,7 +338,7 @@ void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n)
     beq_n = d_tds->sygusToBuiltin(eq_n);
   }
   // ----- check rewriting redundancy
-  if (d_drewrite != nullptr)
+  if (options::sygusRewSynthFilterCong())
   {
     Trace("cr-filter-debug") << "Add rewrite pair..." << std::endl;
     Assert(!d_drewrite->areEqual(bn, beq_n));
@@ -357,7 +355,8 @@ void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n)
       if (d_pairs.find(t) == d_pairs.end())
       {
         Trace("crf-match") << "CRF add term : " << t << std::endl;
-        d_match_trie.addTerm(t);
+        Node ti = d_drewrite->toInternal(t);
+        d_match_trie.addTerm(ti);
       }
       d_pairs[t].insert(to);
     }
@@ -369,7 +368,13 @@ bool CandidateRewriteFilter::notify(Node s,
                                     std::vector<Node>& vars,
                                     std::vector<Node>& subs)
 {
+  Trace("crf-match-debug") << "Got : " << s << " matches " << n << std::endl;
   Assert(!d_curr_pair_rhs.isNull());
+  // convert back to original forms
+  s = d_drewrite->toExternal(s);
+  Assert(!s.isNull());
+  n = d_drewrite->toExternal(n);
+  Assert(!n.isNull());
   std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator it =
       d_pairs.find(n);
   if (Trace.isOn("crf-match"))
@@ -379,18 +384,29 @@ bool CandidateRewriteFilter::notify(Node s,
     for (unsigned i = 0, size = vars.size(); i < size; i++)
     {
       Trace("crf-match") << "    " << vars[i] << " -> " << subs[i] << std::endl;
-      // TODO (#1923) ensure that we use an internal representation to
-      // ensure polymorphism is handled correctly
-      Assert(vars[i].getType().isComparableTo(subs[i].getType()));
     }
   }
+#ifdef CVC4_ASSERTIONS
+  for (unsigned i = 0, size = vars.size(); i < size; i++)
+  {
+    // By using internal representation of terms, we ensure polymorphism is
+    // handled correctly.
+    Assert(vars[i].getType().isComparableTo(subs[i].getType()));
+  }
+#endif
+  // must convert the inferred substitution to original form
+  std::vector<Node> esubs;
+  for (const Node& s : subs)
+  {
+    esubs.push_back(d_drewrite->toExternal(s));
+  }
   Assert(it != d_pairs.end());
   for (const Node& nr : it->second)
   {
     Node nrs =
-        nr.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+        nr.substitute(vars.begin(), vars.end(), esubs.begin(), esubs.end());
     bool areEqual = (nrs == d_curr_pair_rhs);
-    if (!areEqual && d_drewrite != nullptr)
+    if (!areEqual && options::sygusRewSynthFilterCong())
     {
       // if dynamic rewriter is available, consult it
       areEqual = d_drewrite->areEqual(nrs, d_curr_pair_rhs);
diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h
index 9a09680cc..ca071faa4 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.h
+++ b/src/theory/quantifiers/candidate_rewrite_filter.h
@@ -165,7 +165,13 @@ class CandidateRewriteFilter
    * detail, if (t,s) is a relevant pair, then t in d_pairs[s].
    */
   std::map<Node, std::unordered_set<Node, NodeHashFunction> > d_pairs;
-  /** Match trie storing all terms in the domain of d_pairs. */
+  /** Match trie storing all terms in the domain of d_pairs.
+   *
+   * Notice that we store d_drewrite->toInternal(t) instead of t, for each
+   * term t, so that polymorphism is handled properly. In particular, this
+   * prevents matches between terms select( x, y ) and select( z, y ) where
+   * the type of x and z are different.
+   */
   MatchTrie d_match_trie;
   /** Notify class */
   class CandidateRewriteFilterNotifyMatch : public NotifyMatch
diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp
index ef1cb3a9d..d8c5ac7b5 100644
--- a/src/theory/quantifiers/dynamic_rewrite.cpp
+++ b/src/theory/quantifiers/dynamic_rewrite.cpp
@@ -124,9 +124,20 @@ Node DynamicRewriter::toInternal(Node a)
     }
   }
   d_term_to_internal[a] = ret;
+  d_internal_to_term[ret] = a;
   return ret;
 }
 
+Node DynamicRewriter::toExternal(Node ai)
+{
+  std::map<Node, Node>::iterator it = d_internal_to_term.find(ai);
+  if (it != d_internal_to_term.end())
+  {
+    return it->second;
+  }
+  return Node::null();
+}
+
 Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n)
 {
   std::vector<TypeNode> ctypes;
diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h
index 75f668b11..50bae0268 100644
--- a/src/theory/quantifiers/dynamic_rewrite.h
+++ b/src/theory/quantifiers/dynamic_rewrite.h
@@ -62,6 +62,17 @@ class DynamicRewriter
    * Check whether this class knows that the equality a = b holds.
    */
   bool areEqual(Node a, Node b);
+  /**
+   * Convert node a to its internal representation, which replaces all
+   * interpreted operators in a by a unique uninterpreted symbol.
+   */
+  Node toInternal(Node a);
+  /**
+   * Convert internal node ai to its original representation. It is the case
+   * that toExternal(toInternal(a))=a. If ai is not a term returned by
+   * toInternal, this method returns null.
+   */
+  Node toExternal(Node ai);
 
  private:
   /** index over argument types to function skolems
@@ -96,13 +107,10 @@ class DynamicRewriter
   };
   /** the internal operator symbol trie for this class */
   std::map<Node, OpInternalSymTrie> d_ois_trie;
-  /**
-   * Convert node a to its internal representation, which replaces all
-   * interpreted operators in a by a unique uninterpreted symbol.
-   */
-  Node toInternal(Node a);
   /** cache of the above function */
   std::map<Node, Node> d_term_to_internal;
+  /** inverse of the above map */
+  std::map<Node, Node> d_internal_to_term;
   /** stores congruence closure over terms given to this class. */
   eq::EqualityEngine d_equalityEngine;
   /** list of all equalities asserted to equality engine */