From: Andres Noetzli Date: Wed, 5 Jun 2019 20:01:34 +0000 (-0700) Subject: Prevent letification from shadowing variables (#3042) X-Git-Tag: cvc5-1.0.0~4122 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6b01e8740111e69219e5d733e1123955f8cd2ea7;p=cvc5.git Prevent letification from shadowing variables (#3042) Fixes #3005. When printing nodes, we introduce `let` expressions on the fly. However, when doing that, we have to be careful that we don't shadow existing variables with the same name. When quantifiers are involved, we do not descend into the quantifiers to avoid letifying terms with bound variables that then go out of scope (see #1863). Thus, to avoid shadowing variables appearing in quantifiers, we have to collect all the variables appearing in that term to make sure that the let does not shadow them. In #3005, the issue was caused by a `let` that was introduced outside of a quantifier and then was shadowed in the body of the quantifier by another `let` introduced for that body. --- diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 25ffb0778..841f9ea28 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -236,6 +236,38 @@ bool getFreeVariables(TNode n, return !fvs.empty(); } +bool getVariables(TNode n, std::unordered_set& vs) +{ + std::unordered_set visited; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + std::unordered_set::iterator itv = + visited.find(cur); + if (itv == visited.end()) + { + if (cur.isVar()) + { + vs.insert(cur); + } + else + { + for (const TNode& cn : cur) + { + visit.push_back(cn); + } + } + visited.insert(cur); + } + } while (!visit.empty()); + + return !vs.empty(); +} + void getSymbols(TNode n, std::unordered_set& syms) { std::unordered_set visited; diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 656f162ae..727f5ba75 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -72,6 +72,14 @@ bool getFreeVariables(TNode n, std::unordered_set& fvs, bool computeFv = true); +/** + * Get all variables in n. + * @param n The node under investigation + * @param vs The set which free variables are added to + * @return true iff this node contains a free variable. + */ +bool getVariables(TNode n, std::unordered_set& vs); + /** * For term n, this function collects the symbols that occur as a subterms * of n. A symbol is a variable that does not have kind BOUND_VARIABLE. diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp index cf5f35457..a024c97a7 100644 --- a/src/printer/dagification_visitor.cpp +++ b/src/printer/dagification_visitor.cpp @@ -17,6 +17,8 @@ #include "printer/dagification_visitor.h" #include "context/context.h" +#include "expr/node_algorithm.h" +#include "expr/node_manager_attributes.h" #include "theory/substitutions.h" #include @@ -24,18 +26,20 @@ namespace CVC4 { namespace printer { -DagificationVisitor::DagificationVisitor(unsigned threshold, std::string letVarPrefix) : - d_threshold(threshold), - d_letVarPrefix(letVarPrefix), - d_nodeCount(), - d_top(), - d_context(new context::Context()), - d_substitutions(new theory::SubstitutionMap(d_context)), - d_letVar(0), - d_done(false), - d_uniqueParent(), - d_substNodes() { - +DagificationVisitor::DagificationVisitor(unsigned threshold, + std::string letVarPrefix) + : d_threshold(threshold), + d_letVarPrefix(letVarPrefix), + d_nodeCount(), + d_reservedLetNames(), + d_top(), + d_context(new context::Context()), + d_substitutions(new theory::SubstitutionMap(d_context)), + d_letVar(0), + d_done(false), + d_uniqueParent(), + d_substNodes() +{ // 0 doesn't make sense AlwaysAssertArgument(threshold > 0, threshold); } @@ -51,8 +55,28 @@ bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) { { // for quantifiers, we visit them but we don't recurse on them visit(current, parent); + + // search for variables that start with the let prefix + std::unordered_set vs; + expr::getVariables(current, vs); + for (const TNode v : vs) + { + const std::string name = v.getAttribute(expr::VarNameAttr()); + if (name.compare(0, d_letVarPrefix.size(), d_letVarPrefix) == 0) + { + d_reservedLetNames.insert(name); + } + } return true; } + else if (current.isVar()) + { + const std::string name = current.getAttribute(expr::VarNameAttr()); + if (name.compare(0, d_letVarPrefix.size(), d_letVarPrefix) == 0) + { + d_reservedLetNames.insert(name); + } + } // don't visit variables, constants, or those exprs that we've // already seen more than the threshold: if we've increased // the count beyond the threshold already, we've done the same @@ -137,7 +161,11 @@ void DagificationVisitor::done(TNode node) { // construct the let binder std::stringstream ss; - ss << d_letVarPrefix << d_letVar++; + do + { + ss.str(""); + ss << d_letVarPrefix << d_letVar++; + } while (d_reservedLetNames.find(ss.str()) != d_reservedLetNames.end()); Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY | NodeManager::SKOLEM_EXACT_NAME); // apply previous substitutions to the rhs, enabling cascading LETs diff --git a/src/printer/dagification_visitor.h b/src/printer/dagification_visitor.h index 18f31e662..6df5f32b4 100644 --- a/src/printer/dagification_visitor.h +++ b/src/printer/dagification_visitor.h @@ -21,6 +21,7 @@ #include #include +#include #include #include "expr/node.h" @@ -68,6 +69,12 @@ class DagificationVisitor { */ std::unordered_map d_nodeCount; + /** + * The set of variable names with the let prefix that appear in the + * expression. + */ + std::unordered_set d_reservedLetNames; + /** * The top-most node we are visiting. */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b63930569..0a5f0a972 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -586,6 +586,7 @@ set(regress_0_tests regress0/printer/bv_consts_bin.smt2 regress0/printer/bv_consts_dec.smt2 regress0/printer/empty_symbol_name.smt2 + regress0/printer/let_shadowing.smt2 regress0/printer/tuples_and_records.cvc regress0/push-pop/boolean/fuzz_12.smt2 regress0/push-pop/boolean/fuzz_13.smt2 diff --git a/test/regress/regress0/printer/let_shadowing.smt2 b/test/regress/regress0/printer/let_shadowing.smt2 new file mode 100644 index 000000000..3251e4e38 --- /dev/null +++ b/test/regress/regress0/printer/let_shadowing.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --dump raw-benchmark --preprocess-only +; SCRUBBER: grep assert +; EXPECT: (assert (let ((_let_1 (* x y))) (= _let_1 _let_1 _let_0))) +; EXPECT: (assert (let ((_let_1 (and a b))) (= _let_1 _let_1 (forall ((_let_0 Int)) (= 0 _let_0) )))) +; EXPECT: (assert (let ((_let_1 (and a b))) (= _let_1 _let_1 (forall ((x Int)) (forall ((y Int)) (let ((_let_2 (and b a))) (and _let_1 _let_2 _let_2 (= 0 _let_0))) ) )))) +(set-logic NIA) +(declare-const _let_0 Int) +(declare-const x Int) +(declare-const y Int) +(declare-const a Bool) +(declare-const b Bool) +(assert (= (* x y) (* x y) _let_0)) +(assert (= (and a b) (and a b) (forall ((_let_0 Int)) (= 0 _let_0)))) +(assert (= (and a b) (and a b) (forall ((x Int)) (forall ((y Int)) (and (and a b) (and b a) (and b a) (= 0 _let_0)))))) +(check-sat)