Ensure uses of ground terms in triggers are preprocessed and registered (#5808)

This ensures ground terms in triggers are preprocessed and registered in the master equality engine. This avoids cases where our E-matching algorithm is incomplete where it should not be.

Positive impact (+222-69) on SMT-LIB, 30 second timeout

2 files changed, 130 insertions, 5 deletions

diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 34f413b71..ecd8164d5 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/ematching/trigger.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/ematching/candidate_generator.h"
 #include "theory/quantifiers/ematching/ho_trigger.h"
@@ -56,7 +57,14 @@ void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){
 Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector<Node>& nodes)
     : d_quantEngine(qe), d_quant(q)
 {
-  d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() );
+  // We must ensure that the ground subterms of the trigger have been
+  // preprocessed.
+  Valuation& val = qe->getValuation();
+  for (const Node& n : nodes)
+  {
+    Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms);
+    d_nodes.push_back(np);
+  }
   if (Trace.isOn("trigger"))
   {
     quantifiers::QuantAttributes* qa = d_quantEngine->getQuantAttributes();
@@ -92,7 +100,6 @@ Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector<Node>& nodes)
     ++(qe->d_statistics.d_multi_triggers);
   }
 
-  // Notice() << "Trigger : " << (*this) << "  for " << q << std::endl;
   Trace("trigger-debug") << "Finished making trigger." << std::endl;
 }
 
@@ -117,6 +124,26 @@ Node Trigger::getInstPattern() const
 
 uint64_t Trigger::addInstantiations()
 {
+  uint64_t gtAddedLemmas = 0;
+  if (!d_groundTerms.empty())
+  {
+    // for each ground term t that does not exist in the equality engine, we
+    // add a purification lemma of the form (k = t).
+    eq::EqualityEngine* ee = d_quantEngine->getEqualityQuery()->getEngine();
+    for (const Node& gt : d_groundTerms)
+    {
+      if (!ee->hasTerm(gt))
+      {
+        SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+        Node k = sm->mkPurifySkolem(gt, "gt");
+        Node eq = k.eqNode(gt);
+        Trace("trigger-gt-lemma")
+            << "Trigger: ground term purify lemma: " << eq << std::endl;
+        d_quantEngine->addLemma(eq);
+        gtAddedLemmas++;
+      }
+    }
+  }
   uint64_t addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this);
   if (Debug.isOn("inst-trigger"))
   {
@@ -126,7 +153,7 @@ uint64_t Trigger::addInstantiations()
                             << " lemmas, trigger was " << d_nodes << std::endl;
     }
   }
-  return addedLemmas;
+  return gtAddedLemmas + addedLemmas;
 }
 
 bool Trigger::sendInstantiation(InstMatch& m)
@@ -999,6 +1026,70 @@ int Trigger::getActiveScore() {
   return d_mg->getActiveScore( d_quantEngine );
 }
 
+Node Trigger::ensureGroundTermPreprocessed(Valuation& val,
+                                           Node n,
+                                           std::vector<Node>& gts)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+    if (it == visited.end())
+    {
+      if (cur.getNumChildren() == 0)
+      {
+        visited[cur] = cur;
+      }
+      else if (!quantifiers::TermUtil::hasInstConstAttr(cur))
+      {
+        // cur has no INST_CONSTANT, thus is ground.
+        Node vcur = val.getPreprocessedTerm(cur);
+        gts.push_back(vcur);
+        visited[cur] = vcur;
+      }
+      else
+      {
+        visited[cur] = Node::null();
+        visit.push_back(cur);
+        visit.insert(visit.end(), cur.begin(), cur.end());
+      }
+    }
+    else if (it->second.isNull())
+    {
+      Node ret = cur;
+      bool childChanged = false;
+      std::vector<Node> children;
+      if (cur.getMetaKind() == metakind::PARAMETERIZED)
+      {
+        children.push_back(cur.getOperator());
+      }
+      for (const Node& cn : cur)
+      {
+        it = visited.find(cn);
+        Assert(it != visited.end());
+        Assert(!it->second.isNull());
+        childChanged = childChanged || cn != it->second;
+        children.push_back(it->second);
+      }
+      if (childChanged)
+      {
+        ret = nm->mkNode(cur.getKind(), children);
+      }
+      visited[cur] = ret;
+    }
+  } while (!visit.empty());
+  Assert(visited.find(n) != visited.end());
+  Assert(!visited.find(n)->second.isNull());
+  return visited[n];
+}
+
 void Trigger::debugPrint(const char* c) const
 {
   Trace(c) << "TRIGGER( " << d_nodes << " )" << std::endl;
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index 201d4258b..9fbf41674 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -20,8 +20,9 @@
 #include <map>
 
 #include "expr/node.h"
-#include "theory/quantifiers/inst_match.h"
 #include "options/quantifiers_options.h"
+#include "theory/quantifiers/inst_match.h"
+#include "theory/valuation.h"
 
 namespace CVC4 {
 namespace theory {
@@ -414,8 +415,41 @@ class Trigger {
    * Instantiate::addInstantiation(...).
    */
   virtual bool sendInstantiation(InstMatch& m);
+  /**
+   * Ensure that all ground subterms of n have been preprocessed. This makes
+   * calls to the provided valuation to obtain the preprocessed form of these
+   * terms. The preprocessed form of each ground subterm is added to gts.
+   *
+   * As an optimization, this method does not preprocess terms with no
+   * arguments, e.g. variables and constants are not preprocessed (as they
+   * should not change after preprocessing), nor are they added to gts.
+   *
+   * @param val The valuation to use for looking up preprocessed terms.
+   * @param n The node to process, which is in inst-constant form (free
+   * variables have been substituted by corresponding INST_CONSTANT).
+   * @param gts The set of preprocessed ground subterms of n.
+   * @return The converted form of n where all ground subterms have been
+   * replaced by their preprocessed form.
+   */
+  static Node ensureGroundTermPreprocessed(Valuation& val,
+                                           Node n,
+                                           std::vector<Node>& gts);
   /** The nodes comprising this trigger. */
-  std::vector< Node > d_nodes;
+  std::vector<Node> d_nodes;
+  /**
+   * The preprocessed ground terms in the nodes of the trigger, which as an
+   * optimization omits variables and constant subterms. These terms are
+   * important since we must ensure that the quantifier-free solvers are
+   * aware of these terms. In particular, when adding instantiations for
+   * a trigger P(f(a), x), we first check if f(a) is a term in the master
+   * equality engine. If it is not, then we add the lemma k = f(a) where k
+   * is the purification skolem for f(a). This ensures that f(a) will be
+   * registered as a term in the master equality engine on the next
+   * instantiation round. This is particularly important for cases where
+   * P(f(a), x) is matched with P(f(b), c), where a=b in the current context.
+   * This example would fail to match when f(a) is not registered.
+   */
+  std::vector<Node> d_groundTerms;
   /** The quantifiers engine associated with this trigger. */
   QuantifiersEngine* d_quantEngine;
   /** The quantified formula this trigger is for. */