[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 

6 files changed, 117 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 */
-
-
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ddf810b0c..1e4f42ffd 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -847,6 +847,7 @@ set(regress_0_tests
   regress0/quantifiers/issue4437-unc-quant.smt2
   regress0/quantifiers/issue4576.smt2
   regress0/quantifiers/issue5645-dt-cm-spurious.smt2
+  regress0/quantifiers/issue5693-prenex.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macros-int-real.smt2
   regress0/quantifiers/macros-real-arg.smt2
@@ -1784,6 +1785,7 @@ set(regress_1_tests
   regress1/quantifiers/nra-interleave-inst.smt2
   regress1/quantifiers/opisavailable-12.smt2
   regress1/quantifiers/parametric-lists.smt2
+  regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2
   regress1/quantifiers/psyco-001-bv.smt2
   regress1/quantifiers/psyco-107-bv.smt2
   regress1/quantifiers/psyco-196.smt2
diff --git a/test/regress/regress0/quantifiers/issue5693-prenex.smt2 b/test/regress/regress0/quantifiers/issue5693-prenex.smt2
new file mode 100644
index 000000000..15ee0e7cf
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue5693-prenex.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --full-saturate-quant -i --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :pre-skolem-quant true)
+(declare-fun v7 () Bool)
+(assert (forall ((q49 Bool) (q55 Bool)) (xor v7 (exists ((q49 Bool)) (xor v7 q49 q49)) v7 (= q55 q49))))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 b/test/regress/regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2
new file mode 100644
index 000000000..f0a4560d1
--- /dev/null
+++ b/test/regress/regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2
@@ -0,0 +1,19 @@
+(set-info :smt-lib-version 2.6)
+(set-logic LRA)
+(set-info :source |
+   Scholl, Christoph; Disch, Stefan; Pigorsch, Florian and Kupferschmid,
+   Stefan; Using an SMT Solver and Craig Interpolation to Detect and Remove
+   Redundant Linear Constraints in Representations of Non-Convex Polyhedra.
+   Proceedings of 6th International Workshop on Satisfiability Modulo
+   Theories, Princeton, USA, July 2008.
+   <http://abs.informatik.uni-freiburg.de/smtbench/>
+|)
+(set-info :category "random")
+(set-info :status unsat)
+(declare-fun x1 () Real)
+(declare-fun x2 () Real)
+(declare-fun x3 () Real)
+(declare-fun x4 () Real)
+(assert (forall ((?x1 Real)) (exists ((?x2 Real)) (forall ((?x3 Real)) (exists ((?x4 Real)) (or (and (and (and (>= (+ (+ (* (- 54) ?x1) (* 62 ?x3)) (* (- 53) ?x4)) 79) (not (= (+ (+ (* (- 49) ?x1) (* 25 ?x2)) (* 51 ?x3)) 12))) (or (< (+ (+ (* 5 ?x1) (* 20 ?x2)) (* (- 1) ?x3)) 0) (not (= (+ (+ (* 58 ?x1) (* 61 ?x2)) (* 74 ?x3)) (- 18))))) (or (and (>= (+ (+ (* 48 ?x1) (* (- 47) ?x2)) (* 1 ?x4)) 61) (>= (+ (+ (* (- 19) ?x1) (* (- 80) ?x2)) (* (- 66) ?x3)) 25)) (and (<= (+ (+ (* (- 63) ?x2) (* (- 98) ?x3)) (* (- 4) ?x4)) (- 28)) (not (= (+ (+ (+ (* 10 ?x1) (* 47 ?x2)) (* 77 ?x3)) (* 73 ?x4)) 72))))) (and (or (or (= (+ (+ (* 40 ?x1) (* 16 ?x3)) (* 33 ?x4)) 0) (not (= (+ (+ (* 94 ?x2) (* (- 32) ?x3)) (* (- 19) ?x4)) (- 6)))) (or (not (= (+ (+ (+ (* (- 8) ?x1) (* (- 45) ?x2)) (* 34 ?x3)) (* 11 ?x4)) 57)) (> (+ (* (- 7) ?x2) (* (- 17) ?x3)) 0))) (and (< (+ (+ (+ (* 51 ?x1) (* 5 ?x2)) (* (- 86) ?x3)) (* (- 33) ?x4)) (- 32)) (and (>= (+ (* 50 ?x1) (* (- 46) ?x4)) 37) (not (= (+ (* (- 95) ?x2) (* (- 96) ?x4)) (- 24))))))))))))
+(check-sat)
+(exit)