AbstractVoidVisitor (Kodkod API)

java.lang.Object
- kodkod.ast.visitor.AbstractVoidVisitor

All Implemented Interfaces:

VoidVisitor
```
public abstract class AbstractVoidVisitor
extends Object
implements VoidVisitor
```
Implements a depth first traversal of the kodkod AST.

Author:

Emina Torlak

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`void`	`visit(BinaryExpression binExpr)` Visits the left and right subexpressions if this.visited(binExpr) returns false.
`void`	`visit(BinaryFormula binFormula)` Visits the left and right children if this.visited(binFormula) returns false.
`void`	`visit(BinaryIntExpression intExpr)` Visits the children of the given integer expression if this.visited(intExpr) returns false.
`void`	`visit(ComparisonFormula compFormula)` Visits the left and right children if this.visited(compFormula) returns false.
`void`	`visit(Comprehension comprehension)` Visits the declarations and the formula if this.visited(comprehension) returns false.
`void`	`visit(ConstantExpression constExpr)` Does nothing.
`void`	`visit(ConstantFormula constant)` Does nothing.
`void`	`visit(Decl decl)` Visits the variable and expression of this decl if this.visited(decl) returns false.
`void`	`visit(Decls decls)` Visits all the children of the given declarations node if this.visited(decls) returns false.
`void`	`visit(ExprToIntCast intExpr)` Visits intExpr.expression if this.visited(intExpr) returns false.
`void`	`visit(IfExpression ifExpr)` Visits the if-condition, the then-expression, and the else-expression if this.visited(ifExpr) returns false.
`void`	`visit(IfIntExpression intExpr)` Visits the if-condition, the then-expression, and the else-expression if this.visited(intExpr) returns false.
`void`	`visit(IntComparisonFormula intComp)` Visits the children of the given integer comparison formula if this.visited(intComp) returns false.
`void`	`visit(IntConstant intConst)` Does nothing.
`void`	`visit(IntToExprCast castExpr)` Visits castExpr.intExpr if this.visited(castExpr) returns false.
`void`	`visit(MultiplicityFormula multFormula)` Visits the formula if this.visited(multFormula) returns false.
`void`	`visit(NaryExpression expr)` Visits the children if this.visited(expr) returns false.
`void`	`visit(NaryFormula formula)` Visits the children if this.visited(formula) returns false.
`void`	`visit(NaryIntExpression intExpr)` Visits the children if this.visited(intExpr) returns false.
`void`	`visit(NotFormula not)` Visits the subformula if this.visited(not) returns false.
`void`	`visit(ProjectExpression project)` Visits project.expression and project.columns if this.visited(project) returns false.
`void`	`visit(QuantifiedFormula quantFormula)` Visits the declarations and the formula if this.visited(quantFormula) returns false.
`void`	`visit(Relation relation)` Does nothing.
`void`	`visit(RelationPredicate pred)` Visits the children of the predicate if this.visited(pred) returns false.
`void`	`visit(SumExpression intExpr)` Visits the children of the given sum expression if this.visited(intExpr) returns false.
`void`	`visit(UnaryExpression unaryExpr)` Visits the subexpression if this.visited(unaryExpr) returns false.
`void`	`visit(UnaryIntExpression intExpr)` Visits the subexpression if this.visited(intExpr) returns false.
`void`	`visit(Variable variable)` Does nothing.

Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Method Detail
  - visit
```
public void visit(BinaryExpression binExpr)
```
    Visits the left and right subexpressions if this.visited(binExpr) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    binExpr.left.accept(this) && binExpr.right.accept(this)
  - visit
```
public void visit(BinaryFormula binFormula)
```
    Visits the left and right children if this.visited(binFormula) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    binFormula.left.accept(this) && binFormula.right.accept(this)
  - visit
```
public void visit(BinaryIntExpression intExpr)
```
    Visits the children of the given integer expression if this.visited(intExpr) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    intExpr.left.accept(this) && intExpr.right.accept(this)
  - visit
```
public void visit(ComparisonFormula compFormula)
```
    Visits the left and right children if this.visited(compFormula) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    compFormula.left.accept(this) && compFormula.right.accept(this)
  - visit
```
public void visit(Comprehension comprehension)
```
    Visits the declarations and the formula if this.visited(comprehension) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    comprehension.declarations.accept(this) && comprehension.formula.accept(this)
  - visit
```
public void visit(ConstantExpression constExpr)
```
    Does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
  - visit
```
public void visit(ConstantFormula constant)
```
    Does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
  - visit
```
public void visit(Decl decl)
```
    Visits the variable and expression of this decl if this.visited(decl) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    decl.variable.accept(this) && decl.expression.accept(this)
  - visit
```
public void visit(Decls decls)
```
    Visits all the children of the given declarations node if this.visited(decls) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    all d: declarations.declarations | d.variable.accept(this) && d.expression.accept(this)
  - visit
```
public void visit(ExprToIntCast intExpr)
```
    Visits intExpr.expression if this.visited(intExpr) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    intExpr.expression.accept(this)
  - visit
```
public void visit(IfExpression ifExpr)
```
    Visits the if-condition, the then-expression, and the else-expression if this.visited(ifExpr) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    ifExpr.condition.accept(this) && ifExpr.thenExpr.accept(this) && ifExpr.elseExpr.accept(this)
  - visit
```
public void visit(IfIntExpression intExpr)
```
    Visits the if-condition, the then-expression, and the else-expression if this.visited(intExpr) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    intExpr.condition.accept(this) && intExpr.thenExpr.accept(this) && intExpr.elseExpr.accept(this)
  - visit
```
public void visit(IntComparisonFormula intComp)
```
    Visits the children of the given integer comparison formula if this.visited(intComp) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    intComp.left.accept(this) && intComp.right.accept(this)
  - visit
```
public void visit(IntConstant intConst)
```
    Does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
  - visit
```
public void visit(IntToExprCast castExpr)
```
    Visits castExpr.intExpr if this.visited(castExpr) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    castExpr.expression.accept(this)
  - visit
```
public void visit(MultiplicityFormula multFormula)
```
    Visits the formula if this.visited(multFormula) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    multFormula.expression.accept(this)
  - visit
```
public void visit(NaryExpression expr)
```
    Visits the children if this.visited(expr) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    all i: [0..#expr.children) | expr.child(i).accept(this)
  - visit
```
public void visit(NaryFormula formula)
```
    Visits the children if this.visited(formula) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    all i: [0..#formula.children) | formula.child(i).accept(this)
  - visit
```
public void visit(NaryIntExpression intExpr)
```
    Visits the children if this.visited(intExpr) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    all i: [0..#intExpr.children) | intExpr.child(i).accept(this)
  - visit
```
public void visit(NotFormula not)
```
    Visits the subformula if this.visited(not) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    not.formula.accept(this)
  - visit
```
public void visit(ProjectExpression project)
```
    Visits project.expression and project.columns if this.visited(project) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    project.expression.accept(this) && all i: project.arity | project.columns[i].accept(this)
  - visit
```
public void visit(QuantifiedFormula quantFormula)
```
    Visits the declarations and the formula if this.visited(quantFormula) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    quantFormula.declarations.accept(this) && quantFormula.formula.accept(this)
  - visit
```
public void visit(Relation relation)
```
    Does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
  - visit
```
public void visit(RelationPredicate pred)
```
    Visits the children of the predicate if this.visited(pred) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    pred.relation.accept(this) && (pred.name = FUNCTION => pred.domain.accept(this) && pred.range.accept(this)) && (pred.name = TOTAL_ORDERING => pred.ordered.accept(this) && pred.first.accept(this) && pred.last.accept(this) )
  - visit
```
public void visit(SumExpression intExpr)
```
    Visits the children of the given sum expression if this.visited(intExpr) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    intExpr.decls.accept(this) && intExpr.intExpr.accept(this)
  - visit
```
public void visit(UnaryExpression unaryExpr)
```
    Visits the subexpression if this.visited(unaryExpr) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    unaryExpr.expression.accept(this)
  - visit
```
public void visit(UnaryIntExpression intExpr)
```
    Visits the subexpression if this.visited(intExpr) returns false. Otherwise does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor
    
    Ensures:
    
    unaryExpr.expression.accept(this)
  - visit
```
public void visit(Variable variable)
```
    Does nothing.
    
    Specified by:
    
    visit in interface VoidVisitor

Class AbstractVoidVisitor

Method Summary

Methods inherited from class java.lang.Object

Method Detail

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit