Uses of Interface
org.smtlib.IExpr.IAttribute

Packages that use IExpr.IAttribute

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

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

Modifier and Type	Field	Description
List<IExpr.IAttribute<?>>	SymbolTable.Entry.attributes	Any attributes (null if none), e.g.

Methods in org.smtlib that return IExpr.IAttribute

Modifier and Type	Method	Description
IExpr.IAttribute<?>	IExpr.IFactory.attribute(IExpr.IKeyword k)	Creates an attribute with just a keyword and no attribute value.
<T extends IAttributeValue> IExpr.IAttribute<T>	IExpr.IFactory.attribute(IExpr.IKeyword k, T value)	Creates an attribute with a keyword and a value.
IExpr.IAttribute<?>	IParser.parseAttribute()	Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.

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

Modifier and Type	Method	Description
List<IExpr.IAttribute<?>>	ILogic.attributeList()	The attributes in source order, including repeated keywords
List<IExpr.IAttribute<?>>	ITheory.attributeList()	The attributes in source order, including repeated keywords
default List<IExpr.IAttribute<?>>	ICommand.Ideclare_fun.attributes()	Returns any trailing attributes given after the result sort -- an experimental, non-standard extension (SMT-LIB's declare-fun has no attribute* production); accepting one at all is unconditional at parse time, but the command is rejected at type-checking time unless --relax is set.
List<IExpr.IAttribute<?>>	IExpr.IAttributedExpr.attributes()
Map<IExpr.IKeyword,IExpr.IAttribute<?>>	ILogic.attributes()	The attributes of the logic
List<IExpr.IAttribute<? extends IAttributeValue>>	IResponse.IAttributeList.attributes()
List<IExpr.IAttribute<?>>	ISort.IFamily.attributes()	Any attributes declared on this sort symbol (e.g.
Map<IExpr.IKeyword,IExpr.IAttribute<?>>	ITheory.attributes()	The attributes (keyword-value pairs) of the theory.

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

Modifier and Type	Method	Description
IResponse.IAttributeList	IResponse.IFactory.get_info_response(IExpr.IAttribute<?> attr)
T	IVisitor.TreeVisitor.visit(IExpr.IAttribute<?> e)
T	IVisitor.visit(IExpr.IAttribute<?> e)
ISort	TypeChecker.visit(IExpr.IAttribute<?> e)

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

Modifier and Type	Method	Description
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.
IExpr.IAttributedExpr	IExpr.IFactory.attributedExpr(IExpr e, List<IExpr.IAttribute<?>> attributes)	Creates an attributed expression (an expression with a positive number of attributes).
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).
IResponse.IAttributeList	IResponse.IFactory.get_info_response(List<IExpr.IAttribute<?>> attrList)

Constructor parameters in org.smtlib with type arguments of type IExpr.IAttribute

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

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

Modifier and Type	Field	Description
protected List<IExpr.IAttribute<?>>	C_declare_fun.attributes	Any trailing attributes (see attributes()) -- never null, Collections.emptyList() if none (the common case: this is a non-standard extension, only meaningful at all under --relax).

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

Modifier and Type	Method	Description
List<IExpr.IAttribute<?>>	C_declare_fun.attributes()

Uses of IExpr.IAttribute in org.smtlib.impl

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

Modifier and Type	Class	Description
static class	SMTExpr.Attribute<TT extends IAttributeValue>	Represents an SMT-LIB attribute: a keyword optionally paired with a value.

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

Modifier and Type	Field	Description
protected List<IExpr.IAttribute<?>>	SMTExpr.AttributedExpr.attributes
protected Map<IExpr.IKeyword,IExpr.IAttribute<?>>	SMTExpr.Logic.attributes	The logic's attributes — last occurrence wins for duplicate keywords
protected Map<IExpr.IKeyword,IExpr.IAttribute<?>>	SMTExpr.Theory.attributes	The theory attributes — last occurrence wins for duplicate keywords
protected List<IExpr.IAttribute<?>>	Sort.Family.attributes
protected List<IExpr.IAttribute<?>>	SMTExpr.Logic.attributesList	All logic attributes in source order, preserving duplicates
protected List<IExpr.IAttribute<?>>	SMTExpr.Theory.attributesList	All theory attributes in source order, preserving duplicates

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

Modifier and Type	Method	Description
IExpr.IAttribute<?>	Factory.attribute(IExpr.IKeyword k)
<T extends IAttributeValue> IExpr.IAttribute<T>	Factory.attribute(IExpr.IKeyword k, T value)

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

Modifier and Type	Method	Description
List<IExpr.IAttribute<?>>	SMTExpr.Logic.attributeList()
List<IExpr.IAttribute<?>>	SMTExpr.Theory.attributeList()
List<IExpr.IAttribute<? extends IAttributeValue>>	Response.Seq.attributes()
List<IExpr.IAttribute<?>>	SMTExpr.AttributedExpr.attributes()
Map<IExpr.IKeyword,IExpr.IAttribute<?>>	SMTExpr.Logic.attributes()	The attributes, as a Map, keyed by the keyword in the attribute
Map<IExpr.IKeyword,IExpr.IAttribute<?>>	SMTExpr.Theory.attributes()	The attributes, as a Map, keyed by the keyword in the attribute
List<IExpr.IAttribute<?>>	Sort.Family.attributes()

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

Modifier and Type	Method	Description
IResponse.IAttributeList	Response.Factory.get_info_response(IExpr.IAttribute<? extends IAttributeValue> attr)

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

Modifier and Type	Method	Description
IExpr.IAttributedExpr	Factory.attributedExpr(IExpr e, List<IExpr.IAttribute<?>> attributes)
Sort.Family	Factory.createSortFamily(IExpr.IIdentifier identifier, IExpr.INumeral arity, List<IExpr.IAttribute<?>> attributes)
IResponse.IAttributeList	Response.Factory.get_info_response(List<IExpr.IAttribute<? extends IAttributeValue>> attributes)

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

Modifier	Constructor	Description
	Seq(IExpr.IAttribute<T> attr)

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

Modifier	Constructor	Description
	AttributedExpr(IExpr expression, List<IExpr.IAttribute<?>> attributes)	Creates an attributed expression from the given base expression and attribute list.
	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).
	Logic(SMT.Configuration smtConfig, IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)	Creates a logic
	Seq(List<IExpr.IAttribute<? extends IAttributeValue>> list)
	Theory(IExpr.ISymbol name, Collection<IExpr.IAttribute<?>> attributes)	Creates a theory

Uses of IExpr.IAttribute in org.smtlib.logic

Constructor parameters in org.smtlib.logic with type arguments of type IExpr.IAttribute

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

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

Modifier and Type	Method	Description
IExpr.IAttribute<?>	Parser.parseAttribute()	Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.
protected IExpr.IAttribute<?>	Parser.parseAttributeRest(IExpr.IKeyword keyword)	Parses the (optional) value of an attribute whose keyword has already been parsed.

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

Modifier and Type	Method	Description
List<IExpr.IAttribute<?>>	Parser.parseAttributeSequence()	Parse a sequence of attributes (keyword with optional value) terminated by a right parenthesis, returning null with error messages if an error occurs.
List<IExpr.IAttribute<?>>	Parser.parseTermAttributeSequence()	Parses the attributes of an annotated term (! t attr+) up to the right parenthesis.

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

Modifier and Type	Method	Description
Void	Printer.visit(IExpr.IAttribute<? extends IAttributeValue> e)

Uses of IExpr.IAttribute in org.smtlib.solvers

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

Modifier and Type	Method	Description
String	Solver_simplify.Translator.visit(IExpr.IAttribute<?> e)