From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 19 May 2020 20:38:05 +0000 (-0500)
Subject: Use fresh variables when miniscoping (#4296)
X-Git-Tag: cvc5-1.0.0~3317
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6bb98062a5578d126db6a3e8cdca083881893b32;p=cvc5.git

Use fresh variables when miniscoping (#4296)

Fixes #4288.

When applying miniscoping, we previously were reusing variables across quantified formulas in the resulting conjunction. This ensures our miniscoping ensures fresh variables.
---

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 10c5741fe..df86922bc 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1664,6 +1664,7 @@ Node QuantifiersRewriter::mkForall( std::vector< Node >& args, Node body, std::v
 
 //computes miniscoping, also eliminates variables that do not occur free in body
 Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ){
+  NodeManager* nm = NodeManager::currentNM();
   if( body.getKind()==FORALL ){
     //combine prenex
     std::vector< Node > newArgs;
@@ -1677,10 +1678,36 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo
     // be applied first
     if (options::miniscopeQuant() || options::aggressiveMiniscopeQuant())
     {
-      // break apart
+      // Break apart the quantifed formula
+      // forall x. P1 ^ ... ^ Pn ---> forall x. P1 ^ ... ^ forall x. Pn
       NodeBuilder<> t(kind::AND);
-      for( unsigned i=0; i<body.getNumChildren(); i++ ){
-        t << computeMiniscoping( args, body[i], qa );
+      std::vector<Node> argsc;
+      for (unsigned i = 0, nchild = body.getNumChildren(); i < nchild; i++)
+      {
+        if (argsc.empty())
+        {
+          // If not done so, we must create fresh copy of args. This is to
+          // ensure that quantified formulas do not reuse variables.
+          for (const Node& v : args)
+          {
+            argsc.push_back(nm->mkBoundVar(v.getType()));
+          }
+        }
+        Node b = body[i];
+        Node bodyc =
+            b.substitute(args.begin(), args.end(), argsc.begin(), argsc.end());
+        if (b == bodyc)
+        {
+          // Did not contain variables in args, thus it is ground. Since we did
+          // not use them, we keep the variables argsc for the next child.
+          t << b;
+        }
+        else
+        {
+          t << computeMiniscoping(argsc, bodyc, qa);
+          // We used argsc, clear so we will construct a fresh copy above.
+          argsc.clear();
+        }
       }
       Node retVal = t;
       return retVal;