@CheckReturnValue @ParametersAreNonnullByDefault @FieldsAreNonnullByDefault @ReturnValuesAreNonnullByDefault
Package org.sosy_lab.java_smt.basicimpl
Abstract base classes for easier implementation of a solver backend.
-
Class Summary 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 implementingFloatingPointFormulaManager.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 implementingNumeralFormulaManager.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 CachingModel 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.FunctionDeclarationImpl<F extends Formula,T> Declaration of a function.ShutdownHook A utility class for interrupting a parallel running solver thread.Tokenizer Helper class for splitting up an SMT-LIB2 file into a string of commands. -
Enum Summary Enum Description AbstractNumeralFormulaManager.NonLinearArithmetic