Prevent letification from shadowing variables (#3042)
authorAndres Noetzli <noetzli@stanford.edu>
Wed, 5 Jun 2019 20:01:34 +0000 (13:01 -0700)
committerGitHub <noreply@github.com>
Wed, 5 Jun 2019 20:01:34 +0000 (13:01 -0700)
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.

src/expr/node_algorithm.cpp
src/expr/node_algorithm.h
src/printer/dagification_visitor.cpp
src/printer/dagification_visitor.h
test/regress/CMakeLists.txt
test/regress/regress0/printer/let_shadowing.smt2 [new file with mode: 0644]

index 25ffb077894f0a700dddb7d5878096d68d984ca5..841f9ea28d4fce06ca98ae69604caef1c46e939a 100644 (file)
@@ -236,6 +236,38 @@ bool getFreeVariables(TNode n,
   return !fvs.empty();
 }
 
+bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs)
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    std::unordered_set<TNode, TNodeHashFunction>::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<Node, NodeHashFunction>& syms)
 {
   std::unordered_set<TNode, TNodeHashFunction> visited;
index 656f162ae28c317fb41b2b14af6d52c031918130..727f5ba75d6cc5762301abad2be8c514b3921b3f 100644 (file)
@@ -72,6 +72,14 @@ bool getFreeVariables(TNode n,
                       std::unordered_set<Node, NodeHashFunction>& 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<TNode, TNodeHashFunction>& 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.
index cf5f354572224a304a10b8e1eaf620715075ac8e..a024c97a70b24ecd759ad0b7925081c4c90eb5db 100644 (file)
@@ -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 <sstream>
 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<TNode, TNodeHashFunction> 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
index 18f31e662eb98370bd77cd69e67886f4ee653fe1..6df5f32b4bcb70eef913662e8a32c835dad0a8cd 100644 (file)
@@ -21,6 +21,7 @@
 
 #include <string>
 #include <unordered_map>
+#include <unordered_set>
 #include <vector>
 
 #include "expr/node.h"
@@ -68,6 +69,12 @@ class DagificationVisitor {
    */
   std::unordered_map<TNode, unsigned, TNodeHashFunction> d_nodeCount;
 
+  /**
+   * The set of variable names with the let prefix that appear in the
+   * expression.
+   */
+  std::unordered_set<std::string> d_reservedLetNames;
+
   /**
    * The top-most node we are visiting.
    */
index b63930569a6d8f9518e0d4b6ab36181eb279592b..0a5f0a9726024b32e0cf91262566dcad40509358 100644 (file)
@@ -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 (file)
index 0000000..3251e4e
--- /dev/null
@@ -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)