Index (SARL 2.0 main 56 [557c7b9])

A B C D E F G H I J K L M N O P Q R S T U V W Y Z
All Classes and Interfaces|All Packages|Serialized Form

A

abs(Number) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns absolute value of number, preserving type.
add(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a symbolic expression which is the result of adding arg1 from arg0.
add(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory
add(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a symbolic expression which is the result of adding the two given symbolic expressions.
add(IntegerNumber, IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Adds two integer numbers and returns the result.
add(Interval, Interval) - Method in interface dev.civl.sarl.IF.number.NumberFactory: To calculate the sum of two non-null and not empty Interval with same type (real/integer)
add(Number, Number) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Adds two numbers and returns result.
add(RationalNumber, RationalNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Adds two rational numbers and returns the result.
add(Range, Number) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Return a Range containing all x+constant, where x is in range and constant is a non- null finite Number.
add(Range, Range) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Return a Range containing all x+y, where x is in range0 and y is in range1.
add(Iterable<? extends NumericExpression>) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a symbolic expression representing the sum of the given argument sequence.
add(T) - Method in interface dev.civl.sarl.IF.object.SymbolicSequence: Appends an element to the end of a sequence.
ADD - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the sum of its arguments.
addAlias(String) - Method in interface dev.civl.sarl.IF.config.ProverInfo: Adds the given string to the set of aliases.
addMonomials(Monomial[]) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Computes the sum of a non-empty set of Monomials of the same type.
addMonomials(Monomial, Monomial) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Computes the sum of any two Monomials of the same type.
addOption(String) - Method in interface dev.civl.sarl.IF.config.ProverInfo: Adds the given string to the end of the list of options.
addTermMaps(Monomial[], Monomial[]) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Computes the sum of two term maps as a term map.
affineTransform(Interval, Number, Number) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Computes the affineTransform of the input interval itv with two numbers: a and b as parameters.
affineTransform(Range, Number, Number) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Return a Range containing all x*a+b, where x is in range, a and b are Numbers.
aggressivelySimplifyTopContext(Set<SymbolicConstant>) - Method in interface dev.civl.sarl.IF.Reasoner
ALL - Enum constant in enum class dev.civl.sarl.simplify.IF.Range.RangeSign: The range contains at least a negative number and a positive number (0 is optionally contained)
ALT_ERGO - Enum constant in enum class dev.civl.sarl.IF.config.ProverInfo.ProverKind: Alt-Ergo, https://alt-ergo.ocamlpro.com.
and(BooleanExpression, BooleanExpression) - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory: Returns a symbolic expression representing the conjunction of the two given arguments.
and(BooleanExpression, BooleanExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a symbolic expression representing the conjunction of the two given arguments.
and(Iterable<? extends BooleanExpression>) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a symbolic expression which represents the conjunction of the expressions in the given array args.
AND - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the conjunction of symbolic expressions of boolean type.
append(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Appends an element to the end of a concrete symbolic array.
apply(SymbolicExpression, Iterable<? extends SymbolicExpression>) - Method in interface dev.civl.sarl.IF.CoreUniverse: The result of applying an uninterpreted function to a sequence of arguments.
apply(Transform<T, U>) - Method in interface dev.civl.sarl.IF.object.SymbolicSequence: Returns a sequence obtained by applying a function to every element of this sequence; also known as "map".
apply(S) - Method in interface dev.civl.sarl.IF.Transform: Apply this Transform to the element x of S.
apply(T) - Method in interface dev.civl.sarl.IF.Predicate: Apply this predicate to the element x of T.
APPLY - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the application of a function to some arguments.
argument(int) - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression: Returns the i-th argument (child) of the operator.
array(SymbolicType, SymbolicExpression[]) - Method in interface dev.civl.sarl.IF.CoreUniverse: Creates a concrete array expression backed by the given Java array.
array(SymbolicType, Iterable<? extends SymbolicObject>) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the concrete array consisting of given sequence of elements.
ARRAY - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: A concrete array.
ARRAY - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicType.SymbolicTypeKind
ARRAY_ELEMENT - Enum constant in enum class dev.civl.sarl.IF.expr.ReferenceExpression.ReferenceKind: An array element of reference.
ARRAY_ELEMENT - Enum constant in enum class dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference.VSReferenceKind: An array element of reference.
ARRAY_LAMBDA - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an array expression of type T[] formed by providing a function f from integers to T.
ARRAY_READ - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the result of reading an element from an array.
ARRAY_SECTION - Enum constant in enum class dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference.VSReferenceKind: An reference to a "section" of an array.
ARRAY_WRITE - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the array resulting from modifying a single element of an array.
arrayDimensionAndBaseType(SymbolicArrayType) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the dimension and base type of an array type.
arrayElementReference(ReferenceExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Given a reference to an array and an index (integer), returns a reference to the element of the array at that index
arrayElementReference(ReferenceExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given a reference to an array and an index (integer), returns a reference to the element of the array at that index.
ArrayElementReference - Interface in dev.civl.sarl.IF.expr: A reference to an element of an array.
arrayLambda(SymbolicCompleteArrayType, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns an expression representing an array with element type T defined by a function f from int to T.
arrayRead(SymbolicExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns an expression representing the value of the element of the array at position index.
arrayReadCondSimplify - Static variable in class dev.civl.sarl.IF.SARLConstants: Simplifies an expression such as (a WITH i:=x)[j] to i==j?x:a[j].
arrayType(SymbolicType) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the incomplete array type with the given element type.
arrayType(SymbolicType) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory: Creates a SymbolicArrayType that has elements of type elementType
arrayType(SymbolicType, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the complete array type with the given element type and extent (array length).
arrayType(SymbolicType, NumericExpression) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory: Creates a SymbolicCompleteArrayType
arrayWrite(SymbolicExpression, NumericExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns an expression representing the result of modifying an array by changing the value at position index.
asInterval() - Method in interface dev.civl.sarl.simplify.IF.Range: If this range is an interval, return the Interval representation, otherwise, returns null.
assign(SymbolicExpression, ReferenceExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given a symbolic expression value, a reference to a point within that value, and a subValue, returns the symbolic expression obtained by replacing the referenced part of value with subValue.
assumptionAsInterval(SymbolicConstant) - Method in interface dev.civl.sarl.IF.Reasoner: If the context can be represented as a simple interval constraint, i.e., an expression of the form A invalid input: '<'= x invalid input: '<'= B, where A and B are concrete numbers, x is the given symbolic constant, and invalid input: '<'= could be invalid input: '<' in either case, this returns the interval [A,B] (or (A,B], or, ...).
atomString() - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression: A string representation appropriate for nesting in other expressions, typically by surrounding the normal string version with parentheses if necessary.
atomString() - Method in interface dev.civl.sarl.IF.number.Number: The string representation used when this number appears inside of another expression.

B

baseType() - Method in interface dev.civl.sarl.IF.type.SymbolicArrayType
bigIntegerValue() - Method in interface dev.civl.sarl.IF.number.IntegerNumber: Returns this integer as an instance of Java's BigInteger.
If this number is infinite, it will return null;
BIT_AND - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the result of applying bit-wise and operation on two given unsigned integers.
BIT_NOT - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the result of applying bit-wise not operation on the given unsigned integers.
BIT_OR - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the result of applying bit-wise or operation on two given unsigned integers.
BIT_SHIFT_LEFT - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the result of applying bit-wise left shifting operation on two given values.
BIT_SHIFT_RIGHT - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the result of applying bit-wise right shifting operation on two given values.
BIT_XOR - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the result of applying bit-wise exclusive-or operation on two given unsigned integers.
bitand(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the result of bit-and operation for two given unsigned integers, those two unsigned integers are in the form of NumericExpression.
bitnot(NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the result of bit-not operation for the given unsigned integer, the given unsigned integer is in the form of NumericExpression.
bitor(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the result of bit-or operation for two given unsigned integers, those two unsigned integers are in the form of NumericExpression.
bitshiftLeft(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the result of bit-left-shift operation for the given unsigned integer, the given unsigned integer is in the form of NumericExpression.
bitshiftRight(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the result of bit-right-shift operation for the given unsigned integer, the given unsigned integer is in the form of NumericExpression.
bitvector2Integer(SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Converts a bit vector to an integer.
bitVectorType(int) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the SymbolicCompleteArrayType representing a bitVectorType, which is an array of booleans with concrete length.
bitxor(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the result of bit-xor operation for two given unsigned integers, those two unsigned integers are in the form of NumericExpression.
body - Variable in class dev.civl.sarl.IF.CoreUniverse.ForallStructure: The body of the expression: the boolean formula that is claimed to hold if i is between the lower and upper bounds (inclusive).
bool(boolean) - Method in interface dev.civl.sarl.IF.CoreUniverse: Short cut for symbolic(booleanObject(value)).
bool(BooleanObject) - Method in interface dev.civl.sarl.IF.CoreUniverse: The symbolic expression wrapping the given boolean object (true or false).
BOOLEAN - Enum constant in enum class dev.civl.sarl.IF.object.SymbolicObject.SymbolicObjectKind
BOOLEAN - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicType.SymbolicTypeKind
booleanExpression(SymbolicExpression.SymbolicOperator, SymbolicObject...) - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory: Returns an expression, given the operator and an array of arguments
BooleanExpression - Interface in dev.civl.sarl.IF.expr: A symbolic expression of boolean type.
BooleanExpressionFactory - Interface in dev.civl.sarl.expr.IF
booleanFactory() - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Returns the boolean expression factory used by this expression factory.
booleanFactory() - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns the boolean expression factory used by this numeric expression factory.
booleanFactory() - Method in interface dev.civl.sarl.preuniverse.IF.FactorySystem
booleanObject(boolean) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the BooleanObject wrapping the given boolean value.
booleanObject(boolean) - Method in interface dev.civl.sarl.object.IF.ObjectFactory
BooleanObject - Interface in dev.civl.sarl.IF.object: A symbolic object wrapping a single boolean value.
booleanSymbolicConstant(StringObject) - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory
BooleanSymbolicConstant - Interface in dev.civl.sarl.IF.expr: A SymbolicConstant of boolean type.
booleanType() - Method in interface dev.civl.sarl.IF.CoreUniverse: The boolean type.
booleanType() - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory
BOUNDED - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicIntegerType.IntegerKind
boundedIntegerType(NumericExpression, NumericExpression, boolean) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the bounded integer types with specified upper and lower bounds.
boundedIntegerType(NumericExpression, NumericExpression, boolean) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory
boundVariable - Variable in class dev.civl.sarl.IF.CoreUniverse.ForallStructure: The integer bound variable used in the forall expression.

C

canonic(T) - Method in interface dev.civl.sarl.object.IF.ObjectFactory: Returns the canonic representative of the object's equivalence class.
canonicalRenamer(String) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns an operator on SymbolicExpressions that replaces all symbolic constants (including bound ones) with symbolic constants with unique canonical names.
canonicalRenamer(String, Predicate<SymbolicConstant>) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns an operator on SymbolicExpressions that replaces all symbolic constants (including bound ones) with symbolic constants with unique canonical names.
CanonicalRenamer - Interface in dev.civl.sarl.IF: A substituter used to assign new, canonical names to all symbolic constants occurring in a sequence of expressions.
canonize(T[]) - Method in interface dev.civl.sarl.object.IF.ObjectFactory: Canonizes each object in an array.
cardinality(SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse
cast(NumericExpression, SymbolicType) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a NumericExpression with the symbolic type passed in the second argument
cast(SymbolicType, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Casts expression to new type.
CAST - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the result of converting a value from one type to another.
ceil(NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory
ceil(NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given an expression x of real type, returns an expression of integer type representing the least integer greater than or equal to x.
ceil(RationalNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns the least integer greater than or equal to the given rational number.
CHAR - Enum constant in enum class dev.civl.sarl.IF.object.SymbolicObject.SymbolicObjectKind
CHAR - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicType.SymbolicTypeKind
character(char) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a concrete symbolic expression of character type which wraps the given Java char.
characterType() - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the character type.
characterType() - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory
charObject(char) - Method in interface dev.civl.sarl.object.IF.ObjectFactory
charObject(char) - Method in interface dev.civl.sarl.preuniverse.IF.PreUniverse: Returns the charObject wrapping the given char value.
CharObject - Interface in dev.civl.sarl.IF.object: A symbolic object wrapping a single char value.
checkBigOClaim(BooleanExpression, NumericExpression, NumericSymbolicConstant[], int[]) - Method in interface dev.civl.sarl.IF.Reasoner: Attempts to prove a uniform "Big-O" claim.
cleanBoundVariables(SymbolicExpression) - Method in interface dev.civl.sarl.preuniverse.IF.PreUniverse: Changes the names of the bound variables in the expression so that every bound variable has a unique name.
cloneBoundCleaner(UnaryOperator<SymbolicExpression>) - Method in interface dev.civl.sarl.preuniverse.IF.PreUniverse
comparator() - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Returns a comparator on all SymbolicExpression objects.
comparator() - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a comparator on all numeric expressions that are controlled by this factory
comparator() - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a comparator on the set of all symbolic objects.
comparator() - Method in interface dev.civl.sarl.object.IF.ObjectFactory: Returns a Comparator on all SymbolicObjects.
compare(IntegerNumber, IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns a positive value if arg0 is greater than arg1, 0 if arg0 equals arg1, -1 if arg0 is less than arg1.
compare(Interval, Interval) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Computes the relationships of two Intervals.
compare(Number) - Method in interface dev.civl.sarl.IF.number.Interval: Determines when the given number lies to the left, inside, or to the right of this interval.
compare(Number, Number) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns a positive value if arg0 is greater than arg1, 0 if arg0 equals arg1, a negative value if arg0 is less than arg1.
compare(RationalNumber, RationalNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns a positive value if arg0>arg1, 0 if arg0 equals arg1, -1 if arg0invalid input: '<'arg1.
compareTo(ProverFunctionInterpretation) - Method in class dev.civl.sarl.prove.IF.ProverFunctionInterpretation
compatible(SymbolicType, SymbolicType) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a boolean expression which holds iff the two types are compatible.
complement(Range) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Return the complement Range of the input range.
CONCRETE - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: TODO: this will go away in the refactoring.
concreteValueOfUninterpretedType(SymbolicUninterpretedType, IntObject) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a symbolic expression of a SymbolicUninterpretedType.
cond(BooleanExpression, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: "If-then-else" expression.
COND - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for a conditional expression, also known as "if-then-else", as in C's ternary expression arg0 ? arg1 : arg2.
Configurations - Class in dev.civl.sarl.IF.config: This is the public interface for managing SARL configuration objects and files.
Configurations() - Constructor for class dev.civl.sarl.IF.config.Configurations
constant(Number) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Returns a Constant wrapping the given concrete Number.
Constant - Interface in dev.civl.sarl.ideal.IF: A constant, i.e., a concrete number.
constantArray(SymbolicType, NumericExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns an array in which every element has the same value.
constantSubstituter(Map<SymbolicConstant, SymbolicExpression>) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a substituter for which the base substitutions are specified by an explicit Java Map.
constantSubstitutionMap() - Method in interface dev.civl.sarl.IF.Reasoner: In the process of simplifying the initial context, this simplifier may have "solved" for some of the symbolic constants occurring in the context.
constantTerm(IdealFactory) - Method in interface dev.civl.sarl.ideal.IF.Polynomial: The constant term of this polynomial, which may be 0.
contains(Number) - Method in interface dev.civl.sarl.IF.number.Interval: Does this interval contain the given number? The behavior is unspecified if this method is given a number which has a different type from that of this interval.
contains(Range) - Method in interface dev.civl.sarl.simplify.IF.Range: Is this set a superset of the given one?
containsArgument(BooleanExpression, SymbolicObject) - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory: Is one of the arguments of the given expression equal to arg?
containsNumber(Number) - Method in interface dev.civl.sarl.simplify.IF.Range: Does this set contain the given number as a member?
containsQuantifier() - Method in interface dev.civl.sarl.IF.object.SymbolicObject: Does this symbolic object contain a quantified expression anywhere in its structure?
containsSubobject(SymbolicObject) - Method in interface dev.civl.sarl.IF.object.SymbolicObject: Does this symbolic object contain a sub-object equal to the given one?
containsSubobjectIgnoringType(SymbolicObject) - Method in interface dev.civl.sarl.IF.object.SymbolicObject
ContextPartition - Interface in dev.civl.sarl.simplify.IF: Provides a partition of the set of conjunctive clauses of a BooleanExpression (the context) and a method to use that partition for context minimization.
CoreUniverse - Interface in dev.civl.sarl.IF: A CoreUniverse provides most of the functionality of a SymbolicUniverse, including the mechanisms to create and manipulate SymbolicExpressions and other SymbolicObjects.
CoreUniverse.ForallStructure - Class in dev.civl.sarl.IF: The result of analyzing certain "forall" expressions.
CVC4 - Enum constant in enum class dev.civl.sarl.IF.config.ProverInfo.ProverKind: CVC4 using CVC4's presentation language through its command line interface.
CVC5 - Enum constant in enum class dev.civl.sarl.IF.config.ProverInfo.ProverKind: CVC4, using SMT-LIB2 through CVC5's command line interface.

D

decrement(IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: arg - 1
decrement(Number) - Method in interface dev.civl.sarl.IF.number.NumberFactory: subtracts 1 of proper type
decrement(RationalNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: arg-1.0
defaultProofDir - Static variable in class dev.civl.sarl.IF.SARLConstants: Default directory name for theorem provers to use.
definition - Variable in class dev.civl.sarl.prove.IF.ProverFunctionInterpretation
denominator() - Method in interface dev.civl.sarl.IF.number.RationalNumber: Returns the denominator from a representation of this rational number as the quotient of two Java BigIntegers.
denominator(IdealFactory) - Method in interface dev.civl.sarl.ideal.IF.RationalExpression: Returns the denominator of this rational expression.
denominator(RationalNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns the denominator in a representation of the rational number as the quotient of two integers.
DENSE_ARRAY_WRITE - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for expression that represents the result of multiple writes to distinct concrete positions in an array.
DENSE_TUPLE_WRITE - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator representing the result of multiple writes to different components of a tuple.
denseArrayWrite(SymbolicExpression, Iterable<? extends SymbolicExpression>) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns an array obtained by performing a sequence of writes, given in a "dense" format, to an array.
dereference(SymbolicExpression, ReferenceExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given a reference and a value, returns the sub-expression of value specified by the reference.
DERIV - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: The (partial) derivative operator.
derivative(SymbolicExpression, IntObject, IntObject) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the function which is the degree-th derivative of function with respect to the index-th parameter.
dev.civl.sarl - module dev.civl.sarl
dev.civl.sarl - package dev.civl.sarl: This is the root package for SARL, and contains the single class SARL.
dev.civl.sarl.expr.IF - package dev.civl.sarl.expr.IF: This package provides the internal interface for the representation of basic symbolic expressions.
dev.civl.sarl.herbrand.IF - package dev.civl.sarl.herbrand.IF: This package provides the internal interface supporting Herbrand arithmetic, i.e., arithmetic in which all operations are treated as uninterpreted operations.
dev.civl.sarl.ideal.IF - package dev.civl.sarl.ideal.IF: The ideal module supports reasoning about numerical expressions using "ideal" mathematical reals and integers.
dev.civl.sarl.IF - package dev.civl.sarl.IF: This package and its subpackages provide the "public interface" to SARL.
dev.civl.sarl.IF.config - package dev.civl.sarl.IF.config: The config module provides a SARLConfig type, which encapsulates configuration information such as the list of available theorem provers with information on each.
dev.civl.sarl.IF.expr - package dev.civl.sarl.IF.expr: The public interface package dealing with symbolic expressions.
dev.civl.sarl.IF.expr.valueSetReference - package dev.civl.sarl.IF.expr.valueSetReference
dev.civl.sarl.IF.number - package dev.civl.sarl.IF.number: The number package supports infinite-precision integer and rational numbers.
dev.civl.sarl.IF.object - package dev.civl.sarl.IF.object: The object package provides the SymbolicObject interface, which is the root of the symbolic object type hierarchy.
dev.civl.sarl.IF.type - package dev.civl.sarl.IF.type: The type package provides interfaces for all of the symbolic types.
dev.civl.sarl.number.IF - package dev.civl.sarl.number.IF: A utility package supporting infinite precision integer and rational numbers, and a variety of arithmetic operations on them.
dev.civl.sarl.object.IF - package dev.civl.sarl.object.IF: Internal interface for the symbolic object module, providing mechanisms for creating SymbolicObjects.
dev.civl.sarl.preuniverse.IF - package dev.civl.sarl.preuniverse.IF: This package provides all of the functionality of a symbolic universe except reasoning.
dev.civl.sarl.prove.IF - package dev.civl.sarl.prove.IF: Module "prove" constitutes the interface between SARL and (possibly external) theorem provers.
dev.civl.sarl.reason.IF - package dev.civl.sarl.reason.IF: The internal interface for the "reason" module, which deals with Reasoners --- objects used to prove theorems and simplify symbolic expressions.
dev.civl.sarl.simplify.IF - package dev.civl.sarl.simplify.IF: Interfaces for the simplification of symbolic expressions.
dev.civl.sarl.type.IF - package dev.civl.sarl.type.IF: Internal interface for the "type" module, providing a SymbolicTypeFactory for producing SymbolicType s.
dev.civl.sarl.universe.IF - package dev.civl.sarl.universe.IF: Internal interface for the "universe" module.
diff(SymbolicRange, SymbolicRange) - Method in interface dev.civl.sarl.expr.IF.SymbolicRangeFactory
differentiable(SymbolicExpression, IntObject, Iterable<? extends NumericExpression>, Iterable<? extends NumericExpression>) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns an expression of boolean type which encodes the claim that a function is differentiable on a closed interval in R^n.
DIFFERENTIABLE - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: A predicate which declares a real-valued function to have some number of continuous derivatives over a bounded, rectangular, closed interval in R^n.
dimensions() - Method in interface dev.civl.sarl.IF.type.SymbolicArrayType
disjoint(SymbolicRange, SymbolicRange) - Method in interface dev.civl.sarl.expr.IF.SymbolicRangeFactory: NOTE: Currently only support ranges with a step value of 1.
divide(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a symbolic expression which is the result of dividing arg0 by arg1.
divide(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory
divide(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a symbolic expression which is the result of dividing arg0 by arg1.
divide(IntegerNumber, IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Divides two integer numbers and returns the result.
divide(Interval, Interval) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Divides two given Intervals and returns result.
divide(Interval, Number) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Return the Interval consisting of all Numbers that each Number x in the Interval multiplies with the given num is in the given interval.
divide(Number, Number) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Divides two numbers and returns result.
divide(RationalNumber, RationalNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Divides two rational numbers and returns the result.
divide(Range, Number) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Return a Range containing all x/constant, where x is in range and constant is a non- null and non-zero finite Number.
divide(Range, Range) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Return a Range containing all x/y, where x is in range0 and y is is in range1.
DIVIDE - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for real number division.
divideIntegerMonomials(Monomial, Monomial) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Divides two Monomials of integer type.
divides(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Does the integer a divide the integer b evenly? I.e, does there exist an integer n such that b=a*n?

E

elementType() - Method in interface dev.civl.sarl.IF.type.SymbolicArrayType: The type of each element of the array, a non-null symbolic type.
elementType() - Method in interface dev.civl.sarl.IF.type.SymbolicSetType: The type of the elements of the set.
EMPTY - Enum constant in enum class dev.civl.sarl.simplify.IF.Range.RangeSign: The range is empty
emptyArray(SymbolicType) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns array of length 0.
emptyIntegerInterval() - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns the empty integer interval: (0,0).
emptyMap(SymbolicMapType) - Method in interface dev.civl.sarl.IF.CoreUniverse
emptyPPList - Static variable in interface dev.civl.sarl.ideal.IF.IdealFactory: An empty array (i.e., one of length 0) of PrimitivePower.
emptyRealInterval() - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns the empty real interval: (0.0, 0.0).
emptySequence() - Method in interface dev.civl.sarl.object.IF.ObjectFactory: Returns the empty sequence.
emptySet(boolean) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Returns an empty Range of the specified type (integer/real) with no interval contained.
emptyTermList - Static variable in interface dev.civl.sarl.ideal.IF.IdealFactory: An empty array (i.e., one of length 0) of Monomial.
entrySet(SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the entry set of the map.
entryType(SymbolicMapType) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a tuple type which has two components: component 0 is the key type of the map type; component 1 is the value type of the map type.
entryType(SymbolicMapType) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory
EQ0 - Enum constant in enum class dev.civl.sarl.simplify.IF.Range.RangeSign: The range consists exactly of 0 and nothing else.
equals(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a BooleanExpression with the result of the equals operation on 2 NumericExpressions
equals(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns expression equivalent to arg0 = arg1 ("equals").
equals(SymbolicRange, SymbolicRange) - Method in interface dev.civl.sarl.expr.IF.SymbolicRangeFactory: NOTE: Currently only support ranges with a step value of 1.
equals(Object) - Method in interface dev.civl.sarl.IF.object.SymbolicObject: The equals method, included here to emphasize that the method provided by Object must be overridden!
equals(Object) - Method in class dev.civl.sarl.prove.IF.ProverFunctionInterpretation
EQUALS - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for comparison of two values for equality.
equiv(BooleanExpression, BooleanExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a symbolic expression representing "p is equivalent to q", i.e., pinvalid input: '<'=>q.
exists(SymbolicConstant, BooleanExpression) - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory: Returns the existentially quantified expression exists(x).e.
exists(SymbolicConstant, BooleanExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the existentially quantified expression exists(x).e.
EXISTS - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for for existential quantification: ∃ x .
existsInt(NumericSymbolicConstant, NumericExpression, NumericExpression, BooleanExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: A special case of "exists" that is very common: exists integer i such that lowinvalid input: '<'=iinvalid input: '<'high and p(i).
expand(IdealFactory) - Method in interface dev.civl.sarl.ideal.IF.Monomial: Returns the expansion of this monomial.
expand(NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory
expand(NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Attempts to expand an expression as a sum of simpler expressions.
expand(Range, Range) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Returns a Range R such that the intersection of R and C= contextRange is I=range and R is "as simple as possible".
expr - Variable in exception class dev.civl.sarl.IF.SARLBoundException: The symbolic expression into which the index points (typically, an array)
expression(SymbolicExpression.SymbolicOperator, SymbolicType, SymbolicObject...) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Returns an expression with the given operator, type, and argument sequence.
expression(SymbolicExpression.SymbolicOperator, SymbolicType, SymbolicObject...) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns an expression, given the operator, type, and array of arguments
expression(SymbolicExpression.SymbolicOperator, SymbolicType, SymbolicObject...) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory
EXPRESSION - Enum constant in enum class dev.civl.sarl.IF.object.SymbolicObject.SymbolicObjectKind
expressionFactory() - Method in interface dev.civl.sarl.preuniverse.IF.FactorySystem
ExpressionFactory - Interface in dev.civl.sarl.expr.IF: An ExpressionFactory is used to instantiate instances of SymbolicExpression.
Expressions - Class in dev.civl.sarl.expr.IF: This class provides static methods for producing factories that create various kinds of SymbolicExpression.
Expressions() - Constructor for class dev.civl.sarl.expr.IF.Expressions
extent() - Method in interface dev.civl.sarl.IF.type.SymbolicCompleteArrayType: Returns the extent (length) of any array of this type.
extractBoolean(BooleanExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: If the given expression has a concrete Boolean value, this returns it, else it returns null.
extractCharacter(SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: If the given expression is a concrete character expression, this returns the character value, else it returns null.
extractNumber(BooleanExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.SymbolicUniverse: Attempts to extract a concrete numeric value from the given expression, using the assumption if necessary to simplify the expression.
extractNumber(NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Attempts to interpret the given symbolic expression as a concrete number.
extractNumber(NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the Number value if the given symbolic expression has a concrete numerical value, else returns null.
extractNumber(NumericExpression) - Method in interface dev.civl.sarl.IF.Reasoner: If the given expression can be reduced to a concrete numeric value using the context, returns that concrete value, else returns null.

F

factorOrs(BooleanExpression[]) - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory

Given an array of or-expressions (expressions with operation SymbolicExpression.SymbolicOperator.OR), this method computes the "greatest common divisor" of those expressions and replaces each element of the array with the expressions that results from "dividing by" that gcd.

factorTermMap(Monomial[]) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

Computes a Monomial which is equivalent to the sum of the terms in the given term map.

FactorySystem - Interface in dev.civl.sarl.preuniverse.IF

falseExpr() - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory

Returns a false BooleanExpression

falseExpression() - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the boolean literal false.

falseObj() - Method in interface dev.civl.sarl.object.IF.ObjectFactory

FLOAT - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicRealType.RealKind

floor(NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory

floor(NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

Given an expression x of real type, returns an expression of integer type representing the greatest integer less than or equal to x.

floor(RationalNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns the greatest integer less than or equal to the given rational number.

forall(SymbolicConstant, BooleanExpression) - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory

Returns the universally quantified expression forall(x).e.

forall(SymbolicConstant, BooleanExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the universally quantified expression forall(x).e.

FORALL - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator

Operator for for universal quantification: ∀ x .

forallInt(NumericSymbolicConstant, NumericExpression, NumericExpression, BooleanExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

A special case of "forall" that is very common: forall integers i such that lowinvalid input: '<'=iinvalid input: '<'high, p(i).

ForallStructure() - Constructor for class dev.civl.sarl.IF.CoreUniverse.ForallStructure

fraction(IntegerNumber, IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns the rational number which is the quotient of the two integers.

fullySubstitute(Map<SymbolicExpression, SymbolicExpression>, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

Substitute the given SymbolicExpression expression by repeatedly applying the method

invalid reference

#apply(SymbolicExpression)

until no more substitution can happen.

function - Variable in class dev.civl.sarl.prove.IF.ProverFunctionInterpretation

FUNCTION - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicType.SymbolicTypeKind

functionType(SymbolicTypeSequence, SymbolicType) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory

Creates a SymbolicFunctionType, which represents an abstract mathematical function

functionType(SymbolicTypeSequence, SymbolicType, SymbolicFunctionType.SpecialRelationKind) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory

Creates a SymbolicFunctionType, which represents an abstract mathematical function

functionType(Iterable<? extends SymbolicType>, SymbolicType) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the specified function type.

functionType(Iterable<? extends SymbolicType>, SymbolicType, SymbolicFunctionType.SpecialRelationKind) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the specified function type.

G

gaussianElimination(RationalNumber[][]) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Performs Gauss-Jordan Elimination on a matrix of rational numbers, transforming the matrix to reduced row echelon form.

gcd(IntegerNumber, IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns the greatest common divisor of two integers.

GE0 - Enum constant in enum class dev.civl.sarl.simplify.IF.Range.RangeSign

The range contains 0 and a positive number and every element of the range is greater than or equal to 0.

get(int) - Method in interface dev.civl.sarl.IF.object.SymbolicSequence

Gets the index-th element of this sequence

get(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

getAliases() - Method in interface dev.civl.sarl.IF.config.ProverInfo

Returns the set of aliases associated to this theorem prover.

getArguments() - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression

Returns the sequence of arguments as an Iterable object.

getArgumentsAsArray(BooleanExpression) - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory

Given a BooleanExpression with operator SymbolicExpression.SymbolicOperator.AND, SymbolicExpression.SymbolicOperator.OR, or SymbolicExpression.SymbolicOperator.NOT, this method returns the arguments of that operator as an array.

getBoolean() - Method in interface dev.civl.sarl.IF.object.BooleanObject

Returns the underlying boolean value (true or false) wrapped by this BooleanObject.

getBooleanComparator() - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory

Returns a Comparator on BooleanExpressions produced by this factory.

getChar() - Method in interface dev.civl.sarl.IF.object.CharObject

getClauses() - Method in interface dev.civl.sarl.IF.expr.BooleanExpression

Returns a sequence of boolean expressions whose conjunction is equivalent to this.

getConcreteExponent(RationalExpression) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

Given the exponent in a potential power expression, this method computes a concrete integer that can be factored out of that exponent so that the exponent is in canonical form.

getDefaultConfiguration() - Static method in class dev.civl.sarl.IF.config.Configurations

Looks for a SARL configuration file, and, if one is not found, creates one in the user's home directory.

getErrFile() - Method in interface dev.civl.sarl.IF.CoreUniverse

Summary:Get the name (path) of the prover unexpected error file.

getFirst() - Method in interface dev.civl.sarl.IF.object.SymbolicSequence

Returns the "first" element of this collection or null if the collection is empty.

getFirstAlias() - Method in interface dev.civl.sarl.IF.config.ProverInfo

Returns one of the alias strings in the set of aliases.

getForallStructure(BooleanExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

Attempts to find a boolean expression equivalent to forallExpr but with the structure

getFreeSymbolicConstants(SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the set of unbound symbolic constants occurring in an expression.

getFreeVars() - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression

Get the set of free variables occurring in this symbolic expression.

getFullCollapsedContext() - Method in interface dev.civl.sarl.IF.Reasoner

Returns the full context associated to this Reasoner.

getFullContext(int) - Method in interface dev.civl.sarl.IF.Reasoner

getFullContextStack() - Method in interface dev.civl.sarl.IF.Reasoner

getIndex() - Method in interface dev.civl.sarl.IF.expr.ArrayElementReference

The index of the referenced element

getIndex() - Method in interface dev.civl.sarl.IF.expr.TupleComponentReference

Returns the index of the referenced field (i.e., component).

getIndex() - Method in interface dev.civl.sarl.IF.expr.UnionMemberReference

Gets the member index.

getIndex() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.VSArrayElementReference

The index of the referenced element

getIndex() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.VSTupleComponentReference

Returns the index of the referenced field (i.e., component).

getIndex() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.VSUnionMemberReference

Gets the member index.

getInt() - Method in interface dev.civl.sarl.IF.object.IntObject

Gets the int value.

getIntegerLengthBound() - Method in interface dev.civl.sarl.IF.CoreUniverse

Get the current upper bound of the integer length.

getKind() - Method in interface dev.civl.sarl.IF.config.ProverInfo

The kind of theorem prover this is.

getLower() - Method in interface dev.civl.sarl.IF.expr.SymbolicRange

getModel() - Method in interface dev.civl.sarl.IF.ModelResult

Returns the model, a map assigning a concrete symbolic expression value to each symbolic constant occurring in the query.

getNumber() - Method in interface dev.civl.sarl.IF.object.NumberObject

Get the underlying Number.

getNumNewNames() - Method in interface dev.civl.sarl.IF.CanonicalRenamer

Returns the number of new (post-canonicalized) symbolic constants at the current time.

getNumNull() - Method in interface dev.civl.sarl.IF.object.SymbolicSequence

Returns the number of "NULL" elements of this sequence, i.e., symbolic expressions for which method SymbolicExpression.isNull() returns true.

getNumProvers() - Method in interface dev.civl.sarl.IF.config.SARLConfig

The number of theorem provers supported by this configuration.

getOffset() - Method in interface dev.civl.sarl.IF.expr.OffsetReference

Returns the offset.

getOffset() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.VSOffsetReference

Returns the offset.

getOptions() - Method in interface dev.civl.sarl.IF.config.ProverInfo

Returns the sequence of command line options that should be used when invoking this theorem prover.

getOrder() - Method in interface dev.civl.sarl.IF.object.SymbolicObject

Experimental: get the number which imposes a total order on the set of all canonic symbolic object.

getOutputFileDir() - Method in interface dev.civl.sarl.IF.config.SARLConfig

getOutputStream() - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the output stream to which information (such as queries) will be printed.

getParent() - Method in interface dev.civl.sarl.IF.expr.NTReferenceExpression

As this is a reference to an array element, tuple component, union member, or an offset reference, returns the reference to the parent, i.e., the array, tuple, union, or the other reference, resp.

getParent() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.NTValueSetReference

As this is an VSArrayElementReference, VSArraySectionReference, VSOffsetReference, VSTupleComponentReference or VSUnionMemberReference, returns the reference to the parent, i.e.

getPath() - Method in interface dev.civl.sarl.IF.config.ProverInfo

The path to the executable theorem prover.

getProbabilisticBound() - Method in interface dev.civl.sarl.IF.CoreUniverse

The upper bound on the probability of error when deciding whether a polynomial is 0.

getProver(int) - Method in interface dev.civl.sarl.IF.config.SARLConfig

Gets the index-th theorem prover.

getProvers() - Method in interface dev.civl.sarl.IF.config.SARLConfig

Returns all the provers supported by this configuration as an iterable sequence.

getProverWithAlias(String) - Method in interface dev.civl.sarl.IF.config.SARLConfig

Finds a prover supported by this configuration with the given alias.

getProverWithKind(ProverInfo.ProverKind) - Method in interface dev.civl.sarl.IF.config.SARLConfig

Finds a prover of the given kind supported by this configuration.

getRangeKind() - Method in interface dev.civl.sarl.IF.expr.SymbolicRange

getReasoner(BooleanExpression, boolean, ProverFunctionInterpretation[]) - Method in interface dev.civl.sarl.reason.IF.ReasonerFactory

Gets a Reasoner for the given context.

getReasoner(List<BooleanExpression>, boolean, ProverFunctionInterpretation[]) - Method in interface dev.civl.sarl.reason.IF.ReasonerFactory

getReducedCollapsedContext() - Method in interface dev.civl.sarl.IF.Reasoner

Returns the reduced context associated to this Reasoner.

getReducedContext(int) - Method in interface dev.civl.sarl.IF.Reasoner

getReducedContextStack() - Method in interface dev.civl.sarl.IF.Reasoner

getResultType() - Method in interface dev.civl.sarl.IF.ValidityResult

Returns the result type of this result.

getShowErrors() - Method in interface dev.civl.sarl.IF.config.ProverInfo

Should the prover print a message every time the underlying theorem prover reports an error? (In any case, the error is interpreted as an inconclusive result.)

getShowInconclusives() - Method in interface dev.civl.sarl.IF.config.ProverInfo

Should the prover print a message every time it reports an inconclusive result?

getShowProverQueries() - Method in interface dev.civl.sarl.IF.CoreUniverse

Gets the showProverQueries flag: if true, the theorem prover queries processed by the underlying theorem prover(s) will be printed to the output stream.

getShowQueries() - Method in interface dev.civl.sarl.IF.config.ProverInfo

Should the prover print all the queries?

getShowQueries() - Method in interface dev.civl.sarl.IF.CoreUniverse

Gets the showQueries flag: if true, SARL theorem prover queries will be printed to the output stream.

getSingletonValue() - Method in interface dev.civl.sarl.simplify.IF.Range

If this range represents a singleton set (a set consisting of exactly one Number), this method returns the value of its sole element; otherwise, returns null.

getStep() - Method in interface dev.civl.sarl.IF.expr.SymbolicRange

getString() - Method in interface dev.civl.sarl.IF.object.StringObject

Gets the string.

getSummands(NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

Decomposes an expression as a sum of terms, returning those terms as an array.

getTimeout() - Method in interface dev.civl.sarl.IF.config.ProverInfo

Returns time limit in seconds or -1 if the time is unlimited.

getTruePrimitives() - Method in interface dev.civl.sarl.ideal.IF.Monomial

Returns the Primitives which are not Polynomials occurring in this Monomial.

getType(int) - Method in interface dev.civl.sarl.IF.type.SymbolicTypeSequence

Returns the index-th type in this sequence.

getUnsatisfiability() - Method in interface dev.civl.sarl.IF.expr.BooleanExpression

Is this boolean expression unsatisfiable, i.e., equivalent to false,? The result is cached here for convenience, using method

invalid reference

#setUnsatisfiable(ResultType)

getUpper() - Method in interface dev.civl.sarl.IF.expr.SymbolicRange

getUseBackwardSubstitution() - Method in interface dev.civl.sarl.IF.CoreUniverse

Shall the Reasoners generated by this universe use backwards substitution when simplifying, in order to solve for certain numeric expressions in terms of others?

getValidity() - Method in interface dev.civl.sarl.IF.expr.BooleanExpression

Is this boolean expression valid, i.e., equivalent to true, i.e., a tautology? The result is cached here for convenience, using method BooleanExpression.setValidity(ResultType).

getVersion() - Method in interface dev.civl.sarl.IF.config.ProverInfo

The version, e.g.

GT0 - Enum constant in enum class dev.civl.sarl.simplify.IF.Range.RangeSign

Every element of the range is greater than 0 and the range is non-empty.

H

hashCode() - Method in interface dev.civl.sarl.IF.object.SymbolicObject: The hash code method, included here to emphasize that the method provided by Object must be overridden!
hashCode() - Method in class dev.civl.sarl.prove.IF.ProverFunctionInterpretation
hasNontrivialExpansion(IdealFactory) - Method in interface dev.civl.sarl.ideal.IF.Monomial: Determines whether or not this monomial could possibly have a non-trivial expansion.
hasTermWithNontrivialExpansion(IdealFactory) - Method in interface dev.civl.sarl.ideal.IF.Polynomial: Does this polynomial contain a term with a nontrivial factorization? This is stronger than asking if the polynomial has a nontrivial factorization.
Herbrand - Class in dev.civl.sarl.herbrand.IF
Herbrand() - Constructor for class dev.civl.sarl.herbrand.IF.Herbrand
HERBRAND - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicIntegerType.IntegerKind
HERBRAND - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicRealType.RealKind
herbrandIntegerType() - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the Herbrand integer type.
herbrandIntegerType() - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory
herbrandRealType() - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the Herbrand real type.
herbrandRealType() - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory

I

id() - Method in interface dev.civl.sarl.IF.object.SymbolicObject

Every canonic symbolic object has a unique ID number, returned by this method.

Ideal - Class in dev.civl.sarl.ideal.IF

Entry point for the ideal module, providing static methods to create an IdealFactory and a

invalid reference

SimplifierFactory

Ideal() - Constructor for class dev.civl.sarl.ideal.IF.Ideal

IDEAL - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicIntegerType.IntegerKind

IDEAL - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicRealType.RealKind

IdealFactory - Interface in dev.civl.sarl.ideal.IF

An IdealFactory provides a few services beyond those guaranteed by an arbitrary NumericExpressionFactory.

identifier - Variable in class dev.civl.sarl.prove.IF.ProverFunctionInterpretation

IDENTITY - Enum constant in enum class dev.civl.sarl.IF.expr.ReferenceExpression.ReferenceKind

The identity reference.

IDENTITY - Enum constant in enum class dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference.VSReferenceKind

The identity reference.

identityReference() - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory

Returns the identity (or "trivial") reference I.

identityReference() - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the identity (or "trivial") reference I.

implies(BooleanExpression, BooleanExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns a symbolic expression representing "p implies q", i.e., p=>q.

increment(IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory

add(arg, 1)

increment(Number) - Method in interface dev.civl.sarl.IF.number.NumberFactory

adds 1 of proper type

increment(RationalNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory

add(arg, 1.0)

incrementProverValidCount() - Method in interface dev.civl.sarl.preuniverse.IF.PreUniverse

incrementValidCount() - Method in interface dev.civl.sarl.preuniverse.IF.PreUniverse

index - Variable in exception class dev.civl.sarl.IF.SARLBoundException

The offending index

infiniteInteger(boolean) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns an infinite IntegerNumber, its signum is determined by the given boolean value.

infiniteNumber(boolean, boolean) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns an infinite Number, its type is determined by the first boolean argument isIntegeral and its signum is determined by the second boolean argument isPositiveInfinity.

infiniteRational(boolean) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns an infinite RationalNumber, its signum is determined by the given boolean value.

init() - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory

Initializes fields; should be called after comparators have been set and linked.

init() - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory

Initialize this expression factory.

init() - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory

Initialize this numeric expression factory.

init() - Method in interface dev.civl.sarl.object.IF.ObjectFactory

Initializes the fields of this factory.

init() - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory

Initializes the factory; should be called only after the comparators have all been linked.

inputTypes() - Method in interface dev.civl.sarl.IF.type.SymbolicFunctionType

The ordered sequence of input types.

inRange(NumericExpression, SymbolicRange) - Method in interface dev.civl.sarl.expr.IF.SymbolicRangeFactory

insert(int, T) - Method in interface dev.civl.sarl.IF.object.SymbolicSequence

Inserts element at position index, shifting all subsequence elements up one.

insertElementAt(SymbolicExpression, int, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

Inserts value an position index in array, shifting subsequence elements "up".

INT - Enum constant in enum class dev.civl.sarl.IF.object.SymbolicObject.SymbolicObjectKind

INT_DIVIDE - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator

Operator for integer division.

intConstant(int) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

Returns an integer Constant wrapping a Java int value.

integer(int) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the integer symbolic expression with the given int value.

integer(int) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns an integer number corresponding to the given Java int.

integer(long) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the numeric symbolic expression with the given long value.

integer(long) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns the IntegerNumber with value specified by the long.

integer(String) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns the integer number specified by the given string.

integer(BigInteger) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the numeric symbolic expression with the given BigInteger value.

integer(BigInteger) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns the IntegerNumber with value specified by the BigInteger.

INTEGER - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicType.SymbolicTypeKind

integer2Bitvector(NumericExpression, SymbolicCompleteArrayType) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the conversion of a bit vector from an integer.

integerKind() - Method in interface dev.civl.sarl.IF.type.SymbolicIntegerType

a method to return the kind of the integer type.

IntegerNumber - Interface in dev.civl.sarl.IF.number

An instance of this class represents an integer number.

integerToRational(IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Casts an integer to a rational number.

integerType() - Method in interface dev.civl.sarl.IF.CoreUniverse

The "ideal" integer type, representing the set of mathematical integers.

integerType() - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory

integerValue(RationalNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns the value of the rational number as an integer number.

intersect(Range, Range) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory

Return the intersection Range of range0 and range1.

intersection(Interval, Interval) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns the interval which is the intersection of the two given intervals.

intersects(Range) - Method in interface dev.civl.sarl.simplify.IF.Range

Is the intersection of this set with the given one nonempty?

interval(boolean, Number, boolean, Number, boolean) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory

Returns a Range consisting of exactly one interval representing all x between the Number lower (exclusively iff strictLower is true, else inclusively) and the Number upper (exclusively iff strictUpper is true, else inclusively).
Preconditions:
> All arguments should satisfy the preconditions of Interval.
Postconditions:
> The generated interval instance should satisfy the postconditions of Interval.

Interval - Interface in dev.civl.sarl.IF.number

An instance of Interval represents a numeric interval.

INTERVAL - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicRange.RangeKind

A contiguous range of values.

intervalApproximation(NumericExpression) - Method in interface dev.civl.sarl.IF.Reasoner

Returns an interval over-approximation of the given expression.

intervalOverApproximation() - Method in interface dev.civl.sarl.simplify.IF.Range

Get the over-approximated Interval of this range.

IntervalUnion() - Constructor for class dev.civl.sarl.IF.number.NumberFactory.IntervalUnion

intObject(int) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the IntObject wrapping the given Java int value.

intObject(int) - Method in interface dev.civl.sarl.object.IF.ObjectFactory

IntObject - Interface in dev.civl.sarl.IF.object

A symbolic object wrapping a single Java "int" value.

intValue() - Method in interface dev.civl.sarl.IF.number.IntegerNumber

Attempts to extract a Java int value from this IntegerNumber.

isArrayElementReference() - Method in interface dev.civl.sarl.IF.expr.ReferenceExpression

Is this an array element reference?

isArrayElementReference() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference

Is this an array element reference?

isArraySectionReference() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference

Is this an array section reference?

isBoolean() - Method in interface dev.civl.sarl.IF.type.SymbolicType

Tells whether the type is the boolean type.

isCanonic() - Method in interface dev.civl.sarl.IF.object.SymbolicObject

Is this object the unique representative of its equivalence class (under "equals")?

isChar() - Method in interface dev.civl.sarl.IF.type.SymbolicType

Tells whether the type is a char type

isComplete() - Method in interface dev.civl.sarl.IF.type.SymbolicArrayType

Is this a complete array type, i.e., is the extent specified? If true, this can be safely cast to SymbolicCompleteArrayType.

isEmpty() - Method in interface dev.civl.sarl.IF.number.Interval

Is the interval empty? The empty interval should be (0, 0).

isEmpty() - Method in interface dev.civl.sarl.simplify.IF.Range

Is this an empty set?

isFalse() - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression

Is this the boolean "false" expression?

isFloor(SymbolicExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory

isFloor(SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

Is the given symbolic expression a "floor" expression, i.e., an application of the floor function, which returns the greatest integer less than or equal to its argument.

isHerbrand() - Method in interface dev.civl.sarl.IF.type.SymbolicType

Is this a Herbrand type? There are Herbrand variants of real and integer types.

isIdeal() - Method in interface dev.civl.sarl.IF.type.SymbolicType

Is this an Ideal numeric type? These are the mathematical integer and real types.

isIdentityReference() - Method in interface dev.civl.sarl.IF.expr.ReferenceExpression

Is this the identity reference?

isIdentityReference() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference

Is this the identity reference?

isInfinite() - Method in interface dev.civl.sarl.IF.number.Number

Is this number infinite?

isInteger() - Method in interface dev.civl.sarl.IF.object.NumberObject

Does the number have integer type? (Note: a rational number which is integer, e.g., "2/1", does not have integer type.)

isInteger() - Method in interface dev.civl.sarl.IF.type.SymbolicType

Tells whether the type is an integer type.

isIntegral() - Method in interface dev.civl.sarl.IF.number.Interval

Does this interval have integer type? If so, then both the upper and lower bounds will have integer type.

isIntegral() - Method in interface dev.civl.sarl.simplify.IF.Range

Is this an integer set?

isIntegral(RationalNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns true iff the rational number is an integer, e.g., "3.0", or "4/2".

isNegative() - Method in interface dev.civl.sarl.IF.object.IntObject

Is the int value negative?

isNonnegative(RationalExpression) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

Given a rational expression rational returns an expression equivalent to 0≤rational.

isNonZero(Monomial) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

Computes an expression equivalent to "monomial != 0".

isNull() - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression

Is this the "NULL" symbolic expression? A NULL expression has operator SymbolicExpression.SymbolicOperator.NULL, 0 arguments, and null type.

isNullReference() - Method in interface dev.civl.sarl.IF.expr.ReferenceExpression

Is this the null reference?

isNumeric() - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression

Is this a numeric expression, i.e., does this have integer or real type? If true, this may be safely cast to NumericExpression.

isNumeric() - Method in interface dev.civl.sarl.IF.type.SymbolicType

Tells whether the type is a real or integer type

isOffsetReference() - Method in interface dev.civl.sarl.IF.expr.ReferenceExpression

Is this an "offset reference"?

isOffsetReference() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference

Is this an offset reference?

isOne() - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression

Is this the integer or real 1 expression?

isOne() - Method in interface dev.civl.sarl.IF.number.Number

Is this number equal to 1?

isOne() - Method in interface dev.civl.sarl.IF.object.IntObject

Is the int value 1?

isOne() - Method in interface dev.civl.sarl.IF.object.NumberObject

Convenience method to determine whether this concrete expression is 1.

isPermutCall(SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

isPositive() - Method in interface dev.civl.sarl.IF.object.IntObject

Is the int value positive?

isPositive(RationalExpression) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

Given a rational expression rational returns an expression equivalent to 0<rational.

isReal() - Method in interface dev.civl.sarl.IF.object.NumberObject

Does the number have real (not integer) type?

isReal() - Method in interface dev.civl.sarl.IF.type.SymbolicType

Tells whether the type is a real type.

isSigmaCall(SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

isSubsetOf(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

isTrivialMonic() - Method in interface dev.civl.sarl.ideal.IF.Monic

Is this the trivial monic, i.e., the monic consisting of 0 factors (and therefore equivalent to 1)?

isTrue() - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression

Is this the boolean "true" expression?

isTupleComponentReference() - Method in interface dev.civl.sarl.IF.expr.ReferenceExpression

Is this a tuple component reference?

isTupleComponentReference() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference

Is this a tuple component reference?

isUnionMemberReference() - Method in interface dev.civl.sarl.IF.expr.ReferenceExpression

Is this a union member reference?

isUnionMemberReference() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference

Is this a union member reference?

isUniversal() - Method in interface dev.civl.sarl.IF.number.Interval

Is the interval an universal set?

isUniversal() - Method in interface dev.civl.sarl.simplify.IF.Range

Is this a universal set?

isValid(BooleanExpression) - Method in interface dev.civl.sarl.IF.Reasoner

Equivalent to valid(predicate).getResultType()==ResultType.YES.

isValueSetTemplateType(SymbolicType) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory

isZero() - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression

Is this the integer or real 0 expression?

isZero() - Method in interface dev.civl.sarl.IF.number.Interval

Does the interval represent exactly the single number of 0?

isZero() - Method in interface dev.civl.sarl.IF.number.Number

Is this number equal to 0? Same as signum() == 0, but sometimes more convenient.

isZero() - Method in interface dev.civl.sarl.IF.object.IntObject

Is the int value zero?

isZero() - Method in interface dev.civl.sarl.IF.object.NumberObject

Convenience method to determine whether this concrete expression is 0.

isZero(Monomial) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

Computes boolean expression equivalent to m=0.

J

join(Interval, Interval) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns the smallest interval containing both of the given intervals.

K

Key Features - Search tag in Overview: Section
keySet(SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse
keyType() - Method in interface dev.civl.sarl.IF.type.SymbolicMapType: Returns the type of the domain (keys).

L

lambda(SymbolicConstant, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the lambda expression lambda(x).e, i.e., the expression representing the function which given x returns e, where e might possibly involve the variable x.
LAMBDA - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for a lambda expression, as in the lambda calculus: λ x .
lcm(IntegerNumber, IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns the least common multiple of the two positive integers.
LE0 - Enum constant in enum class dev.civl.sarl.simplify.IF.Range.RangeSign: Every element of the range is less than or equal to 0 and the range contains 0 and a negative number.
length(SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the length of any symbolic expression of array type.
LENGTH - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for getting the length of an array.
LESS_THAN - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for a less-than expression: x < y.
LESS_THAN_EQUALS - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for a less-than-or-equals expression: x ≤ y .
lessThan(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a BooleanExpression with the result of the lessThan operation on 2 NumericExpressions
lessThan(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns expression equivalent to arg0 invalid input: '<' arg1.
lessThanEquals(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a BooleanExpression with the result of the lessThanEquals operation on 2 NumericExpressions
lessThanEquals(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns expression equivalent to arg0 invalid input: '<'= arg1 ("less than or equal to").
LINEAR_ORDER - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicFunctionType.SpecialRelationKind: The function type represents a linear order binary relation
location - Variable in exception class dev.civl.sarl.IF.SARLBoundException: The kind of operation that resulted in the exception, e.g., "an array write operation" or "an array read operation"
lower() - Method in interface dev.civl.sarl.IF.number.Interval: The lower bound of this interval.
lower(IdealFactory) - Method in interface dev.civl.sarl.ideal.IF.Monomial: Computes a term map from performing a single outer-level expansion.
lowerBound - Variable in class dev.civl.sarl.IF.CoreUniverse.ForallStructure: The lower bound (inclusive) of the bound variable.
lowerBound - Variable in exception class dev.civl.sarl.IF.SARLBoundException: The lowest value that an index should take; can be null, representing "unknown"
lowerBound() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.VSArraySectionReference
LT0 - Enum constant in enum class dev.civl.sarl.simplify.IF.Range.RangeSign: Every element of the range is less than 0 and the range is not empty.

M

make(SymbolicExpression.SymbolicOperator, SymbolicType, SymbolicObject[]) - Method in interface dev.civl.sarl.IF.CoreUniverse: Applies the given operator to the arguments and returns the resulting expression in the form used by this universe.
makeConfigFile() - Static method in class dev.civl.sarl.IF.config.Configurations: Makes a new SARL configuration file in the user's home directory.
makeProverDir() - Static method in class dev.civl.sarl.universe.IF.Universes: Creates a new directory to be used by theorem provers.
MAP - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicType.SymbolicTypeKind
mapSize(SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse
mapSubstituter(UnaryOperator<SymbolicExpression>) - Method in interface dev.civl.sarl.IF.CoreUniverse
mapSubstituter(Map<SymbolicExpression, SymbolicExpression>) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a substituter for which the base substitutions are specified by an explicit Java Map.
mapType(SymbolicType, SymbolicType) - Method in interface dev.civl.sarl.IF.CoreUniverse: Under construction.
mapType(SymbolicType, SymbolicType) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory
max(List<NumericExpression>) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a NumericExpression which is equivalent to the maximum of all NumericExpressions in exprs.
maxDegreeOf(NumberFactory, Primitive) - Method in interface dev.civl.sarl.ideal.IF.Monomial: Computes the maximum degree to which primitive occurs in this Monomial.
maxWith(IntObject) - Method in interface dev.civl.sarl.IF.object.IntObject: Returns the maximum of this and that as an IntObject.
MAYBE - Enum constant in enum class dev.civl.sarl.IF.ValidityResult.ResultType: Nothing can be concluded about the validity of the query
min(List<NumericExpression>) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a NumericExpression which is equivalent to the minimum of all NumericExpressions in exprs.
minimizeFor(SymbolicExpression, PreUniverse) - Method in interface dev.civl.sarl.simplify.IF.ContextPartition: Returns a formula equivalent to or weaker than the original context but which can be used as the context for check validity or simplifying expr.
minus(NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a symbolic expression which is the negative of the given numerical expression.
minus(NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a symbolic expression which is the negative of the given numerical expression.
minus(IntObject) - Method in interface dev.civl.sarl.IF.object.IntObject: Returns the result of subtracting that from this, as an IntObject.
minWith(IntObject) - Method in interface dev.civl.sarl.IF.object.IntObject: Returns the minimum of this and that as an IntObject.
mod(IntegerNumber, IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Modulo operations.
modelResult(Map<SymbolicConstant, SymbolicExpression>) - Static method in class dev.civl.sarl.prove.IF.Prove: Constructs a new ModelResult wrapping the given mapping from symbolic constants to symbolic expressions.
ModelResult - Interface in dev.civl.sarl.IF: A result to a validity query which also requested a model in case the answer was "NO", and for which the answer was "NO".
modulo(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a symbolic expression which represents arg0 modulo arg1.
modulo(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Returns a symbolic expression which represents arg0 modulo arg1.
modulo(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a symbolic expression which represents arg0 modulo arg1.
MODULO - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: The integer modulus operator.
monic(IdealFactory) - Method in interface dev.civl.sarl.ideal.IF.Monomial: Returns the monic factor of this monomial.
monic(SymbolicType, PrimitivePower[]) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Returns a (possibly trivial) monic as specified.
Monic - Interface in dev.civl.sarl.ideal.IF: A Monic is a product of powers of primitive expressions x₁^{i
₁}*...*x_n^i_n, where the x _i are primitives and the i_j are positive concrete ints.
monicComparator() - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: The Comparator on Monics.
monicFactors(IdealFactory) - Method in interface dev.civl.sarl.ideal.IF.Monic: Returns the factors of this monic as a map from Primitive to PrimitivePower.
monicFactory() - Method in interface dev.civl.sarl.ideal.IF.IdealFactory
monicMask(Monic, boolean[]) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Given a Monic returns the Monic obtained by removing some of the PrimitivePower factors according to the given mask.
monomial(Constant, Monic) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Returns a Monomial which is the product of the given constant and the given monic.
Monomial - Interface in dev.civl.sarl.ideal.IF: A Monomial is the product of a constant and a Monic.
monomialConstant(IdealFactory) - Method in interface dev.civl.sarl.ideal.IF.Monomial: Returns the constant factor of this monomial.
monomialDegree(NumberFactory) - Method in interface dev.civl.sarl.ideal.IF.Monomial: Returns the degree of the monic where each factor is considered to have degree 1.
monomialOrder(IdealFactory) - Method in interface dev.civl.sarl.ideal.IF.Monomial: Computes the "monomial order" of this Monomial.
multiply(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a symbolic expression which is the result of multiplying the two given symbolic exprssions.
multiply(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory
multiply(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a symbolic expression which is the result of multiplying the two given symbolic expressions.
multiply(IntegerNumber, IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Multiplies two integer numbers and returns the result.
multiply(Interval, Interval) - Method in interface dev.civl.sarl.IF.number.NumberFactory: To calculate the product of two non-null and not empty Interval with same type (real/integer)
This is the smallest interval containing all x1*x2, where x1 is in i1 and x2 is in i2.
multiply(Number, Interval) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Multiply the given Interval with a given Number and returns result.
multiply(Number, Number) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Multiplies two numbers and returns result.
multiply(RationalNumber, RationalNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Multiplies two rational numbers and returns the result.
multiply(Range, Number) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Return a Range containing all x*constant, where x is in range and constant is a non- null finite Number.
multiply(Range, Range) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Return a Range containing all x*y, where x is in range0 and y is in range1.
multiply(Iterable<? extends NumericExpression>) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns symbolic expression representing the product of the given sequence of expressions.
MULTIPLY - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the numerical product of symbolic expressions.
multiplyConstantMonomial(Constant, Monomial) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Returns the product of a Constant and a Monomial of the same type.
multiplyConstantTermMap(Constant, Monomial[]) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Computes the term map obtained by multiplying the given Constant with every term in a given term map.
multiplyMonomials(Monomial, Monomial) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Computes the product of any two Monomials of the same type.
multiplyTermMaps(Monomial[], Monomial[]) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Returns the products of the two term maps as a term map.

N

name() - Method in interface dev.civl.sarl.IF.expr.SymbolicConstant: Returns the name of this symbolic constant.
name() - Method in interface dev.civl.sarl.IF.type.SymbolicTupleType: Returns the name of this tuple type, a non-null StringObject.
name() - Method in interface dev.civl.sarl.IF.type.SymbolicUninterpretedType
name() - Method in interface dev.civl.sarl.IF.type.SymbolicUnionType: The name of this union type.
nameSubstituter(Map<StringObject, StringObject>) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a substituter specified by a mapping of old names to new names for symbolic constants.
negate(IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns the negation of the given integer number, i.e., -x.
negate(Interval) - Method in interface dev.civl.sarl.IF.number.NumberFactory: To negate the given non-null interval.
negate(Number) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Negates the number, preserving the type (IntegerNumberIF or RationalNumberIF).
negate(RationalNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns the negation of the given rational number, i.e., -x.
NEGATIVE - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for numerical negation, i.e., - x.
negativeInfinityInteger() - Method in interface dev.civl.sarl.IF.number.NumberFactory: Return a IntegerNumber representing the negative infinity.
negativeInfinityRational() - Method in interface dev.civl.sarl.IF.number.NumberFactory: Return a RationalNumber representing the negative infinity.
neq(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a BooleanExpression with the result of the notEquals operation on 2 NumericExpressions
neq(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns expression equivalent to arg0 != arg1 ("not equals").
neq(SymbolicRange, SymbolicRange) - Method in interface dev.civl.sarl.expr.IF.SymbolicRangeFactory: NOTE: Currently only support ranges with a step value of 1.
NEQ - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for comparison of two values for inequality.
newCnfFactory(SymbolicTypeFactory, ObjectFactory) - Static method in class dev.civl.sarl.expr.IF.Expressions: Produces a new factory for creating BooleanExpressions that uses Conjunctive Normal Form (CNF) as the canonical representation of boolean expressions.
newConfiguration(File) - Static method in class dev.civl.sarl.IF.config.Configurations: Parses the specified SARL configuration file.
newConfiguration(Collection<ProverInfo>) - Static method in class dev.civl.sarl.IF.config.Configurations: Creates a new SARLConfig object based on the given list of prover information objects.
newContextPartition(PreUniverse, List<BooleanExpression>) - Static method in class dev.civl.sarl.simplify.IF.Simplify
newExpressionFactory(NumericExpressionFactory) - Static method in class dev.civl.sarl.expr.IF.Expressions: Produces a new instance of the standard expression factory.
newFactorySystem(ObjectFactory, SymbolicTypeFactory, ExpressionFactory) - Static method in class dev.civl.sarl.preuniverse.IF.PreUniverses
newHerbrandExpressionFactory(NumberFactory, ObjectFactory, SymbolicTypeFactory) - Static method in class dev.civl.sarl.expr.IF.Expressions: Produces a new expression factory in which the underlying NumericExpressionFactory is based on "Herbrand arithmetic", i.e., arithmetic in which the numeric operations are treated as uninterpreted functions.
newHerbrandFactory(NumberFactory, ObjectFactory, SymbolicTypeFactory, BooleanExpressionFactory) - Static method in class dev.civl.sarl.herbrand.IF.Herbrand
newHerbrandFactorySystem() - Static method in class dev.civl.sarl.preuniverse.IF.PreUniverses
newHerbrandUniverse() - Static method in class dev.civl.sarl.universe.IF.Universes
newHerbrandUniverse(SARLConfig, ProverInfo) - Static method in class dev.civl.sarl.universe.IF.Universes
newHerbrandUniverse(SARLConfig, ProverInfo, Path) - Static method in class dev.civl.sarl.universe.IF.Universes
newHerbrandUniverse(Path) - Static method in class dev.civl.sarl.universe.IF.Universes
newIdealExpressionFactory(NumberFactory, ObjectFactory, SymbolicTypeFactory) - Static method in class dev.civl.sarl.expr.IF.Expressions: Produces a new expression factory in which the underlying NumericExpressionFactory uses "ideal" (mathematical) integer and real arithmetic, i.e., infinite precision, unbounded arithmetic.
newIdealFactory(NumberFactory, ObjectFactory, SymbolicTypeFactory, BooleanExpressionFactory) - Static method in class dev.civl.sarl.ideal.IF.Ideal: Creates a new ideal factory based on the given factories.
newIdealFactorySystem() - Static method in class dev.civl.sarl.preuniverse.IF.PreUniverses
newIdealUniverse() - Static method in class dev.civl.sarl.SARL
newIdealUniverse() - Static method in class dev.civl.sarl.universe.IF.Universes
newIdealUniverse(SARLConfig, ProverInfo) - Static method in class dev.civl.sarl.SARL
newIdealUniverse(SARLConfig, ProverInfo) - Static method in class dev.civl.sarl.universe.IF.Universes
newIdealUniverse(SARLConfig, ProverInfo, Path) - Static method in class dev.civl.sarl.SARL: Returns a symbolic universe that only deals with ideal (mathematical) integers and reals.
newIdealUniverse(SARLConfig, ProverInfo, Path) - Static method in class dev.civl.sarl.universe.IF.Universes
newIdealUniverse(Path) - Static method in class dev.civl.sarl.SARL: Returns a symbolic universe that only deals with ideal (mathematical) integers and reals.
newIdealUniverse(Path) - Static method in class dev.civl.sarl.universe.IF.Universes
newInterval(boolean, Number, boolean, Number, boolean) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns a new Interval as specified.
newIntervalUnionFactory() - Static method in class dev.civl.sarl.simplify.IF.Simplify
newMinimalBoundCleaner() - Method in interface dev.civl.sarl.preuniverse.IF.PreUniverse: Produces a new object for renaming bound variables in a minimal way.
newMultiProverFactory(PreUniverse, SARLConfig, Path) - Static method in class dev.civl.sarl.prove.IF.Prove: Constructs a new theorem prover factory based on the given configuration.
newObjectFactory(NumberFactory) - Static method in class dev.civl.sarl.object.IF.Objects
newPreUniverse(FactorySystem) - Static method in class dev.civl.sarl.preuniverse.IF.PreUniverses
newProver(BooleanExpression) - Method in interface dev.civl.sarl.prove.IF.TheoremProverFactory: Returns a new instance of TheoremProver with the given context.
newProver(BooleanExpression, ProverFunctionInterpretation[]) - Method in interface dev.civl.sarl.prove.IF.TheoremProverFactory: Returns a new instance of TheoremProver with the given context.
newProverFactory(PreUniverse, ProverInfo, Path) - Static method in class dev.civl.sarl.prove.IF.Prove: Constructs a new theorem prover factory based on a single underlying theorem prover.
newProverPredicate(SymbolicUniverse, String, SymbolicConstant[], SymbolicExpression) - Static method in class dev.civl.sarl.prove.IF.ProverFunctionInterpretation
newRange(Interval...) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Create a new Range based on given non-null Intervals.
If the given intervals represents an empty interval array, this function will return an empty Range with 0 interval.
newReasonerFactory(PreUniverse, IdealFactory, TheoremProverFactory) - Static method in class dev.civl.sarl.reason.IF.Reason: Create a reasoner factory
newStandardExpressionFactory(NumberFactory, ObjectFactory, SymbolicTypeFactory) - Static method in class dev.civl.sarl.expr.IF.Expressions: Produces a new expression factory that uses both Herbrand and Ideal arithmetic.
newStandardUniverse() - Static method in class dev.civl.sarl.SARL
newStandardUniverse() - Static method in class dev.civl.sarl.universe.IF.Universes
newStandardUniverse(SARLConfig, ProverInfo) - Static method in class dev.civl.sarl.SARL
newStandardUniverse(SARLConfig, ProverInfo) - Static method in class dev.civl.sarl.universe.IF.Universes
newStandardUniverse(SARLConfig, ProverInfo, Path) - Static method in class dev.civl.sarl.SARL: Returns a new standard symbolic universe, which supports all symbolic types, including Herbrand integer and real types, and ideal (mathematical) integers and reals.
newStandardUniverse(SARLConfig, ProverInfo, Path) - Static method in class dev.civl.sarl.universe.IF.Universes
newStandardUniverse(Path) - Static method in class dev.civl.sarl.SARL: Returns a new standard symbolic universe, which supports all symbolic types, including Herbrand integer and real types, and ideal (mathematical) integers and reals.
newStandardUniverse(Path) - Static method in class dev.civl.sarl.universe.IF.Universes
newTypeFactory(ObjectFactory) - Static method in class dev.civl.sarl.type.IF.Types
NO - Enum constant in enum class dev.civl.sarl.IF.ValidityResult.ResultType: No, the predicate is not valid under the given context
NONE - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicFunctionType.SpecialRelationKind: Not special relation
not(BooleanExpression) - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory: Returns a symbolic expression representing the logical negation of the given expression arg.
not(BooleanExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a symbolic expression representing the logical negation of the given expression arg.
NOT - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for logical negation ("not").
notLessThan(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a BooleanExpression with the result of the notLessThan operation on 2 NumericExpressions
notLessThanEquals(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a BooleanExpression with the result of the notLessThanEquals operation on 2 NumericExpressions
nthRootInt(IntegerNumber, IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Calculate the nth root of the given number and n.
ntRationalExpression(Monomial, Monomial) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Constructs new instance of NTRationalExpression.
NTReferenceExpression - Interface in dev.civl.sarl.IF.expr: A non-trivial ReferenceExpression, i.e., one which is not the null reference or the identity reference.
NTValueSetReference - Interface in dev.civl.sarl.IF.expr.valueSetReference: A non-trivial ValueSetReference, i.e., one which is not the identity reference.
NULL - Enum constant in enum class dev.civl.sarl.IF.expr.ReferenceExpression.ReferenceKind: The "null" reference.
NULL - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator used to represent no symbolic expression in cases where Java's null is not acceptable.
nullExpression() - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Returns the special expression "NULL", which has the NULL operator, null type, and no arguments.
nullExpression() - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the "NULL" expression.
nullReference() - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Returns the "null reference", a symbolic expression of reference type which is not equal to a reference value returned by any of the other methods, and which cannot be dereferenced.
nullReference() - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the "null reference", a symbolic expression of reference type which is not equal to a reference value returned by any of the other methods, and which cannot be dereferenced.
numArguments() - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression: The number of arguments (children) of this symbolic expression.
number() - Method in interface dev.civl.sarl.ideal.IF.Constant: Returns the underlying Number wrapped by this Constant.
number(int) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory
number(Number) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the concrete symbolic expression wrapping the given number.
number(NumberObject) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory
number(NumberObject) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the concrete symbolic expression wrapping the given number object.
number(String) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Makes best guest on type of number based on string.
Number - Interface in dev.civl.sarl.IF.number: A number is some kind of representation of a real number.
NUMBER - Enum constant in enum class dev.civl.sarl.IF.object.SymbolicObject.SymbolicObjectKind
numberFactory() - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns the number factory used by this numeric factory.
numberFactory() - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the number factory used by this universe.
numberFactory() - Method in interface dev.civl.sarl.object.IF.ObjectFactory
numberFactory() - Method in interface dev.civl.sarl.preuniverse.IF.FactorySystem
NumberFactory - Interface in dev.civl.sarl.IF.number: A number factory is used to produce concrete rational and integer numbers.
NumberFactory.IntervalUnion - Class in dev.civl.sarl.IF.number: A simple type for recording the result of attempting to take the union of two intervals i1 and i2.
numberObject(Number) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the NumberObject wrapping the given Number value.
numberObject(Number) - Method in interface dev.civl.sarl.object.IF.ObjectFactory
NumberObject - Interface in dev.civl.sarl.IF.object: A symbolic object wrapping a single instance of Number.
Numbers - Class in dev.civl.sarl.number.IF
Numbers() - Constructor for class dev.civl.sarl.number.IF.Numbers
numerator() - Method in interface dev.civl.sarl.IF.number.RationalNumber: Returns the numerator from a representation of this rational number as the quotient of two Java BigIntegers.
numerator(IdealFactory) - Method in interface dev.civl.sarl.ideal.IF.RationalExpression: Returns the numerator of this rational expression
numerator(RationalNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns the numerator in a representation of the rational number as the quotient of two integers.
numericalCompareTo(Number) - Method in interface dev.civl.sarl.IF.number.Number: This is a numerical comparison, so the order is a numerical order based on the value of this and other.
NumericExpression - Interface in dev.civl.sarl.IF.expr: Marker interface for an expression of numeric type ( SymbolicIntegerType SymbolicRealType).
NumericExpressionFactory - Interface in dev.civl.sarl.expr.IF: A NumericExpressionFactory provides all of the functionality needed to create and manipulate expressions of numeric type.
numericFactory() - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Returns the numeric expression factory used by this expression factory.
numericFactory() - Method in interface dev.civl.sarl.preuniverse.IF.FactorySystem
NumericSymbolicConstant - Interface in dev.civl.sarl.IF.expr: A SymbolicConstant which has integer or real type, i.e., type belonging to SymbolicIntegerType or SymbolicRealType.
numObjects() - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the number of canonic symbolic objects controlled by this universe.
numObjects() - Method in interface dev.civl.sarl.object.IF.ObjectFactory
numProverValidCalls() - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the total number of calls made to the validity method in the underlying automated theorem prover.
numTypes() - Method in interface dev.civl.sarl.IF.type.SymbolicTypeSequence: Returns the number of types in this sequence.
numValidCalls() - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the total number of calls made to methods Reasoner.valid(BooleanExpression) and Reasoner.validOrModel(BooleanExpression).

O

objectFactory() - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory

Returns the object factory used by this expression factory.

objectFactory() - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory

Returns the object factory used by this numeric factory.

objectFactory() - Method in interface dev.civl.sarl.preuniverse.IF.FactorySystem

objectFactory() - Method in interface dev.civl.sarl.preuniverse.IF.PreUniverse

Returns the ObjectFactory used by this universe.

objectFactory() - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory

ObjectFactory - Interface in dev.civl.sarl.object.IF

A factory for producing certain SymbolicObjects.

Objects - Class in dev.civl.sarl.object.IF

Objects() - Constructor for class dev.civl.sarl.object.IF.Objects

objectWithId(int) - Method in interface dev.civl.sarl.IF.CoreUniverse

Gets the canonic SymbolicObject belonging to this universe with the given ID number.

objectWithId(int) - Method in interface dev.civl.sarl.object.IF.ObjectFactory

Gets the canonic object with the given ID number.

OFFSET - Enum constant in enum class dev.civl.sarl.IF.expr.ReferenceExpression.ReferenceKind

An offset reference.

OFFSET - Enum constant in enum class dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference.VSReferenceKind

An offset reference.

offsetReference(ReferenceExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory

Given a ReferenceExpression and a NumericExpression offset, returns an offsetReference.

offsetReference(ReferenceExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

OffsetReference - Interface in dev.civl.sarl.IF.expr

A reference to some point which is specified by an integer "offset" from another reference.

one(SymbolicType) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

Returns either the integer number one (1) or the real number 1 (1.0).

oneInt() - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory

Returns a symbolic expression of integer type with the value of 1

oneInt() - Method in interface dev.civl.sarl.IF.CoreUniverse

The symbolic expression representing the integer 1.

oneInteger() - Method in interface dev.civl.sarl.IF.number.NumberFactory

The integer number zero.

oneIntegerObj() - Method in interface dev.civl.sarl.object.IF.ObjectFactory

oneIntObj() - Method in interface dev.civl.sarl.object.IF.ObjectFactory

oneIntObject() - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

Returns an IntObject wrapping the int 1.

oneRational() - Method in interface dev.civl.sarl.IF.number.NumberFactory

The rational number one.

oneReal() - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory

Returns a symbolic expression of real type with the value of 1

oneReal() - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the symbolic expression representing the real number 1.

oneRealObj() - Method in interface dev.civl.sarl.object.IF.ObjectFactory

oneTermMap(SymbolicType) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

Returns a

invalid reference

SymbolicMap

with a single entry mapping the monic One to itself.

operator() - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression

The operator of this symbolic expression.

or(BooleanExpression, BooleanExpression) - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory

Returns a symbolic expression representing the disjunction of the two given arguments.

or(BooleanExpression, BooleanExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns a symbolic expression representing the disjunction of the two given arguments.

or(Iterable<? extends BooleanExpression>) - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory

Returns a symbolic expression which represents the disjunction of the expressions in the given array args.

or(Iterable<? extends BooleanExpression>) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns a symbolic expression which represents the disjunction of the expressions in the given array args.

OR - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator

Operator for an expression representing the disjunction of symbolic expressions of boolean type.

outputType() - Method in interface dev.civl.sarl.IF.type.SymbolicFunctionType

The output type, a non-null symbolic type.

P

parameters - Variable in class dev.civl.sarl.prove.IF.ProverFunctionInterpretation

PARTIAL_ORDER - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicFunctionType.SpecialRelationKind

The function type represents a partial order binary relation

permut(SymbolicExpression, SymbolicExpression, NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

A permutation predicate, which asserts the slice from lower index low to higher index high in array array_a is a permutation of the slice from lower index low to higher index high in array array_b.

PIECEWISE_LINEAR_ORDER - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicFunctionType.SpecialRelationKind

The function type represents a piecewise linear order binary relation

plus(IntObject) - Method in interface dev.civl.sarl.IF.object.IntObject

Returns the result of addting this and that, as an IntObject.

polynomial(SymbolicType, Monomial[]) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

Produces the result of summing the Monomials of a term map as a Polynomial.

Polynomial - Interface in dev.civl.sarl.ideal.IF

A polynomial: an expression which is the sum of monomials.

polynomialDegree(NumberFactory) - Method in interface dev.civl.sarl.ideal.IF.Polynomial

The "polynomial degree" is the maximum monomial degree of the terms comprising this polynomial.

polynomialFactory() - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

What is the purpose of the polynomial factory.

polyProbThreshold - Static variable in class dev.civl.sarl.IF.SARLConstants

Used in a heuristic to determine when to use probabilistic methods to determine polynomial zero-ness.

positiveInfinityInteger() - Method in interface dev.civl.sarl.IF.number.NumberFactory

Return a IntegerNumber representing the positive infinity.

positiveInfinityRational() - Method in interface dev.civl.sarl.IF.number.NumberFactory

Return a RationalNumber representing the positive infinity.

power(NumericExpression, int) - Method in interface dev.civl.sarl.IF.CoreUniverse

Equivalent to power(base, intObject(exponent)).

power(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory

General power operator: e^b.

power(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

power(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

General power operator: e^b.

power(NumericExpression, IntegerNumber) - Method in interface dev.civl.sarl.IF.CoreUniverse

Concrete power operator: e^b, where b is a concrete non-negative IntegerNumber.

power(NumericExpression, NumberObject) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory

Concrete power operator: e^b, where b is a NumberObject with a concrete non-negative integer value.

power(IntegerNumber, int) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Calculate the given integer number powering a given exponent and returns result.

power(IntegerNumber, IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Calculate the given IntegerNumber base powering a given IntegerNumber exponent and returns result.

power(Interval, int) - Method in interface dev.civl.sarl.IF.number.NumberFactory

To calculate the power-result of a given non-null and not empty Interval with a given natural number.

power(Interval, IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory

To calculate the power-result of a given non-null and not empty Interval with a given non-null non-negative IntegerNumber.

power(Number, int) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Calculate the given number powering a given exponent and returns result.

power(Number, IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Calculate the given Number base powering a given IntegerNumber exponent and returns result.

power(RationalNumber, int) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Calculate the given rational number powering a given exponent and returns result.

power(RationalNumber, IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Calculate the given RationalNumber base powering a given IntegerNumber exponent and returns result.

power(Range, int) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory

Return a Range containing all x^exp, where x is in range and exp is a natural numbers.

power(Range, IntegerNumber) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory

Return a Range containing all x^exp, where x is in range and exp is an IntegerNumber.

POWER - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator

Operator for exponentiation, i.e., the raising of some number to some power: x ^y.

powerInt(IdealFactory, IntegerNumber) - Method in interface dev.civl.sarl.ideal.IF.Constant

powerInt(IdealFactory, IntegerNumber) - Method in interface dev.civl.sarl.ideal.IF.Monic

powerInt(IdealFactory, IntegerNumber) - Method in interface dev.civl.sarl.ideal.IF.Monomial

powerInt(IdealFactory, IntegerNumber) - Method in interface dev.civl.sarl.ideal.IF.PrimitivePower

powerInt(IdealFactory, IntegerNumber) - Method in interface dev.civl.sarl.ideal.IF.RationalExpression

Computes an expression equivalent to raising this expression to the exponent power.

powerRational(IdealFactory, RationalExpression) - Method in interface dev.civl.sarl.ideal.IF.RationalExpression

Computes an expression equivalent to raising this expression to the exponent power.

powerTermMap(SymbolicType, Monomial[], NumberObject) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

Raises a term map to the given power, returning the result as a term map.

Predicate<T> - Interface in dev.civl.sarl.IF

A Predicate on type T is an object that provides a method "apply" which takes an element of T and returns true or false.

PreUniverse - Interface in dev.civl.sarl.preuniverse.IF

A PreUniverse provides most of the services of a SymbolicUniverse, but not those that require reasoning, specifically theorem proving and simplification.

PreUniverses - Class in dev.civl.sarl.preuniverse.IF

PreUniverses() - Constructor for class dev.civl.sarl.preuniverse.IF.PreUniverses

primitive(IdealFactory) - Method in interface dev.civl.sarl.ideal.IF.PrimitivePower

Returns the Primitive which is the base in this primitive power expression.

Primitive - Interface in dev.civl.sarl.ideal.IF

A numeric primitive expression, e.g., a symbolic constant of numeric type, an array read expression of numeric type, or a tuple read expression of numeric type.

primitivePower(Primitive, NumberObject) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory

Returns an instance of PrimitivePower representing raising the given primitive the given exponent.

PrimitivePower - Interface in dev.civl.sarl.ideal.IF

A power of a Primitive expression, xⁱ, where x is a Primitive and i is a concrete positive int.

primitivePowerExponent(IdealFactory) - Method in interface dev.civl.sarl.ideal.IF.PrimitivePower

Returns the exponent in this primitive power expression, which is a positive integer represented as an NumberObject.

print(PrintStream) - Method in interface dev.civl.sarl.IF.config.ProverInfo

Prints a complete representation of this object in the format that is expected in a SARL configuration file.

printCompressed(SymbolicExpression, PrintStream) - Method in interface dev.civl.sarl.IF.CoreUniverse

Prints the expression by preceding with a sequence of definitions of sub-expressions which are used more than once.

printCompressedTree(String, SymbolicExpression, PrintStream) - Method in interface dev.civl.sarl.IF.CoreUniverse

Use this method to print large symbolic expression hierarchically.

printCompressedTree(String, StringBuffer) - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression

Prints compressed tree representation of this expression.

printExprTree(SymbolicExpression, PrintStream) - Method in interface dev.civl.sarl.IF.CoreUniverse

print symbolic expression as tree structure

Prove - Class in dev.civl.sarl.prove.IF

This is the entry point for module prove.

Prove() - Constructor for class dev.civl.sarl.prove.IF.Prove

ProverFunctionInterpretation - Class in dev.civl.sarl.prove.IF

A data structure that represents the interpretation of a

invalid reference

LogicFunction

ProverInfo - Interface in dev.civl.sarl.IF.config

Abstract interface representing information about an external theorem prover: what kind of prover it is, where it can be found, etc.

ProverInfo.ProverKind - Enum Class in dev.civl.sarl.IF.config

A classification of the different kinds of theorem provers.

pureType(SymbolicType) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the "pure" version of the type, i.e., the compatible SymbolicType that contains no SymbolicExpressions.

pureType(SymbolicType) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory

The pureType of t1 is t1 after removing the length for example, CommonSymbolicCompleteArrayType(type1) should have the same pureType as CommonSymbolicArrayType(type1)

put(SymbolicExpression, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

Q

quickEquals(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

R

Range - Interface in dev.civl.sarl.simplify.IF

An abstract representation of a set of Numbers.

Range.RangeSign - Enum Class in dev.civl.sarl.simplify.IF

A categorization of ranges based on their relationship to 0.

RangeFactory - Interface in dev.civl.sarl.simplify.IF

Factory for producing instances of Range.

rational(double) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the symbolic expression of real type (SymbolicRealType) representing the given double value.

rational(float) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the symbolic expression of real type (SymbolicRealType) representing the given float value.

rational(int) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the symbolic expression of real type (SymbolicRealType) representing the given int value.

rational(int, int) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the rational number obtained by dividing two integers, numerator and denominator.

rational(long) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the symbolic expression of real type (SymbolicRealType) representing the given long value.

rational(long, long) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the rational number obtained by dividing two long integers.

rational(Number) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns a rational representation of the number.

rational(String) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns the rational number specified by the given string, where the string is a decimal representation of the number.

rational(BigInteger) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the symbolic expression of real type (SymbolicRealType) representing the given BigInteger value.

rational(BigInteger, BigInteger) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the rational number obtained by dividing two BigIntegers.

rational(BigInteger, BigInteger) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Returns the rational number which is the quotient of the two given integers.

RationalExpression - Interface in dev.civl.sarl.ideal.IF

A RationalExpression is the quotient of two Monomials of real type.

RationalNumber - Interface in dev.civl.sarl.IF.number

An instance of this class represents a rational number.

REAL - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicType.SymbolicTypeKind

REAL_FACTORY - Static variable in class dev.civl.sarl.number.IF.Numbers

The only number factory you will ever need.

realKind() - Method in interface dev.civl.sarl.IF.type.SymbolicRealType

Returns the kind of real type this is.

realType() - Method in interface dev.civl.sarl.IF.CoreUniverse

The "ideal" real type, representing the set of mathematical real numbers.

realType() - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory

Reason - Class in dev.civl.sarl.reason.IF

Provides a static method for producing a new ReasonerFactory.

Reason() - Constructor for class dev.civl.sarl.reason.IF.Reason

reasoner(BooleanExpression) - Method in interface dev.civl.sarl.IF.SymbolicUniverse

Returns a Reasoner for the given context.

reasoner(List<BooleanExpression>) - Method in interface dev.civl.sarl.IF.SymbolicUniverse

Reasoner - Interface in dev.civl.sarl.IF

A reasoner provides methods to simplify SymbolicExpressions and prove or disprove certain theorems, all under an over-arching assumption known as the "context".

ReasonerFactory - Interface in dev.civl.sarl.reason.IF

A factory for producing instances of Reasoner.

reduction(SymbolicExpression[], NumericExpression, SymbolicExpression, List<BooleanExpression>) - Method in interface dev.civl.sarl.IF.CoreUniverse

a $reduction function that takes a list of operands, the number of elements per operand and an operator, returns the element-wise reduction result of the operator over the operands.

referencedType(SymbolicType, ReferenceExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the type referenced by a reference into an expression of the given type.

ReferenceExpression - Interface in dev.civl.sarl.IF.expr

An expression representing a way to reference into values.

ReferenceExpression.ReferenceKind - Enum Class in dev.civl.sarl.IF.expr

The different kinds of references.

referenceKind() - Method in interface dev.civl.sarl.IF.expr.ReferenceExpression

Gets the kind of this reference.

referenceType() - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory

referenceType() - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns the type of all reference expressions.

REGULAR - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicRange.RangeKind

A range of values which are evenly spaced by a step value.

relativeGaussianElimination(RationalNumber[][], RationalNumber[][]) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Performs a form of "relative Gauss-Jordan elimination".

remove(int) - Method in interface dev.civl.sarl.IF.object.SymbolicSequence

"Removes" the element at position index, shifting all subsequent elements down one; more precisely, returns a new sequence obtained by removing that element from this sequence.

removeElementAt(SymbolicExpression, int) - Method in interface dev.civl.sarl.IF.CoreUniverse

Removes an element in a specified position in a concrete symbolic array.

removeEntryWithKey(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

removeQuantifiers(BooleanExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

Returns arg with all clauses containing quantifers removed.

restrictLower(Interval, Number, boolean) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Restricts the lower bound of an interval as specified.

restrictUpper(Interval, Number, boolean) - Method in interface dev.civl.sarl.IF.number.NumberFactory

Restricts the upper bound of an interval as specified.

RESULT_MAYBE - Static variable in class dev.civl.sarl.prove.IF.Prove

A constant of type ValidityResult which has ValidityResult.ResultType

invalid reference

ResultType.MAYBE

RESULT_NO - Static variable in class dev.civl.sarl.prove.IF.Prove

A constant of type ValidityResult which has ValidityResult.ResultType

invalid reference

ResultType.NO

RESULT_YES - Static variable in class dev.civl.sarl.prove.IF.Prove

A constant of type ValidityResult which has ValidityResult.ResultType

invalid reference

ResultType.YES

roundToZero(NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory

roundToZero(NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse

Given an expression x of real type, returns an expression of integer type representing the resulting of rounding x towards 0.

S

SARL - Class in dev.civl.sarl: The SARL class provides static methods for creating new symbolic universes.
SARL() - Constructor for class dev.civl.sarl.SARL
SARLBoundException - Exception Class in dev.civl.sarl.IF: An exception that occurs when an index is out of bounds.
SARLBoundException(SymbolicExpression, NumericExpression, NumericExpression, NumericExpression, String) - Constructor for exception class dev.civl.sarl.IF.SARLBoundException: Constructs new out-of-bounds exception with a message formed from the given parameters.
SARLConfig - Interface in dev.civl.sarl.IF.config: A SARL configuration encapsulates information about the complete set of external theorem provers available to SARL.
SARLConstants - Class in dev.civl.sarl.IF
SARLConstants() - Constructor for class dev.civl.sarl.IF.SARLConstants
SARLException - Exception Class in dev.civl.sarl.IF: Root of the SARL exception type hierarchy.
SARLException(String) - Constructor for exception class dev.civl.sarl.IF.SARLException
SARLInternalException - Exception Class in dev.civl.sarl.IF: A SARL internal exception represents an error that is "not supposed to happen." It can be used like an assertion, whenever you feel that something should always be true.
SARLInternalException(String) - Constructor for exception class dev.civl.sarl.IF.SARLInternalException: Constructs a new instance whose message is formed by pre-pending to the given msg string stating that this is an internal error and the error should be reported to the developers.
scientificString(RationalNumber, int) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Constructs a string representation of the given rational number in scientific notation: x.xxxx * 10^{-yyy}.
sequence() - Method in interface dev.civl.sarl.IF.type.SymbolicTupleType: Returns the sequence of component types of this tuple object.
sequence() - Method in interface dev.civl.sarl.IF.type.SymbolicUnionType: The sequence of types comprising this union.
sequence(SymbolicType[]) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory: Creates a SymbolicTypeSequecne from an array of SymbolicType
sequence(Iterable<? extends SymbolicType>) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory: Creates a SymbolicTypeSequence from a list of SymbolicTypes
sequence(Iterable<? extends T>) - Method in interface dev.civl.sarl.object.IF.ObjectFactory: Returns a SymbolicSequence comprising the given sequence of elements.
sequence(T[]) - Method in interface dev.civl.sarl.object.IF.ObjectFactory: Returns a SymbolicSequence comprising the sequence of elements specified as an array.
SEQUENCE - Enum constant in enum class dev.civl.sarl.IF.object.SymbolicObject.SymbolicObjectKind
set(int, T) - Method in interface dev.civl.sarl.IF.object.SymbolicSequence: "Sets" the element at specified position, or, more precisely, returns a new sequence identical to this except with the element at the specified index set to the given element.
SET - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicType.SymbolicTypeKind
setAdd(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse
setDifference(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse
setErrFile(String) - Method in interface dev.civl.sarl.IF.CoreUniverse: Summary:Set name (path) for prover unexpected error file.
setExpressionComparator(Comparator<SymbolicExpression>) - Method in interface dev.civl.sarl.object.IF.ObjectFactory: Sets the expression comparator for this object factory.
setExpressionComparator(Comparator<SymbolicExpression>) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory: setting the way you want to comparator to compare two expressions used when comparing CompleteArrayType
setExtend(int, T, T) - Method in interface dev.civl.sarl.IF.object.SymbolicSequence: If index is less than the original size s, same as set.
setInCanonic() - Method in interface dev.civl.sarl.IF.object.SymbolicObject: Set the id of this object to a special value indicating that this object is in the process of being made canonic.
setIntegerLengthBound(int) - Method in interface dev.civl.sarl.IF.CoreUniverse: Set the upper bound of the length of the integer type.
setIntersection(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse
setKind(ProverInfo.ProverKind) - Method in interface dev.civl.sarl.IF.config.ProverInfo: Sets the prover kind.
setLogicFunctions(ProverFunctionInterpretation[]) - Method in interface dev.civl.sarl.IF.SymbolicUniverse: Set a list of logic functions with their definitions to the universe so that Reasoners created by this universe can take use of the definitions of the given logic functions.
setMinus(Range, Range) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Return the difference Range of range0 and range1.
setNumericExpressionFactory(NumericExpressionFactory) - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory: The boolean factory needs a numeric expression factory in order to negate expressions like "ainvalid input: '<'b" or "ainvalid input: '<'=b".
setOrder(RationalNumber) - Method in interface dev.civl.sarl.IF.object.SymbolicObject: Experimental: sets the number which imposes a total order on the set of all canonic symbolic object.
setOutputStream(PrintStream) - Method in interface dev.civl.sarl.IF.CoreUniverse: Sets the output stream, the stream to which information (such as queries) will be printed.
setPath(File) - Method in interface dev.civl.sarl.IF.config.ProverInfo: Sets the path to the executable theorem prover.
setProbabilisticBound(RationalNumber) - Method in interface dev.civl.sarl.IF.CoreUniverse: Sets the upper bound on the probability of error when deciding whether a polynomial is 0.
setRemove(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse
setShowErrors(boolean) - Method in interface dev.civl.sarl.IF.config.ProverInfo: Sets whether the prover prints a message every time the underlying theorem prover reports an error.
setShowInconclusives(boolean) - Method in interface dev.civl.sarl.IF.config.ProverInfo: Sets whether the prover prints a message every time it reports an inconclusive result.
setShowProverQueries(boolean) - Method in interface dev.civl.sarl.IF.CoreUniverse: Sets the showProverQueries flag.
setShowQueries(boolean) - Method in interface dev.civl.sarl.IF.config.ProverInfo: Tell this prover whether it should print every query.
setShowQueries(boolean) - Method in interface dev.civl.sarl.IF.CoreUniverse: Sets the showQueries flag.
setTimeout(double) - Method in interface dev.civl.sarl.IF.config.ProverInfo: Sets the timeout, i.e., the time limit in seconds.
setType(SymbolicType) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the type for "set of T"; not yet implemented.
setType(SymbolicType) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory
setTypeComparator(Comparator<SymbolicType>) - Method in interface dev.civl.sarl.object.IF.ObjectFactory: Sets the type comparator of for this factory.
setTypeSequenceComparator(Comparator<SymbolicTypeSequence>) - Method in interface dev.civl.sarl.object.IF.ObjectFactory: Sets the type sequence comparator of this factory.
setUnion(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse
setUnsatisfiability(ValidityResult.ResultType) - Method in interface dev.civl.sarl.IF.expr.BooleanExpression: Store the unsatisfiability result for this boolean expression.
setUseBackwardSubstitution(boolean) - Method in interface dev.civl.sarl.IF.CoreUniverse: Sets the value of the "useBackwardSubstitution" flag.
setValidity(ValidityResult.ResultType) - Method in interface dev.civl.sarl.IF.expr.BooleanExpression: Store the validity result for this boolean expression.
setVersion(String) - Method in interface dev.civl.sarl.IF.config.ProverInfo: Sets the version string.
sigma(NumericExpression, NumericExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: A fold sum expression.
sign() - Method in interface dev.civl.sarl.simplify.IF.Range: Get the Range.RangeSign of this range.
signum() - Method in interface dev.civl.sarl.IF.number.Number: Returns 0 if this number equals 0, -1 if this number is negative, 1 if this number is positive.
signum() - Method in interface dev.civl.sarl.IF.object.IntObject: Returns -1 if the int value is negative, 0 if the int value is zero, or +1 if the int value is positive.
signum() - Method in interface dev.civl.sarl.IF.object.NumberObject: Returns either -1, 0, or +1, depending on whether the value of this expression is invalid input: '<'0, 0, or >0 (respectively).
simpleSubstituter(SymbolicConstant, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a substituter that replaces a specific symbolic constant with some specific value.
simplify(T) - Method in interface dev.civl.sarl.IF.Reasoner: Simplify the given expression under the context.
simplify(T, Set<SymbolicConstant>) - Method in interface dev.civl.sarl.IF.Reasoner
Simplify - Class in dev.civl.sarl.simplify.IF: Entry point for module "simplify", providing static method to create basic range factories and context partitions
Simplify() - Constructor for class dev.civl.sarl.simplify.IF.Simplify
SINGLETON - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicRange.RangeKind: A range consisting of a single value.
singletonInterval(Number) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns the interval consisting of the single finite number x: [x,x].
singletonSequence(SymbolicType) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory: Creates a SymbolicTypeSequence of 1 element that has a SymbolicType
singletonSequence(T) - Method in interface dev.civl.sarl.object.IF.ObjectFactory: Returns the sequence of length 1 consisting of the given element.
singletonSet(Number) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Returns a Range consisting of exactly one interval representing the single specified Number number.
The type of number determines the type of returned Range.
Preconditions:
> The number must be non-null and infinite.
size() - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression
size() - Method in interface dev.civl.sarl.IF.object.SymbolicSequence: Returns the number of elements in this sequence.
soleSelector() - Method in interface dev.civl.sarl.IF.type.SymbolicUninterpretedType
specialRelationKind() - Method in interface dev.civl.sarl.IF.type.SymbolicFunctionType
status - Variable in class dev.civl.sarl.IF.number.NumberFactory.IntervalUnion
step() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.VSArraySectionReference
strictLower() - Method in interface dev.civl.sarl.IF.number.Interval: Is the lower bound strict, i.e., does the interval consist of all x strictly greater than the lower bound and ...?
strictlyBelow(SymbolicRange, SymbolicRange) - Method in interface dev.civl.sarl.expr.IF.SymbolicRangeFactory: NOTE: Currently only support ranges with a step value of 1.
strictUpper() - Method in interface dev.civl.sarl.IF.number.Interval: Is the upper bound strict, i.e., does the interval consist of all x strictly less than the upper bound and ...?
STRING - Enum constant in enum class dev.civl.sarl.IF.object.SymbolicObject.SymbolicObjectKind
stringExpression(String) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a symbolic expression of type array-of-char which is a literal array consisting of the sequence of characters in the given string.
stringObject(String) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the StringObject wrapping the given String value.
stringObject(String) - Method in interface dev.civl.sarl.object.IF.ObjectFactory
StringObject - Interface in dev.civl.sarl.IF.object: A symbolic object wrapping a single String.
subSequence(int, int) - Method in interface dev.civl.sarl.IF.object.SymbolicSequence: Returns the subsequence whose first element is the element at position start and last element is the element at position end-1.
subset(SymbolicRange, SymbolicRange) - Method in interface dev.civl.sarl.expr.IF.SymbolicRangeFactory: NOTE: Currently only support ranges with a step value of 1.
subtract(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a symbolic expression which is the result of subtracting arg1 and arg0.
subtract(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory
subtract(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns a symbolic expression which is the result of subtracting arg1 from arg0.
subtract(IntegerNumber, IntegerNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Subtracts two integer numbers and returns the result.
subtract(Number, Number) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Subtracts two numbers and returns result.
subtract(RationalNumber, RationalNumber) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Subtracts two rational numbers and returns the result.
subtract(Range, Number) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Return a Range containing all x-constant, where x is in range and constant is a non- null finite Number.
subtract(Range, Range) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Return a Range containing all x-y, where x is in range0 and y is in range1.
SUBTRACT - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for numerical subtraction: x − y.
symbolic(boolean) - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory: Short cut for symbolic(booleanObject(value)).
symbolic(BooleanObject) - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory: The symbolic expression wrapping the given boolean object (true or false).
SYMBOLIC_CONSTANT - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator used to represent a symbolic constant.
SymbolicArrayType - Interface in dev.civl.sarl.IF.type: An array type T[].
SymbolicCompleteArrayType - Interface in dev.civl.sarl.IF.type: A complete array type specifies not only the element type but also the extent (length) of the array.
symbolicConstant(StringObject, SymbolicType) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory
symbolicConstant(StringObject, SymbolicType) - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory
symbolicConstant(StringObject, SymbolicType) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the SymbolicConstant with the given name and type.
SymbolicConstant - Interface in dev.civl.sarl.IF.expr: A "symbolic constant" is a symbol used in symbolic execution to represent an input value.
SymbolicExpression - Interface in dev.civl.sarl.IF.expr: An instance SymbolicExpression represents a symbolic expression.
SymbolicExpression.SymbolicOperator - Enum Class in dev.civl.sarl.IF.expr: An enumerated type for the different kinds of symbolic expressions.
SymbolicFunctionType - Interface in dev.civl.sarl.IF.type: A function type is specified by the number and types of inputs, and a single output type.
SymbolicFunctionType.SpecialRelationKind - Enum Class in dev.civl.sarl.IF.type
SymbolicIntegerType - Interface in dev.civl.sarl.IF.type: SymbolicIntegerType is an interface that contains representation for a Symbolic Integer Type: It has three kinds: - herbrand: it doesn't do simplifications, when used in equations - ideal: - bounded: Also it has a method to return the kind of the integer.
SymbolicIntegerType.IntegerKind - Enum Class in dev.civl.sarl.IF.type: three kinds for the integer type
SymbolicMapType - Interface in dev.civl.sarl.IF.type: T map type is a type consisting of two components: a key type K and a value type V.
SymbolicObject - Interface in dev.civl.sarl.IF.object: The root of the symbolic object type hierarchy.
SymbolicObject.SymbolicObjectKind - Enum Class in dev.civl.sarl.IF.object
symbolicObjectKind() - Method in interface dev.civl.sarl.IF.object.SymbolicObject: Which kind of symbolic object is this? The kind determines the specific type to which this object can be safely cast.
symbolicRange(NumericExpression) - Method in interface dev.civl.sarl.expr.IF.SymbolicRangeFactory: Generates a new SymbolicRange which only includes "element".
symbolicRange(NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.SymbolicRangeFactory: Generates a new SymbolicRange which ranges from "lower" (inclusive) to "upper" (exclusive).
symbolicRange(NumericExpression, NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.SymbolicRangeFactory: Generates a new SymbolicRange which ranges from "lower" (inclusive) to "upper" (exclusive) taking "step" number of steps.
SymbolicRange - Interface in dev.civl.sarl.IF.expr: Represents a symbolic range of integer values.
SymbolicRange.RangeKind - Enum Class in dev.civl.sarl.IF.expr
SymbolicRangeFactory - Interface in dev.civl.sarl.expr.IF: Factory for creating and manipulating SymbolicRange's.
SymbolicRealType - Interface in dev.civl.sarl.IF.type: A real number type.
SymbolicRealType.RealKind - Enum Class in dev.civl.sarl.IF.type: The different kinds of real types.
symbolicRepresentation(NumericExpression, PreUniverse) - Method in interface dev.civl.sarl.simplify.IF.Range: Given a NumericExpression x, returns a BooleanExpression which holds iff x is in this Range.
SymbolicSequence<T> - Interface in dev.civl.sarl.IF.object: A finite ordered immutable sequence of symbolic expressions.
SymbolicSetType - Interface in dev.civl.sarl.IF.type: The type representing a set.
SymbolicTupleType - Interface in dev.civl.sarl.IF.type: A tuple type is specified by (1) a name, and (2) an ordered, finite sequence of component types.
SymbolicType - Interface in dev.civl.sarl.IF.type: A symbolic type represents the type of a symbolic expression.
SymbolicType.SymbolicTypeKind - Enum Class in dev.civl.sarl.IF.type: The different kinds of types.
SymbolicTypeFactory - Interface in dev.civl.sarl.type.IF: A factory used to produce SymbolicTypes and other related objects.
SymbolicTypeSequence - Interface in dev.civl.sarl.IF.type: A finite, ordered sequence of SymbolicType.
symbolicUninterpretedType(String) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns an uninterpreted type which is an instance of SymbolicUninterpretedType.
SymbolicUninterpretedType - Interface in dev.civl.sarl.IF.type: This class represents uninterpreted types.
SymbolicUnionType - Interface in dev.civl.sarl.IF.type: A union type of a sequence of types t_i.
SymbolicUniverse - Interface in dev.civl.sarl.IF: A symbolic universe is used for the creation and manipulation of SymbolicObjects.

T

termMap(IdealFactory) - Method in interface dev.civl.sarl.ideal.IF.Monomial: Returns the term map of this monomial.
TheoremProver - Interface in dev.civl.sarl.prove.IF: Provides an abstract interface for an automated theorem prover operating under a fixed context (i.e., a boolean expression assumed to hold).
TheoremProverException - Exception Class in dev.civl.sarl.IF
TheoremProverException(String) - Constructor for exception class dev.civl.sarl.IF.TheoremProverException
TheoremProverFactory - Interface in dev.civl.sarl.prove.IF: A factory for producing instances of TheoremProver.
toString() - Method in interface dev.civl.sarl.IF.object.SymbolicObject: Returns a string representation of this object, included here to emphasize that the method provided by Object must be overridden! Same as toStringBuffer(false).toString();
toStringBuffer(boolean) - Method in interface dev.civl.sarl.IF.object.SymbolicObject: Returns a string representation of this object as a StringBuffer.
toStringBufferLong() - Method in interface dev.civl.sarl.IF.object.SymbolicObject: Returns a detailed string representation of this object as a StringBuffer.
totalDegree(NumberFactory) - Method in interface dev.civl.sarl.ideal.IF.Monomial: The degree of this monomial if it were fully expanded to a polynomial in which the variables cannot be expressed as the sum, product, difference, or quotient of expressions.
Transform<S,T> - Interface in dev.civl.sarl.IF: A Transform from type S to type T is an object that provides a method "apply" which takes an element of S and returns an element of T.
TREE_ORDER - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicFunctionType.SpecialRelationKind: The function type represents a tree order binary relation
trivialProverFactory() - Static method in class dev.civl.sarl.prove.IF.Prove
trueExpr() - Method in interface dev.civl.sarl.expr.IF.BooleanExpressionFactory: Returns a true BooleanExpression
trueExpression() - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the boolean literal true.
trueObj() - Method in interface dev.civl.sarl.object.IF.ObjectFactory
tryUnion(Reasoner, SymbolicRange, SymbolicRange) - Method in interface dev.civl.sarl.expr.IF.SymbolicRangeFactory: Attempts to create a single SymbolicRange which is equivalent to the union of the input SymbolicRanges range0 and range1.
tuple(SymbolicTupleType, SymbolicExpression[]) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the concrete tuple with the given members.
tuple(SymbolicTupleType, Iterable<? extends SymbolicObject>) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the concrete tuple expression with the given tuple components.
TUPLE - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: A concrete tuple.
TUPLE - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicType.SymbolicTypeKind
TUPLE_COMPONENT - Enum constant in enum class dev.civl.sarl.IF.expr.ReferenceExpression.ReferenceKind: A tuple component reference.
TUPLE_COMPONENT - Enum constant in enum class dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference.VSReferenceKind: A tuple component reference.
TUPLE_READ - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the result of reading a component of a tuple.
TUPLE_WRITE - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for an expression representing the result of modifying a single component of a tuple.
tupleComponentReference(ReferenceExpression, IntObject) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Given a reference to a tuple, and a field index, returns a reference to that component of the tuple
tupleComponentReference(ReferenceExpression, IntObject) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given a reference to a tuple, and a field index, returns a reference to that component of the tuple.
TupleComponentReference - Interface in dev.civl.sarl.IF.expr: A reference into a specified field of a tuple value.
tupleRead(SymbolicExpression, IntObject) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns an expression that represents the result of reading a component in a tuple value.
tupleType(StringObject, SymbolicTypeSequence) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory: Creates a SymbolicTupleType
tupleType(StringObject, Iterable<? extends SymbolicType>) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the tuple type defined by the given sequence of component types.
tupleWrite(SymbolicExpression, IntObject, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns an expression representing the result of modifying a tuple by changing the value of one component.
type() - Method in interface dev.civl.sarl.IF.expr.SymbolicConstant: Returns the type of this symbolic constant.
type() - Method in interface dev.civl.sarl.IF.expr.SymbolicExpression: Returns the type of this symbolic expression.
TYPE - Enum constant in enum class dev.civl.sarl.IF.object.SymbolicObject.SymbolicObjectKind
TYPE_SEQUENCE - Enum constant in enum class dev.civl.sarl.IF.object.SymbolicObject.SymbolicObjectKind
typeComparator() - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory: Creates a TypeComparator that is used to compare SymbolicTypes
typeFactory() - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Returns the symbolic type factory used by this expression factory.
typeFactory() - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns the type factory used by this numeric expression factory.
typeFactory() - Method in interface dev.civl.sarl.preuniverse.IF.FactorySystem
typeFactory() - Method in interface dev.civl.sarl.preuniverse.IF.PreUniverse: Returns the SymbolicTypeFactory used by this universe.
typeKind() - Method in interface dev.civl.sarl.IF.type.SymbolicType: Returns the kind of the type.
Types - Class in dev.civl.sarl.type.IF: This class provides a static method for the creation of a new SymbolicTypeFactory.
Types() - Constructor for class dev.civl.sarl.type.IF.Types
typeSequence(Iterable<? extends SymbolicType>) - Method in interface dev.civl.sarl.preuniverse.IF.PreUniverse: Given an iterable collection of SymbolicTypes, returns a SymbolicTypeSequence conatining those SymbolicTypes

U

UnaryOperator<T> - Interface in dev.civl.sarl.IF: A UnaryOperator on a type T is an object which provides a method "apply" that takes an element of T and returns an element of T.
UNINTERPRETED - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicType.SymbolicTypeKind
uninterpretedType(StringObject) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory: Returns an uninterpreted type which is an instance of SymbolicUninterpretedType.
union - Variable in class dev.civl.sarl.IF.number.NumberFactory.IntervalUnion
union(Interval, Interval, NumberFactory.IntervalUnion) - Method in interface dev.civl.sarl.IF.number.NumberFactory: Computes the union of two intervals or reports that the union is not an interval and why.
union(Range, Range) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Return the union Range of range0 and range1.
UNION - Enum constant in enum class dev.civl.sarl.IF.type.SymbolicType.SymbolicTypeKind
UNION_EXTRACT - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for extracting an element of a SymbolicUnionType to an element of a member type.
UNION_INJECT - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator for injecting an element of a member type into a SymbolicUnionType that includes that member type.
UNION_MEMBER - Enum constant in enum class dev.civl.sarl.IF.expr.ReferenceExpression.ReferenceKind: A union member reference.
UNION_MEMBER - Enum constant in enum class dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference.VSReferenceKind: A union member reference.
UNION_TEST - Enum constant in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Operator to determine whether an expression in a SymbolicUnionType is in the image of injection from a specified member type.
unionExtract(IntObject, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Casts an object whose type is a union type to a representation whose type is the appropriate member type of the union type.
unionInject(SymbolicUnionType, IntObject, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Casts an object belonging to one of the members of a union type to the union type.
unionMemberReference(ReferenceExpression, IntObject) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Given a reference to a union (expression of union type) and an index of a member type of that union, returns a reference to the underlying element
unionMemberReference(ReferenceExpression, IntObject) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given a reference to a union (expression of union type) and an index of a member type of that union, returns a reference to the underlying element.
UnionMemberReference - Interface in dev.civl.sarl.IF.expr: A reference to a member of a SymbolicUnionType.
unionTest(IntObject, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Tests whether an object of a union type is in the image of injection from the member type of the given index.
unionType(StringObject, SymbolicTypeSequence) - Method in interface dev.civl.sarl.type.IF.SymbolicTypeFactory: Creates a SymbolicUnionType
unionType(StringObject, Iterable<? extends SymbolicType>) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the type which is the union of the given member types.
universalIntegerInterval() - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns the universal integer interval: (-∞, +∞).
universalRealInterval() - Method in interface dev.civl.sarl.IF.number.NumberFactory: Returns the universal real interval: (-∞, +∞).
universalSet(boolean) - Method in interface dev.civl.sarl.simplify.IF.RangeFactory: Returns a range of either integer or real type.
Universes - Class in dev.civl.sarl.universe.IF: This class provides static methods for the creation of new SymbolicUniverses.
Universes() - Constructor for class dev.civl.sarl.universe.IF.Universes
unsat(BooleanExpression) - Method in interface dev.civl.sarl.IF.Reasoner: Attempts to determine whether the statement p(x) invalid input: '&'invalid input: '&' q(x) is unsatisfiable.
unsat(BooleanExpression) - Method in interface dev.civl.sarl.prove.IF.TheoremProver: Attempts to determine whether the statement p(x) invalid input: '&'invalid input: '&' q(x) is unsatisfiable.
upper() - Method in interface dev.civl.sarl.IF.number.Interval: The upper bound of this interval.
upperBound - Variable in class dev.civl.sarl.IF.CoreUniverse.ForallStructure: The upper bound (inclusive) of the bound variable.
upperBound - Variable in exception class dev.civl.sarl.IF.SARLBoundException: The greatest value that an index should take; can be null, representing "unknown"
upperBound() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.VSArraySectionReference
useBackwardSubstitution - Static variable in class dev.civl.sarl.IF.SARLConstants: Shall this universe use backwards substitution to solve for certain numeric expressions in terms of others when simplifying? This is used in the Gaussian elimination simplification phase.
useDoubleOrNegation - Static variable in class dev.civl.sarl.IF.SARLConstants: Should an "OR" expression e be simplified as not(simplify(not(e))) ?
useMultiOrReduction - Static variable in class dev.civl.sarl.IF.SARLConstants: A technique for simplifying a context in CNF form that contains multiple or-clauses.
Using SARL - Search tag in Overview: Section

V

valid(BooleanExpression) - Method in interface dev.civl.sarl.IF.Reasoner: Attempts to determine whether the statement p(x)=>q(x) is a tautology.
valid(BooleanExpression) - Method in interface dev.civl.sarl.prove.IF.TheoremProver: Attempts to determine whether the statement p(x)=>q(x) is valid, i.e., is a tautology.
validityResult(ValidityResult.ResultType) - Static method in class dev.civl.sarl.prove.IF.Prove: Returns one of the constants Prove.RESULT_YES, Prove.RESULT_NO, Prove.RESULT_MAYBE, corresponding to the given type.
ValidityResult - Interface in dev.civl.sarl.IF: A ValidityResult represents the result of a validity query.
ValidityResult.ResultType - Enum Class in dev.civl.sarl.IF: The 3 kinds of results to the "valid" question: yes, no, or maybe (a.k.a, "I don't know").
validOrModel(BooleanExpression) - Method in interface dev.civl.sarl.IF.Reasoner: Attempts to determine whether p(x)=>q(x) is valid, and, if not, also returns a model (counter-example).
validOrModel(BooleanExpression) - Method in interface dev.civl.sarl.prove.IF.TheoremProver: Attempts to determine whether p(x)=>q(x) is valid, and, if not, also returns a model (counterexample).
value() - Method in interface dev.civl.sarl.ideal.IF.Constant: Returns the NumberObject wrapped by this Constant.
valueOf(String) - Static method in enum class dev.civl.sarl.IF.config.ProverInfo.ProverKind: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class dev.civl.sarl.IF.expr.ReferenceExpression.ReferenceKind: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class dev.civl.sarl.IF.expr.SymbolicRange.RangeKind: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference.VSReferenceKind: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class dev.civl.sarl.IF.object.SymbolicObject.SymbolicObjectKind: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class dev.civl.sarl.IF.type.SymbolicFunctionType.SpecialRelationKind: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class dev.civl.sarl.IF.type.SymbolicIntegerType.IntegerKind: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class dev.civl.sarl.IF.type.SymbolicRealType.RealKind: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class dev.civl.sarl.IF.type.SymbolicType.SymbolicTypeKind: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class dev.civl.sarl.IF.ValidityResult.ResultType: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class dev.civl.sarl.simplify.IF.Range.RangeSign: Returns the enum constant of this class with the specified name.
values() - Static method in enum class dev.civl.sarl.IF.config.ProverInfo.ProverKind: Returns an array containing the constants of this enum class, in the order they are declared.
values() - Static method in enum class dev.civl.sarl.IF.expr.ReferenceExpression.ReferenceKind: Returns an array containing the constants of this enum class, in the order they are declared.
values() - Static method in enum class dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator: Returns an array containing the constants of this enum class, in the order they are declared.
values() - Static method in enum class dev.civl.sarl.IF.expr.SymbolicRange.RangeKind: Returns an array containing the constants of this enum class, in the order they are declared.
values() - Static method in enum class dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference.VSReferenceKind: Returns an array containing the constants of this enum class, in the order they are declared.
values() - Static method in enum class dev.civl.sarl.IF.object.SymbolicObject.SymbolicObjectKind: Returns an array containing the constants of this enum class, in the order they are declared.
values() - Static method in enum class dev.civl.sarl.IF.type.SymbolicFunctionType.SpecialRelationKind: Returns an array containing the constants of this enum class, in the order they are declared.
values() - Static method in enum class dev.civl.sarl.IF.type.SymbolicIntegerType.IntegerKind: Returns an array containing the constants of this enum class, in the order they are declared.
values() - Static method in enum class dev.civl.sarl.IF.type.SymbolicRealType.RealKind: Returns an array containing the constants of this enum class, in the order they are declared.
values() - Static method in enum class dev.civl.sarl.IF.type.SymbolicType.SymbolicTypeKind: Returns an array containing the constants of this enum class, in the order they are declared.
values() - Static method in enum class dev.civl.sarl.IF.ValidityResult.ResultType: Returns an array containing the constants of this enum class, in the order they are declared.
values() - Static method in enum class dev.civl.sarl.simplify.IF.Range.RangeSign: Returns an array containing the constants of this enum class, in the order they are declared.
valueSetAssigns(SymbolicExpression, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Copies a subset of a value v to another value v' with a given value set template.
valueSetContains(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Test if a value set template vst0 contains another value set template vst1.
valueSetContains(SymbolicType, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Test if an array of value set references "refArr0", that is associated with the given "valueType", contains another array of value set references "refArr1", that is associated with the given "valueType" as well.
valueSetDiff(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given two value set templates, returns their set difference.
valueSetDiff(SymbolicType, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory
valueSetElimWidening(BooleanExpression, SymbolicExpression, SymbolicExpression, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.SymbolicUniverse
valueSetElimWidening(Reasoner, SymbolicType, SymbolicExpression, SymbolicExpression, NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory
valueSetHavoc(SymbolicExpression, SymbolicExpression, String, int) - Method in interface dev.civl.sarl.IF.CoreUniverse
valueSetNoIntersect(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Test if two value set templates have no intersection, i.e., if applying the two templates to the same object, their referred parts have no overlap.
valueSetProtectiveWidening(BooleanExpression, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.SymbolicUniverse
valueSetProtectiveWidening(Reasoner, SymbolicType, SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory
valueSetRefereceNoIntersect(SymbolicType, ValueSetReference, ValueSetReference) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Tests if the two given ValueSetReferences have NO intersection, i.e., if applying the two reference to the same object, if their referred parts have no overlap.
ValueSetReference - Interface in dev.civl.sarl.IF.expr.valueSetReference
ValueSetReference.VSReferenceKind - Enum Class in dev.civl.sarl.IF.expr.valueSetReference: The different kinds of reference set elements.
valueSetReferenceKind() - Method in interface dev.civl.sarl.IF.expr.valueSetReference.ValueSetReference: Gets the kind of this value set reference.
valueSetReferences(SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the set of ValueSetReferences in the given value set template.
valueSetReferenceType() - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory
valueSetReferenceType() - Method in interface dev.civl.sarl.IF.CoreUniverse
valueSetTemplate(SymbolicType, ValueSetReference[]) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Given a symbolic type of a symbolic value and a list of ValueSetReferences, returns symbolic expression representing a value set template.
valueSetTemplate(SymbolicType, ValueSetReference[]) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given a symbolic type of a symbolic value and a list of ValueSetReferences, returns symbolic expression representing a value set template.
valueSetTemplateType() - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Returns the type of a value set template.
valueSetTemplateType() - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the type of a value set template.
valueSetUnion(SymbolicExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given two value set templates, returns the union of the two.
valueSetWidening(BooleanExpression, SymbolicExpression) - Method in interface dev.civl.sarl.IF.SymbolicUniverse: Apply a default widening operator to the value set references in the given value set template.
valueSetWidening(Reasoner, SymbolicType, SymbolicExpression) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Apply a default widening operator to a value set template, which is in the form of an array of value set references and a symbolic type that is referred by these references.
valueType() - Method in interface dev.civl.sarl.IF.type.SymbolicMapType: Returns the type of the range (values).
valueType(SymbolicExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the SymbolicType of values, to which the given value set template refers.
vsArrayElementReference(ValueSetReference, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Given a value set reference to a (set-of) array(s) and an index (integer), returns a reference to the (set-of) elements of the (set-of) array(s) at that index
vsArrayElementReference(ValueSetReference, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given a value set reference to a (set-of) array(s) and an index (integer), returns a reference to the (set-of) elements of the (set-of) array(s) at that index
VSArrayElementReference - Interface in dev.civl.sarl.IF.expr.valueSetReference: A reference to an (set-of) element(s) of a (set-of) array value(s).
vsArraySectionReference(ValueSetReference, NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given a reference to a (set-of) array(s) and an inclusive lower index bound, an exclusive upper index bound and a DEFAULT step, which is one, of the range of the section, returns a reference to the (set-of) section(s) of the array(s) with the given bounds.
vsArraySectionReference(ValueSetReference, NumericExpression, NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Given a reference to a (set-of) array(s) and an inclusive lower index bound, an exclusive upper index bound and a step, returns a reference to the (set-of) section(s) of the array(s) with the given bounds.
vsArraySectionReference(ValueSetReference, NumericExpression, NumericExpression, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given a reference to a (set-of) array(s) and an inclusive lower index bound, an exclusive upper index bound and a step of the range of the section, returns a reference to the (set-of) section(s) of the array(s) with the given bounds.
VSArraySectionReference - Interface in dev.civl.sarl.IF.expr.valueSetReference: A reference to a (set-of) section(s) of a (set-of) array(s).
vsIdentityReference() - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Returns the identity (or "trivial") value set reference I.
vsIdentityReference() - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the identity (or "trivial") value set reference I.
VSIdentityReference - Interface in dev.civl.sarl.IF.expr.valueSetReference: A reference to a single object value.
vsOffsetReference(ValueSetReference, NumericExpression) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Given a reference to a (set-of) value(s) and a integral offset, returns a reference to a (set-of) value(s), which is obtained by applying the (set-of) offset(s) to the given (set-of) value(s).
vsOffsetReference(ValueSetReference, NumericExpression) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given a reference to a (set-of) value(s) and a integral offset, returns a reference to a (set-of) value(s), which is obtained by applying the (set-of) offset(s) to the given (set-of) value(s).
VSOffsetReference - Interface in dev.civl.sarl.IF.expr.valueSetReference: A reference to some point(s) which is specified by an integer "offset" from another value set reference.
vsTupleComponentReference(ValueSetReference, IntObject) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Given a reference to a (set-of) tuple(s), and a field index, returns a reference to that (set-of) component(s) of the tuple(s).
vsTupleComponentReference(ValueSetReference, IntObject) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given a reference to a (set-of) tuple(s), and a field index, returns a reference to that (set-of) component(s) of the tuple(s).
VSTupleComponentReference - Interface in dev.civl.sarl.IF.expr.valueSetReference: A reference into a (set-of) specified field(s) of a (set-of) tuple value(s).
vsUnionMemberReference(ValueSetReference, IntObject) - Method in interface dev.civl.sarl.expr.IF.ExpressionFactory: Given a reference to a (set-of) union(s) (expression of union type) and an index of a member type of that union, returns a reference to the (set-of) underlying element(s).
vsUnionMemberReference(ValueSetReference, IntObject) - Method in interface dev.civl.sarl.IF.CoreUniverse: Given a reference to a (set-of) union(s) (expression of union type) and an index of a member type of that union, returns a reference to the (set-of) underlying element(s).
VSUnionMemberReference - Interface in dev.civl.sarl.IF.expr.valueSetReference: A reference to a (set-of) members of a (set-of) union value(s).

W

workingDirectory() - Method in interface dev.civl.sarl.prove.IF.TheoremProverFactory: The directory that can be used for files generated by the theory provers created by this factory.
workingDirectory() - Method in interface dev.civl.sarl.reason.IF.ReasonerFactory: Returns the working directory for the theorem provers created by this factory.

Y

YES - Enum constant in enum class dev.civl.sarl.IF.ValidityResult.ResultType: Yes, the predicate is valid under the given context

Z

Z3 - Enum constant in enum class dev.civl.sarl.IF.config.ProverInfo.ProverKind: Microsoft's Z3, using SMT-LIB2 through Z3's command line interface.
zero(SymbolicType) - Method in interface dev.civl.sarl.ideal.IF.IdealFactory: Returns either the integer constant 0 or the real constant 0, according to the given type.
zeroInt() - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a symbolic expression of integer type with the value of 0
zeroInt() - Method in interface dev.civl.sarl.ideal.IF.IdealFactory
zeroInt() - Method in interface dev.civl.sarl.IF.CoreUniverse: The symbolic expression representing the 0 integer value.
zeroInteger() - Method in interface dev.civl.sarl.IF.number.NumberFactory: The integer number zero.
zeroIntegerObj() - Method in interface dev.civl.sarl.object.IF.ObjectFactory
zeroIntObj() - Method in interface dev.civl.sarl.object.IF.ObjectFactory
zeroRational() - Method in interface dev.civl.sarl.IF.number.NumberFactory: The rational number zero.
zeroReal() - Method in interface dev.civl.sarl.expr.IF.NumericExpressionFactory: Returns a symbolic expression of real type with the value of 0
zeroReal() - Method in interface dev.civl.sarl.ideal.IF.IdealFactory
zeroReal() - Method in interface dev.civl.sarl.IF.CoreUniverse: Returns the symbolic expression representing the real number 0.
zeroRealObj() - Method in interface dev.civl.sarl.object.IF.ObjectFactory

A B C D E F G H I J K L M N O P Q R S T U V W Y Z
All Classes and Interfaces|All Packages|Serialized Form