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

G

GE - Static variable in class org.smtlib.Utils
get_assertions() - Method in class org.smtlib.AbstractSolver
get_assertions() - Method in interface org.smtlib.ICommand.IFactory: Creates a get-assertions command object.
get_assertions() - Method in class org.smtlib.impl.Factory
get_assertions() - Method in interface org.smtlib.ISolver: Returns the list of formulae in the current assertion set, in the order they were asserted.
get_assertions() - Method in class org.smtlib.solvers.Solver_altergo: Alt-Ergo ignores get-assertions, writing nothing; answered unsupported without sending it
get_assertions() - Method in class org.smtlib.solvers.Solver_bitwuzla: See Solver_bitwuzla.get_proof(): Bitwuzla rejects get-assertions the same way.
get_assertions() - Method in class org.smtlib.solvers.Solver_cvc5: cvc5 answers get-assertions with :produce-assertions off
get_assertions() - Method in class org.smtlib.solvers.Solver_simplify: See Solver_test.get_assertions().
get_assertions() - Method in class org.smtlib.solvers.Solver_test
get_assertions() - Method in class org.smtlib.solvers.Solver_z3_4_3: Not a correction: this adapter sends commands by its own means (z3 4.3 itself reports get-assertions without :produce-assertions, which set_option_impl sends as :interactive-mode)
get_assertions_response(List<IExpr>) - Method in class org.smtlib.impl.Response.Factory
get_assertions_response(List<IExpr>) - Method in interface org.smtlib.IResponse.IFactory
get_assignment() - Method in class org.smtlib.AbstractSolver
get_assignment() - Method in interface org.smtlib.ICommand.IFactory: Creates a get-assignment command object.
get_assignment() - Method in class org.smtlib.impl.Factory
get_assignment() - Method in interface org.smtlib.ISolver: Returns the truth-value assignments for all named Boolean formulae in the current model.
get_assignment() - Method in class org.smtlib.solvers.Solver_altergo: Alt-Ergo answers get-assignment in assert mode after a check.
get_assignment() - Method in class org.smtlib.solvers.Solver_bitwuzla: See Solver_bitwuzla.get_proof(): Bitwuzla rejects get-assignment the same way.
get_assignment() - Method in class org.smtlib.solvers.Solver_cvc5: cvc5 answers get-assignment with :produce-assignments off (if :produce-models is on), and in assert mode after a check
get_assignment() - Method in class org.smtlib.solvers.Solver_simplify: See Solver_test.get_assignment().
get_assignment() - Method in class org.smtlib.solvers.Solver_smtinterpol: SMTInterpol answers get-assignment after unsat, and in assert mode after a check
get_assignment() - Method in class org.smtlib.solvers.Solver_test
get_assignment() - Method in class org.smtlib.solvers.Solver_yices2: yices2 answers get-assignment with :produce-assignments off, and in assert mode after a check
get_assignment() - Method in class org.smtlib.solvers.Solver_z3_4_3: z3 4.3 answers get-assignment (with ()) when :produce-assignments is not enabled, which SMT-LIB makes an error
get_assignment() - Method in class org.smtlib.solvers.Solver_z3_recent: z3 answers get-assignment with :produce-assignments off, and in assert mode after a check
get_assignment_response(List<IResponse.IPair<IExpr.ISymbol, Boolean>>) - Method in class org.smtlib.impl.Response.Factory
get_assignment_response(List<IResponse.IPair<IExpr.ISymbol, Boolean>>) - Method in interface org.smtlib.IResponse.IFactory
get_info(IExpr.IKeyword) - Method in class org.smtlib.AbstractSolver
get_info(IExpr.IKeyword) - Method in interface org.smtlib.ICommand.IFactory: Creates a get-info command object.
get_info(IExpr.IKeyword) - Method in class org.smtlib.impl.Factory
get_info(IExpr.IKeyword) - Method in interface org.smtlib.ISolver: Returns the value of the named info item.
get_info(IExpr.IKeyword) - Method in class org.smtlib.solvers.Solver_bitwuzla: Answered entirely client-side (never forwarded -- see class comment point 1).
get_info(IExpr.IKeyword) - Method in class org.smtlib.solvers.Solver_simplify: Simplify has no get-info; answered here
get_info(IExpr.IKeyword) - Method in class org.smtlib.solvers.Solver_test
get_info(IExpr.IKeyword) - Method in class org.smtlib.solvers.Solver_yices2: yices2 answers get-info :status with the last set-info :status value, but with (error "no info for :status") when none was set; SMT-LIB requires unsupported for a flag the solver does not support.
get_info(IExpr.IKeyword) - Method in class org.smtlib.solvers.Solver_z3_4_3: Not a correction: this adapter sends commands by its own means, so it scrubs run-dependent values for testing itself, as AbstractSolver.get_info does
get_info(IExpr.IKeyword) - Method in class org.smtlib.solvers.Solver_z3_recent: z3 reports a query stopped by its per-query time limit, -t:, with :reason-unknown "canceled" in incremental mode (after a push; checked with z3 4.16.0 and 5.1.0, while 4.8.12 and 4.12.6 give up first, as incomplete), and in every mode in 4.6 and 4.7; one-shot queries in newer versions, and other solvers such as cvc5, report "timeout".
get_info_response(List<IExpr.IAttribute<?>>) - Method in interface org.smtlib.IResponse.IFactory
get_info_response(List<IExpr.IAttribute<? extends IAttributeValue>>) - Method in class org.smtlib.impl.Response.Factory
get_info_response(IExpr.IAttribute<?>) - Method in interface org.smtlib.IResponse.IFactory
get_info_response(IExpr.IAttribute<? extends IAttributeValue>) - Method in class org.smtlib.impl.Response.Factory
get_model() - Method in class org.smtlib.AbstractSolver
get_model() - Method in interface org.smtlib.ICommand.IFactory: Creates a get-model command object.
get_model() - Method in class org.smtlib.impl.Factory
get_model() - Method in interface org.smtlib.ISolver: Returns a satisfying model for the current assertion set.
get_model() - Method in class org.smtlib.solvers.Solver_altergo: Alt-Ergo answers get-model in assert mode after a check
get_model() - Method in class org.smtlib.solvers.Solver_bitwuzla: With :produce-models on, Bitwuzla writes nothing for get-model unless its last check returned sat (and crashes if a reset came since); after an assert, push, pop or reset-assertions, or with the option set after the check, it writes an ordinary error.
get_model() - Method in class org.smtlib.solvers.Solver_cvc5: cvc5 answers get-model in assert mode after a check
get_model() - Method in class org.smtlib.solvers.Solver_simplify: See Solver_test.get_model().
get_model() - Method in class org.smtlib.solvers.Solver_smtinterpol: SMTInterpol answers get-model with :produce-models off, and in assert mode after a check
get_model() - Method in class org.smtlib.solvers.Solver_test
get_model() - Method in class org.smtlib.solvers.Solver_yices2: yices2 answers get-model with :produce-models off, and in assert mode after a check
get_model() - Method in class org.smtlib.solvers.Solver_z3_4_3: The :produce-models check corrects z3 4.3 answering get-model with that option at its (non-standard) default of true; z3 4.3 itself reports get-model when no model is available
get_model() - Method in class org.smtlib.solvers.Solver_z3_recent: z3 answers get-model in assert mode after a check
get_option(IExpr.IKeyword) - Method in class org.smtlib.AbstractSolver
get_option(IExpr.IKeyword) - Method in interface org.smtlib.ICommand.IFactory: Creates a get-option command object.
get_option(IExpr.IKeyword) - Method in class org.smtlib.impl.Factory
get_option(IExpr.IKeyword) - Method in interface org.smtlib.ISolver: Returns the current value of the named option.
get_option(IExpr.IKeyword) - Method in class org.smtlib.solvers.Solver_altergo: Alt-Ergo ignores get-option, writing nothing; answered from the values set (see set_option_impl) and the SMT-LIB defaults
get_option(IExpr.IKeyword) - Method in class org.smtlib.solvers.Solver_bitwuzla: Answered entirely client-side (never forwarded -- see class comment point 1): from whatever this run has set via Solver_bitwuzla.set_option_impl(org.smtlib.IExpr.IKeyword, org.smtlib.IAttributeValue), falling back to the standard SMT-LIB default for any option never set, and "unsupported" for anything not a recognized standard option at all (matching what a compliant solver would say about an option it doesn't have).
get_option(IExpr.IKeyword) - Method in class org.smtlib.solvers.Solver_cvc5: See the class Javadoc: wraps a bare-symbol answer for a string-typed option (Utils.stringOptions -- currently just :regular-output-channel and :diagnostic-output-channel) into a proper SMT-LIB string literal with the same text, working around cvc5 answering those two with an unquoted symbol instead.
get_option(IExpr.IKeyword) - Method in class org.smtlib.solvers.Solver_simplify: Simplify has no get-option; answered from the values kept by set_option
get_option(IExpr.IKeyword) - Method in class org.smtlib.solvers.Solver_test
get_option(IExpr.IKeyword) - Method in class org.smtlib.solvers.Solver_z3_4_3: Sent to the solver, except where z3 4.3's answer does not conform: it defaults :produce-models to true (SMT-LIB: false), writes the channel names unquoted, knows :produce-assertions only as :interactive-mode (see set_option_impl), and answers unsupported, not the default value, for a standard option it lacks
get_option_response(IAttributeValue) - Method in class org.smtlib.impl.Response.Factory
get_option_response(IAttributeValue) - Method in interface org.smtlib.IResponse.IFactory
get_proof() - Method in class org.smtlib.AbstractSolver
get_proof() - Method in interface org.smtlib.ICommand.IFactory: Creates a get-proof command object.
get_proof() - Method in class org.smtlib.impl.Factory
get_proof() - Method in interface org.smtlib.ISolver: Returns a proof of unsatisfiability for the current assertion set.
get_proof() - Method in class org.smtlib.solvers.Solver_altergo: Alt-Ergo writes nothing for get-proof (it ignores it); answered unsupported without sending it
get_proof() - Method in class org.smtlib.solvers.Solver_bitwuzla: Bitwuzla rejects get-proof as an unsupported command and exits (class comment point 1); a conforming solver without proofs answers unsupported.
get_proof() - Method in class org.smtlib.solvers.Solver_cvc5: cvc5 answers get-proof in assert mode after a check
get_proof() - Method in class org.smtlib.solvers.Solver_simplify: See Solver_test.get_proof().
get_proof() - Method in class org.smtlib.solvers.Solver_smtinterpol: SMTInterpol answers get-proof after sat, and in assert mode after a check
get_proof() - Method in class org.smtlib.solvers.Solver_test
get_proof() - Method in class org.smtlib.solvers.Solver_z3_4_3: z3 4.3 itself reports get-proof without :produce-proofs or when no proof is available; the checks here only give the same messages as the other adapters
get_proof() - Method in class org.smtlib.solvers.Solver_z3_recent: z3 answers get-proof in assert mode after a check
get_proof_response(ISexpr) - Method in class org.smtlib.impl.Response.Factory
get_proof_response(ISexpr) - Method in interface org.smtlib.IResponse.IFactory
get_unsat_assumptions() - Method in class org.smtlib.AbstractSolver
get_unsat_assumptions() - Method in interface org.smtlib.ICommand.IFactory: Creates a get-unsat-assumptions command object.
get_unsat_assumptions() - Method in class org.smtlib.impl.Factory
get_unsat_assumptions() - Method in interface org.smtlib.ISolver: Returns the subset of check-sat-assuming assumptions that caused the result to be unsat.
get_unsat_assumptions() - Method in class org.smtlib.solvers.Solver_altergo: Alt-Ergo ignores get-unsat-assumptions, writing nothing; answered unsupported without sending it
get_unsat_assumptions() - Method in class org.smtlib.solvers.Solver_bitwuzla: Bitwuzla writes nothing for get-unsat-assumptions unless its last check returned unsat; then it writes a fragment and an error if the option is off or was set after the check, or an assert, push, pop, reset-assertions or reset came since.
get_unsat_assumptions() - Method in class org.smtlib.solvers.Solver_cvc5: cvc5 aborts on get-unsat-assumptions in assert mode after a check
get_unsat_assumptions() - Method in class org.smtlib.solvers.Solver_simplify: See Solver_test.get_unsat_assumptions().
get_unsat_assumptions() - Method in class org.smtlib.solvers.Solver_smtinterpol: SMTInterpol answers get-unsat-assumptions in assert mode after a check
get_unsat_assumptions() - Method in class org.smtlib.solvers.Solver_test
get_unsat_assumptions() - Method in class org.smtlib.solvers.Solver_yices2: yices2 answers get-unsat-assumptions, wrongly, in assert mode after a check
get_unsat_assumptions() - Method in class org.smtlib.solvers.Solver_z3_recent: z3 answers get-unsat-assumptions in assert mode after a check
get_unsat_assumptions_response(List<IExpr>) - Method in class org.smtlib.impl.Response.Factory
get_unsat_assumptions_response(List<IExpr>) - Method in interface org.smtlib.IResponse.IFactory
get_unsat_core() - Method in class org.smtlib.AbstractSolver
get_unsat_core() - Method in interface org.smtlib.ICommand.IFactory: Creates a get-unsat-core command object.
get_unsat_core() - Method in class org.smtlib.impl.Factory
get_unsat_core() - Method in interface org.smtlib.ISolver: Returns the named formulae that form an unsatisfiable core of the current assertion set.
get_unsat_core() - Method in class org.smtlib.solvers.Solver_altergo: Alt-Ergo ignores get-unsat-core, writing nothing (with --sat-solver Tableaux it writes a non-SMT-LIB core after check-sat instead); answered unsupported without sending it
get_unsat_core() - Method in class org.smtlib.solvers.Solver_bitwuzla: With :produce-unsat-cores on, Bitwuzla writes nothing for get-unsat-core unless its last check returned unsat, and a fragment and an error if an assert, push, pop, reset-assertions or reset came since or the option was set after the check.
get_unsat_core() - Method in class org.smtlib.solvers.Solver_cvc5: cvc5 answers get-unsat-core in assert mode after a check
get_unsat_core() - Method in class org.smtlib.solvers.Solver_simplify: See Solver_test.get_unsat_core().
get_unsat_core() - Method in class org.smtlib.solvers.Solver_smtinterpol: SMTInterpol answers get-unsat-core in assert mode after a check
get_unsat_core() - Method in class org.smtlib.solvers.Solver_test
get_unsat_core() - Method in class org.smtlib.solvers.Solver_yices2: yices2 answers get-unsat-core in assert mode after a check
get_unsat_core() - Method in class org.smtlib.solvers.Solver_z3_4_3: z3 4.3 itself reports get-unsat-core without :produce-unsat-cores or when no core is available; the checks here only give the same messages as the other adapters
get_unsat_core() - Method in class org.smtlib.solvers.Solver_z3_recent: z3 answers get-unsat-core in assert mode after a check
get_unsat_core_response(List<IExpr.ISymbol>) - Method in class org.smtlib.impl.Response.Factory
get_unsat_core_response(List<IExpr.ISymbol>) - Method in interface org.smtlib.IResponse.IFactory
get_value(List<IExpr>) - Method in interface org.smtlib.ICommand.IFactory: Creates a get-value command object.
get_value(List<IExpr>) - Method in class org.smtlib.impl.Factory
get_value(IExpr...) - Method in class org.smtlib.AbstractSolver
get_value(IExpr...) - Method in interface org.smtlib.ISolver: Returns the values of the given expressions in the current satisfying model.
get_value(IExpr...) - Method in class org.smtlib.solvers.Solver_altergo: Alt-Ergo ignores get-value, writing nothing; answered unsupported without sending it
get_value(IExpr...) - Method in class org.smtlib.solvers.Solver_bitwuzla: With :produce-models on, Bitwuzla writes nothing for get-value unless its last check returned sat, and a fragment and an error if an assert, push, pop or reset-assertions came since or the option was set after the check.
get_value(IExpr...) - Method in class org.smtlib.solvers.Solver_cvc5: cvc5 answers get-value in assert mode after a check
get_value(IExpr...) - Method in class org.smtlib.solvers.Solver_simplify: See Solver_test.get_value(IExpr...).
get_value(IExpr...) - Method in class org.smtlib.solvers.Solver_smtinterpol: SMTInterpol answers get-value with :produce-models off, and in assert mode after a check
get_value(IExpr...) - Method in class org.smtlib.solvers.Solver_test
get_value(IExpr...) - Method in class org.smtlib.solvers.Solver_yices2: yices2 answers get-value with :produce-models off, and in assert mode after a check
get_value(IExpr...) - Method in class org.smtlib.solvers.Solver_z3_4_3: See get_model: z3 4.3 defaults :produce-models to true
get_value(IExpr...) - Method in class org.smtlib.solvers.Solver_z3_recent: z3 answers get-value in assert mode after a check
get_value_response(List<IResponse.IPair<IExpr, IExpr>>) - Method in class org.smtlib.impl.Response.Factory
get_value_response(List<IResponse.IPair<IExpr, IExpr>>) - Method in interface org.smtlib.IResponse.IFactory
getCharset() - Method in class org.smtlib.SolverProcess: The charset being used to encode text sent to the process and decode text read back from it
getDiag() - Method in class org.smtlib.Log: Returns the current diagnostic stream.
getOut() - Method in class org.smtlib.Log: Returns the current regular-output stream.
getToken() - Method in class org.smtlib.sexpr.Lexer: Returns the next lexical token, advancing the scanner.
getToken(Class<?>) - Method in class org.smtlib.sexpr.Lexer: Returns the next lexical token; if the token returned matches the given class (or is a subclass), then the scanner is advanced; if the token does not match, the scanner is not advanced.
getToken(String) - Method in class org.smtlib.sexpr.Lexer: Returns the first token found in the given text
getToken(Matcher) - Method in class org.smtlib.sexpr.Lexer: Returns the next token found in the given matcher, advancing the matcher
getToken(Matcher) - Method in class org.smtlib.sexpr.Parser: Reports a vertical tab or form feed between tokens (except with --relax), which is then read as white space, and a keyword that is not a colon followed by a simple symbol (#185)
GLOBAL_DECLARATIONS - Static variable in class org.smtlib.Utils: The string designating an option item
GT - 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