Package org.smtlib.impl

Class Sort.ErrorDefinition

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.Sort.ErrorDefinition

All Implemented Interfaces:

INode, IPos.IPosable, ISort.IDefinition, ISort.IErrorDefinition

Enclosing class:

Sort

public static class Sort.ErrorDefinition
extends Pos.Printable
implements ISort.IErrorDefinition

A placeholder sort definition used when a sort declaration is ill-formed, to suppress cascading errors.

Field Summary

Fields

Modifier and Type	Field	Description
protected String	error
protected IExpr.IIdentifier	id

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

pos

Constructor Summary

Constructors

Constructor	Description
ErrorDefinition(IExpr.IIdentifier id, String error, IPos pos)	Creates an error placeholder for the given identifier, error message, and source position.

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); }
String	errorMessage()	The error message describing why the definition is ill-formed
IPos	errorPos()	The source position of the error
ISort	eval(List<ISort> sorts)	A new sort expression that results from applying the sort symbol to a list of sort expressions
IExpr.IIdentifier	identifier()	The identifier for the 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

equals, hashCode, 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

id

protected IExpr.IIdentifier id

error

protected String error

Constructor Details

ErrorDefinition

public ErrorDefinition(IExpr.IIdentifier id,
 String error,
 IPos pos)

Creates an error placeholder for the given identifier, error message, and source position.

Method Details

errorMessage

public String errorMessage()

Description copied from interface: ISort.IErrorDefinition

The error message describing why the definition is ill-formed

Specified by:

errorMessage in interface ISort.IErrorDefinition

errorPos

public IPos errorPos()

Description copied from interface: ISort.IErrorDefinition

The source position of the error

Specified by:

errorPos in interface ISort.IErrorDefinition

identifier

public IExpr.IIdentifier identifier()

Description copied from interface: ISort.IDefinition

The identifier for the sort symbol

Specified by:

identifier in interface ISort.IDefinition

eval

public ISort 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

intArity

public int intArity()

Description copied from interface: ISort.IDefinition

The arity of the symbol

Specified by:

intArity in interface ISort.IDefinition

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