Uses of Interface
org.smtlib.IExpr.ISymbol

Packages that use IExpr.ISymbol

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

Fields in org.smtlib declared as IExpr.ISymbol

Modifier and Type	Field	Description
static final IExpr.ISymbol	Utils.ABS
static final IExpr.ISymbol	Utils.AND
static final IExpr.ISymbol	Utils.ARRAY
static final IExpr.ISymbol	Utils.ARROW
static final IExpr.ISymbol	Utils.AT
static final IExpr.ISymbol	Utils.BITVEC_SYM	Canonical ISymbol form of BITVEC, for structural comparison against a parsed identifier's head symbol (see TypeChecker.isBitVec() and SymbolTable's bit-vector family check) instead of comparing via .toString().
static final IExpr.ISymbol	Utils.BVADD
static final IExpr.ISymbol	Utils.BVAND
static final IExpr.ISymbol	Utils.BVASHR
static final IExpr.ISymbol	Utils.BVCOMP
static final IExpr.ISymbol	Utils.BVLSHR
static final IExpr.ISymbol	Utils.BVMUL
static final IExpr.ISymbol	Utils.BVNAND
static final IExpr.ISymbol	Utils.BVNEG
static final IExpr.ISymbol	Utils.BVNEGO
static final IExpr.ISymbol	Utils.BVNOR
static final IExpr.ISymbol	Utils.BVNOT
static final IExpr.ISymbol	Utils.BVOR
static final IExpr.ISymbol	Utils.BVSADDO
static final IExpr.ISymbol	Utils.BVSDIV
static final IExpr.ISymbol	Utils.BVSGE
static final IExpr.ISymbol	Utils.BVSGT
static final IExpr.ISymbol	Utils.BVSHL
static final IExpr.ISymbol	Utils.BVSLE
static final IExpr.ISymbol	Utils.BVSLT
static final IExpr.ISymbol	Utils.BVSMOD
static final IExpr.ISymbol	Utils.BVSMULO
static final IExpr.ISymbol	Utils.BVSREM
static final IExpr.ISymbol	Utils.BVSUB
static final IExpr.ISymbol	Utils.BVUADDO
static final IExpr.ISymbol	Utils.BVUDIV
static final IExpr.ISymbol	Utils.BVUGE
static final IExpr.ISymbol	Utils.BVUGT
static final IExpr.ISymbol	Utils.BVULE
static final IExpr.ISymbol	Utils.BVULT
static final IExpr.ISymbol	Utils.BVUMULO
static final IExpr.ISymbol	Utils.BVUREM
static final IExpr.ISymbol	Utils.BVXNOR
static final IExpr.ISymbol	Utils.BVXOR
static final IExpr.ISymbol	Utils.CHAR	Head of the Strings theory's (_ char H) constants.
static final IExpr.ISymbol	Utils.CONCAT
static final IExpr.ISymbol	Utils.DISTINCT
static final IExpr.ISymbol	Utils.DIV
static final IExpr.ISymbol	Utils.EQ
static final IExpr.ISymbol	Utils.EXP
static final IExpr.ISymbol	Utils.EXTRACT
static final IExpr.ISymbol	Utils.FALSE	Symbol constant for boolean false.
static final IExpr.ISymbol	Utils.FLOAT128
static final IExpr.ISymbol	Utils.FLOAT16	Short names for common FloatingPoint sorts (FloatingPoint.smt2's :notes documents each as a synonym for a specific (_ FloatingPoint eb sb) instance) -- resolved by SymbolTable.lookupSort() to the exact same ISort.IDefinition as that instance, not registered as their own independent sorts (see Utils.loadTheory(), which excludes them from the generic :sorts loader for the same reason).
static final IExpr.ISymbol	Utils.FLOAT32
static final IExpr.ISymbol	Utils.FLOAT64
static final IExpr.ISymbol	Utils.FLOATINGPOINT_SYM	Canonical ISymbol form of FLOATINGPOINT, for structural comparison against a parsed identifier's head symbol (see TypeChecker.isFloatingPoint() and SymbolTable's FloatingPoint family check) instead of comparing via .toString().
static final IExpr.ISymbol	Utils.FP
static final IExpr.ISymbol	Utils.FP_ABS
static final IExpr.ISymbol	Utils.FP_ADD
static final IExpr.ISymbol	Utils.FP_DIV
static final IExpr.ISymbol	Utils.FP_EQ
static final IExpr.ISymbol	Utils.FP_FMA
static final IExpr.ISymbol	Utils.FP_GEQ
static final IExpr.ISymbol	Utils.FP_GT
static final IExpr.ISymbol	Utils.FP_IS_INFINITE
static final IExpr.ISymbol	Utils.FP_IS_NAN
static final IExpr.ISymbol	Utils.FP_IS_NEGATIVE
static final IExpr.ISymbol	Utils.FP_IS_NORMAL
static final IExpr.ISymbol	Utils.FP_IS_POSITIVE
static final IExpr.ISymbol	Utils.FP_IS_SUBNORMAL
static final IExpr.ISymbol	Utils.FP_IS_ZERO
static final IExpr.ISymbol	Utils.FP_LEQ
static final IExpr.ISymbol	Utils.FP_LT
static final IExpr.ISymbol	Utils.FP_MAX
static final IExpr.ISymbol	Utils.FP_MIN
static final IExpr.ISymbol	Utils.FP_MUL
static final IExpr.ISymbol	Utils.FP_NAN
static final IExpr.ISymbol	Utils.FP_NEG
static final IExpr.ISymbol	Utils.FP_NEG_INF
static final IExpr.ISymbol	Utils.FP_NEG_ZERO
static final IExpr.ISymbol	Utils.FP_POS_INF	Zero-arity indexed identifiers, e.g.
static final IExpr.ISymbol	Utils.FP_POS_ZERO
static final IExpr.ISymbol	Utils.FP_REM
static final IExpr.ISymbol	Utils.FP_ROUND_TO_INTEGRAL
static final IExpr.ISymbol	Utils.FP_SQRT
static final IExpr.ISymbol	Utils.FP_SUB
static final IExpr.ISymbol	Utils.FP_TO_REAL
static final IExpr.ISymbol	Utils.FP_TO_SBV
static final IExpr.ISymbol	Utils.FP_TO_UBV
static final IExpr.ISymbol	Utils.GE
static final IExpr.ISymbol	Utils.GT
static final IExpr.ISymbol	Utils.IMPLIES
static final IExpr.ISymbol	Utils.INT_TO_BV
static final IExpr.ISymbol	Utils.ITE
static final IExpr.ISymbol	Utils.LE
static final IExpr.ISymbol	Utils.LT
static final IExpr.ISymbol	Utils.MINUS
static final IExpr.ISymbol	Utils.MOD
static final IExpr.ISymbol	Utils.MULT
static final IExpr.ISymbol	Utils.NOT
static final IExpr.ISymbol	Utils.OR
static final IExpr.ISymbol	Utils.PLUS
static final IExpr.ISymbol	Utils.REPEAT
static final IExpr.ISymbol	Utils.ROTATE_LEFT
static final IExpr.ISymbol	Utils.ROTATE_RIGHT
static final IExpr.ISymbol	Utils.ROUNDINGMODE_SYM
static final IExpr.ISymbol	Utils.SBV_TO_INT
static final IExpr.ISymbol	Utils.SELECT
static final IExpr.ISymbol	Utils.SIGN_EXTEND
static final IExpr.ISymbol	Utils.SLASH
static final IExpr.ISymbol	Utils.STORE
IExpr.ISymbol	TypeChecker.Variable.symbol
static final IExpr.ISymbol	Utils.TO_FP
static final IExpr.ISymbol	Utils.TO_FP_UNSIGNED
static final IExpr.ISymbol	Utils.TRUE	Symbol constant for boolean true.
static final IExpr.ISymbol	Utils.UBV_TO_INT	Bitvector/Int conversions and overflow predicates (SMT-LIB 2.7 FixedSizeBitVectors).
static final IExpr.ISymbol	Utils.XOR
static final IExpr.ISymbol	Utils.ZERO_EXTEND

Fields in org.smtlib with type parameters of type IExpr.ISymbol

Modifier and Type	Field	Description
protected Map<IExpr.ISymbol,TypeChecker.Variable>	TypeChecker.currentScope
protected List<Map<IExpr.ISymbol,TypeChecker.Variable>>	TypeChecker.parameters

Methods in org.smtlib that return IExpr.ISymbol

Modifier and Type	Method	Description
IExpr.ISymbol	IResponse.IFactory.constant(String id)	Returns a constant response with the given canonical name
IExpr.ISymbol	IExpr.IPattern.constructor()
IExpr.ISymbol	IExpr.IParameterizedIdentifier.head()	The head symbol of the identifier
IExpr.ISymbol	IExpr.IAsIdentifier.headSymbol()	The head symbol of the identifier
IExpr.ISymbol	IExpr.IIdentifier.headSymbol()	The head symbol of the identifier
IExpr.ISymbol	IExpr.IQualifiedIdentifier.headSymbol()	The head symbol of the identifier
IExpr.ISymbol	ICommand.Iset_logic.logic()	Returns the logic name.
IExpr.ISymbol	ILogic.logicName()	The name of the logic
IExpr.ISymbol	IExpr.IBinding.parameter()
IExpr.ISymbol	IExpr.IDeclaration.parameter()
IExpr.ISymbol	IParser.parseSymbol()	Parse an SMT-LIB symbol; return null and log an error response if there is no symbol
IExpr.ISymbol	ICommand.Ideclare_sort_parameter.sortSymbol()	Returns the name of the sort parameter being declared.
IExpr.ISymbol	ICommand.Ideclare_sort.sortSymbol()	Returns the name of the sort being declared.
IExpr.ISymbol	ICommand.Idefine_sort.sortSymbol()	Returns the name of the sort being defined.
IExpr.ISymbol	ICommand.Ideclare_const.symbol()	Returns the name of the constant being declared.
IExpr.ISymbol	ICommand.Ideclare_fun.symbol()	Returns the name of the function being declared.
IExpr.ISymbol	ICommand.Idefine_fun_rec.symbol()	Returns the name of the function being defined.
IExpr.ISymbol	ICommand.Idefine_fun.symbol()	Returns the name of the function being defined.
IExpr.ISymbol	IExpr.IConstructor.symbol()
IExpr.ISymbol	IExpr.IFactory.symbol(String v)	Creates an ISymbol object from a canonical String representation of the symbol.
IExpr.ISymbol	IExpr.IFunctionDeclaration.symbol()
IExpr.ISymbol	IExpr.ISelector.symbol()
IExpr.ISymbol	IExpr.ISortDeclaration.symbol()
IExpr.ISymbol	ISort.IParameter.symbol()	The symbol that names the parameter
IExpr.ISymbol	ITheory.theoryName()	The name of the theory

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

Modifier and Type	Method	Description
List<IResponse.IPair<IExpr.ISymbol,Boolean>>	IResponse.IAssignmentResponse.assignments()
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.
List<IExpr.ISymbol>	IResponse.IUnsatCoreResponse.names()
List<IExpr.ISymbol>	IExpr.IPattern.params()
List<IExpr.ISymbol>	ISort.IDatatype.symbols()

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

Modifier and Type	Method	Description
boolean	SymbolTable.addSortParameter(IExpr.ISymbol symbol, boolean global)	Adds the given symbol as a sort to the top scope of the sort table; returns false if the given symbol is already in the top scope (and the sort table is unchanged); returns true if the symbol is not already in the top scope.
protected boolean	TypeChecker.badSymbol(IExpr.ISymbol s)	Reports a symbol that is not legal (see SMT.Configuration.isOKSymbol), which only the API (or declare-fun's name) can produce; returns true if it is not legal
IExpr.IBinding	IExpr.IFactory.binding(IExpr.ISymbol symbol, IExpr expr)	Creates a binding for a Let expression.
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.
default void	IParser.checkUserId(IExpr.ISymbol id)	Checks that a user-defined symbol does not begin with the reserved characters @ or .; throws a ParserException if the check fails.
IExpr.IConstructor	IExpr.IFactory.constructor(IExpr.ISymbol symbol, List<IExpr.ISelector> selectors)	Creates a constructor declaration.
ISort.IParameter	ISort.IFactory.createSortParameter(IExpr.ISymbol symbol)	Creates a parameter for a parameterized sort abbreviation.
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.Ideclare_sort	ICommand.IFactory.declare_sort(IExpr.ISymbol sym, IExpr.INumeral arity)	Creates a declare-sort command object.
ICommand.Ideclare_sort_parameter	ICommand.IFactory.declare_sort_parameter(IExpr.ISymbol sym)	Creates a declare-sort-parameter 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.
IExpr.IFunctionDeclaration	IExpr.IFactory.functionDeclaration(IExpr.ISymbol symbol, List<IExpr.IDeclaration> parameters, ISort sort)	Creates a function declaration (used in define-funs-rec).
IExpr.IParameterizedIdentifier	IExpr.IFactory.id(IExpr.ISymbol symbol, List<IExpr.IIndex> indices)	Creates a parameterized identifier from a symbol and a non-empty list of indices (each INumeral or ISymbol).
boolean	SymbolTable.isLogicSymbol(IExpr.ISymbol s, boolean sort)	Whether the symbol is a function (sort, if sort is true) symbol of the logic or its theories
IExpr.IPattern	IExpr.IFactory.pattern(IExpr.ISymbol constructor, List<IExpr.ISymbol> params)	Creates a match pattern.
IExpr.ISelector	IExpr.IFactory.selector(IExpr.ISymbol symbol, ISort sort)	Creates a selector declaration.
ICommand.Iset_logic	ICommand.IFactory.set_logic(IExpr.ISymbol logic)	Creates a set-logic command object.
protected boolean	TypeChecker.shadowsLogic(IExpr.ISymbol s, boolean sort)	Reports a bound variable (sort parameter, if sort is true) with the name of a function (sort) symbol of the logic or its theories, which only --relax allows (SMT-LIB Remark 7); returns true if reported
IExpr.ISortDeclaration	IExpr.IFactory.sortDeclaration(IExpr.ISymbol symbol, IExpr.INumeral arity)	Creates a sort declaration (symbol + arity) for use in declare-datatype(s).
T	IVisitor.TreeVisitor.visit(IExpr.ISymbol e)
T	IVisitor.visit(IExpr.ISymbol e)
ISort	TypeChecker.visit(IExpr.ISymbol e)

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

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).
IResponse.IAssignmentResponse	IResponse.IFactory.get_assignment_response(List<IResponse.IPair<IExpr.ISymbol,Boolean>> assignments)
IResponse.IUnsatCoreResponse	IResponse.IFactory.get_unsat_core_response(List<IExpr.ISymbol> names)
IExpr.IPattern	IExpr.IFactory.pattern(IExpr.ISymbol constructor, List<IExpr.ISymbol> params)	Creates a match pattern.

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

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

Uses of IExpr.ISymbol in org.smtlib.command

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

Modifier and Type	Field	Description
protected IExpr.ISymbol	C_declare_fun.fcnName	The name of the function being declared
protected IExpr.ISymbol	C_define_fun.fcnName	The name of the function being defined
protected IExpr.ISymbol	C_set_logic.logicName	The name of the logic to set
protected IExpr.ISymbol	C_define_sort.sortName	The name of the sort being defined
protected IExpr.ISymbol	C_declare_sort_parameter.sortSymbol	The new sort symbol
protected IExpr.ISymbol	C_declare_sort.sortSymbol	The new sort symbol

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

Modifier and Type	Method	Description
IExpr.ISymbol	C_set_logic.logic()	The name of the logic to set
IExpr.ISymbol	C_declare_sort_parameter.sortSymbol()	The sort symbol declared by this command
IExpr.ISymbol	C_declare_sort.sortSymbol()	The sort symbol declared by this command
IExpr.ISymbol	C_define_sort.sortSymbol()	Returns the name of the sort being defined.
IExpr.ISymbol	C_declare_fun.symbol()
IExpr.ISymbol	C_define_fun.symbol()	The name of the function being defined

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

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_declare_sort(IExpr.ISymbol id, IExpr.INumeral n)	Constructs a new command object
	C_declare_sort_parameter(IExpr.ISymbol id)	Constructs a new command object
	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
	C_set_logic(IExpr.ISymbol logic)	Constructs a command instance for the given logic name.

Uses of IExpr.ISymbol in org.smtlib.impl

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

Modifier and Type	Class	Description
static class	SMTExpr.Symbol	This class represents an SMT Symbol

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

Modifier and Type	Field	Description
protected IExpr.ISymbol	SMTExpr.Pattern.constructor
protected IExpr.ISymbol	SMTExpr.ParameterizedIdentifier.head
protected IExpr.ISymbol	SMTExpr.Logic.logicName	The name of the logic
protected IExpr.ISymbol	SMTExpr.Binding.parameter
protected IExpr.ISymbol	SMTExpr.Declaration.parameter
protected IExpr.ISymbol	SMTExpr.Constructor.symbol
protected IExpr.ISymbol	SMTExpr.FunctionDeclaration.symbol
protected IExpr.ISymbol	SMTExpr.Selector.symbol
protected IExpr.ISymbol	SMTExpr.SortDeclaration.symbol
protected IExpr.ISymbol	Sort.Parameter.symbol
protected IExpr.ISymbol	SMTExpr.Theory.theoryName	The name of the theory

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

Modifier and Type	Field	Description
protected List<IExpr.ISymbol>	SMTExpr.Pattern.params
protected List<IExpr.ISymbol>	SMTExpr.Datatype.symbols

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

Modifier and Type	Method	Description
IExpr.ISymbol	Response.Factory.constant(String sym)
IExpr.ISymbol	SMTExpr.Pattern.constructor()
IExpr.ISymbol	SMTExpr.ParameterizedIdentifier.head()
IExpr.ISymbol	SMTExpr.AsIdentifier.headSymbol()
IExpr.ISymbol	SMTExpr.ParameterizedIdentifier.headSymbol()
IExpr.ISymbol	SMTExpr.Symbol.headSymbol()
IExpr.ISymbol	SMTExpr.Logic.logicName()	The name of the logic
IExpr.ISymbol	SMTExpr.Binding.parameter()
IExpr.ISymbol	SMTExpr.Declaration.parameter()
IExpr.ISymbol	Factory.symbol(String v)
IExpr.ISymbol	SMTExpr.Constructor.symbol()
IExpr.ISymbol	SMTExpr.FunctionDeclaration.symbol()
IExpr.ISymbol	SMTExpr.Selector.symbol()
IExpr.ISymbol	SMTExpr.SortDeclaration.symbol()
IExpr.ISymbol	Sort.Parameter.symbol()
IExpr.ISymbol	SMTExpr.Theory.theoryName()	The name of the theory

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

Modifier and Type	Method	Description
List<IResponse.IPair<IExpr.ISymbol,Boolean>>	Response.AssignmentResponse.assignments()
List<IExpr.ISymbol>	Response.UnsatCoreResponse.names()
List<IExpr.ISymbol>	SMTExpr.Pattern.params()
List<IExpr.ISymbol>	SMTExpr.Datatype.symbols()

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

Modifier and Type	Method	Description
void	Response.AssignmentResponse.add(IExpr.ISymbol name, Boolean value)
IExpr.IBinding	Factory.binding(IExpr.ISymbol symbol, IExpr expr)
IExpr.IConstructor	Factory.constructor(IExpr.ISymbol symbol, List<IExpr.ISelector> selectors)
Sort.Parameter	Factory.createSortParameter(IExpr.ISymbol symbol)
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.Ideclare_sort	Factory.declare_sort(IExpr.ISymbol s, IExpr.INumeral n)
ICommand.Ideclare_sort_parameter	Factory.declare_sort_parameter(IExpr.ISymbol s)
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)
IExpr.IFunctionDeclaration	Factory.functionDeclaration(IExpr.ISymbol symbol, List<IExpr.IDeclaration> parameters, ISort sort)
IExpr.IParameterizedIdentifier	Factory.id(IExpr.ISymbol symbol, List<IExpr.IIndex> indices)
IExpr.IPattern	Factory.pattern(IExpr.ISymbol constructor, List<IExpr.ISymbol> params)
IExpr.ISelector	Factory.selector(IExpr.ISymbol symbol, ISort sort)
ICommand.Iset_logic	Factory.set_logic(IExpr.ISymbol s)
IExpr.ISortDeclaration	Factory.sortDeclaration(IExpr.ISymbol symbol, IExpr.INumeral arity)

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

Modifier and Type	Method	Description
Response.AssignmentResponse	Response.Factory.get_assignment_response(List<IResponse.IPair<IExpr.ISymbol,Boolean>> assignments)
Response.UnsatCoreResponse	Response.Factory.get_unsat_core_response(List<IExpr.ISymbol> names)
IExpr.IPattern	Factory.pattern(IExpr.ISymbol constructor, List<IExpr.ISymbol> params)

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

Modifier	Constructor	Description
	Binding(IExpr.ISymbol parameter, IExpr expr)	Creates a binding of the given symbol to the given expression.
	Constructor(IExpr.ISymbol symbol, List<IExpr.ISelector> selectors)	Creates a constructor with the given name and list of selector declarations.
	Declaration(IExpr.ISymbol parameter, ISort sort)	Creates a declaration binding the given symbol to the given sort.
	FunctionDeclaration(IExpr.ISymbol symbol, List<IExpr.IDeclaration> parameters, ISort sort)	Creates a function declaration with the given name, parameter declarations, and result sort.
	Logic(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)	Creates a logic
	Parameter(IExpr.ISymbol symbol)	Creates a sort parameter for the given symbol name.
	ParameterizedIdentifier(IExpr.ISymbol symbol, List<IExpr.IIndex> indices)	Creates a parameterized identifier from the given head symbol and index list.
	Pattern(IExpr.ISymbol constructor, List<IExpr.ISymbol> params)	Creates a pattern from the given constructor symbol and variable list.
	Pattern(IExpr.ISymbol constructor, List<IExpr.ISymbol> params, boolean parenthesized)	Creates a pattern that is written in parentheses even if it has no variables, as (c)
	Selector(IExpr.ISymbol symbol, ISort sort)	Creates a selector with the given name and result sort.
	SortDeclaration(IExpr.ISymbol symbol, IExpr.INumeral arity)	Creates a sort declaration for the given sort name and arity.
	Theory(IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)	Creates a theory

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

Modifier	Constructor	Description
	AssignmentResponse(List<IResponse.IPair<IExpr.ISymbol,Boolean>> assignments)
	Pattern(IExpr.ISymbol constructor, List<IExpr.ISymbol> params)	Creates a pattern from the given constructor symbol and variable list.
	Pattern(IExpr.ISymbol constructor, List<IExpr.ISymbol> params, boolean parenthesized)	Creates a pattern that is written in parentheses even if it has no variables, as (c)
	UnsatCoreResponse(List<IExpr.ISymbol> names)

Uses of IExpr.ISymbol in org.smtlib.logic

Constructors in org.smtlib.logic with parameters of type IExpr.ISymbol

Modifier	Constructor	Description
	ALL(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	AUFLIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	AUFLIRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	AUFNIRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	DifferenceLogic(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	LIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	Logic(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	LRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_ABV(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_AUFBV(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_AUFLIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_AX(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_BV(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_EIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_FP(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_IDL(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_LIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_LRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_NIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_NRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_RDL(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_UF(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_UFBV(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_UFIDL(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_UFLIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_UFLRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	QF_UFNRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	UFLRA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)
	UFNIA(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)

Uses of IExpr.ISymbol in org.smtlib.sexpr

Fields in org.smtlib.sexpr declared as IExpr.ISymbol

Modifier and Type	Field	Description
IExpr.ISymbol	Parser.commandName	This field is used only to communicate the position of the name of a command to the command creator (instead of using method arguments).

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

Modifier and Type	Method	Description
List<IResponse.IPair<IExpr.ISymbol,Boolean>>	Parser.parseAssignmentList()	Parses a parenthesized list of (symbol bool) pairs, as returned by a get-assignment response.
IResponse.IPair<IExpr.ISymbol,Boolean>	Parser.parseAssignmentPair()	Parses one (symbol bool) pair, as found in a get-assignment response.
List<IExpr.ISymbol>	Parser.parseSymbolList()	Parses a parenthesized list of names, as returned by a get-unsat-core response.

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

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

Uses of IExpr.ISymbol in org.smtlib.solvers

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

Modifier and Type	Method	Description
String	Solver_simplify.Translator.name(IExpr.ISymbol e)	The Simplify name of a symbol, as a function name or a bound variable
String	Solver_simplify.Translator.visit(IExpr.ISymbol e)