Merge pull request #491 from sosy-lab/feat/cleanup-bound-vars

Cleanup usage of bound variables

Author: kfriedberger

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