Uses of Interface
org.smtlib.IExpr.IFunctionDeclaration

Packages that use IExpr.IFunctionDeclaration

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 IExpr.IFunctionDeclaration in org.smtlib

Methods in org.smtlib that return IExpr.IFunctionDeclaration

Modifier and Type	Method	Description
IExpr.IFunctionDeclaration	IExpr.IFactory.functionDeclaration(IExpr.ISymbol symbol, List<IExpr.IDeclaration> parameters, ISort sort)	Creates a function declaration (used in define-funs-rec).
IExpr.IFunctionDeclaration	IParser.parseFunctionDeclaration()	Parses a function declaration "(symbol (sorted_var*) sort)" used in define-funs-rec

Methods in org.smtlib that return types with arguments of type IExpr.IFunctionDeclaration

Modifier and Type	Method	Description
List<IExpr.IFunctionDeclaration>	ICommand.Idefine_funs_rec.declarations()	Returns the list of function declarations.

Methods in org.smtlib with parameters of type IExpr.IFunctionDeclaration

Modifier and Type	Method	Description
T	IVisitor.TreeVisitor.visit(IExpr.IFunctionDeclaration e)
T	IVisitor.visit(IExpr.IFunctionDeclaration e)
ISort	TypeChecker.visit(IExpr.IFunctionDeclaration e)

Method parameters in org.smtlib with type arguments of type IExpr.IFunctionDeclaration

Modifier and Type	Method	Description
static List<IResponse>	TypeChecker.checkFcnsRec(SymbolTable symTable, boolean global, List<IExpr.IFunctionDeclaration> decls, List<IExpr> bodies)	Type-checks a define-funs-rec command: for each declaration verifies the symbol is new and sorts are valid, pre-adds all functions to the symbol table for mutual recursion, then checks each body expression.
ICommand.Idefine_funs_rec	ICommand.IFactory.define_funs_rec(List<IExpr.IFunctionDeclaration> declarations, List<IExpr> bodies)	Creates a define-funs-rec command object.

Uses of IExpr.IFunctionDeclaration in org.smtlib.command

Fields in org.smtlib.command with type parameters of type IExpr.IFunctionDeclaration

Modifier and Type	Field	Description
protected List<IExpr.IFunctionDeclaration>	C_define_funs_rec.declarations	The list of function declarations (name, parameters, result sort)

Methods in org.smtlib.command that return types with arguments of type IExpr.IFunctionDeclaration

Modifier and Type	Method	Description
List<IExpr.IFunctionDeclaration>	C_define_funs_rec.declarations()

Constructor parameters in org.smtlib.command with type arguments of type IExpr.IFunctionDeclaration

Modifier	Constructor	Description
	C_define_funs_rec(List<IExpr.IFunctionDeclaration> declarations, List<IExpr> bodies)	Constructs a command instance

Uses of IExpr.IFunctionDeclaration in org.smtlib.impl

Classes in org.smtlib.impl that implement IExpr.IFunctionDeclaration

Modifier and Type	Class	Description
static class	SMTExpr.FunctionDeclaration	Represents a function declaration header (name, sorted parameters, result sort), used in define-funs-rec.

Methods in org.smtlib.impl that return IExpr.IFunctionDeclaration

Modifier and Type	Method	Description
IExpr.IFunctionDeclaration	Factory.functionDeclaration(IExpr.ISymbol symbol, List<IExpr.IDeclaration> parameters, ISort sort)

Method parameters in org.smtlib.impl with type arguments of type IExpr.IFunctionDeclaration

Modifier and Type	Method	Description
ICommand.Idefine_funs_rec	Factory.define_funs_rec(List<IExpr.IFunctionDeclaration> ds, List<IExpr> bs)

Uses of IExpr.IFunctionDeclaration in org.smtlib.sexpr

Methods in org.smtlib.sexpr that return IExpr.IFunctionDeclaration

Modifier and Type	Method	Description
IExpr.IFunctionDeclaration	Parser.parseFunctionDeclaration()	Parses a function declaration "( symbol ( sorted_var* ) sort )" used in define-funs-rec

Methods in org.smtlib.sexpr with parameters of type IExpr.IFunctionDeclaration

Modifier and Type	Method	Description
Void	Printer.visit(IExpr.IFunctionDeclaration e)

Uses of IExpr.IFunctionDeclaration in org.smtlib.solvers

Methods in org.smtlib.solvers with parameters of type IExpr.IFunctionDeclaration

Modifier and Type	Method	Description
String	Solver_simplify.Translator.visit(IExpr.IFunctionDeclaration e)