SMTExpr.Datatype

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.SMTExpr.Datatype

All Implemented Interfaces:: INode, IPos.IPosable, ISort.IDatatype

Enclosing class:: SMTExpr

public static class SMTExpr.Datatype extends Pos.Printable implements ISort.IDatatype

Represents a datatype body: a list of constructors and (for parametric forms) a list of sort parameter symbols.

Field Summary

Fields

Modifier and Type

Field

Description

protected List<IExpr.IConstructor>

constructors

protected List<IExpr.ISymbol>

symbols

Fields inherited from class org.smtlib.impl.Pos.Posable
pos
Constructor Summary

Constructors

Constructor

Description

Datatype(List<IExpr.IConstructor> constructors, List<IExpr.ISymbol> symbols)

Creates a datatype body; symbols is non-null only for parametric (par) forms.
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); }

List<IExpr.IConstructor>

constructors()

List<IExpr.ISymbol>

symbols()

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

Methods inherited from interface org.smtlib.ISort.IDatatype
toString

Field Details
- constructors
  
  protected List<IExpr.IConstructor> constructors
- symbols
  
  protected List<IExpr.ISymbol> symbols
Constructor Details
- Datatype
  
  public Datatype(List<IExpr.IConstructor> constructors, List<IExpr.ISymbol> symbols)
  
  Creates a datatype body; symbols is non-null only for parametric (par) forms.
Method Details
- constructors
  
  public List<IExpr.IConstructor> constructors()
  
  Specified by:
  
  constructors in interface ISort.IDatatype
- symbols
  
  public List<IExpr.ISymbol> symbols()
  
  Specified by:
  
  symbols in interface ISort.IDatatype
- 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