fmrisc.ProofNavigator.Proving

Class GroundExpressions

java.lang.Object

fmrisc.ProofNavigator.Syntax.ASTVisitorBase

fmrisc.ProofNavigator.Proving.GroundExpressions

All Implemented Interfaces:

ASTVisitor

public final class GroundExpressions
extends ASTVisitorBase

Compute ground (sub)expressions.

Constructor Summary

Constructors

Constructor and Description
GroundExpressions()

Method Summary

Modifier and Type	Method and Description
static GroundExpressions	compute(Expression exp) Compute collection of all ground subexpressions of an expression.
static GroundExpressions	compute(ProofState state) Compute collection of ground subexpressions of a proof state.
java.util.Collection<Expression>	getExpressions() Get the collection of ground expressions collected in this set.
boolean	has(Expression exp) Check whether collection contains expression.

Methods inherited from class fmrisc.ProofNavigator.Syntax.ASTVisitorBase

isCloned, visit

Methods inherited from class java.lang.Object

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

Constructor Detail

GroundExpressions

public GroundExpressions()

Method Detail

compute

public static GroundExpressions compute(Expression exp)

Compute collection of all ground subexpressions of an expression.

Parameters:

exp - an expression.

Returns:

a collection of Expression objects representing all ground subexpressions of exp (including exp itself), i.e. all expressions that do not contain free variables.

compute

public static GroundExpressions compute(ProofState state)

Compute collection of ground subexpressions of a proof state.

Parameters:

state - a proof state.

Returns:

a collection of Expression objects representing all ground subexpressions of the formulas (assumptions and goals) in state, i.e. all expressions that do not contain free variables.

getExpressions

public java.util.Collection<Expression> getExpressions()

Get the collection of ground expressions collected in this set.

Returns:

a Collection of Expression objects representing the expressions collected in this set (every expression occurs exactly once in the collection).

has

public boolean has(Expression exp)

Check whether collection contains expression.

Parameters:

exp - an expression.

Returns:

true iff collection contains exp.