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...) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

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

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

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

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

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

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.

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

DebuggingArrayFormulaManager(ArrayFormulaManager, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingArrayFormulaManager

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

DebuggingBitvectorFormulaManager(BitvectorFormulaManager, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

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

DebuggingBooleanFormulaManager(BooleanFormulaManager, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingBooleanFormulaManager

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

DebuggingEnumerationFormulaManager(EnumerationFormulaManager, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingEnumerationFormulaManager

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

DebuggingFloatingPointFormulaManager(FloatingPointFormulaManager, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

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

DebuggingFormulaManager(FormulaManager, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingFormulaManager

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

DebuggingIntegerFormulaManager(IntegerFormulaManager, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingIntegerFormulaManager

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

DebuggingInterpolatingProverEnvironment(InterpolatingProverEnvironment<T>, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingInterpolatingProverEnvironment

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

DebuggingModel(Model, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingModel

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

DebuggingNumeralFormulaManager(NumeralFormulaManager<ParamFormulaType, ResultFormulaType>, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

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

DebuggingOptimizationProverEnvironment(OptimizationProverEnvironment, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingOptimizationProverEnvironment

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

DebuggingProverEnvironment(BasicProverEnvironment<Void>, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingProverEnvironment

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

DebuggingQuantifiedFormulaManager(QuantifiedFormulaManager, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingQuantifiedFormulaManager

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

DebuggingRationalFormulaManager(RationalFormulaManager, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingRationalFormulaManager

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

DebuggingSLFormulaManager(SLFormulaManager, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingSLFormulaManager

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

DebuggingStringFormulaManager(StringFormulaManager, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

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

DebuggingUFManager(UFManager, DebuggingAssertions) - Constructor for class org.sosy_lab.java_smt.delegate.debugging.DebuggingUFManager

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.

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

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

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

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

DOUBLE_PRECISION_MANTISSA_SIZE - 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).

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

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(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

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

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.

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

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

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

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

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.

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

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

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

Whether the number is positive (TRUE) or negative (FALSE).

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

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

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 52 bit mantissa and a single sign 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 23 bit mantissa and a single sign bit.

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

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

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(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

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

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

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

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

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

Creates a floating point formula from the given exponent, mantissa, and sign bit with the specified type.

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

makeNumber(BigInteger, BigInteger, boolean, 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

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

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, boolean, 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

Returns a StringFormula representing the given constant.

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

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

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.

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

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, BigInteger, BigInteger, int, int) - Static method in class org.sosy_lab.java_smt.api.FloatingPointNumber

of(String, int, int) - Static method in class org.sosy_lab.java_smt.api.FloatingPointNumber

of(String, FunctionDeclarationKind, List<FormulaType<?>>, FormulaType<F>, T) - Static method in class org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl

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 (may be 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...) - Method in class org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager

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

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

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 sub-class.

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 for two bitvector formulas using the BitvectorFormulaManager.divide(BitvectorFormula, BitvectorFormula, boolean) operation.

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

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

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

SINGLE_PRECISION_MANTISSA_SIZE - 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 for the Euclidean division (modulo) of two bitvector formulas.

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

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

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

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.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.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 class org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor

visitBoundVar(BooleanFormula, int) - Method in interface org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor

Visit a boolean variable bound by a quantifier.

visitBoundVar(BooleanFormula, int) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor

visitBoundVariable(Formula, int) - Method in class org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor

visitBoundVariable(Formula, int) - Method in class org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor

visitBoundVariable(Formula, int) - Method in interface org.sosy_lab.java_smt.api.visitors.FormulaVisitor

Visit a variable bound by a quantifier.

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 a 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

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