From 9e7ee41e7c50a972afd6f7210ecf94d798beb235 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 4 Oct 2024 11:35:00 -0500
Subject: [PATCH] Downgrade the required use of fresh-binder to a warning
 (#11256)

This makes us introduce a fresh variable when fresh-binders is false in
the rare case where we have a let-term that induces a capturing
substitution. This happens for inputs like `(forall ((x Int)) (let ((y
x)) (forall ((x Int)) (P y))`.

This behavior was introduced in https://github.com/cvc5/cvc5/pull/11079,
and actually causes several errors to be caught and thrown in SMT-LIB,
which are now warnings after this PR.

As a consequence of this PR, when this warning is thrown:
- Proof reference checking will fail unless this behavior is modelled
upstream in the proof checkers,
- The parser is not deterministic since it resorts to constructing a
fresh variable for the inner quantified formula.

Note that the latter does not really impact applications e.g.
distributed solving which rely on sharing quantified lemmas since the
quantified formulas we share will have resolved issues with variable
shadowing.

---------

Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
---
 src/parser/parser_state.cpp                   | 69 ++++++++++++-------
 .../issue11066-fresh-binders-err.smt2         |  6 +-
 2 files changed, 48 insertions(+), 27 deletions(-)

diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp
index c20c1aa5938..d1322cada31 100644
--- a/src/parser/parser_state.cpp
+++ b/src/parser/parser_state.cpp
@@ -217,40 +217,61 @@ std::vector<Term> ParserState::bindBoundVarsCtx(
   std::vector<Term> vars;
   for (std::pair<std::string, Sort>& i : sortedVarNames)
   {
-    bool wasDecl = isDeclared(i.first);
-    Term v = bindBoundVar(i.first, i.second, fresh);
-    vars.push_back(v);
-    // If wasDecl, then:
+    std::map<std::pair<std::string, Sort>, Term>::const_iterator itv =
+        d_varCache.find(i);
+    if (itv == d_varCache.end() || !isDeclared(i.first))
+    {
+      // haven't created this variable yet, or its not declared
+      Term v = bindBoundVar(i.first, i.second, fresh);
+      vars.push_back(v);
+      continue;
+    }
+    Term v = itv->second;
+    // If we are here, then:
     // (1) we are not using fresh declarations
     // (2) there are let binders present,
     // (3) the current variable was shadowed.
     // We must check whether the variable is present in the let bindings.
-    if (wasDecl)
+    bool reqFresh = false;
+    // a dummy variable used for checking containment below
+    Term vr = d_tm.mkVar(v.getSort(), "dummy");
+    // check if it is contained in a let binder, if so, we require making a
+    // fresh variable, despite fresh-binders being false.
+    for (std::vector<std::pair<std::string, Term>>& lbs : letBinders)
     {
-      // a dummy variable used for checking containment below
-      Term vr = d_tm.mkVar(v.getSort(), "dummy");
-      // check if it is contained in a let binder, if so, we fail
-      for (std::vector<std::pair<std::string, Term>>& lbs : letBinders)
+      for (std::pair<std::string, Term>& lb : lbs)
       {
-        for (std::pair<std::string, Term>& lb : lbs)
+        // To test containment, we use Term::substitute.
+        // If the substitution does anything at all, then we will throw a
+        // warning. We expect this warning to be very rare.
+        Term slbt = lb.second.substitute({v}, {vr});
+        if (slbt != lb.second)
         {
-          // To test containment, we use Term::substitute.
-          // If the substitution does anything at all, then
-          // we will throw an error. Thus, this does not
-          // incur a performance penalty versus checking containment.
-          Term slbt = lb.second.substitute({v}, {vr});
-          if (slbt != lb.second)
-          {
-            std::stringstream ss;
-            ss << "Cannot use variable shadowing for " << i.first
-               << " since this symbol occurs in a let term that is present in "
-                  "the current context. Set fresh-binders to true to avoid "
-                  "this error";
-            parseError(ss.str());
-          }
+          reqFresh = true;
+          break;
         }
       }
+      if (reqFresh)
+      {
+        break;
+      }
     }
+    if (reqFresh)
+    {
+      // Note that if this warning is thrown:
+      // 1. proof reference checking will not be accurate in settings where
+      // variables are parsed as canonical.
+      // 2. the parser will not be deterministic for the same input even when
+      // fresh-binders is false, since we are constructing a fresh variable
+      // below.
+      Warning() << "Constructing a fresh variable for " << i.first
+                << " since this symbol occurs in a let term that is present in "
+                   "the current context. Set fresh-binders to true or use -q to avoid "
+                   "this warning."
+                << std::endl;
+    }
+    v = bindBoundVar(i.first, i.second, reqFresh);
+    vars.push_back(v);
   }
   return vars;
 }
diff --git a/test/regress/cli/regress0/quantifiers/issue11066-fresh-binders-err.smt2 b/test/regress/cli/regress0/quantifiers/issue11066-fresh-binders-err.smt2
index 99e1534cfea..da00df974f7 100644
--- a/test/regress/cli/regress0/quantifiers/issue11066-fresh-binders-err.smt2
+++ b/test/regress/cli/regress0/quantifiers/issue11066-fresh-binders-err.smt2
@@ -1,8 +1,8 @@
 ; DISABLE-TESTER: dump
+; DISABLE-TESTER: alethe
 ; REQUIRES: no-competition
-; SCRUBBER: grep -o "Cannot use variable shadowing"
-; EXPECT: Cannot use variable shadowing
-; EXIT: 1
+; EXPECT-ERROR: Constructing a fresh variable for x since this symbol occurs in a let term that is present in the current context. Set fresh-binders to true or use -q to avoid this warning.
+; EXPECT: unsat
 (set-logic ALL)
 (assert (exists ((x Real))
           (let ((?y x))