Uses of Interface
org.smtlib.IAttributeValue

Packages that use IAttributeValue

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

Classes in org.smtlib with type parameters of type IAttributeValue

Modifier and Type	Interface	Description
static interface	IExpr.IAttribute<TT extends IAttributeValue>	This interface represents an SMT-LIB attribute-value pair; the value may be null (keyword-only attribute).

Subinterfaces of IAttributeValue in org.smtlib

Modifier and Type	Interface	Description
interface	IExpr	This interface represents the functionality for any class implementing an SMT-LIB term or formula
static interface	IExpr.IAsIdentifier	This interface represents SMT-LIB identifiers that are sort qualifiers on function ids
static interface	IExpr.IAttributedExpr	This interface represents an SMT-LIB expression with attributes.
static interface	IExpr.IBinaryLiteral	This interface represents SMT-LIB binary literals
static interface	IExpr.IDecimal	This interface represents non-negative decimal numbers of arbitrary size (i.e.
static interface	IExpr.IError	This interface represents an error, e.g.
static interface	IExpr.IExists	This interface represents an SMT-LIB quantified exists expression
static interface	IExpr.IFcnExpr	This interface represents SMT-LIB expressions that are a function identifier applied to one or more arguments.
static interface	IExpr.IForall	This interface represents an SMT-LIB quantified forall expression
static interface	IExpr.IHexLiteral	This interface represents SMT-LIB hex literals
static interface	IExpr.IIdentifier	This interface represents SMT-LIB identifiers (either ids or parameterized ids)
static interface	IExpr.IIndex	Marker interface for the index types in a parameterized identifier: INumeral and ISymbol, plus IHexLiteral, which the Strings theory's (_ char H) uses, and IBinaryLiteral, which no theory uses but which is parsed so that a solver reports it; each theory decides which kinds it accepts.
static interface	IExpr.ILambda	This interface represents an SMT-LIB lambda expression: (lambda (sorted_var+) term).
static interface	IExpr.ILet	This interface represents an SMT-LIB let-expression
static interface	IExpr.ILiteral	This interface represents all literal (explicit constant) expressions.
static interface	IExpr.IMatch	This interface represents an SMT-LIB 2.7 match expression.
static interface	IExpr.INumeral	This interface represents non-negative integers of arbitrary size.
static interface	IExpr.IParameterizedIdentifier	This interface represents SMT-LIB parameterized identifiers
static interface	IExpr.IPatternTerms	This interface represents the value of a :pattern attribute: a list of terms (a multi-pattern), written in the concrete syntax as ( t1 ... tn ).
static interface	IExpr.IQualifiedIdentifier	This interface represents SMT-LIB identifiers for function ids (either ids or parameterized ids or as-type identifiers)
static interface	IExpr.IStringLiteral	This interface represents SMT-LIB string literals
static interface	IExpr.ISymbol	This interface represents SMT-LIB ids; equal ids have equal (using .equals) values of value().

Fields in org.smtlib with type parameters of type IAttributeValue

Modifier and Type	Field	Description
final Map<String,IAttributeValue>	Utils.defaults	The set of default values for all standard options
protected Map<String,IAttributeValue>	AbstractSolver.options	Map that keeps current values of options.

Methods in org.smtlib with type parameters of type IAttributeValue

Modifier and Type	Method	Description
<T extends IAttributeValue> IExpr.IAttribute<T>	IExpr.IFactory.attribute(IExpr.IKeyword k, T value)	Creates an attribute with a keyword and a value.
<T extends IAttributeValue> IExpr.IAttributedExpr	IExpr.IFactory.attributedExpr(IExpr e, IExpr.IKeyword key, T value)	Creates an attributed expression with just one attribute.

Methods in org.smtlib that return IAttributeValue

Modifier and Type	Method	Description
IAttributeValue	IParser.parseAttributeValue()	Parses a value for an attribute, returning null with error messages if an error occurs
IAttributeValue	ICommand.Iset_info.value()	Returns the attribute value.
IAttributeValue	ICommand.Iset_option.value()	Returns the option value, or null if none was provided.
IAttributeValue	ILogic.value(IExpr.IKeyword keyword)	The value of an attribute; returns null if the attribute does not exist for this logic.
IAttributeValue	ITheory.value(IExpr.IKeyword keyword)	The value of an attribute; returns null if the attribute does not exist for this theory

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

Modifier and Type	Method	Description
List<IExpr.IAttribute<? extends IAttributeValue>>	IResponse.IAttributeList.attributes()
default List<IAttributeValue>	ITheory.values(IExpr.IKeyword keyword)	All values for a given attribute keyword (handles multiple occurrences of the same keyword).

Methods in org.smtlib with parameters of type IAttributeValue

Modifier and Type	Method	Description
IResponse	AbstractSolver.checkPrintSuccess(SMT.Configuration smtConfig, IExpr.IKeyword key, IAttributeValue value)	Answers a set-option of :print-success locally (it is never sent), else returns null
IResponse	IResponse.IFactory.get_option_response(IAttributeValue v)
static String	Utils.invalidSetInfoValue(IExpr.IKeyword key, IAttributeValue value)	The reason value is not a valid value for the standard set-info attribute key, or null if it is valid or key is not a standard set-info attribute
IResponse	AbstractSolver.set_info(IExpr.IKeyword key, IAttributeValue value)
ICommand.Iset_info	ICommand.IFactory.set_info(IExpr.IKeyword infoflag, IAttributeValue value)	Creates a set-info command object.
IResponse	ISolver.set_info(IExpr.IKeyword key, IAttributeValue value)	Annotates the problem with an info attribute (e.g.
IResponse	AbstractSolver.set_option(IExpr.IKeyword key, IAttributeValue value)
ICommand.Iset_option	ICommand.IFactory.set_option(IExpr.IKeyword option, IAttributeValue value)	Creates a set-option command object.
IResponse	ISolver.set_option(IExpr.IKeyword option, IAttributeValue value)	Sets an SMT-LIB option.
protected IResponse	AbstractSolver.set_option_impl(IExpr.IKeyword key, IAttributeValue value)	Override in subclasses to handle solver-specific options.

Uses of IAttributeValue in org.smtlib.command

Fields in org.smtlib.command declared as IAttributeValue

Modifier and Type	Field	Description
protected IAttributeValue	C_set_info.value	The value of the info flag
protected IAttributeValue	C_set_option.value	The value of the option

Methods in org.smtlib.command that return IAttributeValue

Modifier and Type	Method	Description
IAttributeValue	C_set_info.value()
IAttributeValue	C_set_option.value()	The new value of the option being set

Methods in org.smtlib.command with parameters of type IAttributeValue

Modifier and Type	Method	Description
IResponse.IError	C_set_option.checkOptionType(SMT.Configuration smtConfig, IExpr.IKeyword keyword, IAttributeValue t)	This method checks that the value for the given keyword has the correct type, when the keyword is used as the key for an SMT-LIB option.

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

Modifier	Constructor	Description
	C_set_info(IExpr.IKeyword keyword, IAttributeValue value)	Construct an instance of the command
	C_set_option(IExpr.IKeyword keyword, IAttributeValue value)	Construct an instance of the command

Uses of IAttributeValue in org.smtlib.impl

Classes in org.smtlib.impl with type parameters of type IAttributeValue

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

Classes in org.smtlib.impl that implement IAttributeValue

Modifier and Type	Class	Description
static class	Pos.AbstractExpr	A Printable that also implements IExpr, additionally holding the sort computed for the expression by the type checker (null if not yet, or never, computed).
class	SMTExpr	This class defines a number of subclasses that implement the SMT-LIB abstract AST; they are used by commands and expressions.
static class	SMTExpr.AsIdentifier	This class represents an SMT as-identifier AST
static class	SMTExpr.AttributedExpr	Represents an SMT-LIB attributed expression ((! expr attrs...)).
static class	SMTExpr.BinaryLiteral	Represents an SMT-LIB binary literal (e.g.
static class	SMTExpr.Decimal	This class represents an SMT Decimal literal expression or syntax token
static class	SMTExpr.Error	Represents an expression-level error node inserted during parsing to allow error recovery.
static class	SMTExpr.Exists	Represents an SMT-LIB existential quantifier expression.
static class	SMTExpr.FcnExpr	Represents a function-application expression: a qualified identifier applied to a list of argument expressions.
static class	SMTExpr.Forall	Represents an SMT-LIB universal quantifier expression.
static class	SMTExpr.HexLiteral	Represents an SMT-LIB hex literal (e.g.
static class	SMTExpr.Lambda	Represents an SMT-LIB lambda expression (SMT-LIB 2.7ff, HO-Core theory).
static class	SMTExpr.Let	Represents an SMT-LIB let expression: a list of bindings and a body expression.
static class	SMTExpr.Literal<T>	Abstract base class for all literal value AST nodes; holds the typed value and provides a shared implementation.
static class	SMTExpr.Match	Represents an SMT-LIB 2.7 match expression: an expression matched against a list of cases.
static class	SMTExpr.Numeral	This class represents an SMT Numeral expression or syntax token
static class	SMTExpr.ParameterizedIdentifier	This class represents an SMT parameterized-identifier AST (e.g.
static class	SMTExpr.PatternTerms	Represents the value of a :pattern attribute: a list of trigger terms.
static class	SMTExpr.StringLiteral	This class represents an SMT String literal expression or syntax token
static class	SMTExpr.Symbol	This class represents an SMT Symbol

Fields in org.smtlib.impl declared as IAttributeValue

Modifier and Type	Field	Description
protected TT	SMTExpr.Attribute.value

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

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

Methods in org.smtlib.impl that return IAttributeValue

Modifier and Type	Method	Description
IAttributeValue	SMTExpr.Logic.value(IExpr.IKeyword keyword)	The value of a given attribute
IAttributeValue	SMTExpr.Theory.value(IExpr.IKeyword keyword)	The value of a given attribute (last occurrence wins for duplicate keywords)

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

Modifier and Type	Method	Description
List<IExpr.IAttribute<? extends IAttributeValue>>	Response.Seq.attributes()
List<IAttributeValue>	SMTExpr.Theory.values(IExpr.IKeyword keyword)	All values for a given attribute keyword, in source order

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

Modifier and Type	Method	Description
IResponse	Response.Factory.get_option_response(IAttributeValue v)
ICommand.Iset_info	Factory.set_info(IExpr.IKeyword k, IAttributeValue v)
ICommand.Iset_option	Factory.set_option(IExpr.IKeyword k, IAttributeValue v)

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

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

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

Modifier	Constructor	Description
	Seq(List<IExpr.IAttribute<? extends IAttributeValue>> list)

Uses of IAttributeValue in org.smtlib.sexpr

Subinterfaces of IAttributeValue in org.smtlib.sexpr

Modifier and Type	Interface	Description
interface	ISexpr	This interface represents S-expressions as used in SMT-LIB; they are used as values for attributes in the standard concrete syntax.
static interface	ISexpr.ISeq	Represents a sequence of S-expressions
static interface	ISexpr.IToken<T>	Represents a single S-expression token

Classes in org.smtlib.sexpr that implement IAttributeValue

Modifier and Type	Class	Description
class	Sexpr	This is the root class for S-expressions in the concrete syntax
static class	Sexpr.Seq	The class corresponding to sequences of S-expressions
static class	Sexpr.Token<T>	Represents a single S-expression token with intrinsic type T

Methods in org.smtlib.sexpr that return IAttributeValue

Modifier and Type	Method	Description
IAttributeValue	Parser.parseAttributeValue()	Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.

Method parameters in org.smtlib.sexpr with type arguments of type IAttributeValue

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

Uses of IAttributeValue in org.smtlib.solvers

Fields in org.smtlib.solvers with type parameters of type IAttributeValue

Modifier and Type	Field	Description
protected Map<String,IAttributeValue>	Solver_test.options	The data structure that maintains the current values of options and info items for this solver.

Methods in org.smtlib.solvers with parameters of type IAttributeValue

Modifier and Type	Method	Description
IResponse	Solver_simplify.set_info(IExpr.IKeyword key, IAttributeValue value)	See Solver_test.set_info(IKeyword,IAttributeValue).
IResponse	Solver_test.set_info(IExpr.IKeyword key, IAttributeValue value)
IResponse	Solver_simplify.set_option(IExpr.IKeyword option, IAttributeValue value)	Simplify has no set-option; options are kept here, and the :produce- options answer unsupported since Simplify cannot produce models, proofs or cores
IResponse	Solver_test.set_option(IExpr.IKeyword key, IAttributeValue value)
protected IResponse	Solver_altergo.set_option_impl(IExpr.IKeyword key, IAttributeValue value)	Sent to Alt-Ergo, and kept here for get_option when Alt-Ergo accepts it
protected IResponse	Solver_bitwuzla.set_option_impl(IExpr.IKeyword key, IAttributeValue value)	Sent to bitwuzla, and also kept here for get_option, which bitwuzla does not support
protected IResponse	Solver_cvc5.set_option_impl(IExpr.IKeyword key, IAttributeValue value)
protected IResponse	Solver_z3_4_3_2.set_option_impl(IExpr.IKeyword key, IAttributeValue value)	Corrects a non-conformance of z3 4.3.2: set-option of an option it does not know answers an error, (error "line L column C: unknown parameter 'foo'\nLegal parameters are:\n ..."), which names the option and then lists every parameter of its module, one per line.
protected IResponse	Solver_z3_4_3.set_option_impl(IExpr.IKeyword key, IAttributeValue value)	z3 4.3 accepts :interactive-mode, :produce-assertions and the other :produce- options after set-logic, which SMT-LIB forbids, so that is reported here; values are kept here for get_option.