Uses of Class
org.smtlib.command.C_define_fun

Packages that use C_define_fun

Package	Description
org.smtlib.command	This package contains implementations of the SMT-LIB commands, implementing the interfaces defined in ICommand; these implementations are independent of the concrete syntax that might be used, except that each command object has methods that can parse or print representations of the command in the standard (or potentially other) concrete syntaxes.

Uses of C_define_fun in org.smtlib.command

Subclasses of C_define_fun in org.smtlib.command

Modifier and Type	Class	Description
class	C_define_const	Implements the define-const command: syntactic sugar for define-fun with no parameters
class	C_define_fun_rec	Implements the define-fun-rec command (recursive function definition); syntactically identical to define-fun (see C_define_fun), differing only in the dispatch target -- shares that class's fields, accessors, and constructor.

Methods in org.smtlib.command that return C_define_fun

Modifier and Type	Method	Description
static C_define_fun	C_define_fun.parse(Parser p)	Parses the command arguments and creates a command instance