public final class ExistsFormula extends QuantifiedFormula
precedence
Modifier and Type | Method and Description |
---|---|
void |
accept(ASTVisitor visitor)
Accept visitor for a visit.
|
static ExistsFormula |
construct(TypedIdentifier[] vars,
Formula body)
Construct an existentially quantified formula.
|
java.lang.String |
getQuantifier()
Get string representation of quantifier.
|
getBody
accept, acceptChildren, getPrecedence, getVariables
getPosition, isLeftAssociative, isRightAssociative, setPosition
accept, accept, print, printCore, toString, toStringCore
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait
getPrecedence, isLeftAssociative, isRightAssociative
getPosition, setPosition
accept, acceptChildren, print, printCore, toString, toStringCore
public static ExistsFormula construct(TypedIdentifier[] vars, Formula body)
vars
- the bound variables of the formula.body
- the body of the formula.public java.lang.String getQuantifier()
getQuantifier
in class QuantifiedExpression
public void accept(ASTVisitor visitor)
accept
in interface AST
accept
in class QuantifiedFormula
visitor
- the visitor who is accepted by this node.