Uses of Class
kodkod.ast.IntExpression

Packages that use IntExpression

Package	Description
kodkod.ast	Contains classes for creating Kodkod formulas, expressions, and integer expressions.
kodkod.ast.visitor	Contains visitors for Kodkod formulas, expressions, and integer expressions.
kodkod.engine	Provides classes for analyzing and evaluating Kodkod ASTs with respect to finite bounds or instances.
kodkod.engine.fol2sat	Provides a facade for translating, evaluating, and approximating Kodkod formulas, expressions, and int expressions with respect to a given Bounds (or Instance) and Options.

Uses of IntExpression in kodkod.ast

Subclasses of IntExpression in kodkod.ast

Modifier and Type	Class and Description
class	BinaryIntExpression A binary integer expression such as x + y.
class	ExprToIntCast An IntExpression representing the cardinality of an Expression or the sum of all the integer atoms contained in the expression.
class	IfIntExpression An int expression whose value depends on the truth of a condition.
class	IntConstant An integer constant (literal).
class	NaryIntExpression A int expression with more than two children, composed with an nary operator.
class	SumExpression Denotes the integer obtained by summing the values of an iteger expression ie for all values of a scalar x drawn from a set e.
class	UnaryIntExpression A unary integer intExpr, e.g.

Methods in kodkod.ast that return IntExpression

Modifier and Type	Method and Description
IntExpression	IntExpression.abs() Returns an IntExpression that represents the absolute value of this int expression.
static IntExpression	IntExpression.and(Collection<? extends IntExpression> intExprs) Returns the bitwise and of the given int expressions.
static IntExpression	IntExpression.and(IntExpression... intExprs) Returns the bitwise and of the given int expressions.
IntExpression	IntExpression.and(IntExpression intExpr) Returns an IntExpression that represents the bitwise AND of this and the given int node.
IntExpression	Expression.apply(ExprCastOperator op) Returns the cast of this expression to an integer expression, that represents either the cardinality of this expression (if op is CARDINALITY) or the sum of the integer atoms it contains (if op is SUM).
IntExpression	IntExpression.apply(IntOperator op) Returns an expression that represents the application of the given unary operator to this integer expression.
IntExpression	NaryIntExpression.child(int i) Returns the ith child of this int expression.
IntExpression	ProjectExpression.column(int i) Returns the ith column.
static IntExpression	IntExpression.compose(IntOperator op, Collection<? extends IntExpression> intExprs) Returns the composition of the given int expressions using the given operator.
static IntExpression	IntExpression.compose(IntOperator op, IntExpression... intExprs) Returns the composition of the given int expressions using the given operator.
IntExpression	IntExpression.compose(IntOperator op, IntExpression intExpr) Returns an expression that combines this and the given integer expression using the specified operator.
IntExpression	Expression.count() Returns the cardinality of this expression.
IntExpression	IntExpression.divide(IntExpression intExpr) Returns an IntExpression that represents the quotient of the division between this and the given int node.
IntExpression	IfIntExpression.elseExpr() Returns the else-expression.
IntExpression	UnaryIntExpression.intExpr() Returns this.intExpr.
IntExpression	SumExpression.intExpr() Returns this.intExpr.
IntExpression	IntToExprCast.intExpr() Returns this.intExpr.
IntExpression	IntComparisonFormula.left() Returns the left child of this.
IntExpression	BinaryIntExpression.left() Returns the left child of this.
IntExpression	IntExpression.minus(IntExpression intExpr) Returns an IntExpression that represents the difference between this and the given int node.
IntExpression	IntExpression.modulo(IntExpression intExpr) Returns an IntExpression that represents the remainder of the division between this and the given int node.
static IntExpression	IntExpression.multiply(Collection<? extends IntExpression> intExprs) Returns the product of the given int expressions.
static IntExpression	IntExpression.multiply(IntExpression... intExprs) Returns the product of the given int expressions.
IntExpression	IntExpression.multiply(IntExpression intExpr) Returns an IntExpression that represents the product of this and the given int node.
IntExpression	IntExpression.negate() Returns an IntExpression that represents the negation of this int expression.
IntExpression	IntExpression.not() Returns an IntExpression that represents the bitwise negation of this int expression.
static IntExpression	IntExpression.or(Collection<? extends IntExpression> intExprs) Returns the bitwise or of the given int expressions.
static IntExpression	IntExpression.or(IntExpression... intExprs) Returns the bitwise or of the given int expressions.
IntExpression	IntExpression.or(IntExpression intExpr) Returns an IntExpression that represents the bitwise OR of this and the given int node.
static IntExpression	IntExpression.plus(Collection<? extends IntExpression> intExprs) Returns the plus of the given int expressions.
static IntExpression	IntExpression.plus(IntExpression... intExprs) Returns the sum of the given int expressions.
IntExpression	IntExpression.plus(IntExpression intExpr) Returns an IntExpression that represents the sum of this and the given int node.
IntExpression	IntComparisonFormula.right() Returns the right child of this.
IntExpression	BinaryIntExpression.right() Returns the right child of this.
IntExpression	IntExpression.sha(IntExpression intExpr) Returns an IntExpression that represents the right shift of this and the given int node, with sign extension.
IntExpression	IntExpression.shl(IntExpression intExpr) Returns an IntExpression that represents the left shift of this by the given int node.
IntExpression	IntExpression.shr(IntExpression intExpr) Returns an IntExpression that represents the right shift of this and the given int node, with zero extension.
IntExpression	IntExpression.signum() Returns an IntExpression that represents the sign of this int expression.
IntExpression	Expression.sum() Returns the sum of the integer atoms in this expression.
IntExpression	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.
IntExpression	Formula.thenElse(IntExpression thenExpr, IntExpression elseExpr) Returns the if expression constructed from this formula and the specified then and else integer expressions.
IntExpression	IfIntExpression.thenExpr() Returns the then-expression.
IntExpression	IntExpression.xor(IntExpression intExpr) Returns an IntExpression that represents the bitwise XOR of this and the given int node.

Methods in kodkod.ast that return types with arguments of type IntExpression

Modifier and Type	Method and Description
Iterator<IntExpression>	ProjectExpression.columns() Returns an iterator over this.columns, in proper sequence.
Iterator<IntExpression>	NaryIntExpression.iterator() Returns an iterator over this int expression's children, in the increasing order of indices.

Methods in kodkod.ast with parameters of type IntExpression

Modifier and Type	Method and Description
static IntExpression	IntExpression.and(IntExpression... intExprs) Returns the bitwise and of the given int expressions.
IntExpression	IntExpression.and(IntExpression intExpr) Returns an IntExpression that represents the bitwise AND of this and the given int node.
Formula	IntExpression.compare(IntCompOperator op, IntExpression intExpr) Returns a formula comparing this and the given integer expression using the specified operator.
static IntExpression	IntExpression.compose(IntOperator op, IntExpression... intExprs) Returns the composition of the given int expressions using the given operator.
IntExpression	IntExpression.compose(IntOperator op, IntExpression intExpr) Returns an expression that combines this and the given integer expression using the specified operator.
IntExpression	IntExpression.divide(IntExpression intExpr) Returns an IntExpression that represents the quotient of the division between this and the given int node.
Formula	IntExpression.eq(IntExpression intExpr) Returns a formula stating that the given int expression and this have the same value.
Formula	IntExpression.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	IntExpression.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	IntExpression.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	IntExpression.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	IntExpression.minus(IntExpression intExpr) Returns an IntExpression that represents the difference between this and the given int node.
IntExpression	IntExpression.modulo(IntExpression intExpr) Returns an IntExpression that represents the remainder of the division between this and the given int node.
static IntExpression	IntExpression.multiply(IntExpression... intExprs) Returns the product of the given int expressions.
IntExpression	IntExpression.multiply(IntExpression intExpr) Returns an IntExpression that represents the product of this and the given int node.
static IntExpression	IntExpression.or(IntExpression... intExprs) Returns the bitwise or of the given int expressions.
IntExpression	IntExpression.or(IntExpression intExpr) Returns an IntExpression that represents the bitwise OR of this and the given int node.
static IntExpression	IntExpression.plus(IntExpression... intExprs) Returns the sum of the given int expressions.
IntExpression	IntExpression.plus(IntExpression intExpr) Returns an IntExpression that represents the sum of this and the given int node.
Expression	Expression.project(IntExpression... columns) Returns the projection of this expression onto the specified columns.
IntExpression	IntExpression.sha(IntExpression intExpr) Returns an IntExpression that represents the right shift of this and the given int node, with sign extension.
IntExpression	IntExpression.shl(IntExpression intExpr) Returns an IntExpression that represents the left shift of this by the given int node.
IntExpression	IntExpression.shr(IntExpression intExpr) Returns an IntExpression that represents the right shift of this and the given int node, with zero extension.
IntExpression	Formula.thenElse(IntExpression thenExpr, IntExpression elseExpr) Returns the if expression constructed from this formula and the specified then and else integer expressions.
IntExpression	IntExpression.xor(IntExpression intExpr) Returns an IntExpression that represents the bitwise XOR of this and the given int node.

Method parameters in kodkod.ast with type arguments of type IntExpression

Modifier and Type	Method and Description
static IntExpression	IntExpression.and(Collection<? extends IntExpression> intExprs) Returns the bitwise and of the given int expressions.
static IntExpression	IntExpression.compose(IntOperator op, Collection<? extends IntExpression> intExprs) Returns the composition of the given int expressions using the given operator.
static IntExpression	IntExpression.multiply(Collection<? extends IntExpression> intExprs) Returns the product of the given int expressions.
static IntExpression	IntExpression.or(Collection<? extends IntExpression> intExprs) Returns the bitwise or of the given int expressions.
static IntExpression	IntExpression.plus(Collection<? extends IntExpression> intExprs) Returns the plus of the given int expressions.

Constructors in kodkod.ast with parameters of type IntExpression

Constructor and Description
BinaryIntExpression(IntExpression left, IntOperator op, IntExpression right) Constructs a new binary int formula: left op right

Uses of IntExpression in kodkod.ast.visitor

Methods in kodkod.ast.visitor that return IntExpression

Modifier and Type	Method and Description
IntExpression	AbstractReplacer.visit(BinaryIntExpression intExpr) Calls lookup(intExpr) and returns the cached value, if any.
IntExpression	AbstractReplacer.visit(ExprToIntCast intExpr) Calls lookup(intExpr) and returns the cached value, if any.
IntExpression	AbstractReplacer.visit(IfIntExpression intExpr) Calls lookup(intExpr) and returns the cached value, if any.
IntExpression	AbstractReplacer.visit(IntConstant intconst) Calls lookup(intconst) and returns the cached value, if any.
IntExpression	AbstractReplacer.visit(NaryIntExpression intExpr) Calls lookup(intExpr) and returns the cached value, if any.
IntExpression	AbstractReplacer.visit(SumExpression intExpr) Calls lookup(intExpr) and returns the cached value, if any.
IntExpression	AbstractReplacer.visit(UnaryIntExpression intExpr) Calls lookup(intExpr) and returns the cached value, if any.

Uses of IntExpression in kodkod.engine

Methods in kodkod.engine with parameters of type IntExpression

Modifier and Type	Method and Description
int	Evaluator.evaluate(IntExpression intExpr) Evaluates the specified int expession with respect to the relation-tuple mappings given by this.instance and using this.options.

Uses of IntExpression in kodkod.engine.fol2sat

Methods in kodkod.engine.fol2sat with parameters of type IntExpression

Modifier and Type	Method and Description
static Int	Translator.evaluate(IntExpression intExpr, Instance instance, Options options) Evalutes the given intexpression to an Int using the provided instance and options.