Tests: use one central method to select solvers.

This refactoring simplifies to disable specific solvers for local testing.

Author: kfriedberger

src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java

@@ -52,7 +52,7 @@ public class NonLinearArithmeticTest<T extends NumeralFormula> extends SolverBas
   @Parameters(name = "{0} {1} {2}")
   public static Iterable<Object[]> getAllSolversAndTheories() {
     return Lists.cartesianProduct(
-            Arrays.asList(Solvers.values()),
+            Arrays.asList(ParameterizedSolverBasedTest0.getAllSolvers()),
             ImmutableList.of(FormulaType.IntegerType, FormulaType.RationalType),
             Arrays.asList(NonLinearArithmetic.values()))
         .stream()

src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java

@@ -34,7 +34,8 @@ public class NonLinearArithmeticWithModuloTest extends SolverBasedTest0 {
   @Parameters(name = "{0} {1}")
   public static Iterable<Object[]> getAllSolversAndTheories() {
     return Lists.cartesianProduct(
-            Arrays.asList(Solvers.values()), Arrays.asList(NonLinearArithmetic.values()))
+            Arrays.asList(ParameterizedSolverBasedTest0.getAllSolvers()),
+            Arrays.asList(NonLinearArithmetic.values()))
         .stream()
         .map(List::toArray)
         .collect(toImmutableList());

src/org/sosy_lab/java_smt/test/SolverAllSatTest.java

@@ -38,7 +38,7 @@ public class SolverAllSatTest extends SolverBasedTest0 {
   @Parameters(name = "solver {0} with prover {1}")
   public static Iterable<Object[]> getAllSolvers() {
     List<Object[]> junitParams = new ArrayList<>();
-    for (Solvers solver : Solvers.values()) {
+    for (Solvers solver : ParameterizedSolverBasedTest0.getAllSolvers()) {
       junitParams.add(new Object[] {solver, "normal"});
       junitParams.add(new Object[] {solver, "itp"});
       junitParams.add(new Object[] {solver, "opt"});

src/org/sosy_lab/java_smt/test/SolverBasedTest0.java

@@ -426,7 +426,7 @@ protected void evaluateInModel(
   public abstract static class ParameterizedSolverBasedTest0 extends SolverBasedTest0 {
 
     @Parameters(name = "{0}")
-    public static Object[] getAllSolvers() {
+    public static Solvers[] getAllSolvers() {
       return Solvers.values();
     }
 

src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java

@@ -56,6 +56,7 @@
 import org.sosy_lab.java_smt.api.SolverContext;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.test.SolverBasedTest0.ParameterizedSolverBasedTest0;
 
 @SuppressWarnings("resource")
 @RunWith(Parameterized.class)
@@ -95,7 +96,7 @@ public class SolverConcurrencyTest {
 
   @Parameters(name = "{0}")
   public static Object[] getAllSolvers() {
-    return Solvers.values();
+    return ParameterizedSolverBasedTest0.getAllSolvers();
   }
 
   @Parameter(0)

src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java

@@ -30,6 +30,7 @@
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.SolverContext;
+import org.sosy_lab.java_smt.test.SolverBasedTest0.ParameterizedSolverBasedTest0;
 
 /**
  * This JUnit test class is mainly intended for automated CI checks on different operating systems,
@@ -50,7 +51,7 @@ public class SolverContextFactoryTest {
 
   @Parameters(name = "{0}")
   public static Object[] getAllSolvers() {
-    return Solvers.values();
+    return ParameterizedSolverBasedTest0.getAllSolvers();
   }
 
   @Parameter(0)

src/org/sosy_lab/java_smt/test/TimeoutTest.java

@@ -37,7 +37,7 @@ public class TimeoutTest extends SolverBasedTest0 {
   @Parameters(name = "{0} with delay {1}")
   public static List<Object[]> getAllSolversAndDelays() {
     List<Object[]> lst = new ArrayList<>();
-    for (Solvers solver : Solvers.values()) {
+    for (Solvers solver : ParameterizedSolverBasedTest0.getAllSolvers()) {
       for (int delay : DELAYS) {
         lst.add(new Object[] {solver, delay});
       }

src/org/sosy_lab/java_smt/test/VariableNamesTest.java

@@ -23,10 +23,6 @@
 import java.util.function.BiFunction;
 import java.util.function.Function;
 import org.junit.Test;
-import org.junit.runner.RunWith;
-import org.junit.runners.Parameterized;
-import org.junit.runners.Parameterized.Parameter;
-import org.junit.runners.Parameterized.Parameters;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.FloatingPointFormula;
@@ -40,9 +36,8 @@
 import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor;
 import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
 
-@RunWith(Parameterized.class)
 @SuppressFBWarnings(value = "DLS_DEAD_LOCAL_STORE")
-public class VariableNamesTest extends SolverBasedTest0 {
+public class VariableNamesTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
 
   private static final ImmutableList<String> NAMES =
       ImmutableList.of(
@@ -175,19 +170,6 @@ protected List<String> getAllNames() {
         .build();
   }
 
-  @Parameters(name = "{0}")
-  public static Object[] getAllSolvers() {
-    return Solvers.values();
-  }
-
-  @Parameter(0)
-  public Solvers solver;
-
-  @Override
-  protected Solvers solverToUse() {
-    return solver;
-  }
-
   boolean allowInvalidNames() {
     return true;
   }