simplify API inheritance by using default methods.

Author: kfriedberger

src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java

@@ -413,4 +413,8 @@ default BitvectorFormula extract(BitvectorFormula number, int msb, int lsb, bool
 
   /** All given bitvectors are pairwise unequal. */
   BooleanFormula distinct(List<BitvectorFormula> pBits);
+
+  default BooleanFormula distinct(BitvectorFormula... pBits) {
+    return distinct(List.of(pBits));
+  }
 }

src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java

@@ -10,6 +10,7 @@
 
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
 import java.util.Collection;
+import java.util.List;
 import java.util.Set;
 import java.util.stream.Collector;
 import org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor;
@@ -111,7 +112,9 @@ default BooleanFormula makeBoolean(boolean value) {
   /**
    * @see #and(BooleanFormula, BooleanFormula)
    */
-  BooleanFormula and(BooleanFormula... bits);
+  default BooleanFormula and(BooleanFormula... bits) {
+    return and(List.of(bits));
+  }
 
   /** Return a stream {@link Collector} that creates a conjunction of all elements in the stream. */
   Collector<BooleanFormula, ?, BooleanFormula> toConjunction();
@@ -133,7 +136,9 @@ default BooleanFormula makeBoolean(boolean value) {
   /**
    * @see #or(BooleanFormula, BooleanFormula)
    */
-  BooleanFormula or(BooleanFormula... bits);
+  default BooleanFormula or(BooleanFormula... bits) {
+    return or(List.of(bits));
+  }
 
   /** Return a stream {@link Collector} that creates a disjunction of all elements in the stream. */
   Collector<BooleanFormula, ?, BooleanFormula> toDisjunction();

src/org/sosy_lab/java_smt/api/UFManager.java

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -18,8 +18,10 @@ <T extends Formula> FunctionDeclaration<T> declareUF(
       String name, FormulaType<T> returnType, List<FormulaType<?>> args);
 
   /** Declare an uninterpreted function. */
-  <T extends Formula> FunctionDeclaration<T> declareUF(
-      String name, FormulaType<T> returnType, FormulaType<?>... args);
+  default <T extends Formula> FunctionDeclaration<T> declareUF(
+      String name, FormulaType<T> returnType, FormulaType<?>... args) {
+    return declareUF(name, returnType, List.of(args));
+  }
 
   /**
    * Create an uninterpreted function call.
@@ -35,7 +37,9 @@ <T extends Formula> FunctionDeclaration<T> declareUF(
   /**
    * @see #callUF(FunctionDeclaration, List)
    */
-  <T extends Formula> T callUF(FunctionDeclaration<T> funcType, Formula... args);
+  default <T extends Formula> T callUF(FunctionDeclaration<T> funcType, Formula... args) {
+    return callUF(funcType, List.of(args));
+  }
 
   /**
    * Declares and calls an uninterpreted function with exactly the given name.
@@ -52,5 +56,8 @@ <T extends Formula> T declareAndCallUF(
   /**
    * @see #declareAndCallUF(String, FormulaType, List)
    */
-  <T extends Formula> T declareAndCallUF(String name, FormulaType<T> pReturnType, Formula... pArgs);
+  default <T extends Formula> T declareAndCallUF(
+      String name, FormulaType<T> pReturnType, Formula... pArgs) {
+    return declareAndCallUF(name, pReturnType, List.of(pArgs));
+  }
 }

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

@@ -17,7 +17,6 @@
 import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Iterables;
 import java.util.ArrayDeque;
-import java.util.Arrays;
 import java.util.Collection;
 import java.util.Deque;
 import java.util.HashMap;
@@ -117,11 +116,6 @@ public BooleanFormula and(Collection<BooleanFormula> pBits) {
     }
   }
 
-  @Override
-  public BooleanFormula and(BooleanFormula... pBits) {
-    return and(Arrays.asList(pBits));
-  }
-
   /**
    * Create an n-ary conjunction. The default implementation delegates to {@link #and(Object,
    * Object)} and assumes that all simplifications are done by that method. This method can be
@@ -154,11 +148,6 @@ public BooleanFormula or(BooleanFormula pBits1, BooleanFormula pBits2) {
     return wrap(or(param1, param2));
   }
 
-  @Override
-  public BooleanFormula or(BooleanFormula... pBits) {
-    return or(Arrays.asList(pBits));
-  }
-
   protected abstract TFormulaInfo or(TFormulaInfo pParam1, TFormulaInfo pParam2);
 
   @Override

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

@@ -49,18 +49,6 @@ public final <T extends Formula> FunctionDeclaration<T> declareUF(
         formulaCreator.declareUFImpl(pName, toSolverType(pReturnType), argTypes));
   }
 
-  @Override
-  public <T extends Formula> FunctionDeclaration<T> declareUF(
-      String pName, FormulaType<T> pReturnType, FormulaType<?>... pArgs) {
-    checkVariableName(pName);
-    return declareUF(pName, pReturnType, Arrays.asList(pArgs));
-  }
-
-  @Override
-  public <T extends Formula> T callUF(FunctionDeclaration<T> funcType, Formula... args) {
-    return formulaCreator.callFunction(funcType, Arrays.asList(args));
-  }
-
   @Override
   public final <T extends Formula> T callUF(
       FunctionDeclaration<T> pFunc, List<? extends Formula> pArgs) {

src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBooleanFormulaManager.java

@@ -129,17 +129,6 @@ public BooleanFormula and(Collection<BooleanFormula> bits) {
     return result;
   }
 
-  @Override
-  public BooleanFormula and(BooleanFormula... bits) {
-    debugging.assertThreadLocal();
-    for (BooleanFormula f : bits) {
-      debugging.assertFormulaInContext(f);
-    }
-    BooleanFormula result = delegate.and(bits);
-    debugging.addFormulaTerm(result);
-    return result;
-  }
-
   @Override
   public Collector<BooleanFormula, ?, BooleanFormula> toConjunction() {
     return Collectors.collectingAndThen(
@@ -175,17 +164,6 @@ public BooleanFormula or(Collection<BooleanFormula> bits) {
     return result;
   }
 
-  @Override
-  public BooleanFormula or(BooleanFormula... bits) {
-    debugging.assertThreadLocal();
-    for (BooleanFormula f : bits) {
-      debugging.assertFormulaInContext(f);
-    }
-    BooleanFormula result = delegate.or(bits);
-    debugging.addFormulaTerm(result);
-    return result;
-  }
-
   @Override
   public Collector<BooleanFormula, ?, BooleanFormula> toDisjunction() {
     return Collectors.collectingAndThen(

src/org/sosy_lab/java_smt/delegate/debugging/DebuggingUFManager.java

@@ -34,15 +34,6 @@ public <T extends Formula> FunctionDeclaration<T> declareUF(
     return result;
   }
 
-  @Override
-  public <T extends Formula> FunctionDeclaration<T> declareUF(
-      String name, FormulaType<T> returnType, FormulaType<?>... args) {
-    debugging.assertThreadLocal();
-    FunctionDeclaration<T> result = delegate.declareUF(name, returnType, args);
-    debugging.addFunctionDeclaration(result);
-    return result;
-  }
-
   @Override
   public <T extends Formula> T callUF(
       FunctionDeclaration<T> funcType, List<? extends Formula> args) {
@@ -56,18 +47,6 @@ public <T extends Formula> T callUF(
     return result;
   }
 
-  @Override
-  public <T extends Formula> T callUF(FunctionDeclaration<T> funcType, Formula... args) {
-    debugging.assertThreadLocal();
-    debugging.assertDeclarationInContext(funcType);
-    for (Formula t : args) {
-      debugging.assertFormulaInContext(t);
-    }
-    T result = delegate.callUF(funcType, args);
-    debugging.addFormulaTerm(result);
-    return result;
-  }
-
   @Override
   public <T extends Formula> T declareAndCallUF(
       String name, FormulaType<T> pReturnType, List<Formula> pArgs) {

src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBooleanFormulaManager.java

@@ -97,12 +97,6 @@ public BooleanFormula and(Collection<BooleanFormula> pBits) {
     return delegate.and(pBits);
   }
 
-  @Override
-  public BooleanFormula and(BooleanFormula... pBits) {
-    stats.booleanOperations.getAndIncrement();
-    return delegate.and(pBits);
-  }
-
   @Override
   public Collector<BooleanFormula, ?, BooleanFormula> toConjunction() {
     return Collectors.collectingAndThen(Collectors.toList(), this::and);
@@ -120,12 +114,6 @@ public BooleanFormula or(Collection<BooleanFormula> pBits) {
     return delegate.or(pBits);
   }
 
-  @Override
-  public BooleanFormula or(BooleanFormula... pBits) {
-    stats.booleanOperations.getAndIncrement();
-    return delegate.or(pBits);
-  }
-
   @Override
   public Collector<BooleanFormula, ?, BooleanFormula> toDisjunction() {
     return Collectors.collectingAndThen(Collectors.toList(), this::or);

src/org/sosy_lab/java_smt/delegate/statistics/StatisticsUFManager.java

@@ -33,26 +33,13 @@ public <T extends Formula> FunctionDeclaration<T> declareUF(
     return delegate.declareUF(pName, pReturnType, pArgs);
   }
 
-  @Override
-  public <T extends Formula> FunctionDeclaration<T> declareUF(
-      String pName, FormulaType<T> pReturnType, FormulaType<?>... pArgs) {
-    stats.ufOperations.getAndIncrement();
-    return delegate.declareUF(pName, pReturnType, pArgs);
-  }
-
   @Override
   public <T extends Formula> T callUF(
       FunctionDeclaration<T> pFuncType, List<? extends Formula> pArgs) {
     stats.ufOperations.getAndIncrement();
     return delegate.callUF(pFuncType, pArgs);
   }
 
-  @Override
-  public <T extends Formula> T callUF(FunctionDeclaration<T> pFuncType, Formula... pArgs) {
-    stats.ufOperations.getAndIncrement();
-    return delegate.callUF(pFuncType, pArgs);
-  }
-
   @Override
   public <T extends Formula> T declareAndCallUF(
       String pName, FormulaType<T> pReturnType, List<Formula> pArgs) {

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBooleanFormulaManager.java

@@ -116,13 +116,6 @@ public BooleanFormula and(Collection<BooleanFormula> pBits) {
     }
   }
 
-  @Override
-  public BooleanFormula and(BooleanFormula... pBits) {
-    synchronized (sync) {
-      return delegate.and(pBits);
-    }
-  }
-
   @Override
   public Collector<BooleanFormula, ?, BooleanFormula> toConjunction() {
     return Collectors.collectingAndThen(Collectors.toList(), this::and);
@@ -142,13 +135,6 @@ public BooleanFormula or(Collection<BooleanFormula> pBits) {
     }
   }
 
-  @Override
-  public BooleanFormula or(BooleanFormula... pBits) {
-    synchronized (sync) {
-      return delegate.or(pBits);
-    }
-  }
-
   @Override
   public Collector<BooleanFormula, ?, BooleanFormula> toDisjunction() {
     return Collectors.collectingAndThen(Collectors.toList(), this::or);