Named constructors

stp_term stp_ite(stp_tm tm, stp_term a, stp_term b, stp_term c)

stp_term stp_eq(stp_tm tm, stp_term a, stp_term b)

stp_term stp_distinct(stp_tm tm, size_t n, const stp_term *args)

stp_term stp_distinct2(stp_tm tm, stp_term a, stp_term b)

stp_term stp_apply(stp_tm tm, stp_term a, stp_term b)

stp_term stp_apply_n(stp_tm tm, size_t n, const stp_term *args)

stp_term stp_not(stp_tm tm, stp_term a)

stp_term stp_and(stp_tm tm, size_t n, const stp_term *args)

stp_term stp_and2(stp_tm tm, stp_term a, stp_term b)

stp_term stp_or(stp_tm tm, size_t n, const stp_term *args)

stp_term stp_or2(stp_tm tm, stp_term a, stp_term b)

stp_term stp_xor(stp_tm tm, size_t n, const stp_term *args)

stp_term stp_xor2(stp_tm tm, stp_term a, stp_term b)

stp_term stp_implies(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvnot(stp_tm tm, stp_term a)

stp_term stp_bvand(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvand_n(stp_tm tm, size_t n, const stp_term *args)

stp_term stp_bvor(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvor_n(stp_tm tm, size_t n, const stp_term *args)

stp_term stp_bvxor(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvxor_n(stp_tm tm, size_t n, const stp_term *args)

stp_term stp_bvnand(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvnor(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvxnor(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvneg(stp_tm tm, stp_term a)

stp_term stp_bvadd(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvadd_n(stp_tm tm, size_t n, const stp_term *args)

stp_term stp_bvsub(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvmul(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvmul_n(stp_tm tm, size_t n, const stp_term *args)

stp_term stp_bvudiv(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvurem(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvsdiv(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvsrem(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvsmod(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvshl(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvlshr(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvashr(stp_tm tm, stp_term a, stp_term b)

stp_term stp_concat(stp_tm tm, stp_term a, stp_term b)

stp_term stp_concat_n(stp_tm tm, size_t n, const stp_term *args)

stp_term stp_bvcomp(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvult(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvule(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvugt(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvuge(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvslt(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvsle(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvsgt(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvsge(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvuaddo(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvsaddo(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvumulo(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvsmulo(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvusubo(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvssubo(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvnego(stp_tm tm, stp_term a)

stp_term stp_bvsdivo(stp_tm tm, stp_term a, stp_term b)

stp_term stp_bvredand(stp_tm tm, stp_term a)

stp_term stp_bvredor(stp_tm tm, stp_term a)

stp_term stp_select(stp_tm tm, stp_term a, stp_term b)

stp_term stp_store(stp_tm tm, stp_term a, stp_term b, stp_term c)

stp_term stp_fp_abs(stp_tm tm, stp_term a)

stp_term stp_fp_neg(stp_tm tm, stp_term a)

stp_term stp_fp_add(stp_tm tm, stp_term rm, stp_term a, stp_term b)

stp_term stp_fp_sub(stp_tm tm, stp_term rm, stp_term a, stp_term b)

stp_term stp_fp_mul(stp_tm tm, stp_term rm, stp_term a, stp_term b)

stp_term stp_fp_div(stp_tm tm, stp_term rm, stp_term a, stp_term b)

stp_term stp_fp_fma(stp_tm tm, stp_term rm, stp_term a, stp_term b, stp_term c)

stp_term stp_fp_sqrt(stp_tm tm, stp_term rm, stp_term a)

stp_term stp_fp_rem(stp_tm tm, stp_term a, stp_term b)

stp_term stp_fp_rti(stp_tm tm, stp_term rm, stp_term a)

stp_term stp_fp_min(stp_tm tm, stp_term a, stp_term b)

stp_term stp_fp_max(stp_tm tm, stp_term a, stp_term b)

stp_term stp_fp_eq(stp_tm tm, stp_term a, stp_term b)

stp_term stp_fp_lt(stp_tm tm, stp_term a, stp_term b)

stp_term stp_fp_leq(stp_tm tm, stp_term a, stp_term b)

stp_term stp_fp_gt(stp_tm tm, stp_term a, stp_term b)

stp_term stp_fp_geq(stp_tm tm, stp_term a, stp_term b)

stp_term stp_fp_is_normal(stp_tm tm, stp_term a)

stp_term stp_fp_is_subnormal(stp_tm tm, stp_term a)

stp_term stp_fp_is_zero(stp_tm tm, stp_term a)

stp_term stp_fp_is_inf(stp_tm tm, stp_term a)

stp_term stp_fp_is_nan(stp_tm tm, stp_term a)

stp_term stp_fp_is_neg(stp_tm tm, stp_term a)

stp_term stp_fp_is_pos(stp_tm tm, stp_term a)

stp_term stp_fp_to_real(stp_tm tm, stp_term a)

stp_term stp_fp_to_ieee_bv(stp_tm tm, stp_term a)

stp_term stp_real_add(stp_tm tm, stp_term a, stp_term b)

stp_term stp_real_add_n(stp_tm tm, size_t n, const stp_term *args)

stp_term stp_real_sub(stp_tm tm, stp_term a, stp_term b)

stp_term stp_real_neg(stp_tm tm, stp_term a)

stp_term stp_real_mul(stp_tm tm, stp_term a, stp_term b)

stp_term stp_real_div(stp_tm tm, stp_term a, stp_term b)

stp_term stp_real_lt(stp_tm tm, stp_term a, stp_term b)

stp_term stp_real_le(stp_tm tm, stp_term a, stp_term b)

stp_term stp_real_gt(stp_tm tm, stp_term a, stp_term b)

stp_term stp_real_ge(stp_tm tm, stp_term a, stp_term b)

stp_term stp_extract(stp_tm, uint32_t hi, uint32_t lo, stp_term)

the indexed and sort-taking constructors, by hand

stp_term stp_zero_extend(stp_tm, uint32_t k, stp_term)

stp_term stp_sign_extend(stp_tm, uint32_t k, stp_term)

stp_term stp_repeat(stp_tm, uint32_t k, stp_term)

stp_term stp_rotate_left(stp_tm, uint32_t k, stp_term)

stp_term stp_rotate_right(stp_tm, uint32_t k, stp_term)

stp_term stp_bit(stp_tm, stp_term bv, uint32_t i)

sugar: (= ((_ extract i i) bv) #b1)

stp_term stp_bool_to_bv1(stp_tm, stp_term b)

sugar: (ite b #b1 #b0)

stp_term stp_bv1_to_bool(stp_tm, stp_term bv1)

sugar: (= bv1 #b1)

stp_term stp_to_fp(stp_tm, stp_sort fp, stp_term rm, stp_term fp_or_real_or_sbv)

(_ to_fp e s) by argument sort

stp_term stp_to_fp_unsigned(stp_tm, stp_sort fp, stp_term rm, stp_term bv)

stp_term stp_to_fp_from_bits(stp_tm, stp_sort fp, stp_term bv)

the reinterpretation

stp_term stp_fp_to_ubv(stp_tm, uint32_t m, stp_term rm, stp_term)

stp_term stp_fp_to_sbv(stp_tm, uint32_t m, stp_term rm, stp_term)

stp_term stp_fp_add_rm(stp_tm, stp_rm, stp_term, stp_term)

Every FP function taking a stp_term rm also has a _rm variant taking stp_rm.

stp_term stp_fp_sub_rm(stp_tm, stp_rm, stp_term, stp_term)

stp_term stp_fp_mul_rm(stp_tm, stp_rm, stp_term, stp_term)

stp_term stp_fp_div_rm(stp_tm, stp_rm, stp_term, stp_term)

stp_term stp_fp_fma_rm(stp_tm, stp_rm, stp_term, stp_term, stp_term)

stp_term stp_fp_sqrt_rm(stp_tm, stp_rm, stp_term)

stp_term stp_fp_rti_rm(stp_tm, stp_rm, stp_term)

stp_term stp_to_fp_rm(stp_tm, stp_sort fp, stp_rm, stp_term fp_or_real_or_sbv)

stp_term stp_to_fp_unsigned_rm(stp_tm, stp_sort fp, stp_rm, stp_term bv)

stp_term stp_fp_to_ubv_rm(stp_tm, uint32_t m, stp_rm, stp_term)

stp_term stp_fp_to_sbv_rm(stp_tm, uint32_t m, stp_rm, stp_term)