java.lang.Object
- org.sosy_lab.java_smt.test.SolverBasedTest0

Direct Known Subclasses:

SolverBasedTest0.ParameterizedSolverBasedTest0
```
public abstract class SolverBasedTest0
extends Object
```
Abstract base class with helpful utilities for writing tests that use an SMT solver. It instantiates and closes the SMT solver before and after each test, and provides fields with direct access to the most relevant instances.
To run the tests using all available solvers, add the following code to your class:
```
 
  @Parameters(name="{0}")
  public static List<Object[]> getAllSolvers() {
    return allSolversAsParameters();
  }

  @Parameter(0)
  public Solvers solver;

  @Override
  protected Solvers solverToUse() {
    return solver;
  }
 
 
```
assertThatFormula(BooleanFormula) can be used to easily write assertions about formulas using Truth.
Test that rely on a theory that not all solvers support should call one of the require methods at the beginning.

Nested Class Summary

Nested Classes
Modifier and Type Class Description

static class SolverBasedTest0.ParameterizedSolverBasedTest0

Field Summary

Fields
Modifier and Type	Field	Description
`protected @Nullable ArrayFormulaManager`	`amgr`
`protected BooleanFormulaManager`	`bmgr`
`protected @Nullable BitvectorFormulaManager`	`bvmgr`
`protected Configuration`	`config`
`protected SolverContext`	`context`
`protected @Nullable EnumerationFormulaManager`	`emgr`
`protected SolverContextFactory`	`factory`
`protected UFManager`	`fmgr`
`protected @Nullable FloatingPointFormulaManager`	`fpmgr`
`protected IntegerFormulaManager`	`imgr`
`protected LogManager`	`logger`
`protected FormulaManager`	`mgr`
`protected @Nullable QuantifiedFormulaManager`	`qmgr`
`protected @Nullable RationalFormulaManager`	`rmgr`
`protected ShutdownManager`	`shutdownManager`
`protected @Nullable StringFormulaManager`	`smgr`

Constructor Summary

Constructors
Constructor Description

SolverBasedTest0()

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`protected ProverEnvironmentSubject`	`assertThatEnvironment(BasicProverEnvironment<?> prover)`	Use this for checking assertions about ProverEnvironments with Truth: `assertThatEnvironment(stack).is...()`.
`protected BooleanFormulaSubject`	`assertThatFormula(BooleanFormula formula)`	Use this for checking assertions about BooleanFormulas with Truth: `assertThatFormula(formula).is...()`.
`void`	`closeSolver()`
`protected ConfigurationBuilder`	`createTestConfigBuilder()`
`protected void`	`evaluateInModel(BooleanFormula constraint, Formula formula, Collection<Object> possibleExpectedValues, Collection<Formula> possibleExpectedFormulas)`
`void`	`initSolver()`
`protected org.sosy_lab.java_smt.solvers.opensmt.Logics`	`logicToUse()`	This method is only called, if OpenSMT is called.
`protected void`	`requireArrayModel()`
`protected void`	`requireArrays()`	Skip test if the solver does not support arrays.
`protected void`	`requireBitvectors()`	Skip test if the solver does not support bitvectors.
`protected void`	`requireBitvectorToInt()`
`protected void`	`requireEnumeration()`	Skip test if the solver does not support enumeration theory.
`protected void`	`requireFloats()`
`protected void`	`requireIntegers()`	Skip test if the solver does not support integers.
`protected void`	`requireInterpolation()`
`protected void`	`requireModel()`
`protected void`	`requireOptimization()`	Skip test if the solver does not support optimization.
`protected void`	`requireParser()`
`protected void`	`requireQuantifiers()`	Skip test if the solver does not support quantifiers.
`protected void`	`requireRationalFloor()`
`protected void`	`requireRationals()`	Skip test if the solver does not support rationals.
`protected void`	`requireStrings()`	Skip test if the solver does not support strings.
`protected void`	`requireSubstitution()`
`protected void`	`requireUnsatCore()`
`protected void`	`requireUnsatCoreOverAssumptions()`
`protected void`	`requireUserPropagators()`
`protected void`	`requireVisitor()`
`protected ShutdownNotifier`	`shutdownNotifierToUse()`
`protected SolverContextFactory.Solvers`	`solverToUse()`	Return the solver to use in this test.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

config
```
protected Configuration config
```

logger
```
protected final LogManager logger
```

factory
```
protected SolverContextFactory factory
```

context
```
protected SolverContext context
```

mgr
```
protected FormulaManager mgr
```

bmgr
```
protected BooleanFormulaManager bmgr
```

fmgr
```
protected UFManager fmgr
```

imgr
```
protected IntegerFormulaManager imgr
```

rmgr

protected @Nullable RationalFormulaManager rmgr

bvmgr

protected @Nullable BitvectorFormulaManager bvmgr

qmgr

protected @Nullable QuantifiedFormulaManager qmgr

amgr

protected @Nullable ArrayFormulaManager amgr

fpmgr

protected @Nullable FloatingPointFormulaManager fpmgr

smgr

protected @Nullable StringFormulaManager smgr

emgr

protected @Nullable EnumerationFormulaManager emgr

shutdownManager

protected ShutdownManager shutdownManager

Constructor Detail
- SolverBasedTest0
```
public SolverBasedTest0()
```

Method Detail

shutdownNotifierToUse

protected ShutdownNotifier shutdownNotifierToUse()

solverToUse
```
protected SolverContextFactory.Solvers solverToUse()
```
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.

logicToUse
```
protected org.sosy_lab.java_smt.solvers.opensmt.Logics logicToUse()
```
This method is only called, if OpenSMT is called. OpenSMT needs to know the logic upfront.

createTestConfigBuilder

protected ConfigurationBuilder createTestConfigBuilder()

initSolver

public final void initSolver()
                      throws InvalidConfigurationException

Throws:: InvalidConfigurationException

closeSolver
```
public final void closeSolver()
```

requireIntegers
```
protected final void requireIntegers()
```
Skip test if the solver does not support integers.

requireRationals
```
protected final void requireRationals()
```
Skip test if the solver does not support rationals.

requireRationalFloor

protected final void requireRationalFloor()

requireBitvectors
```
protected final void requireBitvectors()
```
Skip test if the solver does not support bitvectors.

requireBitvectorToInt

protected final void requireBitvectorToInt()

requireQuantifiers
```
protected final void requireQuantifiers()
```
Skip test if the solver does not support quantifiers.

requireArrays
```
protected void requireArrays()
```
Skip test if the solver does not support arrays.

requireFloats
```
protected final void requireFloats()
```

requireStrings
```
protected final void requireStrings()
```
Skip test if the solver does not support strings.

requireEnumeration
```
protected final void requireEnumeration()
```
Skip test if the solver does not support enumeration theory.

requireOptimization
```
protected final void requireOptimization()
```
Skip test if the solver does not support optimization.

requireInterpolation

protected final void requireInterpolation()

requireParser
```
protected void requireParser()
```

requireArrayModel
```
protected void requireArrayModel()
```

requireModel
```
protected void requireModel()
```

requireVisitor
```
protected void requireVisitor()
```

requireUnsatCore
```
protected void requireUnsatCore()
```

requireUnsatCoreOverAssumptions

protected void requireUnsatCoreOverAssumptions()

requireSubstitution
```
protected void requireSubstitution()
```

requireUserPropagators

protected void requireUserPropagators()

assertThatFormula
```
protected final BooleanFormulaSubject assertThatFormula(BooleanFormula formula)
```
Use this for checking assertions about BooleanFormulas with Truth: assertThatFormula(formula).is...().

assertThatEnvironment
```
protected final ProverEnvironmentSubject assertThatEnvironment(BasicProverEnvironment<?> prover)
```
Use this for checking assertions about ProverEnvironments with Truth: assertThatEnvironment(stack).is...().
For new code, we suggest using ProverEnvironmentSubject.assertThat(BasicProverEnvironment) with a static import.

evaluateInModel

protected void evaluateInModel(BooleanFormula constraint,
                               Formula formula,
                               Collection<Object> possibleExpectedValues,
                               Collection<Formula> possibleExpectedFormulas)
                        throws SolverException,
                               InterruptedException

Throws:: SolverException; InterruptedException

Class SolverBasedTest0

Nested Class Summary

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

config

logger

factory

context

mgr

bmgr

fmgr

imgr

rmgr

bvmgr

qmgr

amgr

fpmgr

smgr

emgr

shutdownManager

Constructor Detail

SolverBasedTest0

Method Detail

shutdownNotifierToUse

solverToUse

logicToUse

createTestConfigBuilder

initSolver

closeSolver

requireIntegers

requireRationals

requireRationalFloor

requireBitvectors

requireBitvectorToInt

requireQuantifiers

requireArrays

requireFloats

requireStrings

requireEnumeration

requireOptimization

requireInterpolation

requireParser

requireArrayModel

requireModel

requireVisitor

requireUnsatCore

requireUnsatCoreOverAssumptions

requireSubstitution

requireUserPropagators

assertThatFormula

assertThatEnvironment

evaluateInModel