fmrisc.Syntax
Class ForallFormula
java.lang.Object
fmrisc.Syntax.ASTBase
fmrisc.Syntax.ExpressionBase
fmrisc.Syntax.QuantifiedExpression
fmrisc.Syntax.ForallFormula
- All Implemented Interfaces:
- AST, Expression
public final class ForallFormula
- extends QuantifiedExpression
Handling of universally quantified formulas.
Methods inherited from class java.lang.Object |
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait |
ForallFormula
public ForallFormula(TypedIdentifier[] variables,
Expression base)
- construct forall formula of variables and base formula
- Parameters:
variables
- the quantified variablesbase
- the base formula
construct
public QuantifiedExpression construct(TypedIdentifier[] variables,
Expression base)
- Construct quantified expression.
- Specified by:
construct
in class QuantifiedExpression
- Parameters:
variables
- typed variables.base
- an expression.
- Returns:
- a quantified expression of the same kind as this expression
with the denoted variables and base expression.
printCore
public void printCore(java.io.PrintWriter out)
- Prints text representation on out (without new line termination).
- Specified by:
printCore
in interface AST
- Overrides:
printCore
in class QuantifiedExpression
- Parameters:
out
- the stream on which the text is written