From 6ddfbe07e3f855c712d86f832c1065cb082bfd1a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 8 Mar 2022 01:12:23 -0600 Subject: [PATCH] Eliminate shadowing in the quantifiers rewriter (#8244) Fixes #8227. Recently, we allowed unevaluatable terms to be in the range of substitutions solved during preprocess. In very rare cases, it may be the case that a quantified formula is substituted into itself, e.g.: forall x. P(x, b) where b was solved to be forall x. P(x, c) This leads to forall x. P(x, forall x. P(x, c)) where x is shadowed. To resolve this issue, we eliminate shadowing in the quantifiers rewriter, e.g. we rewrite the above to forall x. P(x, forall y. P(y, c)). An alternative solution would be to ensure we use capture avoiding substitutions, but this severely complicates our usage of substitutions throughout the preprocessor / proof system. This PR also eliminates some dead code in the quantifiers rewriter. --- src/preprocessing/passes/non_clausal_simp.cpp | 2 +- .../quantifiers/quantifiers_rewriter.cpp | 110 +++++++++++------- src/theory/quantifiers/quantifiers_rewriter.h | 42 ++++--- test/regress/CMakeLists.txt | 1 + .../quantifiers/issue8227-subs-shadow.smt2 | 8 ++ 5 files changed, 104 insertions(+), 59 deletions(-) create mode 100644 test/regress/regress0/quantifiers/issue8227-subs-shadow.smt2 diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 8474cef6a..4af8d7ffd 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -293,8 +293,8 @@ PreprocessingPassResult NonClausalSimp::applyInternal( for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { Node assertion = (*assertionsToPreprocess)[i]; - TrustNode assertionNew = newSubstitutions->applyTrusted(assertion, rw); Trace("non-clausal-simplify") << "assertion = " << assertion << std::endl; + TrustNode assertionNew = newSubstitutions->applyTrusted(assertion, rw); if (!assertionNew.isNull()) { Trace("non-clausal-simplify") diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 4b98f8337..4f20ec67f 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -57,19 +57,28 @@ namespace quantifiers { * formula with body F, and a is the rational corresponding to the argument * position of the variable, e.g. lit is ((_ is C) x) and x is * replaced by (C y1 ... yn), where the argument position of yi is i. + * - QElimShadowAttribute: cached on (q, q', v), which is used to replace a + * shadowed variable v, which is quantified by a subformula q' of quantified + * formula q. Shadowed variables may be introduced when e.g. quantified formulas + * appear on the right hand sides of substitutions in preprocessing. They are + * eliminated by the rewriter. */ struct QRewPrenexAttributeId { }; -typedef expr::Attribute QRewPrenexAttribute; +using QRewPrenexAttribute = expr::Attribute; struct QRewMiniscopeAttributeId { }; -typedef expr::Attribute QRewMiniscopeAttribute; +using QRewMiniscopeAttribute = expr::Attribute; struct QRewDtExpandAttributeId { }; -typedef expr::Attribute QRewDtExpandAttribute; +using QRewDtExpandAttribute = expr::Attribute; +struct QElimShadowAttributeId +{ +}; +using QElimShadowAttribute = expr::Attribute; std::ostream& operator<<(std::ostream& out, RewriteStep s) { @@ -505,37 +514,34 @@ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node } } -Node QuantifiersRewriter::computeProcessTerms(Node body, - std::vector& new_vars, - std::vector& new_conds, - Node q, +Node QuantifiersRewriter::computeProcessTerms(const Node& q, + const std::vector& args, + Node body, QAttributes& qa) const { - std::map< Node, Node > cache; - if( qa.isFunDef() ){ - Node h = QuantAttributes::getFunDefHead( q ); - Assert(!h.isNull()); - // if it is a function definition, rewrite the body independently - Node fbody = QuantAttributes::getFunDefBody( q ); - Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl; - if (!fbody.isNull()) - { - Node r = computeProcessTerms2(fbody, cache, new_vars, new_conds); - Assert(new_vars.size() == h.getNumChildren()); - return NodeManager::currentNM()->mkNode(EQUAL, h, r); - } - // It can happen that we can't infer the shape of the function definition, - // for example: forall xy. f( x, y ) = 1 + f( x, y ), this is rewritten to - // forall xy. false. + options::IteLiftQuantMode iteLiftMode = options::IteLiftQuantMode::NONE; + if (qa.isStandard()) + { + iteLiftMode = d_opts.quantifiers.iteLiftQuant; } - return computeProcessTerms2(body, cache, new_vars, new_conds); + std::vector new_conds; + std::map cache; + Node n = computeProcessTerms2(q, args, body, cache, new_conds, iteLiftMode); + if (!new_conds.empty()) + { + new_conds.push_back(n); + n = NodeManager::currentNM()->mkNode(OR, new_conds); + } + return n; } Node QuantifiersRewriter::computeProcessTerms2( + const Node& q, + const std::vector& args, Node body, std::map& cache, - std::vector& new_vars, - std::vector& new_conds) const + std::vector& new_conds, + options::IteLiftQuantMode iteLiftMode) const { NodeManager* nm = NodeManager::currentNM(); Trace("quantifiers-rewrite-term-debug2") @@ -544,14 +550,43 @@ Node QuantifiersRewriter::computeProcessTerms2( if( iti!=cache.end() ){ return iti->second; } + if (body.isClosure()) + { + // Ensure no shadowing. If this term is a closure quantifying a variable + // in args, then we introduce fresh variable(s) and replace this closure + // to be over the fresh variables instead. + std::vector oldVars; + std::vector newVars; + for (const Node& v : body[0]) + { + if (std::find(args.begin(), args.end(), v) != args.end()) + { + Trace("quantifiers-rewrite-unshadow") + << "Found shadowed variable " << v << " in " << q << std::endl; + BoundVarManager* bvm = nm->getBoundVarManager(); + oldVars.push_back(v); + Node cacheVal = BoundVarManager::getCacheValue(q, body, v); + Node nv = bvm->mkBoundVar(cacheVal, v.getType()); + newVars.push_back(nv); + } + } + if (!oldVars.empty()) + { + Assert(oldVars.size() == newVars.size()); + Node sbody = body.substitute( + oldVars.begin(), oldVars.end(), newVars.begin(), newVars.end()); + cache[body] = sbody; + return sbody; + } + } bool changed = false; std::vector children; - for (size_t i = 0; i < body.getNumChildren(); i++) + for (const Node& bc : body) { // do the recursive call on children - Node nn = computeProcessTerms2(body[i], cache, new_vars, new_conds); + Node nn = computeProcessTerms2(q, args, bc, cache, new_conds, iteLiftMode); children.push_back(nn); - changed = changed || nn != body[i]; + changed = changed || nn != bc; } // make return value @@ -572,8 +607,7 @@ Node QuantifiersRewriter::computeProcessTerms2( Trace("quantifiers-rewrite-term-debug2") << "Returning " << ret << " for " << body << std::endl; // do context-independent rewriting - if (ret.getKind() == EQUAL - && d_opts.quantifiers.iteLiftQuant != options::IteLiftQuantMode::NONE) + if (ret.getKind() == EQUAL && iteLiftMode != options::IteLiftQuantMode::NONE) { for (size_t i = 0; i < 2; i++) { @@ -582,8 +616,7 @@ Node QuantifiersRewriter::computeProcessTerms2( Node no = i == 0 ? ret[1] : ret[0]; if (no.getKind() != ITE) { - bool doRewrite = - d_opts.quantifiers.iteLiftQuant == options::IteLiftQuantMode::ALL; + bool doRewrite = (iteLiftMode == options::IteLiftQuantMode::ALL); std::vector childrenIte; childrenIte.push_back(ret[i][0]); for (size_t j = 1; j <= 2; j++) @@ -1922,9 +1955,7 @@ bool QuantifiersRewriter::doOperation(Node q, } else if (computeOption == COMPUTE_PROCESS_TERMS) { - return is_std - && d_opts.quantifiers.iteLiftQuant - != options::IteLiftQuantMode::NONE; + return true; } else if (computeOption == COMPUTE_COND_SPLIT) { @@ -1981,12 +2012,7 @@ Node QuantifiersRewriter::computeOperation(Node f, } else if (computeOption == COMPUTE_PROCESS_TERMS) { - std::vector< Node > new_conds; - n = computeProcessTerms( n, args, new_conds, f, qa ); - if( !new_conds.empty() ){ - new_conds.push_back( n ); - n = NodeManager::currentNM()->mkNode( OR, new_conds ); - } + n = computeProcessTerms(f, args, n, qa); } else if (computeOption == COMPUTE_COND_SPLIT) { diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index b3e9ec8c2..1aabfe3c3 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -18,6 +18,7 @@ #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H +#include "options/quantifiers_options.h" #include "proof/trust_node.h" #include "theory/theory_rewriter.h" @@ -233,10 +234,26 @@ class QuantifiersRewriter : public TheoryRewriter std::vector& activeArgs, Node n, Node ipl); - Node computeProcessTerms2(Node body, + /** + * It may introduce new conditions C into new_conds. It returns a node retBody + * such that q of the form + * forall args. body + * is equivalent to: + * forall args. ( C V retBody ) + * + * @param q The original quantified formula we are processing + * @param args The bound variables of q + * @param body The subformula of the body of q we are processing + * @param cache Cache from terms to their processed form + * @param new_conds New conditions to add as disjunctions to the return + * @param iteLiftMode The mode for lifting ITEs from body. + */ + Node computeProcessTerms2(const Node& q, + const std::vector& args, + Node body, std::map& cache, - std::vector& new_vars, - std::vector& new_conds) const; + std::vector& new_conds, + options::IteLiftQuantMode iteLiftMode) const; static void computeDtTesterIteSplit( Node n, std::map& pcons, @@ -276,24 +293,17 @@ class QuantifiersRewriter : public TheoryRewriter /** compute process terms * * This takes as input a quantified formula q with attributes qa whose - * body is body. + * bound variables are args, and whose body is body. * * This rewrite eliminates problematic terms from the bodies of * quantified formulas, which includes performing: * - Certain cases of ITE lifting, - * - Elimination of extended arithmetic functions like to_int/is_int/div/mod, - * - Elimination of select over store. - * - * It may introduce new variables V into new_vars and new conditions C into - * new_conds. It returns a node retBody such that q of the form - * forall X. body - * is equivalent to: - * forall X, V. ( C => retBody ) + * - Elimination of select over store, + * - Elimination of shadowed variables. */ - Node computeProcessTerms(Node body, - std::vector& new_vars, - std::vector& new_conds, - Node q, + Node computeProcessTerms(const Node& q, + const std::vector& args, + Node body, QAttributes& qa) const; //------------------------------------- end process terms //------------------------------------- extended rewrite diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f659c200f..2a6add5b2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1030,6 +1030,7 @@ set(regress_0_tests regress0/quantifiers/issue7353-var-elim-par-dt.smt2 regress0/quantifiers/issue8001-mem-leak.smt2 regress0/quantifiers/issue8159-3-qext-nterm.smt2 + regress0/quantifiers/issue8227-subs-shadow.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macro-back-subs-sat.smt2 regress0/quantifiers/macros-int-real.smt2 diff --git a/test/regress/regress0/quantifiers/issue8227-subs-shadow.smt2 b/test/regress/regress0/quantifiers/issue8227-subs-shadow.smt2 new file mode 100644 index 000000000..ffbe0bc88 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue8227-subs-shadow.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun v0 () Bool) +(declare-fun v25 () Bool) +(declare-fun v88 () Bool) +(assert (= v25 (or v0 (not v0)))) +(assert (= v0 (= v88 (forall ((q131 Bool)) (xor v88 q131 q131 v25))))) +(check-sat) -- 2.30.2