Module dev.civl.sarl

Package dev.civl.sarl.IF.expr

Enum Class SymbolicExpression.SymbolicOperator

java.lang.Object

java.lang.Enum<SymbolicExpression.SymbolicOperator>

dev.civl.sarl.IF.expr.SymbolicExpression.SymbolicOperator

All Implemented Interfaces:

Serializable, Comparable<SymbolicExpression.SymbolicOperator>, Constable

Enclosing interface:

SymbolicExpression

public static enum SymbolicExpression.SymbolicOperator
extends Enum<SymbolicExpression.SymbolicOperator>

An enumerated type for the different kinds of symbolic expressions.

Nested Class Summary

Nested classes/interfaces inherited from class java.lang.Enum

Enum.EnumDesc<E extends Enum<E>>

Enum Constant Summary

Enum Constants

Enum Constant	Description
ADD	Operator for an expression representing the sum of its arguments.
AND	Operator for an expression representing the conjunction of symbolic expressions of boolean type.
APPLY	Operator for an expression representing the application of a function to some arguments.
ARRAY	A concrete array.
ARRAY_LAMBDA	Operator for an array expression of type T[] formed by providing a function f from integers to T.
ARRAY_READ	Operator for an expression representing the result of reading an element from an array.
ARRAY_WRITE	Operator for an expression representing the array resulting from modifying a single element of an array.
BIT_AND	Operator for an expression representing the result of applying bit-wise and operation on two given unsigned integers.
BIT_NOT	Operator for an expression representing the result of applying bit-wise not operation on the given unsigned integers.
BIT_OR	Operator for an expression representing the result of applying bit-wise or operation on two given unsigned integers.
BIT_SHIFT_LEFT	Operator for an expression representing the result of applying bit-wise left shifting operation on two given values.
BIT_SHIFT_RIGHT	Operator for an expression representing the result of applying bit-wise right shifting operation on two given values.
BIT_XOR	Operator for an expression representing the result of applying bit-wise exclusive-or operation on two given unsigned integers.
CAST	Operator for an expression representing the result of converting a value from one type to another.
CONCRETE	TODO: this will go away in the refactoring.
COND	Operator for a conditional expression, also known as "if-then-else", as in C's ternary expression arg0 ? arg1 : arg2.
DENSE_ARRAY_WRITE	Operator for expression that represents the result of multiple writes to distinct concrete positions in an array.
DENSE_TUPLE_WRITE	Operator representing the result of multiple writes to different components of a tuple.
DERIV	The (partial) derivative operator.
DIFFERENTIABLE	A predicate which declares a real-valued function to have some number of continuous derivatives over a bounded, rectangular, closed interval in R^n.
DIVIDE	Operator for real number division.
EQUALS	Operator for comparison of two values for equality.
EXISTS	Operator for for existential quantification: ∃ x .
FORALL	Operator for for universal quantification: ∀ x .
INT_DIVIDE	Operator for integer division.
LAMBDA	Operator for a lambda expression, as in the lambda calculus: λ x .
LENGTH	Operator for getting the length of an array.
LESS_THAN	Operator for a less-than expression: x < y.
LESS_THAN_EQUALS	Operator for a less-than-or-equals expression: x ≤ y .
MODULO	The integer modulus operator.
MULTIPLY	Operator for an expression representing the numerical product of symbolic expressions.
NEGATIVE	Operator for numerical negation, i.e., - x.
NEQ	Operator for comparison of two values for inequality.
NOT	Operator for logical negation ("not").
NULL	Operator used to represent no symbolic expression in cases where Java's null is not acceptable.
OR	Operator for an expression representing the disjunction of symbolic expressions of boolean type.
POWER	Operator for exponentiation, i.e., the raising of some number to some power: x y.
SUBTRACT	Operator for numerical subtraction: x − y.
SYMBOLIC_CONSTANT	Operator used to represent a symbolic constant.
TUPLE	A concrete tuple.
TUPLE_READ	Operator for an expression representing the result of reading a component of a tuple.
TUPLE_WRITE	Operator for an expression representing the result of modifying a single component of a tuple.
UNION_EXTRACT	Operator for extracting an element of a SymbolicUnionType to an element of a member type.
UNION_INJECT	Operator for injecting an element of a member type into a SymbolicUnionType that includes that member type.
UNION_TEST	Operator to determine whether an expression in a SymbolicUnionType is in the image of injection from a specified member type.

Method Summary

Modifier and Type	Method	Description
static SymbolicExpression.SymbolicOperator	valueOf(String name)	Returns the enum constant of this class with the specified name.
static SymbolicExpression.SymbolicOperator[]	values()	Returns an array containing the constants of this enum class, in the order they are declared.

Methods inherited from class java.lang.Enum

compareTo, describeConstable, equals, getDeclaringClass, hashCode, name, ordinal, toString, valueOf

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Enum Constant Details

ADD

public static final SymbolicExpression.SymbolicOperator ADD

Operator for an expression representing the sum of its arguments. The arguments and the expression are all instances of NumericExpression. The arguments must all have the same numeric (integer or real) type, which is also the type of the expression. There can be any number of arguments (including 0). The sum with 0 arguments is equivalent to the 0 of the type of the expression.

AND

public static final SymbolicExpression.SymbolicOperator AND

Operator for an expression representing the conjunction of symbolic expressions of boolean type. The arguments and the expression are all instances of BooleanExpression. The arguments and the expression itself all have boolean type. There can be any number of arguments (including 0). The conjunction with 0 arguments is equivalent to the "true" expression.

See Also:

• OR
• NOT

APPLY

public static final SymbolicExpression.SymbolicOperator APPLY

Operator for an expression representing the application of a function to some arguments. Takes 2 arguments. Arg0 is a SymbolicExpression of SymbolicFunctionType. Arg1 is an Iterable<? extends SymbolicExpression> containing the ordered sequence of arguments to the function.

ARRAY

public static final SymbolicExpression.SymbolicOperator ARRAY

A concrete array. The arguments are the elements of the array.

ARRAY_LAMBDA

public static final SymbolicExpression.SymbolicOperator ARRAY_LAMBDA

Operator for an array expression of type T[] formed by providing a function f from integers to T. Has one argument: a symbolic expression f of SymbolicFunctionType. Note that the length of the array may (or may not) be specified in the type of the resulting expression.

ARRAY_READ

public static final SymbolicExpression.SymbolicOperator ARRAY_READ

Operator for an expression representing the result of reading an element from an array. 2 arguments. Arg0 is the array expression (a symbolic expression of SymbolicArrayType), Arg1 is the index expression (a SymbolicExpression of integer type).

See Also:

• ARRAY_WRITE

ARRAY_WRITE

public static final SymbolicExpression.SymbolicOperator ARRAY_WRITE

Operator for an expression representing the array resulting from modifying a single element of an array. 3 Arguments. Arg0 is the original array expression, arg1 is the index expression, arg2 is the new value being assigned to that position in the array.

See Also:

• ARRAY_READ

BIT_AND

public static final SymbolicExpression.SymbolicOperator BIT_AND

Operator for an expression representing the result of applying bit-wise and operation on two given unsigned integers. 2 arguments: Both Arg0 and Arg1 are unsigned integers.

BIT_NOT

public static final SymbolicExpression.SymbolicOperator BIT_NOT

Operator for an expression representing the result of applying bit-wise not operation on the given unsigned integers. a arguments: Arg0 is an unsigned integer.

BIT_OR

public static final SymbolicExpression.SymbolicOperator BIT_OR

Operator for an expression representing the result of applying bit-wise or operation on two given unsigned integers. 2 arguments: Both Arg0 and Arg1 are unsigned integers.

BIT_XOR

public static final SymbolicExpression.SymbolicOperator BIT_XOR

Operator for an expression representing the result of applying bit-wise exclusive-or operation on two given unsigned integers. 2 arguments: Both Arg0 and Arg1 are unsigned integers.

BIT_SHIFT_LEFT

public static final SymbolicExpression.SymbolicOperator BIT_SHIFT_LEFT

Operator for an expression representing the result of applying bit-wise left shifting operation on two given values. 2 arguments: Both Arg0 and Arg1 are integers or unsigned integers.

BIT_SHIFT_RIGHT

public static final SymbolicExpression.SymbolicOperator BIT_SHIFT_RIGHT

Operator for an expression representing the result of applying bit-wise right shifting operation on two given values. 2 arguments: Both Arg0 and Arg1 are integers or unsigned integers.

CAST

public static final SymbolicExpression.SymbolicOperator CAST

Operator for an expression representing the result of converting a value from one type to another. 1 argument: the value being cast. The SymbolicExpression.type() method in this expression yields the new type to which the element is being cast.

CONCRETE

public static final SymbolicExpression.SymbolicOperator CONCRETE

TODO: this will go away in the refactoring. Operator for a concrete value acting as a symbolic expression. One argument, which is the concrete value. Argument may be BooleanObject, NumberObject, CharObject, or an Iterable<? extends SymbolicExpression> . The last case is used to represent concrete values for arrays or tuples.

COND

public static final SymbolicExpression.SymbolicOperator COND

Operator for a conditional expression, also known as "if-then-else", as in C's ternary expression arg0 ? arg1 : arg2. 3 arguments. Arg0 is the boolean predicate expression (an instance of BooleanExpression), arg1 is the expression which is the result if arg0 evaluates to true, arg2 the expression which is the result if arg0 evaluates to false. arg1 and arg2 must have the same type, which is the type of the conditional expression.

DENSE_ARRAY_WRITE

public static final SymbolicExpression.SymbolicOperator DENSE_ARRAY_WRITE

Operator for expression that represents the result of multiple writes to distinct concrete positions in an array. 2 arguments. Arg0 is an expression of SymbolicArrayType T[]. Arg1 is an Iterable<? extends SymbolicExpression> . Say the elements of the iterable object are v₀ ,...,v_n-1. Each element of the sequence is either NULL (i.e., the expression with operator NULL) or an expression of type T. The dense array write expression represents the result of starting with arg0 and then for each i for which v_i is non-NULL, setting the array element in position i to v_i. It is thus equivalent to a sequence of array write operations (which can be performed in any order since they are to distinct positions). It is included here to allow a dense representation of the array, which can have performance benefits, in particular constant-time lookup and modification (just like for regular concrete arrays).

See Also:

• ARRAY_WRITE
• DENSE_TUPLE_WRITE

DENSE_TUPLE_WRITE

public static final SymbolicExpression.SymbolicOperator DENSE_TUPLE_WRITE

Operator representing the result of multiple writes to different components of a tuple. Similar to DENSE_ARRAY_WRITE. Arg0 is an expression of SymbolicTupleType. Arg1 is an Iterable<? extends SymbolicExpression> . The writes to the components of the tuple are taken from arg1 in order. Entries which are NULL are ignored (as with arrays). The number of elements in arg1 may be less than the number of components in the tuple, in which case only those elements are used. If the length of arg1 is greater, the extra elements are ignored.

See Also:

• DENSE_ARRAY_WRITE

DERIV

public static final SymbolicExpression.SymbolicOperator DERIV

The (partial) derivative operator. Arg0 is an expression of type function from R^n to R, for some positive integer n. Arg1 is an IntObject which is a concrete integer in [0,n); it is the index of the independent variable with respect to which the derivative is being taken. Arg2 is an IntObject which is a natural number and is the degree of the derivative (i.e., the number of compositions of the derivative operator).

DIFFERENTIABLE

public static final SymbolicExpression.SymbolicOperator DIFFERENTIABLE

A predicate which declares a real-valued function to have some number of continuous derivatives over a bounded, rectangular, closed interval in R^n. Arg0 is a function from R^n to R for some positive integer n. Arg1 is the degree, a nonnegative integer IntObject which tells the number of partial derivatives (of any combination) that exist and are continuous. Arg2 is a sequence of real-value expressions which are the lower bounds of the intervals in the domain; the length is n. Arg3 is a similar sequence of upper bounds. Degree 0 means the function is continuous on the domain.

DIVIDE

public static final SymbolicExpression.SymbolicOperator DIVIDE

Operator for real number division. 2 arguments: arg0 the numerator, arg1 the denominator. Both must be symbolic expressions of SymbolicRealType. Result also has SymbolicRealType.

See Also:

• INT_DIVIDE

EQUALS

public static final SymbolicExpression.SymbolicOperator EQUALS

Operator for comparison of two values for equality. Two arguments of any type or kind, not necessarily only NumericExpressions. Result is a BooleanExpression.

See Also:

• NEQ

EXISTS

public static final SymbolicExpression.SymbolicOperator EXISTS

Operator for for existential quantification: ∃ x . e. 2 arguments. arg0 is a SymbolicConstant x, the bound variable. Arg1 is e, a BooleanExpression which may involve x. Result has boolean type.

See Also:

• FORALL

FORALL

public static final SymbolicExpression.SymbolicOperator FORALL

Operator for for universal quantification: ∀ x . e. 2 arguments. arg0 is a SymbolicConstant x, the bound variable. Arg1 is e, a BooleanExpression which may involve x. Result has boolean type.

See Also:

• EXISTS

INT_DIVIDE

public static final SymbolicExpression.SymbolicOperator INT_DIVIDE

Operator for integer division. Two arguments, both SymbolicExpressions of SymbolicIntegerType. Arg0 is the numerator, arg1 the denominator. Result has SymbolicIntegerType. Result is obtained by rounding towards 0. Undefined behavior if denominator is not positive.

See Also:

• DIVIDE

LAMBDA

public static final SymbolicExpression.SymbolicOperator LAMBDA

Operator for a lambda expression, as in the lambda calculus: λ x . e. Two arguments. Arg0 is a SymbolicConstant x, the bound variable. Arg1 is e, a SymbolicExpression possibly involving x. The result has SymbolicFunctionType and represents the function of one variable which, given x returns e.

LENGTH

public static final SymbolicExpression.SymbolicOperator LENGTH

Operator for getting the length of an array. Has 1 argument, arg0, which is the array expression, a SymbolicExpression of type SymbolicArrayType. Result has SymbolicIntegerType.

LESS_THAN

public static final SymbolicExpression.SymbolicOperator LESS_THAN

Operator for a less-than expression: x < y. Two arguments, both instances of NumericExpression with the same numeric type. Arg0 is x, arg1 is y. Result has boolean type.

See Also:

• LESS_THAN_EQUALS

LESS_THAN_EQUALS

public static final SymbolicExpression.SymbolicOperator LESS_THAN_EQUALS

Operator for a less-than-or-equals expression: x ≤ y . Two arguments, both instances of NumericExpression with the same numeric type. Arg0 is x, arg1 is y. Result has boolean type.

See Also:

• LESS_THAN

MODULO

public static final SymbolicExpression.SymbolicOperator MODULO

The integer modulus operator. Takes 2 arguments, result represents x mod y (or x%y in C). Arg0 is x, arg1 is y. Both arguments and the result are NumericExpressions of SymbolicIntegerType. Undefined behavior if y is not positive.

See Also:

• INT_DIVIDE

MULTIPLY

public static final SymbolicExpression.SymbolicOperator MULTIPLY

Operator for an expression representing the numerical product of symbolic expressions. Can have any number of arguments, all of same numeric type. Result is also a NumericExpression.

See Also:

• ADD

NEGATIVE

public static final SymbolicExpression.SymbolicOperator NEGATIVE

Operator for numerical negation, i.e., - x. 1 argument, which is a NumericExpression. The result is a NumericExpression of the same type as that of the argument.

NEQ

public static final SymbolicExpression.SymbolicOperator NEQ

Operator for comparison of two values for inequality. Two arguments, both symbolic expressions of the same type. Result is a BooleanExpression.

See Also:

• EQUALS

NOT

public static final SymbolicExpression.SymbolicOperator NOT

Operator for logical negation ("not"). Takes one argument, a BooleanExpression. Result is a BooleanExpression.

See Also:

• AND
• OR

NULL

public static final SymbolicExpression.SymbolicOperator NULL

Operator used to represent no symbolic expression in cases where Java's null is not acceptable. This is the only kind of SymbolicExpression that has a null type! Takes no arguments.

OR

public static final SymbolicExpression.SymbolicOperator OR

Operator for an expression representing the disjunction of symbolic expressions of boolean type. Has any number of arguments, all of boolean type. Result is also a BooleanExpression.

See Also:

• AND

POWER

public static final SymbolicExpression.SymbolicOperator POWER

Operator for exponentiation, i.e., the raising of some number to some power: x ^y. Takes two arguments: arg0 is the base x, arg1 is the exponent y. The exponent can be either a NumericExpression or an IntObject. In the latter case, the int must be non-negative.

SUBTRACT

public static final SymbolicExpression.SymbolicOperator SUBTRACT

Operator for numerical subtraction: x − y. Two arguments, both NumericExpressions of the same type: arg0 is x, arg1 is y. Result is also a NumericExpression of the same type.

SYMBOLIC_CONSTANT

public static final SymbolicExpression.SymbolicOperator SYMBOLIC_CONSTANT

Operator used to represent a symbolic constant. Takes one argument, a StringObject, which gives the name of the symbolic constant. Note that a symbolic constant can have any SymbolicType, including a SymbolicFunctionType.

TUPLE

public static final SymbolicExpression.SymbolicOperator TUPLE

A concrete tuple. The arguments are the components of the tuple.

TUPLE_READ

public static final SymbolicExpression.SymbolicOperator TUPLE_READ

Operator for an expression representing the result of reading a component of a tuple. Takes two arguments: arg0 is the tuple expression, arg1 is an IntObject giving the index into the tuple.

See Also:

• TUPLE_WRITE

TUPLE_WRITE

public static final SymbolicExpression.SymbolicOperator TUPLE_WRITE

Operator for an expression representing the result of modifying a single component of a tuple. Takes three arguments: arg0 is the original expression of SymbolicTupleType, arg1 is an IntObject specifying the index into the tuple, and arg2 is the expression that will be the new value for specified component. The result represents the tuple that is the same as arg0, except in component arg1, where the value is arg2.

See Also:

• TUPLE_READ
• DENSE_TUPLE_WRITE

UNION_EXTRACT

public static final SymbolicExpression.SymbolicOperator UNION_EXTRACT

Operator for extracting an element of a SymbolicUnionType to an element of a member type. Takes 2 arguments: arg0 is an IntObject giving the index of a member type of a union type; arg1 is a SymbolicExpression whose type is the union type. The resulting expression has type the specified member type. This essentially pulls the expression out of the union and casts it to the member type. If arg1 does not belong to the member type (as determined by a UNION_TEST expression), the value of this expression is undefined.

UNION_INJECT

public static final SymbolicExpression.SymbolicOperator UNION_INJECT

Operator for injecting an element of a member type into a SymbolicUnionType that includes that member type. Takes 2 arguments: arg0 is an IntObject giving the index of the member type of the union type; arg1 is a SymbolicExpression whose type is the member type. The union type itself is the type of the UNION_INJECT expression.

UNION_TEST

public static final SymbolicExpression.SymbolicOperator UNION_TEST

Operator to determine whether an expression in a SymbolicUnionType is in the image of injection from a specified member type. Takes 2 arguments: arg0 is an IntObject giving the index of a member type of the union type; arg1 is a SymbolicExpression whose type is the union type. This is a boolean-valued expression whose value is true iff arg1 belongs to the specified member type of the union type.

Method Details

values

public static SymbolicExpression.SymbolicOperator[] values()

Returns an array containing the constants of this enum class, in the order they are declared.

Returns:

an array containing the constants of this enum class, in the order they are declared

valueOf

public static SymbolicExpression.SymbolicOperator valueOf(String name)

Returns the enum constant of this class with the specified name. The string must match exactly an identifier used to declare an enum constant in this class. (Extraneous whitespace characters are not permitted.)

Parameters:

name - the name of the enum constant to be returned.

Returns:

the enum constant with the specified name

Throws:

IllegalArgumentException - if this enum class has no constant with the specified name

NullPointerException - if the argument is null