fmrisc.ProgramExplorer.Judgements

Class Simplification

java.lang.Object

fmrisc.ProgramExplorer.Syntax.ASTVisitorBase

fmrisc.ProgramExplorer.Syntax.ASTCloner

fmrisc.ProgramExplorer.Judgements.Simplification

All Implemented Interfaces:

ASTVisitor

public final class Simplification
extends ASTCloner

Simplify a specification formula to make it easier understandable.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	Simplification.Tag The following simplifications are implemented: o Some "quasi-normalization": (A /\ B) /\ C to A /\ (B /\ C) (A \/ B) \/ C to A \/ (B \/ C) A imp (B imp C) to (A /\ B) imp C This simplifies pretty-printing and further processing.

Method Summary

Modifier and Type	Method and Description
static void	collect(Simplification.Tag tag, Formula formula, java.util.Collection<Formula> result) Decompose formula into subformulas if it is of denoted formula type.
static Formula	perform(Formula formula) Simplify the given formula.
void	visit(AndFormula formula) Process conjunction.
void	visit(ArrayTerm exp) Process quantified expression
void	visit(EqualsFormula formula) Process binary atomic formula.
void	visit(ExistsFormula exp) Process quantified expression
void	visit(ForallFormula exp) Process quantified expression
void	visit(GreaterEqualFormula formula) Process binary atomic formula.
void	visit(GreaterFormula formula) Process binary atomic formula.
void	visit(IfThenElseFormula formula) Process disjunction.
void	visit(ImpliesFormula formula) Process implication.
void	visit(LambdaFormula exp) Process quantified expression
void	visit(LambdaTerm exp) Process quantified expression
void	visit(LessEqualFormula formula) Process binary atomic formula.
void	visit(LessFormula formula) Process binary atomic formula.
void	visit(LetExpression exp) Process quantified expression
void	visit(LetFormula exp) Process quantified expression
void	visit(LetTerm exp) Process quantified expression
void	visit(NotEqualsFormula formula) Process binary atomic formula.
void	visit(NotFormula formula) Process negation.
void	visit(OrFormula formula) Process disjunction.
void	visit(SimilarFormula formula) Process binary atomic 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

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

Methods inherited from class java.lang.Object

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

Method Detail

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(EqualsFormula formula)

Process binary atomic formula.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(GreaterEqualFormula formula)

Process binary atomic formula.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(GreaterFormula formula)

Process binary atomic formula.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(LessEqualFormula formula)

Process binary atomic formula.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(LessFormula formula)

Process binary atomic formula.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(NotEqualsFormula formula)

Process binary atomic formula.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(SimilarFormula formula)

Process binary atomic formula.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(NotFormula formula)

Process negation.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(AndFormula formula)

Process conjunction.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(OrFormula formula)

Process disjunction.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(ImpliesFormula formula)

Process implication.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(IfThenElseFormula formula)

Process disjunction.

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

formula - the formula to be simplified.

visit

public void visit(ForallFormula exp)

Process quantified expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - a quantified expression.

visit

public void visit(ExistsFormula exp)

Process quantified expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - a quantified expression.

visit

public void visit(ArrayTerm exp)

Process quantified expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - a quantified expression.

visit

public void visit(LambdaTerm exp)

Process quantified expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - a quantified expression.

visit

public void visit(LambdaFormula exp)

Process quantified expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - a quantified expression.

visit

public void visit(LetExpression exp)

Process quantified expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

Parameters:

exp - a quantified expression.

visit

public void visit(LetTerm exp)

Process quantified expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - a quantified expression.

visit

public void visit(LetFormula exp)

Process quantified expression

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTCloner

Parameters:

exp - a quantified expression.

collect

public static void collect(Simplification.Tag tag,
                           Formula formula,
                           java.util.Collection<Formula> result)

Decompose formula into subformulas if it is of denoted formula type.

Parameters:

tag - a tag indicating the type of the formula.

formula - a formula to be decomposed.

result - the result of the decomposition.