Uses of Interface
org.smtlib.ISort

Packages that use ISort

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.logic	This package contains implementations of classes that implement the constraints of individual logics.
org.smtlib.sexpr	This package is a concrete implementation of a particular concrete syntax for the abstract SMT-LIB semantics.

Uses of ISort in org.smtlib

Subinterfaces of ISort in org.smtlib

Modifier and Type	Interface	Description
static interface	ISort.IApplication	The interface for a Sort expression that consists of either an arity 0 sort symbol or a positive-arity symbol with the appropriate number of arguments.
static interface	ISort.IFcnSort	An interface to represent the Sort of a function; this is not something that can be written as a sort expression in SMT-LIB, but it is convenient to be able to represent the sorts of function ids uniformly with the sorts of other ids.
static interface	ISort.IParameter	The interface for a sort parameter, as used in sort abbreviations (including in the defining expression).

Fields in org.smtlib declared as ISort

Modifier and Type	Field	Description
ISort	TypeChecker.Variable.sort

Methods in org.smtlib that return ISort

Modifier and Type	Method	Description
ISort[]	ISort.IFcnSort.argSorts()
ISort	Utils.asSort(ISexpr sexpr, SymbolTable symtab)
ISort	ISort.IDefinition.eval(List<ISort> sorts)	A new sort expression that results from applying the sort symbol to a list of sort expressions
ISort	ISort.expand()	Expands all abbreviations
ISort	ISort.IApplication.expand()	Expands any head abbreviations, if any; requires definition() to be defined
ISort	ICommand.Idefine_sort.expression()	Returns the sort expression that is the definition.
ISort	SymbolTable.lookup(IExpr.IIdentifier name, List<ISort> argSorts, ISort resultSort, StringBuilder reason)	Lookup a Symbol with the given name and argument Sorts and result Sort.
ISort	ISort.IApplication.param(int i)	Returns the ith parameter
ISort	IParser.parseSort(List<ISort.IParameter> parameters)	Parses a sort, returning null with error messages if a valid sort is not in the next parser tokens.
ISort	IExpr.IAsIdentifier.qualifier()	The Sort qualifier
ISort	ICommand.Ideclare_const.resultSort()	Returns the sort of the constant being declared.
ISort	ICommand.Ideclare_fun.resultSort()	Returns the result sort.
ISort	ICommand.Idefine_fun_rec.resultSort()	Returns the result sort.
ISort	ICommand.Idefine_fun.resultSort()	Returns the result sort.
ISort	ISort.IFcnSort.resultSort()
ISort	TypeChecker.save(IExpr e, ISort s)
ISort	IExpr.IDeclaration.sort()
ISort	IExpr.IFunctionDeclaration.sort()
ISort	IExpr.ISelector.sort()
ISort	IExpr.sort()	The sort computed for this expression by the type checker, or null if not yet (or never) computed.
ISort	ISort.IAbbreviation.sortExpression()	The sort expression that the abbreviation represents, presumably using the given parameters
ISort	ISort.substitute(Map<ISort.IParameter,ISort> map)	Returns a new sort with any parameters substituted
ISort	TypeChecker.visit(ICommand e)
ISort	TypeChecker.visit(ICommand.IScript e)
ISort	TypeChecker.visit(IExpr.IAsIdentifier e)
ISort	TypeChecker.visit(IExpr.IAttribute<?> e)
ISort	TypeChecker.visit(IExpr.IAttributedExpr e)
ISort	TypeChecker.visit(IExpr.IBinaryLiteral e)
ISort	TypeChecker.visit(IExpr.IBinding e)
ISort	TypeChecker.visit(IExpr.IConstructor e)
ISort	TypeChecker.visit(IExpr.IDecimal e)
ISort	TypeChecker.visit(IExpr.IDeclaration e)
ISort	TypeChecker.visit(IExpr.IError e)
ISort	TypeChecker.visit(IExpr.IExists e)
ISort	TypeChecker.visit(IExpr.IFcnExpr e)
ISort	TypeChecker.visit(IExpr.IForall e)
ISort	TypeChecker.visit(IExpr.IFunctionDeclaration e)
ISort	TypeChecker.visit(IExpr.IHexLiteral e)
ISort	TypeChecker.visit(IExpr.IKeyword e)
ISort	TypeChecker.visit(IExpr.ILambda e)	Type-checks a lambda expression: (lambda (sorted_var+) term), SMT-LIB 2.7ff (the optional HO-Core theory -- see SMT/logics/HO-Core.smt2).
ISort	TypeChecker.visit(IExpr.ILet e)
ISort	TypeChecker.visit(IExpr.IMatch e)
ISort	TypeChecker.visit(IExpr.IMatchCase e)
ISort	TypeChecker.visit(IExpr.INumeral e)
ISort	TypeChecker.visit(IExpr.IParameterizedIdentifier e)
ISort	TypeChecker.visit(IExpr.IPattern e)
ISort	TypeChecker.visit(IExpr.ISelector e)
ISort	TypeChecker.visit(IExpr.ISortDeclaration e)
ISort	TypeChecker.visit(IExpr.IStringLiteral e)
ISort	TypeChecker.visit(IExpr.ISymbol e)
ISort	TypeChecker.visit(ILogic s)
ISort	TypeChecker.visit(IResponse e)
ISort	TypeChecker.visit(IResponse.IAssertionsResponse e)
ISort	TypeChecker.visit(IResponse.IAssignmentResponse e)
ISort	TypeChecker.visit(IResponse.IAttributeList e)
ISort	TypeChecker.visit(IResponse.IError e)
ISort	TypeChecker.visit(IResponse.IProofResponse e)
ISort	TypeChecker.visit(IResponse.IUnsatAssumptionsResponse e)
ISort	TypeChecker.visit(IResponse.IUnsatCoreResponse e)
ISort	TypeChecker.visit(IResponse.IValueResponse e)
ISort	TypeChecker.visit(ISort.IAbbreviation s)
ISort	TypeChecker.visit(ISort.IApplication s)
ISort	TypeChecker.visit(ISort.IDatatype e)
ISort	TypeChecker.visit(ISort.IFamily s)
ISort	TypeChecker.visit(ISort.IFcnSort s)
ISort	TypeChecker.visit(ISort.IParameter s)
ISort	TypeChecker.visit(ITheory s)
ISort	TypeChecker.visit(ISexpr.ISeq e)
ISort	TypeChecker.visit(ISexpr.IToken<?> e)

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

Modifier and Type	Method	Description
List<ISort>	ICommand.Ideclare_fun.argSorts()	Returns the list of argument sorts.
List<ISort>	ISort.IApplication.parameters()	Returns the list of parameters

Methods in org.smtlib with parameters of type ISort

Modifier and Type	Method	Description
boolean	SymbolTable.addSortDefinition(IExpr.IIdentifier identifier, List<ISort.IParameter> parameters, ISort definition, boolean global)	Adds a new sort abbreviation definition to the given frame (global = background, else current).
static List<IResponse>	TypeChecker.checkFcn(SymbolTable symTable, IExpr.IIdentifier id, List<IExpr.IDeclaration> params, ISort result, IExpr expr)
static List<IResponse>	TypeChecker.checkFcn(SymbolTable symTable, IExpr.IIdentifier id, List<ISort> sorts, ISort result, IPos pos)
void	ILanguage.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)	Checks whether the given function declaration is permitted in the language, throwing an exception if not
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.
static List<IResponse>	TypeChecker.checkSortAbbreviation(SymbolTable symTable, IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	ILanguage.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)	Checks whether the given sort declaration is permitted in the language, throwing an exception if not
static boolean	SymbolTable.containsParameter(ISort sort)	Whether the sort contains a sort parameter.
ISort.IFcnSort	ISort.IFactory.createFcnSort(ISort[] args, ISort result)	Creates a function sort.
ISort.IAbbreviation	ISort.IFactory.createSortAbbreviation(IExpr.IIdentifier identifier, List<ISort.IParameter> params, ISort sortExpr)	Creates a new sort abbreviation.
ISort.IApplication	ISort.IFactory.createSortExpression(IExpr.IIdentifier sortFamily, ISort... exprs)	Creates a sort expression, applying a family to a list of sort arguments; the arity of the identifier in the applicable symbol table must match the number of sort arguments.
IExpr.IDeclaration	IExpr.IFactory.declaration(IExpr.ISymbol symbol, ISort sort)	Creates a parameter declaration.
ICommand.Ideclare_const	ICommand.IFactory.declare_const(IExpr.ISymbol symbol, ISort resultSort)	Creates a declare-const command object.
ICommand.Ideclare_fun	ICommand.IFactory.declare_fun(IExpr.ISymbol id, List<ISort> argSorts, ISort resultSort)	Creates a declare-fun command object.
ICommand.Idefine_const	ICommand.IFactory.define_const(IExpr.ISymbol symbol, ISort resultSort, IExpr expression)	Creates a define-const command object.
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.
ICommand.Idefine_sort	ICommand.IFactory.define_sort(IExpr.ISymbol id, List<ISort.IParameter> parameters, ISort expression)	Creates a define-sort command object.
boolean	ISort.equalsNoExpand(ISort sort)	Raw structural comparison, deliberately without abbreviation expansion or parameter substitution -- so a user-defined alias and its expansion, which equals(Object) treats as equal, are NOT equal here.
boolean	ISort.IApplication.equalsNoExpand(ISort sort)
boolean	ISort.IParameter.equalsNoExpand(ISort sort)
IExpr.IFunctionDeclaration	IExpr.IFactory.functionDeclaration(IExpr.ISymbol symbol, List<IExpr.IDeclaration> parameters, ISort sort)	Creates a function declaration (used in define-funs-rec).
IExpr.IAsIdentifier	IExpr.IFactory.id(IExpr.IIdentifier identifier, ISort qualifier)	Creates an 'as' identifier from an identifier and a sort qualifier.
ISort	SymbolTable.lookup(IExpr.IIdentifier name, List<ISort> argSorts, ISort resultSort, StringBuilder reason)	Lookup a Symbol with the given name and argument Sorts and result Sort.
ISort.IFcnSort	SymbolTable.lookupInstance(int arity, IExpr.IIdentifier name, ISort resultSort)	The signature of the arity-n function name, instantiated so that its result sort is resultSort (a par entry's parameters are bound by unification), or null if there is no such function or its result sort cannot be resultSort.
protected String	TypeChecker.pr(ISort e)	Utility method for printing a sort, using the default printer
static ISort.IFcnSort	TypeChecker.resolveFcnSort(SymbolTable symTable, IExpr.IIdentifier id, List<ISort> sorts, ISort result, IPos pos, List<IResponse> errors)	Checks a function signature as checkFcn does, adding any errors to errors; returns the signature with its sorts resolved in the current scope (so a sort parameter in scope becomes its IParameter), or null if there were errors.
ISort	TypeChecker.save(IExpr e, ISort s)
IExpr.ISelector	IExpr.IFactory.selector(IExpr.ISymbol symbol, ISort sort)	Creates a selector declaration.
void	IExpr.setSort(ISort sort)	Records the sort computed for this expression by the type checker.

Method parameters in org.smtlib with type arguments of type ISort

Modifier and Type	Method	Description
static List<IResponse>	TypeChecker.checkFcn(SymbolTable symTable, IExpr.IIdentifier id, List<ISort> sorts, ISort result, IPos pos)
void	ILanguage.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)	Checks whether the given function declaration is permitted in the language, throwing an exception if not
ISort.IApplication	ISort.IFactory.createSortExpression(IExpr.IIdentifier sortFamily, List<ISort> exprs)	Creates a sort expression, applying a family to a list of sort arguments; the arity of the identifier in the applicable symbol table must match the number of sort arguments.
ICommand.Ideclare_fun	ICommand.IFactory.declare_fun(IExpr.ISymbol id, List<ISort> argSorts, ISort resultSort)	Creates a declare-fun command object.
ISort	ISort.IDefinition.eval(List<ISort> sorts)	A new sort expression that results from applying the sort symbol to a list of sort expressions
ISort	SymbolTable.lookup(IExpr.IIdentifier name, List<ISort> argSorts, ISort resultSort, StringBuilder reason)	Lookup a Symbol with the given name and argument Sorts and result Sort.
static ISort.IFcnSort	TypeChecker.resolveFcnSort(SymbolTable symTable, IExpr.IIdentifier id, List<ISort> sorts, ISort result, IPos pos, List<IResponse> errors)	Checks a function signature as checkFcn does, adding any errors to errors; returns the signature with its sorts resolved in the current scope (so a sort parameter in scope becomes its IParameter), or null if there were errors.
ISort	ISort.substitute(Map<ISort.IParameter,ISort> map)	Returns a new sort with any parameters substituted

Constructors in org.smtlib with parameters of type ISort

Modifier	Constructor	Description
	Variable(IExpr.ISymbol sym, ISort sort, IExpr expr, boolean closed)

Uses of ISort in org.smtlib.command

Fields in org.smtlib.command declared as ISort

Modifier and Type	Field	Description
protected ISort	C_define_sort.expression	The defining expression for the function
protected ISort	C_declare_fun.resultSort	The result sort of the function being declared
protected ISort	C_define_fun.resultSort	The sort of the result

Fields in org.smtlib.command with type parameters of type ISort

Modifier and Type	Field	Description
protected List<ISort>	C_declare_fun.argSorts	The sorts of the arguments of the function being declared -- never null (every construction path, parser or direct, always supplies a real list, empty for a zero-argument function).

Methods in org.smtlib.command that return ISort

Modifier and Type	Method	Description
ISort	C_define_sort.expression()	The defining expression for the function
ISort	C_declare_fun.resultSort()
ISort	C_define_fun.resultSort()	The result sort

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

Modifier and Type	Method	Description
List<ISort>	C_declare_fun.argSorts()

Constructors in org.smtlib.command with parameters of type ISort

Modifier	Constructor	Description
	C_declare_const(IExpr.ISymbol symbol, ISort resultSort)	Constructs a command instance from its components
	C_declare_fun(IExpr.ISymbol symbol, List<ISort> argSorts, ISort resultSort)	Constructs a command instance for an ordinary (non-attributed, non-par) declaration
	C_declare_fun(IExpr.ISymbol symbol, List<ISort> argSorts, ISort resultSort, List<IExpr.IAttribute<?>> attributes)	Constructs a command instance for an ordinary declaration, including any trailing attributes (see attributes()).
	C_declare_fun(IExpr.ISymbol symbol, List<ISort> argSorts, ISort resultSort, List<IExpr.IAttribute<?>> attributes, List<ISort.IParameter> parameters)	Constructs a command instance from all of its components, including the par-polymorphic parameters (see parameters()) for the "(declare-fun par ...)" form.
	C_define_const(IExpr.ISymbol symbol, ISort resultSort, IExpr expression)	Constructs a command instance
	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
	C_define_sort(IExpr.ISymbol id, List<ISort.IParameter> parameters, ISort expr)	Constructs a command instance

Constructor parameters in org.smtlib.command with type arguments of type ISort

Modifier	Constructor	Description
	C_declare_fun(IExpr.ISymbol symbol, List<ISort> argSorts, ISort resultSort)	Constructs a command instance for an ordinary (non-attributed, non-par) declaration
	C_declare_fun(IExpr.ISymbol symbol, List<ISort> argSorts, ISort resultSort, List<IExpr.IAttribute<?>> attributes)	Constructs a command instance for an ordinary declaration, including any trailing attributes (see attributes()).
	C_declare_fun(IExpr.ISymbol symbol, List<ISort> argSorts, ISort resultSort, List<IExpr.IAttribute<?>> attributes, List<ISort.IParameter> parameters)	Constructs a command instance from all of its components, including the par-polymorphic parameters (see parameters()) for the "(declare-fun par ...)" form.

Uses of ISort in org.smtlib.impl

Classes in org.smtlib.impl that implement ISort

Modifier and Type	Class	Description
class	Sort	This class implements the abstract ISort interface
static class	Sort.Application	Represents a sort expression consisting of a sort symbol or sort abbreviation symbol applied to a corresponding number of sort arguments
static class	Sort.FcnSort	Represents the class of the sort of a function symbol.
static class	Sort.Parameter	Represents a Sort parameter, such as in either the parameter list or the expression of a Sort abbreviation

Fields in org.smtlib.impl declared as ISort

Modifier and Type	Field	Description
protected ISort[]	Sort.FcnSort.argSorts
protected ISort	Sort.Application.expanded	Cached value for expanded()
protected static final ISort[]	Sort.FcnSort.noargs
protected ISort	SMTExpr.AsIdentifier.qualifier
protected ISort	Sort.FcnSort.resultSort
protected ISort	Pos.AbstractExpr.sort
protected ISort	SMTExpr.Declaration.sort
protected ISort	SMTExpr.FunctionDeclaration.sort
protected ISort	SMTExpr.Selector.sort
protected ISort	Sort.Abbreviation.sortExpression

Fields in org.smtlib.impl with type parameters of type ISort

Modifier and Type	Field	Description
protected List<ISort>	Sort.Application.sortParameters

Methods in org.smtlib.impl that return ISort

Modifier and Type	Method	Description
ISort[]	Sort.FcnSort.argSorts()
ISort	Sort.Abbreviation.eval(List<ISort> sorts)
ISort	Sort.ErrorDefinition.eval(List<ISort> sorts)
ISort	Sort.Parameter.eval(List<ISort> sorts)
ISort	Sort.Application.expand()
ISort	Sort.FcnSort.expand()
ISort	Sort.Parameter.expand()
ISort	Sort.Application.param(int i)
ISort	SMTExpr.AsIdentifier.qualifier()
ISort	Sort.FcnSort.resultSort()
ISort	Pos.AbstractExpr.sort()
ISort	SMTExpr.Declaration.sort()
ISort	SMTExpr.FunctionDeclaration.sort()
ISort	SMTExpr.Selector.sort()
ISort	Sort.Abbreviation.sortExpression()
ISort	Sort.Application.substitute(Map<ISort.IParameter,ISort> map)
ISort	Sort.FcnSort.substitute(Map<ISort.IParameter,ISort> map)
ISort	Sort.Parameter.substitute(Map<ISort.IParameter,ISort> map)

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

Modifier and Type	Method	Description
List<ISort>	Sort.Application.parameters()

Methods in org.smtlib.impl with parameters of type ISort

Modifier and Type	Method	Description
void	SMTExpr.Logic.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	SMTExpr.Logic.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
Sort.FcnSort	Factory.createFcnSort(ISort[] args, ISort result)
Sort.Abbreviation	Factory.createSortAbbreviation(IExpr.IIdentifier identifier, List<ISort.IParameter> params, ISort sortExpr)
Sort.Application	Factory.createSortExpression(IExpr.IIdentifier sortFamily, ISort... exprs)
IExpr.IDeclaration	Factory.declaration(IExpr.ISymbol symbol, ISort sort)
ICommand.Ideclare_const	Factory.declare_const(IExpr.ISymbol s, ISort r)
ICommand.Ideclare_fun	Factory.declare_fun(IExpr.ISymbol id, List<ISort> args, ISort r)
ICommand.Idefine_const	Factory.define_const(IExpr.ISymbol s, ISort r, IExpr e)
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)
ICommand.Idefine_sort	Factory.define_sort(IExpr.ISymbol id, List<ISort.IParameter> ps, ISort e)
boolean	Sort.Application.equalsNoExpand(ISort sort)
boolean	Sort.FcnSort.equalsNoExpand(ISort sort)
boolean	Sort.Parameter.equalsNoExpand(ISort sort)
IExpr.IFunctionDeclaration	Factory.functionDeclaration(IExpr.ISymbol symbol, List<IExpr.IDeclaration> parameters, ISort sort)
IExpr.IAsIdentifier	Factory.id(IExpr.IIdentifier identifier, ISort qualifier)
IExpr.ISelector	Factory.selector(IExpr.ISymbol symbol, ISort sort)
void	Pos.AbstractExpr.setSort(ISort sort)

Method parameters in org.smtlib.impl with type arguments of type ISort

Modifier and Type	Method	Description
void	SMTExpr.Logic.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
Sort.Application	Factory.createSortExpression(IExpr.IIdentifier sortFamily, List<ISort> exprs)
ICommand.Ideclare_fun	Factory.declare_fun(IExpr.ISymbol id, List<ISort> args, ISort r)
ISort	Sort.Abbreviation.eval(List<ISort> sorts)
ISort	Sort.ErrorDefinition.eval(List<ISort> sorts)
ISort.IApplication	Sort.Family.eval(List<ISort> sorts)
ISort	Sort.Parameter.eval(List<ISort> sorts)
ISort	Sort.Application.substitute(Map<ISort.IParameter,ISort> map)
ISort	Sort.FcnSort.substitute(Map<ISort.IParameter,ISort> map)
ISort	Sort.Parameter.substitute(Map<ISort.IParameter,ISort> map)

Constructors in org.smtlib.impl with parameters of type ISort

Modifier	Constructor	Description
	Abbreviation(IExpr.IIdentifier identifier, List<ISort.IParameter> parameters, ISort sortExpression)	Creates a sort abbreviation with the given identifier, parameter list, and defining expression.
	Application(IExpr.IIdentifier sortID, ISort... sortParameters)	Creates a sort application from a sort identifier and a varargs array of sort arguments.
	AsIdentifier(IExpr.IIdentifier symbol, ISort qualifier)	Creates an as-identifier from the given base identifier and sort qualifier.
	Declaration(IExpr.ISymbol parameter, ISort sort)	Creates a declaration binding the given symbol to the given sort.
	FcnSort(ISort resultSort)	Creates a zero-argument (nullary) function sort with the given result sort.
	FcnSort(ISort[] argSorts, ISort resultSort)	Creates a function sort with the given argument sorts and result sort.
	FunctionDeclaration(IExpr.ISymbol symbol, List<IExpr.IDeclaration> parameters, ISort sort)	Creates a function declaration with the given name, parameter declarations, and result sort.
	Selector(IExpr.ISymbol symbol, ISort sort)	Creates a selector with the given name and result sort.

Constructor parameters in org.smtlib.impl with type arguments of type ISort

Modifier	Constructor	Description
	Application(IExpr.IIdentifier sortID, List<ISort> sortParameters)	Creates a sort application from a sort identifier and a list of sort arguments.
	Application(IExpr.IIdentifier sortID, List<ISort> sortParameters, boolean parenthesized)	Creates a sort application that is written in parentheses even if it has no parameters, as (S)

Uses of ISort in org.smtlib.logic

Methods in org.smtlib.logic that return ISort

Modifier and Type	Method	Description
protected ISort	Logic.sortApp(String name, ISort... params)	Creates the sort expression name(params...), e.g.

Methods in org.smtlib.logic with parameters of type ISort

Modifier and Type	Method	Description
protected void	Logic.checkArraySorts(List<ISort> argSorts, ISort resultSort, IExpr.IIdentifier id)	Checks the Array sorts in a function's argument and result sorts
protected void	Logic.checkArraySorts(ISort sort, IPos pos)	Checks every Array sort within sort, expanding abbreviations, against Logic.allowedArraySort(org.smtlib.ISort.IApplication).
void	ALL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	AUFLIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	AUFLIRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	AUFNIRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	LIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	LRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_ABV.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_AUFBV.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_AUFLIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_AX.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_BV.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_EIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_FP.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_IDL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_NIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_NRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_RDL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UF.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFIDL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFLIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFLRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFNRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	UFLRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	UFNIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	ALL.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	AUFLIA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	AUFLIRA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	AUFNIRA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	LIA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	LRA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_ABV.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_AUFBV.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_AUFLIA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_AX.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_BV.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_EIA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_FP.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_IDL.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_NIA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_NRA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_RDL.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_UFIDL.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_UFLIA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_UFLRA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_UFNRA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	UFLRA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	UFNIA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
protected static boolean	Logic.isBitVecSort(ISort sort)	Whether sort, with abbreviations expanded, is a (_ BitVec n) sort
void	Logic.noFunctions(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	Logic.noSorts(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
protected static boolean	Logic.sameSort(ISort sort, ISort allowed)	Whether sort, with abbreviations expanded, is structurally the same as allowed
protected ISort	Logic.sortApp(String name, ISort... params)	Creates the sort expression name(params...), e.g.

Method parameters in org.smtlib.logic with type arguments of type ISort

Modifier and Type	Method	Description
protected void	Logic.checkArraySorts(List<ISort> argSorts, ISort resultSort, IExpr.IIdentifier id)	Checks the Array sorts in a function's argument and result sorts
void	ALL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	AUFLIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	AUFLIRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	AUFNIRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	LIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	LRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_ABV.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_AUFBV.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_AUFLIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_AX.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_BV.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_EIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_FP.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_IDL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_NIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_NRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_RDL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UF.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFIDL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFLIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFLRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFNRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	UFLRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	UFNIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	Logic.noFunctions(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)

Uses of ISort in org.smtlib.sexpr

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

Modifier and Type	Method	Description
List<ISort>	Parser.parseSortList(List<ISort.IParameter> parameters)	Parses sequence of sorts up to a right-parenthesis, returning null with error messages if an error occurs.