[quantifiers] Fix prenex computation (#5879)

Previously our prenex computation could generate quantifiers of the form forall x y y. F, which would lead to an assertion failure in getFreeVariablesScope, as it assumes that no shadowing occurs. This commit makes the prenex computation take a set rather than a vector, thus avoiding duplications of prenexed variables. It also changes mkForall to take a constant vector, since it does not modify the given vector.

Fixes #5693 

3 files changed, 89 insertions, 65 deletions

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 2439e28b6..34ebfcd59 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -375,7 +375,8 @@ bool getFreeVariablesScope(TNode n,
         for (const TNode& cn : cur[0])
         {
           // should not shadow
-          Assert(scope.find(cn) == scope.end());
+          Assert(scope.find(cn) == scope.end())
+              << "Shadowed variable " << cn << " in " << cur << "\n";
           scope.insert(cn);
         }
         // must make recursive call to use separate cache
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 6ca2e5b22..2126bf1f0 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1237,12 +1237,13 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
   return body;
 }
 
-Node QuantifiersRewriter::computePrenex(Node q,
-                                        Node body,
-                                        std::vector<Node>& args,
-                                        std::vector<Node>& nargs,
-                                        bool pol,
-                                        bool prenexAgg)
+Node QuantifiersRewriter::computePrenex(
+    Node q,
+    Node body,
+    std::unordered_set<Node, NodeHashFunction>& args,
+    std::unordered_set<Node, NodeHashFunction>& nargs,
+    bool pol,
+    bool prenexAgg)
 {
   NodeManager* nm = NodeManager::currentNM();
   Kind k = body.getKind();
@@ -1271,10 +1272,13 @@ Node QuantifiersRewriter::computePrenex(Node q,
         }
         subs.push_back(vv);
       }
-      if( pol ){
-        args.insert( args.end(), subs.begin(), subs.end() );
-      }else{
-        nargs.insert( nargs.end(), subs.begin(), subs.end() );
+      if (pol)
+      {
+        args.insert(subs.begin(), subs.end());
+      }
+      else
+      {
+        nargs.insert(subs.begin(), subs.end());
       }
       Node newBody = body[1];
       newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
@@ -1368,45 +1372,43 @@ Node QuantifiersRewriter::computePrenexAgg(Node n,
   }
   else
   {
-    std::vector<Node> args;
-    std::vector<Node> nargs;
+    std::unordered_set<Node, NodeHashFunction> argsSet;
+    std::unordered_set<Node, NodeHashFunction> nargsSet;
     Node q;
-    Node nn = computePrenex(q, n, args, nargs, true, true);
+    Node nn = computePrenex(q, n, argsSet, nargsSet, true, true);
+    Assert(n != nn || argsSet.empty());
+    Assert(n != nn || nargsSet.empty());
     if (n != nn)
     {
       Node nnn = computePrenexAgg(nn, visited);
       // merge prenex
       if (nnn.getKind() == FORALL)
       {
-        args.insert(args.end(), nnn[0].begin(), nnn[0].end());
+        argsSet.insert(nnn[0].begin(), nnn[0].end());
         nnn = nnn[1];
         // pos polarity variables are inner
-        if (!args.empty())
+        if (!argsSet.empty())
         {
-          nnn = mkForall(args, nnn, true);
+          nnn = mkForall({argsSet.begin(), argsSet.end()}, nnn, true);
         }
-        args.clear();
+        argsSet.clear();
       }
       else if (nnn.getKind() == NOT && nnn[0].getKind() == FORALL)
       {
-        nargs.insert(nargs.end(), nnn[0][0].begin(), nnn[0][0].end());
+        nargsSet.insert(nnn[0][0].begin(), nnn[0][0].end());
         nnn = nnn[0][1].negate();
       }
-      if (!nargs.empty())
+      if (!nargsSet.empty())
       {
-        nnn = mkForall(nargs, nnn.negate(), true).negate();
+        nnn = mkForall({nargsSet.begin(), nargsSet.end()}, nnn.negate(), true)
+                  .negate();
       }
-      if (!args.empty())
+      if (!argsSet.empty())
       {
-        nnn = mkForall(args, nnn, true);
+        nnn = mkForall({argsSet.begin(), argsSet.end()}, nnn, true);
       }
       ret = nnn;
     }
-    else
-    {
-      Assert(args.empty());
-      Assert(nargs.empty());
-    }
   }
   visited[n] = ret;
   return ret;
@@ -1516,43 +1518,58 @@ Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QA
   }
 }
 
-Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ){
-  if( args.empty() ){
+Node QuantifiersRewriter::mkForAll(const std::vector<Node>& args,
+                                   Node body,
+                                   QAttributes& qa)
+{
+  if (args.empty())
+  {
     return body;
-  }else{
-    std::vector< Node > children;
-    children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
-    children.push_back( body );
-    if( !qa.d_ipl.isNull() ){
-      children.push_back( qa.d_ipl );
-    }
-    return NodeManager::currentNM()->mkNode( kind::FORALL, children );
   }
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<Node> children;
+  children.push_back(nm->mkNode(kind::BOUND_VAR_LIST, args));
+  children.push_back(body);
+  if (!qa.d_ipl.isNull())
+  {
+    children.push_back(qa.d_ipl);
+  }
+  return nm->mkNode(kind::FORALL, children);
 }
 
-Node QuantifiersRewriter::mkForall( std::vector< Node >& args, Node body, bool marked ) {
+Node QuantifiersRewriter::mkForall(const std::vector<Node>& args,
+                                   Node body,
+                                   bool marked)
+{
   std::vector< Node > iplc;
   return mkForall( args, body, iplc, marked );
 }
 
-Node QuantifiersRewriter::mkForall( std::vector< Node >& args, Node body, std::vector< Node >& iplc, bool marked ) {
-  if( args.empty() ){
+Node QuantifiersRewriter::mkForall(const std::vector<Node>& args,
+                                   Node body,
+                                   std::vector<Node>& iplc,
+                                   bool marked)
+{
+  if (args.empty())
+  {
     return body;
-  }else{
-    std::vector< Node > children;
-    children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
-    children.push_back( body );
-    if( marked ){
-      Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() );
-      QuantIdNumAttribute ida;
-      avar.setAttribute(ida,0);
-      iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) );
-    }
-    if( !iplc.empty() ){
-      children.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) );
-    }
-    return NodeManager::currentNM()->mkNode( FORALL, children );
   }
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<Node> children;
+  children.push_back(nm->mkNode(kind::BOUND_VAR_LIST, args));
+  children.push_back(body);
+  if (marked)
+  {
+    Node avar = nm->mkSkolem("id", nm->booleanType());
+    QuantIdNumAttribute ida;
+    avar.setAttribute(ida, 0);
+    iplc.push_back(nm->mkNode(kind::INST_ATTRIBUTE, avar));
+  }
+  if (!iplc.empty())
+  {
+    children.push_back(nm->mkNode(kind::INST_PATTERN_LIST, iplc));
+  }
+  return nm->mkNode(kind::FORALL, children);
 }
 
 //computes miniscoping, also eliminates variables that do not occur free in body
@@ -1865,9 +1882,10 @@ Node QuantifiersRewriter::computeOperation(Node f,
     }
     else
     {
-      std::vector< Node > nargs;
-      n = computePrenex(f, n, args, nargs, true, false);
-      Assert(nargs.empty());
+      std::unordered_set<Node, NodeHashFunction> argsSet, nargsSet;
+      n = computePrenex(f, n, argsSet, nargsSet, true, false);
+      Assert(nargsSet.empty());
+      args.insert(args.end(), argsSet.begin(), argsSet.end());
     }
   }
   else if (computeOption == COMPUTE_VAR_ELIMINATION)
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 1ceab7fc0..93f2c5dba 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -248,8 +248,8 @@ class QuantifiersRewriter : public TheoryRewriter
    */
   static Node computePrenex(Node q,
                             Node body,
-                            std::vector<Node>& args,
-                            std::vector<Node>& nargs,
+                            std::unordered_set<Node, NodeHashFunction>& args,
+                            std::unordered_set<Node, NodeHashFunction>& nargs,
                             bool pol,
                             bool prenexAgg);
   /**
@@ -289,9 +289,16 @@ public:
    * The result is wrapped in a trust node of kind TrustNodeKind::REWRITE.
    */
   static TrustNode preprocess(Node n, bool isInst = false);
-  static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
-  static Node mkForall( std::vector< Node >& args, Node body, bool marked = false );
-  static Node mkForall( std::vector< Node >& args, Node body, std::vector< Node >& iplc, bool marked = false );
+  static Node mkForAll(const std::vector<Node>& args,
+                       Node body,
+                       QAttributes& qa);
+  static Node mkForall(const std::vector<Node>& args,
+                       Node body,
+                       bool marked = false);
+  static Node mkForall(const std::vector<Node>& args,
+                       Node body,
+                       std::vector<Node>& iplc,
+                       bool marked = false);
 }; /* class QuantifiersRewriter */
 
 }/* CVC4::theory::quantifiers namespace */
@@ -299,5 +306,3 @@ public:
 }/* CVC4 namespace */
 
 #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */
-
-