ICommand.Ideclare_datatype

All Superinterfaces:: ICommand, INode, IPos.IPosable

All Known Implementing Classes:: C_declare_datatype

Enclosing interface:: ICommand

public static interface ICommand.Ideclare_datatype extends ICommand

Interface for the SMT-LIB declare-datatype command.

Nested Class Summary

Nested classes/interfaces inherited from interface org.smtlib.ICommand
ICommand.Iassert, ICommand.Icheck_sat, ICommand.Icheck_sat_assuming, ICommand.Icomment, ICommand.Ideclare_const, ICommand.Ideclare_datatype, ICommand.Ideclare_datatypes, ICommand.Ideclare_fun, ICommand.Ideclare_sort, ICommand.Ideclare_sort_parameter, ICommand.Idefine_const, ICommand.Idefine_fun, ICommand.Idefine_fun_rec, ICommand.Idefine_funs_rec, ICommand.Idefine_sort, ICommand.Iecho, ICommand.Iexit, ICommand.IFactory, ICommand.IFinder, ICommand.Iget_assertions, ICommand.Iget_assignment, ICommand.Iget_info, ICommand.Iget_model, ICommand.Iget_option, ICommand.Iget_proof, ICommand.Iget_unsat_assumptions, ICommand.Iget_unsat_core, ICommand.Iget_value, ICommand.Ipop, ICommand.Ipush, ICommand.Ireset, ICommand.Ireset_assertions, ICommand.IScript, ICommand.Iset_info, ICommand.Iset_logic, ICommand.Iset_option
Method Summary

Modifier and Type

Method

Description

ISort.IDatatype

datatype()

Returns the datatype body.

IExpr.ISortDeclaration

sortDeclaration()

Returns the sort declaration (name and arity).

Methods inherited from interface org.smtlib.ICommand
commandName, execute

Methods inherited from interface org.smtlib.INode
accept

Methods inherited from interface org.smtlib.IPos.IPosable
pos, setPos

Method Details
- sortDeclaration
  
  IExpr.ISortDeclaration sortDeclaration()
  
  Returns the sort declaration (name and arity).
- datatype
  
  ISort.IDatatype datatype()
  
  Returns the datatype body.