Letify quantifier bodies independently (#6112)

This fixes a subtle bug with how quantifier bodies are letified.

It makes our letification more conservative so that let symbols are never pushed inside quantifier bodies, instead quantifier bodies are letified independently of the context.

diff --git a/src/printer/let_binding.cpp b/src/printer/let_binding.cpp
index 9f26d38000c034bd268d1e0b5f325c9c5e07bc1b..ca3ab40f6ecc7c48ff048e819605884a7f5fe2d4 100644 (file)
--- a/src/printer/let_binding.cpp
+++ b/src/printer/let_binding.cpp
@@ -57,7 +57,7 @@ void LetBinding::letify(std::vector<Node>& letList)
   // populate the d_letList and d_letMap
   convertCountToLet();
   // add the new entries to the letList
-letList.insert(letList.end(), d_letList.begin() + prevSize, d_letList.end());
+  letList.insert(letList.end(), d_letList.begin() + prevSize, d_letList.end());
 }
 
 void LetBinding::pushScope() { d_context.push(); }
@@ -103,6 +103,11 @@ Node LetBinding::convert(Node n, const std::string& prefix, bool letTop) const
         ss << prefix << id;
         visited[cur] = nm->mkBoundVar(ss.str(), cur.getType());
       }
+      else if (cur.isClosure())
+      {
+        // do not convert beneath quantifiers
+        visited[cur] = cur;
+      }
       else
       {
         visited[cur] = Node::null();

diff --git a/src/printer/let_binding.h b/src/printer/let_binding.h
index e14740b611919fccbc6919651ef556b7cb34f727..83f3183ca9d38e6fc99e559b6bcf121d68834174 100644 (file)
--- a/src/printer/let_binding.h
+++ b/src/printer/let_binding.h
@@ -69,6 +69,19 @@ namespace CVC4 {
  * d_letList[i] does not contain subterm d_letList[j] for j>i.
  * It is intended that d_letList contains only unique nodes. Each node
  * in d_letList is mapped to a unique identifier in d_letMap.
+ *
+ * Notice that this class will *not* use introduced let symbols when converting
+ * the bodies of quantified formulas. Consider the formula:
+ * (let ((Q (forall ((x Int)) (= x (+ a a))))) (and (= (+ a a) (+ a a)) Q Q))
+ * where "let" above is from the user. When this is letified by this class,
+ * note that (+ a a) occurs as a subterm of Q, however it is not seen until
+ * after we have seen Q twice, since we traverse in reverse topological order.
+ * Since we do not traverse underneath quantified formulas, this means that Q
+ * may be marked as a term-to-letify before (+ a a), which leads to violation
+ * of the above invariant concerning containment. Thus, when converting, if
+ * a let symbol is introduced for (+ a a), we will not replace the occurence
+ * of (+ a a) within Q. Instead, the user of this class is responsible for
+ * letifying the bodies of quantified formulas independently.
  */
 class LetBinding
 {

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 7a27794e6fcd7c5441fee26f43c2c4b78f1641d2..e1a4058e8205553986cf35dfe8e3c92645cff46d 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -931,17 +931,22 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::WITNESS:
   {
     out << smtKindString(k, d_variant) << " ";
-    toStream(out, n[0], toDepth, lbind);
+    // do not letify the bound variable list
+    toStream(out, n[0], toDepth, nullptr);
     out << " ";
     if (n.getNumChildren() == 3)
     {
       out << "(! ";
     }
-    toStreamWithLetify(out, n[1], toDepth - 1, lbind);
+    // Use a fresh let binder, since using existing let symbols may violate
+    // scoping issues for let-bound variables, see explanation in let_binding.h.
+    size_t dag = lbind == nullptr ? 0 : lbind->getThreshold()-1;
+    toStream(out, n[1], toDepth - 1, dag);
     if (n.getNumChildren() == 3)
     {
       out << " ";
-      toStream(out, n[2], toDepth, lbind);
+      // do not letify the annotation
+      toStream(out, n[2], toDepth, nullptr);
       out << ")";
     }
     out << ")";

diff --git a/test/regress/regress0/printer/let_shadowing.smt2 b/test/regress/regress0/printer/let_shadowing.smt2
index 14f2316a7504d740813153dc3360de2d3a91544a..02eb3376aeef671aaed6180e4304e746be98ac86 100644 (file)
--- a/test/regress/regress0/printer/let_shadowing.smt2
+++ b/test/regress/regress0/printer/let_shadowing.smt2
@@ -3,7 +3,7 @@
 ; SCRUBBER: grep assert
 ; EXPECT: (assert (let ((_let_1 (* x y))) (and (= _let_1 _let_1) (= _let_1 _let_0))))
 ; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((_let_0 Int)) (= 0 _let_0))))))
-; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _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)))))))))
+; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((x Int)) (forall ((y Int)) (let ((_let_1 (and b a))) (and (and a b) _let_1 _let_1 (= 0 _let_0)))))))))
 (set-logic NIA)
 (declare-const _let_0 Int)
 (declare-const x Int)