Uses of Interface
org.smtlib.IExpr.IDeclaration

Packages that use IExpr.IDeclaration

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

Methods in org.smtlib that return IExpr.IDeclaration

Modifier and Type	Method	Description
IExpr.IDeclaration	IExpr.IFactory.declaration(IExpr.ISymbol symbol, ISort sort)	Creates a parameter declaration.
IExpr.IDeclaration	IParser.parseDeclaration()	Parses a declaration "(id sort)", returning null with error messages if an error occurs

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

Modifier and Type	Method	Description
List<IExpr.IDeclaration>	ICommand.Idefine_fun_rec.parameters()	Returns the list of formal parameters.
List<IExpr.IDeclaration>	ICommand.Idefine_fun.parameters()	Returns the list of formal parameters.
List<IExpr.IDeclaration>	IExpr.IExists.parameters()
List<IExpr.IDeclaration>	IExpr.IForall.parameters()
List<IExpr.IDeclaration>	IExpr.IFunctionDeclaration.parameters()
List<IExpr.IDeclaration>	IExpr.ILambda.parameters()
List<IExpr.IDeclaration>	IParser.parseDeclarations()	Parses a parenthesized sequence of IDeclaration items, returning null with error messages if an error occurs

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

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

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

Modifier and Type	Method	Description
static List<IResponse>	TypeChecker.checkFcn(SymbolTable symTable, IExpr.IIdentifier id, List<IExpr.IDeclaration> params, ISort result, IExpr expr)
static List<IResponse>	TypeChecker.checkFcnRec(SymbolTable symTable, boolean global, IExpr.ISymbol id, List<IExpr.IDeclaration> params, ISort result, IExpr expr)	Type-checks a define-fun-rec command: verifies the symbol is new, validates sorts, pre-adds the function to the symbol table so the body may call it recursively, then checks the body expression.
ICommand.Idefine_fun	ICommand.IFactory.define_fun(IExpr.ISymbol id, List<IExpr.IDeclaration> declarations, ISort resultSort, IExpr expression)	Creates a define-fun command object.
ICommand.Idefine_fun_rec	ICommand.IFactory.define_fun_rec(IExpr.ISymbol id, List<IExpr.IDeclaration> declarations, ISort resultSort, IExpr expression)	Creates a define-fun-rec command object.
IExpr.IExists	IExpr.IFactory.exists(List<IExpr.IDeclaration> params, IExpr e)	Creates an Exists expression.
IExpr.IExists	IExpr.IFactory.exists(List<IExpr.IDeclaration> params, IExpr e, List<IExpr> patterns)	Creates an Exists expression with trigger patterns: each element of patterns is a separate single-term pattern, emitted as :pattern (p).
IExpr.IForall	IExpr.IFactory.forall(List<IExpr.IDeclaration> params, IExpr e)	Creates a Forall expression.
IExpr.IForall	IExpr.IFactory.forall(List<IExpr.IDeclaration> params, IExpr e, List<IExpr> patterns)	Creates a Forall expression with trigger patterns: each element of patterns is a separate single-term pattern, emitted as :pattern (p).
IExpr.IFunctionDeclaration	IExpr.IFactory.functionDeclaration(IExpr.ISymbol symbol, List<IExpr.IDeclaration> parameters, ISort sort)	Creates a function declaration (used in define-funs-rec).
IExpr.ILambda	IExpr.IFactory.lambda(List<IExpr.IDeclaration> params, IExpr e)	Creates a Lambda expression (SMT-LIB 2.7ff, HO-Core theory).

Uses of IExpr.IDeclaration in org.smtlib.command

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

Modifier and Type	Field	Description
protected List<IExpr.IDeclaration>	C_define_fun.args	The sorts of the arguments of the function being defined

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

Modifier and Type	Method	Description
List<IExpr.IDeclaration>	C_define_fun.parameters()	The sorts of the arguments of the function being defined

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

Modifier	Constructor	Description
	C_define_fun(IExpr.ISymbol id, List<IExpr.IDeclaration> declarations, ISort resultSort, IExpr expr)	Constructs a command instance
	C_define_fun_rec(IExpr.ISymbol id, List<IExpr.IDeclaration> declarations, ISort resultSort, IExpr expr)	Constructs a command instance

Uses of IExpr.IDeclaration in org.smtlib.impl

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

Modifier and Type	Class	Description
static class	SMTExpr.Declaration	Represents a sorted variable declaration (parameter name and its sort), used in forall/exists/define-fun.

Fields in org.smtlib.impl with type parameters of type IExpr.IDeclaration

Modifier and Type	Field	Description
protected List<IExpr.IDeclaration>	SMTExpr.Exists.parameters
protected List<IExpr.IDeclaration>	SMTExpr.Forall.parameters
protected List<IExpr.IDeclaration>	SMTExpr.FunctionDeclaration.parameters
protected List<IExpr.IDeclaration>	SMTExpr.Lambda.parameters

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

Modifier and Type	Method	Description
IExpr.IDeclaration	Factory.declaration(IExpr.ISymbol symbol, ISort sort)

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

Modifier and Type	Method	Description
List<IExpr.IDeclaration>	SMTExpr.Exists.parameters()
List<IExpr.IDeclaration>	SMTExpr.Forall.parameters()
List<IExpr.IDeclaration>	SMTExpr.FunctionDeclaration.parameters()
List<IExpr.IDeclaration>	SMTExpr.Lambda.parameters()

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

Modifier and Type	Method	Description
ICommand.Idefine_fun	Factory.define_fun(IExpr.ISymbol id, List<IExpr.IDeclaration> ps, ISort r, IExpr e)
ICommand.Idefine_fun_rec	Factory.define_fun_rec(IExpr.ISymbol id, List<IExpr.IDeclaration> ps, ISort r, IExpr e)
IExpr.IExists	Factory.exists(List<IExpr.IDeclaration> params, IExpr e)
IExpr.IExists	Factory.exists(List<IExpr.IDeclaration> params, IExpr e, List<IExpr> patterns)
IExpr.IForall	Factory.forall(List<IExpr.IDeclaration> params, IExpr e)
IExpr.IForall	Factory.forall(List<IExpr.IDeclaration> params, IExpr e, List<IExpr> patterns)
IExpr.IFunctionDeclaration	Factory.functionDeclaration(IExpr.ISymbol symbol, List<IExpr.IDeclaration> parameters, ISort sort)
IExpr.ILambda	Factory.lambda(List<IExpr.IDeclaration> params, IExpr e)

Constructor parameters in org.smtlib.impl with type arguments of type IExpr.IDeclaration

Modifier	Constructor	Description
	Exists(List<IExpr.IDeclaration> parameters, IExpr expr)	Creates an exists expression with the given bound variable declarations and body.
	Forall(List<IExpr.IDeclaration> parameters, IExpr expr)	Creates a forall expression with the given bound variable declarations and body.
	FunctionDeclaration(IExpr.ISymbol symbol, List<IExpr.IDeclaration> parameters, ISort sort)	Creates a function declaration with the given name, parameter declarations, and result sort.
	Lambda(List<IExpr.IDeclaration> parameters, IExpr expr)	Creates a lambda expression with the given bound variable declarations and body.

Uses of IExpr.IDeclaration in org.smtlib.sexpr

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

Modifier and Type	Method	Description
IExpr.IDeclaration	Parser.parseDeclaration()	Parses a declaration "(id sort)", returning null with error messages if an error occurs

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

Modifier and Type	Method	Description
List<IExpr.IDeclaration>	Parser.parseDeclarations()	Parses a parenthesized sequence of IDeclaration items

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

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

Uses of IExpr.IDeclaration in org.smtlib.solvers

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

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