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:
   quantifier ( variable-decl-list | restrict? ) expression ;
   variable-decl-sub-list (; variable-decl-sub-list)* ;
   type ID (, ID)* (: domain)?
 quantifier: $forall | $exists | $uniform
 $forall (int x, y: dom; double z | x > 0 && z<5.9} x*z > -1
  • Method Details

    • quantifier

      Returns the quantifier.
      The quantifier used by this quantifier expression.
    • 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.
      the interval sequence; may be null
    • 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}}.
      the bound variable declaration list
    • restriction

      ExpressionNode restriction()
      Returns the predicate which specifies the restriction on the domain of the bound variables.
      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.
      The quantified expression.