Package org.sosy_lab.java_smt.test
Class SolverBasedTest0.ParameterizedSolverBasedTest0
- java.lang.Object
-
- org.sosy_lab.java_smt.test.SolverBasedTest0
-
- org.sosy_lab.java_smt.test.SolverBasedTest0.ParameterizedSolverBasedTest0
-
- Direct Known Subclasses:
SolverStackTest0
- Enclosing class:
- SolverBasedTest0
public abstract static class SolverBasedTest0.ParameterizedSolverBasedTest0 extends SolverBasedTest0
-
-
Nested Class Summary
-
Nested classes/interfaces inherited from class org.sosy_lab.java_smt.test.SolverBasedTest0
SolverBasedTest0.ParameterizedSolverBasedTest0
-
-
Constructor Summary
Constructors Constructor Description ParameterizedSolverBasedTest0()
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description static SolverContextFactory.Solvers[]
getAllSolvers()
protected SolverContextFactory.Solvers
solverToUse()
Return the solver to use in this test.-
Methods inherited from class org.sosy_lab.java_smt.test.SolverBasedTest0
assertThatEnvironment, assertThatFormula, closeSolver, createTestConfigBuilder, evaluateInModel, initSolver, logicToUse, requireArrayModel, requireArrays, requireBitvectors, requireBitvectorToInt, requireEnumeration, requireFloats, requireFPToBitvector, requireIntegers, requireInterpolation, requireModel, requireOptimization, requireParser, requireQuantifierElimination, requireQuantifiers, requireRationalFloor, requireRationals, requireStrings, requireSubstitution, requireUnsatCore, requireUnsatCoreOverAssumptions, requireUserPropagators, requireVisitor, shutdownNotifierToUse
-
-
-
-
Field Detail
-
solver
public SolverContextFactory.Solvers solver
-
-
Method Detail
-
getAllSolvers
public static SolverContextFactory.Solvers[] getAllSolvers()
-
solverToUse
protected SolverContextFactory.Solvers solverToUse()
Description copied from class:SolverBasedTest0
Return the solver to use in this test. The default is SMTInterpol because it's the only solver guaranteed on all platforms. Overwrite to specify a different solver.- Overrides:
solverToUse
in classSolverBasedTest0
-
-