kodkod.ast

Class IntExpression

java.lang.Object

kodkod.ast.Node

kodkod.ast.IntExpression

Direct Known Subclasses:

BinaryIntExpression, ExprToIntCast, IfIntExpression, IntConstant, NaryIntExpression, SumExpression, UnaryIntExpression

public abstract class IntExpression
extends Node

A Node whose value is an integer rather than a relational expression.

Author:

Emina Torlak

Method Summary

Modifier and Type	Method and Description
IntExpression	abs() Returns an IntExpression that represents the absolute value of this int expression.
abstract <E,F,D,I> I	accept(ReturnVisitor<E,F,D,I> visitor) Accepts the given visitor and returns the result of the visit (i.e.
abstract void	accept(VoidVisitor visitor) Accepts the given void visitor by calling visitor.visit(this).
static IntExpression	and(Collection<? extends IntExpression> intExprs) Returns the bitwise and of the given int expressions.
static IntExpression	and(IntExpression... intExprs) Returns the bitwise and of the given int expressions.
IntExpression	and(IntExpression intExpr) Returns an IntExpression that represents the bitwise AND of this and the given int node.
IntExpression	apply(IntOperator op) Returns an expression that represents the application of the given unary operator to this integer expression.
Expression	cast(IntCastOperator op) Returns an expression that is the relational representation of this integer expression specified by the given operator.
Formula	compare(IntCompOperator op, IntExpression intExpr) Returns a formula comparing this and the given integer expression using the specified operator.
static IntExpression	compose(IntOperator op, Collection<? extends IntExpression> intExprs) Returns the composition of the given int expressions using the given operator.
static IntExpression	compose(IntOperator op, IntExpression... intExprs) Returns the composition of the given int expressions using the given operator.
IntExpression	compose(IntOperator op, IntExpression intExpr) Returns an expression that combines this and the given integer expression using the specified operator.
IntExpression	divide(IntExpression intExpr) Returns an IntExpression that represents the quotient of the division between this and the given int node.
Formula	eq(IntExpression intExpr) Returns a formula stating that the given int expression and this have the same value.
Formula	gt(IntExpression intExpr) Returns a formula stating that the value of this int expression is greater than the value of the given int expression The effect of this method is the same as calling this.compare(GT, intExpr).
Formula	gte(IntExpression intExpr) Returns a formula stating that the value of this int expression is greater than or equal to the value of the given int expression The effect of this method is the same as calling this.compare(GTE, intExpr).
Formula	lt(IntExpression intExpr) Returns a formula stating that the value of this int expression is less than the value of the given int expression The effect of this method is the same as calling this.compare(LT, intExpr).
Formula	lte(IntExpression intExpr) Returns a formula stating that the value of this int expression is less than or equal to the value of the given int expression The effect of this method is the same as calling this.compare(LTE, intExpr).
IntExpression	minus(IntExpression intExpr) Returns an IntExpression that represents the difference between this and the given int node.
IntExpression	modulo(IntExpression intExpr) Returns an IntExpression that represents the remainder of the division between this and the given int node.
static IntExpression	multiply(Collection<? extends IntExpression> intExprs) Returns the product of the given int expressions.
static IntExpression	multiply(IntExpression... intExprs) Returns the product of the given int expressions.
IntExpression	multiply(IntExpression intExpr) Returns an IntExpression that represents the product of this and the given int node.
IntExpression	negate() Returns an IntExpression that represents the negation of this int expression.
IntExpression	not() Returns an IntExpression that represents the bitwise negation of this int expression.
static IntExpression	or(Collection<? extends IntExpression> intExprs) Returns the bitwise or of the given int expressions.
static IntExpression	or(IntExpression... intExprs) Returns the bitwise or of the given int expressions.
IntExpression	or(IntExpression intExpr) Returns an IntExpression that represents the bitwise OR of this and the given int node.
static IntExpression	plus(Collection<? extends IntExpression> intExprs) Returns the plus of the given int expressions.
static IntExpression	plus(IntExpression... intExprs) Returns the sum of the given int expressions.
IntExpression	plus(IntExpression intExpr) Returns an IntExpression that represents the sum of this and the given int node.
IntExpression	sha(IntExpression intExpr) Returns an IntExpression that represents the right shift of this and the given int node, with sign extension.
IntExpression	shl(IntExpression intExpr) Returns an IntExpression that represents the left shift of this by the given int node.
IntExpression	shr(IntExpression intExpr) Returns an IntExpression that represents the right shift of this and the given int node, with zero extension.
IntExpression	signum() Returns an IntExpression that represents the sign of this int expression.
IntExpression	sum(Decls decls) Returns an integer expression that is the sum of all values that this integer expression can take given the provided declarations.
Expression	toBitset() Returns an expression whose meaning is the set containing the atoms that represent the powers of 2 (bits) present in this integer expression.
Expression	toExpression() Returns an expression whose meaning is the singleton set containing the atom that represents the integer given by this integer expression.
IntExpression	xor(IntExpression intExpr) Returns an IntExpression that represents the bitwise XOR of this and the given int node.

Methods inherited from class kodkod.ast.Node

toString

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Method Detail

abs

public final IntExpression abs()

Returns an IntExpression that represents the absolute value of this int expression. The effect of this method is the same as calling this.apply(ABS).

Returns:

this.apply(ABS)

accept

public abstract <E,F,D,I> I accept(ReturnVisitor<E,F,D,I> visitor)

Accepts the given visitor and returns the result of the visit (i.e. the result of the call visitor.visit(this))

Specified by:

accept in class Node

Returns:

the result of being visited by the given visitor

See Also:

Node.accept(kodkod.ast.visitor.ReturnVisitor)

accept

public abstract void accept(VoidVisitor visitor)

Accepts the given void visitor by calling visitor.visit(this).

Specified by:

accept in class Node

See Also:

Node.accept(kodkod.ast.visitor.VoidVisitor)

and

public static IntExpression and(Collection<? extends IntExpression> intExprs)

Returns the bitwise and of the given int expressions. The effect of this method is the same as calling compose(AND, intExprs).

Returns:

compose(AND, intExprs)

and

public static IntExpression and(IntExpression... intExprs)

Returns the bitwise and of the given int expressions. The effect of this method is the same as calling compose(AND, intExprs).

Returns:

compose(AND, intExprs)

and

public final IntExpression and(IntExpression intExpr)

Returns an IntExpression that represents the bitwise AND of this and the given int node. The effect of this method is the same as calling this.compose(AND, intExpr).

Returns:

this.compose(AND, intExpr)

apply

public final IntExpression apply(IntOperator op)

Returns an expression that represents the application of the given unary operator to this integer expression.

Requires:

op.unary()

Returns:

{e: IntExpression | e.op = op and e.intExpr = this }

cast

public final Expression cast(IntCastOperator op)

Returns an expression that is the relational representation of this integer expression specified by the given operator.

Returns:

an expression that is the relational representation of this integer expression specified by the given operator.

compare

public Formula compare(IntCompOperator op,
                       IntExpression intExpr)

Returns a formula comparing this and the given integer expression using the specified operator.

Returns:

{f: Formula | f.left = this and f.right = intExpr and f.op = op }

compose

public static IntExpression compose(IntOperator op,
                                    Collection<? extends IntExpression> intExprs)

Returns the composition of the given int expressions using the given operator.

Requires:

intExprs.length = 2 => op.binary(), intExprs.length > 2 => op.nary()

Returns:

intExprs.size() = 1 => intExprs.iterator().next() else {e: IntExpression | e.children = intExprs.toArray() and e.op = this }

compose

public static IntExpression compose(IntOperator op,
                                    IntExpression... intExprs)

Returns the composition of the given int expressions using the given operator.

Requires:

intExprs.length = 2 => op.binary(), intExprs.length > 2 => op.nary()

Returns:

intExprs.length=1 => intExprs[0] else {e: IntExpression | e.children = intExprs and e.op = this }

compose

public final IntExpression compose(IntOperator op,
                                   IntExpression intExpr)

Returns an expression that combines this and the given integer expression using the specified operator.

Requires:

op.binary()

Returns:

{e: IntExpression | e.left = this and e.right = intExpr and e.op = op }

divide

public final IntExpression divide(IntExpression intExpr)

Returns an IntExpression that represents the quotient of the division between this and the given int node. The effect of this method is the same as calling this.compose(DIVIDE, intExpr).

Returns:

this.compose(DIVIDE, intExpr)

eq

public final Formula eq(IntExpression intExpr)

Returns a formula stating that the given int expression and this have the same value. The effect of this method is the same as calling this.compare(EQ, intExpr).

Returns:

this.compare(EQ, intExpr)

gt

public final Formula gt(IntExpression intExpr)

Returns a formula stating that the value of this int expression is greater than the value of the given int expression The effect of this method is the same as calling this.compare(GT, intExpr).

Returns:

this.compare(GT, intExpr)

gte

public final Formula gte(IntExpression intExpr)

Returns a formula stating that the value of this int expression is greater than or equal to the value of the given int expression The effect of this method is the same as calling this.compare(GTE, intExpr).

Returns:

this.compare(GTE, intExpr)

lt

public final Formula lt(IntExpression intExpr)

Returns a formula stating that the value of this int expression is less than the value of the given int expression The effect of this method is the same as calling this.compare(LT, intExpr).

Returns:

this.compare(LT, intExpr)

lte

public final Formula lte(IntExpression intExpr)

Returns a formula stating that the value of this int expression is less than or equal to the value of the given int expression The effect of this method is the same as calling this.compare(LTE, intExpr).

Returns:

this.compare(LTE, intExpr)

minus

public final IntExpression minus(IntExpression intExpr)

Returns an IntExpression that represents the difference between this and the given int node. The effect of this method is the same as calling this.compose(MINUS, intExpr).

Returns:

this.compose(MINUS, intExpr)

modulo

public final IntExpression modulo(IntExpression intExpr)

Returns an IntExpression that represents the remainder of the division between this and the given int node. The effect of this method is the same as calling this.compose(MODULO, intExpr).

Returns:

this.compose(MODULO, intExpr)

multiply

public static IntExpression multiply(Collection<? extends IntExpression> intExprs)

Returns the product of the given int expressions. The effect of this method is the same as calling compose(MULTIPLY, intExprs).

Returns:

compose(MULTIPLY, intExprs)

multiply

public static IntExpression multiply(IntExpression... intExprs)

Returns the product of the given int expressions. The effect of this method is the same as calling compose(MULTIPLY, intExprs).

Returns:

compose(MULTIPLY, intExprs)

multiply

public final IntExpression multiply(IntExpression intExpr)

Returns an IntExpression that represents the product of this and the given int node. The effect of this method is the same as calling this.compose(MULTIPLY, intExpr).

Returns:

this.compose(MULTIPLY, intExpr)

negate

public final IntExpression negate()

Returns an IntExpression that represents the negation of this int expression. The effect of this method is the same as calling this.apply(NEG).

Returns:

this.apply(NEG)

not

public final IntExpression not()

Returns an IntExpression that represents the bitwise negation of this int expression. The effect of this method is the same as calling this.apply(NOT).

Returns:

this.apply(NOT)

or

public static IntExpression or(Collection<? extends IntExpression> intExprs)

Returns the bitwise or of the given int expressions. The effect of this method is the same as calling compose(OR, intExprs).

Returns:

compose(OR, intExprs)

or

public static IntExpression or(IntExpression... intExprs)

Returns the bitwise or of the given int expressions. The effect of this method is the same as calling compose(OR, intExprs).

Returns:

compose(OR, intExprs)

or

public final IntExpression or(IntExpression intExpr)

Returns an IntExpression that represents the bitwise OR of this and the given int node. The effect of this method is the same as calling this.compose(OR, intExpr).

Returns:

this.compose(OR, intExpr)

plus

public static IntExpression plus(Collection<? extends IntExpression> intExprs)

Returns the plus of the given int expressions. The effect of this method is the same as calling compose(PLUS, intExprs).

Returns:

compose(PLUS, intExprs)

plus

public static IntExpression plus(IntExpression... intExprs)

Returns the sum of the given int expressions. The effect of this method is the same as calling compose(PLUS, intExprs).

Returns:

compose(PLUS, intExprs)

plus

public final IntExpression plus(IntExpression intExpr)

Returns an IntExpression that represents the sum of this and the given int node. The effect of this method is the same as calling this.compose(PLUS, intExpr).

Returns:

this.compose(PLUS, intExpr)

sha

public final IntExpression sha(IntExpression intExpr)

Returns an IntExpression that represents the right shift of this and the given int node, with sign extension. The effect of this method is the same as calling this.compose(SHA, intExpr).

Returns:

this.compose(SHA, intExpr)

shl

public final IntExpression shl(IntExpression intExpr)

Returns an IntExpression that represents the left shift of this by the given int node. The effect of this method is the same as calling this.compose(SHL, intExpr).

Returns:

this.compose(SHL, intExpr)

shr

public final IntExpression shr(IntExpression intExpr)

Returns an IntExpression that represents the right shift of this and the given int node, with zero extension. The effect of this method is the same as calling this.compose(SHR, intExpr).

Returns:

this.compose(SHR, intExpr)

signum

public final IntExpression signum()

Returns an IntExpression that represents the sign of this int expression. The effect of this method is the same as calling this.apply(SGN).

Returns:

this.apply(SGN)

sum

public final IntExpression sum(Decls decls)

Returns an integer expression that is the sum of all values that this integer expression can take given the provided declarations.

Returns:

{e: IntExpression | e.decls = decls and e.intExpr = this }

toBitset

public final Expression toBitset()

Returns an expression whose meaning is the set containing the atoms that represent the powers of 2 (bits) present in this integer expression. The effect of this method is the same as calling this.cast(BITSETCAST).

Returns:

this.cast(BITSETCAST)

toExpression

public final Expression toExpression()

Returns an expression whose meaning is the singleton set containing the atom that represents the integer given by this integer expression. The effect of this method is the same as calling this.cast(INTCAST).

Returns:

this.cast(INTCAST)

xor

public final IntExpression xor(IntExpression intExpr)

Returns an IntExpression that represents the bitwise XOR of this and the given int node. The effect of this method is the same as calling this.compose(XOR, intExpr).

Returns:

this.compose(XOR, intExpr)