Improve trigger filter instances (#1402)

1 files changed, 179 insertions, 17 deletions

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index d06b5268b..ce306541f 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -42,6 +42,7 @@ void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){
   }else{
     //determined a ground (dis)equality must hold or else q is a tautology?
   }
+  d_weight = Trigger::getTriggerWeight(n);
 }
 
 /** trigger class constructor */
@@ -220,7 +221,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
   }
 
   // check if higher-order
-  Trace("trigger") << "Collect higher-order variable triggers..." << std::endl;
+  Trace("trigger-debug") << "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()
@@ -490,9 +492,15 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod
               tinfo.erase( added2[i] );
             }else{
               if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
-                //discard if we added a subterm as a trigger with all variables that nu has
-                Trace("auto-gen-trigger-debug2") << "......subsumes parent." << std::endl;
-                rm_nu = true;
+                if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
+                {
+                  // discard if we added a subterm as a trigger with all
+                  // variables that nu has
+                  Trace("auto-gen-trigger-debug2")
+                      << "......subsumes parent " << tinfo[nu].d_weight << " "
+                      << tinfo[added2[i]].d_weight << "." << std::endl;
+                  rm_nu = true;
+                }
               }
               if( std::find( added.begin(), added.end(), added2[i] )==added.end() ){
                 added.push_back( added2[i] );
@@ -550,8 +558,13 @@ bool Trigger::isPureTheoryTrigger( Node n ) {
 }
 
 int Trigger::getTriggerWeight( Node n ) {
-  if( isAtomicTrigger( n ) ){
+  if (n.getKind() == APPLY_UF)
+  {
     return 0;
+  }
+  else if (isAtomicTrigger(n))
+  {
+    return 1;
   }else{
     if( options::relationalTriggers() ){
       if( isRelationalTrigger( n ) ){
@@ -562,7 +575,7 @@ int Trigger::getTriggerWeight( Node n ) {
         }
       }
     }
-    return 1;
+    return 2;
   }
 }
 
@@ -608,18 +621,25 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu
     collectPatTerms( q, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo2, false );
     std::vector< Node > temp;
     temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
-    quantifiers::TermUtil::filterInstances( temp );
-    if( temp.size()!=patTerms2.size() ){
-      Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl;
-      Trace("trigger-filter-instance") << "Old: ";
-      for( unsigned i=0; i<patTerms2.size(); i++ ){
-        Trace("trigger-filter-instance") << patTerms2[i] << " ";
-      }
-      Trace("trigger-filter-instance") << std::endl << "New: ";
-      for( unsigned i=0; i<temp.size(); i++ ){
-        Trace("trigger-filter-instance") << temp[i] << " ";
+    filterTriggerInstances(temp);
+    if (Trace.isOn("trigger-filter-instance"))
+    {
+      if (temp.size() != patTerms2.size())
+      {
+        Trace("trigger-filter-instance") << "Filtered an instance: "
+                                         << std::endl;
+        Trace("trigger-filter-instance") << "Old: ";
+        for (unsigned i = 0; i < patTerms2.size(); i++)
+        {
+          Trace("trigger-filter-instance") << patTerms2[i] << " ";
+        }
+        Trace("trigger-filter-instance") << std::endl << "New: ";
+        for (unsigned i = 0; i < temp.size(); i++)
+        {
+          Trace("trigger-filter-instance") << temp[i] << " ";
+        }
+        Trace("trigger-filter-instance") << std::endl;
       }
-      Trace("trigger-filter-instance") << std::endl;
     }
     if( tstrt==quantifiers::TRIGGER_SEL_ALL ){
       for( unsigned i=0; i<temp.size(); i++ ){
@@ -646,6 +666,148 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu
   }
 }
 
+int Trigger::isTriggerInstanceOf(Node n1,
+                                 Node n2,
+                                 std::vector<Node>& fv1,
+                                 std::vector<Node>& fv2)
+{
+  Assert(n1 != n2);
+  int status = 0;
+  std::unordered_set<TNode, TNodeHashFunction> subs_vars;
+  std::unordered_set<std::pair<TNode, TNode>,
+                     PairHashFunction<TNode,
+                                      TNode,
+                                      TNodeHashFunction,
+                                      TNodeHashFunction> >
+      visited;
+  std::vector<std::pair<TNode, TNode> > visit;
+  std::pair<TNode, TNode> cur;
+  TNode cur1;
+  TNode cur2;
+  visit.push_back(std::pair<TNode, TNode>(n1, n2));
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      visited.insert(cur);
+      cur1 = cur.first;
+      cur2 = cur.second;
+      Assert(cur1 != cur2);
+      // recurse if they have the same operator
+      if (cur1.hasOperator() && cur2.hasOperator()
+          && cur1.getNumChildren() == cur2.getNumChildren()
+          && cur1.getOperator() == cur2.getOperator()
+          && cur1.getOperator().getKind()!=INST_CONSTANT)
+      {
+        visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
+        for (unsigned i = 0, size = cur1.getNumChildren(); i < size; i++)
+        {
+          if (cur1[i] != cur2[i])
+          {
+            visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
+          }
+          else if (cur1[i].getKind() == INST_CONSTANT)
+          {
+            if (subs_vars.find(cur1[i]) != subs_vars.end())
+            {
+              return 0;
+            }
+            // the variable must map to itself in the substitution
+            subs_vars.insert(cur1[i]);
+          }
+        }
+      }
+      else
+      {
+        bool success = false;
+        // check if we are in a unifiable instance case
+        // must be only this case
+        for (unsigned r = 0; r < 2; r++)
+        {
+          if (status == 0 || ((status == 1) == (r == 0)))
+          {
+            TNode curi = r == 0 ? cur1 : cur2;
+            if (curi.getKind() == INST_CONSTANT
+                && subs_vars.find(curi) == subs_vars.end())
+            {
+              TNode curj = r == 0 ? cur2 : cur1;
+              // RHS must be a simple trigger
+              if (getTriggerWeight(curj) == 0)
+              {
+                // must occur in the free variables in the other
+                std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
+                if (std::find(free_vars.begin(), free_vars.end(), curi)
+                    != free_vars.end())
+                {
+                  status = r == 0 ? 1 : -1;
+                  subs_vars.insert(curi);
+                  success = true;
+                  break;
+                }
+              }
+            }
+          }
+        }
+        if (!success)
+        {
+          return 0;
+        }
+      }
+    }
+  } while (!visit.empty());
+  return status;
+}
+
+void Trigger::filterTriggerInstances(std::vector<Node>& nodes)
+{
+  std::map<unsigned, std::vector<Node> > fvs;
+  for (unsigned i = 0, size = nodes.size(); i < size; i++)
+  {
+    quantifiers::TermUtil::computeVarContains(nodes[i], fvs[i]);
+  }
+  std::vector<bool> active;
+  active.resize(nodes.size(), true);
+  for (unsigned i = 0, size = nodes.size(); i < size; i++)
+  {
+    std::vector<Node>& fvsi = fvs[i];
+    if (active[i])
+    {
+      for (unsigned j = i + 1, size2 = nodes.size(); j < size2; j++)
+      {
+        if (active[j])
+        {
+          int result = isTriggerInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
+          if (result == 1)
+          {
+            Trace("filter-instances") << nodes[j] << " is an instance of "
+                                      << nodes[i] << std::endl;
+            active[i] = false;
+            break;
+          }
+          else if (result == -1)
+          {
+            Trace("filter-instances") << nodes[i] << " is an instance of "
+                                      << nodes[j] << std::endl;
+            active[j] = false;
+          }
+        }
+      }
+    }
+  }
+  std::vector<Node> temp;
+  for (unsigned i = 0; i < nodes.size(); i++)
+  {
+    if (active[i])
+    {
+      temp.push_back(nodes[i]);
+    }
+  }
+  nodes.clear();
+  nodes.insert(nodes.begin(), temp.begin(), temp.end());
+}
+
 Node Trigger::getInversionVariable( Node n ) {
   if( n.getKind()==INST_CONSTANT ){
     return n;