fmrisc.ProofNavigator.Proving.CVCL

Class CVCLFormulaMask

java.lang.Object

fmrisc.ProofNavigator.Proving.CVCL.CVCLFormulaMask

public final class CVCLFormulaMask
extends java.lang.Object

Mask certain formulas for CVCL as atomic.

Constructor Summary

Constructors

Constructor and Description
CVCLFormulaMask() Create formula mask with initial context.

Method Summary

Modifier and Type	Method and Description
Expression	getFormula(Identifier mask) Get formula associated to mask identifier
Expression	getMask(Expression f) Mask a formula.
java.util.Collection<ValueSymbol>	getSymbols() Return mask symbols generated since last call of resetSymbols().
void	resetSymbols() Reset collection of generated mask symbols.

Methods inherited from class java.lang.Object

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

Constructor Detail

CVCLFormulaMask

public CVCLFormulaMask()

Create formula mask with initial context.

Method Detail

getMask

public Expression getMask(Expression f)

Mask a formula.

Parameters:

f - a formula expression

Returns:

an expression that replaces the formula (either a reference or a reference application)

getFormula

public Expression getFormula(Identifier mask)

Get formula associated to mask identifier

Parameters:

mask - identifier of a mask

Returns:

formula expression to which mask is bound (null, if none)

resetSymbols

public void resetSymbols()

Reset collection of generated mask symbols.

getSymbols

public java.util.Collection<ValueSymbol> getSymbols()

Return mask symbols generated since last call of resetSymbols().

Returns:

collection of ValueSymbol objects representing the mask symbols.