Cleanup usage of bound variables

src/org/sosy_lab/java_smt/api/visitors/BooleanFormulaTransformationVisitor.java

@@ -37,11 +37,6 @@ public BooleanFormula visitConstant(boolean value) {
     return bfmgr.makeBoolean(value);
   }
 
-  @Override
-  public BooleanFormula visitBoundVar(BooleanFormula var, int deBruijnIdx) {
-    return var;
-  }
-
   @Override
   public BooleanFormula visitAtom(BooleanFormula pAtom, FunctionDeclaration<BooleanFormula> decl) {
     return pAtom;

src/org/sosy_lab/java_smt/api/visitors/BooleanFormulaVisitor.java

@@ -31,8 +31,23 @@ public interface BooleanFormulaVisitor<R> {
    */
   R visitConstant(boolean value);
 
-  /** Visit a boolean variable bound by a quantifier. */
-  R visitBoundVar(BooleanFormula var, int deBruijnIdx);
+  /**
+   * Visit a boolean variable bound by a quantifier.
+   *
+   * <p>Since JavaSMT no longer explicitly visits bound variables, and never has done so for most
+   * solvers, this method will be removed in the future. Bound variables are available when visiting
+   * a quantified formula, and can be accessed in {@link #visitQuantifier}. When entering the body
+   * of a quantified formula, bound variables are seen as free variables, as documented in {@link
+   * FormulaVisitor#visitQuantifier}.
+   */
+  @Deprecated(since = "2025.07, because bound variables are never created or used in the visitor")
+  @SuppressWarnings("unused")
+  default R visitBoundVar(BooleanFormula var, int deBruijnIdx) {
+    throw new UnsupportedOperationException(
+        "Bound variables are no longer explicitly visited in JavaSMT. "
+            + "Use a combination of 'visitQuantifier' (for the whole quantified formula) and "
+            + "'visitAtom' (for variables in the body) instead.");
+  }
 
   /**
    * Visit a NOT-expression.

src/org/sosy_lab/java_smt/api/visitors/DefaultBooleanFormulaVisitor.java

@@ -28,11 +28,6 @@ public R visitConstant(boolean value) {
     return visitDefault();
   }
 
-  @Override
-  public R visitBoundVar(BooleanFormula var, int deBruijnIdx) {
-    return visitDefault();
-  }
-
   @Override
   public R visitAtom(BooleanFormula pAtom, FunctionDeclaration<BooleanFormula> decl) {
     return visitDefault();

src/org/sosy_lab/java_smt/api/visitors/DefaultFormulaVisitor.java

@@ -29,11 +29,6 @@ public R visitFreeVariable(Formula f, String name) {
     return visitDefault(f);
   }
 
-  @Override
-  public R visitBoundVariable(Formula f, int deBruijnIdx) {
-    return visitDefault(f);
-  }
-
   @Override
   public R visitConstant(Formula f, Object value) {
     return visitDefault(f);

src/org/sosy_lab/java_smt/api/visitors/FormulaTransformationVisitor.java

@@ -33,11 +33,6 @@ public Formula visitFreeVariable(Formula f, String name) {
     return f;
   }
 
-  @Override
-  public Formula visitBoundVariable(Formula f, int deBruijnIdx) {
-    return f;
-  }
-
   @Override
   public Formula visitConstant(Formula f, Object value) {
     return f;

src/org/sosy_lab/java_smt/api/visitors/FormulaVisitor.java

@@ -38,11 +38,22 @@ public interface FormulaVisitor<R> {
    * Visit a variable bound by a quantifier. The variable can have any sort (both boolean and
    * non-boolean).
    *
+   * <p>This method is deprecated because bound variables are no longer explicitly visited. When
+   * entering a quantified formula, bound variables are seen as free variables, as documented in
+   * {@link #visitQuantifier}. When entering the body of a quantified formula, bound variables are
+   * replaced by free variables, and are visited with {@link #visitFreeVariable}.
+   *
    * @param f Formula representing the variable.
    * @param deBruijnIdx de-Bruijn index of the bound variable, which can be used to find the
    *     matching quantifier.
    */
-  R visitBoundVariable(Formula f, int deBruijnIdx);
+  @Deprecated(since = "2025.07, because bound variables are never created or used in the visitor")
+  default R visitBoundVariable(Formula f, int deBruijnIdx) {
+    throw new UnsupportedOperationException(
+        "Bound variables are no longer explicitly visited in JavaSMT. "
+            + "Use a combination of 'visitQuantifier' (for the whole quantified formula) and "
+            + "'visitFreeVariable' (in the body) instead.");
+  }
 
   /**
    * Visit a constant, such as "true"/"false", a numeric constant like "1" or "1.0", a String

src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java

@@ -319,14 +319,6 @@ public R visitFreeVariable(Formula f, String name) {
               formulaCreator.getBooleanVarDeclaration(casted)));
     }
 
-    @Override
-    public R visitBoundVariable(Formula f, int deBruijnIdx) {
-
-      // Only boolean formulas can appear here.
-      assert f instanceof BooleanFormula;
-      return delegate.visitBoundVar((BooleanFormula) f, deBruijnIdx);
-    }
-
     @Override
     public R visitConstant(Formula f, Object value) {
       checkState(value instanceof Boolean);

src/org/sosy_lab/java_smt/basicimpl/AbstractQuantifiedFormulaManager.java

@@ -8,6 +8,8 @@
 
 package org.sosy_lab.java_smt.basicimpl;
 
+import static com.google.common.base.Preconditions.checkArgument;
+
 import com.google.common.collect.Lists;
 import java.util.List;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -41,6 +43,8 @@ protected abstract TFormulaInfo eliminateQuantifiers(TFormulaInfo pExtractInfo)
   @Override
   public BooleanFormula mkQuantifier(
       Quantifier q, List<? extends Formula> pVariables, BooleanFormula pBody) {
+    checkArgument(
+        !pVariables.isEmpty(), "Missing variables for quantifier '%s' and body '%s'.", q, pBody);
     return wrap(
         mkQuantifier(q, Lists.transform(pVariables, this::extractInfo), extractInfo(pBody)));
   }

src/org/sosy_lab/java_smt/basicimpl/FormulaTransformationVisitorImpl.java

@@ -41,15 +41,6 @@ public Void visitFreeVariable(Formula f, String name) {
     return null;
   }
 
-  @Override
-  public Void visitBoundVariable(Formula f, int deBruijnIdx) {
-    Preconditions.checkNotNull(f);
-
-    // Bound variable transformation is not allowed.
-    pCache.put(f, f);
-    return null;
-  }
-
   @Override
   public Void visitConstant(Formula f, Object value) {
     Preconditions.checkNotNull(f);

src/org/sosy_lab/java_smt/basicimpl/RecursiveFormulaVisitorImpl.java

@@ -64,11 +64,6 @@ public TraversalProcess visitFreeVariable(Formula pF, String pName) {
     return delegate.visitFreeVariable(pF, pName);
   }
 
-  @Override
-  public TraversalProcess visitBoundVariable(Formula pF, int pDeBruijnIdx) {
-    return delegate.visitBoundVariable(pF, pDeBruijnIdx);
-  }
-
   @Override
   public TraversalProcess visitConstant(Formula pF, Object pValue) {
     return delegate.visitConstant(pF, pValue);

src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java

@@ -133,7 +133,7 @@ public static List<String> tokenize(String input) {
     }
     if (level != 0) {
       // Throw an exception if the brackets don't match
-      throw new IllegalArgumentException();
+      throw new IllegalArgumentException("brackets do not match, too many open brackets");
     }
     return builder.build();
   }

src/org/sosy_lab/java_smt/example/FormulaClassifier.java

@@ -253,12 +253,6 @@ public Integer visitFreeVariable(Formula pF, String pName) {
       return 1;
     }
 
-    @Override
-    public Integer visitBoundVariable(Formula pF, int pDeBruijnIdx) {
-      checkType(pF);
-      return 1;
-    }
-
     @Override
     public Integer visitConstant(Formula pF, Object pValue) {
       checkType(pF);

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java

@@ -393,6 +393,7 @@ public FormulaType<?> getFormulaType(Term formula) {
     return bitwuzlaSortToType(pType);
   }
 
+  @SuppressWarnings("deprecation")
   @Override
   public <R> R visit(FormulaVisitor<R> visitor, Formula formula, Term f)
       throws UnsupportedOperationException {

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java

@@ -206,7 +206,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, Long f) {
   // Hopefully a helpful template for when visitor gets implemented
   // Btor only has bitvec arrays and ufs with bitvecs and arrays of bitvecs
   // (and quantifier with bitvecs only)
-  @SuppressWarnings("unused")
+  @SuppressWarnings({"deprecation", "unused"})
   private <R> R visit1(FormulaVisitor<R> visitor, Formula formula, Long f) {
     if (BtorJNI.boolector_is_const(getEnv(), f)) {
       // Handles all constants (bitvec, bool)

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java

@@ -296,6 +296,7 @@ private static String getName(Expr e) {
     return dequote(e.toString());
   }
 
+  @SuppressWarnings("deprecation")
   @Override
   public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Expr f) {
     checkState(!f.isNull());

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4QuantifiedFormulaManager.java

@@ -8,6 +8,8 @@
 
 package org.sosy_lab.java_smt.solvers.cvc4;
 
+import static com.google.common.base.Preconditions.checkArgument;
+
 import edu.stanford.CVC4.Expr;
 import edu.stanford.CVC4.ExprManager;
 import edu.stanford.CVC4.Kind;
@@ -72,23 +74,22 @@ protected Expr eliminateQuantifiers(Expr pExtractInfo)
    */
   @Override
   public Expr mkQuantifier(Quantifier pQ, List<Expr> pVars, Expr pBody) {
-    if (pVars.isEmpty()) {
-      throw new IllegalArgumentException("Empty variable list for quantifier.");
-    } else {
-      // CVC4 uses its own lists for quantifier that may only have bound vars
-      vectorExpr vec = new vectorExpr();
-      Expr substBody = pBody;
-      // every free needs a bound copy. As the internal Id is different for every variable, even
-      // with the same name, this is fine.
-      for (Expr var : pVars) {
-        Expr boundCopy = ((CVC4FormulaCreator) formulaCreator).makeBoundCopy(var);
-        vec.add(boundCopy);
-        substBody = substBody.substitute(var, boundCopy);
-      }
-      Expr quantifiedVars = exprManager.mkExpr(Kind.BOUND_VAR_LIST, vec);
+    checkArgument(
+        !pVars.isEmpty(), "Missing variables for quantifier '%s' and body '%s'.", pQ, pBody);
 
-      Kind quant = pQ == Quantifier.EXISTS ? Kind.EXISTS : Kind.FORALL;
-      return exprManager.mkExpr(quant, quantifiedVars, substBody);
+    // CVC4 uses its own lists for quantifier that may only have bound vars
+    vectorExpr vec = new vectorExpr();
+    Expr substBody = pBody;
+    // every free needs a bound copy. As the internal Id is different for every variable, even
+    // with the same name, this is fine.
+    for (Expr var : pVars) {
+      Expr boundCopy = ((CVC4FormulaCreator) formulaCreator).makeBoundCopy(var);
+      vec.add(boundCopy);
+      substBody = substBody.substitute(var, boundCopy);
     }
+    Expr quantifiedVars = exprManager.mkExpr(Kind.BOUND_VAR_LIST, vec);
+
+    Kind quant = pQ == Quantifier.EXISTS ? Kind.EXISTS : Kind.FORALL;
+    return exprManager.mkExpr(quant, quantifiedVars, substBody);
   }
 }

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java

@@ -369,6 +369,7 @@ private String getName(Term e) {
     }
   }
 
+  @SuppressWarnings("deprecation")
   @Override
   public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
     checkState(!f.isNull());

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5QuantifiedFormulaManager.java

@@ -8,6 +8,8 @@
 
 package org.sosy_lab.java_smt.solvers.cvc5;
 
+import static com.google.common.base.Preconditions.checkArgument;
+
 import io.github.cvc5.Kind;
 import io.github.cvc5.Solver;
 import io.github.cvc5.Sort;
@@ -63,22 +65,21 @@ protected Term eliminateQuantifiers(Term input) throws SolverException, Interrup
    */
   @Override
   public Term mkQuantifier(Quantifier pQ, List<Term> pVars, Term pBody) {
-    if (pVars.isEmpty()) {
-      throw new IllegalArgumentException("Empty variable list for quantifier.");
-    } else {
-      List<Term> boundVars = new ArrayList<>();
-      Term substBody = pBody;
-      // every free needs a bound copy. As the internal Id is different for every variable, even
-      // with the same name, this is fine.
-      for (Term var : pVars) {
-        Term boundCopy = ((CVC5FormulaCreator) formulaCreator).makeBoundCopy(var);
-        boundVars.add(boundCopy);
-        substBody = substBody.substitute(var, boundCopy);
-      }
+    checkArgument(
+        !pVars.isEmpty(), "Missing variables for quantifier '%s' and body '%s'.", pQ, pBody);
 
-      Kind quant = pQ == Quantifier.EXISTS ? Kind.EXISTS : Kind.FORALL;
-      Term boundVarsList = termManager.mkTerm(Kind.VARIABLE_LIST, boundVars.toArray(new Term[0]));
-      return termManager.mkTerm(quant, boundVarsList, substBody);
+    List<Term> boundVars = new ArrayList<>();
+    Term substBody = pBody;
+    // every free needs a bound copy. As the internal Id is different for every variable, even
+    // with the same name, this is fine.
+    for (Term var : pVars) {
+      Term boundCopy = ((CVC5FormulaCreator) formulaCreator).makeBoundCopy(var);
+      boundVars.add(boundCopy);
+      substBody = substBody.substitute(var, boundCopy);
     }
+
+    Kind quant = pQ == Quantifier.EXISTS ? Kind.EXISTS : Kind.FORALL;
+    Term boundVarsList = termManager.mkTerm(Kind.VARIABLE_LIST, boundVars.toArray(new Term[0]));
+    return termManager.mkTerm(quant, boundVarsList, substBody);
   }
 }