Uses of Interface
dev.civl.sarl.IF.expr.SymbolicExpression

Packages that use SymbolicExpression

Package	Description
dev.civl.sarl.expr.IF	This package provides the internal interface for the representation of basic symbolic expressions.
dev.civl.sarl.ideal.IF	The ideal module supports reasoning about numerical expressions using "ideal" mathematical reals and integers.
dev.civl.sarl.IF	This package and its subpackages provide the "public interface" to SARL.
dev.civl.sarl.IF.expr	The public interface package dealing with symbolic expressions.
dev.civl.sarl.IF.expr.valueSetReference
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	The type package provides interfaces for all of the symbolic types.
dev.civl.sarl.object.IF	Internal interface for the symbolic object module, providing mechanisms for creating SymbolicObjects.
dev.civl.sarl.preuniverse.IF	This package provides all of the functionality of a symbolic universe except reasoning.
dev.civl.sarl.prove.IF	Module "prove" constitutes the interface between SARL and (possibly external) theorem provers.
dev.civl.sarl.simplify.IF	Interfaces for the simplification of symbolic expressions.
dev.civl.sarl.type.IF	Internal interface for the "type" module, providing a SymbolicTypeFactory for producing SymbolicType s.

Uses of SymbolicExpression in dev.civl.sarl.expr.IF

Methods in dev.civl.sarl.expr.IF that return SymbolicExpression

Modifier and Type	Method	Description
SymbolicExpression	ExpressionFactory.expression(SymbolicExpression.SymbolicOperator operator, SymbolicType type, SymbolicObject... arguments)	Returns an expression with the given operator, type, and argument sequence.
SymbolicExpression	ExpressionFactory.nullExpression()	Returns the special expression "NULL", which has the NULL operator, null type, and no arguments.
SymbolicExpression	ExpressionFactory.valueSetDiff(SymbolicType valueType, SymbolicExpression refArr0, SymbolicExpression refArr1)
SymbolicExpression	ExpressionFactory.valueSetElimWidening(Reasoner reasoner, SymbolicType valueType, SymbolicExpression refArr, SymbolicExpression elimExpr, NumericExpression lower, NumericExpression upper)
SymbolicExpression	ExpressionFactory.valueSetProtectiveWidening(Reasoner reasoner, SymbolicType valueType, SymbolicExpression refArrM, SymbolicExpression refArrP)
SymbolicExpression	ExpressionFactory.valueSetTemplate(SymbolicType valueType, ValueSetReference[] vsRefs)	Given a symbolic type of a symbolic value and a list of ValueSetReferences, returns symbolic expression representing a value set template.
SymbolicExpression	ExpressionFactory.valueSetWidening(Reasoner reasoner, SymbolicType valueType, SymbolicExpression refArr)	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.

Methods in dev.civl.sarl.expr.IF that return types with arguments of type SymbolicExpression

Modifier and Type	Method	Description
Comparator<SymbolicExpression>	ExpressionFactory.comparator()	Returns a comparator on all SymbolicExpression objects.

Methods in dev.civl.sarl.expr.IF with parameters of type SymbolicExpression

Modifier and Type	Method	Description
BooleanExpression	ExpressionFactory.valueSetContains(SymbolicType valueType, SymbolicExpression refArr0, SymbolicExpression refArr1)	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.
SymbolicExpression	ExpressionFactory.valueSetDiff(SymbolicType valueType, SymbolicExpression refArr0, SymbolicExpression refArr1)
SymbolicExpression	ExpressionFactory.valueSetElimWidening(Reasoner reasoner, SymbolicType valueType, SymbolicExpression refArr, SymbolicExpression elimExpr, NumericExpression lower, NumericExpression upper)
SymbolicExpression	ExpressionFactory.valueSetProtectiveWidening(Reasoner reasoner, SymbolicType valueType, SymbolicExpression refArrM, SymbolicExpression refArrP)
SymbolicExpression	ExpressionFactory.valueSetWidening(Reasoner reasoner, SymbolicType valueType, SymbolicExpression refArr)	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.

Uses of SymbolicExpression in dev.civl.sarl.ideal.IF

Subinterfaces of SymbolicExpression in dev.civl.sarl.ideal.IF

Modifier and Type	Interface	Description
interface	Constant	A constant, i.e., a concrete number.
interface	Monic	A Monic is a product of powers of primitive expressions x1i 1*...*xnin, where the x i are primitives and the ij are positive concrete ints.
interface	Monomial	A Monomial is the product of a constant and a Monic.
interface	Polynomial	A polynomial: an expression which is the sum of monomials.
interface	Primitive	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.
interface	PrimitivePower	A power of a Primitive expression, xi, where x is a Primitive and i is a concrete positive int.
interface	RationalExpression	A RationalExpression is the quotient of two Monomials of real type.

Uses of SymbolicExpression in dev.civl.sarl.IF

Fields in dev.civl.sarl.IF declared as SymbolicExpression

Modifier and Type	Field	Description
SymbolicExpression	SARLBoundException.expr	The symbolic expression into which the index points (typically, an array)

Methods in dev.civl.sarl.IF with type parameters of type SymbolicExpression

Modifier and Type	Method	Description
<T extends SymbolicExpression> T	Reasoner.simplify(T expression)	Simplify the given expression under the context.
<T extends SymbolicExpression> T	Reasoner.simplify(T expression, Set<SymbolicConstant> aggressiveSet)

Methods in dev.civl.sarl.IF that return SymbolicExpression

Modifier and Type	Method	Description
SymbolicExpression	CoreUniverse.append(SymbolicExpression concreteArray, SymbolicExpression element)	Appends an element to the end of a concrete symbolic array.
SymbolicExpression	CoreUniverse.apply(SymbolicExpression function, Iterable<? extends SymbolicExpression> argumentSequence)	The result of applying an uninterpreted function to a sequence of arguments.
SymbolicExpression	CoreUniverse.array(SymbolicType elementType, SymbolicExpression[] elements)	Creates a concrete array expression backed by the given Java array.
SymbolicExpression	CoreUniverse.array(SymbolicType elementType, Iterable<? extends SymbolicObject> elements)	Returns the concrete array consisting of given sequence of elements.
SymbolicExpression	CoreUniverse.arrayLambda(SymbolicCompleteArrayType arrayType, SymbolicExpression function)	Returns an expression representing an array with element type T defined by a function f from int to T.
SymbolicExpression	CoreUniverse.arrayRead(SymbolicExpression array, NumericExpression index)	Returns an expression representing the value of the element of the array at position index.
SymbolicExpression	CoreUniverse.arrayWrite(SymbolicExpression array, NumericExpression index, SymbolicExpression value)	Returns an expression representing the result of modifying an array by changing the value at position index.
SymbolicExpression	CoreUniverse.assign(SymbolicExpression value, ReferenceExpression reference, SymbolicExpression subValue)	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.
SymbolicExpression	CoreUniverse.cast(SymbolicType newType, SymbolicExpression expression)	Casts expression to new type.
SymbolicExpression	CoreUniverse.character(char theChar)	Returns a concrete symbolic expression of character type which wraps the given Java char.
SymbolicExpression	CoreUniverse.concreteValueOfUninterpretedType(SymbolicUninterpretedType type, IntObject key)	Returns a symbolic expression of a SymbolicUninterpretedType.
SymbolicExpression	CoreUniverse.cond(BooleanExpression predicate, SymbolicExpression trueCase, SymbolicExpression falseCase)	"If-then-else" expression.
SymbolicExpression	CoreUniverse.constantArray(SymbolicType elementType, NumericExpression length, SymbolicExpression value)	Returns an array in which every element has the same value.
SymbolicExpression	CoreUniverse.denseArrayWrite(SymbolicExpression array, Iterable<? extends SymbolicExpression> values)	Returns an array obtained by performing a sequence of writes, given in a "dense" format, to an array.
SymbolicExpression	CoreUniverse.dereference(SymbolicExpression value, ReferenceExpression reference)	Given a reference and a value, returns the sub-expression of value specified by the reference.
SymbolicExpression	CoreUniverse.derivative(SymbolicExpression function, IntObject index, IntObject degree)	Returns the function which is the degree-th derivative of function with respect to the index-th parameter.
SymbolicExpression	CoreUniverse.emptyArray(SymbolicType elementType)	Returns array of length 0.
SymbolicExpression	CoreUniverse.emptyMap(SymbolicMapType mapType)
SymbolicExpression	CoreUniverse.entrySet(SymbolicExpression map)	Returns the entry set of the map.
SymbolicExpression	CoreUniverse.fullySubstitute(Map<SymbolicExpression,SymbolicExpression> substituteMap, SymbolicExpression expression)	Substitute the given SymbolicExpression expression by repeatedly applying the method invalid reference #apply(SymbolicExpression) until no more substitution can happen.
SymbolicExpression	CoreUniverse.get(SymbolicExpression map, SymbolicExpression key)
SymbolicExpression	CoreUniverse.insertElementAt(SymbolicExpression concreteArray, int index, SymbolicExpression value)	Inserts value an position index in array, shifting subsequence elements "up".
SymbolicExpression	CoreUniverse.integer2Bitvector(NumericExpression integer, SymbolicCompleteArrayType bitVectorType)	Returns the conversion of a bit vector from an integer.
SymbolicExpression	CoreUniverse.keySet(SymbolicExpression map)
SymbolicExpression	CoreUniverse.lambda(SymbolicConstant boundVariable, SymbolicExpression expression)	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.
SymbolicExpression	CoreUniverse.make(SymbolicExpression.SymbolicOperator operator, SymbolicType type, SymbolicObject[] arguments)	Applies the given operator to the arguments and returns the resulting expression in the form used by this universe.
SymbolicExpression	CoreUniverse.nullExpression()	Returns the "NULL" expression.
SymbolicExpression	CoreUniverse.put(SymbolicExpression map, SymbolicExpression key, SymbolicExpression value)
SymbolicExpression	CoreUniverse.reduction(SymbolicExpression[] operands, NumericExpression count, SymbolicExpression op, List<BooleanExpression> compatibleConditionsOutput)	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.
SymbolicExpression	CoreUniverse.removeElementAt(SymbolicExpression concreteArray, int index)	Removes an element in a specified position in a concrete symbolic array.
SymbolicExpression	CoreUniverse.removeEntryWithKey(SymbolicExpression map, SymbolicExpression key)
SymbolicExpression	CoreUniverse.setAdd(SymbolicExpression set, SymbolicExpression value)
SymbolicExpression	CoreUniverse.setDifference(SymbolicExpression set1, SymbolicExpression set2)
SymbolicExpression	CoreUniverse.setIntersection(SymbolicExpression set1, SymbolicExpression set2)
SymbolicExpression	CoreUniverse.setRemove(SymbolicExpression set, SymbolicExpression value)
SymbolicExpression	CoreUniverse.setUnion(SymbolicExpression set1, SymbolicExpression set2)
SymbolicExpression	CoreUniverse.stringExpression(String theString)	Returns a symbolic expression of type array-of-char which is a literal array consisting of the sequence of characters in the given string.
SymbolicExpression	CoreUniverse.tuple(SymbolicTupleType type, SymbolicExpression[] components)	Returns the concrete tuple with the given members.
SymbolicExpression	CoreUniverse.tuple(SymbolicTupleType type, Iterable<? extends SymbolicObject> components)	Returns the concrete tuple expression with the given tuple components.
SymbolicExpression	CoreUniverse.tupleRead(SymbolicExpression tuple, IntObject index)	Returns an expression that represents the result of reading a component in a tuple value.
SymbolicExpression	CoreUniverse.tupleWrite(SymbolicExpression tuple, IntObject index, SymbolicExpression value)	Returns an expression representing the result of modifying a tuple by changing the value of one component.
SymbolicExpression	CoreUniverse.unionExtract(IntObject memberIndex, SymbolicExpression object)	Casts an object whose type is a union type to a representation whose type is the appropriate member type of the union type.
SymbolicExpression	CoreUniverse.unionInject(SymbolicUnionType unionType, IntObject memberIndex, SymbolicExpression object)	Casts an object belonging to one of the members of a union type to the union type.
SymbolicExpression	CoreUniverse.valueSetAssigns(SymbolicExpression oldValue, SymbolicExpression valueSetTemplate, SymbolicExpression newValue)	Copies a subset of a value v to another value v' with a given value set template.
SymbolicExpression	CoreUniverse.valueSetDiff(SymbolicExpression vst0, SymbolicExpression vst1)	Given two value set templates, returns their set difference.
SymbolicExpression	SymbolicUniverse.valueSetElimWidening(BooleanExpression context, SymbolicExpression vst, SymbolicExpression elimExpr, SymbolicExpression lower, SymbolicExpression upper)
SymbolicExpression	SymbolicUniverse.valueSetProtectiveWidening(BooleanExpression context, SymbolicExpression vstM, SymbolicExpression vstP)
SymbolicExpression	CoreUniverse.valueSetTemplate(SymbolicType valueType, ValueSetReference[] vsRefs)	Given a symbolic type of a symbolic value and a list of ValueSetReferences, returns symbolic expression representing a value set template.
SymbolicExpression	CoreUniverse.valueSetUnion(SymbolicExpression vst0, SymbolicExpression vst1)	Given two value set templates, returns the union of the two.
SymbolicExpression	SymbolicUniverse.valueSetWidening(BooleanExpression context, SymbolicExpression vst)	Apply a default widening operator to the value set references in the given value set template.

Methods in dev.civl.sarl.IF that return types with arguments of type SymbolicExpression

Modifier and Type	Method	Description
UnaryOperator<SymbolicExpression>	CoreUniverse.constantSubstituter(Map<SymbolicConstant,SymbolicExpression> map)	Returns a substituter for which the base substitutions are specified by an explicit Java Map.
Map<SymbolicConstant,SymbolicExpression>	Reasoner.constantSubstitutionMap()	In the process of simplifying the initial context, this simplifier may have "solved" for some of the symbolic constants occurring in the context.
Map<SymbolicConstant,SymbolicExpression>	ModelResult.getModel()	Returns the model, a map assigning a concrete symbolic expression value to each symbolic constant occurring in the query.
UnaryOperator<SymbolicExpression>	CoreUniverse.mapSubstituter(UnaryOperator<SymbolicExpression> operator)
UnaryOperator<SymbolicExpression>	CoreUniverse.mapSubstituter(Map<SymbolicExpression,SymbolicExpression> map)	Returns a substituter for which the base substitutions are specified by an explicit Java Map.
UnaryOperator<SymbolicExpression>	CoreUniverse.nameSubstituter(Map<StringObject,StringObject> nameMap)	Returns a substituter specified by a mapping of old names to new names for symbolic constants.
UnaryOperator<SymbolicExpression>	CoreUniverse.simpleSubstituter(SymbolicConstant var, SymbolicExpression value)	Returns a substituter that replaces a specific symbolic constant with some specific value.
dev.civl.sarl.util.Pair<SymbolicExpression,Integer>	CoreUniverse.valueSetHavoc(SymbolicExpression value, SymbolicExpression valueSetTemplate, String prefix, int startCount)

Methods in dev.civl.sarl.IF with parameters of type SymbolicExpression

Modifier and Type	Method	Description
SymbolicExpression	CoreUniverse.append(SymbolicExpression concreteArray, SymbolicExpression element)	Appends an element to the end of a concrete symbolic array.
SymbolicExpression	CoreUniverse.apply(SymbolicExpression function, Iterable<? extends SymbolicExpression> argumentSequence)	The result of applying an uninterpreted function to a sequence of arguments.
SymbolicExpression	CoreUniverse.array(SymbolicType elementType, SymbolicExpression[] elements)	Creates a concrete array expression backed by the given Java array.
SymbolicExpression	CoreUniverse.arrayLambda(SymbolicCompleteArrayType arrayType, SymbolicExpression function)	Returns an expression representing an array with element type T defined by a function f from int to T.
SymbolicExpression	CoreUniverse.arrayRead(SymbolicExpression array, NumericExpression index)	Returns an expression representing the value of the element of the array at position index.
SymbolicExpression	CoreUniverse.arrayWrite(SymbolicExpression array, NumericExpression index, SymbolicExpression value)	Returns an expression representing the result of modifying an array by changing the value at position index.
SymbolicExpression	CoreUniverse.assign(SymbolicExpression value, ReferenceExpression reference, SymbolicExpression subValue)	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.
NumericExpression	CoreUniverse.bitvector2Integer(SymbolicExpression bitvector)	Converts a bit vector to an integer.
NumericExpression	CoreUniverse.cardinality(SymbolicExpression set)
SymbolicExpression	CoreUniverse.cast(SymbolicType newType, SymbolicExpression expression)	Casts expression to new type.
SymbolicExpression	CoreUniverse.cond(BooleanExpression predicate, SymbolicExpression trueCase, SymbolicExpression falseCase)	"If-then-else" expression.
SymbolicExpression	CoreUniverse.constantArray(SymbolicType elementType, NumericExpression length, SymbolicExpression value)	Returns an array in which every element has the same value.
SymbolicExpression	CoreUniverse.denseArrayWrite(SymbolicExpression array, Iterable<? extends SymbolicExpression> values)	Returns an array obtained by performing a sequence of writes, given in a "dense" format, to an array.
SymbolicExpression	CoreUniverse.dereference(SymbolicExpression value, ReferenceExpression reference)	Given a reference and a value, returns the sub-expression of value specified by the reference.
SymbolicExpression	CoreUniverse.derivative(SymbolicExpression function, IntObject index, IntObject degree)	Returns the function which is the degree-th derivative of function with respect to the index-th parameter.
BooleanExpression	CoreUniverse.differentiable(SymbolicExpression function, IntObject degree, Iterable<? extends NumericExpression> lowerBounds, Iterable<? extends NumericExpression> upperBounds)	Returns an expression of boolean type which encodes the claim that a function is differentiable on a closed interval in R^n.
SymbolicExpression	CoreUniverse.entrySet(SymbolicExpression map)	Returns the entry set of the map.
BooleanExpression	CoreUniverse.equals(SymbolicExpression arg0, SymbolicExpression arg1)	Returns expression equivalent to arg0 = arg1 ("equals").
Character	CoreUniverse.extractCharacter(SymbolicExpression expression)	If the given expression is a concrete character expression, this returns the character value, else it returns null.
SymbolicExpression	CoreUniverse.fullySubstitute(Map<SymbolicExpression,SymbolicExpression> substituteMap, SymbolicExpression expression)	Substitute the given SymbolicExpression expression by repeatedly applying the method invalid reference #apply(SymbolicExpression) until no more substitution can happen.
SymbolicExpression	CoreUniverse.get(SymbolicExpression map, SymbolicExpression key)
Set<SymbolicConstant>	CoreUniverse.getFreeSymbolicConstants(SymbolicExpression expr)	Returns the set of unbound symbolic constants occurring in an expression.
SymbolicExpression	CoreUniverse.insertElementAt(SymbolicExpression concreteArray, int index, SymbolicExpression value)	Inserts value an position index in array, shifting subsequence elements "up".
boolean	CoreUniverse.isPermutCall(SymbolicExpression expr)
boolean	CoreUniverse.isSigmaCall(SymbolicExpression expr)
BooleanExpression	CoreUniverse.isSubsetOf(SymbolicExpression set1, SymbolicExpression set2)
SymbolicExpression	CoreUniverse.keySet(SymbolicExpression map)
SymbolicExpression	CoreUniverse.lambda(SymbolicConstant boundVariable, SymbolicExpression expression)	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.
NumericExpression	CoreUniverse.length(SymbolicExpression array)	Returns the length of any symbolic expression of array type.
NumericExpression	CoreUniverse.mapSize(SymbolicExpression map)
BooleanExpression	CoreUniverse.neq(SymbolicExpression arg0, SymbolicExpression arg1)	Returns expression equivalent to arg0 != arg1 ("not equals").
BooleanExpression	CoreUniverse.permut(SymbolicExpression array_a, SymbolicExpression array_b, NumericExpression low, NumericExpression high)	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.
void	CoreUniverse.printCompressed(SymbolicExpression expr, PrintStream out)	Prints the expression by preceding with a sequence of definitions of sub-expressions which are used more than once.
void	CoreUniverse.printCompressedTree(String prefix, SymbolicExpression expr, PrintStream out)	Use this method to print large symbolic expression hierarchically.
void	CoreUniverse.printExprTree(SymbolicExpression expr, PrintStream out)	print symbolic expression as tree structure
SymbolicExpression	CoreUniverse.put(SymbolicExpression map, SymbolicExpression key, SymbolicExpression value)
BooleanExpression	CoreUniverse.quickEquals(SymbolicExpression arg0, SymbolicExpression arg1)
SymbolicExpression	CoreUniverse.reduction(SymbolicExpression[] operands, NumericExpression count, SymbolicExpression op, List<BooleanExpression> compatibleConditionsOutput)	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.
SymbolicExpression	CoreUniverse.removeElementAt(SymbolicExpression concreteArray, int index)	Removes an element in a specified position in a concrete symbolic array.
SymbolicExpression	CoreUniverse.removeEntryWithKey(SymbolicExpression map, SymbolicExpression key)
SymbolicExpression	CoreUniverse.setAdd(SymbolicExpression set, SymbolicExpression value)
SymbolicExpression	CoreUniverse.setDifference(SymbolicExpression set1, SymbolicExpression set2)
SymbolicExpression	CoreUniverse.setIntersection(SymbolicExpression set1, SymbolicExpression set2)
SymbolicExpression	CoreUniverse.setRemove(SymbolicExpression set, SymbolicExpression value)
SymbolicExpression	CoreUniverse.setUnion(SymbolicExpression set1, SymbolicExpression set2)
NumericExpression	CoreUniverse.sigma(NumericExpression low, NumericExpression high, SymbolicExpression function)	A fold sum expression.
UnaryOperator<SymbolicExpression>	CoreUniverse.simpleSubstituter(SymbolicConstant var, SymbolicExpression value)	Returns a substituter that replaces a specific symbolic constant with some specific value.
SymbolicExpression	CoreUniverse.tuple(SymbolicTupleType type, SymbolicExpression[] components)	Returns the concrete tuple with the given members.
SymbolicExpression	CoreUniverse.tupleRead(SymbolicExpression tuple, IntObject index)	Returns an expression that represents the result of reading a component in a tuple value.
SymbolicExpression	CoreUniverse.tupleWrite(SymbolicExpression tuple, IntObject index, SymbolicExpression value)	Returns an expression representing the result of modifying a tuple by changing the value of one component.
SymbolicExpression	CoreUniverse.unionExtract(IntObject memberIndex, SymbolicExpression object)	Casts an object whose type is a union type to a representation whose type is the appropriate member type of the union type.
SymbolicExpression	CoreUniverse.unionInject(SymbolicUnionType unionType, IntObject memberIndex, SymbolicExpression object)	Casts an object belonging to one of the members of a union type to the union type.
BooleanExpression	CoreUniverse.unionTest(IntObject memberIndex, SymbolicExpression object)	Tests whether an object of a union type is in the image of injection from the member type of the given index.
SymbolicExpression	CoreUniverse.valueSetAssigns(SymbolicExpression oldValue, SymbolicExpression valueSetTemplate, SymbolicExpression newValue)	Copies a subset of a value v to another value v' with a given value set template.
BooleanExpression	CoreUniverse.valueSetContains(SymbolicExpression vst0, SymbolicExpression vst1)	Test if a value set template vst0 contains another value set template vst1.
SymbolicExpression	CoreUniverse.valueSetDiff(SymbolicExpression vst0, SymbolicExpression vst1)	Given two value set templates, returns their set difference.
SymbolicExpression	SymbolicUniverse.valueSetElimWidening(BooleanExpression context, SymbolicExpression vst, SymbolicExpression elimExpr, SymbolicExpression lower, SymbolicExpression upper)
dev.civl.sarl.util.Pair<SymbolicExpression,Integer>	CoreUniverse.valueSetHavoc(SymbolicExpression value, SymbolicExpression valueSetTemplate, String prefix, int startCount)
BooleanExpression	CoreUniverse.valueSetNoIntersect(SymbolicExpression vst0, SymbolicExpression vst1)	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.
SymbolicExpression	SymbolicUniverse.valueSetProtectiveWidening(BooleanExpression context, SymbolicExpression vstM, SymbolicExpression vstP)
Iterable<ValueSetReference>	CoreUniverse.valueSetReferences(SymbolicExpression valueSetTemplate)	Returns the set of ValueSetReferences in the given value set template.
SymbolicExpression	CoreUniverse.valueSetUnion(SymbolicExpression vst0, SymbolicExpression vst1)	Given two value set templates, returns the union of the two.
SymbolicExpression	SymbolicUniverse.valueSetWidening(BooleanExpression context, SymbolicExpression vst)	Apply a default widening operator to the value set references in the given value set template.
SymbolicType	CoreUniverse.valueType(SymbolicExpression valueSetTemplate)	Returns the SymbolicType of values, to which the given value set template refers.

Method parameters in dev.civl.sarl.IF with type arguments of type SymbolicExpression

Modifier and Type	Method	Description
SymbolicExpression	CoreUniverse.apply(SymbolicExpression function, Iterable<? extends SymbolicExpression> argumentSequence)	The result of applying an uninterpreted function to a sequence of arguments.
UnaryOperator<SymbolicExpression>	CoreUniverse.constantSubstituter(Map<SymbolicConstant,SymbolicExpression> map)	Returns a substituter for which the base substitutions are specified by an explicit Java Map.
SymbolicExpression	CoreUniverse.denseArrayWrite(SymbolicExpression array, Iterable<? extends SymbolicExpression> values)	Returns an array obtained by performing a sequence of writes, given in a "dense" format, to an array.
SymbolicExpression	CoreUniverse.fullySubstitute(Map<SymbolicExpression,SymbolicExpression> substituteMap, SymbolicExpression expression)	Substitute the given SymbolicExpression expression by repeatedly applying the method invalid reference #apply(SymbolicExpression) until no more substitution can happen.
SymbolicExpression	CoreUniverse.fullySubstitute(Map<SymbolicExpression,SymbolicExpression> substituteMap, SymbolicExpression expression)	Substitute the given SymbolicExpression expression by repeatedly applying the method invalid reference #apply(SymbolicExpression) until no more substitution can happen.
UnaryOperator<SymbolicExpression>	CoreUniverse.mapSubstituter(UnaryOperator<SymbolicExpression> operator)
UnaryOperator<SymbolicExpression>	CoreUniverse.mapSubstituter(Map<SymbolicExpression,SymbolicExpression> map)	Returns a substituter for which the base substitutions are specified by an explicit Java Map.
UnaryOperator<SymbolicExpression>	CoreUniverse.mapSubstituter(Map<SymbolicExpression,SymbolicExpression> map)	Returns a substituter for which the base substitutions are specified by an explicit Java Map.

Constructors in dev.civl.sarl.IF with parameters of type SymbolicExpression

Modifier	Constructor	Description
	SARLBoundException(SymbolicExpression expr, NumericExpression index, NumericExpression lowerBound, NumericExpression upperBound, String location)	Constructs new out-of-bounds exception with a message formed from the given parameters.

Uses of SymbolicExpression in dev.civl.sarl.IF.expr

Subinterfaces of SymbolicExpression in dev.civl.sarl.IF.expr

Modifier and Type	Interface	Description
interface	ArrayElementReference	A reference to an element of an array.
interface	BooleanExpression	A symbolic expression of boolean type.
interface	BooleanSymbolicConstant	A SymbolicConstant of boolean type.
interface	NTReferenceExpression	A non-trivial ReferenceExpression, i.e., one which is not the null reference or the identity reference.
interface	NumericExpression	Marker interface for an expression of numeric type ( SymbolicIntegerType SymbolicRealType).
interface	NumericSymbolicConstant	A SymbolicConstant which has integer or real type, i.e., type belonging to SymbolicIntegerType or SymbolicRealType.
interface	OffsetReference	A reference to some point which is specified by an integer "offset" from another reference.
interface	ReferenceExpression	An expression representing a way to reference into values.
interface	SymbolicConstant	A "symbolic constant" is a symbol used in symbolic execution to represent an input value.
interface	TupleComponentReference	A reference into a specified field of a tuple value.
interface	UnionMemberReference	A reference to a member of a SymbolicUnionType.

Uses of SymbolicExpression in dev.civl.sarl.IF.expr.valueSetReference

Subinterfaces of SymbolicExpression in dev.civl.sarl.IF.expr.valueSetReference

Modifier and Type	Interface	Description
interface	NTValueSetReference	A non-trivial ValueSetReference, i.e., one which is not the identity reference.
interface	ValueSetReference
interface	VSArrayElementReference	A reference to an (set-of) element(s) of a (set-of) array value(s).
interface	VSArraySectionReference	A reference to a (set-of) section(s) of a (set-of) array(s).
interface	VSIdentityReference	A reference to a single object value.
interface	VSOffsetReference	A reference to some point(s) which is specified by an integer "offset" from another value set reference.
interface	VSTupleComponentReference	A reference into a (set-of) specified field(s) of a (set-of) tuple value(s).
interface	VSUnionMemberReference	A reference to a (set-of) members of a (set-of) union value(s).

Uses of SymbolicExpression in dev.civl.sarl.IF.object

Classes in dev.civl.sarl.IF.object with type parameters of type SymbolicExpression

Modifier and Type	Interface	Description
interface	SymbolicSequence<T extends SymbolicExpression>	A finite ordered immutable sequence of symbolic expressions.

Methods in dev.civl.sarl.IF.object with type parameters of type SymbolicExpression

Modifier and Type	Method	Description
<U extends SymbolicExpression> SymbolicSequence<U>	SymbolicSequence.apply(Transform<T,U> transform)	Returns a sequence obtained by applying a function to every element of this sequence; also known as "map".

Uses of SymbolicExpression in dev.civl.sarl.IF.type

Methods in dev.civl.sarl.IF.type that return types with arguments of type SymbolicExpression

Modifier and Type	Method	Description
Function<SymbolicExpression,IntObject>	SymbolicUninterpretedType.soleSelector()

Uses of SymbolicExpression in dev.civl.sarl.object.IF

Methods in dev.civl.sarl.object.IF with type parameters of type SymbolicExpression

Modifier and Type	Method	Description
<T extends SymbolicExpression> SymbolicSequence<T>	ObjectFactory.emptySequence()	Returns the empty sequence.
<T extends SymbolicExpression> SymbolicSequence<T>	ObjectFactory.sequence(Iterable<? extends T> elements)	Returns a SymbolicSequence comprising the given sequence of elements.
<T extends SymbolicExpression> SymbolicSequence<T>	ObjectFactory.sequence(T[] elements)	Returns a SymbolicSequence comprising the sequence of elements specified as an array.
<T extends SymbolicExpression> SymbolicSequence<T>	ObjectFactory.singletonSequence(T element)	Returns the sequence of length 1 consisting of the given element.

Methods in dev.civl.sarl.object.IF with parameters of type SymbolicExpression

Modifier and Type	Method	Description
<T extends SymbolicExpression> SymbolicSequence<T>	ObjectFactory.sequence(T[] elements)	Returns a SymbolicSequence comprising the sequence of elements specified as an array.

Method parameters in dev.civl.sarl.object.IF with type arguments of type SymbolicExpression

Modifier and Type	Method	Description
void	ObjectFactory.setExpressionComparator(Comparator<SymbolicExpression> c)	Sets the expression comparator for this object factory.

Uses of SymbolicExpression in dev.civl.sarl.preuniverse.IF

Methods in dev.civl.sarl.preuniverse.IF that return SymbolicExpression

Modifier and Type	Method	Description
SymbolicExpression	PreUniverse.cleanBoundVariables(SymbolicExpression expr)	Changes the names of the bound variables in the expression so that every bound variable has a unique name.

Methods in dev.civl.sarl.preuniverse.IF that return types with arguments of type SymbolicExpression

Modifier and Type	Method	Description
UnaryOperator<SymbolicExpression>	PreUniverse.cloneBoundCleaner(UnaryOperator<SymbolicExpression> boundCleaner)
UnaryOperator<SymbolicExpression>	PreUniverse.newMinimalBoundCleaner()	Produces a new object for renaming bound variables in a minimal way.

Methods in dev.civl.sarl.preuniverse.IF with parameters of type SymbolicExpression

Modifier and Type	Method	Description
SymbolicExpression	PreUniverse.cleanBoundVariables(SymbolicExpression expr)	Changes the names of the bound variables in the expression so that every bound variable has a unique name.

Method parameters in dev.civl.sarl.preuniverse.IF with type arguments of type SymbolicExpression

Modifier and Type	Method	Description
UnaryOperator<SymbolicExpression>	PreUniverse.cloneBoundCleaner(UnaryOperator<SymbolicExpression> boundCleaner)

Uses of SymbolicExpression in dev.civl.sarl.prove.IF

Fields in dev.civl.sarl.prove.IF declared as SymbolicExpression

Modifier and Type	Field	Description
final SymbolicExpression	ProverFunctionInterpretation.definition

Methods in dev.civl.sarl.prove.IF with parameters of type SymbolicExpression

Modifier and Type	Method	Description
static ProverFunctionInterpretation	ProverFunctionInterpretation.newProverPredicate(SymbolicUniverse universe, String identifier, SymbolicConstant[] parameters, SymbolicExpression definition)

Method parameters in dev.civl.sarl.prove.IF with type arguments of type SymbolicExpression

Modifier and Type	Method	Description
static ModelResult	Prove.modelResult(Map<SymbolicConstant,SymbolicExpression> model)	Constructs a new ModelResult wrapping the given mapping from symbolic constants to symbolic expressions.

Uses of SymbolicExpression in dev.civl.sarl.simplify.IF

Methods in dev.civl.sarl.simplify.IF with parameters of type SymbolicExpression

Modifier and Type	Method	Description
List<BooleanExpression>	ContextPartition.minimizeFor(SymbolicExpression expr, PreUniverse universe)	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.

Uses of SymbolicExpression in dev.civl.sarl.type.IF

Method parameters in dev.civl.sarl.type.IF with type arguments of type SymbolicExpression

Modifier and Type	Method	Description
void	SymbolicTypeFactory.setExpressionComparator(Comparator<SymbolicExpression> c)	setting the way you want to comparator to compare two expressions used when comparing CompleteArrayType