ICommand.Ideclare_datatypes

All Superinterfaces:: ICommand, INode, IPos.IPosable

All Known Implementing Classes:: C_declare_datatypes

Enclosing interface:: ICommand

public static interface ICommand.Ideclare_datatypes extends ICommand

Interface for the SMT-LIB declare-datatypes 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

List<ISort.IDatatype>

datatypes()

Returns the list of datatype bodies, parallel to sortDeclarations().

List<IExpr.ISortDeclaration>

sortDeclarations()

Returns the list of sort declarations (names and arities).

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
- sortDeclarations
  
  List<IExpr.ISortDeclaration> sortDeclarations()
  
  Returns the list of sort declarations (names and arities).
- datatypes
  
  List<ISort.IDatatype> datatypes()
  
  Returns the list of datatype bodies, parallel to sortDeclarations().