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

E

earlierSourceLine(int) - Method in class org.smtlib.AbstractSolver: The source line for line n of the solver's input, which may be that of an earlier command
echo - Variable in class org.smtlib.SMT.Configuration: True if the application is to echo commands as it executes them; only applies in interactiveMode mode
echo(IExpr.IStringLiteral) - Method in class org.smtlib.AbstractSolver
echo(IExpr.IStringLiteral) - Method in interface org.smtlib.ICommand.IFactory: Creates an echo command object.
echo(IExpr.IStringLiteral) - Method in class org.smtlib.impl.Factory
echo(IExpr.IStringLiteral) - Method in interface org.smtlib.ISolver: Echoes the argument string back to the output channel.
echo(IExpr.IStringLiteral) - Method in class org.smtlib.solvers.Solver_simplify
echo(IExpr.IStringLiteral) - Method in class org.smtlib.solvers.Solver_test
echo(IExpr.IStringLiteral) - Method in class org.smtlib.solvers.Solver_yices2: yices2 writes echo's text unquoted, so where it ends cannot be found (#136); the response to echo is its argument
echo(IExpr.IStringLiteral) - Method in class org.smtlib.solvers.Solver_z3_4_3: z3 4.3 writes echo's text unquoted, so where it ends cannot be found (#136); the response to echo is its argument
echo(IExpr.IStringLiteral) - Method in class org.smtlib.solvers.Solver_z3_4_5
empty() - Method in class org.smtlib.impl.Response.Factory
empty() - Method in interface org.smtlib.IResponse.IFactory
EMPTY - Static variable in class org.smtlib.impl.Response
EMPTY - Static variable in interface org.smtlib.sexpr.Lexer.IPLexToken
emptyParentheses - Variable in class org.smtlib.impl.SMTExpr.Pattern: Whether the pattern was written as (c), in parentheses with no variables
emptyParentheses - Variable in class org.smtlib.impl.Sort.Application: Whether the sort was written as (S), in parentheses with no parameters
encode(IExpr.IIdentifier) - Method in class org.smtlib.solvers.Solver_simplify: See Solver_test.encode(org.smtlib.IExpr.IIdentifier).
encode(IExpr.IIdentifier) - Method in class org.smtlib.solvers.Solver_test
END_WAIT_MILLIS - Static variable in class org.smtlib.AbstractSolver: How long (ms) to wait for the solver process to end, once a send has found it gone or ending
endChar - Static variable in class org.smtlib.CharSequenceInfinite: The character to use to mark the end of input
endDrainMillis - Variable in class org.smtlib.SolverProcess: Once the solver's standard output has ended, how long (ms) to wait at most for its standard error to end too, so that what it wrote there just before exiting (typically an error) is read in full rather than lost to the stderr reader not having caught up
endedAfter(double, long) - Method in class org.smtlib.SolverProcess: Whether the process has ended on its own (not stopped or interrupted here), waiting at most waitMillis for that, after running at least the given number of seconds
endedByTimeLimit - Variable in class org.smtlib.AbstractSolver: True once the solver's whole-run time limit (smtConfig.timeoutTotal) has ended it; every later command then gets responseFactory.timeout() (exit tolerates it), rather than an error about the process having exited.
endMarker - Variable in class org.smtlib.SolverProcess: The text that marks the end of the text returned from the process
Entry(IExpr.IIdentifier, ISort.IFcnSort, List<IExpr.IAttribute<?>>, List<ISort.IParameter>) - Constructor for class org.smtlib.SymbolTable.Entry: Constructs a symbol table entry
EOD(int) - Method in class org.smtlib.sexpr.Lexer: Creates a lexical token for a end-of-data at the given position
eol - Static variable in class org.smtlib.sexpr.Printer: The system-dependent line termination
eol - Static variable in class org.smtlib.SolverProcess
EQ - Static variable in class org.smtlib.Utils
equals(Object) - Method in interface org.smtlib.IExpr.IKeyword
equals(Object) - Method in class org.smtlib.impl.Pos.Posable
equals(Object) - Method in class org.smtlib.impl.SMTExpr.AsIdentifier
equals(Object) - Method in class org.smtlib.impl.SMTExpr.BinaryLiteral
equals(Object) - Method in class org.smtlib.impl.SMTExpr.Decimal: Equal to any IDecimal with the same BigDecimal value
equals(Object) - Method in class org.smtlib.impl.SMTExpr.HexLiteral
equals(Object) - Method in class org.smtlib.impl.SMTExpr.Keyword: Equal to any IKeyword designating the same abstract keyword.
equals(Object) - Method in class org.smtlib.impl.SMTExpr.Numeral: Equal to any INumeral with the same numeric value
equals(Object) - Method in class org.smtlib.impl.SMTExpr.ParameterizedIdentifier
equals(Object) - Method in class org.smtlib.impl.SMTExpr.StringLiteral: Equal to any IStringLiteral with the same string value
equals(Object) - Method in class org.smtlib.impl.SMTExpr.Symbol
equals(Object) - Method in class org.smtlib.impl.Sort.Abbreviation
equals(Object) - Method in class org.smtlib.impl.Sort.Application
equals(Object) - Method in class org.smtlib.impl.Sort.Family
equals(Object) - Method in class org.smtlib.impl.Sort.FcnSort
equals(Object) - Method in class org.smtlib.impl.Sort.Parameter
equals(Object) - Method in interface org.smtlib.ISort: Structural equality after expansion of abbreviations (an alias and its literal expansion are equal), but without any substitution of free parameters.
equals(Object) - Method in interface org.smtlib.ISort.IApplication
equals(Object) - Method in interface org.smtlib.ISort.IParameter
equals(Object) - Method in record class org.smtlib.SolverResolver.Resolution: Indicates whether some other object is "equal to" this one.
equalsNoExpand(ISort) - Method in class org.smtlib.impl.Sort.Application
equalsNoExpand(ISort) - Method in class org.smtlib.impl.Sort.FcnSort
equalsNoExpand(ISort) - Method in class org.smtlib.impl.Sort.Parameter
equalsNoExpand(ISort) - Method in interface org.smtlib.ISort: Raw structural comparison, deliberately without abbreviation expansion or parameter substitution -- so a user-defined alias and its expansion, which ISort.equals(Object) treats as equal, are NOT equal here.
equalsNoExpand(ISort) - Method in interface org.smtlib.ISort.IApplication
equalsNoExpand(ISort) - Method in interface org.smtlib.ISort.IParameter
error - Variable in class org.smtlib.impl.Sort.ErrorDefinition
error(String) - Method in interface org.smtlib.IExpr.IFactory: Creates an error expression.
error(String) - Method in class org.smtlib.impl.Factory
error(String) - Method in class org.smtlib.impl.Response.Factory
error(String) - Method in interface org.smtlib.IResponse.IFactory
error(String) - Method in class org.smtlib.sexpr.Printer: Utility function to print error messages in this printer's format
error(String) - Method in class org.smtlib.SMT: Helper function to log a command-line error
error(String, IPos) - Method in class org.smtlib.impl.Response.Factory
error(String, IPos) - Method in interface org.smtlib.IResponse.IFactory
error(String, IPos) - Method in class org.smtlib.sexpr.Parser: Creates a ParserException with the given message and position; callers should throw the result.
error(String, IPos) - Method in class org.smtlib.TypeChecker: Utility method for recording an error
error(String, ILexToken) - Method in class org.smtlib.sexpr.Parser: Creates a ParserException from the given message and token; callers should throw the result.
error(SMT.Configuration, String, IPos) - Static method in class org.smtlib.impl.Command: Creates a ParserException with the given message and position.
Error(String) - Constructor for class org.smtlib.impl.Response.Error
Error(String) - Constructor for class org.smtlib.impl.SMTExpr.Error: Creates an error expression node with the given informational message.
Error(String, IPos) - Constructor for class org.smtlib.impl.Response.Error
ERROR_BEHAVIOR - Static variable in class org.smtlib.Utils: The string designating an info item
ErrorDefinition(IExpr.IIdentifier, String, IPos) - Constructor for class org.smtlib.impl.Sort.ErrorDefinition: Creates an error placeholder for the given identifier, error message, and source position.
errorMessage() - Method in class org.smtlib.impl.Sort.ErrorDefinition
errorMessage() - Method in interface org.smtlib.ISort.IErrorDefinition: The error message describing why the definition is ill-formed
errorMsg() - Method in class org.smtlib.impl.Response.Error
errorMsg() - Method in interface org.smtlib.IResponse.IError: Returns the error message held by this response
errorOut - Variable in class org.smtlib.SolverProcess
errorPos() - Method in class org.smtlib.impl.Sort.ErrorDefinition
errorPos() - Method in interface org.smtlib.ISort.IErrorDefinition: The source position of the error
errorResponse - Variable in exception class org.smtlib.Utils.SMTLIBException: The error response describing the problem that caused this exception.
errorSettleMillis - Variable in class org.smtlib.SolverProcess: How long (ms) to wait for error-stream text to arrive before concluding a command produced none, and (once some has arrived) how much longer to wait for further stragglers before returning it.
errorStopsSolver(IResponse) - Method in class org.smtlib.AbstractSolver: Whether, after the given error response, the solver stops processing input (whether or not its process actually exits).
errorStopsSolver(IResponse) - Method in class org.smtlib.solvers.Solver_cvc5: cvc5 carries on after most errors (e.g.
eval(List<ISort>) - Method in class org.smtlib.impl.Sort.Abbreviation
eval(List<ISort>) - Method in class org.smtlib.impl.Sort.ErrorDefinition
eval(List<ISort>) - Method in class org.smtlib.impl.Sort.Family
eval(List<ISort>) - Method in class org.smtlib.impl.Sort.Parameter
eval(List<ISort>) - Method in interface org.smtlib.ISort.IDefinition: A new sort expression that results from applying the sort symbol to a list of sort expressions
exc(Exception, Object) - Method in class org.smtlib.sexpr.Printer: Utility function to create an exception using the message from the first argument and the position from the second, if it is IPosable.
exec() - Method in class org.smtlib.SMT: Executes, presuming all options (e.g.
exec(String[]) - Method in class org.smtlib.Driver: The non-static entry point to the application
exec(String[]) - Method in class org.smtlib.SMT: The method that does all the execution for the main method, here made a non-static method, so that multiple SMT operations can be proceeding independently.
executable - Variable in class org.smtlib.SMT.Configuration: The path to the executable for the solver to use
executable() - Method in record class org.smtlib.SolverResolver.Resolution: Returns the value of the executable record component.
execute(ICommand) - Method in class org.smtlib.AbstractSolver: Once the solver process has exited, every command but exit (and a comment, which has no response) answers AbstractSolver.exitedResponse(), including those an adapter answers itself or checks with its own queries
execute(ICommand) - Method in interface org.smtlib.ISolver: Executes the command on this solver
execute(ICommand) - Method in class org.smtlib.solvers.Solver_test: Once exited, every command but exit (and a comment) answers as a process-based solver's would
execute(ISolver) - Method in class org.smtlib.command.C_assert
execute(ISolver) - Method in class org.smtlib.command.C_check_sat_assuming
execute(ISolver) - Method in class org.smtlib.command.C_check_sat
execute(ISolver) - Method in class org.smtlib.command.C_comment
execute(ISolver) - Method in class org.smtlib.command.C_declare_const
execute(ISolver) - Method in class org.smtlib.command.C_declare_datatype
execute(ISolver) - Method in class org.smtlib.command.C_declare_datatypes
execute(ISolver) - Method in class org.smtlib.command.C_declare_fun
execute(ISolver) - Method in class org.smtlib.command.C_declare_sort_parameter
execute(ISolver) - Method in class org.smtlib.command.C_declare_sort
execute(ISolver) - Method in class org.smtlib.command.C_define_const
execute(ISolver) - Method in class org.smtlib.command.C_define_fun_rec
execute(ISolver) - Method in class org.smtlib.command.C_define_fun
execute(ISolver) - Method in class org.smtlib.command.C_define_funs_rec
execute(ISolver) - Method in class org.smtlib.command.C_define_sort
execute(ISolver) - Method in class org.smtlib.command.C_echo
execute(ISolver) - Method in class org.smtlib.command.C_exit
execute(ISolver) - Method in class org.smtlib.command.C_get_assertions
execute(ISolver) - Method in class org.smtlib.command.C_get_assignment
execute(ISolver) - Method in class org.smtlib.command.C_get_info
execute(ISolver) - Method in class org.smtlib.command.C_get_model
execute(ISolver) - Method in class org.smtlib.command.C_get_option
execute(ISolver) - Method in class org.smtlib.command.C_get_proof
execute(ISolver) - Method in class org.smtlib.command.C_get_unsat_assumptions
execute(ISolver) - Method in class org.smtlib.command.C_get_unsat_core
execute(ISolver) - Method in class org.smtlib.command.C_get_value
execute(ISolver) - Method in class org.smtlib.command.C_pop
execute(ISolver) - Method in class org.smtlib.command.C_push
execute(ISolver) - Method in class org.smtlib.command.C_reset_assertions
execute(ISolver) - Method in class org.smtlib.command.C_reset
execute(ISolver) - Method in class org.smtlib.command.C_set_info
execute(ISolver) - Method in class org.smtlib.command.C_set_logic
execute(ISolver) - Method in class org.smtlib.command.C_set_option
execute(ISolver) - Method in class org.smtlib.ext.C_exec: Executes the command, which executes the script
execute(ISolver) - Method in class org.smtlib.ext.C_what
execute(ISolver) - Method in interface org.smtlib.ICommand: Executes the command on the given solver; presumes that the command type-checked successfully.
execute(ISolver) - Method in interface org.smtlib.ICommand.IScript
execute(ISolver) - Method in class org.smtlib.impl.Script: Executes the current list
executePipelined(List<ICommand>) - Method in class org.smtlib.AbstractSolver: Executes the commands in order, as a script does: returns the first error, or else the last command's response.
exists(List<IExpr.IDeclaration>, IExpr) - Method in interface org.smtlib.IExpr.IFactory: Creates an Exists expression.
exists(List<IExpr.IDeclaration>, IExpr) - Method in class org.smtlib.impl.Factory
exists(List<IExpr.IDeclaration>, IExpr, List<IExpr>) - Method in interface org.smtlib.IExpr.IFactory: Creates an Exists expression with trigger patterns: each element of patterns is a separate single-term pattern, emitted as :pattern (p).
exists(List<IExpr.IDeclaration>, IExpr, List<IExpr>) - Method in class org.smtlib.impl.Factory
Exists(List<IExpr.IDeclaration>, IExpr) - Constructor for class org.smtlib.impl.SMTExpr.Exists: Creates an exists expression with the given bound variable declarations and body.
EXISTS - Static variable in class org.smtlib.sexpr.Utils
EXISTS - Static variable in class org.smtlib.Utils: The String for the exists reserved word
exit() - Method in class org.smtlib.AbstractSolver
exit() - Method in interface org.smtlib.ICommand.IFactory: Creates an exit command object.
exit() - Method in class org.smtlib.impl.Factory
exit() - Method in interface org.smtlib.ISolver: Terminates the solver; no further commands are permitted.
exit() - Method in class org.smtlib.SolverProcess: Aborts the process; returns immediately if already stopped
exit() - Method in class org.smtlib.solvers.Solver_altergo: Alt-Ergo is silent for exit, as for any successful command, but no echo can follow it, since the process ends; so success is answered once the process has ended.
exit() - Method in class org.smtlib.solvers.Solver_simplify
exit() - Method in class org.smtlib.solvers.Solver_test
exit() - Method in class org.smtlib.solvers.Solver_z3_4_3
exitedResponse() - Method in class org.smtlib.AbstractSolver: The response to any command once the solver process has exited: timeout if its whole-run time limit ended it, else the error AbstractSolver.SOLVER_EXITED; null while the process runs (or has not been started)
EXP - Static variable in class org.smtlib.Utils
expand() - Method in class org.smtlib.impl.Sort.Application
expand() - Method in class org.smtlib.impl.Sort.FcnSort
expand() - Method in class org.smtlib.impl.Sort.Parameter
expand() - Method in interface org.smtlib.ISort: Expands all abbreviations
expand() - Method in interface org.smtlib.ISort.IApplication: Expands any head abbreviations, if any; requires definition() to be defined
EXPAND_DEFINITIONS - Static variable in class org.smtlib.Utils: The string designating an option item
expanded - Variable in class org.smtlib.impl.Sort.Application: Cached value for expanded()
expr() - Method in class org.smtlib.command.C_assert: Returns the asserted formula
expr() - Method in interface org.smtlib.ICommand.Iassert: Returns the expression to be asserted.
expr() - Method in interface org.smtlib.IExpr.IAttributedExpr
expr() - Method in interface org.smtlib.IExpr.IBinding
expr() - Method in interface org.smtlib.IExpr.IExists
expr() - Method in interface org.smtlib.IExpr.IForall
expr() - Method in interface org.smtlib.IExpr.ILambda
expr() - Method in interface org.smtlib.IExpr.ILet
expr() - Method in interface org.smtlib.IExpr.IMatch
expr() - Method in class org.smtlib.impl.SMTExpr.AttributedExpr
expr() - Method in class org.smtlib.impl.SMTExpr.Binding
expr() - Method in class org.smtlib.impl.SMTExpr.Exists
expr() - Method in class org.smtlib.impl.SMTExpr.Forall
expr() - Method in class org.smtlib.impl.SMTExpr.Lambda
expr() - Method in class org.smtlib.impl.SMTExpr.Let
expr() - Method in class org.smtlib.impl.SMTExpr.Match
expression - Variable in class org.smtlib.command.C_define_fun: The defining expression for the function
expression - Variable in class org.smtlib.command.C_define_sort: The defining expression for the function
expression - Variable in class org.smtlib.impl.SMTExpr.AttributedExpr
expression - Variable in class org.smtlib.impl.SMTExpr.Binding
expression - Variable in class org.smtlib.impl.SMTExpr.Exists
expression - Variable in class org.smtlib.impl.SMTExpr.Forall
expression - Variable in class org.smtlib.impl.SMTExpr.Lambda
expression - Variable in class org.smtlib.impl.SMTExpr.Let
expression - Variable in class org.smtlib.impl.SMTExpr.Match
expression - Variable in class org.smtlib.TypeChecker.Variable
expression() - Method in class org.smtlib.command.C_define_fun: The defining expression for the function
expression() - Method in class org.smtlib.command.C_define_sort: The defining expression for the function
expression() - Method in interface org.smtlib.ICommand.Idefine_fun_rec: Returns the defining expression (body).
expression() - Method in interface org.smtlib.ICommand.Idefine_fun: Returns the defining expression (body).
expression() - Method in interface org.smtlib.ICommand.Idefine_sort: Returns the sort expression that is the definition.
exprFactory - Variable in class org.smtlib.SMT.Configuration: The factory to use to create IExpr objects
exprs() - Method in class org.smtlib.command.C_get_value: The terms whose values are to be gotten
exprs() - Method in interface org.smtlib.ICommand.Iget_value: Returns the list of expressions whose values are requested.
EXTRACT - 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