hlt.osf.base

Class SortExpression

java.lang.Object

hlt.osf.base.OsfExpression

hlt.osf.base.SortExpression

All Implemented Interfaces:

Contextable

Direct Known Subclasses:

BinarySortExpression, DisjunctiveSortExpression, NotSortExpression, SymbolSortExpression

public abstract class SortExpression
extends OsfExpression

This is the class of all OSF sort expressions. It will always evaluate as a code, which then can be retrieved as an explicit sort or a disjunctive sort.

Constructor Summary

Constructors

Constructor and Description
SortExpression()

Method Summary

Methods

Modifier and Type	Method and Description
boolean	isAnd()
boolean	isButnot()
boolean	isDisjunction()
boolean	isNot()
boolean	isOr()
boolean	isParenthesized() This returns whether or not this expression is parenthesized.
boolean	isSymbol()
java.lang.String	maxLowerBound() Returns the string form of this sort's (possibly disjunctive) maximal lower bound after it has been evaluated in its context.
SortExpression	setParenthesized(boolean value) This sets whether or not this expression is to be parenthesized.
java.lang.String	toString()
abstract byte	type() This returns the type of Boolean expression this sort expression is; one of: Context.SYM() if this is a sort symbol; Context.DIS() if this is a disjunctive sort; Context.NOT() if this is a negated sort expression; Context.AND() if this is a sort-expression conjunction; Context.OR () if this is a sort-expression disjunction; Context.BNT() if this is a sort-expression complementation.
BitCode	value() Returns this sort expression's bit code in its context.

Methods inherited from class hlt.osf.base.OsfExpression

context, displayForm, setContext

Methods inherited from class java.lang.Object

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

Constructor Detail

SortExpression

public SortExpression()

Method Detail

type

public abstract byte type()

This returns the type of Boolean expression this sort expression is; one of:

• Context.SYM() if this is a sort symbol;
• Context.DIS() if this is a disjunctive sort;
• Context.NOT() if this is a negated sort expression;
• Context.AND() if this is a sort-expression conjunction;
• Context.OR () if this is a sort-expression disjunction;
• Context.BNT() if this is a sort-expression complementation.

isSymbol

public boolean isSymbol()

isDisjunction

public boolean isDisjunction()

isNot

public boolean isNot()

isAnd

public boolean isAnd()

isOr

public boolean isOr()

isButnot

public boolean isButnot()

value

public BitCode value()

Returns this sort expression's bit code in its context.

maxLowerBound

public java.lang.String maxLowerBound()

Returns the string form of this sort's (possibly disjunctive) maximal lower bound after it has been evaluated in its context.

isParenthesized

public boolean isParenthesized()

This returns whether or not this expression is parenthesized. This is used for rendering its original string form.

setParenthesized

public SortExpression setParenthesized(boolean value)

This sets whether or not this expression is to be parenthesized. This is used for rendering its original string form.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object