Kind

The kind of a bitwuzla::Term.

Terms of a given kind are created via bitwuzla::mk_term(). The kind of a term can be queried via bitwuzla::Term::kind().

The string representation of a term kind can be queried via std::string std::to_string(bitwuzla::Kind kind), and printed to a given ostream via std::ostream& bitwuzla::operator<<(std::ostream& out, Kind kind).

namespace bitwuzla {

enum class bitwuzla::Kind

The term kind.

Values:

enumerator CONSTANT

First order constant.

enumerator CONST_ARRAY

Constant array.

enumerator VALUE

Value.

enumerator VARIABLE

Bound variable.

enumerator AND

Boolean and.

SMT-LIB: and

Number of arguments: >= 2

Arguments: \(Bool \times ... \times Bool \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator DISTINCT

Disequality.

SMT-LIB: distinct

Number of Arguments: >= 2

Arguments: \(S \times ... \times S \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator EQUAL

Equality.

SMT-LIB: =

Number of Arguments: >= 2

Arguments: \(S \times ... \times S \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator IFF

Boolean if and only if.

SMT-LIB: =

Number of Arguments: >= 2

Arguments: \(Bool \times ... \times Bool \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator IMPLIES

Boolean implies.

SMT-LIB: =>

Number of Arguments: >= 2

Arguments: \(Bool \times ... \times Bool \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator NOT

Boolean not.

SMT-LIB: not

Number of Arguments: 1

Arguments: \(Bool \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator OR

Boolean or.

SMT-LIB: or

Number of Arguments: >= 2

Arguments: \(Bool \times ... \times Bool \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator XOR

Boolean xor.

SMT-LIB: xor

Number of Arguments: >= 2

Arguments: \(Bool \times ... \times Bool \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator ITE

If-then-else.

SMT-LIB: ite

Number of Arguments: 3

Arguments: \(Bool \times S \times S \rightarrow S\)

Create with:

  • C

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator EXISTS

Existential quantification.

SMT-LIB: exists

Number of Arguments: >= 2

Arguments:\(S_1 \times ... \times S_n \times Bool \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FORALL

Universal quantification.

SMT-LIB: forall

Number of Arguments: >= 2

Arguments:\(S_1 \times ... \times S_n \times Bool \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator APPLY

Function application.

Number of Arguments: >= 2

Arguments:\((S_1 \times ... \times S_n \rightarrow S) \times S_1 \times ... \times S_n \rightarrow S\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator LAMBDA

Lambda.

Number of Arguments: >= 2

Arguments:\(S_1 \times ... \times S_n \times S \rightarrow (S_1 \times ... \times S_n \rightarrow S)\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator ARRAY_SELECT

Array select.

SMT-LIB: select

Number of Arguments: 2

Arguments: \((S_i \rightarrow S_e) \times S_i \rightarrow S_e\)

Create with:

  • C

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator ARRAY_STORE

Array store.

SMT-LIB: store

Number of Arguments: 3

Arguments:\((S_i \rightarrow S_e) \times S_i \times S_e \rightarrow (S_i \rightarrow S_e)\)

Create with:

  • C

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_ADD

Bit-vector addition.

SMT-LIB: bvadd

Number of Arguments: >= 2

Arguments: \(BV_n \times ... \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_AND

Bit-vector and.

SMT-LIB: bvand

Number of Arguments: >= 2

Arguments: \(BV_n \times ... \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_ASHR

Bit-vector arithmetic right shift.

SMT-LIB: bvashr

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_COMP

Bit-vector comparison.

SMT-LIB: bvcomp

Number of Arguments: >= 2

Arguments: \(BV_n \times ... \times BV_n \rightarrow BV_1\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_CONCAT

Bit-vector concat.

SMT-LIB: concat

Number of Arguments: >= 2

Arguments:\(BV_n \times ... \times BV_m \rightarrow BV_{n + ... + m}\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_DEC

Bit-vector decrement.

Decrement by one.

Number of arguments: 1

Arguments: \(BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_INC

Bit-vector increment.

Increment by one.

Number of Arguments: 1

Arguments: \(BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_MUL

Bit-vector multiplication.

SMT-LIB: bvmul

Number of Arguments: >= 2

Arguments: \(BV_n \times ... \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_NAND

Bit-vector nand.

SMT-LIB: bvnand

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_NEG

Bit-vector negation (two’s complement).

SMT-LIB: bvneg

Number of Arguments: 1

Arguments: \(BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_NEG_OVERFLOW

Bit-vector negation overflow test.

Predicate indicating if bit-vector negation produces an overflow.

SMT-LIB: bvnego

Number of Arguments: 1

Arguments: \(BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_NOR

Bit-vector nor.

SMT-LIB: bvnor

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_NOT

Bit-vector not (one’s complement).

SMT-LIB: bvnot

Number of Arguments: 1

Arguments: \(BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_OR

Bit-vector or.

SMT-LIB: bvor

Number of Arguments: >= 2

Arguments: \(BV_n \times ... \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_REDAND

Bit-vector and reduction.

Bit-wise and reduction), all bits are and’ed together into a single bit. This corresponds to bit-wise and reduction as known from Verilog.

Number of Arguments: 1

Arguments: \(BV_n \rightarrow BV_1\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_REDOR

Bit-vector reduce or.

Bit-wise or reduction), all bits are or’ed together into a single bit. This corresponds to bit-wise or reduction as known from Verilog.

Number of Arguments: 1

Arguments: \(BV_n \rightarrow BV_1\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_REDXOR

Bit-vector reduce xor.

Bit-wise xor reduction), all bits are xor’ed together into a single bit. This corresponds to bit-wise xor reduction as known from Verilog.

Number of Arguments: 1

Arguments: \(BV_n \rightarrow BV_1\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_ROL

Bit-vector rotate left (not indexed).

This is a non-indexed variant of SMT-LIB rotate_left.

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_ROR

Bit-vector rotate right.

This is a non-indexed variant of SMT-LIB rotate_right.

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SADD_OVERFLOW

Bit-vector signed addition overflow test.

Predicate indicating if signed addition produces an overflow.

SMT-LIB: bvsaddo

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SDIV_OVERFLOW

Bit-vector signed division overflow test.

Predicate indicating if signed division produces an overflow.

SMT-LIB: bvsdivo

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SDIV

Bit-vector signed division.

SMT-LIB: bvsdiv

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SGE

Bit-vector signed greater than or equal.

SMT-LIB: bvsle

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SGT

Bit-vector signed greater than.

SMT-LIB: bvslt

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SHL

Bit-vector logical left shift.

SMT-LIB: bvshl

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SHR

Bit-vector logical right shift.

SMT-LIB: bvshr

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SLE

Bit-vector signed less than or equal.

SMT-LIB: bvsle

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SLT

Bit-vector signed less than.

SMT-LIB: bvslt

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SMOD

Bit-vector signed modulo.

SMT-LIB: bvsmod

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SMUL_OVERFLOW

Bit-vector signed multiplication overflow test.

Predicate indicating if signed multiplication produces an overflow.

SMT-LIB: bvsmulo

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SREM

Bit-vector signed remainder.

SMT-LIB: bvsrem

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SSUB_OVERFLOW

Bit-vector signed subtraction overflow test.

Predicate indicatin if signed subtraction produces an overflow.

SMT-LIB: bvssubo

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SUB

Bit-vector subtraction.

SMT-LIB: bvsub

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_UADD_OVERFLOW

Bit-vector unsigned addition overflow test.

Predicate indicating if unsigned addition produces an overflow.

SMT-LIB: bvuaddo

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_UDIV

Bit-vector unsigned division.

SMT-LIB: bvudiv

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_UGE

Bit-vector unsigned greater than or equal.

SMT-LIB: bvuge

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_UGT

Bit-vector unsigned greater than.

SMT-LIB: bvugt

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_ULE

Bit-vector unsigned less than or equal.

SMT-LIB: bvule

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_ULT

Bit-vector unsigned less than.

SMT-LIB: bvult

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_UMUL_OVERFLOW

Bit-vector unsigned multiplication overflow test.

Predicate indicating if unsigned multiplication produces an overflow.

SMT-LIB: bvumulo

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_UREM

Bit-vector unsigned remainder.

SMT-LIB: bvurem

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_USUB_OVERFLOW

Bit-vector unsigned subtraction overflow test.

Predicate indicating if unsigned subtraction produces an overflow.

SMT-LIB: bvusubo

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_XNOR

Bit-vector xnor.

SMT-LIB: bvxnor

Number of Arguments: 2

Arguments: \(BV_n \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_XOR

Bit-vector xor.

SMT-LIB: bvxor

Number of Arguments: >= 2

Arguments: \(BV_n \times ... \times BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_EXTRACT

Bit-vector extract.

SMT-LIB: extract (indexed)

Number of Arguments: 1

Number of Indices: 2 ( \(u\), \(l\) with \(u \geq l\))

Arguments: \(BV_n \rightarrow BV_{u - l + 1}\)

Create with:

  • C

    • bitwuzla_mk_term1_indexed2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_REPEAT

Bit-vector repeat.

SMT-LIB: repeat (indexed)

Number of Arguments: 1

Number of Indices: 1 ( \(i\) s.t. \(i \cdot n\) fits into uint64_t)

Arguments: \(BV_n \rightarrow BV_{n * i}\)

Create with:

  • C

    • bitwuzla_mk_term1_indexed1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_ROLI

Bit-vector rotate left by integer.

SMT-LIB: rotate_left (indexed)

Number of Arguments: 1

Number of Indices: 1

Arguments: \(BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term1_indexed1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_RORI

Bit-vector rotate right by integer.

SMT-LIB: rotate_right (indexed)

Number of Arguments: 1

Number of Indices: 1

Arguments: \(BV_n \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term1_indexed1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_SIGN_EXTEND

Bit-vector sign extend.

SMT-LIB: sign_extend (indexed)

Number of Arguments: 1

Number of Indices: 1 ( \(i\) s.t. \(i + n\) fits into uint64_t)

Arguments: \(BV_n \rightarrow BV_{n + i}\)

Create with:

  • C

    • bitwuzla_mk_term1_indexed1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator BV_ZERO_EXTEND

Bit-vector zero extend.

SMT-LIB: zero_extend (indexed)

Number of Arguments: 1

Number of Indices: 1 ( \(i\) s.t. \(i + n\) fits into uint64_t)

Arguments: \(BV_n \rightarrow BV_{n + i}\)

Create with:

  • C

    • bitwuzla_mk_term1_indexed1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_ABS

Floating-point absolute value.

SMT-LIB: fp.abs

Number of Arguments: 1

Arguments: \(\mathit{FP}_{es} \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_ADD

Floating-point addition.

SMT-LIB: fp.add

Number of Arguments: 3

Arguments:\(RM \times \mathit{FP}_{es} \times \mathit{FP}_{es} \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_DIV

Floating-point division.

SMT-LIB: fp.div

Number of Arguments: 3

Arguments:\(RM \times \mathit{FP}_{es} \times \mathit{FP}_{es} \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_EQUAL

Floating-point equality.

SMT-LIB: fp.eq

Number of Arguments: >= 2

Arguments:\(\mathit{FP}_{es} \times ... \times \mathit{FP}_{es} \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_FMA

Floating-point fused multiplcation and addition.

SMT-LIB: fp.fma

Number of Arguments: 4

Arguments:\(RM \times \mathit{FP}_{es} \times \mathit{FP}_{es} \times \mathit{FP}_{es} \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_FP

Floating-point IEEE 754 value.

SMT-LIB: fp

Number of Arguments: 3

Arguments:\(BV_1 \times BV_e \times BV_{s-1} \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_GEQ

Floating-point greater than or equal.

SMT-LIB: fp.geq

Number of Arguments: 2

Arguments:\(\mathit{FP}_{es} \times ... \times \mathit{FP}_{es} \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_GT

Floating-point greater than.

SMT-LIB: fp.gt

Number of Arguments: 2

Arguments:\(\mathit{FP}_{es} \times ... \times \mathit{FP}_{es} \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_IS_INF

Floating-point is infinity tester.

SMT-LIB: fp.isInfinite

Number of Arguments: 1

Arguments: \(\mathit{FP}_{es} \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_IS_NAN

Floating-point is Nan tester.

SMT-LIB: fp.isNaN

Number of Arguments: 1

Arguments: \(\mathit{FP}_{es} \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_IS_NEG

Floating-point is negative tester.

SMT-LIB: fp.isNegative

Number of Arguments: 1

Arguments: \(\mathit{FP}_{es} \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_IS_NORMAL

Floating-point is normal tester.

SMT-LIB: fp.isNormal

Number of Arguments: 1

Arguments: \(\mathit{FP}_{es} \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_IS_POS

Floating-point is positive tester.

SMT-LIB: fp.isPositive

Number of Arguments: 1

Arguments: \(\mathit{FP}_{es} \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_IS_SUBNORMAL

Floating-point is subnormal tester.

SMT-LIB: fp.isSubnormal

Number of Arguments: 1

Arguments: \(\mathit{FP}_{es} \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_IS_ZERO

Floating-point is zero tester.

SMT-LIB: fp.isZero

Number of Arguments: 1

Arguments: \(\mathit{FP}_{es} \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_LEQ

Floating-point less than or equal.

SMT-LIB: fp.leq

Number of Arguments: >= 2

Arguments:\(\mathit{FP}_{es} \times ... \times \mathit{FP}_{es} \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_LT

Floating-point less than.

SMT-LIB: fp.lt

Number of Arguments: >= 2

Arguments: \(\mathit{FP}_{es} \rightarrow Bool\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_MAX

Floating-point max.

SMT-LIB: fp.max

Number of Arguments: 2

Arguments:\(\mathit{FP}_{es} \times \mathit{FP}_{es} \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_MIN

Floating-point min.

SMT-LIB: fp.min

Number of Arguments: 2

Arguments:\(\mathit{FP}_{es} \times \mathit{FP}_{es} \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_MUL

Floating-point multiplcation.

SMT-LIB: fp.mul

Number of Arguments: 3

Arguments:\(RM \times \mathit{FP}_{es} \times \mathit{FP}_{es} \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_NEG

Floating-point negation.

SMT-LIB: fp.neg

Number of Arguments: 1

Arguments: \(\mathit{FP}_{es} \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_REM

Floating-point remainder.

SMT-LIB: fp.rem

Number of Arguments: 2

Arguments:\(\mathit{FP}_{es} \times \mathit{FP}_{es} \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_RTI

Floating-point round to integral.

SMT-LIB: fp.roundToIntegral

Number of Arguments: 2

Arguments:\(RM \times \mathit{FP}_{es} \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_SQRT

Floating-point square root.

SMT-LIB: fp.sqrt

Number of Arguments: 2

Arguments:\(RM \times \mathit{FP}_{es} \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_SUB

Floating-point subtraction.

SMT-LIB: fp.sub

Number of Arguments: 3

Arguments:\(RM \times \mathit{FP}_{es} \times \mathit{FP}_{es} \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term3()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_TO_FP_FROM_BV

Floating-point to_fp from IEEE 754 bit-vector.

SMT-LIB: to_fp (indexed)

Number of Arguments: 1

Number of Indices: 2 ( \(e\), \(s\))

Arguments: \(BV_n \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term1_indexed2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_TO_FP_FROM_FP

Floating-point to_fp from floating-point.

SMT-LIB: to_fp (indexed)

Number of Arguments: 2

Number of Indices: 2 ( \(e\), \(s\))

Arguments:\(RM \times \mathit{FP}_{e's'} \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term2_indexed2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_TO_FP_FROM_SBV

Floating-point to_fp from signed bit-vector value.

SMT-LIB: to_fp (indexed)

Number of Arguments: 2

Number of Indices: 2 ( \(e\), \(s\))

Arguments: \(RM \times BV_n \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term2_indexed2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_TO_FP_FROM_UBV

Floating-point to_fp from unsigned bit-vector value.

SMT-LIB: to_fp_unsigned (indexed)

Number of Arguments: 2

Number of Indices: 2 ( \(e\), \(s\))

Arguments: \(RM \times BV_n \rightarrow \mathit{FP}_{es}\)

Create with:

  • C

    • bitwuzla_mk_term2_indexed2()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_TO_SBV

Floating-point to_sbv.

SMT-LIB: fp.to_sbv (indexed)

Number of Arguments: 2

Number of Indices: 1 ( \(n\))

Arguments: \(RM \times \mathit{FP}_{es} \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2_indexed1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

enumerator FP_TO_UBV

Floating-point to_ubv.

SMT-LIB: fp.to_ubv (indexed)

Number of Arguments: 2

Number of Indices: 1 ( \(n\))

Arguments: \(RM \times \mathit{FP}_{es} \rightarrow BV_n\)

Create with:

  • C

    • bitwuzla_mk_term2_indexed1()

    • bitwuzla_mk_term()

  • C++

    • bitwuzla::mk_term()

std::ostream &bitwuzla::operator<<(std::ostream &out, Kind kind)

Print kind to output stream.

Parameters:

  • out – The output stream.

  • kind – The kind.

Returns:

The output stream.

}

namespace std {

std::string std::to_string(bitwuzla::Kind kind)

Get string representation of given kind.

Parameters:

kind – The kind.

Returns:

The string representation.

}