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

R

RANDOM_SEED - Static variable in class org.smtlib.Utils

The string designating an option item

rdr - Variable in class org.smtlib.CharSequenceReader

The Reader that supplies characters for the CharSequence

readChars() - Method in class org.smtlib.CharSequenceInfinite

Reads more characters into the buffer; may block until some are read; returns false if end of input has been reached, in which case no additional chars should have been read.

readChars() - Method in class org.smtlib.CharSequenceReader

readChars() - Method in class org.smtlib.CharSequenceSocket

readErrorOutput(long) - Method in class org.smtlib.SolverProcess

For pipelined reading: the text that has arrived on standard error, waiting up to waitMillis for some (see StreamGobbler.drain)

readOutput(long) - Method in class org.smtlib.SolverProcess

For pipelined reading, which, unlike SolverProcess.listen(), does not pair the text with one command: the next text the solver wrote on standard output, waiting up to waitMillis for it (not at all if 0; until some arrives or the output ends if negative).

readPipelined(boolean) - Method in class org.smtlib.AbstractSolver

Reads what the solver has written for pipelined commands, matching each response to its command in order; with wait, until every pending command has its response (or the solver has stopped), else only what has already arrived.

readProperties() - Method in class org.smtlib.SMT.Configuration

readRemainingErrorOutput() - Method in class org.smtlib.SolverProcess

For pipelined reading, once the output has ended: the rest of the text on standard error, up to its end (waiting at most endDrainMillis)

realsIntsTheorySet - Variable in class org.smtlib.SymbolTable

true if the RealsInts theory is set (which allows implicit promotion of ints to reals)

REASON_UNKNOWN - Static variable in class org.smtlib.Utils

The string designating an info item

recordChange(AbstractSolver.StackChange, IResponse) - Method in class org.smtlib.AbstractSolver

Records the response to a command of the given kind that changes the assertion stack, and returns it.

REGULAR_OUTPUT_CHANNEL - Static variable in class org.smtlib.Utils

The string designating an option item

relax - Variable in class org.smtlib.SMT.Configuration

When true, allows some convenience relaxations of the SMTLIB standard; when false, the standard is strictly enforced.

remove() - Method in class org.smtlib.SymbolTable.Iterator

removeListener(Log.IListener) - Method in class org.smtlib.Log

Removes a listener (found by using object equality ==)

REPEAT - Static variable in class org.smtlib.Utils

reportsEarlierLines() - Method in class org.smtlib.AbstractSolver

Whether the solver's messages name lines of earlier commands (see AbstractSolver.earlierSourceLine(int))

reportsEarlierLines() - Method in class org.smtlib.solvers.Solver_bitwuzla

reportSeedIgnored() - Method in class org.smtlib.AbstractSolver

Reports that --seed, if given, is ignored, for an adapter whose solver has no random seed

REPRODUCIBLE_RESOURCE_LIMIT - Static variable in class org.smtlib.Utils

The string designating an option item

requireNoChangeSinceCheck(String, Set<AbstractSolver.StackChange>) - Method in class org.smtlib.AbstractSolver

Returns an error response if, since a check command, the solver has accepted a command of one of the given kinds (after which the solver wrongly keeps answering the get- commands about that check, which SMT-LIB's assert mode makes errors), else null

requireOptionEnabled(String, String) - Method in class org.smtlib.AbstractSolver

Returns an error response if the given option has not been enabled (per AbstractSolver.get_option(IKeyword)), else null.

requireSatOrUnknown(String) - Method in class org.smtlib.AbstractSolver

Returns an error response unless AbstractSolver.checkStatus() is sat or unknown, else null.

requireUnsat(String, String) - Method in class org.smtlib.AbstractSolver

Returns an error response unless AbstractSolver.checkStatus() is unsat, else null.

reservedSince - Static variable in class org.smtlib.sexpr.Utils

The SMT-LIB version in which a reserved word became reserved, for those not reserved in V2.0

reservedSince - Variable in class org.smtlib.SMT.Configuration

The version in which a reserved word became reserved, for those not reserved in V2.0

reservedWords - Static variable in class org.smtlib.sexpr.Utils

All reserved words (reserved-non-commands plus command names)

reservedWords - Variable in class org.smtlib.SMT.Configuration

A list of all reserved words

reservedWordsNotCommands - Static variable in class org.smtlib.sexpr.Utils

Reserved words that are not commands (e.g.

reservedWordsNotCommands - Variable in class org.smtlib.SMT.Configuration

A list of reserved words that are not commands

reset() - Method in class org.smtlib.AbstractSolver

reset() - Method in interface org.smtlib.ICommand.IFactory

Creates a reset command object.

reset() - Method in class org.smtlib.impl.Factory

reset() - Method in interface org.smtlib.ISolver

Resets the solver to the initial state, clearing all assertions, declarations, and options.

reset() - Method in class org.smtlib.solvers.Solver_bitwuzla

Bitwuzla's reset restores its option defaults, so the values get_option answers from are dropped too (except the output channels, which are jSMTLIB's own and stay redirected).

reset() - Method in class org.smtlib.solvers.Solver_cvc5

reset() - Method in class org.smtlib.solvers.Solver_simplify

Transplanted from Solver_test.reset(): this class has no real process operation to ask for a reset (Simplify's protocol has no such concept), so this remains an entirely local, client-side reset exactly as it was as an inherited Solver_test method -- it does not, and did not before this restructuring, reset any BG_PUSH state already accumulated in the real Simplify process itself.

reset() - Method in class org.smtlib.solvers.Solver_test

reset() - Method in class org.smtlib.solvers.Solver_z3_4_3

reset() - Method in class org.smtlib.solvers.Solver_z3_recent

reset_assertions() - Method in class org.smtlib.AbstractSolver

reset_assertions() - Method in interface org.smtlib.ICommand.IFactory

Creates a reset-assertions command object.

reset_assertions() - Method in class org.smtlib.impl.Factory

reset_assertions() - Method in interface org.smtlib.ISolver

Removes asserted formulae (but not global declarations when :global-declarations is true).

reset_assertions() - Method in class org.smtlib.solvers.Solver_altergo

Alt-Ergo ignores reset-assertions, writing nothing and keeping the assertions; answered unsupported without sending it

reset_assertions() - Method in class org.smtlib.solvers.Solver_bitwuzla

reset_assertions() - Method in class org.smtlib.solvers.Solver_simplify

Transplanted from Solver_test.reset_assertions().

reset_assertions() - Method in class org.smtlib.solvers.Solver_test

reset_assertions() - Method in class org.smtlib.solvers.Solver_z3_4_3

z3-4.3 predates reset-assertions (added in SMT-LIB 2.5), and turns out to already handle that gracefully on its own: sent the literal, unrecognized command text, its SMT2 front-end replies with the literal token "unsupported" -- confirmed directly against a real z3-4.3.1 binary -- rather than erroring or crashing.

RESET_ASSERTIONS - Enum constant in enum class org.smtlib.AbstractSolver.StackChange

Resolution(String, Class<?>, String, String, String[]) - Constructor for record class org.smtlib.SolverResolver.Resolution

Creates an instance of a Resolution record class.

resolve(Properties, String, String, String, String, Function<String, Class<?>>) - Static method in class org.smtlib.SolverResolver

Resolves the solver: the adapter: a .adapter.<platform> property, then .adapter (an error if the class it names is not found); else the class Solver_<name> (with - and .

resolveExecutableForSolver(String) - Method in class org.smtlib.SMT

Resolves the executable path SMT.startSolver(org.smtlib.SMT.Configuration, java.lang.String, java.lang.String) would use for the given solver name (absent an explicit caller-supplied override -- startSolver's own executable parameter takes precedence there, which this standalone method has no equivalent of), without instantiating an adapter or starting anything -- lets a caller check whether the file actually exists before committing to run tests against it (see the test harness's LogicTests#solversFromEnv, which filters the solver list against this up front so a missing binary is one WARNING line instead of a wall of per-file failures).

resolveExecutablePath(String, String) - Static method in class org.smtlib.SMT

Resolves the path of a solver executable, whether from the properties (.exec or the solver name) or supplied by the caller: null, or an absolute path: returned unchanged; a relative path with a directory part (e.g.

resolveFcnSort(SymbolTable, IExpr.IIdentifier, List<ISort>, ISort, IPos, List<IResponse>) - Static method in class org.smtlib.TypeChecker

Checks a function signature as checkFcn does, adding any errors to errors; returns the signature with its sorts resolved in the current scope (so a sort parameter in scope becomes its IParameter), or null if there were errors.

response() - Method in class org.smtlib.AbstractSolver.Pending

The response read for the command, or null if not yet read

Response - Class in org.smtlib.impl

This class holds subclasses that are implementations of the various IResponse interfaces.

Response.AssertionsResponse - Class in org.smtlib.impl

Implements the IResponse.IAssertionsResponse interface

Response.AssignmentResponse - Class in org.smtlib.impl

Implements the IResponse.IAssignmentResponse interface

Response.Error - Class in org.smtlib.impl

Implements the IResponse.IError interface

Response.Factory - Class in org.smtlib.impl

Implements the IResponse.IFactory interface

Response.Pair<T1,T2> - Class in org.smtlib.impl

Implements the IResponse.IPair interface

Response.ProofResponse - Class in org.smtlib.impl

Implements the IResponse.IProofResponse interface

Response.Seq - Class in org.smtlib.impl

Implementation of IAttributeList: a list of attributes returned by get-info.

Response.UnsatAssumptionsResponse - Class in org.smtlib.impl

Implements the IResponse.IUnsatAssumptionsResponse interface

Response.UnsatCoreResponse - Class in org.smtlib.impl

Implements the IResponse.IUnsatCoreResponse interface

Response.ValueResponse - Class in org.smtlib.impl

Implements the IResponse.IValueResponse interface

responseEnd(CharSequence, int) - Static method in class org.smtlib.AbstractSolver

The index just past the response that starts at start (an atom, a string literal, a quoted symbol, or one balanced S-expression), or -1 if that response is not yet complete

responseFactory - Variable in class org.smtlib.SMT.Configuration

The factory to use to create IResponse objects

responseParser - Variable in class org.smtlib.solvers.Solver_z3_4_3

The parser that parses responses from the solver

restrictionError(String, IExpr) - Method in class org.smtlib.logic.Logic

Builds a VisitorException for a restriction violation (e.g.

result - Variable in class org.smtlib.TypeChecker

Compilation of errors

resultSort - Variable in class org.smtlib.command.C_declare_fun

The result sort of the function being declared

resultSort - Variable in class org.smtlib.command.C_define_fun

The sort of the result

resultSort - Variable in class org.smtlib.impl.Sort.FcnSort

resultSort() - Method in class org.smtlib.command.C_declare_fun

resultSort() - Method in class org.smtlib.command.C_define_fun

The result sort

resultSort() - Method in interface org.smtlib.ICommand.Ideclare_const

Returns the sort of the constant being declared.

resultSort() - Method in interface org.smtlib.ICommand.Ideclare_fun

Returns the result sort.

resultSort() - Method in interface org.smtlib.ICommand.Idefine_fun_rec

Returns the result sort.

resultSort() - Method in interface org.smtlib.ICommand.Idefine_fun

Returns the result sort.

resultSort() - Method in class org.smtlib.impl.Sort.FcnSort

resultSort() - Method in interface org.smtlib.ISort.IFcnSort

ROTATE_LEFT - Static variable in class org.smtlib.Utils

ROTATE_RIGHT - Static variable in class org.smtlib.Utils

ROUNDINGMODE_SYM - Static variable in class org.smtlib.Utils

RP - Static variable in interface org.smtlib.sexpr.Lexer.IPLexToken

RP(int) - Method in class org.smtlib.sexpr.Lexer

Creates a lexical token for a right parenthesis at the given position

run() - Method in interface org.smtlib.sexpr.Printer.PrintArgs

run() - Method in class org.smtlib.SolverProcess.StreamGobbler

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