Functions and operators

template<class I>
using stp::api::if_integral = std::enable_if_t<std::is_integral_v<I> && !std::is_same_v<I, bool>, int>

template<class F>
using stp::api::if_floating = std::enable_if_t<std::is_floating_point_v<F>, int>

using stp::api::OptionValue = std::variant<bool, std::int64_t, std::uint64_t, std::string, std::vector<std::string>>

using stp::api::StatisticValue = std::variant<std::uint64_t, double, std::string>

const char *stp::api::to_string(Kind)

const char *stp::api::smtlib_name(Kind)

“bvadd”, “fp.add”, “select”, …

const char *stp::api::to_string(SortKind)

const char *stp::api::to_string(RoundingMode)

“RNE” …

const char *stp::api::to_string(UnknownReason)

const char *stp::api::to_string(ErrorCode)

const char *stp::api::to_string(Verdict)

const char *stp::api::to_string(Validity)

const char *stp::api::to_string(Tier)

const char *stp::api::to_string(Settable)

std::ostream &stp::api::operator<<(std::ostream&, Kind)

std::ostream &stp::api::operator<<(std::ostream&, RoundingMode)

std::ostream &stp::api::operator<<(std::ostream&, UnknownReason)

std::ostream &stp::api::operator<<(std::ostream&, Verdict)

std::ostream &stp::api::operator<<(std::ostream&, Validity)

Term stp::api::extract(std::uint32_t hi, std::uint32_t lo, const Term&)

Term stp::api::zero_extend(std::uint32_t k, const Term&)

Term stp::api::sign_extend(std::uint32_t k, const Term&)

Term stp::api::repeat(std::uint32_t k, const Term&)

Term stp::api::rotate_left(std::uint32_t k, const Term&)

Term stp::api::rotate_right(std::uint32_t k, const Term&)

Term stp::api::concat(const Term&, const Term&)

Term stp::api::bit(const Term &bv, std::uint32_t i)

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

Term stp::api::bool_to_bv1(const Term &b)

(ite b #b1 #b0)

Term stp::api::bv1_to_bool(const Term &bv1)

(= bv1 #b1)

Term stp::api::array_from_bytes(TermManager &tm, const std::vector<std::uint8_t> &bytes, std::uint32_t index_width = 32)

A store chain over (as const … 0) holding bytes at indices [0, n) of an Array BV[index_width] BV8.

Term stp::api::to_fp(const Sort &fp, const Term &rm, const Term &fp_or_real_or_sbv)

The SMT-LIB (_ to_fp e s) family, by argument sort (FP, Real or signed BV).

Term stp::api::to_fp(const Sort &fp, RoundingMode rm, const Term &fp_or_real_or_sbv)

Term stp::api::to_fp_unsigned(const Sort &fp, const Term &rm, const Term &bv)

Term stp::api::to_fp_unsigned(const Sort &fp, RoundingMode rm, const Term &bv)

Term stp::api::to_fp_from_bits(const Sort &fp, const Term &bv)

the reinterpretation

Term stp::api::fp_to_ubv(std::uint32_t m, const Term &rm, const Term&)

Term stp::api::fp_to_sbv(std::uint32_t m, const Term &rm, const Term&)

Term stp::api::fp_to_ubv(std::uint32_t m, RoundingMode rm, const Term&)

Term stp::api::fp_to_sbv(std::uint32_t m, RoundingMode rm, const Term&)

inline Term stp::api::operator+(const Term &a, const Term &b)

inline Term stp::api::operator-(const Term &a, const Term &b)

inline Term stp::api::operator*(const Term &a, const Term &b)

inline Term stp::api::operator/(const Term &a, const Term &b)

inline Term stp::api::operator-(const Term &a)

inline Term stp::api::operator~(const Term &a)

inline Term stp::api::operator&(const Term &a, const Term &b)

inline Term stp::api::operator|(const Term &a, const Term &b)

inline Term stp::api::operator^(const Term &a, const Term &b)

inline Term stp::api::operator<<(const Term &a, const Term &b)

inline Term stp::api::operator!(const Term &a)

inline Term stp::api::operator&&(const Term &a, const Term &b)

inline Term stp::api::operator||(const Term &a, const Term &b)

Version stp::api::version()

std::map<std::string, std::string> stp::api::capabilities()

What this build can do. Keys are stable strings.

bool stp::api::has_sat_backend(std::string_view name)

std::vector<std::string> stp::api::sat_backends()

void stp::api::set_internal_error_policy(InternalErrorPolicy) noexcept

Process-wide by nature: what an INTERNAL or RESOURCE error does. Default POISON; STP_ABORT_ON_INTERNAL_ERROR=1 in the environment selects ABORT.

InternalErrorPolicy stp::api::internal_error_policy() noexcept