Package org.smtlib

Interface ISort.IFactory

All Known Implementing Classes:

Factory

Enclosing interface:

ISort

public static interface ISort.IFactory

The interface for a Sort-creating factory.

Method Summary

Modifier and Type	Method	Description
ISort.IApplication	Bool()	Returns the Bool sort.
ISort.IErrorDefinition	createErrorDefinition(IExpr.IIdentifier id, String errorMessage, IPos pos)	Creates an error-placeholder definition (suppresses cascading errors).
ISort.IFcnSort	createFcnSort(ISort[] args, ISort result)	Creates a function sort.
ISort.IAbbreviation	createSortAbbreviation(IExpr.IIdentifier identifier, List<ISort.IParameter> params, ISort sortExpr)	Creates a new sort abbreviation.
ISort.IApplication	createSortExpression(IExpr.IIdentifier sortFamily, List<ISort> exprs)	Creates a sort expression, applying a family to a list of sort arguments; the arity of the identifier in the applicable symbol table must match the number of sort arguments.
ISort.IApplication	createSortExpression(IExpr.IIdentifier sortFamily, ISort... exprs)	Creates a sort expression, applying a family to a list of sort arguments; the arity of the identifier in the applicable symbol table must match the number of sort arguments.
ISort.IFamily	createSortFamily(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).
ISort.IParameter	createSortParameter(IExpr.ISymbol symbol)	Creates a parameter for a parameterized sort abbreviation.

Method Details

createSortFamily

ISort.IFamily createSortFamily(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).

createSortParameter

ISort.IParameter createSortParameter(IExpr.ISymbol symbol)

Creates a parameter for a parameterized sort abbreviation.

createSortExpression

ISort.IApplication createSortExpression(IExpr.IIdentifier sortFamily,
 ISort... exprs)

Creates a sort expression, applying a family to a list of sort arguments; the arity of the identifier in the applicable symbol table must match the number of sort arguments.

createSortExpression

ISort.IApplication createSortExpression(IExpr.IIdentifier sortFamily,
 List<ISort> exprs)

Creates a sort expression, applying a family to a list of sort arguments; the arity of the identifier in the applicable symbol table must match the number of sort arguments.

createSortAbbreviation

ISort.IAbbreviation createSortAbbreviation(IExpr.IIdentifier identifier,
 List<ISort.IParameter> params,
 ISort sortExpr)

Creates a new sort abbreviation.

createFcnSort

ISort.IFcnSort createFcnSort(ISort[] args,
 ISort result)

Creates a function sort.

createErrorDefinition

ISort.IErrorDefinition createErrorDefinition(IExpr.IIdentifier id,
 String errorMessage,
 IPos pos)

Creates an error-placeholder definition (suppresses cascading errors).

Bool

ISort.IApplication Bool()

Returns the Bool sort.