From 7867526e7070de52db36b1a2988d31ebadecf8b0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 11 Nov 2021 15:39:37 -0600 Subject: [PATCH] Generalize front-end checks to check for shadowed variables (#7634) When using the API, we currently check for free variables in assertions and in terms passed to get-value. We also require checking for variable shadowing. This generalizes the utility method so that both free variables and shadowed variables are checked and reported to the user. --- src/api/cpp/cvc5.cpp | 12 ++- src/expr/node_algorithm.cpp | 194 ++++++++++++++++++++++++------------ src/expr/node_algorithm.h | 28 ++++-- src/smt/assertions.cpp | 9 +- 4 files changed, 165 insertions(+), 78 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 4dcfb466e..7976c19ef 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -4694,6 +4694,7 @@ void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, bool Grammar::containsFreeVariables(const Term& rule) const { + // we allow the argument list and non-terminal symbols to be in scope std::unordered_set scope; for (const Term& sygusVar : d_sygusVars) @@ -4706,8 +4707,7 @@ bool Grammar::containsFreeVariables(const Term& rule) const scope.emplace(*ntsymbol.d_node); } - std::unordered_set fvs; - return expr::getFreeVariablesScope(*rule.d_node, fvs, scope, false); + return expr::hasFreeVariablesScope(*rule.d_node, scope); } std::ostream& operator<<(std::ostream& out, const Grammar& grammar) @@ -5079,8 +5079,12 @@ Term Solver::mkBVFromStrHelper(uint32_t size, Term Solver::getValueHelper(const Term& term) const { // Note: Term is checked in the caller to avoid double checks - CVC5_API_RECOVERABLE_CHECK(!expr::hasFreeVar(term.getNode())) - << "Cannot get value of term containing free variables"; + bool wasShadow = false; + bool freeOrShadowedVar = + expr::hasFreeOrShadowedVar(term.getNode(), wasShadow); + CVC5_API_RECOVERABLE_CHECK(!freeOrShadowedVar) + << "Cannot get value of term containing " + << (wasShadow ? "shadowed" : "free") << " variables"; //////// all checks before this line Node value = d_slv->getValue(*term.d_node); Term res = Term(this, value); diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 13265db71..badf0b75a 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -281,64 +281,32 @@ bool hasBoundVar(TNode n) return n.getAttribute(HasBoundVarAttr()); } -bool hasFreeVar(TNode n) -{ - // optimization for variables and constants - if (n.getNumChildren() == 0) - { - return n.getKind() == kind::BOUND_VARIABLE; - } - std::unordered_set fvs; - return getFreeVariables(n, fvs, false); -} - -struct HasClosureTag -{ -}; -struct HasClosureComputedTag -{ -}; -/** Attribute true for expressions with closures in them */ -typedef expr::Attribute HasClosureAttr; -typedef expr::Attribute HasClosureComputedAttr; - -bool hasClosure(Node n) -{ - if (!n.getAttribute(HasClosureComputedAttr())) - { - bool hasC = false; - if (n.isClosure()) - { - hasC = true; - } - else - { - for (auto i = n.begin(); i != n.end() && !hasC; ++i) - { - hasC = hasClosure(*i); - } - } - if (!hasC && n.hasOperator()) - { - hasC = hasClosure(n.getOperator()); - } - n.setAttribute(HasClosureAttr(), hasC); - n.setAttribute(HasClosureComputedAttr(), true); - return hasC; - } - return n.getAttribute(HasClosureAttr()); -} - -bool getFreeVariables(TNode n, std::unordered_set& fvs, bool computeFv) -{ - std::unordered_set scope; - return getFreeVariablesScope(n, fvs, scope, computeFv); -} - -bool getFreeVariablesScope(TNode n, - std::unordered_set& fvs, - std::unordered_set& scope, - bool computeFv) +/** + * Check variables internal, which is used as a helper to implement many of the + * methods in this file. + * + * This computes the free variables in n, that is, the subterms of n of kind + * BOUND_VARIABLE that are not bound in n or occur in scope, adds these to fvs + * if computeFv is true. + * + * @param n The node under investigation + * @param fvs The set which free variables are added to + * @param scope The scope we are considering. + * @param wasShadow Flag set to true if variable shadowing was encountered. + * Only computed if checkShadow is true. + * @param computeFv If this flag is false, then we only return true/false and + * do not add to fvs. + * @param checkShadow If this flag is true, we immediately return true if a + * variable is shadowing. If this flag is false, we give an assertion failure + * when this occurs. + * @return true iff this node contains a free variable. + */ +bool checkVariablesInternal(TNode n, + std::unordered_set& fvs, + std::unordered_set& scope, + bool& wasShadow, + bool computeFv = true, + bool checkShadow = false) { std::unordered_set visited; std::vector visit; @@ -376,13 +344,26 @@ bool getFreeVariablesScope(TNode n, // add to scope for (const TNode& cn : cur[0]) { - // should not shadow - Assert(scope.find(cn) == scope.end()) - << "Shadowed variable " << cn << " in " << cur << "\n"; + if (checkShadow) + { + if (scope.find(cn) != scope.end()) + { + wasShadow = true; + return true; + } + } + else + { + // should not shadow + Assert(scope.find(cn) == scope.end()) + << "Shadowed variable " << cn << " in " << cur << "\n"; + } scope.insert(cn); } // must make recursive call to use separate cache - if (getFreeVariablesScope(cur[1], fvs, scope, computeFv) && !computeFv) + if (checkVariablesInternal( + cur[1], fvs, scope, wasShadow, computeFv, checkShadow) + && !computeFv) { return true; } @@ -406,6 +387,95 @@ bool getFreeVariablesScope(TNode n, return !fvs.empty(); } +/** Same as above, without checking for shadowing */ +bool getVariablesInternal(TNode n, + std::unordered_set& fvs, + std::unordered_set& scope, + bool computeFv = true) +{ + bool wasShadow = false; + return checkVariablesInternal(n, fvs, scope, wasShadow, computeFv, false); +} + +bool hasFreeVar(TNode n) +{ + // optimization for variables and constants + if (n.getNumChildren() == 0) + { + return n.getKind() == kind::BOUND_VARIABLE; + } + std::unordered_set fvs; + std::unordered_set scope; + return getVariablesInternal(n, fvs, scope, false); +} + +bool hasFreeOrShadowedVar(TNode n, bool& wasShadow) +{ + // optimization for variables and constants + if (n.getNumChildren() == 0) + { + return n.getKind() == kind::BOUND_VARIABLE; + } + std::unordered_set fvs; + std::unordered_set scope; + return checkVariablesInternal(n, fvs, scope, wasShadow, false, true); +} + +struct HasClosureTag +{ +}; +struct HasClosureComputedTag +{ +}; +/** Attribute true for expressions with closures in them */ +typedef expr::Attribute HasClosureAttr; +typedef expr::Attribute HasClosureComputedAttr; + +bool hasClosure(Node n) +{ + if (!n.getAttribute(HasClosureComputedAttr())) + { + bool hasC = false; + if (n.isClosure()) + { + hasC = true; + } + else + { + for (auto i = n.begin(); i != n.end() && !hasC; ++i) + { + hasC = hasClosure(*i); + } + } + if (!hasC && n.hasOperator()) + { + hasC = hasClosure(n.getOperator()); + } + n.setAttribute(HasClosureAttr(), hasC); + n.setAttribute(HasClosureComputedAttr(), true); + return hasC; + } + return n.getAttribute(HasClosureAttr()); +} + +bool getFreeVariables(TNode n, std::unordered_set& fvs) +{ + std::unordered_set scope; + return getVariablesInternal(n, fvs, scope); +} + +bool getFreeVariablesScope(TNode n, + std::unordered_set& fvs, + std::unordered_set& scope) +{ + return getVariablesInternal(n, fvs, scope); +} +bool hasFreeVariablesScope(TNode n, std::unordered_set& scope) +{ + std::unordered_set fvs; + return getVariablesInternal(n, fvs, scope, false); +} + bool getVariables(TNode n, std::unordered_set& vs) { std::unordered_set visited; diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 72ea03176..c3ee4b604 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -84,6 +84,16 @@ bool hasBoundVar(TNode n); */ bool hasFreeVar(TNode n); +/** + * Returns true iff the node n contains a free variable, that is, a node + * of kind BOUND_VARIABLE that is not bound in n, or a BOUND_VARIABLE that + * is shadowed (e.g. it is bound twice in the same context). + * @param n The node under investigation + * @param wasShadow Set to true if n had a shadowed variable. + * @return true iff this node contains a free or shadowed variable. + */ +bool hasFreeOrShadowedVar(TNode n, bool& wasShadow); + /** * Returns true iff the node n contains a closure, that is, a node * whose kind is FORALL, EXISTS, WITNESS, LAMBDA, or any other closure currently @@ -98,27 +108,27 @@ bool hasClosure(Node n); * BOUND_VARIABLE that are not bound in n, adds these to fvs. * @param n The node under investigation * @param fvs The set which free variables are added to - * @param computeFv If this flag is false, then we only return true/false and - * do not add to fvs. * @return true iff this node contains a free variable. */ -bool getFreeVariables(TNode n, - std::unordered_set& fvs, - bool computeFv = true); +bool getFreeVariables(TNode n, std::unordered_set& fvs); /** * Get the free variables in n, that is, the subterms of n of kind * BOUND_VARIABLE that are not bound in n or occur in scope, adds these to fvs. * @param n The node under investigation * @param fvs The set which free variables are added to * @param scope The scope we are considering. - * @param computeFv If this flag is false, then we only return true/false and - * do not add to fvs. * @return true iff this node contains a free variable. */ bool getFreeVariablesScope(TNode n, std::unordered_set& fvs, - std::unordered_set& scope, - bool computeFv = true); + std::unordered_set& scope); +/** + * Return true if n has any free variables in the given scope. + * @param n The node under investigation + * @param scope The scope we are considering. + * @return true iff this node contains a free variable. + */ +bool hasFreeVariablesScope(TNode n, std::unordered_set& scope); /** * Get all variables in n. diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 9c24dd690..8d066c1ba 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -190,16 +190,19 @@ void Assertions::addFormula(TNode n, // Ensure that it does not contain free variables if (maybeHasFv) { - if (expr::hasFreeVar(n)) + bool wasShadow = false; + if (expr::hasFreeOrShadowedVar(n, wasShadow)) { + std::string varType(wasShadow ? "shadowed" : "free"); std::stringstream se; if (isFunDef) { - se << "Cannot process function definition with free variable."; + se << "Cannot process function definition with " << varType + << " variable."; } else { - se << "Cannot process assertion with free variable."; + se << "Cannot process assertion with " << varType << " variable."; if (language::isLangSygus(options().base.inputLanguage)) { // Common misuse of SyGuS is to use top-level assert instead of -- 2.30.2