ICommand.Idefine_sort

All Superinterfaces:: ICommand, INode, IPos.IPosable

All Known Implementing Classes:: C_define_sort

Enclosing interface:: ICommand

public static interface ICommand.Idefine_sort extends ICommand

Interface for the SMT-LIB define-sort 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

expression()

Returns the sort expression that is the definition.

List<ISort.IParameter>

parameters()

Returns the list of sort parameters.

IExpr.ISymbol

sortSymbol()

Returns the name of the sort being defined.

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
- sortSymbol
  
  IExpr.ISymbol sortSymbol()
  
  Returns the name of the sort being defined.
- parameters
  
  List<ISort.IParameter> parameters()
  
  Returns the list of sort parameters.
- expression
  
  ISort expression()
  
  Returns the sort expression that is the definition.