From: Andrew Reynolds Date: Mon, 23 Aug 2021 22:15:41 +0000 (-0500) Subject: Fix non-deterministism in quantified datatypes expansion rewrite (#7036) X-Git-Tag: cvc5-1.0.0~1345 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c04c18994e3272a6b59df4272c6d1b7c791f8802;p=cvc5.git Fix non-deterministism in quantified datatypes expansion rewrite (#7036) Required for properly checking proofs for quantifiers rewrites. --- diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 646a4e485..6d8570287 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -32,6 +32,7 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" +#include "util/rational.h" using namespace std; using namespace cvc5::kind; @@ -50,7 +51,11 @@ namespace quantifiers { * - QRewMiniscopeAttribute: cached on (v, q, i) where q is being miniscoped * for F_i in its body (and F_1 ... F_n), and v is one of the bound variables * that q binds. - * - QRewDtExpandAttribute: cached on + * - QRewDtExpandAttribute: cached on (F, lit, a) where lit is the tested + * literal used for expanding a quantified datatype variable in quantified + * 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. */ struct QRewPrenexAttributeId { @@ -644,7 +649,7 @@ Node QuantifiersRewriter::computeCondSplit(Node body, std::vector tmpArgs = args; for (unsigned j = 0, bsize = b.getNumChildren(); j < bsize; j++) { - if (getVarElimLit(b[j], false, tmpArgs, vars, subs)) + if (getVarElimLit(body, b[j], false, tmpArgs, vars, subs)) { Trace("cond-var-split-debug") << "Variable elimination in child #" << j << " under " << i << std::endl; @@ -855,7 +860,8 @@ Node QuantifiersRewriter::getVarElimEqString(Node lit, return Node::null(); } -bool QuantifiersRewriter::getVarElimLit(Node lit, +bool QuantifiersRewriter::getVarElimLit(Node body, + Node lit, bool pol, std::vector& args, std::vector& vars, @@ -887,10 +893,13 @@ bool QuantifiersRewriter::getVarElimLit(Node lit, std::vector newChildren; newChildren.push_back(c.getConstructor()); std::vector newVars; + BoundVarManager* bvm = nm->getBoundVarManager(); for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++) { TypeNode tn = c[j].getRangeType(); - Node v = nm->mkBoundVar(tn); + Node rn = nm->mkConst(Rational(j)); + Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn); + Node v = bvm->mkBoundVar(cacheVal, tn); newChildren.push_back(v); newVars.push_back(v); } @@ -980,11 +989,20 @@ bool QuantifiersRewriter::getVarElimLit(Node lit, return false; } -bool QuantifiersRewriter::getVarElim(Node n, - bool pol, +bool QuantifiersRewriter::getVarElim(Node body, std::vector& args, std::vector& vars, std::vector& subs) +{ + return getVarElimInternal(body, body, false, args, vars, subs); +} + +bool QuantifiersRewriter::getVarElimInternal(Node body, + Node n, + bool pol, + std::vector& args, + std::vector& vars, + std::vector& subs) { Kind nk = n.getKind(); if (nk == NOT) @@ -998,21 +1016,21 @@ bool QuantifiersRewriter::getVarElim(Node n, { for (const Node& cn : n) { - if (getVarElim(cn, pol, args, vars, subs)) + if (getVarElimInternal(body, cn, pol, args, vars, subs)) { return true; } } return false; } - return getVarElimLit(n, pol, args, vars, subs); + return getVarElimLit(body, n, pol, args, vars, subs); } bool QuantifiersRewriter::hasVarElim(Node n, bool pol, std::vector& args) { std::vector< Node > vars; std::vector< Node > subs; - return getVarElim(n, pol, args, vars, subs); + return getVarElimInternal(n, n, pol, args, vars, subs); } bool QuantifiersRewriter::getVarElimIneq(Node body, @@ -1264,7 +1282,7 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& // standard variable elimination if (options::varElimQuant()) { - getVarElim(body, false, args, vars, subs); + getVarElim(body, args, vars, subs); } // variable elimination based on one-direction inequalities if (vars.empty() && options::varIneqElimQuant()) diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index f0c3b0414..a7f107573 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -70,12 +70,13 @@ class QuantifiersRewriter : public TheoryRewriter static bool isVarElim(Node v, Node s); /** get variable elimination literal * - * If n asserted with polarity pol is equivalent to an equality of the form - * v = s for some v in args, where isVariableElim( v, s ) holds, then this - * method removes v from args, adds v to vars, adds s to subs, and returns - * true. Otherwise, it returns false. + * If n asserted with polarity pol in body, and is equivalent to an equality + * of the form v = s for some v in args, where isVariableElim( v, s ) holds, + * then this method removes v from args, adds v to vars, adds s to subs, and + * returns true. Otherwise, it returns false. */ - static bool getVarElimLit(Node n, + static bool getVarElimLit(Node body, + Node n, bool pol, std::vector& args, std::vector& vars, @@ -110,12 +111,12 @@ class QuantifiersRewriter : public TheoryRewriter Node& var); /** get variable elimination * - * If n asserted with polarity pol entails a literal lit that corresponds - * to a variable elimination for some v via the above method, we return true. - * In this case, we update args/vars/subs based on eliminating v. + * If there exists an n with some polarity in body, and entails a literal that + * corresponds to a variable elimination for some v via the above method + * getVarElimLit, we return true. In this case, we update args/vars/subs + * based on eliminating v. */ - static bool getVarElim(Node n, - bool pol, + static bool getVarElim(Node body, std::vector& args, std::vector& vars, std::vector& subs); @@ -145,6 +146,15 @@ class QuantifiersRewriter : public TheoryRewriter QAttributes& qa); //-------------------------------------end variable elimination utilities private: + /** + * Helper method for getVarElim, called when n has polarity pol in body. + */ + static bool getVarElimInternal(Node body, + Node n, + bool pol, + std::vector& args, + std::vector& vars, + std::vector& subs); static int getPurifyIdLit2(Node n, std::map& visited); static bool addCheckElimChild(std::vector& children, Node c, diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index f96e1e579..99a5126aa 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -505,7 +505,7 @@ bool CegSingleInv::solveTrivial(Node q) std::vector varsTmp; std::vector subsTmp; - QuantifiersRewriter::getVarElim(body, false, args, varsTmp, subsTmp); + QuantifiersRewriter::getVarElim(body, args, varsTmp, subsTmp); // if we eliminated a variable, update body and reprocess if (!varsTmp.empty()) {