ICommand.Idefine_fun

All Superinterfaces:: ICommand, INode, IPos.IPosable

All Known Subinterfaces:: ICommand.Idefine_const

All Known Implementing Classes:: C_define_const, C_define_fun, C_define_fun_rec

Enclosing interface:: ICommand

public static interface ICommand.Idefine_fun extends ICommand

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

IExpr

expression()

Returns the defining expression (body).

List<IExpr.IDeclaration>

parameters()

Returns the list of formal parameters.

ISort

resultSort()

Returns the result sort.

IExpr.ISymbol

symbol()

Returns the name of the function 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
- symbol
  
  IExpr.ISymbol symbol()
  
  Returns the name of the function being defined.
- parameters
  
  List<IExpr.IDeclaration> parameters()
  
  Returns the list of formal parameters.
- resultSort
  
  ISort resultSort()
  
  Returns the result sort.
- expression
  
  IExpr expression()
  
  Returns the defining expression (body).