Enums¶

enum stp_error_code¶

Values:

enumerator STP_ERR_INVALID_ARGUMENT¶

enumerator STP_ERR_SORT_MISMATCH¶

enumerator STP_ERR_ARITY¶

enumerator STP_ERR_INDEX_OUT_OF_RANGE¶

enumerator STP_ERR_VALUE_OUT_OF_RANGE¶

enumerator STP_ERR_DOES_NOT_FIT¶

enumerator STP_ERR_NOT_A_VALUE¶

enumerator STP_ERR_NO_MODEL¶

enumerator STP_ERR_FOREIGN_MANAGER¶

enumerator STP_ERR_NULL_HANDLE¶

enumerator STP_ERR_UNSUPPORTED¶

enumerator STP_ERR_OPTION_UNKNOWN¶

enumerator STP_ERR_OPTION_VALUE¶

enumerator STP_ERR_OPTION_TIMING¶

enumerator STP_ERR_OPTION_CONFLICT¶

enumerator STP_ERR_OPTION_UNAVAILABLE¶

enumerator STP_ERR_PARSE¶

enumerator STP_ERR_IO¶

enumerator STP_ERR_STATE¶

enumerator STP_ERR_RESOURCE¶

enumerator STP_ERR_INTERNAL¶

enumerator STP_ERR_MAX_ENUM¶

enumerator STP_ERR_MIN_ENUM¶

enum stp_kind¶

Values:

enumerator STP_KIND_VALUE¶

enumerator STP_KIND_CONSTANT¶

enumerator STP_KIND_ITE¶

enumerator STP_KIND_EQUAL¶

enumerator STP_KIND_DISTINCT¶

enumerator STP_KIND_APPLY¶

enumerator STP_KIND_NOT¶

enumerator STP_KIND_AND¶

enumerator STP_KIND_OR¶

enumerator STP_KIND_XOR¶

enumerator STP_KIND_IMPLIES¶

enumerator STP_KIND_BV_NOT¶

enumerator STP_KIND_BV_AND¶

enumerator STP_KIND_BV_OR¶

enumerator STP_KIND_BV_XOR¶

enumerator STP_KIND_BV_NAND¶

enumerator STP_KIND_BV_NOR¶

enumerator STP_KIND_BV_XNOR¶

enumerator STP_KIND_BV_NEG¶

enumerator STP_KIND_BV_ADD¶

enumerator STP_KIND_BV_SUB¶

enumerator STP_KIND_BV_MUL¶

enumerator STP_KIND_BV_UDIV¶

enumerator STP_KIND_BV_UREM¶

enumerator STP_KIND_BV_SDIV¶

enumerator STP_KIND_BV_SREM¶

enumerator STP_KIND_BV_SMOD¶

enumerator STP_KIND_BV_SHL¶

enumerator STP_KIND_BV_LSHR¶

enumerator STP_KIND_BV_ASHR¶

enumerator STP_KIND_BV_CONCAT¶

enumerator STP_KIND_BV_EXTRACT¶

enumerator STP_KIND_BV_ZERO_EXTEND¶

enumerator STP_KIND_BV_SIGN_EXTEND¶

enumerator STP_KIND_BV_REPEAT¶

enumerator STP_KIND_BV_ROTATE_LEFT¶

enumerator STP_KIND_BV_ROTATE_RIGHT¶

enumerator STP_KIND_BV_COMP¶

enumerator STP_KIND_BV_ULT¶

enumerator STP_KIND_BV_ULE¶

enumerator STP_KIND_BV_UGT¶

enumerator STP_KIND_BV_UGE¶

enumerator STP_KIND_BV_SLT¶

enumerator STP_KIND_BV_SLE¶

enumerator STP_KIND_BV_SGT¶

enumerator STP_KIND_BV_SGE¶

enumerator STP_KIND_BV_UADDO¶

enumerator STP_KIND_BV_SADDO¶

enumerator STP_KIND_BV_UMULO¶

enumerator STP_KIND_BV_SMULO¶

enumerator STP_KIND_BV_USUBO¶

enumerator STP_KIND_BV_SSUBO¶

enumerator STP_KIND_BV_NEGO¶

enumerator STP_KIND_BV_SDIVO¶

enumerator STP_KIND_BV_REDAND¶

enumerator STP_KIND_BV_REDOR¶

enumerator STP_KIND_SELECT¶

enumerator STP_KIND_STORE¶

enumerator STP_KIND_CONST_ARRAY¶

enumerator STP_KIND_FP_ABS¶

enumerator STP_KIND_FP_NEG¶

enumerator STP_KIND_FP_ADD¶

enumerator STP_KIND_FP_SUB¶

enumerator STP_KIND_FP_MUL¶

enumerator STP_KIND_FP_DIV¶

enumerator STP_KIND_FP_FMA¶

enumerator STP_KIND_FP_SQRT¶

enumerator STP_KIND_FP_REM¶

enumerator STP_KIND_FP_RTI¶

enumerator STP_KIND_FP_MIN¶

enumerator STP_KIND_FP_MAX¶

enumerator STP_KIND_FP_EQ¶

enumerator STP_KIND_FP_LT¶

enumerator STP_KIND_FP_LEQ¶

enumerator STP_KIND_FP_GT¶

enumerator STP_KIND_FP_GEQ¶

enumerator STP_KIND_FP_IS_NORMAL¶

enumerator STP_KIND_FP_IS_SUBNORMAL¶

enumerator STP_KIND_FP_IS_ZERO¶

enumerator STP_KIND_FP_IS_INF¶

enumerator STP_KIND_FP_IS_NAN¶

enumerator STP_KIND_FP_IS_NEG¶

enumerator STP_KIND_FP_IS_POS¶

enumerator STP_KIND_FP_FP¶

enumerator STP_KIND_FP_TO_FP_FROM_BV¶

enumerator STP_KIND_FP_TO_FP_FROM_FP¶

enumerator STP_KIND_FP_TO_FP_FROM_SBV¶

enumerator STP_KIND_FP_TO_FP_FROM_UBV¶

enumerator STP_KIND_FP_TO_FP_FROM_REAL¶

enumerator STP_KIND_FP_TO_UBV¶

enumerator STP_KIND_FP_TO_SBV¶

enumerator STP_KIND_FP_TO_REAL¶

enumerator STP_KIND_FP_TO_IEEE_BV¶

enumerator STP_KIND_REAL_ADD¶

enumerator STP_KIND_REAL_SUB¶

enumerator STP_KIND_REAL_NEG¶

enumerator STP_KIND_REAL_MUL¶

enumerator STP_KIND_REAL_DIV¶

enumerator STP_KIND_REAL_LT¶

enumerator STP_KIND_REAL_LE¶

enumerator STP_KIND_REAL_GT¶

enumerator STP_KIND_REAL_GE¶

enumerator STP_NUM_KINDS¶

enumerator STP_KIND_MAX_ENUM¶

enumerator STP_KIND_MIN_ENUM¶

enum stp_option¶

Values:

enumerator STP_OPT_PRODUCE_MODELS¶

enumerator STP_OPT_SAT_BACKEND¶

enumerator STP_OPT_RANDOM_SEED¶

enumerator STP_OPT_MODEL_ARRAY_FILL¶

enumerator STP_OPT_LOGIC¶

enumerator STP_OPT_SIMPLIFY¶

enumerator STP_OPT_DEFAULT_ROUNDING_MODE¶

enumerator STP_OPT_DISABLE_SIMPLIFICATIONS¶

enumerator STP_OPT_THREADS¶

enumerator STP_OPT_ARRAY_EQUALITY¶

enumerator STP_OPT_BV_EQ_ABSTRACTION¶

enumerator STP_OPT_BV_TERM_ABSTRACTION¶

enumerator STP_OPT_UNINTERPRETED_FUNCTIONS¶

enumerator STP_OPT_UF_ACKERMANN¶

enumerator STP_OPT_UF_SORT_WIDTH¶

enumerator STP_OPT_FP_ABSTRACTION¶

enumerator STP_OPT_CNF_GENERATION_EFFORT¶

enumerator STP_OPT_INCREMENTAL¶

enumerator STP_OPT_INCREMENTAL_AUTO_ENGAGE_AT¶

enumerator STP_OPT_MAX_NUM_CONFL¶

enumerator STP_OPT_MAX_TIME¶

enumerator STP_OPT_CHECK_SANITY¶

enumerator STP_NUM_STABLE_OPTIONS¶

enumerator STP_OPT_MAX_ENUM¶

enumerator STP_OPT_MIN_ENUM¶

enum stp_status¶

Every enum of this header, and of the generated ones it includes, ends with *_MAX_ENUM and *_MIN_ENUM members that are not values: together they widen the type to all of int, so that any int a C caller passes, negative ones included, is a value of the enum for the C++ implementation, which refuses the ones it does not know instead of meeting undefined behaviour.

Values:

enumerator STP_OK¶

enumerator STP_ERROR¶

enumerator STP_STATUS_MAX_ENUM¶

enumerator STP_STATUS_MIN_ENUM¶

enum stp_sort_kind¶

Values:

enumerator STP_SORT_BOOL¶

enumerator STP_SORT_BV¶

enumerator STP_SORT_FP¶

enumerator STP_SORT_RM¶

enumerator STP_SORT_REAL¶

enumerator STP_SORT_ARRAY¶

enumerator STP_SORT_FUN¶

enumerator STP_SORT_UNINTERPRETED¶

enumerator STP_SORT_MAX_ENUM¶

enumerator STP_SORT_MIN_ENUM¶

enum stp_rm¶

Values:

enumerator STP_RM_RNE¶

enumerator STP_RM_RNA¶

enumerator STP_RM_RTP¶

enumerator STP_RM_RTN¶

enumerator STP_RM_RTZ¶

enumerator STP_RM_MAX_ENUM¶

enumerator STP_RM_MIN_ENUM¶

enum stp_result_kind¶

Values:

enumerator STP_SAT¶

enumerator STP_UNSAT¶

enumerator STP_UNKNOWN¶

enumerator STP_RESULT_MAX_ENUM¶

enumerator STP_RESULT_MIN_ENUM¶

enum stp_validity¶

Values:

enumerator STP_VALID¶

enumerator STP_INVALID¶

enumerator STP_UNKNOWN_VALIDITY¶

enumerator STP_VALIDITY_MAX_ENUM¶

enumerator STP_VALIDITY_MIN_ENUM¶

enum stp_unknown_reason¶

Values:

enumerator STP_REASON_NONE¶

enumerator STP_REASON_TIMEOUT¶

enumerator STP_REASON_CONFLICT_LIMIT¶

enumerator STP_REASON_INTERRUPTED¶

enumerator STP_REASON_INCOMPLETE¶

enumerator STP_REASON_RESOURCE_LIMIT¶

enumerator STP_REASON_CARRIER_EXHAUSTED¶

enumerator STP_REASON_ASSUMED_INJECTIVITY¶

enumerator STP_REASON_STOPPED_AFTER_CNF¶

enumerator STP_REASON_OTHER¶

enumerator STP_REASON_MAX_ENUM¶

enumerator STP_REASON_MIN_ENUM¶

enum stp_format¶

Values:

enumerator STP_FORMAT_AUTO¶

enumerator STP_FORMAT_SMTLIB2¶

enumerator STP_FORMAT_DOT¶

enumerator STP_FORMAT_GDL¶

enumerator STP_FORMAT_MAX_ENUM¶

enumerator STP_FORMAT_MIN_ENUM¶

enum stp_parse_mode¶

Values:

enumerator STP_PARSE_DECLARE_AND_ASSERT¶

enumerator STP_PARSE_EXECUTE¶

enumerator STP_PARSE_ONLY¶

enumerator STP_PARSE_SINGLE_QUERY¶: a script as data: one query, nothing that changes the solver (ParseMode::SINGLE_QUERY)

enumerator STP_PARSE_MAX_ENUM¶

enumerator STP_PARSE_MIN_ENUM¶

enum stp_cnf_scope¶

Values:

enumerator STP_CNF_WHOLE¶

enumerator STP_CNF_PARTIAL¶

enumerator STP_CNF_OVER_APPROXIMATION¶

enumerator STP_CNF_SCOPE_MAX_ENUM¶

enumerator STP_CNF_SCOPE_MIN_ENUM¶

enum stp_tier¶

Values:

enumerator STP_TIER_STABLE¶

enumerator STP_TIER_EXPERT¶

enumerator STP_TIER_EXPERIMENTAL¶

enumerator STP_TIER_DIAGNOSTIC¶

enumerator STP_TIER_MAX_ENUM¶

enumerator STP_TIER_MIN_ENUM¶

enum stp_settable¶

Values:

enumerator STP_SETTABLE_ANYTIME¶

enumerator STP_SETTABLE_BEFORE_FIRST_CHECK¶

enumerator STP_SETTABLE_CONSTRUCTION¶

enumerator STP_SETTABLE_MAX_ENUM¶

enumerator STP_SETTABLE_MIN_ENUM¶

enum stp_option_scope¶

Values:

enumerator STP_SCOPE_SOLVER¶

enumerator STP_SCOPE_MANAGER¶

enumerator STP_SCOPE_MAX_ENUM¶

enumerator STP_SCOPE_MIN_ENUM¶

enum stp_fp_class¶

Values:

enumerator STP_FP_NORMAL¶

enumerator STP_FP_SUBNORMAL¶

enumerator STP_FP_ZERO¶

enumerator STP_FP_INFINITY¶

enumerator STP_FP_NAN¶

enumerator STP_FP_MAX_ENUM¶

enumerator STP_FP_MIN_ENUM¶

enum stp_internal_error_policy¶

Values:

enumerator STP_POISON¶

enumerator STP_ABORT¶

enumerator STP_POLICY_MAX_ENUM¶

enumerator STP_POLICY_MIN_ENUM¶