SMTExpr.FunctionDeclaration

java.lang.Object

org.smtlib.impl.Pos.Posable

org.smtlib.impl.Pos.Printable

org.smtlib.impl.SMTExpr.FunctionDeclaration

All Implemented Interfaces:: IExpr.IFunctionDeclaration, INode, IPos.IPosable

Enclosing class:: SMTExpr

public static class SMTExpr.FunctionDeclaration extends Pos.Printable implements IExpr.IFunctionDeclaration

Represents a function declaration header (name, sorted parameters, result sort), used in define-funs-rec.

Field Summary

Fields

Modifier and Type

Field

Description

protected List<IExpr.IDeclaration>

parameters

protected ISort

sort

protected IExpr.ISymbol

symbol

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

Constructors

Constructor

Description

FunctionDeclaration(IExpr.ISymbol symbol, List<IExpr.IDeclaration> parameters, ISort sort)

Creates a function declaration with the given name, parameter declarations, and result sort.
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.IDeclaration>

parameters()

ISort

sort()

IExpr.ISymbol

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
- symbol
  
  protected IExpr.ISymbol symbol
- parameters
  
  protected List<IExpr.IDeclaration> parameters
- sort
  
  protected ISort sort
Constructor Details
- FunctionDeclaration
  
  public FunctionDeclaration(IExpr.ISymbol symbol, List<IExpr.IDeclaration> parameters, ISort sort)
  
  Creates a function declaration with the given name, parameter declarations, and result sort.
Method Details
- symbol
  
  public IExpr.ISymbol symbol()
  
  Specified by:
  
  symbol in interface IExpr.IFunctionDeclaration
- parameters
  
  public List<IExpr.IDeclaration> parameters()
  
  Specified by:
  
  parameters in interface IExpr.IFunctionDeclaration
- sort
  
  public ISort sort()
  
  Specified by:
  
  sort in interface IExpr.IFunctionDeclaration
- 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