Package org.sosy_lab.java_smt.test

Class SolverBasedTest0

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

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	requireNativeFPToBitvector()
protected void	requireOptimization()	Skip test if the solver does not support optimization.
protected void	requireParser()
protected void	requireQuantifierElimination()
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 boolean	solverSupportsNativeFPToBitvector()
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()

requireNativeFPToBitvector

protected final void requireNativeFPToBitvector()

solverSupportsNativeFPToBitvector

protected final boolean solverSupportsNativeFPToBitvector()

requireQuantifiers

protected final void requireQuantifiers()

Skip test if the solver does not support quantifiers.

requireQuantifierElimination

protected final void requireQuantifierElimination()

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