L-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

L

lambda(List<IExpr.IDeclaration>, IExpr) - Method in interface org.smtlib.IExpr.IFactory: Creates a Lambda expression (SMT-LIB 2.7ff, HO-Core theory).
lambda(List<IExpr.IDeclaration>, IExpr) - Method in class org.smtlib.impl.Factory
Lambda(List<IExpr.IDeclaration>, IExpr) - Constructor for class org.smtlib.impl.SMTExpr.Lambda: Creates a lambda expression with the given bound variable declarations and body.
LAMBDA - Static variable in class org.smtlib.sexpr.Utils: Concrete syntax for the lambda token (SMT-LIB 2.7ff, HO-Core theory)
lastError - Variable in class org.smtlib.sexpr.Parser: The most recent error, or null
lastError() - Method in interface org.smtlib.IParser: Returns the most recent error, or null
lastError() - Method in class org.smtlib.sexpr.Parser
lastResponse - Variable in class org.smtlib.SMT: The response from the most recently executed command; used to export results in interactive mode.
LE - Static variable in class org.smtlib.Utils
leftassoc(String, int, Iterator<T>) - Method in class org.smtlib.solvers.Solver_z3_4_3.Translator
length - Variable in class org.smtlib.CharSequenceInfinite: The implicit length of the CharSequence; note that this length may change as characters are read
length - Variable in class org.smtlib.impl.SMTExpr.BinaryLiteral
length - Variable in class org.smtlib.impl.SMTExpr.HexLiteral
length() - Method in class org.smtlib.CharSequenceInfinite: Returns the length of the CharSequence; for this implementation, the return value is at least as great as the unknown length of the CharSequence.
length() - Method in interface org.smtlib.IExpr.IBinaryLiteral: Number of binary bits
length() - Method in interface org.smtlib.IExpr.IHexLiteral: Number of hex digits
length() - Method in class org.smtlib.impl.SMTExpr.BinaryLiteral
length() - Method in class org.smtlib.impl.SMTExpr.HexLiteral
let(List<IExpr.IBinding>, IExpr) - Method in interface org.smtlib.IExpr.IFactory: Creates a Let expression.
let(List<IExpr.IBinding>, IExpr) - Method in class org.smtlib.impl.Factory
Let(List<IExpr.IBinding>, IExpr) - Constructor for class org.smtlib.impl.SMTExpr.Let: Creates a let expression with the given bindings and body.
LET - Static variable in class org.smtlib.sexpr.Utils
LET - Static variable in class org.smtlib.Utils: The String for the let reserved word
Lexer - Class in org.smtlib.sexpr: Converts character sequences (from ISource) into tokens, presuming the standard SMT-LIBv2 concrete syntax.
Lexer(SMT.Configuration, ISource) - Constructor for class org.smtlib.sexpr.Lexer: Creates a Lexer using an SMT configuration object and a source for characters
Lexer.IPLexToken - Interface in org.smtlib.sexpr: An interface used for punctuation tokens that can be retrieved from the parser input.
Lexer.LexToken - Class in org.smtlib.sexpr: A lexical token class for single punctuation characters.
LexToken(String, int) - Constructor for class org.smtlib.sexpr.Lexer.LexToken
LIA - Class in org.smtlib.logic
LIA(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.LIA
lineBeginning(int) - Method in class org.smtlib.impl.Pos.Source
lineBeginning(int) - Method in interface org.smtlib.ISource: Returns the character position of the beginning of the line containing the given position.
lineNumber(int) - Method in class org.smtlib.impl.Pos.Source
lineNumber(int) - Method in interface org.smtlib.ISource: Returns the number (beginning with 1) of the line containing the given character position (which begins at 0).
lineNumberPatterns() - Method in class org.smtlib.AbstractSolver: Patterns matching the line numbers in this solver's messages about the command answered: group 1 is the text before the number, group 2 the number, group 3 the text after it
lineNumberPatterns() - Method in class org.smtlib.solvers.Solver_bitwuzla
lineNumberPatterns() - Method in class org.smtlib.solvers.Solver_cvc5
lineNumberPatterns() - Method in class org.smtlib.solvers.Solver_smtinterpol
lineNumberPatterns() - Method in class org.smtlib.solvers.Solver_yices2
lineNumberPatterns() - Method in class org.smtlib.solvers.Solver_z3_4_3
lineNumberPatterns() - Method in class org.smtlib.solvers.Solver_z3_recent
linesOffset - Variable in class org.smtlib.AbstractSolver: The correction to a line number the solver reports for the command whose response is being read: line N of the solver's input is shown as line N - linesOffset, the line of the user's source on which that command starts.
listen() - Method in class org.smtlib.SolverProcess: Listens to the process's standard output until the designated endMarker is read, combined with whatever error output has arrived.
listeners - Variable in class org.smtlib.Log: The list of listeners to send log messages to
Literal(T) - Constructor for class org.smtlib.impl.SMTExpr.Literal: Creates a literal with the given value.
loadLogic(String, SymbolTable, IPos) - Method in class org.smtlib.Utils: Finds and loads a logic into the given symbol table
loadLogic(ILogic, SymbolTable) - Method in class org.smtlib.Utils
loadTheory(String, SymbolTable) - Method in class org.smtlib.Utils: Loads a theory into the given symbol table.
loadTheory(ITheory, SymbolTable) - Method in class org.smtlib.Utils
location() - Method in class org.smtlib.impl.Pos.Source: The identifier for the location
location() - Method in interface org.smtlib.ISource: User-specified identification of the location of the source; the user is responsible to use the result in the way in which the source object was created.
locationIndication(IPos, String, SMT.Configuration) - Static method in class org.smtlib.Log: Creates a two-line, compiler-style caret diagnostic pointing at the given position; the returned value does not have a final line termination.
log - Variable in class org.smtlib.SMT.Configuration: The log to use for regular, error, and diagnostic output
log - Variable in class org.smtlib.SolverProcess: A place (e.g., log file), if non-null, to write all outbound communications for diagnostic purposes
Log - Class in org.smtlib: This class is used as a collection point for all output.
Log(SMT.Configuration) - Constructor for class org.smtlib.Log: Constructs a Log based on the given configuration, adding a StandardListener
Log.IListener - Interface in org.smtlib: This is an interface to be implemented by any Object that wants to hear log messages; the Object must register itself by calling Log.addListener.
Log.IPendingOutput - Interface in org.smtlib: Output whose content is not yet known, e.g.
Log.StandardListener - Class in org.smtlib: This class logs to the standard PrintStreams out and diag.
logDiag(String) - Method in interface org.smtlib.Log.IListener: Called when a message is sent to the SMT-LIB diagnostic output (it is expected that a line termination will be added)
logDiag(String) - Method in class org.smtlib.Log: Prints the argument to any listeners (adds a line terminator).
logDiag(String) - Method in class org.smtlib.Log.StandardListener: Writes the message to the diag stream
logError(String) - Method in interface org.smtlib.Log.IListener: Called when an error is being recorded on the normal output (it is expected that a line termination will be added)
logError(String) - Method in class org.smtlib.Log: Reports the error to any listeners.
logError(String) - Method in class org.smtlib.Log.StandardListener: Writes the message to the 'out' PrintStream, adding line termination
logError(IResponse.IError) - Method in interface org.smtlib.Log.IListener: Called when an IError is being recorded on the normal output - the listener has the opportunity to record error location information as well
logError(IResponse.IError) - Method in class org.smtlib.Log: Reports the error to any listeners, returning the input.
logError(IResponse.IError) - Method in class org.smtlib.Log.StandardListener: Writes the offending text line, column location in that line, and the error message to the 'out' stream.
logfile - Variable in class org.smtlib.SMT.Configuration: The file to which to write the communication, for debugging or reference; null means default
logic - Variable in class org.smtlib.SMT.Configuration: This field is set from the command-line; if set, then sets the logic used by the solver, as if the first command were the corresponding set-logic command.
logic() - Method in class org.smtlib.command.C_set_logic: The name of the logic to set
logic() - Method in interface org.smtlib.ICommand.Iset_logic: Returns the logic name.
Logic - Class in org.smtlib.logic: Common base for this package's per-logic syntactic-restriction classes (QF_IDL, LRA, QF_UF, etc).
Logic(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.impl.SMTExpr.Logic: Creates a logic
Logic(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.Logic
LOGIC - Static variable in class org.smtlib.sexpr.Utils
LOGIC - Static variable in class org.smtlib.Utils: The String for the logic symbol
logicInUse - Variable in class org.smtlib.SymbolTable: The logic that is being used - this value is used to check that expressions, etc., conform to the language restrictions of the current logic.
logicName - Variable in class org.smtlib.command.C_set_logic: The name of the logic to set
logicName - Variable in class org.smtlib.impl.SMTExpr.Logic: The name of the logic
logicName() - Method in interface org.smtlib.ILogic: The name of the logic
logicName() - Method in class org.smtlib.impl.SMTExpr.Logic: The name of the logic
logicPath - Variable in class org.smtlib.SMT.Configuration: The path on which to find logic and theory definitions
logicSet - Variable in class org.smtlib.solvers.Solver_simplify: Internal state variable - set non-null once the logic is set -- see Solver_test.logicSet.
logicSet - Variable in class org.smtlib.solvers.Solver_test: Internal state variable - set non-null once the logic is set.
logicSet - Variable in class org.smtlib.solvers.Solver_z3_4_3: Set to true once a set-logic command has been executed.
logOut(String) - Method in interface org.smtlib.Log.IListener: Called when messages are logged to the normal output (it is expected that a line termination will be added).
logOut(String) - Method in class org.smtlib.Log: Prints the argument on the regular output stream, with a line termination added, and notifies any listeners.
logOut(String) - Method in class org.smtlib.Log.StandardListener: Writes the message to the 'out' PrintStream, adding line termination
logOut(IResponse) - Method in interface org.smtlib.Log.IListener: Called when a response is logged to the normal output (it is expected that a line termination will be added); the argument is converted to text using the defaultPrinter in the smt configuration.
logOut(IResponse) - Method in class org.smtlib.Log: Prints the argument on the regular output stream and to any listeners
logOut(IResponse) - Method in class org.smtlib.Log.StandardListener: Writes the given response to the out stream, adding line termination
logOutNoln(String) - Method in interface org.smtlib.Log.IListener: Called when a message is sent to the normal output with no line termination (e.g.
logOutNoln(String) - Method in class org.smtlib.Log: Prints the argument on the regular output stream with no newline appended, and notifies any listeners.
logOutNoln(String) - Method in class org.smtlib.Log.StandardListener: Writes the message to the 'out' PrintStream with no line termination
logSolverDiagnostics() - Method in class org.smtlib.AbstractSolver: Logs the standard-error text the solver wrote along with its replies (see SolverProcess.takeDiagnosticOutput), noting a whole-run time-limit report there: the reply stands, but the solver has ended
lookup(int, IExpr.IIdentifier) - Method in class org.smtlib.SymbolTable: Lookup the Symbol with the given identifier and arity, returning its Sort.
lookup(String) - Static method in enum class org.smtlib.SolverCapabilities.Capability: The capability whose token or enum name is the given name, ignoring case; null if none
lookup(IExpr.IIdentifier) - Method in class org.smtlib.SymbolTable: Lookup the Symbol with the given identifier, returning all of its declared entries (of any arity).
lookup(IExpr.IIdentifier, List<ISort>, ISort, StringBuilder) - Method in class org.smtlib.SymbolTable: Lookup a Symbol with the given name and argument Sorts and result Sort.
lookupInstance(int, IExpr.IIdentifier, ISort) - Method in class org.smtlib.SymbolTable: The signature of the arity-n function name, instantiated so that its result sort is resultSort (a par entry's parameters are bound by unification), or null if there is no such function or its result sort cannot be resultSort.
lookupSort(IExpr.IIdentifier) - Method in class org.smtlib.SymbolTable: Looks up the Sort definition with the given name
LP - Static variable in interface org.smtlib.sexpr.Lexer.IPLexToken
LP(int) - Method in class org.smtlib.sexpr.Lexer: Creates a lexical token for a left parenthesis at the given position
LRA - Class in org.smtlib.logic: This logic does not allow uninterpreted functions or nonlinear arithmetic terms
LRA(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.LRA
LT - Static variable in class org.smtlib.Utils

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