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

Field Summary

Fields

Modifier and Type	Field	Description
SolverContextFactory.Solvers	solver

Fields inherited from class org.sosy_lab.java_smt.test.SolverBasedTest0

amgr, bmgr, bvmgr, config, context, emgr, factory, fmgr, fpmgr, imgr, logger, mgr, qmgr, rmgr, shutdownManager, slmgr, smgr, testName

Constructor Summary

Constructors

Constructor	Description
ParameterizedSolverBasedTest0()

Method Summary

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

addNumber, assertThatEnvironment, assertThatFormula, closeSolver, createTestConfigBuilder, enableTracing, evaluateInModel, greaterThanNumber, initSolver, lessThanNumber, logicToUse, makeNumber, makeVariable, multiplyNumber, requireArrayModel, requireArrays, requireBitvectors, requireBitvectorToInt, requireConstArrays, requireEnumeration, requireFloats, requireFPToBitvector, requireIntegers, requireInterpolation, requireModel, requireOptimization, requireParser, requireQuantifierElimination, requireQuantifiers, requireRationalFloor, requireRationals, requireSeparationLogic, requireStrings, requireSubstitution, requireUnsatCore, requireUnsatCoreOverAssumptions, requireUserPropagators, requireVisitor, shutdownNotifierToUse

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Details

solver

public SolverContextFactory.Solvers solver

Constructor Details

ParameterizedSolverBasedTest0

public ParameterizedSolverBasedTest0()

Method Details

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 class SolverBasedTest0