fmrisc.Proving
Class GroundExpressions

java.lang.Object
  fmrisc.Syntax.ASTVisitorBase
      fmrisc.Proving.GroundExpressions

All Implemented Interfaces:

ASTVisitor

public final class GroundExpressions
extends ASTVisitorBase

Compute ground (sub)expressions.

Constructor Summary

GroundExpressions()

Method Summary

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	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.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 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.