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.

  • Field Details

  • Constructor Details

    • SolverBasedTest0

      public SolverBasedTest0()

  • Method Details

    • 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() throws InvalidConfigurationException
      Throws:
      InvalidConfigurationException

    • enableTracing

      protected boolean enableTracing()
      Determines whether execution tracing is enabled for the test suite.

      Tracing is disabled by default for the following reasons:

      • Compatibility: Some solvers lack support for tracing-related operations, such as formula visitation or BitVector-to-Integer conversion.
      • Isolation: Tracing can alter memory pressure or formula allocation patterns, potentially causing non-deterministic behavior or masking bugs.
      • Performance: Enabling tracing may increase execution time and complicate the debugging process.

      To enable tracing, override this method in your test class to return true. The produced trace will be stored in the "output/traces" directory with a filename pattern of "trace_[TestClassName]_[TestMethodName]_[Timestamp].java".

      Returns:
      true if tracing should be enabled; false otherwise.

    • 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()

    • requireFPToBitvector

      protected final void requireFPToBitvector()

    • requireQuantifiers

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

    • requireQuantifierElimination

      protected final void requireQuantifierElimination()

    • requireArrays

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

    • requireConstArrays

      protected final void requireConstArrays()
      Skip test if the solver does not support constant arrays.

    • requireFloats

      protected final void requireFloats()
      Skip test if the solver does not support floats.

    • 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.

    • requireSeparationLogic

      protected final void requireSeparationLogic()

    • 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

    • makeVariable

      protected Formula makeVariable(String name)

    • makeNumber

      protected Formula makeNumber(int number)

    • addNumber

      protected Formula addNumber(Formula x, Formula y)

    • multiplyNumber

      protected Formula multiplyNumber(Formula x, Formula y)

    • lessThanNumber

      protected BooleanFormula lessThanNumber(Formula x, Formula y)

    • greaterThanNumber

      protected BooleanFormula greaterThanNumber(Formula x, Formula y)