From: Andrew Reynolds Date: Tue, 27 Apr 2021 21:25:11 +0000 (-0500) Subject: Fix refutational soundness bug in quantifier prenexing (#6448) X-Git-Tag: cvc5-1.0.0~1822 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d524948b58c4c3f61c623649049f6209b7756ed6;p=cvc5.git 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 fa7e4305d..e4b1be691 100644 --- 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 4c9c0af20..3330decff 100644 --- 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 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(cacheVal, vt); } else diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 08bdaf6eb..f2d017e02 100644 --- 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 index 000000000..07a03d4ce --- /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)