Downgrade the required use of fresh-binder to a warning (cvc5#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 cvc5#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 <[email protected]>

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;
 }

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))