Package org.sosy_lab.java_smt.test

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

    • Constructor Detail

      • SolverBasedTest0

        public SolverBasedTest0()

    • Method Detail

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

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

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