Fix and refactor relevant domain (#6528)

In a handcrafted case, one can make the body of quantified formula another quantified formula when special attributes are used. The relevant domain utility was not robust to this case, leading to instantiations with free variables.

This fixes the issue and also updates its style to use a term context stack, which also avoids a tree traversal of the bodies of quantified formulas in this utility.

Fixes #6476. The benchmark from that issue now times out.

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index fab69106147b459401a949e863baefa787b77ce4..7e2c0c909f9614ed4bfb767ff79cfffa44dbf4e8 100644 (file)
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -15,6 +15,8 @@
 
 #include "theory/quantifiers/relevant_domain.h"
 
+#include "expr/term_context.h"
+#include "expr/term_context_stack.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_registry.h"
@@ -119,7 +121,7 @@ void RelevantDomain::compute(){
       Node q = fm->getAssertedQuantifier( i );
       Node icf = d_qreg.getInstConstantBody(q);
       Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
-      computeRelevantDomain( q, icf, true, true );
+      computeRelevantDomain(q);
     }
 
     Trace("rel-dom-debug") << "account for ground terms" << std::endl;
@@ -161,11 +163,58 @@ void RelevantDomain::compute(){
   }
 }
 
-void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool pol ) {
+void RelevantDomain::computeRelevantDomain(Node q)
+{
+  Assert(q.getKind() == FORALL);
+  Node n = d_qreg.getInstConstantBody(q);
+  // we care about polarity in the traversal, so we use a polarity term context
+  PolarityTermContext tc;
+  TCtxStack ctx(&tc);
+  ctx.pushInitial(n);
+  std::unordered_set<std::pair<Node, uint32_t>,
+                     PairHashFunction<Node, uint32_t, std::hash<Node> > >
+      visited;
+  std::pair<Node, uint32_t> curr;
+  Node node;
+  uint32_t nodeVal;
+  std::unordered_set<
+      std::pair<Node, uint32_t>,
+      PairHashFunction<Node, uint32_t, std::hash<Node> > >::const_iterator itc;
+  bool hasPol, pol;
+  while (!ctx.empty())
+  {
+    curr = ctx.getCurrent();
+    itc = visited.find(curr);
+    ctx.pop();
+    if (itc == visited.end())
+    {
+      visited.insert(curr);
+      node = curr.first;
+      // if not a quantified formula
+      if (!node.isClosure())
+      {
+        nodeVal = curr.second;
+        // get the polarity of the current term and process it
+        PolarityTermContext::getFlags(nodeVal, hasPol, pol);
+        computeRelevantDomainNode(q, node, hasPol, pol);
+        // traverse the children
+        ctx.pushChildren(node, nodeVal);
+      }
+    }
+  }
+}
+
+void RelevantDomain::computeRelevantDomainNode(Node q,
+                                               Node n,
+                                               bool hasPol,
+                                               bool pol)
+{
   Trace("rel-dom-debug") << "Compute relevant domain " << n << "..." << std::endl;
   Node op = d_treg.getTermDatabase()->getMatchOperator(n);
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    if( !op.isNull() ){
+  if (!op.isNull())
+  {
+    for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+    {
       RDomain * rf = getRDomain( op, i );
       if( n[i].getKind()==ITE ){
         for( unsigned j=1; j<=2; j++ ){
@@ -175,14 +224,6 @@ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool po
         computeRelevantDomainOpCh( rf, n[i] );
       }
     }
-    // do not recurse under nested closures
-    if (!n[i].isClosure())
-    {
-      bool newHasPol;
-      bool newPol;
-      QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
-      computeRelevantDomain( q, n[i], newHasPol, newPol );
-    }
   }
 
   if( ( ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) || n.getKind()==GEQ ) && TermUtil::hasInstConstAttr( n ) ){

diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 5581e932fd92a2bb43b071f0fd889bed25faaf7e..5643a466503ebf90505f7e1a263ceb2d4cfd4318 100644 (file)
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -153,10 +153,12 @@ class RelevantDomain : public QuantifiersUtil
   };
   /** Cache of the effect of literals on the relevant domain */
   std::map< bool, std::map< bool, std::map< Node, RDomainLit > > > d_rel_dom_lit;
+  /** Compute the relevant domain for quantified formula q. */
+  void computeRelevantDomain(Node q);
   /** Compute the relevant domain for a subformula n of q,
    * whose polarity is given by hasPol/pol.
    */
-  void computeRelevantDomain(Node q, Node n, bool hasPol, bool pol);
+  void computeRelevantDomainNode(Node q, Node n, bool hasPol, bool pol);
   /** Compute the relevant domain when the term n
    * is in a position to be included in relevant domain rf.
    */