fmrisc.ProofNavigator.Semantics

Class FormulaSymbol

java.lang.Object

fmrisc.ProofNavigator.Semantics.SymbolBase

fmrisc.ProofNavigator.Semantics.FormulaSymbol

All Implemented Interfaces:

Symbol

public final class FormulaSymbol
extends SymbolBase

Entries in FormulaTable.

Constructor Summary

Constructors

Constructor and Description
FormulaSymbol(FormulaDeclIdentifier ident) Construct formula symbol from ident (type is set to null).

Method Summary

Modifier and Type	Method and Description
Environment	getEnvironment() Return environment of symbol (up to the point where the symbol was decld).
Expression	getFormula() Return formula of symbol.
FormulaDeclIdentifier	getFormulaDeclIdentifier() Return identifier of symbol.
Proof	getProof() Return proof of symbol.
boolean	isAxiom() Return axiom status of formula.
void	setAxiom() Set axiom status of formula to true.
void	setEnvironment(Environment env) Set environment of symbol (up to the point where the symbol was decld).
void	setFormula(Expression formula) Set formula of symbol.
void	setProof(Proof proof) Set proof of symbol.

Methods inherited from class fmrisc.ProofNavigator.Semantics.SymbolBase

getIdentifier

Methods inherited from class java.lang.Object

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

Constructor Detail

FormulaSymbol

public FormulaSymbol(FormulaDeclIdentifier ident)

Construct formula symbol from ident (type is set to null).

Parameters:

ident - the identifier of the symbol

Method Detail

getFormulaDeclIdentifier

public FormulaDeclIdentifier getFormulaDeclIdentifier()

Return identifier of symbol.

Returns:

the symbol identifier

getFormula

public Expression getFormula()

Return formula of symbol.

Returns:

the symbol formula

setFormula

public void setFormula(Expression formula)

Set formula of symbol.

Parameters:

formula - the symbol formula

getEnvironment

public Environment getEnvironment()

Return environment of symbol (up to the point where the symbol was decld).

Returns:

the symbol environment

setEnvironment

public void setEnvironment(Environment env)

Set environment of symbol (up to the point where the symbol was decld).

Parameters:

env - the symbol environment

getProof

public Proof getProof()

Return proof of symbol.

Returns:

the symbol proof

setProof

public void setProof(Proof proof)

Set proof of symbol.

Parameters:

proof - the symbol proof

isAxiom

public boolean isAxiom()

Return axiom status of formula.

Returns:

true iff formula is axiom.

setAxiom

public void setAxiom()

Set axiom status of formula to true.