Package org.smtlib

Interface ICommand.Ideclare_fun

All Superinterfaces:

ICommand, INode, IPos.IPosable

All Known Implementing Classes:

C_declare_const, C_declare_fun

Enclosing interface:

ICommand

public static interface ICommand.Ideclare_fun
extends ICommand

Interface for the SMT-LIB declare-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
List<ISort>	argSorts()	Returns the list of argument sorts.
default List<IExpr.IAttribute<?>>	attributes()	Returns any trailing attributes given after the result sort -- an experimental, non-standard extension (SMT-LIB's declare-fun has no attribute* production); accepting one at all is unconditional at parse time, but the command is rejected at type-checking time unless --relax is set.
default List<ISort.IParameter>	parameters()	Returns the par-polymorphic type parameters, for the experimental, non-standard "(declare-fun par (param+) (name sort+ attribute*))" form -- mirrors exactly the par_fun_symbol_decl shape a theory's own :funs entry uses.
ISort	resultSort()	Returns the result sort.
IExpr.ISymbol	symbol()	Returns the name of the function being declared.

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 declared.

argSorts

List<ISort> argSorts()

Returns the list of argument sorts.

resultSort

ISort resultSort()

Returns the result sort.

attributes

default List<IExpr.IAttribute<?>> attributes()

Returns any trailing attributes given after the result sort -- an experimental, non-standard extension (SMT-LIB's declare-fun has no attribute* production); accepting one at all is unconditional at parse time, but the command is rejected at type-checking time unless --relax is set. Never null; empty if none were given -- unlike parameters(), null-vs-empty has no real distinction to encode here (the concrete syntax has no way to write an explicit-but-empty attribute clause).

parameters

default List<ISort.IParameter> parameters()

Returns the par-polymorphic type parameters, for the experimental, non-standard "(declare-fun par (param+) (name sort+ attribute*))" form -- mirrors exactly the par_fun_symbol_decl shape a theory's own :funs entry uses. Accepting this form at all is unconditional at parse time, but the command is rejected at type-checking time unless --relax is set. Null for an ordinary (non-par) declare-fun -- this is load-bearing, not just an empty-list stand-in: Solver_test.declare_fun(org.smtlib.ICommand.Ideclare_fun) branches on null-vs-non-null directly to decide whether --relax is required, and a par-form's parameter list is never actually empty in practice (the grammar requires param+), so there is no "empty par-form" state this could be confused with.