@CheckReturnValue @ParametersAreNonnullByDefault @FieldsAreNonnullByDefault @ReturnValuesAreNonnullByDefault

Package org.sosy_lab.java_smt.api

The core interfaces for abstracting from SMT solvers and providing a common API for all solvers.

Interface Summary

Interface	Description
ArrayFormula<TI extends Formula,TE extends Formula>	A formula of the array sort.
ArrayFormulaManager	This interface represents the theory of (arbitrarily nested) arrays.
BasicProverEnvironment<T>	Super interface for ProverEnvironment and InterpolatingProverEnvironment that provides only the common operations.
BasicProverEnvironment.AllSatCallback<R>	Interface for the BasicProverEnvironment.allSat(org.sosy_lab.java_smt.api.BasicProverEnvironment.AllSatCallback<R>, java.util.List<org.sosy_lab.java_smt.api.BooleanFormula>) callback.
BitvectorFormula	A formula of the bitvector sort.
BitvectorFormulaManager	Manager for dealing with formulas of the bitvector sort.
BooleanFormula	A formula of the boolean sort.
BooleanFormulaManager	Manager for dealing with boolean formulas.
EnumerationFormula	A formula of the enumeration sort.
EnumerationFormulaManager	This interface represents the theory of enumeration, i.e., datatype of limited domain sort (as defined in the SMTLIB2 standard).
Evaluator	This class provides methods to get concrete evaluations for formulas from the satisfiable solver environment.
FloatingPointFormula	Formula of the floating point sort.
FloatingPointFormulaManager	Floating point operations.
FloatingPointRoundingModeFormula	Formula representing a rounding mode for floating-point operations.
Formula	An arbitrary SMT formula.
FormulaManager	FormulaManager class contains all operations which can be performed on formulas.
FunctionDeclaration<E extends Formula>	Function declaration, for both UFs and built-in functions (theory and boolean).
IntegerFormulaManager	Interface which operates over NumeralFormula.IntegerFormulas.
InterpolatingProverEnvironment<T>	This class provides an interface to an incremental SMT solver with methods for pushing and popping formulas as well as SAT checks.
Model	This class provides a model with concrete evaluations for symbols and formulas from the satisfiable solver environment.
NumeralFormula	Formulas of any numeral sort.
NumeralFormula.IntegerFormula
NumeralFormula.RationalFormula
NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>	This interface represents the Numeral Theory.
OptimizationProverEnvironment	Interface for optimization modulo SMT.
PropagatorBackend	The PropagatorBackend class is used by UserPropagator to implement custom user propagators.
ProverEnvironment	An interface to an incremental SMT solver with methods for pushing and popping formulas as well as SAT checks.
QuantifiedFormulaManager	This interface contains methods for working with any theory with quantifiers.
RationalFormulaManager	Interface for operating over NumeralFormula.RationalFormula.
RegexFormula	A formula of the string sort.
SLFormulaManager	The SLFormulaManager can build formulae for separation logic.
SolverContext	Instances of this interface provide access to an SMT solver.
StringFormula	A formula of the string sort.
StringFormulaManager	Manager for dealing with string formulas.
UFManager	Manager for dealing with uninterpreted functions (UFs).
UserPropagator	Allows user-defined propagators (~ theory solvers) to be implemented.

Class Summary

Class	Description
FloatingPointNumber	Represents a floating-point number with customizable precision, consisting of sign, exponent, and mantissa components.
FormulaType<T extends Formula>	Type of a formula.
FormulaType.ArrayFormulaType<TI extends Formula,TE extends Formula>
FormulaType.BitvectorType
FormulaType.EnumerationFormulaType
FormulaType.FloatingPointType
FormulaType.NumeralType<T extends NumeralFormula>
Model.ValueAssignment

Enum Summary

Enum	Description
FloatingPointRoundingMode	Possible floating point rounding modes.
FunctionDeclarationKind	Types of function declarations.
OptimizationProverEnvironment.OptStatus	Status of the optimization problem.
QuantifiedFormulaManager.Quantifier
SolverContext.ProverOptions	Options for the prover environment.
Tactic	Tactic is a generic formula to formula transformation.

Exception Summary

Exception	Description
SolverException	Exception thrown if there is an error during SMT solving.