Fixes for higher-order (#1405)

4 files changed, 94 insertions, 50 deletions

diff --git a/src/theory/quantifiers/ho_trigger.cpp b/src/theory/quantifiers/ho_trigger.cpp
index 0386c0cf0..6354047cf 100644
--- a/src/theory/quantifiers/ho_trigger.cpp
+++ b/src/theory/quantifiers/ho_trigger.cpp
@@ -72,45 +72,87 @@ HigherOrderTrigger::HigherOrderTrigger(
 
 HigherOrderTrigger::~HigherOrderTrigger() {}
 void HigherOrderTrigger::collectHoVarApplyTerms(
-    Node q, TNode n, std::map<Node, std::vector<Node> >& apps)
+    Node q, Node& n, std::map<Node, std::vector<Node> >& apps)
 {
   std::vector<Node> ns;
   ns.push_back(n);
   collectHoVarApplyTerms(q, ns, apps);
+  Assert(ns.size() == 1);
+  n = ns[0];
 }
 
 void HigherOrderTrigger::collectHoVarApplyTerms(
     Node q, std::vector<Node>& ns, std::map<Node, std::vector<Node> >& apps)
 {
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
   // whether the visited node is a child of a HO_APPLY chain
   std::unordered_map<TNode, bool, TNodeHashFunction> withinApply;
-  std::stack<TNode> visit;
+  std::vector<TNode> visit;
   TNode cur;
-  for (unsigned i = 0; i < ns.size(); i++)
+  for (unsigned i = 0, size = ns.size(); i < size; i++)
   {
-    visit.push(ns[i]);
+    visit.push_back(ns[i]);
     withinApply[ns[i]] = false;
     do
     {
-      cur = visit.top();
-      visit.pop();
+      cur = visit.back();
+      visit.pop_back();
 
-      if (visited.find(cur) == visited.end())
+      it = visited.find(cur);
+      if (it == visited.end())
       {
-        visited.insert(cur);
-        bool curWithinApply = withinApply[cur];
-        if (!curWithinApply)
+        // do not look in nested quantifiers
+        if (cur.getKind() == FORALL)
+        {
+          visited[cur] = cur;
+        }
+        else
+        {
+          bool curWithinApply = withinApply[cur];
+          visited[cur] = Node::null();
+          visit.push_back(cur);
+          for (unsigned j = 0, size = cur.getNumChildren(); j < size; j++)
+          {
+            withinApply[cur[j]] = curWithinApply && j == 0;
+            visit.push_back(cur[j]);
+          }
+        }
+      }
+      else if (it->second.isNull())
+      {
+        // carry the conversion
+        Node ret = cur;
+        bool childChanged = false;
+        std::vector<Node> children;
+        if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
+        {
+          children.push_back(cur.getOperator());
+        }
+        for (const Node& nc : cur)
+        {
+          it = visited.find(nc);
+          Assert(it != visited.end());
+          Assert(!it->second.isNull());
+          childChanged = childChanged || nc != it->second;
+          children.push_back(it->second);
+        }
+        if (childChanged)
+        {
+          ret = NodeManager::currentNM()->mkNode(cur.getKind(), children);
+        }
+        // now, convert and store the application
+        if (!withinApply[cur])
         {
           TNode op;
-          if (cur.getKind() == kind::APPLY_UF)
+          if (ret.getKind() == kind::APPLY_UF)
           {
             // could be a fully applied function variable
-            op = cur.getOperator();
+            op = ret.getOperator();
           }
-          else if (cur.getKind() == kind::HO_APPLY)
+          else if (ret.getKind() == kind::HO_APPLY)
           {
-            op = cur;
+            op = ret;
             while (op.getKind() == kind::HO_APPLY)
             {
               op = op[0];
@@ -120,42 +162,27 @@ void HigherOrderTrigger::collectHoVarApplyTerms(
           {
             if (op.getKind() == kind::INST_CONSTANT)
             {
-              Assert(quantifiers::TermUtil::getInstConstAttr(cur) == q);
+              Assert(quantifiers::TermUtil::getInstConstAttr(ret) == q);
               Trace("ho-quant-trigger-debug")
-                  << "Ho variable apply term : " << cur << " with head " << op
+                  << "Ho variable apply term : " << ret << " with head " << op
                   << std::endl;
-              Node app = cur;
-              if (app.getKind() == kind::APPLY_UF)
+              if (ret.getKind() == kind::APPLY_UF)
               {
+                Node prev = ret;
                 // for consistency, convert to HO_APPLY if fully applied
-                app = uf::TheoryUfRewriter::getHoApplyForApplyUf(app);
+                ret = uf::TheoryUfRewriter::getHoApplyForApplyUf(ret);
               }
-              apps[op].push_back(cur);
-            }
-            if (cur.getKind() == kind::HO_APPLY)
-            {
-              curWithinApply = true;
+              apps[op].push_back(ret);
             }
           }
         }
-        else
-        {
-          if (cur.getKind() != HO_APPLY)
-          {
-            curWithinApply = false;
-          }
-        }
-        // do not look in nested quantifiers
-        if (cur.getKind() != FORALL)
-        {
-          for (unsigned i = 0, size = cur.getNumChildren(); i < size; i++)
-          {
-            withinApply[cur[i]] = curWithinApply && i == 0;
-            visit.push(cur[i]);
-          }
-        }
+        visited[cur] = ret;
       }
     } while (!visit.empty());
+
+    // store the conversion
+    Assert(visited.find(ns[i]) != visited.end());
+    ns[i] = visited[ns[i]];
   }
 }
 
diff --git a/src/theory/quantifiers/ho_trigger.h b/src/theory/quantifiers/ho_trigger.h
index 16d676353..e5112abce 100644
--- a/src/theory/quantifiers/ho_trigger.h
+++ b/src/theory/quantifiers/ho_trigger.h
@@ -101,16 +101,18 @@ class HigherOrderTrigger : public Trigger
  public:
   /** Collect higher order var apply terms
    *
-   * Collect all top-level HO_APPLY terms in n whose head is a variable in
-   * quantified formula q. Append all such terms in apps.
+   * Collect all top-level HO_APPLY terms in n whose head is a variable x in
+   * quantified formula q. Append all such terms in apps[x].
+   * This method may modify n so that it is in the expected form required for
+   * higher-order matching, in particular, APPLY_UF terms with variable
+   * operators are converted to curried applications of HO_APPLY.
    */
   static void collectHoVarApplyTerms(Node q,
-                                     TNode n,
+                                     Node& n,
                                      std::map<Node, std::vector<Node> >& apps);
   /** Collect higher order var apply terms
    *
-   * Collect all top-level HO_APPLY terms in terms ns whose head is a variable
-   * in quantified formula q, store in apps.
+   * Same as above, but with multiple terms ns.
    */
   static void collectHoVarApplyTerms(Node q,
                                      std::vector<Node>& ns,
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 4e75f7df8..def9a68bc 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -113,10 +113,19 @@ Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited )
 Node TermUtil::getInstConstAttr( Node n ) {
   if (!n.hasAttribute(InstConstantAttribute()) ){
     Node q;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      q = getInstConstAttr(n[i]);
-      if( !q.isNull() ){
-        break;
+    if (n.hasOperator())
+    {
+      q = getInstConstAttr(n.getOperator());
+    }
+    if (q.isNull())
+    {
+      for (const Node& nc : n)
+      {
+        q = getInstConstAttr(nc);
+        if (!q.isNull())
+        {
+          break;
+        }
       }
     }
     InstConstantAttribute ica;
@@ -277,6 +286,10 @@ void TermUtil::computeVarContains2( Node n, Kind k, std::vector< Node >& varCont
         varContains.push_back( n );
       }
     }else{
+      if (n.hasOperator())
+      {
+        computeVarContains2(n.getOperator(), k, varContains, visited);
+      }
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
         computeVarContains2( n[i], k, varContains, visited );
       }
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 61920250e..d06b5268b 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -223,6 +223,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
   Trace("trigger") << "Collect higher-order variable triggers..." << std::endl;
   std::map<Node, std::vector<Node> > ho_apps;
   HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps);
+  Trace("trigger") << "...got " << ho_apps.size()
+                   << " higher-order applications." << std::endl;
   Trigger* t;
   if (!ho_apps.empty())
   {