Index
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form
U
- UBV_TO_INT - Static variable in class org.smtlib.Utils
-
Bitvector/Int conversions and overflow predicates (SMT-LIB 2.7 FixedSizeBitVectors).
- UFLRA - Class in org.smtlib.logic
- UFLRA(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.UFLRA
- UFNIA - Class in org.smtlib.logic
- UFNIA(SMT.Configuration, IExpr.ISymbol, Collection<IExpr.IAttribute<?>>) - Constructor for class org.smtlib.logic.UFNIA
- unescape(String) - Method in class org.smtlib.Utils
-
Converts a quoted string (which has enclosing double quotes) to a raw sequence of ASCII characters, undoing any SMT-LIBv2 escape sequences, and without the enclosing quotes
- UNEXPECTED_RESPONSE - Static variable in class org.smtlib.sexpr.Parser
-
The start of the error message for solver text that is not SMT-LIB (see parseResponse)
- unheld(Supplier<T>) - Method in class org.smtlib.Log
-
Returns the computation's result, logging what it logs at once rather than holding it (e.g.
- unknown() - Method in class org.smtlib.impl.Response.Factory
- unknown() - Method in interface org.smtlib.IResponse.IFactory
- UNKNOWN - Enum constant in enum class org.smtlib.SolverCapabilities.Support
- UNKNOWN - Static variable in class org.smtlib.impl.Response
- unquotedString(String) - Method in interface org.smtlib.IExpr.IFactory
-
Creates an IStringLiteral from a pure character string with no SMT-LIB escapes or enclosing quotes.
- unquotedString(String) - Method in class org.smtlib.impl.Factory
- unreadOutput() - Method in class org.smtlib.SolverProcess
-
The text the solver wrote that has not been read as a response, on stdout and on stderr (in that order): e.g.
- unsat() - Method in class org.smtlib.impl.Response.Factory
- unsat() - Method in interface org.smtlib.IResponse.IFactory
- UNSAT - Static variable in class org.smtlib.impl.Response
- unsatAssumptionsElements(List<IExpr>) - Method in class org.smtlib.AbstractSolver
-
The elements of a get-unsat-assumptions reply that belong in the response (all of them); an adapter whose solver's reply holds others filters them out
- unsatAssumptionsElements(List<IExpr>) - Method in class org.smtlib.solvers.Solver_z3_recent
-
Drops the labels z3 adds to the unsat assumptions (see Assumptions)
- UnsatAssumptionsResponse(List<IExpr>) - Constructor for class org.smtlib.impl.Response.UnsatAssumptionsResponse
- unsatCoreElements(List<IExpr>) - Method in class org.smtlib.AbstractSolver
-
The elements of a get-unsat-core reply that belong in the unsat core (all of them); an adapter whose solver's reply holds others filters them out
- unsatCoreElements(List<IExpr>) - Method in class org.smtlib.solvers.Solver_z3_4_3
-
Drops the assumptions z3 4.3 adds to the unsat core after check-sat-assuming
- unsatCoreElements(List<IExpr>) - Method in class org.smtlib.solvers.Solver_z3_recent
-
Drops the assumptions z3 adds to the unsat core (see Assumptions)
- UnsatCoreResponse(List<IExpr.ISymbol>) - Constructor for class org.smtlib.impl.Response.UnsatCoreResponse
- unsupported() - Method in class org.smtlib.impl.Response.Factory
- unsupported() - Method in interface org.smtlib.IResponse.IFactory
- UNSUPPORTED - Static variable in class org.smtlib.impl.Response
- usage() - Method in class org.smtlib.Driver
-
Prints out the usage information
- usage() - Method in class org.smtlib.SMT
-
Prints a summary of the command-line arguments
- utils - Variable in class org.smtlib.SMT.Configuration
-
The utils object to use for utility methods
- Utils - Class in org.smtlib.sexpr
-
Constants and reserved-word sets specific to the S-expression concrete syntax.
- Utils - Class in org.smtlib
-
A class of static utility methods and constants for the SMT-LIB package.
- Utils(SMT.Configuration) - Constructor for class org.smtlib.Utils
-
Creates a Utils instance for the given configuration
- Utils.SMTLIBException - Exception Class in org.smtlib
-
A checked exception used internally to propagate SMT-LIB errors that carry an IResponse.IError.
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form