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.

1 files changed, 13 insertions, 0 deletions

diff --git a/src/printer/let_binding.h b/src/printer/let_binding.h
index e14740b61..83f3183ca 100644
--- 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
 {