Uses of Interface
org.smtlib.IExpr.ISortDeclaration

Packages that use IExpr.ISortDeclaration

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

Methods in org.smtlib that return IExpr.ISortDeclaration

Modifier and Type	Method	Description
IExpr.ISortDeclaration	ICommand.Ideclare_datatype.sortDeclaration()	Returns the sort declaration (name and arity).
IExpr.ISortDeclaration	IExpr.IFactory.sortDeclaration(IExpr.ISymbol symbol, IExpr.INumeral arity)	Creates a sort declaration (symbol + arity) for use in declare-datatype(s).

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

Modifier and Type	Method	Description
List<IExpr.ISortDeclaration>	ICommand.Ideclare_datatypes.sortDeclarations()	Returns the list of sort declarations (names and arities).

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

Modifier and Type	Method	Description
ICommand.Ideclare_datatype	ICommand.IFactory.declare_datatype(IExpr.ISortDeclaration sd, ISort.IDatatype d)	Creates a declare-datatype command object.
T	IVisitor.TreeVisitor.visit(IExpr.ISortDeclaration e)
T	IVisitor.visit(IExpr.ISortDeclaration e)
ISort	TypeChecker.visit(IExpr.ISortDeclaration e)

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

Modifier and Type	Method	Description
ICommand.Ideclare_datatypes	ICommand.IFactory.declare_datatypes(List<IExpr.ISortDeclaration> sds, List<ISort.IDatatype> dts)	Creates a declare-datatypes command object.
static List<IResponse>	TypeChecker.validateDatatypeNames(SymbolTable symTable, SMT.Configuration smtConfig, List<IExpr.ISortDeclaration> sortDecls, List<ISort.IDatatype> datatypes)	Checks that constructor and selector names introduced by a datatype group are not already defined (neither in the symbol table nor duplicated within the group).

Uses of IExpr.ISortDeclaration in org.smtlib.command

Fields in org.smtlib.command declared as IExpr.ISortDeclaration

Modifier and Type	Field	Description
protected IExpr.ISortDeclaration	C_declare_datatype.sortDeclaration	The sort declaration (symbol + arity derived from datatype body)

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

Modifier and Type	Field	Description
protected List<IExpr.ISortDeclaration>	C_declare_datatypes.sortDeclarations	The sort declarations: (symbol arity) pairs

Methods in org.smtlib.command that return IExpr.ISortDeclaration

Modifier and Type	Method	Description
IExpr.ISortDeclaration	C_declare_datatype.sortDeclaration()

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

Modifier and Type	Method	Description
List<IExpr.ISortDeclaration>	C_declare_datatypes.sortDeclarations()

Constructors in org.smtlib.command with parameters of type IExpr.ISortDeclaration

Modifier	Constructor	Description
	C_declare_datatype(IExpr.ISortDeclaration sortDeclaration, ISort.IDatatype d)	Constructs a new command object

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

Modifier	Constructor	Description
	C_declare_datatypes(List<IExpr.ISortDeclaration> sortDeclarations, List<ISort.IDatatype> datatypes)	Constructs a new command object

Uses of IExpr.ISortDeclaration in org.smtlib.impl

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

Modifier and Type	Class	Description
static class	SMTExpr.SortDeclaration	Represents a sort declaration (symbol and arity) used in declare-datatype and declare-datatypes.

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

Modifier and Type	Method	Description
IExpr.ISortDeclaration	Factory.sortDeclaration(IExpr.ISymbol symbol, IExpr.INumeral arity)

Methods in org.smtlib.impl with parameters of type IExpr.ISortDeclaration

Modifier and Type	Method	Description
ICommand.Ideclare_datatype	Factory.declare_datatype(IExpr.ISortDeclaration sd, ISort.IDatatype d)

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

Modifier and Type	Method	Description
ICommand.Ideclare_datatypes	Factory.declare_datatypes(List<IExpr.ISortDeclaration> sds, List<ISort.IDatatype> dts)

Uses of IExpr.ISortDeclaration in org.smtlib.sexpr

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

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

Uses of IExpr.ISortDeclaration in org.smtlib.solvers

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

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