Uses of Interface
org.smtlib.ICommand.Idefine_fun

Packages that use ICommand.Idefine_fun

Package	Description
org.smtlib	This package contains the main classes and abstract interfaces for this SMT-LIB tool; the tool provides a stand-alone SMT-LIB-compliant command-line application, an application that responds to SMT-LIB commands over a network port, and an SMT-LIB Java API.
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.
org.smtlib.impl	This package is an implementation of the interfaces defined in org.smtlib.
org.smtlib.sexpr	This package is a concrete implementation of a particular concrete syntax for the abstract SMT-LIB semantics.
org.smtlib.solvers	This package implements various instances of org.smtlib.ISolver, which are specific solvers that wrap and interact with various off-the-shelf SMT solvers currently available.

Uses of ICommand.Idefine_fun in org.smtlib

Subinterfaces of ICommand.Idefine_fun in org.smtlib

Modifier and Type	Interface	Description
static interface	ICommand.Idefine_const	Interface for the SMT-LIB define-const command.

Methods in org.smtlib that return ICommand.Idefine_fun

Modifier and Type	Method	Description
ICommand.Idefine_fun	ICommand.IFactory.define_fun(IExpr.ISymbol id, List<IExpr.IDeclaration> declarations, ISort resultSort, IExpr expression)	Creates a define-fun command object.

Methods in org.smtlib with parameters of type ICommand.Idefine_fun

Modifier and Type	Method	Description
IResponse	AbstractSolver.define_fun(ICommand.Idefine_fun cmd)
IResponse	ISolver.define_fun(ICommand.Idefine_fun cmd)	Defines a named function or constant; returns success or an SMT error response
T	IVisitor.TreeVisitor.visit(ICommand.Idefine_fun e)
default T	IVisitor.visit(ICommand.Idefine_fun e)

Uses of ICommand.Idefine_fun in org.smtlib.command

Classes in org.smtlib.command that implement ICommand.Idefine_fun

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	Implements the define-fun command
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.

Uses of ICommand.Idefine_fun in org.smtlib.impl

Methods in org.smtlib.impl that return ICommand.Idefine_fun

Modifier and Type	Method	Description
ICommand.Idefine_fun	Factory.define_fun(IExpr.ISymbol id, List<IExpr.IDeclaration> ps, ISort r, IExpr e)

Uses of ICommand.Idefine_fun in org.smtlib.sexpr

Methods in org.smtlib.sexpr with parameters of type ICommand.Idefine_fun

Modifier and Type	Method	Description
Void	Printer.visit(ICommand.Idefine_fun e)

Uses of ICommand.Idefine_fun in org.smtlib.solvers

Methods in org.smtlib.solvers with parameters of type ICommand.Idefine_fun

Modifier and Type	Method	Description
IResponse	Solver_simplify.define_fun(ICommand.Idefine_fun cmd)
IResponse	Solver_test.define_fun(ICommand.Idefine_fun cmd)
IResponse	Solver_z3_4_3.define_fun(ICommand.Idefine_fun cmd)