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

T

takeDiagnosticOutput(boolean) - Method in class org.smtlib.SolverProcess: Returns and clears the solver's diagnostic output: standard-error text read with a reply on standard output, which answered instead (see listen()).
terms - Variable in class org.smtlib.command.C_check_sat_assuming: The boolean-sorted terms to assume.
terms - Variable in class org.smtlib.command.C_get_value: The terms whose values are to be gotten
terms - Variable in class org.smtlib.impl.SMTExpr.PatternTerms
terms() - Method in class org.smtlib.command.C_check_sat_assuming: Returns the boolean-sorted terms to assume.
terms() - Method in interface org.smtlib.ICommand.Icheck_sat_assuming: Returns the boolean-sorted terms to assume.
terms() - Method in interface org.smtlib.IExpr.IPatternTerms
terms() - Method in class org.smtlib.impl.SMTExpr.PatternTerms
TEST_SOLVER - Static variable in class org.smtlib.Utils: The name of the test solver, implemented by this SMT app.
testing - Variable in class org.smtlib.SMT.Configuration: When true, a solver's raw response text is scrubbed of known non-deterministic content (elapsed-time figures, memory usage) before being parsed, replacing each with a fixed placeholder (e.g.
text - Variable in class org.smtlib.command.C_comment
text - Variable in class org.smtlib.SMT.Configuration: A string containing the SMT-LIB commands to use; if null the given file is used; if non-null this text is used instead of the content of the file or the input from a port.
text() - Method in class org.smtlib.command.C_comment
text() - Method in interface org.smtlib.ICommand.Icomment: Returns the raw comment text (as captured from source, or as supplied directly via the public API), not yet split into per-line ;-prefixed form -- see Command.write(org.smtlib.sexpr.Printer).
textLine(int) - Method in class org.smtlib.impl.Pos.Source
textLine(int) - Method in interface org.smtlib.ISource: Returns the text of the line containing the given position, at least through the given position, and always ending with a (perhaps added) line termination sequence.
THEORIES - Static variable in class org.smtlib.Utils: The attribute tag for defining theories in a logic
Theory(IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.impl.SMTExpr.Theory: Creates a theory
THEORY - Static variable in class org.smtlib.sexpr.Utils
THEORY - Static variable in class org.smtlib.Utils: The String for the theory symbol
theoryName - Variable in class org.smtlib.impl.SMTExpr.Theory: The name of the theory
theoryName() - Method in class org.smtlib.impl.SMTExpr.Theory: The name of the theory
theoryName() - Method in interface org.smtlib.ITheory: The name of the theory
timeLimitResponse(String) - Method in class org.smtlib.AbstractSolver: Returns responseFactory.timeout(), recording that the solver has ended, if the raw response reports that the solver's whole-run time limit ended it; otherwise null.
timeLimitResponseAfterExit() - Method in class org.smtlib.AbstractSolver: For when a send has found the solver process gone: the timeout response if the process left this solver's report that its whole-run time limit ended it unread (that limit runs on the wall clock, so it can end the solver between commands, and its report then answers no command), or if it ended once that limit had passed; otherwise null
timeout - Variable in class org.smtlib.SMT.Configuration: The soft, per-query timeout, in seconds (fractional allowed), set via -t/--timeout; <=0 means no timeout.
timeout() - Method in class org.smtlib.impl.Response.Factory
timeout() - Method in interface org.smtlib.IResponse.IFactory: The response when the solver's whole-run time limit (SMT.Configuration#timeoutTotal) ended it, normalized across solvers (z3 answers 'timeout' and exits; cvc5 reports the timeout on stderr and aborts); every later command to that solver gets the same response.
TIMEOUT - Static variable in class org.smtlib.impl.Response
timeoutTotal - Variable in class org.smtlib.SMT.Configuration: The whole-run (solver-process-lifetime) timeout, in seconds (fractional allowed), set via -T/--timeout-total; <=0 means no timeout.
TO_FP - Static variable in class org.smtlib.Utils
TO_FP_UNSIGNED - Static variable in class org.smtlib.Utils
token - Variable in enum class org.smtlib.SolverCapabilities.Capability
Token(T) - Constructor for class org.smtlib.sexpr.Sexpr.Token
topLevel - Variable in class org.smtlib.SMT.Configuration: Encodes an aspect of current parser state so that we know what kind of prompt to use.
toProcess - Variable in class org.smtlib.SolverProcess: The Writer object that writes to the spawned process (initialized by start() )
toString() - Method in class org.smtlib.AbstractSolver.Pending
toString() - Method in interface org.smtlib.IExpr.IConstructor
toString() - Method in interface org.smtlib.IExpr.IKeyword: The original textual representation of the keyword
toString() - Method in interface org.smtlib.IExpr.ISelector
toString() - Method in interface org.smtlib.IExpr.IStringLiteral: Returns a value with enclosing quotes and appropriate SMT-LIB escape sequences so that the String value can be represented with SMT-LIB printable characters; the result may have explicit newline characters.
toString() - Method in interface org.smtlib.IExpr.ISymbol: A printable String giving the original text of this symbol.
toString() - Method in class org.smtlib.impl.Pos.Printable
toString() - Method in class org.smtlib.impl.SMTExpr.Symbol: Returns the original String - use for debugging and use a printer to print to concrete syntax.
toString() - Method in interface org.smtlib.ISort.IDatatype
toString() - Method in class org.smtlib.sexpr.Lexer.LexToken
toString() - Method in enum class org.smtlib.SMT.Configuration.SMTLIB
toString() - Method in record class org.smtlib.SolverResolver.Resolution: Returns a string representation of this record class.
toString(T) - Method in interface org.smtlib.IPrinter: Returns the argument as a String using a Printer of the same type as the receiver, but does not modify the receiver.
toString(T) - Method in class org.smtlib.sexpr.Printer: Returns the argument as a String using a Printer of the same type as the receiver, but does not modify the receiver.
toString(T) - Method in class org.smtlib.solvers.Printer
trailingText - Variable in class org.smtlib.impl.Command: Whitespace/comment text, if any, that appeared on the same physical source line immediately after this command's closing parenthesis (before the next line terminator) -- typically a trailing "; comment".
trailingText() - Method in class org.smtlib.impl.Command: The text captured in Command.trailingText, or null if this command has none.
translate(IExpr) - Method in class org.smtlib.solvers.Solver_simplify
translate(INode) - Method in class org.smtlib.AbstractSolver: Translates an in-memory node into the text sent to the solver process.
translate(INode) - Method in class org.smtlib.solvers.Solver_smt: Translates an S-expression into SMT syntax; this solver uses the standard S-expression concrete syntax except for a Bool-quantifier workaround (see Printer).
translate(INode) - Method in class org.smtlib.solvers.Solver_z3_4_3: Translates an S-expression into Z3 syntax
translate(INode) - Method in class org.smtlib.solvers.Solver_z3_4_5: z3 4.5 rejects every check-sat-assuming ("invalid check-sat-assuming command, '(', expected", a parser bug), so it is sent as z3's legacy (check-sat a1 ...
Translator(Writer) - Constructor for class org.smtlib.solvers.Solver_z3_4_3.Translator
Translator(SMT.Configuration) - Constructor for class org.smtlib.solvers.Solver_simplify.Translator
Translator(SMT.Configuration, boolean) - Constructor for class org.smtlib.solvers.Solver_simplify.Translator
TreeVisitor() - Constructor for class org.smtlib.IVisitor.TreeVisitor
TRUE - Static variable in class org.smtlib.Utils: Symbol constant for boolean true.
TypeChecker - Class in org.smtlib: This class is a visitor that type-checks a formula
TypeChecker(SymbolTable) - Constructor for class org.smtlib.TypeChecker: Constructs a formula typechecker from the current symbol table; sorts computed while checking are recorded directly on each IExpr node via IExpr.setSort().
TypeChecker.Variable - Class in org.smtlib

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