fmrisc.ProofNavigator.Semantics

Class FormulaTable

java.lang.Object

fmrisc.ProofNavigator.Semantics.SymbolTable

fmrisc.ProofNavigator.Semantics.FormulaTable

public final class FormulaTable
extends SymbolTable

Symbol table for formulas.

Constructor Summary

Constructors

Constructor and Description
FormulaTable()

Method Summary

Methods

Modifier and Type	Method and Description
FormulaTable	cloneFormulaTable() creates a clone of the symbol table, the clone is a shallow copy (the symbols in the table are not cloned)
Expression	getFormula(Identifier key) returns formula associated to key
FormulaSymbol	getSymbol(Identifier name) returns symbol associated to name (null, if none)
FormulaSymbol	put(FormulaDeclIdentifier key, Expression formula, boolean axiom, Environment env) put formula in formula table

Methods inherited from class fmrisc.ProofNavigator.Semantics.SymbolTable

cloneTable, getSymbols

Methods inherited from class java.lang.Object

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

Constructor Detail

FormulaTable

public FormulaTable()

Method Detail

cloneFormulaTable

public FormulaTable cloneFormulaTable()

creates a clone of the symbol table, the clone is a shallow copy (the symbols in the table are not cloned)

put

public FormulaSymbol put(FormulaDeclIdentifier key,
                Expression formula,
                boolean axiom,
                Environment env)

put formula in formula table

Parameters:

key - the name of the formula

formula - the formula associated to the name

axiom - true iff formula is axiom

env - the environment in which the formula was declared

Returns:

constructed symbol (null, if an error occured)

getSymbol

public FormulaSymbol getSymbol(Identifier name)

returns symbol associated to name (null, if none)

Parameters:

name - the name

Returns:

the symbol associated to the name (may be null)

getFormula

public Expression getFormula(Identifier key)

returns formula associated to key

Parameters:

key - the name of the formula

Returns:

the expression associated to the formula