fmrisc.ProgramExplorer.Judgements

Class Simplification2

java.lang.Object

fmrisc.ProgramExplorer.Syntax.ASTVisitorBase

fmrisc.ProgramExplorer.Syntax.ASTCloner

fmrisc.ProgramExplorer.Judgements.Simplification2

All Implemented Interfaces:

ASTVisitor

public final class Simplification2
extends ASTCloner

Post-processing of a specification formula to make it easier understandable.

Method Summary

Methods

Modifier and Type	Method and Description
static Expression	perform(Expression exp) Simplify the given expression.
static Formula	perform(Formula formula) Simplify the given formula.
void	visit(AndFormula formula) Simplify formula.
void	visit(ExistsFormula formula) Simplify formula.
void	visit(ForallFormula formula) Simplify formula.
void	visit(OrFormula formula) Simplify formula.

Methods inherited from class fmrisc.ProgramExplorer.Syntax.ASTCloner

clone, 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, 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, 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

Methods inherited from class fmrisc.ProgramExplorer.Syntax.ASTVisitorBase

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, 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, 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, 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, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

perform

public static Expression perform(Expression exp)

Simplify the given expression.

Parameters:

exp - the expression to be simplified..

Returns:

a simplified version of the expression.

perform

public static Formula perform(Formula formula)

Simplify the given formula.

Parameters:

formula - the formula to be simplified..

Returns:

a simplified version of the formula.

visit

public void visit(ForallFormula formula)

Simplify formula.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(ExistsFormula formula)

Simplify formula.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(AndFormula formula)

Simplify formula.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(OrFormula formula)

Simplify formula.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.