A function generated from a command. More...

#include <smt_commands.h>

Collaboration diagram for smt_command_functiont:

Public Member Functions
	smt_command_functiont (const smt_declare_function_commandt &function_declaration)

	smt_command_functiont (const smt_define_function_commandt &function_definition)

irep_idt	identifier () const

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

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

Private Attributes
std::vector< smt_sortt >	parameter_sorts

smt_identifier_termt	_identifier

Detailed Description

A function generated from a command.

Used for validating function application term arguments.

Definition at line 145 of file smt_commands.h.

Constructor & Destructor Documentation

◆ smt_command_functiont() [1/2]

smt_command_functiont::smt_command_functiont ( const smt_declare_function_commandt & function_declaration )

explicit

Definition at line 202 of file smt_commands.cpp.

◆ smt_command_functiont() [2/2]

smt_command_functiont::smt_command_functiont ( const smt_define_function_commandt & function_definition )

explicit

Definition at line 211 of file smt_commands.cpp.

Member Function Documentation

◆ identifier()

irep_idt smt_command_functiont::identifier ( ) const

Definition at line 222 of file smt_commands.cpp.

◆ return_sort()

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

Definition at line 227 of file smt_commands.cpp.

◆ validate()

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

Definition at line 233 of file smt_commands.cpp.

Member Data Documentation

◆ _identifier

smt_identifier_termt smt_command_functiont::_identifier

private

Definition at line 149 of file smt_commands.h.

◆ parameter_sorts

std::vector<smt_sortt> smt_command_functiont::parameter_sorts