Module dev.civl.abc

Package dev.civl.abc.ast.node.IF.expression

Interface QuantifiedExpressionNode

All Superinterfaces:

ASTNode, ExpressionNode, ForLoopInitializerNode, InitializerNode, SizeableNode

public interface QuantifiedExpressionNode
extends ExpressionNode

A CIVL-C quantified expression, including three components, bound variable declaration list, (optional) restriction and expression. It has the following syntax:

 quantified: 
   quantifier ( variable-decl-list | restrict? ) expression ;
 
 variable-decl-list:
   variable-decl-sub-list (; variable-decl-sub-list)* ;
   
 variable-decl-sub-list:
   type ID (, ID)* (: domain)?
   
 quantifier: $forall | $exists | $uniform
 

e.g.,

 $forall (int x, y: dom; double z | x > 0 invalid input: '&'invalid input: '&' zinvalid input: '<'5.9} x*z > -1
 

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static enum	QuantifiedExpressionNode.Quantifier	An enumerated type for the different quantifiers.

Nested classes/interfaces inherited from interface dev.civl.abc.ast.node.IF.ASTNode

ASTNode.NodeKind

Nested classes/interfaces inherited from interface dev.civl.abc.ast.node.IF.expression.ExpressionNode

ExpressionNode.ExpressionKind

Method Summary

Modifier and Type	Method	Description
SequenceNode<PairNode<SequenceNode<VariableDeclarationNode>,ExpressionNode>>	boundVariableList()	the bound variable declaration list, which is a sequence node of pairs of variable declaration list and an optional expression that has domain type.
ExpressionNode	expression()	The quantified expression.
SequenceNode<PairNode<ExpressionNode,ExpressionNode>>	intervalSequence()	The following is an experimental field for the $uniform operator.
QuantifiedExpressionNode.Quantifier	quantifier()	Returns the quantifier.
ExpressionNode	restriction()	Returns the predicate which specifies the restriction on the domain of the bound variables.

Methods inherited from interface dev.civl.abc.ast.node.IF.ASTNode

addAllTransformAnnotations, addTransformAnnotation, child, childIndex, children, diff, equiv, getAttribute, getOwner, getScope, getSource, id, keepOnly, nextDFS, nodeKind, numChildren, parent, prettyPrint, prettyRepresentation, prettyRepresentation, print, remove, removeChild, removeTransformAnnotation, setAttribute, setChild, setId, setOwner, setScope, toString, transformAnnotations

Methods inherited from interface dev.civl.abc.ast.node.IF.expression.ExpressionNode

addConversion, copy, expressionKind, getConversion, getConvertedType, getInitialType, getNumConversions, isConstantExpression, isLvalue, removeConversions, setInitialType

Methods inherited from interface dev.civl.abc.ast.node.IF.declaration.InitializerNode

isSideEffectFree

Methods inherited from interface dev.civl.abc.ast.node.IF.expression.SizeableNode

getType

Method Details

quantifier

QuantifiedExpressionNode.Quantifier quantifier()

Returns the quantifier.

Returns:

The quantifier used by this quantifier expression.

intervalSequence

SequenceNode<PairNode<ExpressionNode,ExpressionNode>> intervalSequence()

The following is an experimental field for the $uniform operator. It is a sequence of real closed intervals that specify the domain of uniform convergence of a big-O expression.

Returns:

the interval sequence; may be null

boundVariableList

SequenceNode<PairNode<SequenceNode<VariableDeclarationNode>,ExpressionNode>> boundVariableList()

the bound variable declaration list, which is a sequence node of pairs of variable declaration list and an optional expression that has domain type. The dimension of the domain expression, if present, should agree with the number of variable declarations in the same pair. e.g., $forall(int i,j: dom1; double x, y | x<y) a[i]*x <= b[j]*y This will have the bound variable list as: {{{int i, int j}, dom1}, {{double x, double y}, NULL}}.

Returns:

the bound variable declaration list

restriction

ExpressionNode restriction()

Returns the predicate which specifies the restriction on the domain of the bound variables.

Returns:

the boolean expression involving the bound variable which restricts the domain of that variable, or null if no restriction is present.

expression

ExpressionNode expression()

The quantified expression.

Returns:

The quantified expression.