Uses of Interface
org.smtlib.IExpr.IIdentifier

Packages that use IExpr.IIdentifier

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.ext	This package contains commands that are extensions to SMT-LIB.
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.
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.IIdentifier in org.smtlib

Subinterfaces of IExpr.IIdentifier in org.smtlib

Modifier and Type	Interface	Description
static interface	IExpr.IParameterizedIdentifier	This interface represents SMT-LIB parameterized identifiers
static interface	IExpr.ISymbol	This interface represents SMT-LIB ids; equal ids have equal (using .equals) values of value().

Fields in org.smtlib declared as IExpr.IIdentifier

Modifier and Type	Field	Description
IExpr.IIdentifier	SymbolTable.Entry.name	The identifier

Methods in org.smtlib that return IExpr.IIdentifier

Modifier and Type	Method	Description
IExpr.IIdentifier	ISort.IApplication.family()	The head identifier of the sort expression
IExpr.IIdentifier	IExpr.IAsIdentifier.head()	The head of the identifier
IExpr.IIdentifier	ISort.IAbbreviation.identifier()	The identifier of the abbreviation
IExpr.IIdentifier	ISort.IDefinition.identifier()	The identifier for the sort symbol
IExpr.IIdentifier	ISort.IFamily.identifier()	The unique identifier for this sort symbol
IExpr.IIdentifier	IParser.parseIdentifier()	Parses an identifier (either a symbol or a parameterized identifier) from the token stream, returning null (with logged error messages) if there is not one.

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

Modifier and Type	Method	Description
void	SymbolTable.addDatatypeConstructors(IExpr.IIdentifier sortName, List<IExpr.ISymbol> ctors, boolean global)	Records a datatype's constructors, in the frame its sort was added to (global = background, else current).
void	SymbolTable.addLogicSymbol(IExpr.IIdentifier id, boolean sort)	Records a function (sort, if sort is true) symbol declared by the logic or one of its theories
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).
boolean	SymbolTable.addSortDefinition(IExpr.IIdentifier identifier, IExpr.INumeral arity, List<IExpr.IAttribute<?>> attributes, boolean global)	Adds a new sort family definition, with attributes (e.g.
String	SymbolTable.ambiguousConstant(IExpr.IIdentifier name)	Returns an error message if more than one constant (arity 0) named `name` is declared, so that a bare use of it needs an `as` qualifier; otherwise null.
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.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
ISort.IErrorDefinition	ISort.IFactory.createErrorDefinition(IExpr.IIdentifier id, String errorMessage, IPos pos)	Creates an error-placeholder definition (suppresses cascading errors).
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, 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.
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.
ISort.IFamily	ISort.IFactory.createSortFamily(IExpr.IIdentifier identifier, IExpr.INumeral arity, List<IExpr.IAttribute<?>> attributes)	Creates a sort family with the given identifier, arity, and attributes (null or empty if none).
List<IExpr.ISymbol>	SymbolTable.datatypeConstructors(IExpr.IIdentifier sortName)	The constructors of the datatype sort with the given identifier, or null if no datatype of that name is in scope.
IExpr.IAsIdentifier	IExpr.IFactory.id(IExpr.IIdentifier identifier, ISort qualifier)	Creates an 'as' identifier from an identifier and a sort qualifier.
ISort.IFcnSort	SymbolTable.lookup(int arity, IExpr.IIdentifier name)	Lookup the Symbol with the given identifier and arity, returning its Sort.
List<SymbolTable.Entry>	SymbolTable.lookup(IExpr.IIdentifier name)	Lookup the Symbol with the given identifier, returning all of its declared entries (of any arity).
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.
ISort.IDefinition	SymbolTable.lookupSort(IExpr.IIdentifier name)	Looks up the Sort definition with the given name
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.

Constructors in org.smtlib with parameters of type IExpr.IIdentifier

Modifier	Constructor	Description
	Entry(IExpr.IIdentifier name, ISort.IFcnSort sort, List<IExpr.IAttribute<?>> attrs, List<ISort.IParameter> parameters)	Constructs a symbol table entry

Uses of IExpr.IIdentifier in org.smtlib.ext

Fields in org.smtlib.ext with type parameters of type IExpr.IIdentifier

Modifier and Type	Field	Description
protected List<IExpr.IIdentifier>	C_what.ids	The ids that are the arguments of the command

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

Modifier and Type	Method	Description
List<IExpr.IIdentifier>	C_what.ids()	The ids that are the arguments of the command
List<IExpr.IIdentifier>	Iwhat.ids()	Returns the identifiers to look up and describe.

Constructor parameters in org.smtlib.ext with type arguments of type IExpr.IIdentifier

Modifier	Constructor	Description
	C_what(List<IExpr.IIdentifier> ids)	Constructs a command instance for the given identifiers.

Uses of IExpr.IIdentifier in org.smtlib.impl

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

Modifier and Type	Class	Description
static class	SMTExpr.ParameterizedIdentifier	This class represents an SMT parameterized-identifier AST (e.g.
static class	SMTExpr.Symbol	This class represents an SMT Symbol

Fields in org.smtlib.impl declared as IExpr.IIdentifier

Modifier and Type	Field	Description
protected IExpr.IIdentifier	SMTExpr.AsIdentifier.head
protected IExpr.IIdentifier	Sort.ErrorDefinition.id
protected IExpr.IIdentifier	Sort.Abbreviation.identifier
protected IExpr.IIdentifier	Sort.Family.identifier
protected IExpr.IIdentifier	Sort.Application.sortID

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

Modifier and Type	Method	Description
IExpr.IIdentifier	Sort.Application.family()
IExpr.IIdentifier	SMTExpr.AsIdentifier.head()
IExpr.IIdentifier	Sort.Abbreviation.identifier()
IExpr.IIdentifier	Sort.ErrorDefinition.identifier()
IExpr.IIdentifier	Sort.Family.identifier()
IExpr.IIdentifier	Sort.Parameter.identifier()

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

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)
ISort.IErrorDefinition	Factory.createErrorDefinition(IExpr.IIdentifier id, String errorMessage, IPos pos)
Sort.Abbreviation	Factory.createSortAbbreviation(IExpr.IIdentifier identifier, List<ISort.IParameter> params, ISort sortExpr)
Sort.Application	Factory.createSortExpression(IExpr.IIdentifier sortFamily, List<ISort> exprs)
Sort.Application	Factory.createSortExpression(IExpr.IIdentifier sortFamily, ISort... exprs)
Sort.Family	Factory.createSortFamily(IExpr.IIdentifier identifier, IExpr.INumeral arity, List<IExpr.IAttribute<?>> attributes)
IExpr.IAsIdentifier	Factory.id(IExpr.IIdentifier identifier, ISort qualifier)

Constructors in org.smtlib.impl with parameters of type IExpr.IIdentifier

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, 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)
	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.
	ErrorDefinition(IExpr.IIdentifier id, String error, IPos pos)	Creates an error placeholder for the given identifier, error message, and source position.
	Family(IExpr.IIdentifier identifier, IExpr.INumeral arity, List<IExpr.IAttribute<?>> attributes)	Creates a sort family with the given identifier, arity, and attributes (null or empty if none).

Uses of IExpr.IIdentifier in org.smtlib.logic

Methods in org.smtlib.logic with parameters of type IExpr.IIdentifier

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	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)
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)

Uses of IExpr.IIdentifier in org.smtlib.sexpr

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

Modifier and Type	Method	Description
IExpr.IIdentifier	Parser.parseIdentifier()	Parses an identifier (either symbol or parameterized identifier) from the token stream, returning null with logged error messages if there is not one.

Uses of IExpr.IIdentifier in org.smtlib.solvers

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

Modifier and Type	Method	Description
protected String	Solver_simplify.encode(IExpr.IIdentifier id)	See Solver_test.encode(org.smtlib.IExpr.IIdentifier).
protected String	Solver_test.encode(IExpr.IIdentifier id)