All Classes

Class	Description
AbstractArrayFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
AbstractBitvectorFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
AbstractBooleanFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
AbstractEnumerationFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
AbstractEvaluator<TFormulaInfo,TType,TEnv>
AbstractFloatingPointFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>	Similar to the other Abstract*FormulaManager classes in this package, this class serves as a helper for implementing FloatingPointFormulaManager.
AbstractFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>	Simplifies building a solver from the specific theories.
AbstractModel<TFormulaInfo,TType,TEnv>
AbstractNumeralFormulaManager<TFormulaInfo,TType,TEnv,ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula,TFuncDecl>	Similar to the other Abstract*FormulaManager classes in this package, this class serves as a helper for implementing NumeralFormulaManager.
AbstractNumeralFormulaManager.NonLinearArithmetic
AbstractProver<T>
AbstractProverWithAllSat<T>	This class is a utility-class to avoid repeated implementation of the AllSAT computation.
AbstractQuantifiedFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
AbstractSLFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
AbstractSolverContext
AbstractStringFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
AbstractUFManager<TFormulaInfo,TFunctionDecl,TType,TEnv>	This class simplifies the implementation of the FunctionFormulaManager by converting the types to the solver specific type.
AbstractUserPropagator
AllSatExample	This example shows different ways to get all satisfiable models for a given set of constraints.
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.
BasicProverWithAssumptionsWrapper<T,P extends BasicProverEnvironment<T>>
Binoxxo	This program parses a user-given Binoxxo and solves it with an SMT solver.
Binoxxo.BinoxxoSolver<S>
Binoxxo.BooleanBasedBinoxxoSolver	This solver encodes nore steps into boolean logic, which makes it about 10x faster than the Binoxxo.IntegerBasedBinoxxoSolver.
Binoxxo.IntegerBasedBinoxxoSolver
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.
BooleanFormulaSubject	Subject subclass for testing assertions about BooleanFormulas with Truth (allows using assert_().about(...).that(formula).isUnsatisfiable() etc.).
BooleanFormulaTransformationVisitor	Base class for visitors for boolean formulas that recursively transform boolean formulas.
BooleanFormulaVisitor<R>	Visitor iterating through the boolean part of the formula.
CachingModel
DebuggingArrayFormulaManager
DebuggingBitvectorFormulaManager
DebuggingBooleanFormulaManager
DebuggingEnumerationFormulaManager
DebuggingFloatingPointFormulaManager
DebuggingFormulaManager
DebuggingIntegerFormulaManager
DebuggingInterpolatingProverEnvironment<T>
DebuggingModel
DebuggingNumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
DebuggingOptimizationProverEnvironment
DebuggingProverEnvironment
DebuggingQuantifiedFormulaManager
DebuggingRationalFormulaManager
DebuggingSLFormulaManager
DebuggingSolverContext
DebuggingSolverInformation
DebuggingStringFormulaManager
DebuggingUFManager
DefaultBooleanFormulaVisitor<R>	A formula visitor which allows for the default implementation.
DefaultFormulaVisitor<R>
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.
ExpectedFormulaVisitor<R>	Like DefaultFormulaVisitor, but throws UnsupportedOperationException on unexpected formula types.
FloatingPointFormula	Formula of the floating point sort.
FloatingPointFormulaManager	Floating point operations.
FloatingPointNumber	Represents a floating-point number with customizable precision, consisting of sign, exponent, and mantissa components.
FloatingPointNumber.Sign
FloatingPointRoundingMode	Represents the various rounding modes that can be applied when converting or manipulating floating-point values and formulas.
FloatingPointRoundingModeFormula	Formula representing a rounding mode for floating-point operations.
Formula	An arbitrary SMT formula.
FormulaClassifier	This program parses user-given formulas and prints out the (minimal) matching theory for them.
FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>	This is a helper class with several methods that are commonly used throughout the basicimpl package and may have solver-specific implementations.
FormulaManager	FormulaManager class contains all operations which can be performed on formulas.
FormulaTransformationVisitor	Abstract class for formula transformation.
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>
FormulaVisitor<R>	Visitor iterating through entire formula.
FunctionDeclaration<E extends Formula>	Function declaration, for both UFs and built-in functions (theory and boolean).
FunctionDeclarationImpl<F extends Formula,T>	Declaration of a function.
FunctionDeclarationKind	Types of function declarations.
HoudiniApp	This application executes the inductive-invariant synthesis algorithm called "Houdini" taken from the paper Flanagan and Leino: "Houdini, an Annotation Assistant for ESC/Java".
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.
InterpolatingProverWithAssumptionsWrapper<T>
Interpolation	Examples for Craig/sequential/tree interpolation.
LoggingSolverContext	SolverContext that wraps all prover environments in their logging versions.
Model	This class provides a model with concrete evaluations for symbols and formulas from the satisfiable solver environment.
Model.ValueAssignment
NNFVisitor
NQueens	This example program solves a NQueens problem of given size and prints a possible solution.
NQueens	This example program solves a NQueens problem of given size and prints a possible solution.
NQueensConstraintPropagator	In addition to the enumeration done by NQueensEnumeratingPropagator, this propagator also enforces the queen placement constraints without explicit encoding.
NQueensEnumeratingPropagator	This propagator enumerates the solutions of the NQueens problem by raising a conflict whenever the solver finds a model.
NumeralFormula	Formulas of any numeral sort.
NumeralFormula.IntegerFormula
NumeralFormula.RationalFormula
NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>	This interface represents the Numeral Theory.
OptimizationFormulaWeights	Example for optimizing the weight of some constraints.
OptimizationIntReal	Example for optimizing 'x' with the constraint '0 <= x < 10'.
OptimizationProverEnvironment	Interface for optimization modulo SMT.
OptimizationProverEnvironment.OptStatus	Status of the optimization problem.
PrettyPrinter	This program parses user-given formulas and prints them in a pretty format.
PrettyPrinter
PrettyPrinter.PrinterOption
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.
ProverEnvironmentSubject	Subject subclass for testing assertions about ProverEnvironments with Truth (allows using assert_().about(...).that(stack).isUnsatisfiable() etc.).
ProverWithAssumptionsWrapper
QuantifiedFormulaManager	This interface contains methods for working with any theory with quantifiers.
QuantifiedFormulaManager.Quantifier
RationalFormulaManager	Interface for operating over NumeralFormula.RationalFormula.
RegexFormula	A formula of the string sort.
ShutdownHook	A utility class for interrupting a parallel running solver thread.
SimpleUserPropagator	Example of a simple user propagator that prohibits variables/expressions to be set to true.
SLFormulaManager	The SLFormulaManager can build formulae for separation logic.
SolverBasedTest0	Abstract base class with helpful utilities for writing tests that use an SMT solver.
SolverBasedTest0.ParameterizedSolverBasedTest0
SolverContext	Instances of this interface provide access to an SMT solver.
SolverContext.ProverOptions	Options for the prover environment.
SolverContextFactory	Factory class for loading and generating solver contexts.
SolverContextFactory.Solvers
SolverException	Exception thrown if there is an error during SMT solving.
SolverOverviewTable	This program takes all installed solvers and checks them for version, theories and features and prints them to StdOut in a nice table.
SolverOverviewTable.RowBuilder	This class builds the table row-by-row.
SolverOverviewTable.SolverInfo	just a wrapper for some data.
SolverStackTest0
SolverStatistics
SolverUtils	Central entry point for all utility classes.
StatisticsEnumerationFormulaManager
StatisticsSolverContext
StringFormula	A formula of the string sort.
StringFormulaManager	Manager for dealing with string formulas.
Sudoku	This program parses user-given Sudoku and solves it with an SMT solver.
Sudoku.BooleanBasedSudokuSolver
Sudoku.EnumerationBasedSudokuSolver
Sudoku.IntegerBasedSudokuSolver
Sudoku.SudokuSolver<S>
SynchronizedEnumerationFormulaManager
SynchronizedSolverContext
Tactic	Tactic is a generic formula to formula transformation.
TimerPool
TimerPool.TimerWrapper	A minimal wrapper to keep a reference on the timer and provide a limited view.
Tokenizer	Helper class for splitting up an SMT-LIB2 file into a string of commands.
TraversalProcess	Return class that lets the visitor guide the recursive formula traversal process started with FormulaManager.visitRecursively(org.sosy_lab.java_smt.api.Formula, org.sosy_lab.java_smt.api.visitors.FormulaVisitor<org.sosy_lab.java_smt.api.visitors.TraversalProcess>).
TraversalProcess.TraversalType
UfElimination	UfElimination replaces UFs by fresh variables and adds constraints to enforce the functional consistency.
UfElimination.Result
UFManager	Manager for dealing with uninterpreted functions (UFs).
UserPropagator	Allows user-defined propagators (~ theory solvers) to be implemented.