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.

diff --git a/src/expr/bound_var_manager.cpp b/src/expr/bound_var_manager.cpp
index fa7e4305daf997fc507ec77e938cbcd8783842ac..e4b1be6917bd0f6ac63c8c192421a0781552ac8f 100644 (file)
--- a/src/expr/bound_var_manager.cpp
+++ b/src/expr/bound_var_manager.cpp
@@ -37,6 +37,10 @@ Node BoundVarManager::getCacheValue(TNode cv1, TNode cv2)
 {
   return NodeManager::currentNM()->mkNode(kind::SEXPR, cv1, cv2);
 }
+Node BoundVarManager::getCacheValue(TNode cv1, TNode cv2, TNode cv3)
+{
+  return NodeManager::currentNM()->mkNode(kind::SEXPR, cv1, cv2, cv3);
+}
 
 Node BoundVarManager::getCacheValue(TNode cv1, TNode cv2, size_t i)
 {

diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h
index 4c9c0af20f4136cf2c5a2b67b20866fcaac436fb..3330decffec3dca011fc8630355c70aa3470a6c6 100644 (file)
--- a/src/expr/bound_var_manager.h
+++ b/src/expr/bound_var_manager.h
@@ -83,6 +83,8 @@ class BoundVarManager
   //---------------------------------- utilities for computing Node hash
   /** get cache value from two nodes, returns SEXPR */
   static Node getCacheValue(TNode cv1, TNode cv2);
+  /** get cache value from three nodes, returns SEXPR */
+  static Node getCacheValue(TNode cv1, TNode cv2, TNode cv3);
   /** get cache value from two nodes and a size_t, returns SEXPR */
   static Node getCacheValue(TNode cv1, TNode cv2, size_t i);
   /** get cache value, returns a constant rational node */

diff --git a/src/theory/quantifiers/quantifiers_macros.cpp b/src/theory/quantifiers/quantifiers_macros.cpp
index c7d74228fda1d1029b94bdfa5e6dde6d2c578725..43a404ff9c56960cae6fb7f6751bc276942c04f0 100644 (file)
--- 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 77ce91829696628cda23d98b1b9713688e479725..91b44b520689facfecfbc88d59afaaaf8f93fb7b 100644 (file)
--- 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 123ffee7d79d03ff2b412b0952fd0b8cd68b29d7..3df5aa65f394370229248a3318b7cc717422e11b 100644 (file)
--- 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

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 08bdaf6eba64061ffcf7e8d24c5751c8439ba678..f2d017e024ede7c9eb9af4af8b0568623c4b6a19 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1795,6 +1795,7 @@ set(regress_1_tests
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2
   regress1/quantifiers/lra-vts-inf.smt2
+  regress1/quantifiers/macro-geo-small-3.smt2
   regress1/quantifiers/min-ppgt-em-incomplete.smt2
   regress1/quantifiers/min-ppgt-em-incomplete2.smt2
   regress1/quantifiers/mix-coeff.smt2

diff --git a/test/regress/regress1/quantifiers/macro-geo-small-3.smt2 b/test/regress/regress1/quantifiers/macro-geo-small-3.smt2
new file mode 100644 (file)
index 0000000..07a03d4
--- /dev/null
+++ b/test/regress/regress1/quantifiers/macro-geo-small-3.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-sort U 0)
+(declare-fun T (U U) Bool)
+(define-fun P ((x1 U) (y1 U)) Bool (forall ((z1 U)) (or (not (T z1 x1)) (T z1 y1))))
+(define-fun E ((y2 U)) Bool (forall ((z2 U) (w2 U)) (or (not (P z2 y2)) (P z2 w2) (P w2 z2))))
+(assert (forall ((x3 U)) (exists ((y3 U)) (and (T y3 x3) (not (E x3))))))
+; benchmark triggered unsoundness due to reusing a bound variable for prenexing the lifting of P twice within the definition of E
+(check-sat)