A B C D E F G H I L M N O P Q R S T U V W X Y Z
All Classes All Packages

A

ABORT - Static variable in class org.sosy_lab.java_smt.api.visitors.TraversalProcess

Immediately abort traversal and return to caller.

ABORT_TYPE - org.sosy_lab.java_smt.api.visitors.TraversalProcess.TraversalType

abs(FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

abs(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

abs(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

abs(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

AbstractArrayFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> - Class in org.sosy_lab.java_smt.basicimpl

AbstractArrayFormulaManager(FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl>) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager

AbstractBitvectorFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> - Class in org.sosy_lab.java_smt.basicimpl

AbstractBitvectorFormulaManager(FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl>, AbstractBooleanFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

AbstractBooleanFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> - Class in org.sosy_lab.java_smt.basicimpl

AbstractBooleanFormulaManager(FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl>) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

AbstractEnumerationFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> - Class in org.sosy_lab.java_smt.basicimpl

AbstractEnumerationFormulaManager(FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl>) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager

AbstractEnumerationFormulaManager.EnumType - Class in org.sosy_lab.java_smt.basicimpl

The class 'EnumType' is just a plain internal value-holding class.

AbstractEvaluator<TFormulaInfo,TType,TEnv> - Class in org.sosy_lab.java_smt.basicimpl

AbstractEvaluator(AbstractProver<?>, FormulaCreator<TFormulaInfo, TType, TEnv, ?>) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

AbstractFloatingPointFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> - Class in org.sosy_lab.java_smt.basicimpl

Similar to the other Abstract*FormulaManager classes in this package, this class serves as a helper for implementing FloatingPointFormulaManager.

AbstractFloatingPointFormulaManager(FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl>) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

AbstractFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> - Class in org.sosy_lab.java_smt.basicimpl

Simplifies building a solver from the specific theories.

AbstractFormulaManager(FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl>, AbstractUFManager<TFormulaInfo, ?, TType, TEnv>, AbstractBooleanFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>, IntegerFormulaManager, RationalFormulaManager, AbstractBitvectorFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>, AbstractFloatingPointFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>, AbstractQuantifiedFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>, AbstractArrayFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>, AbstractSLFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>, AbstractStringFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>, AbstractEnumerationFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

Builds a solver from the given theory implementations.

AbstractModel<TFormulaInfo,TType,TEnv> - Class in org.sosy_lab.java_smt.basicimpl

AbstractModel(AbstractProver<?>, FormulaCreator<TFormulaInfo, TType, TEnv, ?>) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractModel

AbstractNumeralFormulaManager<TFormulaInfo,TType,TEnv,ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula,TFuncDecl> - Class in org.sosy_lab.java_smt.basicimpl

Similar to the other Abstract*FormulaManager classes in this package, this class serves as a helper for implementing NumeralFormulaManager.

AbstractNumeralFormulaManager(FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl>, AbstractNumeralFormulaManager.NonLinearArithmetic) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

AbstractNumeralFormulaManager.NonLinearArithmetic - Enum in org.sosy_lab.java_smt.basicimpl

AbstractProver<T> - Class in org.sosy_lab.java_smt.basicimpl

AbstractProver(Set<SolverContext.ProverOptions>) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractProver

AbstractProverWithAllSat<T> - Class in org.sosy_lab.java_smt.basicimpl

This class is a utility-class to avoid repeated implementation of the AllSAT computation.

AbstractProverWithAllSat(Set<SolverContext.ProverOptions>, BooleanFormulaManager, ShutdownNotifier) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat

AbstractQuantifiedFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> - Class in org.sosy_lab.java_smt.basicimpl

AbstractQuantifiedFormulaManager(FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl>) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager

AbstractSLFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> - Class in org.sosy_lab.java_smt.basicimpl

AbstractSLFormulaManager(FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl>) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager

AbstractSolverContext - Class in org.sosy_lab.java_smt.basicimpl

AbstractSolverContext(FormulaManager) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractSolverContext

AbstractStringFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> - Class in org.sosy_lab.java_smt.basicimpl

AbstractStringFormulaManager(FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl>) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

AbstractUFManager<TFormulaInfo,TFunctionDecl,TType,TEnv> - Class in org.sosy_lab.java_smt.basicimpl

This class simplifies the implementation of the FunctionFormulaManager by converting the types to the solver specific type.

AbstractUFManager(FormulaCreator<TFormulaInfo, TType, TEnv, TFunctionDecl>) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractUFManager

AbstractUserPropagator - Class in org.sosy_lab.java_smt.basicimpl

AbstractUserPropagator() - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator

ACKERMANNIZATION - org.sosy_lab.java_smt.api.Tactic

Replaces all applications of UFs with fresh variables and adds constraints to enforce the functional consistency.

add(BitvectorFormula, BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns the addition of the given bitvectors.

add(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

add(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

add(FloatingPointFormula, FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

add(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

add(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

add(FloatingPointFormula, FloatingPointFormula, FloatingPointRoundingMode) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

add(FloatingPointFormula, FloatingPointFormula, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

add(FloatingPointFormula, FloatingPointFormula, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

add(ParamFormulaType, ParamFormulaType) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

add(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

add(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

add(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

add(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

add(TFormulaInfo, TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

ADD - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Addition over integers and rationals.

addConstraint(BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Add a constraint to the latest backtracking point.

addConstraint(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

addConstraint(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

addConstraintImpl(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

addFunctionDeclaration(FunctionDeclaration<?>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverInformation

Needs to be called after a new function is declared to associate it with this context.

addSolver(SolverOverviewTable.SolverInfo) - Method in class org.sosy_lab.java_smt.example.SolverOverviewTable.RowBuilder

Takes a SolverInfo object and splits it into multiple lines which are added to the row.

all() - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Note: The size of the used alphabet depends on the underlying SMT solver.

all() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

all() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

allChar() - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Note: The size of the used alphabet depends on the underlying SMT solver.

allChar() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

allChar() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

allCharImpl() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

allImpl() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

allSat(BasicProverEnvironment.AllSatCallback<R>, List<BooleanFormula>) - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Get all satisfying assignments of the current environment with regard to a subset of terms, and create a region representing all those models.

allSat(BasicProverEnvironment.AllSatCallback<R>, List<BooleanFormula>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat

allSat(BasicProverEnvironment.AllSatCallback<R>, List<BooleanFormula>) - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

AllSatExample - Class in org.sosy_lab.java_smt.example

This example shows different ways to get all satisfiable models for a given set of constraints.

AllSatExample(SolverContext, ProverEnvironment) - Constructor for class org.sosy_lab.java_smt.example.AllSatExample

amgr - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

and(Collection<BooleanFormula>) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

and(Collection<BooleanFormula>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

and(Collection<BooleanFormula>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

and(BitvectorFormula, BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns the bit-wise AND of the given bitvectors.

and(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

and(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

and(BooleanFormula...) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

and(BooleanFormula, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Creates a formula representing an AND of the two arguments.

and(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

and(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

and(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

and(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

AND - org.sosy_lab.java_smt.api.FunctionDeclarationKind

andImpl(Collection<TFormulaInfo>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

Create an n-ary conjunction.

apply(List<BooleanFormula>) - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment.AllSatCallback

Callback for each possible satisfying assignment to given important predicates.

applyCNFImpl(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

Apply conjunctive normal form (CNF) transformation to the given input formula.

applyNNFImpl(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

Apply negation normal form (NNF) transformation to the given input formula.

applyQELightImpl(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

Eliminate quantifiers from the given input formula.

applyTactic(BooleanFormula, Tactic) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Apply a tactic which performs formula transformation.

applyTactic(BooleanFormula, Tactic) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

applyTactic(BooleanFormula, Tactic) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

applyUFEImpl(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

Eliminate UFs from the given input formula.

APPROXIMATE_ALWAYS - org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic

APPROXIMATE_FALLBACK - org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic

ArrayFormula<TI extends Formula,TE extends Formula> - Interface in org.sosy_lab.java_smt.api

A formula of the array sort.

ArrayFormulaManager - Interface in org.sosy_lab.java_smt.api

This interface represents the theory of (arbitrarily nested) arrays.

asList() - Method in interface org.sosy_lab.java_smt.api.Model

Build a list of assignments that stays valid after closing the model.

asList() - Method in class org.sosy_lab.java_smt.basicimpl.CachingModel

asList() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingModel

asMap() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

assertThat(BasicProverEnvironment<?>) - Static method in class org.sosy_lab.java_smt.test.ProverEnvironmentSubject

Use this for checking assertions about ProverEnvironments with Truth: assertThat(stack).is...().

assertThatEnvironment(BasicProverEnvironment<?>) - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

Use this for checking assertions about ProverEnvironments with Truth: assertThatEnvironment(stack).is...().

assertThatFormula(BooleanFormula) - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

Use this for checking assertions about BooleanFormulas with Truth: assertThatFormula(formula).is...().

assertUsing(SolverContext) - Static method in class org.sosy_lab.java_smt.test.BooleanFormulaSubject

Use this for checking assertions about BooleanFormulas (given the corresponding solver) with Truth: assertUsing(context)).that(formula).is...().

assignment(FloatingPointFormula, FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Create a term for assigning one floating-point term to another.

assignment(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

assignment(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

assignment(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

avoidDualStacksIfNotSupported() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

B

BASIC_OPERATORS - Static variable in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

Avoid using basic mathematical or logical operators of SMT-LIB2 as names for symbols.

BasicProverEnvironment<T> - Interface in org.sosy_lab.java_smt.api

Super interface for ProverEnvironment and InterpolatingProverEnvironment that provides only the common operations.

BasicProverEnvironment.AllSatCallback<R> - Interface in org.sosy_lab.java_smt.api

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>> - Class in org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper

Binoxxo - Class in org.sosy_lab.java_smt.example

This program parses a user-given Binoxxo and solves it with an SMT solver.

Binoxxo.BinoxxoSolver<S> - Class in org.sosy_lab.java_smt.example

Binoxxo.BooleanBasedBinoxxoSolver - Class in org.sosy_lab.java_smt.example

This solver encodes nore steps into boolean logic, which makes it about 10x faster than the Binoxxo.IntegerBasedBinoxxoSolver.

Binoxxo.IntegerBasedBinoxxoSolver - Class in org.sosy_lab.java_smt.example

BitvectorFormula - Interface in org.sosy_lab.java_smt.api

A formula of the bitvector sort.

BitvectorFormulaManager - Interface in org.sosy_lab.java_smt.api

Manager for dealing with formulas of the bitvector sort.

BITWUZLA - org.sosy_lab.java_smt.SolverContextFactory.Solvers

bmgr - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

BooleanBasedBinoxxoSolver(SolverContext) - Constructor for class org.sosy_lab.java_smt.example.Binoxxo.BooleanBasedBinoxxoSolver

BooleanBasedSudokuSolver(SolverContext) - Constructor for class org.sosy_lab.java_smt.example.Sudoku.BooleanBasedSudokuSolver

BooleanFormula - Interface in org.sosy_lab.java_smt.api

A formula of the boolean sort.

BooleanFormulaManager - Interface in org.sosy_lab.java_smt.api

Manager for dealing with boolean formulas.

booleanFormulasOf(SolverContext) - Static method in class org.sosy_lab.java_smt.test.BooleanFormulaSubject

Use this for checking assertions about BooleanFormulas (given the corresponding solver) with Truth: assert_().about(booleanFormulasOf(context)).that(formula).is...().

BooleanFormulaSubject - Class in org.sosy_lab.java_smt.test

Subject subclass for testing assertions about BooleanFormulas with Truth (allows using assert_().about(...).that(formula).isUnsatisfiable() etc.).

BooleanFormulaTransformationVisitor - Class in org.sosy_lab.java_smt.api.visitors

Base class for visitors for boolean formulas that recursively transform boolean formulas.

BooleanFormulaTransformationVisitor(FormulaManager) - Constructor for class org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor

BooleanFormulaVisitor<R> - Interface in org.sosy_lab.java_smt.api.visitors

Visitor iterating through the boolean part of the formula.

BooleanType - Static variable in class org.sosy_lab.java_smt.api.FormulaType

BOOLECTOR - org.sosy_lab.java_smt.SolverContextFactory.Solvers

BV_ADD - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Addition over bitvectors.

BV_AND - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Bitwise AND over bitvectors.

BV_ASHR - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Arithmetic right-shift over bitvectors (fill from left with value of first bit).

BV_CONCAT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Concatenation over bitvectors.

BV_EQ - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Equality over bitvectors.

BV_EXTRACT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Extraction over bitvectors.

BV_LSHR - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Logical right-shift over bitvectors (fill from left with zeroes).

BV_MUL - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Multiplication over bitvectors.

BV_NEG - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Negation of a bitvector.

BV_NOT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Bitwise negation of a bitvector.

BV_OR - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Bitwise OR over bitvectors.

BV_ROTATE_LEFT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Performs a circular left rotation on the bitvector.

BV_ROTATE_LEFT_BY_INT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Performs a circular left rotation on the bitvector by a specified number of positions, determined by an integer value.

BV_ROTATE_RIGHT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Performs a circular right rotation on the bitvector.

BV_ROTATE_RIGHT_BY_INT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Performs a circular right rotation on the bitvector by a specified number of positions, determined by an integer value.

BV_SCASTTO_FP - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Cast a signed bitvector to a floating-point number.

BV_SDIV - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Signed division over bitvectors.

BV_SGE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Signed greater-than-or-equal over bitvectors.

BV_SGT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Unsigned greater-than over bitvectors.

BV_SHL - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Logical left-shift over bitvectors (fill from right with zeroes).

BV_SIGN_EXTENSION - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Extend bitvectors according to their sign.

BV_SLE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Signed greater-than-or-equal over bitvectors.

BV_SLT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Unsigned less-than over bitvectors.

BV_SMOD - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Signed modulo over bitvectors.

BV_SREM - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Signed remainder over bitvectors.

BV_SUB - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Subtraction over bitvectors.

BV_UCASTTO_FP - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Cast an unsigned bitvector to a floating-point number.

BV_UDIV - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Unsigned division over bitvectors.

BV_UGE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Unsigned greater-than-or-equal over bitvectors.

BV_UGT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Signed greater-than over bitvectors.

BV_ULE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Unsigned less-than-or-equal over bitvectors.

BV_ULT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Signed less-than over bitvectors.

BV_UREM - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Unsigned remainder over bitvectors.

BV_XOR - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Bitwise XOR over bitvectors.

BV_ZERO_EXTENSION - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Extend bitvectors with zeros.

bvmgr - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

C

CachingModel - Class in org.sosy_lab.java_smt.basicimpl

CachingModel(Model) - Constructor for class org.sosy_lab.java_smt.basicimpl.CachingModel

callFunction(FunctionDeclaration<T>, List<? extends Formula>) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

callFunctionImpl(TFuncDecl, List<TFormulaInfo>) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

callUF(FunctionDeclaration<T>, List<? extends Formula>) - Method in interface org.sosy_lab.java_smt.api.UFManager

Create an uninterpreted function call.

callUF(FunctionDeclaration<T>, List<? extends Formula>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractUFManager

callUF(FunctionDeclaration<T>, List<? extends Formula>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingUFManager

callUF(FunctionDeclaration<T>, Formula...) - Method in interface org.sosy_lab.java_smt.api.UFManager

castFrom(Formula, boolean, FormulaType.FloatingPointType) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Build a FloatingPointFormula from another compatible formula.

castFrom(Formula, boolean, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

castFrom(Formula, boolean, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

castFrom(Formula, boolean, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Build a FloatingPointFormula from another compatible formula.

castFrom(Formula, boolean, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

castFrom(Formula, boolean, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

castFromImpl(TFormulaInfo, boolean, FormulaType.FloatingPointType, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

castTo(FloatingPointFormula, boolean, FormulaType<T>) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Build a formula of compatible type from a FloatingPointFormula.

castTo(FloatingPointFormula, boolean, FormulaType<T>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

castTo(FloatingPointFormula, boolean, FormulaType<T>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

castTo(FloatingPointFormula, boolean, FormulaType<T>, FloatingPointRoundingMode) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Build a formula of compatible type from a FloatingPointFormula.

castTo(FloatingPointFormula, boolean, FormulaType<T>, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

castTo(FloatingPointFormula, boolean, FormulaType<T>, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

castTo(FloatingPointFormula, FormulaType<T>) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Deprecated, for removal: This API element is subject to removal in a future version.

castTo(FloatingPointFormula, FormulaType<T>, FloatingPointRoundingMode) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Deprecated, for removal: This API element is subject to removal in a future version.

castToImpl(TFormulaInfo, boolean, FormulaType<?>, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

charAt(StringFormula, NumeralFormula.IntegerFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Get a substring of length 1 from the given String if the given index is within bounds.

charAt(StringFormula, NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

charAt(StringFormula, NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

charAt(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

check() - Method in interface org.sosy_lab.java_smt.api.OptimizationProverEnvironment

Optimize the objective function subject to the previously imposed constraints.

check() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingOptimizationProverEnvironment

checkEnableSeparationLogic() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

checkGenerateAllSat() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

checkGenerateModels() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

checkGenerateUnsatCores() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

checkGenerateUnsatCoresOverAssumptions() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

checkTreeStructure(int, int[]) - Static method in interface org.sosy_lab.java_smt.api.InterpolatingProverEnvironment

Checks for a valid subtree-structure.

checkVariableName(String) - Static method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

This method is similar to AbstractFormulaManager.isValidName(java.lang.String) and throws an exception for invalid symbol names.

clearAssumptions() - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

clearAssumptions() - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper

close() - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Closes the prover environment.

close() - Method in interface org.sosy_lab.java_smt.api.Evaluator

Free resources associated with this evaluator (existing Formula instances stay valid, but Evaluator.evaluate(Formula) etc.

close() - Method in interface org.sosy_lab.java_smt.api.Model

Free resources associated with this model (existing Model.ValueAssignment instances stay valid, but Evaluator.evaluate(Formula) etc.

close() - Method in interface org.sosy_lab.java_smt.api.SolverContext

Close the solver context.

close() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

close() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

close() - Method in class org.sosy_lab.java_smt.basicimpl.CachingModel

close() - Method in class org.sosy_lab.java_smt.basicimpl.ShutdownHook

close() - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

close() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingModel

close() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverContext

close() - Method in class org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext

close() - Method in class org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext

close() - Method in class org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext

closeAllEvaluators() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

closed - Variable in class org.sosy_lab.java_smt.basicimpl.AbstractProver

closeSolver() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

closure(RegexFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

closure(RegexFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

closure(RegexFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

closure(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

complement(RegexFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

complement(RegexFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

complement(RegexFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

complement(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

concat(List<StringFormula>) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

concat(List<StringFormula>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

concat(List<StringFormula>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

concat(BitvectorFormula, BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Concatenate two bitvectors.

concat(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

concat(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

concat(RegexFormula...) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

concat(StringFormula...) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

concat(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

concatImpl(List<TFormulaInfo>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

concatRegex(List<RegexFormula>) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

concatRegex(List<RegexFormula>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

concatRegex(List<RegexFormula>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

concatRegexImpl(List<TFormulaInfo>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

config - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

CONST - org.sosy_lab.java_smt.api.FunctionDeclarationKind

constraintTestBool1() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

constraintTestBool2() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

constraintTestBool3() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

constraintTestBool4() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

contains(Formula) - Method in class org.sosy_lab.java_smt.api.visitors.TraversalProcess

contains(StringFormula, StringFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

contains(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

contains(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

contains(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

context - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

CONTINUE - Static variable in class org.sosy_lab.java_smt.api.visitors.TraversalProcess

Continue traversal and recurse into current formula subtree.

CONTINUE_TYPE - org.sosy_lab.java_smt.api.visitors.TraversalProcess.TraversalType

convertValue(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

Convert the formula into a Java object as far as possible, i.e., try to match a primitive or simple type like Boolean, BigInteger, Rational, or String.

convertValue(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

Convert the formula into a Java object as far as possible, i.e., try to match a primitive or simple type.

createSolverContext(Configuration, LogManager, ShutdownNotifier) - Static method in class org.sosy_lab.java_smt.SolverContextFactory

Shortcut for getting a SolverContext, the solver is selected using the configuration config.

createSolverContext(Configuration, LogManager, ShutdownNotifier, SolverContextFactory.Solvers) - Static method in class org.sosy_lab.java_smt.SolverContextFactory

Shortcut for getting a SolverContext, the solver is selected using an argument.

createSolverContext(Configuration, LogManager, ShutdownNotifier, SolverContextFactory.Solvers, Consumer<String>) - Static method in class org.sosy_lab.java_smt.SolverContextFactory

This is the most explicit method for getting a SolverContext, the solver, the logger, the shutdownNotifier, and the libraryLoader are provided as parameters by the caller.

createSolverContext(SolverContextFactory.Solvers) - Static method in class org.sosy_lab.java_smt.SolverContextFactory

Minimalistic shortcut for creating a solver context.

createTestConfigBuilder() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

creator - Variable in class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

cross(RegexFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

cross(RegexFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

cross(RegexFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

currentModel - Variable in class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator

custom(Iterable<? extends Formula>) - Static method in class org.sosy_lab.java_smt.api.visitors.TraversalProcess

Traverse only the given children.

custom(Formula) - Static method in class org.sosy_lab.java_smt.api.visitors.TraversalProcess

Traverse only the given child.

CUSTOM_TYPE - org.sosy_lab.java_smt.api.visitors.TraversalProcess.TraversalType

CVC4 - org.sosy_lab.java_smt.SolverContextFactory.Solvers

CVC5 - org.sosy_lab.java_smt.SolverContextFactory.Solvers

D

DebuggingArrayFormulaManager - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingBitvectorFormulaManager - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingBooleanFormulaManager - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingEnumerationFormulaManager - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingFloatingPointFormulaManager - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingFormulaManager - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingIntegerFormulaManager - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingInterpolatingProverEnvironment<T> - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingModel - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingNumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula> - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingOptimizationProverEnvironment - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingProverEnvironment - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingQuantifiedFormulaManager - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingRationalFormulaManager - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingSLFormulaManager - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingSolverContext - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingSolverContext(SolverContextFactory.Solvers, Configuration, SolverContext) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverContext

DebuggingSolverInformation - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingStringFormulaManager - Class in org.sosy_lab.java_smt.delegate.debugging

DebuggingUFManager - Class in org.sosy_lab.java_smt.delegate.debugging

decimalAsInteger(BigDecimal) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

This method tries to represent a BigDecimal using only BigInteger.

declareAndCallUF(String, FormulaType<T>, List<Formula>) - Method in interface org.sosy_lab.java_smt.api.UFManager

Declares and calls an uninterpreted function with exactly the given name.

declareAndCallUF(String, FormulaType<T>, List<Formula>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractUFManager

declareAndCallUF(String, FormulaType<T>, List<Formula>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingUFManager

declareAndCallUF(String, FormulaType<T>, Formula...) - Method in interface org.sosy_lab.java_smt.api.UFManager

declareAndCallUF(String, FormulaType<T>, Formula...) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractUFManager

declareAndCallUF(String, FormulaType<T>, Formula...) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingUFManager

declareEnumeration(String, String...) - Method in interface org.sosy_lab.java_smt.api.EnumerationFormulaManager

declareEnumeration(String, Set<String>) - Method in interface org.sosy_lab.java_smt.api.EnumerationFormulaManager

Declare an enumeration.

declareEnumeration(String, Set<String>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager

declareEnumeration(String, Set<String>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingEnumerationFormulaManager

declareEnumeration(String, Set<String>) - Method in class org.sosy_lab.java_smt.delegate.statistics.StatisticsEnumerationFormulaManager

declareEnumeration(String, Set<String>) - Method in class org.sosy_lab.java_smt.delegate.synchronize.SynchronizedEnumerationFormulaManager

declareEnumeration0(FormulaType.EnumerationFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager

declareEnumerationImpl(String, Set<String>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager

declareUF(String, FormulaType<T>, List<FormulaType<?>>) - Method in interface org.sosy_lab.java_smt.api.UFManager

Declare an uninterpreted function.

declareUF(String, FormulaType<T>, List<FormulaType<?>>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractUFManager

declareUF(String, FormulaType<T>, List<FormulaType<?>>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingUFManager

declareUF(String, FormulaType<T>, FormulaType<?>...) - Method in interface org.sosy_lab.java_smt.api.UFManager

Declare an uninterpreted function.

declareUFImpl(String, TType, List<TType>) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

DefaultBooleanFormulaVisitor<R> - Class in org.sosy_lab.java_smt.api.visitors

A formula visitor which allows for the default implementation.

DefaultBooleanFormulaVisitor() - Constructor for class org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor

DefaultFormulaVisitor<R> - Class in org.sosy_lab.java_smt.api.visitors

DefaultFormulaVisitor() - Constructor for class org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor

delegate - Variable in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

dequote(String) - Static method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

Variable names (symbols) can be wrapped with "|".

difference(RegexFormula, RegexFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

difference(RegexFormula, RegexFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

difference(RegexFormula, RegexFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

difference(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

DISALLOWED_CHARACTER_REPLACEMENT - Static variable in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

Mapping of disallowed char to their escaped counterparts.

distinct(List<BitvectorFormula>) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

All given bitvectors are pairwise unequal.

distinct(List<BitvectorFormula>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

distinct(List<BitvectorFormula>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

distinct(List<ParamFormulaType>) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

All given numbers are pairwise unequal.

distinct(List<ParamFormulaType>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

distinct(List<ParamFormulaType>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

distinct(BitvectorFormula...) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

DISTINCT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Distinct operator for a set of numeric formulas.

distinctImpl(List<TFormulaInfo>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

distinctImpl(List<TFormulaInfo>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

DIV - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Division over rationals and integer division over integers.

divide(BitvectorFormula, BitvectorFormula, boolean) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns the division for two bitvector formulas.

divide(BitvectorFormula, BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

divide(BitvectorFormula, BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

divide(FloatingPointFormula, FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

divide(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

divide(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

divide(FloatingPointFormula, FloatingPointFormula, FloatingPointRoundingMode) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

divide(FloatingPointFormula, FloatingPointFormula, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

divide(FloatingPointFormula, FloatingPointFormula, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

divide(ParamFormulaType, ParamFormulaType) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

Create a formula representing the division of two operands according to Boute's Euclidean definition (DOI: 10.1145/128861.128862).

divide(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

divide(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

divide(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

If a solver does not support this operation, e.g.

divide(TFormulaInfo, TFormulaInfo, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

divide(TFormulaInfo, TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

DOUBLE_PRECISION_EXPONENT_SIZE - Static variable in class org.sosy_lab.java_smt.api.FloatingPointNumber

Deprecated, for removal: This API element is subject to removal in a future version.

DOUBLE_PRECISION_MANTISSA_SIZE - Static variable in class org.sosy_lab.java_smt.api.FloatingPointNumber

Deprecated, for removal: This API element is subject to removal in a future version.

this constant can be confusing, as the SMTLIB2 standard expects the mantissa to include the hidden bit, but this constant does not.

DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT - Static variable in class org.sosy_lab.java_smt.api.FloatingPointNumber

doubleValue() - Method in class org.sosy_lab.java_smt.api.FloatingPointNumber

compute a representation as Java-based double value, if possible.

dualStackGlobalDeclarations() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

This test checks that an SMT solver uses "global declarations": regardless of the stack at declaration time, declarations always live for the full lifetime of the solver (i.e., they do not get deleted on pop()).

dualStackTest() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

dualStackTest2() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

dumpFormula(BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Serialize an input formula to an SMT-LIB format.

dumpFormula(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

dumpFormula(BooleanFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

dumpFormulaImpl(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

E

eliminateQuantifiers(BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.QuantifiedFormulaManager

Eliminate the quantifiers for a given formula.

eliminateQuantifiers(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager

eliminateQuantifiers(BooleanFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingQuantifiedFormulaManager

eliminateQuantifiers(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager

eliminateUfs(BooleanFormula) - Method in class org.sosy_lab.java_smt.utils.UfElimination

Applies the Ackermann transformation to the given Formula.

eliminateUfs(BooleanFormula, UfElimination.Result) - Method in class org.sosy_lab.java_smt.utils.UfElimination

Applies the Ackermann transformation to the given Formula with respect to the UfElimination.Result of another formula.

emgr - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

empty(FormulaManager) - Static method in class org.sosy_lab.java_smt.utils.UfElimination.Result

ENABLE_SEPARATION_LOGIC - org.sosy_lab.java_smt.api.SolverContext.ProverOptions

Whether the solver should enable support for formulae build in SL theory.

enableSL - Variable in class org.sosy_lab.java_smt.basicimpl.AbstractProver

encapsulate(FormulaType<T>, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

encapsulateArray(TFormulaInfo, FormulaType<TI>, FormulaType<TE>) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

encapsulateBitvector(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

encapsulateBoolean(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

encapsulateEnumeration(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

encapsulateFloatingPoint(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

encapsulateRegex(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

encapsulateString(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

encapsulateWithTypeOf(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

EnumerationBasedSudokuSolver(SolverContext) - Constructor for class org.sosy_lab.java_smt.example.Sudoku.EnumerationBasedSudokuSolver

EnumerationFormula - Interface in org.sosy_lab.java_smt.api

A formula of the enumeration sort.

EnumerationFormulaManager - Interface in org.sosy_lab.java_smt.api

This interface represents the theory of enumeration, i.e., datatype of limited domain sort (as defined in the SMTLIB2 standard).

enumerations - Variable in class org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager

EnumType(FormulaType.EnumerationFormulaType, TType, ImmutableMap<String, TFormulaInfo>) - Constructor for class org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager.EnumType

environment - Variable in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

EQ - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Equality over integers and rationals.

EQ_ZERO - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Unary comparison to zero.

equal(BitvectorFormula, BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns the bit-wise equality of the given bitvectors.

equal(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

equal(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

equal(StringFormula, StringFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

equal(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

equal(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

equal(ParamFormulaType, ParamFormulaType) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

equal(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

equal(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

equal(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

equal(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

equal(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

equals(Object) - Method in interface org.sosy_lab.java_smt.api.Formula

checks whether the other object is a formula of the same structure.

equals(Object) - Method in class org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType

equals(Object) - Method in class org.sosy_lab.java_smt.api.FormulaType.BitvectorType

equals(Object) - Method in class org.sosy_lab.java_smt.api.FormulaType.EnumerationFormulaType

equals(Object) - Method in class org.sosy_lab.java_smt.api.FormulaType.FloatingPointType

equals(Object) - Method in class org.sosy_lab.java_smt.api.Model.ValueAssignment

equalWithFPSemantics(FloatingPointFormula, FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Create a term for comparing the equality of two floating-point terms, according to standard floating-point semantics (i.e., NaN != NaN and 0.0 == -0.0).

equalWithFPSemantics(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

equalWithFPSemantics(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

equalWithFPSemantics(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

equivalence(ArrayFormula<TI, TE>, ArrayFormula<TI, TE>) - Method in interface org.sosy_lab.java_smt.api.ArrayFormulaManager

Make a BooleanFormula that represents the equality of two ArrayFormula.

equivalence(ArrayFormula<TI, TE>, ArrayFormula<TI, TE>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager

equivalence(ArrayFormula<TI, TE>, ArrayFormula<TI, TE>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingArrayFormulaManager

equivalence(BooleanFormula, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Creates a formula representing an equivalence of the two arguments.

equivalence(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

Creates a formula representing an equivalence of the two arguments.

equivalence(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

equivalence(EnumerationFormula, EnumerationFormula) - Method in interface org.sosy_lab.java_smt.api.EnumerationFormulaManager

Make a BooleanFormula that represents the equality of two EnumerationFormula of identical enumeration type.

equivalence(EnumerationFormula, EnumerationFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager

equivalence(EnumerationFormula, EnumerationFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingEnumerationFormulaManager

equivalence(EnumerationFormula, EnumerationFormula) - Method in class org.sosy_lab.java_smt.delegate.statistics.StatisticsEnumerationFormulaManager

equivalence(EnumerationFormula, EnumerationFormula) - Method in class org.sosy_lab.java_smt.delegate.synchronize.SynchronizedEnumerationFormulaManager

equivalence(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager

equivalence(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

equivalenceImpl(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager

escape(String) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Get an escaped symbol/name for variables or undefined functions, if necessary.

escape(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

escape(String) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

escapeUnicodeForSmtlib(String) - Static method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

Replace Unicode letters in UTF16 representation with their escape sequences.

eval(T) - Method in interface org.sosy_lab.java_smt.api.Evaluator

Evaluate a given formula substituting the values from the model and return it as formula.

eval(T) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

eval(T) - Method in class org.sosy_lab.java_smt.basicimpl.CachingModel

eval(T) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingModel

evalImpl(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

Simplify the given formula and replace all symbols with their model values.

evaluate(BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.Evaluator

Type-safe evaluation for bitvector formulas.

evaluate(BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

evaluate(BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.CachingModel

evaluate(BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingModel

evaluate(BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.Evaluator

Type-safe evaluation for boolean formulas.

evaluate(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

evaluate(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.CachingModel

evaluate(BooleanFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingModel

evaluate(EnumerationFormula) - Method in interface org.sosy_lab.java_smt.api.Evaluator

Type-safe evaluation for enumeration formulas.

evaluate(EnumerationFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

evaluate(EnumerationFormula) - Method in class org.sosy_lab.java_smt.basicimpl.CachingModel

evaluate(EnumerationFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingModel

evaluate(FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.Evaluator

Type-safe evaluation for floating-point formulas.

evaluate(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

evaluate(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.CachingModel

evaluate(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingModel

evaluate(Formula) - Method in interface org.sosy_lab.java_smt.api.Evaluator

Evaluate a given formula substituting the values from the model.

evaluate(Formula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

evaluate(Formula) - Method in class org.sosy_lab.java_smt.basicimpl.CachingModel

evaluate(Formula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingModel

evaluate(NumeralFormula.IntegerFormula) - Method in interface org.sosy_lab.java_smt.api.Evaluator

Type-safe evaluation for integer formulas.

evaluate(NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

evaluate(NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.basicimpl.CachingModel

evaluate(NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingModel

evaluate(NumeralFormula.RationalFormula) - Method in interface org.sosy_lab.java_smt.api.Evaluator

Type-safe evaluation for rational formulas.

evaluate(NumeralFormula.RationalFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

evaluate(NumeralFormula.RationalFormula) - Method in class org.sosy_lab.java_smt.basicimpl.CachingModel

evaluate(NumeralFormula.RationalFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingModel

evaluate(StringFormula) - Method in interface org.sosy_lab.java_smt.api.Evaluator

Type-safe evaluation for string formulas.

evaluate(StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

evaluate(StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.CachingModel

evaluate(StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingModel

evaluateImpl(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

Simplify the given formula and replace all symbols with their model values.

evaluateInModel(BooleanFormula, Formula, Collection<Object>, Collection<Formula>) - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

Evaluator - Interface in org.sosy_lab.java_smt.api

This class provides methods to get concrete evaluations for formulas from the satisfiable solver environment.

exists(List<? extends Formula>, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.QuantifiedFormulaManager

exists(Formula, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.QuantifiedFormulaManager

Syntax sugar, see QuantifiedFormulaManager.exists(List, BooleanFormula).

EXISTS - org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier

ExpectedFormulaVisitor<R> - Class in org.sosy_lab.java_smt.api.visitors

Like DefaultFormulaVisitor, but throws UnsupportedOperationException on unexpected formula types.

ExpectedFormulaVisitor() - Constructor for class org.sosy_lab.java_smt.api.visitors.ExpectedFormulaVisitor

extend(BitvectorFormula, int, boolean) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Extend a bitvector to the left (add most significant bits).

extend(BitvectorFormula, int, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

extend(BitvectorFormula, int, boolean) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

extend(TFormulaInfo, int, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

extract(BitvectorFormula, int, int) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Extract a range of bits from a bitvector.

extract(BitvectorFormula, int, int) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

extract(BitvectorFormula, int, int) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

extract(BitvectorFormula, int, int, boolean) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Deprecated, for removal: This API element is subject to removal in a future version.

extract(TFormulaInfo, int, int) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

extractInfo(List<? extends Formula>) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

extractInfo(Formula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

extractInfo(Formula) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

extractVariables(Formula) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Extract the names of all free variables and UFs in a formula.

extractVariables(Formula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

Extract names of all free variables in a formula.

extractVariables(Formula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

extractVariablesAndUFs(Formula) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Extract the names of all free variables and UFs in a formula.

extractVariablesAndUFs(Formula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

Extract the names of all free variables and UFs in a formula.

extractVariablesAndUFs(Formula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

extractVariablesAndUFs(Formula, boolean, BiConsumer<String, Formula>) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

Extract all free variables from the formula, optionally including UFs.

extractVariablesAndUFs(TFormulaInfo, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

Wrapper for FormulaCreator.extractVariablesAndUFs(Formula, boolean, BiConsumer) which unwraps both input and output.

extractVariablesAndUFs(TFormulaInfo, boolean, BiConsumer<String, TFormulaInfo>) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

Wrapper for FormulaCreator.extractVariablesAndUFs(Formula, boolean, BiConsumer) which unwraps both input and output.

F

factory - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

fixedCount - Variable in class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator

fixedVariables - Variable in class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator

FloatingPointFormula - Interface in org.sosy_lab.java_smt.api

Formula of the floating point sort.

FloatingPointFormulaManager - Interface in org.sosy_lab.java_smt.api

Floating point operations.

FloatingPointNumber - Class in org.sosy_lab.java_smt.api

Represents a floating-point number with customizable precision, consisting of sign, exponent, and mantissa components.

FloatingPointNumber() - Constructor for class org.sosy_lab.java_smt.api.FloatingPointNumber

FloatingPointNumber.Sign - Enum in org.sosy_lab.java_smt.api

FloatingPointRoundingMode - Enum in org.sosy_lab.java_smt.api

Possible floating point rounding modes.

FloatingPointRoundingModeFormula - Interface in org.sosy_lab.java_smt.api

Formula representing a rounding mode for floating-point operations.

FloatingPointRoundingModeType - Static variable in class org.sosy_lab.java_smt.api.FormulaType

floatValue() - Method in class org.sosy_lab.java_smt.api.FloatingPointNumber

compute a representation as Java-based float value, if possible.

floor(ParamFormulaType) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

The floor operation returns the nearest integer formula that is less or equal to the given argument formula.

floor(ParamFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

floor(ParamFormulaType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

floor(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

FLOOR - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Floor operation, converts from rationals to integers, also known as to_int.

fmgr - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

forall(List<? extends Formula>, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.QuantifiedFormulaManager

forall(Formula, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.QuantifiedFormulaManager

Syntax sugar, see QuantifiedFormulaManager.forall(List, BooleanFormula).

FORALL - org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier

Formula - Interface in org.sosy_lab.java_smt.api

An arbitrary SMT formula.

FormulaClassifier - Class in org.sosy_lab.java_smt.example

This program parses user-given formulas and prints out the (minimal) matching theory for them.

FormulaClassifier(SolverContext) - Constructor for class org.sosy_lab.java_smt.example.FormulaClassifier

FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> - Class in org.sosy_lab.java_smt.basicimpl

This is a helper class with several methods that are commonly used throughout the basicimpl package and may have solver-specific implementations.

FormulaCreator(TEnv, TType, TType, TType, TType, TType) - Constructor for class org.sosy_lab.java_smt.basicimpl.FormulaCreator

FormulaManager - Interface in org.sosy_lab.java_smt.api

FormulaManager class contains all operations which can be performed on formulas.

formulaToDot(Formula, PrettyPrinter.PrinterOption...) - Method in class org.sosy_lab.java_smt.utils.PrettyPrinter

This method returns a Graphviz/Dot representation of the given formula.

formulaToString(Formula, PrettyPrinter.PrinterOption...) - Method in class org.sosy_lab.java_smt.utils.PrettyPrinter

This method returns a multi-line String with pretty-formatted and indented subformulas.

FormulaTransformationVisitor - Class in org.sosy_lab.java_smt.api.visitors

Abstract class for formula transformation.

FormulaTransformationVisitor(FormulaManager) - Constructor for class org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor

FormulaType<T extends Formula> - Class in org.sosy_lab.java_smt.api

Type of a formula.

FormulaType.ArrayFormulaType<TI extends Formula,TE extends Formula> - Class in org.sosy_lab.java_smt.api

FormulaType.BitvectorType - Class in org.sosy_lab.java_smt.api

FormulaType.EnumerationFormulaType - Class in org.sosy_lab.java_smt.api

FormulaType.FloatingPointType - Class in org.sosy_lab.java_smt.api

FormulaType.NumeralType<T extends NumeralFormula> - Class in org.sosy_lab.java_smt.api

FormulaVisitor<R> - Interface in org.sosy_lab.java_smt.api.visitors

Visitor iterating through entire formula.

FP_ABS - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Absolute value of a floating point.

FP_ADD - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Addition over floating points.

FP_AS_IEEEBV - org.sosy_lab.java_smt.api.FunctionDeclarationKind

FP_CASTTO_FP - org.sosy_lab.java_smt.api.FunctionDeclarationKind

FP_CASTTO_SBV - org.sosy_lab.java_smt.api.FunctionDeclarationKind

FP_CASTTO_UBV - org.sosy_lab.java_smt.api.FunctionDeclarationKind

FP_DIV - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Division over floating points.

FP_EQ - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Equal over floating points.

FP_FROM_IEEEBV - org.sosy_lab.java_smt.api.FunctionDeclarationKind

FP_GE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Greater-than-or-equal over floating points.

FP_GT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Greater-than over floating points.

FP_IS_INF - org.sosy_lab.java_smt.api.FunctionDeclarationKind

FP_IS_NAN - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Further FP queries.

FP_IS_NEGATIVE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

FP_IS_NORMAL - org.sosy_lab.java_smt.api.FunctionDeclarationKind

FP_IS_SUBNORMAL - org.sosy_lab.java_smt.api.FunctionDeclarationKind

FP_IS_ZERO - org.sosy_lab.java_smt.api.FunctionDeclarationKind

FP_LE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Less-than-or-equal over floating points.

FP_LT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Less-than over floating points.

FP_MAX - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Maximum of two floating points.

FP_MIN - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Minimum of two floating points.

FP_MUL - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Multiplication over floating points.

FP_NEG - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Negation of a floating point.

FP_REM - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Remainder of the floating point division.

FP_ROUND_AWAY - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Rounding over floating points.

FP_ROUND_EVEN - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Rounding over floating points.

FP_ROUND_NEGATIVE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Rounding over floating points.

FP_ROUND_POSITIVE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Rounding over floating points.

FP_ROUND_TO_INTEGRAL - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Rounding over floating points.

FP_ROUND_ZERO - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Rounding over floating points.

FP_SQRT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Square root of a floating point.

FP_SUB - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Subtraction over floating points.

fpmgr - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

fromCodePoint(NumeralFormula.IntegerFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Returns a String formula representing the single character with the given code point, if it is a valid Unicode code point within the Basic Multilingual Plane (BMP) or planes 1 and 2 (codepoints in range [0x00000, 0x2FFFF]).

fromCodePoint(NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

fromCodePoint(NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

fromCodePoint(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

fromIeeeBitvector(BitvectorFormula, FormulaType.FloatingPointType) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Create a formula that interprets the given bitvector as a floating-point value in the IEEE format, according to the given type.

fromIeeeBitvector(BitvectorFormula, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

fromIeeeBitvector(BitvectorFormula, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

fromIeeeBitvectorImpl(TFormulaInfo, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

fromString(String) - Static method in class org.sosy_lab.java_smt.api.FormulaType

Parse a string and return the corresponding type.

FunctionDeclaration<E extends Formula> - Interface in org.sosy_lab.java_smt.api

Function declaration, for both UFs and built-in functions (theory and boolean).

FunctionDeclarationImpl<F extends Formula,T> - Class in org.sosy_lab.java_smt.basicimpl

Declaration of a function.

FunctionDeclarationImpl() - Constructor for class org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl

FunctionDeclarationKind - Enum in org.sosy_lab.java_smt.api

Types of function declarations.

G

GENERATE_ALL_SAT - org.sosy_lab.java_smt.api.SolverContext.ProverOptions

Whether the solver should allow to query all satisfying assignments for satisfiable formulas.

GENERATE_MODELS - org.sosy_lab.java_smt.api.SolverContext.ProverOptions

Whether the solver should generate models (i.e., satisfying assignments) for satisfiable formulas.

GENERATE_UNSAT_CORE - org.sosy_lab.java_smt.api.SolverContext.ProverOptions

Whether the solver should generate an unsat core for unsatisfiable formulas.

GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS - org.sosy_lab.java_smt.api.SolverContext.ProverOptions

Whether the solver should generate an unsat core for unsatisfiable formulas only over the assumptions explicitly passed to the solver.

generateContext() - Method in class org.sosy_lab.java_smt.SolverContextFactory

Create new context with solver chosen according to the supplied configuration.

generateContext(SolverContextFactory.Solvers) - Method in class org.sosy_lab.java_smt.SolverContextFactory

Create new context with solver name supplied.

generateUnsatCores - Variable in class org.sosy_lab.java_smt.basicimpl.AbstractProver

getAllSolvers() - Static method in class org.sosy_lab.java_smt.test.SolverBasedTest0.ParameterizedSolverBasedTest0

getArgInterpretation(int) - Method in class org.sosy_lab.java_smt.api.Model.ValueAssignment

getArgumentsInterpretation() - Method in class org.sosy_lab.java_smt.api.Model.ValueAssignment

Interpretation assigned for function arguments.

getArgumentTypes() - Method in interface org.sosy_lab.java_smt.api.FunctionDeclaration

getArity() - Method in class org.sosy_lab.java_smt.api.Model.ValueAssignment

getArrayFormulaElementType(ArrayFormula<TI, TE>) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

getArrayFormulaIndexType(ArrayFormula<TI, TE>) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

getArrayFormulaManager() - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Returns the Array-Theory.

getArrayFormulaManager() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

getArrayFormulaManager() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

getArrayType(FormulaType<TD>, FormulaType<TR>) - Static method in class org.sosy_lab.java_smt.api.FormulaType

getArrayType(TType, TType) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

getAssertedConstraintIds() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

getAssertedFormulas() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

getAssignmentAsFormula() - Method in class org.sosy_lab.java_smt.api.Model.ValueAssignment

The formula AST representing the equality of key and value.

getBackend() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator

getBitvectorFormulaManager() - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Returns the Bitvector-Theory.

getBitvectorFormulaManager() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

getBitvectorFormulaManager() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

getBitvectorType(int) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

getBitvectorTypeWithSize(int) - Static method in class org.sosy_lab.java_smt.api.FormulaType

getBooleanFormulaManager() - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Returns the Boolean-Theory.

getBooleanFormulaManager() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

getBooleanFormulaManager() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

getBooleanVarDeclaration(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

getBooleanVarDeclarationImpl(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

getBoolType() - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

getBvRepresentation(BigInteger, int) - Static method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

getCardinality() - Method in class org.sosy_lab.java_smt.api.FormulaType.EnumerationFormulaType

getConstraints() - Method in class org.sosy_lab.java_smt.utils.UfElimination.Result

getDefaultRoundingMode() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

getDoublePrecisionFloatingPointType() - Static method in class org.sosy_lab.java_smt.api.FormulaType

getElements() - Method in class org.sosy_lab.java_smt.api.FormulaType.EnumerationFormulaType

getElementType() - Method in class org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType

getElementType(ArrayFormula<?, TE>) - Method in interface org.sosy_lab.java_smt.api.ArrayFormulaManager

getElementType(ArrayFormula<?, TE>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager

getElementType(ArrayFormula<?, TE>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingArrayFormulaManager

getEnumerationFormulaManager() - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Returns the Enumeration Theory, e.g., also known as 'limited domain'.

getEnumerationFormulaManager() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

getEnumerationFormulaManager() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

getEnumerationFormulaType() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager.EnumType

getEnumerationType(String, Set<String>) - Static method in class org.sosy_lab.java_smt.api.FormulaType

getEnv() - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

getEnvironment() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

getEvaluator() - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Get a temporary view on the current satisfying assignment.

getEvaluatorWithoutChecks() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat

Get an evaluator instance for model evaluation without executing checks for prover options.

getExponent() - Method in class org.sosy_lab.java_smt.api.FloatingPointNumber

The exponent of the floating-point number, given as numeric value from binary representation.

getExponentSize() - Method in class org.sosy_lab.java_smt.api.FloatingPointNumber

getExponentSize() - Method in class org.sosy_lab.java_smt.api.FormulaType.FloatingPointType

Returns the size of the exponent.

getFeatures() - Method in class org.sosy_lab.java_smt.example.SolverOverviewTable.SolverInfo

getFloatingPointFormulaManager() - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Returns the Floating-Point-Theory.

getFloatingPointFormulaManager() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

getFloatingPointFormulaManager() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

getFloatingPointType(int, int) - Static method in class org.sosy_lab.java_smt.api.FormulaType

Deprecated, for removal: This API element is subject to removal in a future version.

this method can be confusing, as the SMTLIB2 standard expects the mantissa to include the hidden bit, but this method expects the mantissa argument without the hidden bit. Use FormulaType.getFloatingPointTypeFromSizesWithoutHiddenBit(int, int) instead if you want to construct a FormulaType.FloatingPointType with the constructing method treating the mantissa argument without the hidden bit, and FormulaType.getFloatingPointTypeFromSizesWithHiddenBit(int, int) if you want it to include the hidden bit in the size of the mantissa argument.

getFloatingPointType(FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

getFloatingPointTypeFromSizesWithHiddenBit(int, int) - Static method in class org.sosy_lab.java_smt.api.FormulaType

Constructs a new IEEE-754 FormulaType.FloatingPointType with the given exponent and mantissa sizes.

getFloatingPointTypeFromSizesWithoutHiddenBit(int, int) - Static method in class org.sosy_lab.java_smt.api.FormulaType

Constructs a new IEEE-754 FormulaType.FloatingPointType with the given exponent and mantissa sizes.

getFormula() - Method in class org.sosy_lab.java_smt.utils.UfElimination.Result

getFormulaCreator() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

getFormulaManager() - Method in interface org.sosy_lab.java_smt.api.SolverContext

Get the formula manager, which is used for formula manipulation.

getFormulaManager() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSolverContext

getFormulaManager() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverContext

getFormulaManager() - Method in class org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext

getFormulaManager() - Method in class org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext

getFormulaManager() - Method in class org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext

getFormulaType() - Method in interface org.sosy_lab.java_smt.api.IntegerFormulaManager

getFormulaType() - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

getFormulaType() - Method in interface org.sosy_lab.java_smt.api.RationalFormulaManager

getFormulaType() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

getFormulaType(T) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Returns the type of the given Formula.

getFormulaType(T) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

getFormulaType(T) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

Returns the type of the given Formula.

getFormulaType(T) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

getFormulaType(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

getGlobalFunctionsForSolver(SolverContextFactory.Solvers) - Static method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverInformation

getGlobalTermsForSolver(SolverContextFactory.Solvers) - Static method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverInformation

getIndexType() - Method in class org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType

getIndexType(ArrayFormula<TI, ?>) - Method in interface org.sosy_lab.java_smt.api.ArrayFormulaManager

getIndexType(ArrayFormula<TI, ?>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager

getIndexType(ArrayFormula<TI, ?>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingArrayFormulaManager

getIntegerFormulaManager() - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Returns the Integer-Theory.

getIntegerFormulaManager() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

getIntegerFormulaManager() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

getIntegerType() - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

getInterpolant(Collection<T>) - Method in interface org.sosy_lab.java_smt.api.InterpolatingProverEnvironment

Get an interpolant for two groups of formulas.

getInterpolant(Collection<T>) - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper

getInterpolant(Collection<T>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingInterpolatingProverEnvironment

getKey() - Method in class org.sosy_lab.java_smt.api.Model.ValueAssignment

The formula AST which is assigned a given value.

getKind() - Method in interface org.sosy_lab.java_smt.api.FunctionDeclaration

getLength(BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns the length of a bitvector, also denoted as bit-size.

getLength(BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

getLength(BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

getMantissa() - Method in class org.sosy_lab.java_smt.api.FloatingPointNumber

The mantissa (aka significand) of the floating-point number, given as numeric value from binary representation.

getMantissaSize() - Method in class org.sosy_lab.java_smt.api.FloatingPointNumber

Deprecated, for removal: This API element is subject to removal in a future version.

this method can be confusing, as the SMTLIB2 standard expects the mantissa to include the hidden bit, but this does not. Use FloatingPointNumber.getMantissaSizeWithoutHiddenBit() instead if you want the mantissa without the hidden bit, and FloatingPointNumber.getMantissaSizeWithHiddenBit() if you want it to include the hidden bit.

getMantissaSize() - Method in class org.sosy_lab.java_smt.api.FormulaType.FloatingPointType

Deprecated, for removal: This API element is subject to removal in a future version.

this method can be confusing, as the SMTLIB2 standard expects the mantissa to include the hidden bit, but this does not. Use FormulaType.FloatingPointType.getMantissaSizeWithoutHiddenBit() instead if you want the mantissa without the hidden bit, and FormulaType.FloatingPointType.getMantissaSizeWithHiddenBit() if you want it to include the hidden bit.

getMantissaSizeWithHiddenBit() - Method in class org.sosy_lab.java_smt.api.FloatingPointNumber

Returns the size of the mantissa (also called a coefficient or significant), including the hidden bit.

getMantissaSizeWithHiddenBit() - Method in class org.sosy_lab.java_smt.api.FormulaType.FloatingPointType

Returns the size of the mantissa (also called a coefficient or significant), including the hidden bit.

getMantissaSizeWithoutHiddenBit() - Method in class org.sosy_lab.java_smt.api.FloatingPointNumber

Returns the size of the mantissa (also called a coefficient or significant), excluding the hidden bit.

getMantissaSizeWithoutHiddenBit() - Method in class org.sosy_lab.java_smt.api.FormulaType.FloatingPointType

Returns the size of the mantissa (also called a coefficient or significant), excluding the hidden bit.

getMathSign() - Method in class org.sosy_lab.java_smt.api.FloatingPointNumber

The sign of the floating-point number, i.e.

getMaxTime() - Method in class org.sosy_lab.java_smt.delegate.statistics.TimerPool

Return the maximal time of all intervals.

getMaxTimeOfAllSatQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getMaxTimeOfInterpolationQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getMaxTimeOfIsUnsatQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getModel() - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Get a satisfying assignment.

getModel() - Method in interface org.sosy_lab.java_smt.api.OptimizationProverEnvironment

Get a satisfying assignment.

getModel() - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

getModelAssignments() - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Get a list of satisfying assignments.

getModelAssignments() - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

getName() - Method in class org.sosy_lab.java_smt.api.FormulaType.EnumerationFormulaType

getName() - Method in interface org.sosy_lab.java_smt.api.FunctionDeclaration

getName() - Method in class org.sosy_lab.java_smt.api.Model.ValueAssignment

Variable name for variables, function name for UFs, and array name for arrays.

getName() - Method in class org.sosy_lab.java_smt.example.SolverOverviewTable.SolverInfo

getNewTimer() - Method in class org.sosy_lab.java_smt.delegate.statistics.TimerPool

getNumberOfAddConstraintQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfAllSatQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfArrayOperations() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfBooleanOperations() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfBVOperations() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfFPOperations() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfInterpolationQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfIntervals() - Method in class org.sosy_lab.java_smt.delegate.statistics.TimerPool

Return the number of intervals.

getNumberOfIsUnsatQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfModelEvaluationQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfModelListings() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfModelQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfNumericOperations() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfPopQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfProverEnvironments() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfPushQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfQuantifierOperations() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfSLOperations() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfStringOperations() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfUFOperations() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfUnsatCoreQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumberOfVisits() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getNumOfSolutions() - Method in class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator

getQuantifiedFormulaManager() - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Returns the interface for handling quantifiers.

getQuantifiedFormulaManager() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

getQuantifiedFormulaManager() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

getRationalFormulaManager() - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Returns the Rational-Theory.

getRationalFormulaManager() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

getRationalFormulaManager() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

getRationalType() - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

getRegexType() - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

getResult() - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment.AllSatCallback

Returning the result generated after all the BasicProverEnvironment.AllSatCallback.apply(java.util.List<org.sosy_lab.java_smt.api.BooleanFormula>) calls went through.

getRoundingModeImpl(FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

getSeqInterpolants(List<? extends Collection<T>>) - Method in interface org.sosy_lab.java_smt.api.InterpolatingProverEnvironment

This method returns interpolants of an 'inductive sequence'.

getSeqInterpolants(List<? extends Collection<T>>) - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper

getSeqInterpolants(List<? extends Collection<T>>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingInterpolatingProverEnvironment

getSeqInterpolants0(List<T>) - Method in interface org.sosy_lab.java_smt.api.InterpolatingProverEnvironment

This utility method wraps each formula in a collection and then forwards to InterpolatingProverEnvironment.getSeqInterpolants(java.util.List<? extends java.util.Collection<T>>).

getSign() - Method in class org.sosy_lab.java_smt.api.FloatingPointNumber

Deprecated, for removal: This API element is subject to removal in a future version.

getSinglePrecisionFloatingPointType() - Static method in class org.sosy_lab.java_smt.api.FormulaType

getSize() - Method in class org.sosy_lab.java_smt.api.FormulaType.BitvectorType

getSLFormulaManager() - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Returns the Seperation-Logic-Theory.

getSLFormulaManager() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

getSLFormulaManager() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

getSolverDeclaration() - Method in class org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl

get a reference to the internal declaration used by the SMT solver.

getSolverInformation(SolverContextFactory.Solvers) - Method in class org.sosy_lab.java_smt.example.SolverOverviewTable

Checks for solver-name, version, theories and features.

getSolverName() - Method in interface org.sosy_lab.java_smt.api.SolverContext

Get solver name (MATHSAT5/Z3/etc...).

getSolverName() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverContext

getSolverName() - Method in class org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext

getSolverName() - Method in class org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext

getSolverName() - Method in class org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext

getSolverStatistics() - Method in class org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext

export statistics about the solver interaction.

getStatistics() - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Get statistics for a concrete ProverEnvironment in a solver.

getStatistics() - Method in interface org.sosy_lab.java_smt.api.SolverContext

Get statistics for a complete solver context.

getStatistics() - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

getStatistics() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverContext

getStatistics() - Method in class org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext

getStatistics() - Method in class org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext

getStatistics() - Method in class org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext

getStringFormulaManager() - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Returns the String Theory.

getStringFormulaManager() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

getStringFormulaManager() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

getStringType() - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

getSubstitution() - Method in class org.sosy_lab.java_smt.utils.UfElimination.Result

getSumTime() - Method in class org.sosy_lab.java_smt.delegate.statistics.TimerPool

getSumTimeOfAllSatQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getSumTimeOfInterpolationQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getSumTimeOfIsUnsatQueries() - Method in class org.sosy_lab.java_smt.delegate.statistics.SolverStatistics

getTheories() - Method in class org.sosy_lab.java_smt.example.SolverOverviewTable.SolverInfo

getTotalSize() - Method in class org.sosy_lab.java_smt.api.FloatingPointNumber

Returns the size of the precision, i.e.

getTotalSize() - Method in class org.sosy_lab.java_smt.api.FormulaType.FloatingPointType

Return the total size of a value of this type in bits.

getTreeInterpolants(List<? extends Collection<T>>, int[]) - Method in interface org.sosy_lab.java_smt.api.InterpolatingProverEnvironment

Compute a sequence of interpolants.

getTreeInterpolants(List<? extends Collection<T>>, int[]) - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper

getTreeInterpolants(List<? extends Collection<T>>, int[]) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingInterpolatingProverEnvironment

getTreeInterpolants0(List<T>, int[]) - Method in interface org.sosy_lab.java_smt.api.InterpolatingProverEnvironment

This utility method wraps each formula in a collection and then forwards to InterpolatingProverEnvironment.getTreeInterpolants(java.util.List<? extends java.util.Collection<T>>, int[]).

getType() - Method in interface org.sosy_lab.java_smt.api.FunctionDeclaration

getType() - Method in class org.sosy_lab.java_smt.api.visitors.TraversalProcess

getUFManager() - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Returns the function for dealing with uninterpreted functions (UFs).

getUFManager() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

getUFManager() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

getUnsatCore() - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Get an unsat core.

getUnsatCore() - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

getValue() - Method in class org.sosy_lab.java_smt.api.Model.ValueAssignment

Value: see the Evaluator.evaluate(org.sosy_lab.java_smt.api.Formula) methods for the possible types.

getValueAsFormula() - Method in class org.sosy_lab.java_smt.api.Model.ValueAssignment

The formula AST which is assigned to a given key.

getVersion() - Method in interface org.sosy_lab.java_smt.api.SolverContext

Get version information out of the solver.

getVersion() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverContext

getVersion() - Method in class org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext

getVersion() - Method in class org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext

getVersion() - Method in class org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext

getVersion() - Method in class org.sosy_lab.java_smt.example.SolverOverviewTable.SolverInfo

greaterOrEquals(BitvectorFormula, BitvectorFormula, boolean) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Compare the given bitvectors.

greaterOrEquals(BitvectorFormula, BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

greaterOrEquals(BitvectorFormula, BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

greaterOrEquals(FloatingPointFormula, FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Returns whether an FP number is greater or equal than another FP number.

greaterOrEquals(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

greaterOrEquals(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

greaterOrEquals(StringFormula, StringFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

greaterOrEquals(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

greaterOrEquals(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

greaterOrEquals(ParamFormulaType, ParamFormulaType) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

greaterOrEquals(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

greaterOrEquals(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

greaterOrEquals(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

greaterOrEquals(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

greaterOrEquals(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

greaterOrEquals(TFormulaInfo, TFormulaInfo, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

greaterThan(BitvectorFormula, BitvectorFormula, boolean) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Compare the given bitvectors.

greaterThan(BitvectorFormula, BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

greaterThan(BitvectorFormula, BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

greaterThan(FloatingPointFormula, FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Returns whether an FP number is greater than another FP number.

greaterThan(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

greaterThan(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

greaterThan(StringFormula, StringFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

greaterThan(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

greaterThan(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

greaterThan(ParamFormulaType, ParamFormulaType) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

greaterThan(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

greaterThan(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

greaterThan(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

greaterThan(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

greaterThan(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

greaterThan(TFormulaInfo, TFormulaInfo, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

GT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Greater-than over integers and rationals.

GTE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Greater-than-or-equal over integers and rationals.

GTE_ZERO - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Unary comparison with zero.

H

hasConstants(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager.EnumType

hashCode() - Method in interface org.sosy_lab.java_smt.api.Formula

returns a valid hashCode satisfying the constraints given by Formula.equals(java.lang.Object).

hashCode() - Method in class org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType

hashCode() - Method in class org.sosy_lab.java_smt.api.FormulaType.BitvectorType

hashCode() - Method in class org.sosy_lab.java_smt.api.FormulaType.EnumerationFormulaType

hashCode() - Method in class org.sosy_lab.java_smt.api.FormulaType.FloatingPointType

hashCode() - Method in class org.sosy_lab.java_smt.api.Model.ValueAssignment

houdini(List<BooleanFormula>, BooleanFormula) - Method in class org.sosy_lab.java_smt.example.HoudiniApp

execute the Houdini algorithm to get the maximal inductive subset L_I for the given lemmas and the transition.

HoudiniApp - Class in org.sosy_lab.java_smt.example

This application executes the inductive-invariant synthesis algorithm called "Houdini" taken from the paper Flanagan and Leino: "Houdini, an Annotation Assistant for ESC/Java".

HoudiniApp(SolverContext) - Constructor for class org.sosy_lab.java_smt.example.HoudiniApp

I

IFF - org.sosy_lab.java_smt.api.FunctionDeclarationKind

If and only if.

ifThenElse(BooleanFormula, T, T) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Creates a formula representing IF cond THEN f1 ELSE f2.

ifThenElse(BooleanFormula, T, T) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

Creates a formula representing "IF cond THEN f1 ELSE f2".

ifThenElse(BooleanFormula, T, T) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

ifThenElse(TFormulaInfo, TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

imgr - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

implication(BooleanFormula, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

implication(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

implication(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

implication(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

implies(BooleanFormula) - Method in class org.sosy_lab.java_smt.test.BooleanFormulaSubject

Check that the subject implies a given formula, i.e.

IMPLIES - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Implication between two boolean formulas.

in(StringFormula, RegexFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

in(StringFormula, RegexFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

in(StringFormula, RegexFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

in(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

indexOf(StringFormula, StringFormula, NumeralFormula.IntegerFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Get the first index for a substring in a String, or -1 if the substring is not found.

indexOf(StringFormula, StringFormula, NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

indexOf(StringFormula, StringFormula, NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

indexOf(TFormulaInfo, TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

initializeWithBackend(PropagatorBackend) - Method in interface org.sosy_lab.java_smt.api.UserPropagator

This method is invoked after the user propagator is registered via BasicProverEnvironment.registerUserPropagator(UserPropagator).

initializeWithBackend(PropagatorBackend) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator

initializeWithBackend(PropagatorBackend) - Method in class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator

initSolver() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

INT_TO_STR - org.sosy_lab.java_smt.api.FunctionDeclarationKind

IntegerBasedBinoxxoSolver(SolverContext) - Constructor for class org.sosy_lab.java_smt.example.Binoxxo.IntegerBasedBinoxxoSolver

IntegerBasedSudokuSolver(SolverContext) - Constructor for class org.sosy_lab.java_smt.example.Sudoku.IntegerBasedSudokuSolver

IntegerFormulaManager - Interface in org.sosy_lab.java_smt.api

Interface which operates over NumeralFormula.IntegerFormulas.

IntegerType - Static variable in class org.sosy_lab.java_smt.api.FormulaType

internalMakeArray(String, FormulaType<TI>, FormulaType<TE>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager

internalMakeArray(FormulaType<TI>, FormulaType<TE>, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager

InterpolatingProverEnvironment<T> - Interface in org.sosy_lab.java_smt.api

This class provides an interface to an incremental SMT solver with methods for pushing and popping formulas as well as SAT checks.

InterpolatingProverWithAssumptionsWrapper<T> - Class in org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper

InterpolatingProverWithAssumptionsWrapper(InterpolatingProverEnvironment<T>, FormulaManager) - Constructor for class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper

Interpolation - Class in org.sosy_lab.java_smt.example

Examples for Craig/sequential/tree interpolation.

intersection(RegexFormula, RegexFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

intersection(RegexFormula, RegexFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

intersection(RegexFormula, RegexFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

intersection(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

isArrayType() - Method in class org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType

isArrayType() - Method in class org.sosy_lab.java_smt.api.FormulaType

isAssertToken(String) - Static method in class org.sosy_lab.java_smt.basicimpl.Tokenizer

Check if the token is an (assert ...).

isBitvectorType() - Method in class org.sosy_lab.java_smt.api.FormulaType.BitvectorType

isBitvectorType() - Method in class org.sosy_lab.java_smt.api.FormulaType

isBooleanType() - Method in class org.sosy_lab.java_smt.api.FormulaType

isClosed() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEvaluator

isCompatible(FormulaType<?>, FormulaType<?>) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

This function checks whether the used type of the function argument is compatible with the declared type in the function declaration.

isDeclarationToken(String) - Static method in class org.sosy_lab.java_smt.basicimpl.Tokenizer

Check if the token is a function or variable declaration.

isDefinitionToken(String) - Static method in class org.sosy_lab.java_smt.basicimpl.Tokenizer

Check if the token is a function definition.

isEnumerationType() - Method in class org.sosy_lab.java_smt.api.FormulaType.EnumerationFormulaType

isEnumerationType() - Method in class org.sosy_lab.java_smt.api.FormulaType

isEquisatisfiableTo(BooleanFormula) - Method in class org.sosy_lab.java_smt.test.BooleanFormulaSubject

isEquivalentTo(BooleanFormula) - Method in class org.sosy_lab.java_smt.test.BooleanFormulaSubject

Check that the subject is equivalent to a given formula, i.e.

isExitToken(String) - Static method in class org.sosy_lab.java_smt.basicimpl.Tokenizer

Check if the token is (exit).

isFalse(BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Check, if the formula is the formula "FALSE".

isFalse(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

isFalse(BooleanFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

isFalse(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

isFloatingPointRoundingModeType() - Method in class org.sosy_lab.java_smt.api.FormulaType

isFloatingPointType() - Method in class org.sosy_lab.java_smt.api.FormulaType.FloatingPointType

isFloatingPointType() - Method in class org.sosy_lab.java_smt.api.FormulaType

isForbiddenToken(String) - Static method in class org.sosy_lab.java_smt.basicimpl.Tokenizer

Check if this is a forbidden token.

isFunction() - Method in class org.sosy_lab.java_smt.api.Model.ValueAssignment

isIEEE754DoublePrecision() - Method in class org.sosy_lab.java_smt.api.FloatingPointNumber

Returns true if this floating-point number is an IEEE-754-2008 double precision type with 64 bits length consisting of an 11 bit exponent, a 53 bit mantissa (including the hidden bit).

isIEEE754SinglePrecision() - Method in class org.sosy_lab.java_smt.api.FloatingPointNumber

Returns true if this floating-point number is an IEEE-754-2008 single precision type with 32 bits length consisting of an 8 bit exponent, a 24 bit mantissa (including the hidden bit).

isInfinity(FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Checks whether a formula is positive or negative infinity.

isInfinity(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

isInfinity(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

isInfinity(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

isIntegerType() - Method in class org.sosy_lab.java_smt.api.FormulaType

isNaN(FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Check whether a floating-point number is NaN.

isNaN(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

isNaN(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

isNaN(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

isNegative() - Method in enum org.sosy_lab.java_smt.api.FloatingPointNumber.Sign

isNegative(FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Checks whether a formula is negative, including -0.0.

isNegative(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

isNegative(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

isNegative(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

isNegativeZero(Double) - Static method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

isNormal(FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Checks whether a formula is normal FP number.

isNormal(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

isNormal(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

isNormal(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

isNumeral(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

Check whether the argument is a numeric constant (including negated constants).

isNumeralType() - Method in class org.sosy_lab.java_smt.api.FormulaType

isNumeralType() - Method in class org.sosy_lab.java_smt.api.FormulaType.NumeralType

isPopToken(String) - Static method in class org.sosy_lab.java_smt.basicimpl.Tokenizer

Check if the token is an (pop ...).

isPushToken(String) - Static method in class org.sosy_lab.java_smt.basicimpl.Tokenizer

Check if the token is an (push ...).

isRationalType() - Method in class org.sosy_lab.java_smt.api.FormulaType

isRegexType() - Method in class org.sosy_lab.java_smt.api.FormulaType

isResetAssertionsToken(String) - Static method in class org.sosy_lab.java_smt.basicimpl.Tokenizer

Check if the token is an (reset-assertions ...).

isResetToken(String) - Static method in class org.sosy_lab.java_smt.basicimpl.Tokenizer

Check if the token is an (reset).

isSatisfiable() - Method in class org.sosy_lab.java_smt.test.BooleanFormulaSubject

Check that the subject is satisfiable.

isSatisfiable() - Method in class org.sosy_lab.java_smt.test.ProverEnvironmentSubject

Check that the subject stack is satisfiable.

isSetLogicToken(String) - Static method in class org.sosy_lab.java_smt.basicimpl.Tokenizer

Check if the token is (set-logic ..).

isSLType() - Method in class org.sosy_lab.java_smt.api.FormulaType

isStringType() - Method in class org.sosy_lab.java_smt.api.FormulaType

isSubnormal(FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Checks whether a formula is subnormal FP number.

isSubnormal(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

isSubnormal(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

isSubnormal(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

isTautological() - Method in class org.sosy_lab.java_smt.test.BooleanFormulaSubject

Check that the subject is tautological, i.e., always holds.

isTrue(BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Check, if the formula is the formula "TRUE".

isTrue(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

isTrue(BooleanFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

isTrue(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

isUnsat() - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Check whether the conjunction of all formulas on the stack is unsatisfiable.

isUnsat() - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

isUnsatisfiable() - Method in class org.sosy_lab.java_smt.test.BooleanFormulaSubject

Check that the subject is unsatisfiable.

isUnsatisfiable() - Method in class org.sosy_lab.java_smt.test.ProverEnvironmentSubject

Check that the subject stack is unsatisfiable.

isUnsatWithAssumptions(Collection<BooleanFormula>) - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Check whether the conjunction of all formulas on the stack together with the list of assumptions is satisfiable.

isUnsatWithAssumptions(Collection<BooleanFormula>) - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

isValidName(String) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Check whether the given String can be used as symbol/name for variables or undefined functions.

isValidName(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

Check whether the given String can be used as symbol/name for variables or undefined functions.

isValidName(String) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

isZero(FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Checks whether a formula is positive or negative zero.

isZero(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

isZero(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

isZero(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

ITE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

If-then-else operator.

iterator() - Method in interface org.sosy_lab.java_smt.api.Model

Iterate over all values present in the model.

L

largerStackUsageTest() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

largeStackUsageTest() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

length(StringFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

length(StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

length(StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

length(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

lessOrEquals(BitvectorFormula, BitvectorFormula, boolean) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Compare the given bitvectors.

lessOrEquals(BitvectorFormula, BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

lessOrEquals(BitvectorFormula, BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

lessOrEquals(FloatingPointFormula, FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Returns whether an FP number is less or equal than another FP number.

lessOrEquals(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

lessOrEquals(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

lessOrEquals(StringFormula, StringFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

lessOrEquals(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

lessOrEquals(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

lessOrEquals(ParamFormulaType, ParamFormulaType) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

lessOrEquals(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

lessOrEquals(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

lessOrEquals(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

lessOrEquals(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

lessOrEquals(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

lessOrEquals(TFormulaInfo, TFormulaInfo, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

lessThan(BitvectorFormula, BitvectorFormula, boolean) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Compare the given bitvectors.

lessThan(BitvectorFormula, BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

lessThan(BitvectorFormula, BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

lessThan(FloatingPointFormula, FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Returns whether an FP number is less than another FP number.

lessThan(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

lessThan(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

lessThan(StringFormula, StringFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

lessThan(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

lessThan(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

lessThan(ParamFormulaType, ParamFormulaType) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

lessThan(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

lessThan(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

lessThan(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

lessThan(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

lessThan(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

lessThan(TFormulaInfo, TFormulaInfo, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

loadLibrariesWithFallback(Consumer<String>, List<String>, List<String>) - Static method in class org.sosy_lab.java_smt.basicimpl.AbstractSolverContext

This method loads the given libraries.

logger - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

LoggingSolverContext - Class in org.sosy_lab.java_smt.delegate.logging

SolverContext that wraps all prover environments in their logging versions.

LoggingSolverContext(LogManager, SolverContext) - Constructor for class org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext

logicToUse() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

This method is only called, if OpenSMT is called.

lower(int, Rational) - Method in interface org.sosy_lab.java_smt.api.OptimizationProverEnvironment

lower(int, Rational) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingOptimizationProverEnvironment

LT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Less-than over integers and rationals.

LTE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Less-than-or-equal over integers and rationals.

M

main(String...) - Static method in class org.sosy_lab.java_smt.example.AllSatExample

main(String...) - Static method in class org.sosy_lab.java_smt.example.Binoxxo

main(String...) - Static method in class org.sosy_lab.java_smt.example.FormulaClassifier

main(String...) - Static method in class org.sosy_lab.java_smt.example.HoudiniApp

main(String...) - Static method in class org.sosy_lab.java_smt.example.Interpolation

main(String...) - Static method in class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueens

main(String...) - Static method in class org.sosy_lab.java_smt.example.NQueens

main(String...) - Static method in class org.sosy_lab.java_smt.example.OptimizationFormulaWeights

main(String...) - Static method in class org.sosy_lab.java_smt.example.OptimizationIntReal

main(String...) - Static method in class org.sosy_lab.java_smt.example.PrettyPrinter

main(String[]) - Static method in class org.sosy_lab.java_smt.example.SimpleUserPropagator

main(String[]) - Static method in class org.sosy_lab.java_smt.example.SolverOverviewTable

main(String...) - Static method in class org.sosy_lab.java_smt.example.Sudoku

makeApplication(FunctionDeclaration<T>, List<? extends Formula>) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Create a function application to the given list of arguments.

makeApplication(FunctionDeclaration<T>, List<? extends Formula>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

makeApplication(FunctionDeclaration<T>, List<? extends Formula>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

makeApplication(FunctionDeclaration<T>, Formula...) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Create a function application to the given list of arguments.

makeApplication(FunctionDeclaration<T>, Formula...) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

makeApplication(FunctionDeclaration<T>, Formula...) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

makeArray(FTI, FTE, TE) - Method in interface org.sosy_lab.java_smt.api.ArrayFormulaManager

Create a new array constant with values initialized to defaultElement.

makeArray(FTI, FTE, TE) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager

makeArray(FTI, FTE, TE) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingArrayFormulaManager

makeArray(String, FTI, FTE) - Method in interface org.sosy_lab.java_smt.api.ArrayFormulaManager

Declare a new array with exactly the given name.

makeArray(String, FTI, FTE) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager

makeArray(String, FTI, FTE) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingArrayFormulaManager

makeArray(String, FormulaType.ArrayFormulaType<TI, TE>) - Method in interface org.sosy_lab.java_smt.api.ArrayFormulaManager

Declare a new array with exactly the given name.

makeArray(String, FormulaType.ArrayFormulaType<TI, TE>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingArrayFormulaManager

makeArray(FormulaType.ArrayFormulaType<TI, TE>, TE) - Method in interface org.sosy_lab.java_smt.api.ArrayFormulaManager

Create a new array constant with values initialized to defaultElement.

makeBitvector(int, long) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Convert a number into a bitvector with given size.

makeBitvector(int, long) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

makeBitvector(int, long) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

makeBitvector(int, BigInteger) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Convert a number into a bitvector with given size.

makeBitvector(int, BigInteger) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

makeBitvector(int, BigInteger) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

makeBitvector(int, NumeralFormula.IntegerFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Convert/Cast/Interpret a numeral formula into a bitvector with given size.

makeBitvector(int, NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

makeBitvector(int, NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

makeBitvectorImpl(int, long) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

makeBitvectorImpl(int, BigInteger) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

makeBitvectorImpl(int, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

makeBoolean(boolean) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Returns a BooleanFormula representing the given value.

makeBooleanImpl(boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

makeConstant(String, FormulaType.EnumerationFormulaType) - Method in interface org.sosy_lab.java_smt.api.EnumerationFormulaManager

Creates a constant of given enumeration type with exactly the given name.

makeConstant(String, FormulaType.EnumerationFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager

makeConstant(String, FormulaType.EnumerationFormulaType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingEnumerationFormulaManager

makeConstant(String, FormulaType.EnumerationFormulaType) - Method in class org.sosy_lab.java_smt.delegate.statistics.StatisticsEnumerationFormulaManager

makeConstant(String, FormulaType.EnumerationFormulaType) - Method in class org.sosy_lab.java_smt.delegate.synchronize.SynchronizedEnumerationFormulaManager

makeConstantImpl(String, FormulaType.EnumerationFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager

makeEmptyHeap(AT, VT) - Method in interface org.sosy_lab.java_smt.api.SLFormulaManager

makeEmptyHeap(AT, VT) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager

makeEmptyHeap(AT, VT) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSLFormulaManager

makeEmptyHeap(TType, TType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager

makeFalse() - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Shortcut for makeBoolean(false).

makeFalse() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

makeFalse() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

makeMagicWand(BooleanFormula, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.SLFormulaManager

makeMagicWand(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager

makeMagicWand(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSLFormulaManager

makeMagicWand(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager

makeMinusInfinity(FormulaType.FloatingPointType) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

makeMinusInfinity(FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeMinusInfinity(FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

makeMinusInfinityImpl(FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNaN(FormulaType.FloatingPointType) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

makeNaN(FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNaN(FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

makeNaNImpl(FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNilElement(AT) - Method in interface org.sosy_lab.java_smt.api.SLFormulaManager

makeNilElement(AT) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager

makeNilElement(AT) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSLFormulaManager

makeNilElement(TType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager

makeNumber(double) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

Create a numeric literal with a given value.

makeNumber(double) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

makeNumber(double) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

makeNumber(double, FormulaType.FloatingPointType) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Creates a floating point formula representing the given double value with the specified type.

makeNumber(double, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNumber(double, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

makeNumber(double, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Creates a floating point formula representing the given double value with the specified type and rounding mode.

makeNumber(double, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNumber(double, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

makeNumber(long) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

makeNumber(long) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

makeNumber(long) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

makeNumber(String) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

makeNumber(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

makeNumber(String) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

makeNumber(String, FormulaType.FloatingPointType) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Creates a floating point formula representing the given string value with the specified type.

makeNumber(String, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNumber(String, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

makeNumber(String, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Creates a floating point formula representing the given string value with the specified type and rounding mode.

makeNumber(String, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNumber(String, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

makeNumber(BigDecimal) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

Create a numeric literal with a given value.

makeNumber(BigDecimal) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

makeNumber(BigDecimal) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

makeNumber(BigDecimal, FormulaType.FloatingPointType) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Creates a floating point formula representing the given BigDecimal value with the specified type.

makeNumber(BigDecimal, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNumber(BigDecimal, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

makeNumber(BigDecimal, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Creates a floating point formula representing the given BigDecimal value with the specified type and rounding mode.

makeNumber(BigDecimal, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNumber(BigDecimal, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

makeNumber(BigInteger) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

makeNumber(BigInteger) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

makeNumber(BigInteger) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

makeNumber(BigInteger, BigInteger, boolean, FormulaType.FloatingPointType) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Deprecated, for removal: This API element is subject to removal in a future version.

makeNumber(BigInteger, BigInteger, FloatingPointNumber.Sign, FormulaType.FloatingPointType) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Creates a floating point formula from the given exponent, mantissa, and sign with the specified type.

makeNumber(BigInteger, BigInteger, FloatingPointNumber.Sign, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNumber(BigInteger, BigInteger, FloatingPointNumber.Sign, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

makeNumber(Rational) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

makeNumber(Rational) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

makeNumber(Rational) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

makeNumber(Rational, FormulaType.FloatingPointType) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Creates a floating point formula representing the given Rational value with the specified type.

makeNumber(Rational, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNumber(Rational, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

makeNumber(Rational, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Creates a floating point formula representing the given Rational value with the specified type and rounding mode.

makeNumber(Rational, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNumber(Rational, FormulaType.FloatingPointType, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

makeNumber(FloatingPointNumber) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Creates a floating point formula from the given FloatingPointNumber.

makeNumberAndRound(String, FormulaType.FloatingPointType, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

Parses the provided string and converts it into a floating-point formula.

makeNumberImpl(double) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

makeNumberImpl(double, FormulaType.FloatingPointType, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNumberImpl(long) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

makeNumberImpl(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

makeNumberImpl(String, FormulaType.FloatingPointType, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

directly catch the most common special String constants.

makeNumberImpl(BigDecimal) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

makeNumberImpl(BigDecimal, FormulaType.FloatingPointType, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNumberImpl(BigInteger) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

makeNumberImpl(BigInteger, BigInteger, FloatingPointNumber.Sign, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeNumberImpl(Rational) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

makePlusInfinity(FormulaType.FloatingPointType) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

makePlusInfinity(FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makePlusInfinity(FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

makePlusInfinityImpl(FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makePointsTo(AF, VF) - Method in interface org.sosy_lab.java_smt.api.SLFormulaManager

makePointsTo(AF, VF) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSLFormulaManager

makePointsTo(Formula, Formula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager

makePointsTo(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager

makeRegex(String) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Returns a RegexFormula representing the given constant.

makeRegex(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

makeRegex(String) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

makeRegexImpl(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

makeStar(BooleanFormula, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.SLFormulaManager

makeStar(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager

makeStar(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSLFormulaManager

makeStar(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager

makeString(String) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Creates a StringFormula representing the given constant String.

makeString(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

makeString(String) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

makeStringImpl(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

makeTrue() - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Shortcut for makeBoolean(true).

makeTrue() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

makeTrue() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

makeVariable(int, String) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Creates a variable with exactly the given name and bitwidth.

makeVariable(int, String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

makeVariable(int, String) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

makeVariable(String) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Creates a variable with exactly the given name.

makeVariable(String) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

Creates a variable with exactly the given name.

makeVariable(String) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Creates a variable of type String with exactly the given name.

makeVariable(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

makeVariable(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

makeVariable(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

makeVariable(String) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

makeVariable(String) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

makeVariable(String) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

makeVariable(String, FormulaType.EnumerationFormulaType) - Method in interface org.sosy_lab.java_smt.api.EnumerationFormulaManager

Creates a variable of given enumeration type with exactly the given name.

makeVariable(String, FormulaType.EnumerationFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager

makeVariable(String, FormulaType.EnumerationFormulaType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingEnumerationFormulaManager

makeVariable(String, FormulaType.EnumerationFormulaType) - Method in class org.sosy_lab.java_smt.delegate.statistics.StatisticsEnumerationFormulaManager

makeVariable(String, FormulaType.EnumerationFormulaType) - Method in class org.sosy_lab.java_smt.delegate.synchronize.SynchronizedEnumerationFormulaManager

makeVariable(String, FormulaType.FloatingPointType) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Creates a variable with exactly the given name.

makeVariable(String, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

makeVariable(String, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

makeVariable(FormulaType.BitvectorType, String) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

makeVariable(FormulaType.BitvectorType, String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

makeVariable(FormulaType.BitvectorType, String) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

makeVariable(FormulaType<T>, String) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Create variable of the type equal to formulaType.

makeVariable(FormulaType<T>, String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

makeVariable(FormulaType<T>, String) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

makeVariable(TType, String) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

makeVariableImpl(int, String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

makeVariableImpl(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

makeVariableImpl(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

makeVariableImpl(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

makeVariableImpl(String, FormulaType.EnumerationFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager

makeVariableImpl(String, FormulaType.FloatingPointType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

MATHSAT5 - org.sosy_lab.java_smt.SolverContextFactory.Solvers

max(FloatingPointFormula, FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Returns the maximum value of the two given floating-point numbers.

max(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

max(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

max(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

maximize(Formula) - Method in interface org.sosy_lab.java_smt.api.OptimizationProverEnvironment

Add the maximization objective.

maximize(Formula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingOptimizationProverEnvironment

mgr - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

min(FloatingPointFormula, FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Returns the minimum value of the two given floating-point numbers.

min(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

min(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

min(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

minimize(Formula) - Method in interface org.sosy_lab.java_smt.api.OptimizationProverEnvironment

Add minimization objective.

minimize(Formula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingOptimizationProverEnvironment

mkQuantifier(QuantifiedFormulaManager.Quantifier, List<? extends Formula>, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.QuantifiedFormulaManager

mkQuantifier(QuantifiedFormulaManager.Quantifier, List<? extends Formula>, BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager

mkQuantifier(QuantifiedFormulaManager.Quantifier, List<? extends Formula>, BooleanFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingQuantifiedFormulaManager

mkQuantifier(QuantifiedFormulaManager.Quantifier, List<TFormulaInfo>, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager

Model - Interface in org.sosy_lab.java_smt.api

This class provides a model with concrete evaluations for symbols and formulas from the satisfiable solver environment.

Model.ValueAssignment - Class in org.sosy_lab.java_smt.api

modelForSatFormula() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

modelForSatFormulaWithLargeValue() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

modelForSatFormulaWithUF() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

modelForUnsatFormula() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

modelForUnsatFormula2() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

modelSet - Variable in class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator

modularCongruence(NumeralFormula.IntegerFormula, NumeralFormula.IntegerFormula, long) - Method in interface org.sosy_lab.java_smt.api.IntegerFormulaManager

Create a term representing the constraint number1 == number2 (mod n).

modularCongruence(NumeralFormula.IntegerFormula, NumeralFormula.IntegerFormula, long) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingIntegerFormulaManager

modularCongruence(NumeralFormula.IntegerFormula, NumeralFormula.IntegerFormula, BigInteger) - Method in interface org.sosy_lab.java_smt.api.IntegerFormulaManager

Create a term representing the constraint number1 == number2 (mod n).

modularCongruence(NumeralFormula.IntegerFormula, NumeralFormula.IntegerFormula, BigInteger) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingIntegerFormulaManager

modularCongruence(ParamFormulaType, ParamFormulaType, long) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

modularCongruence(ParamFormulaType, ParamFormulaType, BigInteger) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

modularCongruence(TFormulaInfo, TFormulaInfo, long) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

modularCongruence(TFormulaInfo, TFormulaInfo, BigInteger) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

modulo(BitvectorFormula, BitvectorFormula, boolean) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Deprecated, for removal: This API element is subject to removal in a future version.

modulo(NumeralFormula.IntegerFormula, NumeralFormula.IntegerFormula) - Method in interface org.sosy_lab.java_smt.api.IntegerFormulaManager

Create a formula representing the modulo of two operands according to Boute's Euclidean definition (DOI: 10.1145/128861.128862).

modulo(NumeralFormula.IntegerFormula, NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingIntegerFormulaManager

modulo(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

modulo(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

If a solver does not support this operation, e.g.

MODULO - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Modulo operator over integers.

MUL - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Multiplication over integers and rationals.

multiCloseTest() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

multiply(BitvectorFormula, BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns the multiplication of the given bitvectors.

multiply(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

multiply(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

multiply(FloatingPointFormula, FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

multiply(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

multiply(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

multiply(FloatingPointFormula, FloatingPointFormula, FloatingPointRoundingMode) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

multiply(FloatingPointFormula, FloatingPointFormula, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

multiply(FloatingPointFormula, FloatingPointFormula, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

multiply(ParamFormulaType, ParamFormulaType) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

multiply(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

multiply(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

multiply(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

multiply(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

If a solver does not support this operation, e.g.

multiply(TFormulaInfo, TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

multiStackTest() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

N

NEAREST_TIES_AWAY - org.sosy_lab.java_smt.api.FloatingPointRoundingMode

NEAREST_TIES_TO_EVEN - org.sosy_lab.java_smt.api.FloatingPointRoundingMode

negate(BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns the negated number, i.e., it is multiplied by "-1".

negate(BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

negate(BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

negate(FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

negate(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

negate(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

negate(ParamFormulaType) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

negate(ParamFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

negate(ParamFormulaType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

negate(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

negate(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

negate(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

NEGATIVE - org.sosy_lab.java_smt.api.FloatingPointNumber.Sign

newEnvironmentForTest(SolverContext, SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

newOptimizationProverEnvironment(SolverContext.ProverOptions...) - Method in interface org.sosy_lab.java_smt.api.SolverContext

Create a fresh new OptimizationProverEnvironment which encapsulates an assertion stack and allows solving optimization queries.

newOptimizationProverEnvironment(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSolverContext

newOptimizationProverEnvironment(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverContext

newOptimizationProverEnvironment(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext

newOptimizationProverEnvironment(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext

newOptimizationProverEnvironment(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext

newOptimizationProverEnvironment0(Set<SolverContext.ProverOptions>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSolverContext

newProverEnvironment(SolverContext.ProverOptions...) - Method in interface org.sosy_lab.java_smt.api.SolverContext

Create a fresh new ProverEnvironment which encapsulates an assertion stack and can be used to check formulas for unsatisfiability.

newProverEnvironment(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSolverContext

newProverEnvironment(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverContext

newProverEnvironment(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext

newProverEnvironment(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext

newProverEnvironment(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext

newProverEnvironment0(Set<SolverContext.ProverOptions>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSolverContext

newProverEnvironmentWithInterpolation(SolverContext.ProverOptions...) - Method in interface org.sosy_lab.java_smt.api.SolverContext

Create a fresh new InterpolatingProverEnvironment which encapsulates an assertion stack and allows generating and retrieve interpolants for unsatisfiable formulas.

newProverEnvironmentWithInterpolation(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSolverContext

newProverEnvironmentWithInterpolation(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverContext

newProverEnvironmentWithInterpolation(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext

newProverEnvironmentWithInterpolation(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext

newProverEnvironmentWithInterpolation(SolverContext.ProverOptions...) - Method in class org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext

newProverEnvironmentWithInterpolation0(Set<SolverContext.ProverOptions>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSolverContext

NNF - org.sosy_lab.java_smt.api.Tactic

Convert the formula to NNF (negated normal form).

NNFVisitor - Class in org.sosy_lab.java_smt.basicimpl.tactics

NNFVisitor(FormulaManager) - Constructor for class org.sosy_lab.java_smt.basicimpl.tactics.NNFVisitor

NO_MODEL_HELP - Static variable in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

none() - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

none() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

none() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

noneImpl() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

not(BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns the bit-wise complement of the given bitvector.

not(BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

not(BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

not(BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Creates a formula representing a negation of the argument.

not(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

not(BooleanFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

not(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

not(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

NOT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

notifyOnDecision() - Method in interface org.sosy_lab.java_smt.api.PropagatorBackend

Enables tracking of decisions made for the associated UserPropagator via UserPropagator.onDecision(BooleanFormula, boolean).

notifyOnFinalCheck() - Method in interface org.sosy_lab.java_smt.api.PropagatorBackend

Enables the final callback UserPropagator.onFinalCheck() that is invoked when the solver finds a full satisfying assignment.

notifyOnKnownValue() - Method in interface org.sosy_lab.java_smt.api.PropagatorBackend

Enables tracking of expression values for the associated UserPropagator via UserPropagator.onKnownValue(org.sosy_lab.java_smt.api.BooleanFormula, boolean).

NQueens - Class in org.sosy_lab.java_smt.example

This example program solves a NQueens problem of given size and prints a possible solution.

NQueens - Class in org.sosy_lab.java_smt.example.nqueens_user_propagator

This example program solves a NQueens problem of given size and prints a possible solution.

NQueens(SolverContext, int) - Constructor for class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueens

NQueensConstraintPropagator - Class in org.sosy_lab.java_smt.example.nqueens_user_propagator

In addition to the enumeration done by NQueensEnumeratingPropagator, this propagator also enforces the queen placement constraints without explicit encoding.

NQueensConstraintPropagator(BooleanFormula[][]) - Constructor for class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensConstraintPropagator

NQueensEnumeratingPropagator - Class in org.sosy_lab.java_smt.example.nqueens_user_propagator

This propagator enumerates the solutions of the NQueens problem by raising a conflict whenever the solver finds a model.

NQueensEnumeratingPropagator() - Constructor for class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator

NumeralFormula - Interface in org.sosy_lab.java_smt.api

Formulas of any numeral sort.

NumeralFormula.IntegerFormula - Interface in org.sosy_lab.java_smt.api

NumeralFormula.RationalFormula - Interface in org.sosy_lab.java_smt.api

NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula> - Interface in org.sosy_lab.java_smt.api

This interface represents the Numeral Theory.

NumeralType() - Constructor for class org.sosy_lab.java_smt.api.FormulaType.NumeralType

O

of(boolean) - Static method in enum org.sosy_lab.java_smt.api.FloatingPointNumber.Sign

get the Sign for a flag.

of(boolean, BigInteger, BigInteger, int, int) - Static method in class org.sosy_lab.java_smt.api.FloatingPointNumber

Deprecated, for removal: This API element is subject to removal in a future version.

of(String, int, int) - Static method in class org.sosy_lab.java_smt.api.FloatingPointNumber

Get a floating-point number encoded as bitvector as defined by IEEE 754.

of(String, FunctionDeclarationKind, List<FormulaType<?>>, FormulaType<F>, T) - Static method in class org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl

of(FloatingPointNumber.Sign, BigInteger, BigInteger, int, int) - Static method in class org.sosy_lab.java_smt.api.FloatingPointNumber

Get a floating-point number with the given sign, exponent, and mantissa.

onDecision(BooleanFormula, boolean) - Method in interface org.sosy_lab.java_smt.api.UserPropagator

This callback is invoked if the solver decides to branch on a registered expression.

onDecision(BooleanFormula, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator

onFinalCheck() - Method in interface org.sosy_lab.java_smt.api.UserPropagator

This callback is invoked when the solver finds a complete satisfying assignment.

onFinalCheck() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator

onFinalCheck() - Method in class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator

onKnownValue(BooleanFormula, boolean) - Method in interface org.sosy_lab.java_smt.api.UserPropagator

This callback is invoked if the solver gets to know the value of a registered expression (UserPropagator.registerExpression(org.sosy_lab.java_smt.api.BooleanFormula)).

onKnownValue(BooleanFormula, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator

onKnownValue(BooleanFormula, boolean) - Method in class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensConstraintPropagator

onKnownValue(BooleanFormula, boolean) - Method in class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator

onPop(int) - Method in interface org.sosy_lab.java_smt.api.UserPropagator

This callback is invoked when the solver backtracks.

onPop(int) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator

onPop(int) - Method in class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator

onPush() - Method in interface org.sosy_lab.java_smt.api.UserPropagator

This callback is invoked whenever the solver creates a new decision level.

onPush() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator

onPush() - Method in class org.sosy_lab.java_smt.example.nqueens_user_propagator.NQueensEnumeratingPropagator

OPENSMT - org.sosy_lab.java_smt.SolverContextFactory.Solvers

OPT - org.sosy_lab.java_smt.api.OptimizationProverEnvironment.OptStatus

The solution was found (maybe unbounded).

OptimizationFormulaWeights - Class in org.sosy_lab.java_smt.example

Example for optimizing the weight of some constraints.

OptimizationIntReal - Class in org.sosy_lab.java_smt.example

Example for optimizing 'x' with the constraint '0 <= x < 10'.

OptimizationProverEnvironment - Interface in org.sosy_lab.java_smt.api

Interface for optimization modulo SMT.

OptimizationProverEnvironment.OptStatus - Enum in org.sosy_lab.java_smt.api

Status of the optimization problem.

optional(RegexFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

optional(RegexFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

optional(RegexFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

or(Collection<BooleanFormula>) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

or(Collection<BooleanFormula>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

or(Collection<BooleanFormula>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

or(BitvectorFormula, BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns the bit-wise OR of the given bitvectors.

or(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

or(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

or(BooleanFormula...) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

or(BooleanFormula, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Creates a formula representing an OR of the two arguments.

or(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

or(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

or(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

or(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

OR - org.sosy_lab.java_smt.api.FunctionDeclarationKind

org.sosy_lab.java_smt - package org.sosy_lab.java_smt

JavaSMT: a generic SMT solver API.

org.sosy_lab.java_smt.api - package org.sosy_lab.java_smt.api

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

org.sosy_lab.java_smt.api.visitors - package org.sosy_lab.java_smt.api.visitors

The visitors of this package allow for efficient traversal, manipulation and transformation of formulas.

org.sosy_lab.java_smt.basicimpl - package org.sosy_lab.java_smt.basicimpl

Abstract base classes for easier implementation of a solver backend.

org.sosy_lab.java_smt.basicimpl.tactics - package org.sosy_lab.java_smt.basicimpl.tactics

Default tactics implementations (formula-to-formula transformations).

org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper - package org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper

Wrapper-classes to guarantee identical behavior for all solvers.

org.sosy_lab.java_smt.delegate.debugging - package org.sosy_lab.java_smt.delegate.debugging

org.sosy_lab.java_smt.delegate.logging - package org.sosy_lab.java_smt.delegate.logging

Wraps the proving environment with loggers.

org.sosy_lab.java_smt.delegate.statistics - package org.sosy_lab.java_smt.delegate.statistics

The classes of this package wrap the whole proving environment and measure all accesses to it.

org.sosy_lab.java_smt.delegate.synchronize - package org.sosy_lab.java_smt.delegate.synchronize

The classes of this package wrap the whole solver context and all corresponding proving environment and synchronize all accesses to it.

org.sosy_lab.java_smt.example - package org.sosy_lab.java_smt.example

Some basic examples for using Java-SMT.

org.sosy_lab.java_smt.example.nqueens_user_propagator - package org.sosy_lab.java_smt.example.nqueens_user_propagator

Some basic examples for using Java-SMT.

org.sosy_lab.java_smt.test - package org.sosy_lab.java_smt.test

Solver-independent tests and test utilities for the solver API.

org.sosy_lab.java_smt.utils - package org.sosy_lab.java_smt.utils

Utility classes implementing algorithms based on the API of JavaSMT.

orImpl(Collection<TFormulaInfo>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

Create an n-ary disjunction.

OTHER - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Solvers support a lot of different built-in theories.

P

ParameterizedSolverBasedTest0() - Constructor for class org.sosy_lab.java_smt.test.SolverBasedTest0.ParameterizedSolverBasedTest0

parse(String) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Parse a boolean formula given as a String in an SMTLIB file format.

parse(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

parse(String) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

parseImpl(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

pop() - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Remove one backtracking point/level from the current stack.

pop() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

pop() - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

popImpl() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

POSITIVE - org.sosy_lab.java_smt.api.FloatingPointNumber.Sign

prefix(StringFormula, StringFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Check whether the given prefix is a real prefix of str.

prefix(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

prefix(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

prefix(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

prettyPrinter(FormulaManager) - Static method in class org.sosy_lab.java_smt.utils.SolverUtils

Creates a new PrettyPrinter instance.

PrettyPrinter - Class in org.sosy_lab.java_smt.example

This program parses user-given formulas and prints them in a pretty format.

PrettyPrinter - Class in org.sosy_lab.java_smt.utils

PrettyPrinter(FormulaManager) - Constructor for class org.sosy_lab.java_smt.utils.PrettyPrinter

PrettyPrinter.PrinterOption - Enum in org.sosy_lab.java_smt.utils

PRINCESS - org.sosy_lab.java_smt.SolverContextFactory.Solvers

propagateConflict(BooleanFormula[]) - Method in interface org.sosy_lab.java_smt.api.PropagatorBackend

Raises a conflict caused by a set of conflicting assignments.

propagateConsequence(BooleanFormula[], BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.PropagatorBackend

Propagates a consequence implied by a set of assigned expressions.

propagateNextDecision(BooleanFormula, Optional<Boolean>) - Method in interface org.sosy_lab.java_smt.api.PropagatorBackend

Propagates a decision to be made by the solver.

PropagatorBackend - Interface in org.sosy_lab.java_smt.api

The PropagatorBackend class is used by UserPropagator to implement custom user propagators.

ProverEnvironment - Interface in org.sosy_lab.java_smt.api

An interface to an incremental SMT solver with methods for pushing and popping formulas as well as SAT checks.

proverEnvironments() - Static method in class org.sosy_lab.java_smt.test.ProverEnvironmentSubject

Use this for checking assertions about ProverEnvironments with Truth: assert_().about(proverEnvironments()).that(stack).is...().

ProverEnvironmentSubject - Class in org.sosy_lab.java_smt.test

Subject subclass for testing assertions about ProverEnvironments with Truth (allows using assert_().about(...).that(stack).isUnsatisfiable() etc.).

ProverWithAssumptionsWrapper - Class in org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper

ProverWithAssumptionsWrapper(ProverEnvironment) - Constructor for class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.ProverWithAssumptionsWrapper

push() - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Create a new backtracking point, i.e., a new level on the assertion stack.

push() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

push() - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

push(BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Push a backtracking point and add a formula to the current stack, asserting it.

pushImpl() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

Q

QE_LIGHT - org.sosy_lab.java_smt.api.Tactic

Perform "best-effort" quantifier elimination: when the bound variable can be "cheaply" eliminated using a pattern-matching approach, eliminate it, and otherwise leave it as-is.

qmgr - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

QuantifiedFormulaManager - Interface in org.sosy_lab.java_smt.api

This interface contains methods for working with any theory with quantifiers.

QuantifiedFormulaManager.Quantifier - Enum in org.sosy_lab.java_smt.api

R

range(char, char) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

range(StringFormula, StringFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

range(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

range(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

range(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

RationalFormulaManager - Interface in org.sosy_lab.java_smt.api

Interface for operating over NumeralFormula.RationalFormula.

RationalType - Static variable in class org.sosy_lab.java_smt.api.FormulaType

RE_COMPLEMENT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

RE_CONCAT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

RE_DIFFERENCE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

RE_INTERSECT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

RE_OPTIONAL - org.sosy_lab.java_smt.api.FunctionDeclarationKind

RE_PLUS - org.sosy_lab.java_smt.api.FunctionDeclarationKind

RE_RANGE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

RE_STAR - org.sosy_lab.java_smt.api.FunctionDeclarationKind

RE_UNION - org.sosy_lab.java_smt.api.FunctionDeclarationKind

RegexFormula - Interface in org.sosy_lab.java_smt.api

A formula of the string sort.

RegexType - Static variable in class org.sosy_lab.java_smt.api.FormulaType

registerEvaluator(E) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

This method registers the Evaluator to be cleaned up before the next change on the prover stack.

registerExpression(BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.PropagatorBackend

Registers an expression to be observed by a UserPropagator.

registerExpression(BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.UserPropagator

Registers an expression to be observed by the UserPropagator.

registerExpression(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator

registerPushedFormula(T) - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

overridden in subclass.

registerPushedFormula(T) - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper

registerUserPropagator(UserPropagator) - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Registers a UserPropagator for this prover environment.

remainder(BitvectorFormula, BitvectorFormula, boolean) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns the remainder (remainder(dividend, divisor) == remainder) for the Euclidean division (dividend = quotient * divisor + remainder) of two bitvector formulas.

remainder(BitvectorFormula, BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

remainder(BitvectorFormula, BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

remainder(FloatingPointFormula, FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

remainder: x - y * n, where n in Z is nearest to x/y.

remainder(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

remainder(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

remainder(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

remainder(TFormulaInfo, TFormulaInfo, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

replace(StringFormula, StringFormula, StringFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Replace the first appearances of target in fullStr with the replacement.

replace(StringFormula, StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

replace(StringFormula, StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

replace(TFormulaInfo, TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

replaceAll(StringFormula, StringFormula, StringFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Replace all appearances of target in fullStr with the replacement.

replaceAll(StringFormula, StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

replaceAll(StringFormula, StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

replaceAll(TFormulaInfo, TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

requireArrayModel() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

requireArrays() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

Skip test if the solver does not support arrays.

requireBitvectors() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

Skip test if the solver does not support bitvectors.

requireBitvectorToInt() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

requireEnumeration() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

Skip test if the solver does not support enumeration theory.

requireFloats() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

requireFPToBitvector() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

requireIntegers() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

Skip test if the solver does not support integers.

requireInterpolation() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

requireModel() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

requireOptimization() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

Skip test if the solver does not support optimization.

requireParser() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

requireQuantifierElimination() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

requireQuantifiers() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

Skip test if the solver does not support quantifiers.

requireRationalFloor() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

requireRationals() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

Skip test if the solver does not support rationals.

requireStrings() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

Skip test if the solver does not support strings.

requireSubstitution() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

requireTheoryCombination() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

requireUfValuesInModel() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

requireUnsatCore() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

requireUnsatCoreOverAssumptions() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

requireUserPropagators() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

requireVisitor() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

rmgr - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

rotateLeft(BitvectorFormula, int) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns a term representing the left rotation (towards most-significant bit) of number by toRotate.

rotateLeft(BitvectorFormula, int) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

rotateLeft(BitvectorFormula, int) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

rotateLeft(BitvectorFormula, BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns a term representing the left rotation (towards most-significant bit) of number by toRotate.

rotateLeft(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

rotateLeft(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

rotateLeft(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

rotateLeftByConstant(TFormulaInfo, int) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

rotateRight(BitvectorFormula, int) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns a term representing the right rotation (towards least-significant bit) of number by toRotate.

rotateRight(BitvectorFormula, int) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

rotateRight(BitvectorFormula, int) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

rotateRight(BitvectorFormula, BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns a term representing the right rotation (towards least-significant bit) of number by toRotate.

rotateRight(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

rotateRight(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

rotateRight(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

rotateRightByConstant(TFormulaInfo, int) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

round(FloatingPointFormula, FloatingPointRoundingMode) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

round(FloatingPointFormula, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

round(FloatingPointFormula, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

round(TFormulaInfo, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

RowBuilder() - Constructor for class org.sosy_lab.java_smt.example.SolverOverviewTable.RowBuilder

The constructor builds the header of the table.

S

satTestBool5() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

select(ArrayFormula<TI, TE>, TI) - Method in interface org.sosy_lab.java_smt.api.ArrayFormulaManager

Read a value that is stored in the array at the specified position.

select(ArrayFormula<TI, TE>, TI) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager

select(ArrayFormula<TI, TE>, TI) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingArrayFormulaManager

select(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager

SELECT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

shiftLeft(BitvectorFormula, BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns a term representing the left shift (towards most-significant bit) of number by toShift.

shiftLeft(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

shiftLeft(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

shiftLeft(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

shiftRight(BitvectorFormula, BitvectorFormula, boolean) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns a term representing the right shift (towards least-significant bit) of number by toShift.

shiftRight(BitvectorFormula, BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

Return a term representing the (arithmetic if signed is true) right shift of number by toShift.

shiftRight(BitvectorFormula, BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

shiftRight(TFormulaInfo, TFormulaInfo, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

ShutdownHook - Class in org.sosy_lab.java_smt.basicimpl

A utility class for interrupting a parallel running solver thread.

ShutdownHook(ShutdownNotifier, Runnable) - Constructor for class org.sosy_lab.java_smt.basicimpl.ShutdownHook

shutdownManager - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

shutdownNotifier - Variable in class org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat

shutdownNotifierToUse() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

shutdownRequested(String) - Method in class org.sosy_lab.java_smt.basicimpl.ShutdownHook

simpleStackTestBool() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

SimpleUserPropagator - Class in org.sosy_lab.java_smt.example

Example of a simple user propagator that prohibits variables/expressions to be set to true.

simplify(T) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Simplify an input formula, while ensuring equivalence.

simplify(T) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

simplify(T) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

simplify(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

Apply a simplification procedure for the given formula.

SINGLE_PRECISION_EXPONENT_SIZE - Static variable in class org.sosy_lab.java_smt.api.FloatingPointNumber

Deprecated, for removal: This API element is subject to removal in a future version.

SINGLE_PRECISION_MANTISSA_SIZE - Static variable in class org.sosy_lab.java_smt.api.FloatingPointNumber

Deprecated, for removal: This API element is subject to removal in a future version.

this constant can be confusing, as the SMTLIB2 standard expects the mantissa to include the hidden bit, but this constant does not.

SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT - Static variable in class org.sosy_lab.java_smt.api.FloatingPointNumber

singleStackTestInteger() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

singleStackTestRational() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

size() - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Get the number of backtracking points/levels on the current stack.

size() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

size() - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

SIZE - Static variable in class org.sosy_lab.java_smt.example.Sudoku

SKIP - Static variable in class org.sosy_lab.java_smt.api.visitors.TraversalProcess

Continue traversal, but do not recurse into current formula subtree.

SKIP_TYPE - org.sosy_lab.java_smt.api.visitors.TraversalProcess.TraversalType

SLFormulaManager - Interface in org.sosy_lab.java_smt.api

The SLFormulaManager can build formulae for separation logic.

smgr - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0

smodulo(BitvectorFormula, BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns the two complement signed remainder (smodulo(dividend, divisor) == remainder) for the Euclidean division (dividend = quotient * divisor + remainder) of two bitvector formulas, with the sign of the remainder following the sign of the divisor.

smodulo(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

smodulo(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

smodulo(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

SMTINTERPOL - org.sosy_lab.java_smt.SolverContextFactory.Solvers

SMTLIB2_KEYWORDS - Static variable in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

Avoid using basic keywords of SMT-LIB2 as names for symbols.

solve(char[][]) - Method in class org.sosy_lab.java_smt.example.Binoxxo.BinoxxoSolver

Solves a Binoxxo using the given grid values and returns a possible solution.

solve(Integer[][]) - Method in class org.sosy_lab.java_smt.example.Sudoku.SudokuSolver

Solves a sudoku using the given grid values and returns a possible solution.

solver - Variable in class org.sosy_lab.java_smt.test.SolverBasedTest0.ParameterizedSolverBasedTest0

solverAssumptionsAsFormula - Variable in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

SolverBasedTest0 - Class in org.sosy_lab.java_smt.test

Abstract base class with helpful utilities for writing tests that use an SMT solver.

SolverBasedTest0() - Constructor for class org.sosy_lab.java_smt.test.SolverBasedTest0

SolverBasedTest0.ParameterizedSolverBasedTest0 - Class in org.sosy_lab.java_smt.test

SolverContext - Interface in org.sosy_lab.java_smt.api

Instances of this interface provide access to an SMT solver.

SolverContext.ProverOptions - Enum in org.sosy_lab.java_smt.api

Options for the prover environment.

SolverContextFactory - Class in org.sosy_lab.java_smt

Factory class for loading and generating solver contexts.

SolverContextFactory(Configuration, LogManager, ShutdownNotifier) - Constructor for class org.sosy_lab.java_smt.SolverContextFactory

This constructor uses the default JavaSMT loader for accessing native libraries.

SolverContextFactory(Configuration, LogManager, ShutdownNotifier, Consumer<String>) - Constructor for class org.sosy_lab.java_smt.SolverContextFactory

This constructor instantiates a factory for building solver contexts for a configured SMT solver (via the parameter pConfig).

SolverContextFactory.Solvers - Enum in org.sosy_lab.java_smt

SolverException - Exception in org.sosy_lab.java_smt.api

Exception thrown if there is an error during SMT solving.

SolverException(String) - Constructor for exception org.sosy_lab.java_smt.api.SolverException

SolverException(String, Throwable) - Constructor for exception org.sosy_lab.java_smt.api.SolverException

solverHasSharedFormulas(SolverContextFactory.Solvers) - Static method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverInformation

solverHasSharedFunctions(SolverContextFactory.Solvers) - Static method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingSolverInformation

SolverOverviewTable - Class in org.sosy_lab.java_smt.example

This program takes all installed solvers and checks them for version, theories and features and prints them to StdOut in a nice table.

SolverOverviewTable() - Constructor for class org.sosy_lab.java_smt.example.SolverOverviewTable

SolverOverviewTable.RowBuilder - Class in org.sosy_lab.java_smt.example

This class builds the table row-by-row.

SolverOverviewTable.SolverInfo - Class in org.sosy_lab.java_smt.example

just a wrapper for some data.

SolverStackTest0 - Class in org.sosy_lab.java_smt.test

SolverStackTest0() - Constructor for class org.sosy_lab.java_smt.test.SolverStackTest0

SolverStatistics - Class in org.sosy_lab.java_smt.delegate.statistics

solverToUse() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0.ParameterizedSolverBasedTest0

solverToUse() - Method in class org.sosy_lab.java_smt.test.SolverBasedTest0

Return the solver to use in this test.

SolverUtils - Class in org.sosy_lab.java_smt.utils

Central entry point for all utility classes.

SPLIT_ONLY_BOOLEAN_OPERATIONS - org.sosy_lab.java_smt.utils.PrettyPrinter.PrinterOption

introduce newlines only for boolean operations, instead of for all operations.

sqrt(FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

sqrt(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

sqrt(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

sqrt(FloatingPointFormula, FloatingPointRoundingMode) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

sqrt(FloatingPointFormula, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

sqrt(FloatingPointFormula, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

sqrt(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

stackTest() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

stackTest2() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

stackTest3() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

stackTest4() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

stackTest5() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

stackTestUnsat() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

stackTestUnsat2() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

start() - Method in class org.sosy_lab.java_smt.delegate.statistics.TimerPool.TimerWrapper

StatisticsEnumerationFormulaManager - Class in org.sosy_lab.java_smt.delegate.statistics

StatisticsSolverContext - Class in org.sosy_lab.java_smt.delegate.statistics

StatisticsSolverContext(SolverContext) - Constructor for class org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext

stop() - Method in class org.sosy_lab.java_smt.delegate.statistics.TimerPool.TimerWrapper

store(ArrayFormula<TI, TE>, TI, TE) - Method in interface org.sosy_lab.java_smt.api.ArrayFormulaManager

Store a value into a cell of the specified array.

store(ArrayFormula<TI, TE>, TI, TE) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager

store(ArrayFormula<TI, TE>, TI, TE) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingArrayFormulaManager

store(TFormulaInfo, TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager

STORE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Store and select on arrays, and constant initialization.

STR_CHAR_AT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_CONCAT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_CONTAINS - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_FROM_CODE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_IN_RE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_INDEX_OF - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_LE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_LENGTH - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_LT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_PREFIX - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_REPLACE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_REPLACE_ALL - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_SUBSTRING - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_SUFFIX - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_TO_CODE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_TO_INT - org.sosy_lab.java_smt.api.FunctionDeclarationKind

STR_TO_RE - org.sosy_lab.java_smt.api.FunctionDeclarationKind

StringFormula - Interface in org.sosy_lab.java_smt.api

A formula of the string sort.

StringFormulaManager - Interface in org.sosy_lab.java_smt.api

Manager for dealing with string formulas.

StringType - Static variable in class org.sosy_lab.java_smt.api.FormulaType

SUB - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Subtraction over integers and rationals.

substitute(T, Map<? extends Formula, ? extends Formula>) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Substitute every occurrence of any item from changeFrom in formula f to the corresponding occurrence from changeTo.

substitute(T, Map<? extends Formula, ? extends Formula>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

substitute(T, Map<? extends Formula, ? extends Formula>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

substring(StringFormula, NumeralFormula.IntegerFormula, NumeralFormula.IntegerFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Get a substring from the given String.

substring(StringFormula, NumeralFormula.IntegerFormula, NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

substring(StringFormula, NumeralFormula.IntegerFormula, NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

substring(TFormulaInfo, TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

subtract(BitvectorFormula, BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns the subtraction of the given bitvectors.

subtract(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

subtract(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

subtract(FloatingPointFormula, FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

subtract(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

subtract(FloatingPointFormula, FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

subtract(FloatingPointFormula, FloatingPointFormula, FloatingPointRoundingMode) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

subtract(FloatingPointFormula, FloatingPointFormula, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

subtract(FloatingPointFormula, FloatingPointFormula, FloatingPointRoundingMode) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

subtract(ParamFormulaType, ParamFormulaType) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

subtract(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

subtract(ParamFormulaType, ParamFormulaType) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

subtract(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

subtract(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

subtract(TFormulaInfo, TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

Sudoku - Class in org.sosy_lab.java_smt.example

This program parses user-given Sudoku and solves it with an SMT solver.

Sudoku.BooleanBasedSudokuSolver - Class in org.sosy_lab.java_smt.example

Sudoku.EnumerationBasedSudokuSolver - Class in org.sosy_lab.java_smt.example

Sudoku.IntegerBasedSudokuSolver - Class in org.sosy_lab.java_smt.example

Sudoku.SudokuSolver<S> - Class in org.sosy_lab.java_smt.example

suffix(StringFormula, StringFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Check whether the given suffix is a real suffix of str.

suffix(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

suffix(StringFormula, StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

suffix(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

sum(List<ParamFormulaType>) - Method in interface org.sosy_lab.java_smt.api.NumeralFormulaManager

sum(List<ParamFormulaType>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

sum(List<ParamFormulaType>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

sumImpl(List<TFormulaInfo>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

supportsAssumptionSolving() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractSolverContext

Whether the solver supports solving under some given assumptions (with all corresponding features) by itself, i.e., whether BasicProverEnvironment.isUnsatWithAssumptions(java.util.Collection) and BasicProverEnvironment.isUnsatWithAssumptions(java.util.Collection) are fully implemented.

symbolsOnStackTest() - Method in class org.sosy_lab.java_smt.test.SolverStackTest0

Create a symbol on a level and pop this level.

SynchronizedEnumerationFormulaManager - Class in org.sosy_lab.java_smt.delegate.synchronize

SynchronizedSolverContext - Class in org.sosy_lab.java_smt.delegate.synchronize

SynchronizedSolverContext(Configuration, LogManager, ShutdownNotifier, SolverContext) - Constructor for class org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext

T

Tactic - Enum in org.sosy_lab.java_smt.api

Tactic is a generic formula to formula transformation.

TimerPool - Class in org.sosy_lab.java_smt.delegate.statistics

TimerPool() - Constructor for class org.sosy_lab.java_smt.delegate.statistics.TimerPool

TimerPool.TimerWrapper - Class in org.sosy_lab.java_smt.delegate.statistics

A minimal wrapper to keep a reference on the timer and provide a limited view.

times(RegexFormula, int) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

times(RegexFormula, int) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

times(RegexFormula, int) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

TO_REAL - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Identity operation, converts from integers to rationals, also known as to_real.

toCodePoint(StringFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Returns an Integer formula representing the code point of the only character of the given String formula, if it represents a single character.

toCodePoint(StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

toCodePoint(StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

toCodePoint(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

toConjunction() - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Return a stream Collector that creates a conjunction of all elements in the stream.

toConjunction() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

toConjunction() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

toConjunctionArgs(BooleanFormula, boolean) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Return a set of formulas such that a conjunction over them is equivalent to the input formula.

toConjunctionArgs(BooleanFormula, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

toConjunctionArgs(BooleanFormula, boolean) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

toDisjunction() - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Return a stream Collector that creates a disjunction of all elements in the stream.

toDisjunction() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

toDisjunction() - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

toDisjunctionArgs(BooleanFormula, boolean) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Return a set of formulas such that a disjunction over them is equivalent to the input formula.

toDisjunctionArgs(BooleanFormula, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

toDisjunctionArgs(BooleanFormula, boolean) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

toIeeeBitvector(FloatingPointFormula) - Method in interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Create a formula that produces a representation of the given floating-point value as a bitvector conforming to the IEEE format.

toIeeeBitvector(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

toIeeeBitvector(FloatingPointFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

toIeeeBitvectorImpl(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

toIntegerFormula(BitvectorFormula, boolean) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Convert/Cast/Interpret a signed/unsigned bitvector formula as an integer formula.

toIntegerFormula(BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

toIntegerFormula(BitvectorFormula, boolean) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

toIntegerFormula(StringFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Interpret a String formula as an Integer formula.

toIntegerFormula(StringFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

toIntegerFormula(StringFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

toIntegerFormula(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

toIntegerFormulaImpl(TFormulaInfo, boolean) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

tokenize(String) - Static method in class org.sosy_lab.java_smt.basicimpl.Tokenizer

Split up a sequence of lisp expressions.

Tokenizer - Class in org.sosy_lab.java_smt.basicimpl

Helper class for splitting up an SMT-LIB2 file into a string of commands.

toSMTLIBString() - Method in class org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType

toSMTLIBString() - Method in class org.sosy_lab.java_smt.api.FormulaType.BitvectorType

toSMTLIBString() - Method in class org.sosy_lab.java_smt.api.FormulaType.EnumerationFormulaType

toSMTLIBString() - Method in class org.sosy_lab.java_smt.api.FormulaType.FloatingPointType

toSMTLIBString() - Method in class org.sosy_lab.java_smt.api.FormulaType

return the correctly formatted SMTLIB2 type declaration.

toString() - Method in class org.sosy_lab.java_smt.api.FloatingPointNumber

Return a bit-representation of sign-bit, exponent, and mantissa, i.e., a concatenation of their bit-representations in this exact ordering.

toString() - Method in interface org.sosy_lab.java_smt.api.Formula

returns an arbitrary representation of the formula, might be human- or machine-readable.

toString() - Method in class org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType

toString() - Method in class org.sosy_lab.java_smt.api.FormulaType.BitvectorType

toString() - Method in class org.sosy_lab.java_smt.api.FormulaType.EnumerationFormulaType

toString() - Method in class org.sosy_lab.java_smt.api.FormulaType.FloatingPointType

toString() - Method in class org.sosy_lab.java_smt.api.FormulaType

toString() - Method in interface org.sosy_lab.java_smt.api.Model

Pretty-printing of the model values.

toString() - Method in class org.sosy_lab.java_smt.api.Model.ValueAssignment

toString() - Method in class org.sosy_lab.java_smt.basicimpl.AbstractModel

toString() - Method in class org.sosy_lab.java_smt.basicimpl.CachingModel

toString() - Method in class org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl

toString() - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

toString() - Method in class org.sosy_lab.java_smt.delegate.statistics.TimerPool

toString() - Method in class org.sosy_lab.java_smt.example.FormulaClassifier

toString() - Method in class org.sosy_lab.java_smt.example.SolverOverviewTable.RowBuilder

toStringFormula(NumeralFormula.IntegerFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

Interpret an Integer formula as a String formula.

toStringFormula(NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

toStringFormula(NumeralFormula.IntegerFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

toStringFormula(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

toType(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

Make sure the value is of correct type (Int vs.

TOWARD_NEGATIVE - org.sosy_lab.java_smt.api.FloatingPointRoundingMode

TOWARD_POSITIVE - org.sosy_lab.java_smt.api.FloatingPointRoundingMode

TOWARD_ZERO - org.sosy_lab.java_smt.api.FloatingPointRoundingMode

transformRecursively(BooleanFormula, BooleanFormulaTransformationVisitor) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Visit the formula recursively with a given BooleanFormulaVisitor.

transformRecursively(BooleanFormula, BooleanFormulaTransformationVisitor) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

transformRecursively(BooleanFormula, BooleanFormulaTransformationVisitor) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

transformRecursively(FormulaVisitor<? extends Formula>, T) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

transformRecursively(FormulaVisitor<? extends Formula>, T, Predicate<Object>) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

transformRecursively(T, FormulaTransformationVisitor) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Visit the formula recursively with a given FormulaVisitor.

transformRecursively(T, FormulaTransformationVisitor) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

transformRecursively(T, FormulaTransformationVisitor) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

transformValueToRange(int, BigInteger) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

transform a negative value into its positive counterpart.

translateFrom(BooleanFormula, FormulaManager) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Translates the formula from another context into the context represented by this.

translateFrom(BooleanFormula, FormulaManager) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

translateFrom(BooleanFormula, FormulaManager) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

TraversalProcess - Class in org.sosy_lab.java_smt.api.visitors

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 - Enum in org.sosy_lab.java_smt.api.visitors

TSEITIN_CNF - org.sosy_lab.java_smt.api.Tactic

Convert the formula to CNF (conjunctive normal form), using extra fresh variables to avoid the size explosion.

U

UF - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Uninterpreted function.

ufElimination(FormulaManager) - Static method in class org.sosy_lab.java_smt.utils.SolverUtils

Creates a new UfElimination instance.

UfElimination - Class in org.sosy_lab.java_smt.utils

UfElimination replaces UFs by fresh variables and adds constraints to enforce the functional consistency.

UfElimination.Result - Class in org.sosy_lab.java_smt.utils

UFManager - Interface in org.sosy_lab.java_smt.api

Manager for dealing with uninterpreted functions (UFs).

UMINUS - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Unary minus.

UNDEF - org.sosy_lab.java_smt.api.OptimizationProverEnvironment.OptStatus

The result is unknown.

unescape(String) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Unescape the symbol/name for variables or undefined functions, if necessary.

unescape(String) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

unescape(String) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

unescapeUnicodeForSmtlib(String) - Static method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

Replace escaped Unicode letters in SMTLIB representation with their UTF16 pendant.

union(RegexFormula, RegexFormula) - Method in interface org.sosy_lab.java_smt.api.StringFormulaManager

union(RegexFormula, RegexFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

union(RegexFormula, RegexFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

union(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

unregisterEvaluator(Evaluator) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractProver

UNSAT - org.sosy_lab.java_smt.api.OptimizationProverEnvironment.OptStatus

The set of constraints is unsatisfiable.

unsatCoreOverAssumptions(Collection<BooleanFormula>) - Method in interface org.sosy_lab.java_smt.api.BasicProverEnvironment

Returns an UNSAT core (if it exists, otherwise Optional.empty()), over the chosen assumptions.

unsatCoreOverAssumptions(Collection<BooleanFormula>) - Method in class org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper

upper(int, Rational) - Method in interface org.sosy_lab.java_smt.api.OptimizationProverEnvironment

upper(int, Rational) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingOptimizationProverEnvironment

USE - org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic

UserPropagator - Interface in org.sosy_lab.java_smt.api

Allows user-defined propagators (~ theory solvers) to be implemented.

V

ValueAssignment(Formula, Formula, BooleanFormula, String, Object, List<?>) - Constructor for class org.sosy_lab.java_smt.api.Model.ValueAssignment

valueOf(String) - Static method in enum org.sosy_lab.java_smt.api.FloatingPointNumber.Sign

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum org.sosy_lab.java_smt.api.FloatingPointRoundingMode

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum org.sosy_lab.java_smt.api.FunctionDeclarationKind

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum org.sosy_lab.java_smt.api.OptimizationProverEnvironment.OptStatus

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum org.sosy_lab.java_smt.api.SolverContext.ProverOptions

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum org.sosy_lab.java_smt.api.Tactic

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum org.sosy_lab.java_smt.api.visitors.TraversalProcess.TraversalType

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum org.sosy_lab.java_smt.SolverContextFactory.Solvers

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum org.sosy_lab.java_smt.utils.PrettyPrinter.PrinterOption

Returns the enum constant of this type with the specified name.

values() - Static method in enum org.sosy_lab.java_smt.api.FloatingPointNumber.Sign

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum org.sosy_lab.java_smt.api.FloatingPointRoundingMode

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum org.sosy_lab.java_smt.api.FunctionDeclarationKind

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum org.sosy_lab.java_smt.api.OptimizationProverEnvironment.OptStatus

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum org.sosy_lab.java_smt.api.SolverContext.ProverOptions

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum org.sosy_lab.java_smt.api.Tactic

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum org.sosy_lab.java_smt.api.visitors.TraversalProcess.TraversalType

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum org.sosy_lab.java_smt.SolverContextFactory.Solvers

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum org.sosy_lab.java_smt.utils.PrettyPrinter.PrinterOption

Returns an array containing the constants of this enum type, in the order they are declared.

VAR - org.sosy_lab.java_smt.api.FunctionDeclarationKind

User-defined variable.

visit(BooleanFormula) - Method in class org.sosy_lab.java_smt.example.FormulaClassifier

visit(BooleanFormula, BooleanFormulaVisitor<R>) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Visit the formula with the given visitor.

visit(BooleanFormula, BooleanFormulaVisitor<R>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

visit(BooleanFormula, BooleanFormulaVisitor<R>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

visit(Formula, FormulaVisitor<R>) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Visit the formula with a given visitor.

visit(Formula, FormulaVisitor<R>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

visit(Formula, FormulaVisitor<R>) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

visit(Formula, FormulaVisitor<R>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

visit(FormulaVisitor<R>, Formula, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

visitAnd(List<BooleanFormula>) - Method in class org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor

visitAnd(List<BooleanFormula>) - Method in interface org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor

Visit an AND-expression with an arbitrary number of boolean arguments.

visitAnd(List<BooleanFormula>) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor

visitAtom(BooleanFormula, FunctionDeclaration<BooleanFormula>) - Method in class org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor

visitAtom(BooleanFormula, FunctionDeclaration<BooleanFormula>) - Method in interface org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor

Visit an SMT atom.

visitAtom(BooleanFormula, FunctionDeclaration<BooleanFormula>) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor

visitBoundVar(BooleanFormula, int) - Method in interface org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor

Deprecated.

visitBoundVariable(Formula, int) - Method in interface org.sosy_lab.java_smt.api.visitors.FormulaVisitor

Deprecated.

visitConstant(boolean) - Method in class org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor

visitConstant(boolean) - Method in interface org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor

Visit a constant with a given value.

visitConstant(boolean) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor

visitConstant(Formula, Object) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor

visitConstant(Formula, Object) - Method in class org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor

visitConstant(Formula, Object) - Method in interface org.sosy_lab.java_smt.api.visitors.FormulaVisitor

Visit a constant, such as "true"/"false", a numeric constant like "1" or "1.0", a String constant like 2hello world" or enumeration constant like "Blue".

visitDefault() - Method in class org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor

visitDefault(Formula) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor

Method for default case, is called by all methods from this class if they are not overridden.

visitDefault(Formula) - Method in class org.sosy_lab.java_smt.api.visitors.ExpectedFormulaVisitor

visitEquivalence(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor

visitEquivalence(BooleanFormula, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor

Visit an equivalence between two formulas of boolean sort: operand1 = operand2.

visitEquivalence(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor

visitEquivalence(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.tactics.NNFVisitor

visitFreeVariable(Formula, String) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor

visitFreeVariable(Formula, String) - Method in class org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor

visitFreeVariable(Formula, String) - Method in interface org.sosy_lab.java_smt.api.visitors.FormulaVisitor

Visit a free variable (such as "x", "y" or "z"), not bound by a quantifier.

visitFunction(Formula, List<Formula>, FunctionDeclaration<?>) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor

visitFunction(Formula, List<Formula>, FunctionDeclaration<?>) - Method in class org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor

visitFunction(Formula, List<Formula>, FunctionDeclaration<?>) - Method in interface org.sosy_lab.java_smt.api.visitors.FormulaVisitor

Visit an arbitrary, potentially uninterpreted function.

visitIfThenElse(BooleanFormula, BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor

visitIfThenElse(BooleanFormula, BooleanFormula, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor

Visit an if-then-else expression.

visitIfThenElse(BooleanFormula, BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor

visitIfThenElse(BooleanFormula, BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.tactics.NNFVisitor

visitImplication(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor

visitImplication(BooleanFormula, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor

Visit an implication.

visitImplication(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor

visitImplication(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.tactics.NNFVisitor

visitNot(BooleanFormula) - Method in class org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor

visitNot(BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor

Visit a NOT-expression.

visitNot(BooleanFormula) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor

visitNot(BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.tactics.NNFVisitor

visitOr(List<BooleanFormula>) - Method in class org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor

visitOr(List<BooleanFormula>) - Method in interface org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor

Visit an OR-expression with an arbitrary number of boolean arguments.

visitOr(List<BooleanFormula>) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor

visitQuantifier(BooleanFormula, QuantifiedFormulaManager.Quantifier, List<Formula>, BooleanFormula) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor

visitQuantifier(BooleanFormula, QuantifiedFormulaManager.Quantifier, List<Formula>, BooleanFormula) - Method in class org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor

visitQuantifier(BooleanFormula, QuantifiedFormulaManager.Quantifier, List<Formula>, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.visitors.FormulaVisitor

Visit a quantified node.

visitQuantifier(QuantifiedFormulaManager.Quantifier, BooleanFormula, List<Formula>, BooleanFormula) - Method in class org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor

visitQuantifier(QuantifiedFormulaManager.Quantifier, BooleanFormula, List<Formula>, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor

Visit a quantifier: forall- or exists-.

visitQuantifier(QuantifiedFormulaManager.Quantifier, BooleanFormula, List<Formula>, BooleanFormula) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor

visitRecursively(BooleanFormula, BooleanFormulaVisitor<TraversalProcess>) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Visit the formula recursively with a given BooleanFormulaVisitor.

visitRecursively(BooleanFormula, BooleanFormulaVisitor<TraversalProcess>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

visitRecursively(BooleanFormula, BooleanFormulaVisitor<TraversalProcess>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

visitRecursively(Formula, FormulaVisitor<TraversalProcess>) - Method in interface org.sosy_lab.java_smt.api.FormulaManager

Visit the formula recursively with a given FormulaVisitor.

visitRecursively(Formula, FormulaVisitor<TraversalProcess>) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager

visitRecursively(Formula, FormulaVisitor<TraversalProcess>) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

visitRecursively(FormulaVisitor<TraversalProcess>, Formula) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

visitRecursively(FormulaVisitor<TraversalProcess>, Formula, Predicate<Formula>) - Method in class org.sosy_lab.java_smt.basicimpl.FormulaCreator

visitXor(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor

visitXor(BooleanFormula, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor

Visit an XOR-expression.

visitXor(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor

visitXor(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.tactics.NNFVisitor

W

wrap(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager

wrap(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager

wrapInteger(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

wrapRegex(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

wrapString(TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager

X

xor(BitvectorFormula, BitvectorFormula) - Method in interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

This method returns the bit-wise XOR of the given bitvectors.

xor(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

xor(BitvectorFormula, BitvectorFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

xor(BooleanFormula, BooleanFormula) - Method in interface org.sosy_lab.java_smt.api.BooleanFormulaManager

Creates a formula representing XOR of the two arguments.

xor(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

xor(BooleanFormula, BooleanFormula) - Method in class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

xor(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager

xor(TFormulaInfo, TFormulaInfo) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

XOR - org.sosy_lab.java_smt.api.FunctionDeclarationKind

Exclusive OR over two formulas.

Y

YICES2 - org.sosy_lab.java_smt.SolverContextFactory.Solvers

Z

Z3 - org.sosy_lab.java_smt.SolverContextFactory.Solvers

A B C D E F G H I L M N O P Q R S T U V W X Y Z
All Classes All Packages