Package org.smtlib.impl

Class Sort.Family

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.Sort.Family

All Implemented Interfaces:

INode, IPos.IPosable, ISort.IDefinition, ISort.IFamily

Enclosing class:

Sort

public static class Sort.Family
extends Pos.Printable
implements ISort.IFamily

Represents a new sort symbol, with a given identifier and arity

Field Summary

Fields

Modifier and Type	Field	Description
protected IExpr.INumeral	arity
protected List<IExpr.IAttribute<?>>	attributes
protected IExpr.IIdentifier	identifier

Fields inherited from class org.smtlib.impl.Pos.Posable

pos

Constructor Summary

Constructors

Constructor	Description
Family(IExpr.IIdentifier identifier, IExpr.INumeral arity, List<IExpr.IAttribute<?>> attributes)	Creates a sort family with the given identifier, arity, and attributes (null or empty if none).

Method Summary

Modifier and Type	Method	Description
<T> T	accept(IVisitor<T> v)	The accept method corresponding to IVisitor, to be implemented in each subclass as { return v.visit(this); }
IExpr.INumeral	arity()	The arity of the sort symbol
List<IExpr.IAttribute<?>>	attributes()	Any attributes declared on this sort symbol (e.g.
boolean	equals(Object o)
ISort.IApplication	eval(List<ISort> sorts)	A new sort expression that results from applying the sort symbol to a list of sort expressions
int	hashCode()
IExpr.IIdentifier	identifier()	The unique identifier for this sort symbol
int	intArity()	The arity of the symbol

Methods inherited from class org.smtlib.impl.Pos.Printable

toString

Methods inherited from class org.smtlib.impl.Pos.Posable

pos, setPos

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface org.smtlib.IPos.IPosable

pos, setPos

Field Details

identifier

protected IExpr.IIdentifier identifier

arity

protected IExpr.INumeral arity

attributes

protected List<IExpr.IAttribute<?>> attributes

Constructor Details

Family

public Family(IExpr.IIdentifier identifier,
 IExpr.INumeral arity,
 List<IExpr.IAttribute<?>> attributes)

Creates a sort family with the given identifier, arity, and attributes (null or empty if none).

Method Details

identifier

public IExpr.IIdentifier identifier()

Description copied from interface: ISort.IFamily

The unique identifier for this sort symbol

Specified by:

identifier in interface ISort.IDefinition

Specified by:

identifier in interface ISort.IFamily

arity

public IExpr.INumeral arity()

Description copied from interface: ISort.IFamily

The arity of the sort symbol

Specified by:

arity in interface ISort.IFamily

attributes

public List<IExpr.IAttribute<?>> attributes()

Description copied from interface: ISort.IFamily

Any attributes declared on this sort symbol (e.g. :right-assoc, as on -> in HO-Core.smt2); empty (never null) if there are none.

Specified by:

attributes in interface ISort.IFamily

intArity

public int intArity()

Description copied from interface: ISort.IDefinition

The arity of the symbol

Specified by:

intArity in interface ISort.IDefinition

eval

public ISort.IApplication eval(List<ISort> sorts)

Description copied from interface: ISort.IDefinition

A new sort expression that results from applying the sort symbol to a list of sort expressions

Specified by:

eval in interface ISort.IDefinition

equals

public boolean equals(Object o)

Overrides:

equals in class Pos.Posable

hashCode

public int hashCode()

Overrides:

hashCode in class Pos.Posable

accept

public <T> T accept(IVisitor<T> v)
             throws IVisitor.VisitorException

Description copied from interface: INode

The accept method corresponding to IVisitor, to be implemented in each subclass as { return v.visit(this); }

Specified by:

accept in interface INode

Type Parameters:

T - the return type desired from the visit methods

Parameters:

v - the visitor class

Returns:

the value returned by the visit method

Throws:

IVisitor.VisitorException