fmrisc.ProgramExplorer.Semantics

Class FormulaSymbol

java.lang.Object

fmrisc.ProgramExplorer.Semantics.SymbolBase

fmrisc.ProgramExplorer.Semantics.GlobalSymbolBase

fmrisc.ProgramExplorer.Semantics.FormulaSymbol

All Implemented Interfaces:

GlobalSymbol, Symbol

Direct Known Subclasses:

AxiomSymbol

public class FormulaSymbol
extends GlobalSymbolBase

A symbol denoting a logical formula.

Method Summary

Modifier and Type	Method and Description
static FormulaSymbol	construct(Identifier name, Formula formula, FormulaDefinition decl, TheorySymbol theory) Construct formula symbol.
FormulaDefinition	getDeclaration() Get declaration.
Formula	getFormula() Get formula.
void	print(java.io.PrintWriter out) Print symbol on output stream.

Methods inherited from class fmrisc.ProgramExplorer.Semantics.GlobalSymbolBase

getLongName

Methods inherited from class fmrisc.ProgramExplorer.Semantics.SymbolBase

getName

Methods inherited from class java.lang.Object

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

Methods inherited from interface fmrisc.ProgramExplorer.Semantics.Symbol

getName

Method Detail

construct

public static FormulaSymbol construct(Identifier name,
                                      Formula formula,
                                      FormulaDefinition decl,
                                      TheorySymbol theory)

Construct formula symbol.

Parameters:

name - the name of the symbol.

formula - the formula identified by the symbol.

decl - the declaration introducing the symbol.

theory - the theory in which the symbol occurs (may be null)

Returns:

the symbol.

getFormula

public Formula getFormula()

Get formula.

Returns:

the formula.

getDeclaration

public FormulaDefinition getDeclaration()

Get declaration.

Specified by:

getDeclaration in interface Symbol

Overrides:

getDeclaration in class SymbolBase

Returns:

the declaration.

print

public void print(java.io.PrintWriter out)

Print symbol on output stream.

Parameters:

out - the output stream.