Fix refutational soundness bug in quantifier prenexing (#6448)

This bug can be triggered by define-fun, quantifier macros or inferred substitutions whose RHS contain quantified formulas.

This corrects the issue by ensuring that bound variables introduced for prenexing are fresh for distinct quantified formula subterms that may share quantified variables.

This was reported by Geoff Sutcliffe via a TPTP run.

3 files changed, 24 insertions, 7 deletions

diff --git a/src/theory/quantifiers/quantifiers_macros.cpp b/src/theory/quantifiers/quantifiers_macros.cpp
index c7d74228f..43a404ff9 100644
--- a/src/theory/quantifiers/quantifiers_macros.cpp
+++ b/src/theory/quantifiers/quantifiers_macros.cpp
@@ -41,9 +41,9 @@ Node QuantifiersMacros::solve(Node lit, bool reqGround)
   {
     return Node::null();
   }
-  lit = lit[1];
-  bool pol = lit.getKind() != NOT;
-  Node n = pol ? lit : lit[0];
+  Node body = lit[1];
+  bool pol = body.getKind() != NOT;
+  Node n = pol ? body : body[0];
   NodeManager* nm = NodeManager::currentNM();
   if (n.getKind() == APPLY_UF)
   {
@@ -54,7 +54,7 @@ Node QuantifiersMacros::solve(Node lit, bool reqGround)
       Node n_def = nm->mkConst(pol);
       Node fdef = solveEq(n, n_def);
       Assert(!fdef.isNull());
-      return fdef;
+      return returnMacro(fdef, lit);
     }
   }
   else if (pol && n.getKind() == EQUAL)
@@ -89,14 +89,14 @@ Node QuantifiersMacros::solve(Node lit, bool reqGround)
             << "...does not contain bad (recursive) operator." << std::endl;
         // must be ground UF term if mode is GROUND_UF
         if (options::macrosQuantMode() != options::MacrosQuantMode::GROUND_UF
-            || preservesTriggerVariables(lit, n_def))
+            || preservesTriggerVariables(body, n_def))
         {
           Trace("macros-debug")
               << "...respects ground-uf constraint." << std::endl;
           Node fdef = solveEq(m, n_def);
           if (!fdef.isNull())
           {
-            return fdef;
+            return returnMacro(fdef, lit);
           }
         }
       }
@@ -278,6 +278,13 @@ Node QuantifiersMacros::solveEq(Node n, Node ndef)
   return op.eqNode(fdef);
 }
 
+Node QuantifiersMacros::returnMacro(Node fdef, Node lit) const
+{
+  Trace("macros") << "* Inferred macro " << fdef << " from " << lit
+                  << std::endl;
+  return fdef;
+}
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/quantifiers/quantifiers_macros.h b/src/theory/quantifiers/quantifiers_macros.h
index 77ce91829..91b44b520 100644
--- a/src/theory/quantifiers/quantifiers_macros.h
+++ b/src/theory/quantifiers/quantifiers_macros.h
@@ -87,6 +87,11 @@ class QuantifiersMacros
    * where n is of the form U(x1...xn).
    */
   Node solveEq(Node n, Node ndef);
+  /**
+   * Returns the macro fdef, which originated from lit. This method is for
+   * debugging.
+   */
+  Node returnMacro(Node fdef, Node lit) const;
   /** Reference to the quantifiers registry */
   QuantifiersRegistry& d_qreg;
 };
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 123ffee7d..3df5aa65f 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1267,7 +1267,12 @@ Node QuantifiersRewriter::computePrenex(
         Node vv;
         if (!q.isNull())
         {
-          Node cacheVal = BoundVarManager::getCacheValue(q, v);
+          // We cache based on the original quantified formula, the subformula
+          // that we are pulling variables from (body), and the variable v.
+          // The argument body is required since in rare cases, two subformulas
+          // may share the same variables. This is the case for define-fun
+          // or inferred substitutions that contain quantified formulas.
+          Node cacheVal = BoundVarManager::getCacheValue(q, body, v);
           vv = bvm->mkBoundVar<QRewPrenexAttribute>(cacheVal, vt);
         }
         else