From 8829c2cbb569296c188ef4285c7fe9568148f48a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 21 May 2021 16:27:19 -0500
Subject: [PATCH] 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.
---
 src/theory/quantifiers/relevant_domain.cpp | 65 ++++++++++++++++++----
 src/theory/quantifiers/relevant_domain.h   |  4 +-
 2 files changed, 56 insertions(+), 13 deletions(-)

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index fab691061..7e2c0c909 100644
--- 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 5581e932f..5643a4665 100644
--- 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.
    */
-- 
2.30.2