Fix for corner case of higher-order matching (#1708)

1 files changed, 63 insertions, 21 deletions

diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 0e0955119..fad6334b8 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -236,7 +236,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
     {
       TNode var = ha.first;
       unsigned vnum = var.getAttribute(InstVarNumAttribute());
-      Node value = m.d_vals[vnum];
+      TNode value = m.d_vals[vnum];
       Trace("ho-unif-debug") << "  val[" << var << "] = " << value << std::endl;
 
       Trace("ho-unif-debug2") << "initialize lambda information..."
@@ -256,7 +256,17 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
       for (unsigned i = 0; i < ha.second.size(); i++)
       {
         std::vector<TNode> args;
-        Node f = uf::TheoryUfRewriter::decomposeHoApply(ha.second[i], args);
+        // must substitute the operator we matched with the original
+        // higher-order variable (var) that matched it. This ensures that the
+        // argument vector (args) below is of the proper length. This handles,
+        // for example, matches like:
+        //   (@ x y) with (@ (@ k1 k2) k3)
+        // where k3 but not k2 should be an argument of the match.
+        Node hmatch = ha.second[i];
+        Trace("ho-unif-debug2") << "Match is " << hmatch << std::endl;
+        hmatch = hmatch.substitute(value, var);
+        Trace("ho-unif-debug2") << "Pre-subs match is " << hmatch << std::endl;
+        Node f = uf::TheoryUfRewriter::decomposeHoApply(hmatch, args);
         // Assert( f==value );
         for (unsigned k = 0, size = args.size(); k < size; k++)
         {
@@ -348,7 +358,9 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
       Trace("ho-unif-debug2") << "finished." << std::endl;
     }
 
-    return sendInstantiation(m, 0);
+    bool ret = sendInstantiation(m, 0);
+    Trace("ho-unif-debug") << "Finished, success = " << ret << std::endl;
+    return ret;
   }
   else
   {
@@ -361,6 +373,8 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
 // occurring as pattern operators (very small)
 bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index)
 {
+  Trace("ho-unif-debug2") << "send inst " << var_index << " / "
+                          << d_ho_var_list.size() << std::endl;
   if (var_index == d_ho_var_list.size())
   {
     // we now have an instantiation to try
@@ -394,13 +408,18 @@ bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m,
                                               Node lbvl,
                                               bool arg_changed)
 {
+  Trace("ho-unif-debug2") << "send inst arg " << arg_index << " / "
+                          << lbvl.getNumChildren() << std::endl;
   if (arg_index == lbvl.getNumChildren())
   {
     // construct the lambda
     if (arg_changed)
     {
+      Trace("ho-unif-debug2")
+          << "  make lambda from children: " << d_lchildren[vnum] << std::endl;
       Node body =
           NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_lchildren[vnum]);
+      Trace("ho-unif-debug2") << "  got " << body << std::endl;
       Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, lbvl, body);
       m.d_vals[vnum] = lam;
       Trace("ho-unif-debug2") << "  try " << vnum << " -> " << lam << std::endl;
@@ -438,35 +457,58 @@ bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m,
 
 int HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
 {
+  if (d_ho_var_types.empty())
+  {
+    return 0;
+  }
+  Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl;
   unsigned numLemmas = 0;
-  if (!d_ho_var_types.empty())
+  // this forces expansion of APPLY_UF terms to curried HO_APPLY chains
+  unsigned size = d_quantEngine->getTermDatabase()->getNumOperators();
+  quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil();
+  NodeManager* nm = NodeManager::currentNM();
+  for (unsigned j = 0; j < size; j++)
   {
-    // this forces expansion of APPLY_UF terms to curried HO_APPLY chains
-    unsigned size = d_quantEngine->getTermDatabase()->getNumOperators();
-    for (unsigned j = 0; j < size; j++)
+    Node f = d_quantEngine->getTermDatabase()->getOperator(j);
+    if (f.isVar())
     {
-      Node f = d_quantEngine->getTermDatabase()->getOperator(j);
-      if (f.isVar())
+      TypeNode tn = f.getType();
+      if (tn.isFunction())
       {
-        TypeNode tn = f.getType();
-        if (d_ho_var_types.find(tn) != d_ho_var_types.end())
+        std::vector<TypeNode> argTypes = tn.getArgTypes();
+        Assert(argTypes.size() > 0);
+        TypeNode range = tn.getRangeType();
+        // for each function type suffix of the type of f, for example if
+        // f : (Int -> (Int -> Int))
+        // we iterate with stn = (Int -> (Int -> Int)) and (Int -> Int)
+        for (unsigned a = 0, size = argTypes.size(); a < size; a++)
         {
-          Node u = d_quantEngine->getTermUtil()->getHoTypeMatchPredicate(tn);
-          Node au = NodeManager::currentNM()->mkNode(kind::APPLY_UF, u, f);
-          if (d_quantEngine->addLemma(au))
+          std::vector<TypeNode> sargts;
+          sargts.insert(sargts.begin(), argTypes.begin() + a, argTypes.end());
+          Assert(sargts.size() > 0);
+          TypeNode stn = nm->mkFunctionType(sargts, range);
+          Trace("ho-quant-trigger-debug")
+              << "For " << f << ", check " << stn << "..." << std::endl;
+          // if a variable of this type occurs in this trigger
+          if (d_ho_var_types.find(stn) != d_ho_var_types.end())
           {
-            // this forces f to be a first-class member of the quantifier-free
-            // equality engine,
-            //  which in turn forces the quantifier-free theory solver to expand
-            //  it to HO_APPLY
-            Trace("ho-quant") << "Added ho match predicate lemma : " << au
-                              << std::endl;
-            numLemmas++;
+            Node u = tutil->getHoTypeMatchPredicate(tn);
+            Node au = nm->mkNode(kind::APPLY_UF, u, f);
+            if (d_quantEngine->addLemma(au))
+            {
+              // this forces f to be a first-class member of the quantifier-free
+              // equality engine, which in turn forces the quantifier-free
+              // theory solver to expand it to an HO_APPLY chain.
+              Trace("ho-quant")
+                  << "Added ho match predicate lemma : " << au << std::endl;
+              numLemmas++;
+            }
           }
         }
       }
     }
   }
+
   return numLemmas;
 }