BitwuzlaKind

The kind of a BitwuzlaTerm.

Terms of a given kind are created via bitwuzla_mk_term(), bitwuzla_mk_term1(), bitwuzla_mk_term2(), bitwuzla_mk_term3(), bitwuzla_mk_term1_indexed1(), bitwuzla_mk_term1_indexed2(), bitwuzla_mk_term2_indexed1(), and bitwuzla_mk_term1_indexed2().

The kind of a term can be queried via bitwuzla_term_get_kind(). The string representation of a term kind can be queried via bitwuzla_term_to_string(), and printed to a given file via bitwuzla_term_print().

enum BitwuzlaKind

The term kind.

Values:

enumerator BITWUZLA_KIND_CONSTANT

First order constant.

enumerator BITWUZLA_KIND_CONST_ARRAY

Constant array.

enumerator BITWUZLA_KIND_VALUE

Value.

enumerator BITWUZLA_KIND_VARIABLE

Bound variable.

enumerator BITWUZLA_KIND_AND

Boolean and.

SMT-LIB: and

Number of arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_DISTINCT

Disequality.

SMT-LIB: distinct

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_EQUAL

Equality.

SMT-LIB: =

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_IFF

Boolean if and only if.

SMT-LIB: =

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_IMPLIES

Boolean implies.

SMT-LIB: =>

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_NOT

Boolean not.

SMT-LIB: not

Number of Arguments: 1

Arguments: \(Bool \rightarrow Bool\)

Create with:

enumerator BITWUZLA_KIND_OR

Boolean or.

SMT-LIB: or

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_XOR

Boolean xor.

SMT-LIB: xor

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_ITE

If-then-else.

SMT-LIB: ite

Number of Arguments: 3

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

Create with:

enumerator BITWUZLA_KIND_EXISTS

Existential quantification.

SMT-LIB: exists

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_FORALL

Universal quantification.

SMT-LIB: forall

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_BV_ADD

Bit-vector addition.

SMT-LIB: bvadd

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_BV_AND

Bit-vector and.

SMT-LIB: bvand

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_BV_COMP

Bit-vector comparison.

SMT-LIB: bvcomp

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_BV_DEC

Bit-vector decrement.

Decrement by one.

Number of arguments: 1

Arguments: \(BV_n \rightarrow BV_n\)

Create with:

enumerator BITWUZLA_KIND_BV_INC

Bit-vector increment.

Increment by one.

Number of Arguments: 1

Arguments: \(BV_n \rightarrow BV_n\)

Create with:

enumerator BITWUZLA_KIND_BV_MUL

Bit-vector multiplication.

SMT-LIB: bvmul

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_BV_NAND

Bit-vector nand.

SMT-LIB: bvnand

Number of Arguments: 2

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

Create with:

enumerator BITWUZLA_KIND_BV_NEG

Bit-vector negation (two’s complement).

SMT-LIB: bvneg

Number of Arguments: 1

Arguments: \(BV_n \rightarrow BV_n\)

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_BV_NOR

Bit-vector nor.

SMT-LIB: bvnor

Number of Arguments: 2

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

Create with:

enumerator BITWUZLA_KIND_BV_NOT

Bit-vector not (one’s complement).

SMT-LIB: bvnot

Number of Arguments: 1

Arguments: \(BV_n \rightarrow BV_n\)

Create with:

enumerator BITWUZLA_KIND_BV_OR

Bit-vector or.

SMT-LIB: bvor

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_BV_SDIV

Bit-vector signed division.

SMT-LIB: bvsdiv

Number of Arguments: 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_BV_SGT

Bit-vector signed greater than.

SMT-LIB: bvslt

Number of Arguments: 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_BV_SLT

Bit-vector signed less than.

SMT-LIB: bvslt

Number of Arguments: 2

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

Create with:

enumerator BITWUZLA_KIND_BV_SMOD

Bit-vector signed modulo.

SMT-LIB: bvsmod

Number of Arguments: 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_BV_SREM

Bit-vector signed remainder.

SMT-LIB: bvsrem

Number of Arguments: 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_BV_SUB

Bit-vector subtraction.

SMT-LIB: bvsub

Number of Arguments: 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_BV_UDIV

Bit-vector unsigned division.

SMT-LIB: bvudiv

Number of Arguments: 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_BV_UGT

Bit-vector unsigned greater than.

SMT-LIB: bvugt

Number of Arguments: 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_BV_ULT

Bit-vector unsigned less than.

SMT-LIB: bvult

Number of Arguments: 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_BV_UREM

Bit-vector unsigned remainder.

SMT-LIB: bvurem

Number of Arguments: 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_BV_XNOR

Bit-vector xnor.

SMT-LIB: bvxnor

Number of Arguments: 2

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

Create with:

enumerator BITWUZLA_KIND_BV_XOR

Bit-vector xor.

SMT-LIB: bvxor

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_FP_ABS

Floating-point absolute value.

SMT-LIB: fp.abs

Number of Arguments: 1

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_FP_IS_INF

Floating-point is infinity tester.

SMT-LIB: fp.isInfinite

Number of Arguments: 1

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

Create with:

enumerator BITWUZLA_KIND_FP_IS_NAN

Floating-point is Nan tester.

SMT-LIB: fp.isNaN

Number of Arguments: 1

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

Create with:

enumerator BITWUZLA_KIND_FP_IS_NEG

Floating-point is negative tester.

SMT-LIB: fp.isNegative

Number of Arguments: 1

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

Create with:

enumerator BITWUZLA_KIND_FP_IS_NORMAL

Floating-point is normal tester.

SMT-LIB: fp.isNormal

Number of Arguments: 1

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

Create with:

enumerator BITWUZLA_KIND_FP_IS_POS

Floating-point is positive tester.

SMT-LIB: fp.isPositive

Number of Arguments: 1

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

Create with:

enumerator BITWUZLA_KIND_FP_IS_SUBNORMAL

Floating-point is subnormal tester.

SMT-LIB: fp.isSubnormal

Number of Arguments: 1

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

Create with:

enumerator BITWUZLA_KIND_FP_IS_ZERO

Floating-point is zero tester.

SMT-LIB: fp.isZero

Number of Arguments: 1

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_FP_LT

Floating-point less than.

SMT-LIB: fp.lt

Number of Arguments: >= 2

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_FP_NEG

Floating-point negation.

SMT-LIB: fp.neg

Number of Arguments: 1

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

Create with:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

enumerator BITWUZLA_KIND_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:

const char *bitwuzla_kind_to_string(BitwuzlaKind kind)

Get the string representation of a term kind.

Note

The returned char* pointer is only valid until the next bitwuzla_kind_to_string call.

Returns:

A string representation of the given term kind.