Uses of Interface
org.smtlib.IExpr.IKeyword

Packages that use IExpr.IKeyword

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

Fields in org.smtlib declared as IExpr.IKeyword

Modifier and Type	Field	Description
static final IExpr.IKeyword	Utils.ALL_STATISTICS	The string designating an info item
static final IExpr.IKeyword	Utils.ASSERTION_STACK_LEVELS	The string designating an info item
static final IExpr.IKeyword	Utils.AUTHORS	The string designating an info item
static final IExpr.IKeyword	Utils.ERROR_BEHAVIOR	The string designating an info item
static final IExpr.IKeyword	Utils.FUNS	The attribute tag for defining functions in a theory
static final IExpr.IKeyword	Utils.NAME	The string designating an info item
protected final IExpr.IKeyword	AbstractSolver.printSuccess
static final IExpr.IKeyword	Utils.REASON_UNKNOWN	The string designating an info item
static final IExpr.IKeyword	Utils.SMTLIB_VERSION	The string designating the smtlib attribute within a logic or theory
static final IExpr.IKeyword	Utils.SORTS	The attribute tag for defining sorts in a theory
static final IExpr.IKeyword	Utils.STATUS	The string designating an info item
static final IExpr.IKeyword	Utils.THEORIES	The attribute tag for defining theories in a logic
static final IExpr.IKeyword	Utils.VERSION	The string designating an info item

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

Modifier and Type	Field	Description
static final HashSet<IExpr.IKeyword>	Utils.infoKeywords
static final HashSet<IExpr.IKeyword>	Utils.setInfoKeywords	The attributes the standard defines for set-info (any other is allowed, but not standard)

Methods in org.smtlib that return IExpr.IKeyword

Modifier and Type	Method	Description
IExpr.IKeyword	ICommand.Iget_info.infoflag()	Returns the info flag keyword being queried.
IExpr.IKeyword	ICommand.Iset_info.infoflag()	Returns the info flag keyword.
IExpr.IKeyword	IExpr.IAttribute.keyword()
IExpr.IKeyword	IExpr.IFactory.keyword(String v)	Creates an IKeyword object from a canonical string representation.
IExpr.IKeyword	ICommand.Iget_option.option()	Returns the option keyword being queried.
IExpr.IKeyword	ICommand.Iset_option.option()	Returns the option keyword.
IExpr.IKeyword	IParser.parseKeyword()	Parse an SMT-LIB keyword; return null and log an error response if there is no valid keyword

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

Modifier and Type	Method	Description
Map<IExpr.IKeyword,IExpr.IAttribute<?>>	ILogic.attributes()	The attributes of the logic
Map<IExpr.IKeyword,IExpr.IAttribute<?>>	ITheory.attributes()	The attributes (keyword-value pairs) of the theory.

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

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.
<T extends IAttributeValue> IExpr.IAttributedExpr	IExpr.IFactory.attributedExpr(IExpr e, IExpr.IKeyword key, T value)	Creates an attributed expression with just one attribute.
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	AbstractSolver.get_info(IExpr.IKeyword option)
ICommand.Iget_info	ICommand.IFactory.get_info(IExpr.IKeyword infoflag)	Creates a get-info command object.
IResponse	ISolver.get_info(IExpr.IKeyword option)	Returns the value of the named info item.
IResponse	AbstractSolver.get_option(IExpr.IKeyword option)
ICommand.Iget_option	ICommand.IFactory.get_option(IExpr.IKeyword option)	Creates a get-option command object.
IResponse	ISolver.get_option(IExpr.IKeyword option)	Returns the current value of the named option.
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
protected static String	AbstractSolver.normalizeForTesting(String raw, IExpr.IKeyword infoflag)	Replaces known sources of non-deterministic content in a raw solver response with a fixed placeholder, so that --testing runs produce byte-for-byte reproducible output across machines and repeated runs.
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.
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
default List<IAttributeValue>	ITheory.values(IExpr.IKeyword keyword)	All values for a given attribute keyword (handles multiple occurrences of the same keyword).
T	IVisitor.TreeVisitor.visit(IExpr.IKeyword e)
T	IVisitor.visit(IExpr.IKeyword e)
ISort	TypeChecker.visit(IExpr.IKeyword e)

Uses of IExpr.IKeyword in org.smtlib.command

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

Modifier and Type	Field	Description
protected IExpr.IKeyword	C_get_info.infoflag	The keyword for the info item to fetch
protected IExpr.IKeyword	C_set_info.infoflag	The keyword info flag
protected IExpr.IKeyword	C_get_option.option	The keyword for the option to fetch
protected IExpr.IKeyword	C_set_option.option	The keyword for the option to set

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

Modifier and Type	Method	Description
IExpr.IKeyword	C_get_info.infoflag()	The keyword for the info item to fetch
IExpr.IKeyword	C_set_info.infoflag()
IExpr.IKeyword	C_get_option.option()	The keyword for the option to fetch
IExpr.IKeyword	C_set_option.option()	The keyword for the option to set

Methods in org.smtlib.command with parameters of type IExpr.IKeyword

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 IExpr.IKeyword

Modifier	Constructor	Description
	C_get_info(IExpr.IKeyword infoflag)	Constructs a command instance given the keyword
	C_get_option(IExpr.IKeyword keyword)	Constructs a command instance for the given keyword
	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 IExpr.IKeyword in org.smtlib.impl

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

Modifier and Type	Class	Description
static class	SMTExpr.Keyword	This class represents an SMT Keyword syntax token

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

Modifier and Type	Field	Description
protected IExpr.IKeyword	SMTExpr.Attribute.keyword

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

Modifier and Type	Field	Description
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

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

Modifier and Type	Method	Description
IExpr.IKeyword	Factory.keyword(String v)
IExpr.IKeyword	SMTExpr.Attribute.keyword()

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

Modifier and Type	Method	Description
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

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

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)
<T extends IAttributeValue> IExpr.IAttributedExpr	Factory.attributedExpr(IExpr e, IExpr.IKeyword key, T value)
ICommand.Iget_info	Factory.get_info(IExpr.IKeyword k)
ICommand.Iget_option	Factory.get_option(IExpr.IKeyword k)
ICommand.Iset_info	Factory.set_info(IExpr.IKeyword k, IAttributeValue v)
ICommand.Iset_option	Factory.set_option(IExpr.IKeyword k, IAttributeValue v)
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)
List<IAttributeValue>	SMTExpr.Theory.values(IExpr.IKeyword keyword)	All values for a given attribute keyword, in source order

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

Modifier	Constructor	Description
	Attribute(IExpr.IKeyword keyword, TT value)	Creates an attribute from the given keyword and (possibly null) value.

Uses of IExpr.IKeyword in org.smtlib.sexpr

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

Modifier and Type	Method	Description
protected IExpr.IAttribute<?>	Parser.parseAttributeRest(IExpr.IKeyword keyword)	Parses the (optional) value of an attribute whose keyword has already been parsed.
Void	Printer.visit(IExpr.IKeyword e)

Uses of IExpr.IKeyword in org.smtlib.solvers

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

Modifier and Type	Method	Description
IResponse	Solver_bitwuzla.get_info(IExpr.IKeyword key)	Answered entirely client-side (never forwarded -- see class comment point 1).
IResponse	Solver_simplify.get_info(IExpr.IKeyword key)	Simplify has no get-info; answered here
IResponse	Solver_test.get_info(IExpr.IKeyword key)
IResponse	Solver_yices2.get_info(IExpr.IKeyword key)	yices2 answers get-info :status with the last set-info :status value, but with (error "no info for :status") when none was set; SMT-LIB requires unsupported for a flag the solver does not support.
IResponse	Solver_z3_4_3.get_info(IExpr.IKeyword key)	Not a correction: this adapter sends commands by its own means, so it scrubs run-dependent values for testing itself, as AbstractSolver.get_info does
IResponse	Solver_z3_recent.get_info(IExpr.IKeyword key)	z3 reports a query stopped by its per-query time limit, -t:, with :reason-unknown "canceled" in incremental mode (after a push; checked with z3 4.16.0 and 5.1.0, while 4.8.12 and 4.12.6 give up first, as incomplete), and in every mode in 4.6 and 4.7; one-shot queries in newer versions, and other solvers such as cvc5, report "timeout".
IResponse	Solver_altergo.get_option(IExpr.IKeyword key)	Alt-Ergo ignores get-option, writing nothing; answered from the values set (see set_option_impl) and the SMT-LIB defaults
IResponse	Solver_bitwuzla.get_option(IExpr.IKeyword key)	Answered entirely client-side (never forwarded -- see class comment point 1): from whatever this run has set via Solver_bitwuzla.set_option_impl(org.smtlib.IExpr.IKeyword, org.smtlib.IAttributeValue), falling back to the standard SMT-LIB default for any option never set, and "unsupported" for anything not a recognized standard option at all (matching what a compliant solver would say about an option it doesn't have).
IResponse	Solver_cvc5.get_option(IExpr.IKeyword option)	See the class Javadoc: wraps a bare-symbol answer for a string-typed option (Utils.stringOptions -- currently just :regular-output-channel and :diagnostic-output-channel) into a proper SMT-LIB string literal with the same text, working around cvc5 answering those two with an unquoted symbol instead.
IResponse	Solver_simplify.get_option(IExpr.IKeyword key)	Simplify has no get-option; answered from the values kept by set_option
IResponse	Solver_test.get_option(IExpr.IKeyword key)
IResponse	Solver_z3_4_3.get_option(IExpr.IKeyword key)	Sent to the solver, except where z3 4.3's answer does not conform: it defaults :produce-models to true (SMT-LIB: false), writes the channel names unquoted, knows :produce-assertions only as :interactive-mode (see set_option_impl), and answers unsupported, not the default value, for a standard option it lacks
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.
String	Solver_simplify.Translator.visit(IExpr.IKeyword e)