I-Index

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form

I

IAttributeValue - Interface in org.smtlib: This interface represents the general class of attribute values; that is, it is the super-interface of any class that may be an attribute value; in the abstract syntax it has no particular structure, though it does include true, false, string literals, numerals, and various pre-defined constants.
ICommand - Interface in org.smtlib: This interface is the generic interface to command classes, providing functionality to type-check the command and to execute it.
ICommand.Iassert - Interface in org.smtlib: Interface for the SMT-LIB assert command.
ICommand.Icheck_sat - Interface in org.smtlib: Interface for the SMT-LIB check-sat command.
ICommand.Icheck_sat_assuming - Interface in org.smtlib: Interface for the SMT-LIB check-sat-assuming command.
ICommand.Icomment - Interface in org.smtlib: Interface for a comment pseudo-command: not part of the SMT-LIB command grammar itself, but modeled as a real, typed ICommand (see issue #115) so that every dispatch path -- execution, typed-visitor traversal, and printing -- treats it uniformly with every other command, rather than falling back on IVisitor's generic visit(ICommand) handling (a reflection-based lookup in Printer's case).
ICommand.Ideclare_const - Interface in org.smtlib: Interface for the SMT-LIB declare-const command.
ICommand.Ideclare_datatype - Interface in org.smtlib: Interface for the SMT-LIB declare-datatype command.
ICommand.Ideclare_datatypes - Interface in org.smtlib: Interface for the SMT-LIB declare-datatypes command.
ICommand.Ideclare_fun - Interface in org.smtlib: Interface for the SMT-LIB declare-fun command.
ICommand.Ideclare_sort - Interface in org.smtlib: Interface for the SMT-LIB declare-sort command.
ICommand.Ideclare_sort_parameter - Interface in org.smtlib: Interface for the SMT-LIB declare-sort-parameter command.
ICommand.Idefine_const - Interface in org.smtlib: Interface for the SMT-LIB define-const command.
ICommand.Idefine_fun - Interface in org.smtlib: Interface for the SMT-LIB define-fun command.
ICommand.Idefine_fun_rec - Interface in org.smtlib: Interface for the SMT-LIB define-fun-rec command.
ICommand.Idefine_funs_rec - Interface in org.smtlib: Interface for the SMT-LIB define-funs-rec command.
ICommand.Idefine_sort - Interface in org.smtlib: Interface for the SMT-LIB define-sort command.
ICommand.Iecho - Interface in org.smtlib: Interface for the SMT-LIB echo command.
ICommand.Iexit - Interface in org.smtlib: Interface for the SMT-LIB exit command.
ICommand.IFactory - Interface in org.smtlib: This is the interface to be used by a concrete ICommand factory.
ICommand.IFinder - Interface in org.smtlib: This interface defines classes that implement techniques for mapping a command name to a class that implements that command.
ICommand.Iget_assertions - Interface in org.smtlib: Interface for the SMT-LIB get-assertions command.
ICommand.Iget_assignment - Interface in org.smtlib: Interface for the SMT-LIB get-assignment command.
ICommand.Iget_info - Interface in org.smtlib: Interface for the SMT-LIB get-info command.
ICommand.Iget_model - Interface in org.smtlib: Interface for the SMT-LIB get-model command (non-standard extension).
ICommand.Iget_option - Interface in org.smtlib: Interface for the SMT-LIB get-option command.
ICommand.Iget_proof - Interface in org.smtlib: Interface for the SMT-LIB get-proof command.
ICommand.Iget_unsat_assumptions - Interface in org.smtlib: Interface for the SMT-LIB get-unsat-assumptions command.
ICommand.Iget_unsat_core - Interface in org.smtlib: Interface for the SMT-LIB get-unsat-core command.
ICommand.Iget_value - Interface in org.smtlib: Interface for the SMT-LIB get-value command.
ICommand.Ipop - Interface in org.smtlib: Interface for the SMT-LIB pop command.
ICommand.Ipush - Interface in org.smtlib: Interface for the SMT-LIB push command.
ICommand.Ireset - Interface in org.smtlib: Interface for the SMT-LIB reset command.
ICommand.Ireset_assertions - Interface in org.smtlib: Interface for the SMT-LIB reset-assertions command.
ICommand.IScript - Interface in org.smtlib: Interface to be implemented by all objects representing SMT-LIB scripts.
ICommand.Iset_info - Interface in org.smtlib: Interface for the SMT-LIB set-info command.
ICommand.Iset_logic - Interface in org.smtlib: Interface for the SMT-LIB set-logic command.
ICommand.Iset_option - Interface in org.smtlib: Interface for the SMT-LIB set-option command.
id - Variable in class org.smtlib.impl.SMTExpr.FcnExpr
id - Variable in class org.smtlib.impl.Sort.ErrorDefinition
id - Variable in enum class org.smtlib.SMT.Configuration.SMTLIB: The canonical string identifier for this version (e.g.
id(IExpr.IIdentifier, ISort) - Method in interface org.smtlib.IExpr.IFactory: Creates an 'as' identifier from an identifier and a sort qualifier.
id(IExpr.IIdentifier, ISort) - Method in class org.smtlib.impl.Factory
id(IExpr.ISymbol, List<IExpr.IIndex>) - Method in interface org.smtlib.IExpr.IFactory: Creates a parameterized identifier from a symbol and a non-empty list of indices (each INumeral or ISymbol).
id(IExpr.ISymbol, List<IExpr.IIndex>) - Method in class org.smtlib.impl.Factory
identifier - Variable in class org.smtlib.impl.Sort.Abbreviation
identifier - Variable in class org.smtlib.impl.Sort.Family
identifier() - Method in class org.smtlib.impl.Sort.Abbreviation
identifier() - Method in class org.smtlib.impl.Sort.ErrorDefinition
identifier() - Method in class org.smtlib.impl.Sort.Family
identifier() - Method in class org.smtlib.impl.Sort.Parameter
identifier() - Method in interface org.smtlib.ISort.IAbbreviation: The identifier of the abbreviation
identifier() - Method in interface org.smtlib.ISort.IDefinition: The identifier for the sort symbol
identifier() - Method in interface org.smtlib.ISort.IFamily: The unique identifier for this sort symbol
ids - Variable in class org.smtlib.ext.C_what: The ids that are the arguments of the command
ids() - Method in class org.smtlib.ext.C_what: The ids that are the arguments of the command
ids() - Method in interface org.smtlib.ext.Iwhat: Returns the identifiers to look up and describe.
Iexec - Interface in org.smtlib.ext: Interface for the SMT-LIB exec command (non-standard extension).
IExpr - Interface in org.smtlib: This interface represents the functionality for any class implementing an SMT-LIB term or formula
IExpr.IAsIdentifier - Interface in org.smtlib: This interface represents SMT-LIB identifiers that are sort qualifiers on function ids
IExpr.IAttribute<TT> - Interface in org.smtlib: This interface represents an SMT-LIB attribute-value pair; the value may be null (keyword-only attribute).
IExpr.IAttributedExpr - Interface in org.smtlib: This interface represents an SMT-LIB expression with attributes.
IExpr.IBinaryLiteral - Interface in org.smtlib: This interface represents SMT-LIB binary literals
IExpr.IBinding - Interface in org.smtlib: This interface represents a binding of a parameter and an expression
IExpr.IConstructor - Interface in org.smtlib: A constructor declaration within a datatype; pairs a constructor name with its selectors.
IExpr.IDecimal - Interface in org.smtlib: This interface represents non-negative decimal numbers of arbitrary size (i.e.
IExpr.IDeclaration - Interface in org.smtlib: This interface represents a declaration of a parameter and its sort
IExpr.IError - Interface in org.smtlib: This interface represents an error, e.g.
IExpr.IExists - Interface in org.smtlib: This interface represents an SMT-LIB quantified exists expression
IExpr.IFactory - Interface in org.smtlib: The interface defining the factory type for producing objects of various subtypes of IExpr; the IPos argument is an optional argument giving information about the textual position of an expression.
IExpr.IFcnExpr - Interface in org.smtlib: This interface represents SMT-LIB expressions that are a function identifier applied to one or more arguments.
IExpr.IForall - Interface in org.smtlib: This interface represents an SMT-LIB quantified forall expression
IExpr.IFunctionDeclaration - Interface in org.smtlib: A function declaration: a name, a parameter list (sorted variables), and a result sort; used in the header list of define-funs-rec.
IExpr.IHexLiteral - Interface in org.smtlib: This interface represents SMT-LIB hex literals
IExpr.IIdentifier - Interface in org.smtlib: This interface represents SMT-LIB identifiers (either ids or parameterized ids)
IExpr.IIndex - Interface in org.smtlib: 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.
IExpr.IKeyword - Interface in org.smtlib: This interface represents SMT-LIB attribute and infoflag names.
IExpr.ILambda - Interface in org.smtlib: This interface represents an SMT-LIB lambda expression: (lambda (sorted_var+) term).
IExpr.ILet - Interface in org.smtlib: This interface represents an SMT-LIB let-expression
IExpr.ILiteral - Interface in org.smtlib: This interface represents all literal (explicit constant) expressions.
IExpr.IMatch - Interface in org.smtlib: This interface represents an SMT-LIB 2.7 match expression.
IExpr.IMatchCase - Interface in org.smtlib: This interface represents one case in a match expression: a pattern and its body.
IExpr.INumeral - Interface in org.smtlib: This interface represents non-negative integers of arbitrary size.
IExpr.IParameterizedIdentifier - Interface in org.smtlib: This interface represents SMT-LIB parameterized identifiers
IExpr.IPattern - Interface in org.smtlib: This interface represents a match pattern: either a bare symbol (variable/nullary-constructor) or a constructor applied to zero or more variable symbols.
IExpr.IPatternTerms - Interface in org.smtlib: This interface represents the value of a :pattern attribute: a list of terms (a multi-pattern), written in the concrete syntax as ( t1 ... tn ).
IExpr.IQualifiedIdentifier - Interface in org.smtlib: This interface represents SMT-LIB identifiers for function ids (either ids or parameterized ids or as-type identifiers)
IExpr.ISelector - Interface in org.smtlib: A selector declaration within a constructor; pairs a selector name with its result sort.
IExpr.ISortDeclaration - Interface in org.smtlib: Pairs a sort name with its arity; used in declare-datatype and declare-datatypes.
IExpr.IStringLiteral - Interface in org.smtlib: This interface represents SMT-LIB string literals
IExpr.ISymbol - Interface in org.smtlib: This interface represents SMT-LIB ids; equal ids have equal (using .equals) values of value().
ILanguage - Interface in org.smtlib: This interface represents the functionality of an SMT-LIB language - the combination of one or more theories and various restrictions on the permitted expressions.
ILexToken - Interface in org.smtlib.sexpr: An interface to indicate AST classes that are also lexical tokens in the concrete syntax.
ILogic - Interface in org.smtlib: This interface represents a definition of an SMT_LIB logic
immediate_exit() - Method in class org.smtlib.impl.Response.Factory
immediate_exit() - Method in interface org.smtlib.IResponse.IFactory
IMMEDIATE_EXIT - Static variable in class org.smtlib.impl.Response
IMMEDIATE_EXIT - Static variable in class org.smtlib.Utils: An ERROR_BEHAVIOR return value
IMPLIES - Static variable in class org.smtlib.Utils
incomplete() - Method in class org.smtlib.impl.Response.Factory
incomplete() - Method in interface org.smtlib.IResponse.IFactory
INCOMPLETE - Static variable in class org.smtlib.impl.Response
INCOMPLETE - Static variable in class org.smtlib.Utils: A REASON_UNKNOWN return value
indent(String) - Method in interface org.smtlib.Log.IListener: Sets the indent prefix used when displaying error-location carets; typically the current prompt string.
indent(String) - Method in class org.smtlib.Log: Sends the call to any listeners.
indent(String) - Method in class org.smtlib.Log.StandardListener
indices - Variable in class org.smtlib.impl.SMTExpr.ParameterizedIdentifier
indices() - Method in interface org.smtlib.IExpr.IParameterizedIdentifier: All indices of the identifier: INumeral or ISymbol, or the literals IIndex describes.
indices() - Method in class org.smtlib.impl.SMTExpr.ParameterizedIdentifier
infoflag - Variable in class org.smtlib.command.C_get_info: The keyword for the info item to fetch
infoflag - Variable in class org.smtlib.command.C_set_info: The keyword info flag
infoflag() - Method in class org.smtlib.command.C_get_info: The keyword for the info item to fetch
infoflag() - Method in class org.smtlib.command.C_set_info
infoflag() - Method in interface org.smtlib.ICommand.Iget_info: Returns the info flag keyword being queried.
infoflag() - Method in interface org.smtlib.ICommand.Iset_info: Returns the info flag keyword.
infoKeywords - Static variable in class org.smtlib.Utils
initFactories(SMT.Configuration) - Static method in class org.smtlib.impl.Factory: Initializes the SMT configuration object for the implementation in org.smtlib.impl - all the appropriate factories, etc.
initFactories(SMT.Configuration) - Static method in class org.smtlib.sexpr.Factory: This method will initialize the factories and default printer in the configuration with appropriate objects from this implementation; it should be called as part of initial set up of the configuration.
initialInputBufferSize - Variable in class org.smtlib.SMT.Configuration: Initial capacity in characters for the input reader's internal buffer.
INode - Interface in org.smtlib: This interface is defined and implemented as a marker that the accept method is available and to ensure that subtypes implement the accept method.
inSatMode() - Method in class org.smtlib.AbstractSolver: Whether the most recent check command was answered sat or unknown, with the assertion stack unchanged since: SMT-LIB's sat mode (false once the whole-run time limit has ended the solver)
INT_TO_BV - Static variable in class org.smtlib.Utils
intArity() - Method in class org.smtlib.impl.Sort.Abbreviation
intArity() - Method in class org.smtlib.impl.Sort.ErrorDefinition
intArity() - Method in class org.smtlib.impl.Sort.Family
intArity() - Method in class org.smtlib.impl.Sort.Parameter
intArity() - Method in interface org.smtlib.ISort.IDefinition: The arity of the symbol
interactive - Variable in class org.smtlib.SMT.Configuration: This variable records whether we are reading from standard input, in which case the input text is usually already present.
INTERACTIVE_MODE - Static variable in class org.smtlib.Utils: The string designating an option item
InternalException(String) - Constructor for exception class org.smtlib.SMT.InternalException
interrupt() - Method in class org.smtlib.AbstractSolver: Interrupts the command the solver is running (see SolverProcess.interrupt())
interrupt() - Method in class org.smtlib.SolverProcess: Interrupts the command the solver is running by sending it SIGINT: z3 then abandons the command (check-sat answers unknown) and goes on; most other solvers exit.
intValue - Variable in class org.smtlib.impl.SMTExpr.BinaryLiteral
intValue - Variable in class org.smtlib.impl.SMTExpr.HexLiteral
intValue() - Method in interface org.smtlib.IExpr.IBinaryLiteral: The binary value as an unsigned integer
intValue() - Method in interface org.smtlib.IExpr.IHexLiteral: The hex value as an unsigned integer
intValue() - Method in interface org.smtlib.IExpr.INumeral
intValue() - Method in class org.smtlib.impl.SMTExpr.BinaryLiteral
intValue() - Method in class org.smtlib.impl.SMTExpr.HexLiteral
intValue() - Method in class org.smtlib.impl.SMTExpr.Numeral
inUnsatMode() - Method in class org.smtlib.AbstractSolver: Whether the most recent check command was answered unsat, with the assertion stack unchanged since: SMT-LIB's unsat mode (false once the whole-run time limit has ended the solver)
invalidSetInfoValue(IExpr.IKeyword, IAttributeValue) - Static method in class org.smtlib.Utils: 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
IParser - Interface in org.smtlib: This is the interface to a parser for SMT-LIB.
IParser.AbortInputException - Exception Class in org.smtlib: An exception to be thrown if parsing is to be intentionally aborted (and restarted, ignoring any tokens since the last successful call to the parser.
IParser.ElementParser<T> - Interface in org.smtlib: Functional interface for a lambda that parses one element from a Parser.
IParser.IFactory - Interface in org.smtlib: The interface for the parser/printer factory
IParser.ParserException - Exception Class in org.smtlib: An exception thrown if parsing is to be aborted.
IParser.SyntaxException - Exception Class in org.smtlib: An exception to be thrown if there is an unrecoverable problem scanning the syntax
IPos - Interface in org.smtlib: This is an interface that supplies information about a range in textual position within a source of characters.
IPos.IPosable - Interface in org.smtlib: This interface identifies classes that can have their position set
IPrinter - Interface in org.smtlib: An interface for printers to concrete syntax; factories are shared with Parsers in IParser.IFactory.
IResponse - Interface in org.smtlib: This interface represents responses that can be received from SMT-LIB commands.
IResponse.IAssertionsResponse - Interface in org.smtlib: Response type for get-assertions, carrying the list of currently asserted formulae.
IResponse.IAssignmentResponse - Interface in org.smtlib: Response type for get-assignment, carrying a list of name-Boolean pairs.
IResponse.IAttributeList - Interface in org.smtlib: Response type for get-info, carrying a list of attribute key-value pairs.
IResponse.IError - Interface in org.smtlib: The interface for error responses
IResponse.IFactory - Interface in org.smtlib: The factory interface for creating the standard IResponse singleton and structured instances.
IResponse.IPair<T1,T2> - Interface in org.smtlib: An interface for simple pairs of objects; used to represent value/assignment response items
IResponse.IProofResponse - Interface in org.smtlib: Response type for get-proof.
IResponse.IUnsatAssumptionsResponse - Interface in org.smtlib: Response type for get-unsat-assumptions, carrying the assumptions (terms, e.g.
IResponse.IUnsatCoreResponse - Interface in org.smtlib: Response type for get-unsat-core, carrying the names of the formulae in the unsat core.
IResponse.IValueResponse - Interface in org.smtlib: Response type for get-value, carrying a list of expression-value pairs.
IS - Static variable in class org.smtlib.Utils: The String for the head of a datatype tester, (_ is C)
isBarQuoted(String) - Static method in class org.smtlib.impl.SMTExpr.Symbol: Whether v is enclosed in a pair of bars
isBitVecArray(ISort.IApplication) - Static method in class org.smtlib.logic.Logic: Whether array is (Array (_ BitVec i) (_ BitVec j)), as QF_ABV and QF_AUFBV require
isBitVecSort(ISort) - Static method in class org.smtlib.logic.Logic: Whether sort, with abbreviations expanded, is a (_ BitVec n) sort
isBool() - Method in class org.smtlib.impl.Sort: Returns true iff the receiver is a Sort expression designating the pre-defined Bool sort
isBool() - Method in interface org.smtlib.ISort: Returns true if the receiver designates the Bool pre-defined Sort.
isConst(IExpr) - Method in class org.smtlib.logic.LRA
isDifferenceOfSymbols(IExpr) - Static method in class org.smtlib.logic.DifferenceLogic: True for (- x y) with x and y symbols
isEOD() - Method in interface org.smtlib.IParser: Returns true if the parser is at the end of data
isEOD() - Method in interface org.smtlib.sexpr.ILexToken: Returns true if this token signals the end of the input.
isEOD() - Method in class org.smtlib.sexpr.Lexer: Returns true if the next token is the end-of-data
isError() - Method in class org.smtlib.AbstractSolver.Pending
isError() - Method in interface org.smtlib.IAttributeValue
isError() - Method in interface org.smtlib.IExpr
isError() - Method in class org.smtlib.impl.Response.AssertionsResponse
isError() - Method in class org.smtlib.impl.Response.AssignmentResponse
isError() - Method in class org.smtlib.impl.Response.Error
isError() - Method in class org.smtlib.impl.Response.ProofResponse
isError() - Method in class org.smtlib.impl.Response.Seq
isError() - Method in class org.smtlib.impl.Response.UnsatAssumptionsResponse
isError() - Method in class org.smtlib.impl.Response.UnsatCoreResponse
isError() - Method in class org.smtlib.impl.Response.ValueResponse
isError() - Method in class org.smtlib.impl.SMTExpr.Attribute
isError() - Method in class org.smtlib.impl.SMTExpr.Literal
isError() - Method in class org.smtlib.impl.SMTExpr.Symbol
isError() - Method in interface org.smtlib.IResponse: Returns true if the response is an error response
isError() - Method in interface org.smtlib.sexpr.ILexToken: Returns true if this token represents a lexical error.
isError() - Method in class org.smtlib.sexpr.Lexer.LexToken
isError() - Method in class org.smtlib.sexpr.Sexpr.Seq
isError() - Method in class org.smtlib.sexpr.Sexpr.Token
ISexpr - Interface in org.smtlib.sexpr: This interface represents S-expressions as used in SMT-LIB; they are used as values for attributes in the standard concrete syntax.
ISexpr.ISeq - Interface in org.smtlib.sexpr: Represents a sequence of S-expressions
ISexpr.IToken<T> - Interface in org.smtlib.sexpr: Represents a single S-expression token
isFlatResponse(String) - Method in class org.smtlib.AbstractSolver: True if the given raw response text is a flat outcome (empty/success/unsupported/an (error ...) s-expression) rather than a structured list — used by the get_assertions/get_value/get_assignment/get_unsat_core/get_unsat_assumptions defaults below to decide whether to delegate to AbstractSolver.parseResponse(String) or reparse the response as the structured list they actually expect.
isFlatResponse(String) - Method in class org.smtlib.solvers.Solver_bitwuzla: Bitwuzla writes its errors as "[error] ..." lines (class comment point 3), so for the get- commands that parse a list reply such a line goes to Solver_bitwuzla.parseResponse(java.lang.String), not the list parser.
isFreeConstant(IExpr) - Method in class org.smtlib.logic.Logic
isHolding() - Method in class org.smtlib.Log: Whether output is held (see Log.hold(IPendingOutput))
isInteger(IExpr) - Method in class org.smtlib.logic.Logic
isLinearInteger(IExpr) - Method in class org.smtlib.logic.Logic
isLinearReal(IExpr) - Method in class org.smtlib.logic.Logic
isLogicSymbol(IExpr.ISymbol, boolean) - Method in class org.smtlib.SymbolTable: Whether the symbol is a function (sort, if sort is true) symbol of the logic or its theories
isLP() - Method in interface org.smtlib.sexpr.ILexToken: Returns true if this token is a left parenthesis.
isLP() - Method in class org.smtlib.sexpr.Lexer: Returns true if the next token is a left parenthesis (without consuming it)
isLP() - Method in class org.smtlib.sexpr.Lexer.LexToken
isMac - Static variable in class org.smtlib.AbstractSolver
isOK() - Method in class org.smtlib.AbstractSolver.Pending
isOK() - Method in interface org.smtlib.IAttributeValue
isOK() - Method in class org.smtlib.impl.Response.AssertionsResponse
isOK() - Method in class org.smtlib.impl.Response.AssignmentResponse
isOK() - Method in class org.smtlib.impl.Response.Error
isOK() - Method in class org.smtlib.impl.Response.ProofResponse
isOK() - Method in class org.smtlib.impl.Response.Seq
isOK() - Method in class org.smtlib.impl.Response.UnsatAssumptionsResponse
isOK() - Method in class org.smtlib.impl.Response.UnsatCoreResponse
isOK() - Method in class org.smtlib.impl.Response.ValueResponse
isOK() - Method in class org.smtlib.impl.SMTExpr.Attribute
isOK() - Method in class org.smtlib.impl.SMTExpr.Symbol
isOK() - Method in interface org.smtlib.IResponse: Returns true if the response is a SUCCESS response
isOK() - Method in class org.smtlib.sexpr.Sexpr.Seq
isOK() - Method in class org.smtlib.sexpr.Sexpr.Token
isOKKeyword(String) - Method in class org.smtlib.SMT.Configuration: True if the string (including the colon) is a legal keyword: a colon followed by a simple symbol, that is, letters, digits and the characters ~!@$%^&*_-+=<>.?/, not starting with a digit and not a reserved word.
isOKString(String) - Method in class org.smtlib.SMT.Configuration: True if the string, as the (unescaped) value of a string literal, is legal in the configured SMT-LIB version: printable and white-space characters only, those beyond ASCII only from V2.5 on
isOKSymbol(String) - Method in class org.smtlib.SMT.Configuration: True if the string, as the value of a symbol (without enclosing bars), is a legal symbol in the configured SMT-LIB version: not a reserved word (|let| is the same symbol as let), without | or \, and of printable and white-space characters only, those beyond ASCII only from V2.5 on
ISolver - Interface in org.smtlib: This is the interface to be implemented by any solver adapter; there is a method for each SMT-LIB command.
ISolver.CreationException - Exception Class in org.smtlib: Thrown by SMT.Configuration.createSolver(java.lang.String, java.lang.String) when a solver adapter cannot be resolved, constructed, or fails to launch.
ISort - Interface in org.smtlib: The interface for an SMT-LIB concept of a Sort.
ISort.IAbbreviation - Interface in org.smtlib: This interface represents a new Sort symbol designating an abbreviation for a (possibly parameterized) sort expression.
ISort.IApplication - Interface in org.smtlib: The interface for a Sort expression that consists of either an arity 0 sort symbol or a positive-arity symbol with the appropriate number of arguments.
ISort.IDatatype - Interface in org.smtlib: The interface for a datatype declaration (used in declare-datatype and declare-datatypes).
ISort.IDefinition - Interface in org.smtlib: A super-interface for definitions of new sort ids.
ISort.IErrorDefinition - Interface in org.smtlib: Represents an erroneous sort definition; by having an actual IDefinition, redundant cascading errors are suppressed.
ISort.IFactory - Interface in org.smtlib: The interface for a Sort-creating factory.
ISort.IFamily - Interface in org.smtlib: This interface represents a new Sort symbol designating either a new Sort (if the arity is 0) or a new parameterized Sort family (if the arity is greater than 0); each new symbol has a (new) name and a non-negative arity.
ISort.IFcnSort - Interface in org.smtlib: An interface to represent the Sort of a function; this is not something that can be written as a sort expression in SMT-LIB, but it is convenient to be able to represent the sorts of function ids uniformly with the sorts of other ids.
ISort.IParameter - Interface in org.smtlib: The interface for a sort parameter, as used in sort abbreviations (including in the defining expression).
ISource - Interface in org.smtlib: This interface represents sources of characters.
isReady() - Method in class org.smtlib.AbstractSolver.Pending
isReady() - Method in interface org.smtlib.Log.IPendingOutput: Whether the content is known, so that Log.IPendingOutput.print() may be called
isRealConst(IExpr) - Method in class org.smtlib.logic.Logic
isReservedWord(String) - Method in class org.smtlib.SMT.Configuration: True if the word is reserved in the configured SMT-LIB version; with --relax, command names are not
isRP() - Method in interface org.smtlib.sexpr.ILexToken: Returns true if this token is a right parenthesis.
isRP() - Method in class org.smtlib.sexpr.Lexer: Returns true if the next token is a right parenthesis (without consuming it)
isRP() - Method in class org.smtlib.sexpr.Lexer.LexToken
isRunning(boolean) - Method in class org.smtlib.SolverProcess: Returns true if the process is still running; this relies on exceptions for control flow and may be a bit expensive.
isTimeLimitResponse(String) - Method in class org.smtlib.AbstractSolver: Whether the raw response text is this solver's report that its whole-run time limit (smtConfig.timeoutTotal) ended it; consulted only when that limit is set.
isTimeLimitResponse(String) - Method in class org.smtlib.solvers.Solver_bitwuzla: When its whole-run limit (--time-limit) ends it, Bitwuzla writes unknown -- as the answer to a running check-sat, or unprompted while idle -- and exits with code 0 (checked with 0.9.1).
isTimeLimitResponse(String) - Method in class org.smtlib.solvers.Solver_cvc5: cvc5 reports 'cvc5 interrupted by timeout.' on stderr, with no answer, when its whole-run limit, --tlimit, ends it, and then aborts (checked with cvc5 1.3.2)
isTimeLimitResponse(String) - Method in class org.smtlib.solvers.Solver_z3_4_3: z3 answers 'timeout' (instead of a result) when its whole-run limit, -T, ends it, and then exits
isTimeLimitResponse(String) - Method in class org.smtlib.solvers.Solver_z3_recent: z3 answers 'timeout' (instead of a result) when its whole-run limit, -T:, ends it, and then exits (checked with z3 4.16.0 and 5.1.0)
isVersion(SMT.Configuration.SMTLIB) - Method in class org.smtlib.SMT.Configuration: Returns true if the configured version equals the given version.
isWindows - Static variable in class org.smtlib.AbstractSolver
ITE - Static variable in class org.smtlib.Utils
iterator() - Method in class org.smtlib.SymbolTable: Returns a fresh iterator over the symbol table's contents
Iterator(SymbolTable) - Constructor for class org.smtlib.SymbolTable.Iterator: Constructs a new iterator, initialized at the beginning
ITheory - Interface in org.smtlib: This interface represents a definition of an SMT-LIB theory
IVisitor<T> - Interface in org.smtlib: This is a visitor interface for visitors over IExpr ASTs.
IVisitor.TreeVisitor<T> - Class in org.smtlib: This class is an implementation of IVisitor meant for further derivation: each visitor is implemented to visit its children without doing anything else; the default return value is null.
IVisitor.VisitorException - Exception Class in org.smtlib: An Exception class to use if there is a problem during execution of an IVisitor (e.g.
Iwhat - Interface in org.smtlib.ext: Interface for the SMT-LIB what command (non-standard extension).

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form