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

P

pair(T1, T2) - Method in class org.smtlib.impl.Response.Factory
pair(T1, T2) - Method in interface org.smtlib.IResponse.IFactory
Pair(T1, T2) - Constructor for class org.smtlib.impl.Response.Pair
PAR - Static variable in class org.smtlib.sexpr.Utils
PAR - Static variable in class org.smtlib.Utils: The String for the par reserved word
param(int) - Method in class org.smtlib.impl.Sort.Application
param(int) - Method in interface org.smtlib.ISort.IApplication: Returns the ith parameter
PARAM - Static variable in class org.smtlib.sexpr.Utils: Concrete syntax for the token that starts a parameterized identifier
parameter - Variable in class org.smtlib.impl.SMTExpr.Binding
parameter - Variable in class org.smtlib.impl.SMTExpr.Declaration
parameter() - Method in interface org.smtlib.IExpr.IBinding
parameter() - Method in interface org.smtlib.IExpr.IDeclaration
parameter() - Method in class org.smtlib.impl.SMTExpr.Binding
parameter() - Method in class org.smtlib.impl.SMTExpr.Declaration
Parameter(IExpr.ISymbol) - Constructor for class org.smtlib.impl.Sort.Parameter: Creates a sort parameter for the given symbol name.
ParameterizedIdentifier(IExpr.ISymbol, List<IExpr.IIndex>) - Constructor for class org.smtlib.impl.SMTExpr.ParameterizedIdentifier: Creates a parameterized identifier from the given head symbol and index list.
parameters - Variable in class org.smtlib.command.C_declare_fun: The par-polymorphic parameters (see parameters()).
parameters - Variable in class org.smtlib.impl.SMTExpr.Exists
parameters - Variable in class org.smtlib.impl.SMTExpr.Forall
parameters - Variable in class org.smtlib.impl.SMTExpr.FunctionDeclaration
parameters - Variable in class org.smtlib.impl.SMTExpr.Lambda
parameters - Variable in class org.smtlib.impl.Sort.Abbreviation
parameters - Variable in class org.smtlib.SymbolTable.Entry: The par-polymorphic parameters declared for this entry (null if this is a plain, monomorphic fun_symbol_decl rather than a par_fun_symbol_decl); sort's argSorts/ resultSort may reference these as ISort.IParameter placeholders, to be bound against actual argument sorts by a caller that wants to use this entry.
parameters - Variable in class org.smtlib.TypeChecker
parameters() - Method in class org.smtlib.command.C_declare_fun
parameters() - Method in class org.smtlib.command.C_define_fun: The sorts of the arguments of the function being defined
parameters() - Method in class org.smtlib.command.C_define_sort: Returns the sort parameters of the sort being defined.
parameters() - Method in interface org.smtlib.ICommand.Ideclare_fun: Returns the par-polymorphic type parameters, for the experimental, non-standard "(declare-fun par (param+) (name sort+ attribute*))" form -- mirrors exactly the par_fun_symbol_decl shape a theory's own :funs entry uses.
parameters() - Method in interface org.smtlib.ICommand.Idefine_fun_rec: Returns the list of formal parameters.
parameters() - Method in interface org.smtlib.ICommand.Idefine_fun: Returns the list of formal parameters.
parameters() - Method in interface org.smtlib.ICommand.Idefine_sort: Returns the list of sort parameters.
parameters() - Method in interface org.smtlib.IExpr.IExists
parameters() - Method in interface org.smtlib.IExpr.IForall
parameters() - Method in interface org.smtlib.IExpr.IFunctionDeclaration
parameters() - Method in interface org.smtlib.IExpr.ILambda
parameters() - Method in class org.smtlib.impl.SMTExpr.Exists
parameters() - Method in class org.smtlib.impl.SMTExpr.Forall
parameters() - Method in class org.smtlib.impl.SMTExpr.FunctionDeclaration
parameters() - Method in class org.smtlib.impl.SMTExpr.Lambda
parameters() - Method in class org.smtlib.impl.Sort.Abbreviation
parameters() - Method in class org.smtlib.impl.Sort.Application
parameters() - Method in interface org.smtlib.ISort.IAbbreviation: The list of parameters of the abbreviation (possibly empty, but not null)
parameters() - Method in interface org.smtlib.ISort.IApplication: Returns the list of parameters
params - Variable in class org.smtlib.impl.SMTExpr.Pattern
params() - Method in interface org.smtlib.IExpr.IPattern
params() - Method in class org.smtlib.impl.SMTExpr.Pattern
parenthesized() - Method in interface org.smtlib.IExpr.IPattern: True if written in parentheses; (c), with no variables, is not SMT-LIB but is parsed (with an error) so that type checking reports it as well
parenthesized() - Method in class org.smtlib.impl.SMTExpr.Pattern
parenthesized() - Method in class org.smtlib.impl.Sort.Application
parenthesized() - Method in interface org.smtlib.ISort.IApplication: True if written in parentheses; (S), with no parameters, is not SMT-LIB but is parsed (with an error) so that type checking reports it as well
parse() - Method in interface org.smtlib.IParser.ElementParser
parse(Parser) - Static method in class org.smtlib.command.C_assert: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_check_sat_assuming: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_check_sat: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_declare_const: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_declare_datatype: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_declare_datatypes: Parses the arguments: ( (symbol numeral)+ ) ( datatype_dec+ )
parse(Parser) - Static method in class org.smtlib.command.C_declare_fun: Parses the arguments of the command, producing a new command instance.
parse(Parser) - Static method in class org.smtlib.command.C_declare_sort_parameter: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_declare_sort: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_define_const: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_define_fun_rec: Parses the command arguments and creates a command instance
parse(Parser) - Static method in class org.smtlib.command.C_define_fun: Parses the command arguments and creates a command instance
parse(Parser) - Static method in class org.smtlib.command.C_define_funs_rec: Parses the command arguments and creates a command instance
parse(Parser) - Static method in class org.smtlib.command.C_define_sort: Parses the command arguments and creates a command instance
parse(Parser) - Static method in class org.smtlib.command.C_echo: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_exit: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_get_assertions: Parses the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_get_assignment: Parses the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_get_info: Creates a command instance by parsing the concrete S-expression syntax
parse(Parser) - Static method in class org.smtlib.command.C_get_model: Parses the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_get_option: Creates a command instance by parsing the concrete S-expression syntax
parse(Parser) - Static method in class org.smtlib.command.C_get_proof: Parses the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_get_unsat_assumptions: Parses the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_get_unsat_core: Parses the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_get_value: Parses the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_pop: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_push: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_reset_assertions: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_reset: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.command.C_set_info: Creates a command instance by parsing the concrete S-expression syntax
parse(Parser) - Static method in class org.smtlib.command.C_set_logic: Creates a command instance by parsing the S-expression concrete syntax
parse(Parser) - Static method in class org.smtlib.command.C_set_option: Creates a command instance by parsing the concrete S-expression syntax
parse(Parser) - Static method in class org.smtlib.ext.C_exec: Parses the arguments of the command, producing a new command instance
parse(Parser) - Static method in class org.smtlib.ext.C_what: Parses the input concrete S-expression syntax to produce a command instance
parseAssertionList() - Method in class org.smtlib.sexpr.Parser: Parses a parenthesized list of terms, as returned by a get-assertions response.
parseAssignmentList() - Method in class org.smtlib.sexpr.Parser: Parses a parenthesized list of (symbol bool) pairs, as returned by a get-assignment response.
parseAssignmentPair() - Method in class org.smtlib.sexpr.Parser: Parses one (symbol bool) pair, as found in a get-assignment response.
parseAttribute() - Method in interface org.smtlib.IParser: Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.
parseAttribute() - Method in class org.smtlib.sexpr.Parser: Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.
parseAttributeRest(IExpr.IKeyword) - Method in class org.smtlib.sexpr.Parser: Parses the (optional) value of an attribute whose keyword has already been parsed.
parseAttributeSequence() - Method in class org.smtlib.sexpr.Parser: Parse a sequence of attributes (keyword with optional value) terminated by a right parenthesis, returning null with error messages if an error occurs.
parseAttributeValue() - Method in interface org.smtlib.IParser: Parses a value for an attribute, returning null with error messages if an error occurs
parseAttributeValue() - Method in class org.smtlib.sexpr.Parser: Parse an attribute (keyword with optional value), returning null with error messages if an error occurs.
parseBinary() - Method in interface org.smtlib.IParser: Parse an SMT-LIB binary literal; return null and log an error response if there is no numeral
parseBinary() - Method in class org.smtlib.sexpr.Parser: Parses a binary literal, returning null with the given message if an error occurs; if the next token is not a binary literal, the token is not consumed,
parseBinding() - Method in interface org.smtlib.IParser: Parses a binding "(id expression)", returning null with error messages if an error occurs
parseBinding() - Method in class org.smtlib.sexpr.Parser: Parses a binding "(id expression)", returning null with error messages if an error occurs
parseBindings() - Method in interface org.smtlib.IParser: Parses a parenthesized sequence of let-bindings, returning null with error messages if an error occurs
parseBindings() - Method in class org.smtlib.sexpr.Parser: Parses a parenthesized sequence of let-bindings
parseCommand() - Method in interface org.smtlib.IParser: Parses an SMT-LIB command, if the parser is looking at text representing a valid SMT-LIB command; returns null and logs errors if the text is not a valid command.
parseCommand() - Method in class org.smtlib.sexpr.Parser: Parses the next text in the source as a SMT-LIB command; if an error occurs, the error is logged and the method skips through a matching number of right parentheses
parseConstructor() - Method in interface org.smtlib.IParser: Parses a constructor declaration "(symbol selector*)"
parseConstructor() - Method in class org.smtlib.sexpr.Parser: Parses a constructor declaration "(symbol selector*)"
parseDatatype() - Method in interface org.smtlib.IParser: Parses a datatype declaration
parseDatatype() - Method in class org.smtlib.sexpr.Parser: Parses a datatype declaration: "( constructor+ )" or "( par ( symbol+ ) ( constructor+ ) )"
parseDecimal() - Method in interface org.smtlib.IParser: Parse an SMT-LIB decimal literal; return null and log an error response if there is no numeral
parseDecimal() - Method in class org.smtlib.sexpr.Parser: Parses a decimal, returning null with the given message if an error occurs; if the next token is not a decimal, the token is not consumed,
parseDeclaration() - Method in interface org.smtlib.IParser: Parses a declaration "(id sort)", returning null with error messages if an error occurs
parseDeclaration() - Method in class org.smtlib.sexpr.Parser: Parses a declaration "(id sort)", returning null with error messages if an error occurs
parseDeclarations() - Method in interface org.smtlib.IParser: Parses a parenthesized sequence of IDeclaration items, returning null with error messages if an error occurs
parseDeclarations() - Method in class org.smtlib.sexpr.Parser: Parses a parenthesized sequence of IDeclaration items
parseExpr() - Method in interface org.smtlib.IParser: Parses a term or formula; return null and log an error response if there is no term or formula
parseExpr() - Method in class org.smtlib.sexpr.Parser: Parses an expression, returning null with error messages if there is not a valid expression in the token stream.
parseFunctionDeclaration() - Method in interface org.smtlib.IParser: Parses a function declaration "(symbol (sorted_var*) sort)" used in define-funs-rec
parseFunctionDeclaration() - Method in class org.smtlib.sexpr.Parser: Parses a function declaration "( symbol ( sorted_var* ) sort )" used in define-funs-rec
parseHex() - Method in interface org.smtlib.IParser: Parse an SMT-LIB hex literal; return null and log an error response if there is no numeral
parseHex() - Method in class org.smtlib.sexpr.Parser: Parses a hex literal, returning null with the given message if an error occurs; if the next token is not a hex literal, the token is not consumed,
parseIdentifier() - Method in interface org.smtlib.IParser: Parses an identifier (either a symbol or a parameterized identifier) from the token stream, returning null (with logged error messages) if there is not one.
parseIdentifier() - Method in class org.smtlib.sexpr.Parser: Parses an identifier (either symbol or parameterized identifier) from the token stream, returning null with logged error messages if there is not one.
parseKeyword() - Method in interface org.smtlib.IParser: Parse an SMT-LIB keyword; return null and log an error response if there is no valid keyword
parseKeyword() - Method in class org.smtlib.sexpr.Parser: Parses a keyword, returning null with an error message if an error occurs; if the next token is not a keyword, the token is not consumed.
parseList(IParser.ElementParser<T>, String, boolean) - Method in class org.smtlib.sexpr.Parser: Parses a parenthesized list of elements using the given element parser.
parseListDatatypes(Parser) - Method in interface org.smtlib.IParser: Parses a parenthesized list of datatype declarations from the given parser.
parseListTerms(Parser) - Method in interface org.smtlib.IParser: Parses a parenthesized list of terms from the given parser.
parseLiteral() - Method in interface org.smtlib.IParser: Parse an SMT-LIB literal of any kind; return null and log an error response if there is no literal
parseLiteral() - Method in class org.smtlib.sexpr.Parser: Parses a literal, returning null with error messages if an error occurs.
parseLogic() - Method in interface org.smtlib.IParser: Parse an SMT-LIB logic; return null and log an error response if there is no valid logic definition
parseLogic() - Method in class org.smtlib.sexpr.Parser: Parses a logic definition (including beginning and ending parentheses, returning null with error messages if it fails; only part of the checking of the contents is performed in this call (the rest is done in loadLogic).
parseLP() - Method in class org.smtlib.sexpr.Parser: Parses a left parenthesis, returning null and emitting an error message if there isn't one (and the next token is not consumed)
parseMatchCase() - Method in class org.smtlib.sexpr.Parser: Parses a single match case: "(pattern term)"
parseNumeral() - Method in interface org.smtlib.IParser: Parse an SMT-LIB numeral; return null and log an error response if there is no numeral
parseNumeral() - Method in class org.smtlib.sexpr.Parser: Parses a numeral, returning null with error messages if an error occurs; if the next token is not a numeral, the token is not consumed,
parsePattern() - Method in class org.smtlib.sexpr.Parser: Parses a match pattern: either a bare symbol (or wildcard _) or "(symbol symbol*)" where params may include _
parseQualifiedIdentifier() - Method in interface org.smtlib.IParser: Parses a qualified identifier (either a symbol, a parameterized identifier, or an as identifier) from the token stream, returning null (with logged error messages) if there is not one.
parseQualifiedIdentifier() - Method in class org.smtlib.sexpr.Parser: Parses a qualified identifier (either a symbol, a parameterized identifier, or an as identifier) from the token stream, returning null (with logged error messages) if there is not one.
Parser - Class in org.smtlib.sexpr: Parses the standard SMT-LIB concrete syntax to produce ASTs of objects that are instances of the org.smtlib.* interfaces.
Parser(SMT.Configuration, ISource) - Constructor for class org.smtlib.sexpr.Parser: Creates a Parser using an SMT configuration object and a source for characters; ordinarily use a factory to obtain a parser.
parseResponse(String) - Method in class org.smtlib.AbstractSolver: Parses the solver's raw response text.
parseResponse(String) - Method in class org.smtlib.sexpr.Parser
parseResponse(String) - Method in class org.smtlib.solvers.Solver_bitwuzla
parseResponse(String) - Method in class org.smtlib.solvers.Solver_z3_4_3: Every command this adapter sends directly to the process ends here, so the solver's report that its whole-run limit ended it is recognized for all of them (see AbstractSolver#timeLimitResponse).
ParserException(String, IPos) - Constructor for exception class org.smtlib.IParser.ParserException: Creates a parse exception from the given error message and problem location
parseRP() - Method in class org.smtlib.sexpr.Parser: Parses a right parenthesis, returning null and emitting an error message if there isn't one (and the next token is not consumed)
parseScript() - Method in interface org.smtlib.IParser: Parses an SMT-LIB command script.
parseScript() - Method in class org.smtlib.sexpr.Parser
parseSelector() - Method in interface org.smtlib.IParser: Parses a selector declaration "(symbol sort)"
parseSelector() - Method in class org.smtlib.sexpr.Parser: Parses a selector declaration "(symbol sort)"
parseSeq(ILexToken) - Method in class org.smtlib.sexpr.Parser: Parses and adds Sexpr to a list until parseSexpr returns null (indicating a RightParen has been seen or end of input or an error)
parseSexpr() - Method in class org.smtlib.sexpr.Parser: Parses an Sexpr
parseSort(List<ISort.IParameter>) - Method in interface org.smtlib.IParser: Parses a sort, returning null with error messages if a valid sort is not in the next parser tokens.
parseSort(List<ISort.IParameter>) - Method in class org.smtlib.sexpr.Parser: Parses a sort, returning null with error messages if a valid sort is not in the next parser tokens.
parseSortList(List<ISort.IParameter>) - Method in class org.smtlib.sexpr.Parser: Parses sequence of sorts up to a right-parenthesis, returning null with error messages if an error occurs.
parseStringLiteral() - Method in interface org.smtlib.IParser: Parse an SMT-LIB string literal; return null and log an error response if there is no valid string literal
parseStringLiteral() - Method in class org.smtlib.sexpr.Parser: Parses a string literal, returning null with an error message if an error occurs; if the next token is not a string literal, the token is not consumed,
parseSymbol() - Method in interface org.smtlib.IParser: Parse an SMT-LIB symbol; return null and log an error response if there is no symbol
parseSymbol() - Method in class org.smtlib.sexpr.Parser: Parses a symbol, returning null with messages and not advancing the parser if an error occurs
parseSymbol(String) - Method in class org.smtlib.sexpr.Parser: Parses a symbol (but not a reserved word unless the configuration field 'relax' is true), returning null with messages if an error occurs; the parser is advanced only if an actual symbol is parsed.
parseSymbolList() - Method in class org.smtlib.sexpr.Parser: Parses a parenthesized list of names, as returned by a get-unsat-core response.
parseSymbolOrReservedWord(String) - Method in class org.smtlib.sexpr.Parser: Parses a symbol or a reserved word, returning null with messages if an error occurs.
parseTermAttributeSequence() - Method in class org.smtlib.sexpr.Parser: Parses the attributes of an annotated term (! t attr+) up to the right parenthesis.
parseTermList() - Method in class org.smtlib.sexpr.Parser: Parses a parenthesized list of terms, as returned by a get-unsat-assumptions response.
parseTheory() - Method in interface org.smtlib.IParser: Parse an SMT-LIB theory; return null and log an error response if there is no valid theory definition
parseTheory() - Method in class org.smtlib.sexpr.Parser: Parses a theory definition (including beginning and ending parentheses, returning null with error messages if it fails; only part of the checking of the contents is performed in this call (the rest is done in loadTheory).
parseValueList() - Method in class org.smtlib.sexpr.Parser: Parses a parenthesized list of (term value) pairs, as returned by a get-value response.
parseValuePair() - Method in class org.smtlib.sexpr.Parser: Parses one (term value) pair, as found in a get-value response.
pattern - Variable in class org.smtlib.impl.SMTExpr.MatchCase
pattern() - Method in interface org.smtlib.IExpr.IMatchCase
pattern() - Method in class org.smtlib.impl.SMTExpr.MatchCase
pattern(IExpr.ISymbol, List<IExpr.ISymbol>) - Method in interface org.smtlib.IExpr.IFactory: Creates a match pattern.
pattern(IExpr.ISymbol, List<IExpr.ISymbol>) - Method in class org.smtlib.impl.Factory
Pattern(IExpr.ISymbol, List<IExpr.ISymbol>) - Constructor for class org.smtlib.impl.SMTExpr.Pattern: Creates a pattern from the given constructor symbol and variable list.
Pattern(IExpr.ISymbol, List<IExpr.ISymbol>, boolean) - Constructor for class org.smtlib.impl.SMTExpr.Pattern: Creates a pattern that is written in parentheses even if it has no variables, as (c)
PATTERN - Static variable in class org.smtlib.sexpr.Utils: The keyword for a quantifier trigger pattern attribute
patternTerms(List<IExpr>) - Method in interface org.smtlib.IExpr.IFactory: Creates the value of a :pattern attribute: the given terms as one (multi-)pattern.
patternTerms(List<IExpr>) - Method in class org.smtlib.impl.Factory
PatternTerms(List<IExpr>) - Constructor for class org.smtlib.impl.SMTExpr.PatternTerms: Creates a pattern from the given (possibly empty) list of terms.
peekToken() - Method in class org.smtlib.sexpr.Lexer: Returns the next lexical token without consuming it; a subsequent call to getToken will return the same token.
pipeline - Variable in class org.smtlib.SMT.Configuration: If true, commands are sent to the solver without waiting for each response where that is possible (AbstractSolver.sendPipelined), and the responses are read as they arrive: by the command-line tool for file or --text input (--pipeline), and by IScript.execute (AbstractSolver.executePipelined)
pipelineInput - Variable in class org.smtlib.SMT: Whether the input being processed may be pipelined (with --pipeline): file and --text input, not the socket or standard input, whose client needs each command's response at once
pipelines(ICommand) - Method in class org.smtlib.AbstractSolver: Whether AbstractSolver.sendPipelined(ICommand) may send the command without waiting for its response.
pipelines(ICommand) - Method in class org.smtlib.solvers.Solver_simplify: Never pipelined: commands are executed here, not sent to a process
pipelines(ICommand) - Method in class org.smtlib.solvers.Solver_z3_4_3: Never pipelined: this adapter sends and corrects commands by its own means
PLUGIN_ID - Static variable in class org.smtlib.Utils: The ID of the core functionality plug-in
PLUS - Static variable in class org.smtlib.Utils
pop() - Method in class org.smtlib.SymbolTable: Removes the top frame from the symbol table stack.
pop(int) - Method in class org.smtlib.AbstractSolver
pop(int) - Method in interface org.smtlib.ISolver: Removes the given number of assertion-stack frames from the solver state.
pop(int) - Method in class org.smtlib.solvers.Solver_bitwuzla
pop(int) - Method in class org.smtlib.solvers.Solver_simplify
pop(int) - Method in class org.smtlib.solvers.Solver_test
pop(int) - Method in class org.smtlib.solvers.Solver_z3_4_3
pop(IExpr.INumeral) - Method in interface org.smtlib.ICommand.IFactory: Creates a pop command object.
pop(IExpr.INumeral) - Method in class org.smtlib.impl.Factory
POP - Enum constant in enum class org.smtlib.AbstractSolver.StackChange
port - Variable in class org.smtlib.Driver: The port to which to send commands (set as a command-line option)
port - Variable in class org.smtlib.SMT.Configuration: The port to use for socket communications; a port > 0 supersedes any file value, but is ignored if the text option is set.
pos - Variable in class org.smtlib.impl.Pos.Posable
pos - Variable in exception class org.smtlib.IParser.ParserException: The location of the parsing problem
pos - Variable in exception class org.smtlib.IVisitor.VisitorException: Position information about the textual location of the error
pos() - Method in class org.smtlib.impl.Pos.Posable
pos() - Method in exception class org.smtlib.IParser.ParserException: Returns the error position
pos() - Method in interface org.smtlib.IPos.IPosable: Textual position of this object
pos() - Method in interface org.smtlib.IResponse.IError: Returns the textual location for the response, if available and applicable, otherwise null.
pos() - Method in exception class org.smtlib.IVisitor.VisitorException
pos() - Method in interface org.smtlib.sexpr.ILexToken: The lexical position of the token
pos() - Method in interface org.smtlib.sexpr.Lexer.IPLexToken
pos() - Method in class org.smtlib.sexpr.Lexer.LexToken
pos(int, int) - Method in class org.smtlib.sexpr.Lexer: Creates an IPos object with the given start and end and the source for this Lexer
pos(int, int) - Method in class org.smtlib.sexpr.Parser: Returns an IPos object for the given character start and end positions and including a reference to the parser's source object.
pos(IPos, IPos) - Method in class org.smtlib.sexpr.Parser: Returns an IPos object for the given character start and end positions and including a reference to the parser's source object.
Pos - Class in org.smtlib.impl: Represents a range of characters in a source - used to indicate the location of errors
Pos(int, int, ISource) - Constructor for class org.smtlib.impl.Pos: Constructor for a Pos object
Pos.AbstractExpr - Class in org.smtlib.impl: 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).
Pos.Posable - Class in org.smtlib.impl: An implementation of IPosable, holding an instance of Pos, that can be used as a base class if necessary
Pos.Printable - Class in org.smtlib.impl: A Posable that also implements INode, with toString() delegating to Printer.
Pos.Source - Class in org.smtlib.impl: An implementation of the ISource interface
Posable() - Constructor for class org.smtlib.impl.Pos.Posable
pr(IExpr) - Method in class org.smtlib.TypeChecker: Utility method for printing an expression, using the default printer
pr(ISort) - Method in class org.smtlib.TypeChecker: Utility method for printing a sort, using the default printer
prefixCommentEnd - Variable in class org.smtlib.sexpr.Lexer: The character range prefixCommentText was captured from (before the one leading newline stripping below, if any, is applied to prefixCommentText itself) -- lets a caller that turns a comment into its own node (see command/C_comment.java) give that node an accurate pos().
prefixCommentStart - Variable in class org.smtlib.sexpr.Lexer: The character range prefixCommentText was captured from (before the one leading newline stripping below, if any, is applied to prefixCommentText itself) -- lets a caller that turns a comment into its own node (see command/C_comment.java) give that node an accurate pos().
prefixCommentText - Variable in class org.smtlib.sexpr.Lexer: Any comment text found before the current token, starting from the first line terminator onward -- i.e.
print() - Method in interface org.smtlib.Log.IPendingOutput: Logs the content, through this Log as usual
print(T) - Method in interface org.smtlib.IPrinter: Prints the argument to the receiver
print(T) - Method in class org.smtlib.sexpr.Printer: Prints the argument to the receiver
PRINT_SUCCESS - Static variable in class org.smtlib.Utils: The string designating an option item
Printable() - Constructor for class org.smtlib.impl.Pos.Printable
printCommand(ICommand) - Method in class org.smtlib.sexpr.Printer: Prints a no-argument command: (commandName()).
printCommand(ICommand, Printer.PrintArgs) - Method in class org.smtlib.sexpr.Printer: Prints (commandName() args) — the space between name and args is emitted here, so the args lambda should not prepend one.
Printer - Class in org.smtlib.sexpr: This class writes out SMT-LIB ASTs as concrete S-expression syntax; aside from white space between tokens it should simply reverse what the Parser class does.
Printer - Class in org.smtlib.solvers
Printer(SMT.Configuration, Writer) - Constructor for class org.smtlib.sexpr.Printer: Creates a printer object that follows the given Configuration's rules.
Printer(SMT.Configuration, Writer) - Constructor for class org.smtlib.solvers.Printer: Creates a printer object that follows the given Configuration's rules.
Printer.PrintArgs - Interface in org.smtlib.sexpr: Functional interface for the argument-printing lambda passed to Printer.printCommand(org.smtlib.ICommand, org.smtlib.sexpr.Printer.PrintArgs).
Printer.WithLines - Class in org.smtlib.sexpr
printSuccess - Variable in class org.smtlib.AbstractSolver
printSuccess - Variable in class org.smtlib.impl.Response.Factory
printSuccessResponse - Variable in class org.smtlib.AbstractSolver
process - Variable in class org.smtlib.SolverProcess: The Java process object (initialized by start() )
processCommandLine(String[], SMT.Configuration) - Method in class org.smtlib.SMT: Parses the command-line, setting any option in the given configuration argument.
processOptions(String[]) - Method in class org.smtlib.Driver: Sets the fields of the class according to the command-line
PRODUCE_ASSERTIONS - Static variable in class org.smtlib.Utils: The string designating an option item
PRODUCE_ASSIGNMENTS - Static variable in class org.smtlib.Utils: The string designating an option item
PRODUCE_MODELS - Static variable in class org.smtlib.Utils: The string designating an option item
PRODUCE_PROOFS - Static variable in class org.smtlib.Utils: The string designating an option item
PRODUCE_UNSAT_ASSUMPTIONS - Static variable in class org.smtlib.Utils: The string designating an option item
PRODUCE_UNSAT_CORES - Static variable in class org.smtlib.Utils: The string designating an option item
produceAssertionsKey(SMT.Configuration) - Static method in class org.smtlib.Utils: Returns the name of the option that gates get-assertions -- renamed from :interactive-mode to :produce-assertions in SMT-LIB 2.5.
prompt - Variable in class org.smtlib.Log.StandardListener: The current indent prefix (see Log.IListener.indent(java.lang.String)), used by Log.StandardListener.logError(IResponse.IError) below to align an error-location caret diagram with the prompt the user actually saw it after.
prompt - Variable in class org.smtlib.SMT.Configuration: The prompt to use when needing new input from the user in an interactive mode.
prompt() - Method in interface org.smtlib.CharSequenceInfinite.IPrompter: Implement this call-back to do whatever user actions are needed to cause more input to be available.
prompt() - Method in class org.smtlib.SMT.Prompter: Prints out the prompt (with no new-line), if a prompt is wanted
prompt() - Method in class org.smtlib.solvers.Solver_smt
prompt2 - Variable in class org.smtlib.SMT.Configuration: The prompt to use when in the middle of a command
prompter - Variable in class org.smtlib.CharSequenceInfinite: The prompter object
Prompter(SMT.Configuration) - Constructor for class org.smtlib.SMT.Prompter: Creates a prompter object - the object knows how to prompt for input based on current settings and state
proof() - Method in class org.smtlib.impl.Response.ProofResponse
proof() - Method in interface org.smtlib.IResponse.IProofResponse
proofResponse(IResponse) - Method in class org.smtlib.AbstractSolver: Wraps a parsed get-proof answer as an IProofResponse; anything else (an error, unsupported) is returned unchanged.
ProofResponse(ISexpr) - Constructor for class org.smtlib.impl.Response.ProofResponse
PROOFS - Enum constant in enum class org.smtlib.SolverCapabilities.Capability: get-proof returns a parsable s-expression (SMT-LIB fixes no proof format)
props - Variable in class org.smtlib.SMT.Configuration: Properties loaded from the jsmtlib.properties file(s); see SMT.Configuration.readProperties().
PROPS_ADAPTER_SUFFIX - Static variable in class org.smtlib.Utils: The suffix for adapter properties, as in org.smtlib.solver_ZZZ.adapter
PROPS_CAPABILITIES_SUFFIX - Static variable in class org.smtlib.SolverCapabilities: The suffix of the property that lists a solver's capabilities
PROPS_COMMAND_SUFFIX - Static variable in class org.smtlib.Utils: The suffix for command-line properties, as in org.smtlib.solver_ZZZ.command
PROPS_DEFAULT_SOLVER - Static variable in class org.smtlib.Utils: The property name that specifies the default solver
PROPS_EXEC_SUFFIX - Static variable in class org.smtlib.Utils: The suffix for executable properties, as in org.smtlib.solver_ZZZ.exec
PROPS_FILE - Static variable in class org.smtlib.Utils: The name of the properties file read by jSMTLIB
PROPS_LOGIC_PATH - Static variable in class org.smtlib.Utils: The property giving the default logic path
PROPS_SOLVER_PREFIX - Static variable in class org.smtlib.Utils: The default prefix for the property names that identify solver executables, as in org.smtlib.solver_ZZZ
ProverException(String) - Constructor for exception class org.smtlib.SolverProcess.ProverException
push() - Method in class org.smtlib.SymbolTable: Adds a new empty frame on the top of the symbol table stack.
push(int) - Method in class org.smtlib.AbstractSolver
push(int) - Method in interface org.smtlib.ISolver: Adds the given number of empty assertion-stack frames to the solver state.
push(int) - Method in class org.smtlib.solvers.Solver_bitwuzla
push(int) - Method in class org.smtlib.solvers.Solver_simplify
push(int) - Method in class org.smtlib.solvers.Solver_test
push(int) - Method in class org.smtlib.solvers.Solver_z3_4_3
push(IExpr.INumeral) - Method in interface org.smtlib.ICommand.IFactory: Creates a push command object.
push(IExpr.INumeral) - Method in class org.smtlib.impl.Factory
PUSH - Enum constant in enum class org.smtlib.AbstractSolver.StackChange

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