Package org.smtlib
Interface ICommand.Idefine_fun_rec
- All Superinterfaces:
ICommand,INode,IPos.IPosable
- All Known Implementing Classes:
C_define_fun_rec
- Enclosing interface:
ICommand
Interface for the SMT-LIB
define-fun-rec 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 TypeMethodDescriptionReturns the defining expression (body).Returns the list of formal parameters.Returns the result sort.symbol()Returns the name of the function being defined.Methods inherited from interface org.smtlib.ICommand
commandName, executeMethods 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).
-