Enumerations

enum class stp::api::CnfScope : std::uint8_t

How a CNF a check hands to the SAT solver relates to the query (Solver::set_cnf_sink, Solver::write_cnf): the whole query; partial, a refinement still to come (array reads, uninterpreted functions, Real arithmetic, the floating-point abstraction) adding what the search asks for; or an over-approximation, the bit-vector abstractions having replaced operations with free inputs.

Values:

enumerator WHOLE

enumerator PARTIAL

enumerator OVER_APPROXIMATION

enum class stp::api::ErrorCode : std::uint16_t

Error codes (errors.toml). RESOURCE and INTERNAL are the two unsafe codes.

Values:

enumerator INVALID_ARGUMENT

enumerator SORT_MISMATCH

enumerator ARITY

enumerator INDEX_OUT_OF_RANGE

enumerator VALUE_OUT_OF_RANGE

enumerator DOES_NOT_FIT

enumerator NOT_A_VALUE

enumerator NO_MODEL

enumerator FOREIGN_MANAGER

enumerator NULL_HANDLE

enumerator UNSUPPORTED

enumerator OPTION_UNKNOWN

enumerator OPTION_VALUE

enumerator OPTION_TIMING

enumerator OPTION_CONFLICT

enumerator OPTION_UNAVAILABLE

enumerator PARSE

enumerator IO

enumerator STATE

enumerator RESOURCE

enumerator INTERNAL

enum class stp::api::Format : std::uint8_t

Values:

enumerator AUTO

enumerator SMTLIB2

enumerator DOT

enumerator GDL

enum class stp::api::InternalErrorPolicy : std::uint8_t

Values:

enumerator POISON

enumerator ABORT

enum class stp::api::Kind : std::uint16_t

Term kinds: one entry per public operator (kinds.toml), each value pinned by its id.

Values:

enumerator VALUE

() -> T

enumerator CONSTANT

() -> T

enumerator ITE

(Bool, T, T) -> T

enumerator EQUAL

(T, T) -> Bool

enumerator DISTINCT

(T, T, …) -> Bool

enumerator APPLY

(Fun[D..,C], D..) -> C

enumerator NOT

(Bool) -> Bool

enumerator AND

(Bool, …) -> Bool

enumerator OR

(Bool, …) -> Bool

enumerator XOR

(Bool, …) -> Bool

enumerator IMPLIES

(Bool, Bool) -> Bool

enumerator BV_NOT

(BV[n]) -> BV[n]

enumerator BV_AND

(BV[n], BV[n], …) -> BV[n]

enumerator BV_OR

(BV[n], BV[n], …) -> BV[n]

enumerator BV_XOR

(BV[n], BV[n], …) -> BV[n]

enumerator BV_NAND

(BV[n], BV[n]) -> BV[n]

enumerator BV_NOR

(BV[n], BV[n]) -> BV[n]

enumerator BV_XNOR

(BV[n], BV[n]) -> BV[n]

enumerator BV_NEG

(BV[n]) -> BV[n]

enumerator BV_ADD

(BV[n], BV[n], …) -> BV[n]

enumerator BV_SUB

(BV[n], BV[n]) -> BV[n]

enumerator BV_MUL

(BV[n], BV[n], …) -> BV[n]

enumerator BV_UDIV

(BV[n], BV[n]) -> BV[n]

enumerator BV_UREM

(BV[n], BV[n]) -> BV[n]

enumerator BV_SDIV

(BV[n], BV[n]) -> BV[n]

enumerator BV_SREM

(BV[n], BV[n]) -> BV[n]

enumerator BV_SMOD

(BV[n], BV[n]) -> BV[n]

enumerator BV_SHL

(BV[n], BV[n]) -> BV[n]

enumerator BV_LSHR

(BV[n], BV[n]) -> BV[n]

enumerator BV_ASHR

(BV[n], BV[n]) -> BV[n]

enumerator BV_CONCAT

(BV[a], BV[b], …) -> BV[a+b+…]

enumerator BV_EXTRACT

(BV[n]) -> BV[hi-lo+1] with n > hi >= lo

enumerator BV_ZERO_EXTEND

(BV[n]) -> BV[n+k]

enumerator BV_SIGN_EXTEND

(BV[n]) -> BV[n+k]

enumerator BV_REPEAT

(BV[n]) -> BV[n*k] with k >= 1

enumerator BV_ROTATE_LEFT

(BV[n]) -> BV[n]

enumerator BV_ROTATE_RIGHT

(BV[n]) -> BV[n]

enumerator BV_COMP

(BV[n], BV[n]) -> BV[1]

enumerator BV_ULT

(BV[n], BV[n]) -> Bool

enumerator BV_ULE

(BV[n], BV[n]) -> Bool

enumerator BV_UGT

(BV[n], BV[n]) -> Bool

enumerator BV_UGE

(BV[n], BV[n]) -> Bool

enumerator BV_SLT

(BV[n], BV[n]) -> Bool

enumerator BV_SLE

(BV[n], BV[n]) -> Bool

enumerator BV_SGT

(BV[n], BV[n]) -> Bool

enumerator BV_SGE

(BV[n], BV[n]) -> Bool

enumerator BV_UADDO

(BV[n], BV[n]) -> Bool

enumerator BV_SADDO

(BV[n], BV[n]) -> Bool

enumerator BV_UMULO

(BV[n], BV[n]) -> Bool

enumerator BV_SMULO

(BV[n], BV[n]) -> Bool

enumerator BV_USUBO

(BV[n], BV[n]) -> Bool

enumerator BV_SSUBO

(BV[n], BV[n]) -> Bool

enumerator BV_NEGO

(BV[n]) -> Bool

enumerator BV_SDIVO

(BV[n], BV[n]) -> Bool

enumerator BV_REDAND

(BV[n]) -> BV[1]

enumerator BV_REDOR

(BV[n]) -> BV[1]

enumerator SELECT

(Array[I,E], I) -> E

enumerator STORE

(Array[I,E], I, E) -> Array[I,E]

enumerator CONST_ARRAY

(E) -> Array[I,E] (the array sort is an argument of mk_const_array)

enumerator FP_ABS

(FP[e,s]) -> FP[e,s]

enumerator FP_NEG

(FP[e,s]) -> FP[e,s]

enumerator FP_ADD

(RM, FP[e,s], FP[e,s]) -> FP[e,s]

enumerator FP_SUB

(RM, FP[e,s], FP[e,s]) -> FP[e,s]

enumerator FP_MUL

(RM, FP[e,s], FP[e,s]) -> FP[e,s]

enumerator FP_DIV

(RM, FP[e,s], FP[e,s]) -> FP[e,s]

enumerator FP_FMA

(RM, FP[e,s], FP[e,s], FP[e,s]) -> FP[e,s]

enumerator FP_SQRT

(RM, FP[e,s]) -> FP[e,s]

enumerator FP_REM

(FP[e,s], FP[e,s]) -> FP[e,s]

enumerator FP_RTI

(RM, FP[e,s]) -> FP[e,s]

enumerator FP_MIN

(FP[e,s], FP[e,s]) -> FP[e,s]

enumerator FP_MAX

(FP[e,s], FP[e,s]) -> FP[e,s]

enumerator FP_EQ

(FP[e,s], FP[e,s]) -> Bool

enumerator FP_LT

(FP[e,s], FP[e,s]) -> Bool

enumerator FP_LEQ

(FP[e,s], FP[e,s]) -> Bool

enumerator FP_GT

(FP[e,s], FP[e,s]) -> Bool

enumerator FP_GEQ

(FP[e,s], FP[e,s]) -> Bool

enumerator FP_IS_NORMAL

(FP[e,s]) -> Bool

enumerator FP_IS_SUBNORMAL

(FP[e,s]) -> Bool

enumerator FP_IS_ZERO

(FP[e,s]) -> Bool

enumerator FP_IS_INF

(FP[e,s]) -> Bool

enumerator FP_IS_NAN

(FP[e,s]) -> Bool

enumerator FP_IS_NEG

(FP[e,s]) -> Bool

enumerator FP_IS_POS

(FP[e,s]) -> Bool

enumerator FP_FP

(BV[1], BV[e], BV[s-1]) -> FP[e,s]

enumerator FP_TO_FP_FROM_BV

(BV[e+s]) -> FP[e,s]

enumerator FP_TO_FP_FROM_FP

(RM, FP[e2,s2]) -> FP[e,s]

enumerator FP_TO_FP_FROM_SBV

(RM, BV[n]) -> FP[e,s]

enumerator FP_TO_FP_FROM_UBV

(RM, BV[n]) -> FP[e,s]

enumerator FP_TO_FP_FROM_REAL

(RM, Real) -> FP[e,s]

enumerator FP_TO_UBV

(RM, FP[e,s]) -> BV[m]

enumerator FP_TO_SBV

(RM, FP[e,s]) -> BV[m]

enumerator FP_TO_REAL

(FP[e,s]) -> Real

enumerator FP_TO_IEEE_BV

(FP[e,s]) -> BV[e+s]

enumerator REAL_ADD

(Real, Real, …) -> Real

enumerator REAL_SUB

(Real, Real) -> Real

enumerator REAL_NEG

(Real) -> Real

enumerator REAL_MUL

(Real, Real) -> Real

enumerator REAL_DIV

(Real, Real) -> Real

enumerator REAL_LT

(Real, Real) -> Bool

enumerator REAL_LE

(Real, Real) -> Bool

enumerator REAL_GT

(Real, Real) -> Bool

enumerator REAL_GE

(Real, Real) -> Bool

enumerator NUM_KINDS

enum class stp::api::Option : std::uint16_t

The stable option tier as a typed enum (options.toml), each value pinned by its id.

Values:

enumerator PRODUCE_MODELS

produce-models

enumerator SAT_BACKEND

sat-backend

enumerator RANDOM_SEED

random-seed

enumerator MODEL_ARRAY_FILL

model-array-fill

enumerator LOGIC

logic

enumerator SIMPLIFY

simplify

enumerator DEFAULT_ROUNDING_MODE

default-rounding-mode

enumerator DISABLE_SIMPLIFICATIONS

disable-simplifications

enumerator THREADS

threads

enumerator ARRAY_EQUALITY

array-equality

enumerator BV_EQ_ABSTRACTION

bv-eq-abstraction

enumerator BV_TERM_ABSTRACTION

bv-term-abstraction

enumerator UNINTERPRETED_FUNCTIONS

uninterpreted-functions

enumerator UF_ACKERMANN

uf-ackermann

enumerator UF_SORT_WIDTH

uf-sort-width

enumerator FP_ABSTRACTION

fp-abstraction

enumerator CNF_GENERATION_EFFORT

cnf-generation-effort

enumerator INCREMENTAL

incremental

enumerator INCREMENTAL_AUTO_ENGAGE_AT

incremental-auto-engage-at

enumerator MAX_NUM_CONFL

max-num-confl

enumerator MAX_TIME

max-time

enumerator CHECK_SANITY

check-sanity

enumerator NUM_STABLE_OPTIONS

enum class stp::api::OptionScope : std::uint8_t

Values:

enumerator SOLVER

enumerator MANAGER

enum class stp::api::ParseMode : std::uint8_t

How a parse treats its input. DECLARE_AND_ASSERT: the input’s declarations, assertions and scopes take effect, silently; check-sat is not executed. EXECUTE: the input runs as the stp command line runs it, answering to the output sink: every command, under the script’s own set-logic. Its checks are the input’s, not the solver’s: they leave no result or model behind. As on the command line, an equality between whole arrays needs array-equality = on there (UNSUPPORTED otherwise). PARSE_ONLY: EXECUTE without the deciding (the command line’s —parse-only): check-sat is skipped. SINGLE_QUERY: a script as data. As DECLARE_AND_ASSERT, the script’s declarations, definitions and assertions are applied and its check-sat is not run, but nothing in it may change the solver’s configuration or state, and it must be one query: set-logic at most once, before any declaration or assertion; set-info (ignored); set-option for :print-success and :produce-models only (ignored); declare-const, declare-fun, declare-sort, define-fun, define-sort, define-const and assert; exactly one check-sat, after which only exit, any number of times. Any other command — push, pop, reset, reset-assertions, check-sat-assuming, a get-* request, echo, a second check-sat, a declaration after the check-sat, any other set-option — and a script with no check-sat are a PARSE error that names the command and its line. As after any parse that fails part way, in any mode, the solver is then as it was before the parse: its assertion stack, the symbols the script declared (not kept) and declared_logic().

Values:

enumerator DECLARE_AND_ASSERT

enumerator EXECUTE

enumerator PARSE_ONLY

enumerator SINGLE_QUERY

enum class stp::api::RoundingMode : std::uint8_t

Contiguous; the engine’s one-hot carrier is internal.

Values:

enumerator RNE

enumerator RNA

enumerator RTP

enumerator RTN

enumerator RTZ

enum class stp::api::Settable : std::uint8_t

Values:

enumerator ANYTIME

enumerator BEFORE_FIRST_CHECK

enumerator CONSTRUCTION

enum class stp::api::SortKind : std::uint8_t

Values:

enumerator BOOL

enumerator BV

enumerator FP

enumerator RM

enumerator REAL

enumerator ARRAY

enumerator FUN

enumerator UNINTERPRETED

enum class stp::api::Tier : std::uint8_t

Values:

enumerator STABLE

enumerator EXPERT

enumerator EXPERIMENTAL

enumerator DIAGNOSTIC

enum class stp::api::UnknownReason : std::uint8_t

Values:

enumerator NONE

the result is not unknown

enumerator TIMEOUT

a time budget expired

enumerator CONFLICT_LIMIT

a conflict budget expired

enumerator INTERRUPTED

interrupt() or a Terminator fired

enumerator INCOMPLETE

the decision procedure is incomplete for this input

enumerator RESOURCE_LIMIT

an internal resource budget (AIG nodes, …)

enumerator CARRIER_EXHAUSTED

an uninterpreted sort ran out of carrier width

enumerator ASSUMED_INJECTIVITY

the answer depended on an injectivity assumption

enumerator STOPPED_AFTER_CNF

option stop-after-cnf was set

enumerator OTHER

enum class stp::api::Validity : std::uint8_t

Values:

enumerator VALID

enumerator INVALID

enumerator UNKNOWN

enum class stp::api::Verdict : std::uint8_t

Values:

enumerator SAT

enumerator UNSAT

enumerator UNKNOWN