Public Member Functions

void validate (const std::vector< smt_termt > &arguments) const

Private Attributes

A function generated from a command.

Used for validating function application term arguments.

Definition at line 146 of file smt_commands.h.

smt_command_functiont::smt_command_functiont ( const smt_declare_function_commandt & function_declaration )

explicit

Definition at line 204 of file smt_commands.cpp.

smt_command_functiont::smt_command_functiont ( const smt_define_function_commandt & function_definition )

explicit

Definition at line 213 of file smt_commands.cpp.

irep_idt smt_command_functiont::identifier ( ) const

Definition at line 224 of file smt_commands.cpp.

smt_sortt smt_command_functiont::return_sort ( const std::vector< smt_termt > & arguments ) const

Definition at line 229 of file smt_commands.cpp.

void smt_command_functiont::validate ( const std::vector< smt_termt > & arguments ) const

Definition at line 235 of file smt_commands.cpp.

smt_identifier_termt smt_command_functiont::_identifier

private

Definition at line 150 of file smt_commands.h.

std::vector<smt_sortt> smt_command_functiont::parameter_sorts

private

Definition at line 149 of file smt_commands.h.

The documentation for this class was generated from the following files: