bitwuzla-cxx 0.4.0 (latest)

type t =

| Constant
(*
First order constant.
*)
| Const_array
(*
Constant array.
*)
| Value
(*
Value.
*)
| Variable
(*
Bound variable.
*)
| And
(*
Boolean and.
SMT-LIB: and
*)
| Distinct
(*
Disequality.
SMT-LIB: distinct
*)
| Equal
(*
Equality.
SMT-LIB: =
*)
| Iff
(*
Boolean if and only if.
SMT-LIB: =
*)
| Implies
(*
Boolean implies.
SMT-LIB: =>
*)
| Not
(*
Boolean not.
SMT-LIB: not
*)
| Or
(*
Boolean or.
SMT-LIB: or
*)
| Xor
(*
Boolean xor.
SMT-LIB: xor
*)
| Ite
(*
If-then-else.
SMT-LIB: ite
*)
| Exists
(*
Existential quantification.
SMT-LIB: exists
*)
| Forall
(*
Universal quantification.
SMT-LIB: forall
*)
| Apply
(*
Function application.
*)
| Lambda
(*
Lambda.
*)
| Select
(*
Array select.
SMT-LIB: select
*)
| Store
(*
Array store.
SMT-LIB: store
*)
| Bv_add
(*
Bit-vector addition.
SMT-LIB: bvadd
*)
| Bv_and
(*
Bit-vector and.
SMT-LIB: bvand
*)
| Bv_ashr
(*
Bit-vector arithmetic right shift.
SMT-LIB: bvashr
*)
| Bv_comp
(*
Bit-vector comparison.
SMT-LIB: bvcomp
*)
| Bv_concat
(*
Bit-vector concat.
SMT-LIB: concat
*)
| Bv_dec
(*
Bit-vector decrement.
Decrement by one.
*)
| Bv_inc
(*
Bit-vector increment.
Increment by one.
*)
| Bv_mul
(*
Bit-vector multiplication.
SMT-LIB: bvmul
*)
| Bv_nand
(*
Bit-vector nand.
SMT-LIB: bvnand
*)
| Bv_neg
(*
Bit-vector negation (two's complement).
SMT-LIB: bvneg
*)
| Bv_nego
(*
Bit-vector negation overflow test.
Predicate indicating if bit-vector negation produces an overflow.
SMT-LIB: bvnego
*)
| Bv_nor
(*
Bit-vector nor.
SMT-LIB: bvnor
*)
| Bv_not
(*
Bit-vector not (one's complement).
SMT-LIB: bvnot
*)
| Bv_or
(*
Bit-vector or.
SMT-LIB: bvor
*)
| 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.
*)
| 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.
*)
| 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.
*)
| Bv_rol
(*
Bit-vector rotate left (not indexed).
This is a non-indexed variant of SMT-LIB rotate_left.
*)
| Bv_ror
(*
Bit-vector rotate right.
This is a non-indexed variant of SMT-LIB rotate_right.
*)
| Bv_saddo
(*
Bit-vector signed addition overflow test.
Single bit to indicate if signed addition produces an overflow.
*)
| Bv_sdivo
(*
Bit-vector signed division overflow test.
Single bit to indicate if signed division produces an overflow.
*)
| Bv_sdiv
(*
Bit-vector signed division.
SMT-LIB: bvsdiv
*)
| Bv_sge
(*
Bit-vector signed greater than or equal.
SMT-LIB: bvsge
*)
| Bv_sgt
(*
Bit-vector signed greater than.
SMT-LIB: bvsgt
*)
| Bv_shl
(*
Bit-vector logical left shift.
SMT-LIB: bvshl
*)
| Bv_shr
(*
Bit-vector logical right shift.
SMT-LIB: bvshr
*)
| Bv_sle
(*
Bit-vector signed less than or equal.
SMT-LIB: bvsle
*)
| Bv_slt
(*
Bit-vector signed less than.
SMT-LIB: bvslt
*)
| Bv_smod
(*
Bit-vector signed modulo.
SMT-LIB: bvsmod
*)
| Bv_smulo
(*
Bit-vector signed multiplication overflow test.
SMT-LIB: bvsmod
*)
| Bv_srem
(*
Bit-vector signed remainder.
SMT-LIB: bvsrem
*)
| Bv_ssubo
(*
Bit-vector signed subtraction overflow test.
Single bit to indicate if signed subtraction produces an overflow.
*)
| Bv_sub
(*
Bit-vector subtraction.
SMT-LIB: bvsub
*)
| Bv_uaddo
(*
Bit-vector unsigned addition overflow test.
Single bit to indicate if unsigned addition produces an overflow.
*)
| Bv_udiv
(*
Bit-vector unsigned division.
SMT-LIB: bvudiv
*)
| Bv_uge
(*
Bit-vector unsigned greater than or equal.
SMT-LIB: bvuge
*)
| Bv_ugt
(*
Bit-vector unsigned greater than.
SMT-LIB: bvugt
*)
| Bv_ule
(*
Bit-vector unsigned less than or equal.
SMT-LIB: bvule
*)
| Bv_ult
(*
Bit-vector unsigned less than.
SMT-LIB: bvult
*)
| Bv_umulo
(*
Bit-vector unsigned multiplication overflow test.
Single bit to indicate if unsigned multiplication produces an overflow.
*)
| Bv_urem
(*
Bit-vector unsigned remainder.
SMT-LIB: bvurem
*)
| Bv_usubo
(*
Bit-vector unsigned subtraction overflow test.
Single bit to indicate if unsigned subtraction produces an overflow.
*)
| Bv_xnor
(*
Bit-vector xnor.
SMT-LIB: bvxnor
*)
| Bv_xor
(*
Bit-vector xor.
SMT-LIB: bvxor
*)
| Bv_extract
(*
Bit-vector extract.
SMT-LIB: extract (indexed)
*)
| Bv_repeat
(*
Bit-vector repeat.
SMT-LIB: repeat (indexed)
*)
| Bv_roli
(*
Bit-vector rotate left by integer.
SMT-LIB: rotate_left (indexed)
*)
| Bv_rori
(*
Bit-vector rotate right by integer.
SMT-LIB: rotate_right (indexed)
*)
| Bv_sign_extend
(*
Bit-vector sign extend.
SMT-LIB: sign_extend (indexed)
*)
| Bv_zero_extend
(*
Bit-vector zero extend.
SMT-LIB: zero_extend (indexed)
*)
| Fp_abs
(*
Floating-point absolute value.
SMT-LIB: fp.abs
*)
| Fp_add
(*
Floating-point addition.
SMT-LIB: fp.add
*)
| Fp_div
(*
Floating-point division.
SMT-LIB: fp.div
*)
| Fp_equal
(*
Floating-point equality.
SMT-LIB: fp.eq
*)
| Fp_fma
(*
Floating-point fused multiplcation and addition.
SMT-LIB: fp.fma
*)
| Fp_fp
(*
Floating-point IEEE 754 value.
SMT-LIB: fp
*)
| Fp_geq
(*
Floating-point greater than or equal.
SMT-LIB: fp.geq
*)
| Fp_gt
(*
Floating-point greater than.
SMT-LIB: fp.gt
*)
| Fp_is_inf
(*
Floating-point is infinity tester.
SMT-LIB: fp.isInfinite
*)
| Fp_is_nan
(*
Floating-point is Nan tester.
SMT-LIB: fp.isNaN
*)
| Fp_is_neg
(*
Floating-point is negative tester.
SMT-LIB: fp.isNegative
*)
| Fp_is_normal
(*
Floating-point is normal tester.
SMT-LIB: fp.isNormal
*)
| Fp_is_pos
(*
Floating-point is positive tester.
SMT-LIB: fp.isPositive
*)
| Fp_is_subnormal
(*
Floating-point is subnormal tester.
SMT-LIB: fp.isSubnormal
*)
| Fp_is_zero
(*
Floating-point is zero tester.
SMT-LIB: fp.isZero
*)
| Fp_leq
(*
Floating-point less than or equal.
SMT-LIB: fp.leq
*)
| Fp_lt
(*
Floating-point less than.
SMT-LIB: fp.lt
*)
| Fp_max
(*
Floating-point max.
SMT-LIB: fp.max
*)
| Fp_min
(*
Floating-point min.
SMT-LIB: fp.min
*)
| Fp_mul
(*
Floating-point multiplcation.
SMT-LIB: fp.mul
*)
| Fp_neg
(*
Floating-point negation.
SMT-LIB: fp.neg
*)
| Fp_rem
(*
Floating-point remainder.
SMT-LIB: fp.rem
*)
| Fp_rti
(*
Floating-point round to integral.
SMT-LIB: fp.roundToIntegral
*)
| Fp_sqrt
(*
Floating-point round to square root.
SMT-LIB: fp.sqrt
*)
| Fp_sub
(*
Floating-point round to subtraction.
SMT-LIB: fp.sqrt
*)
| Fp_to_fp_from_bv
(*
Floating-point to_fp from IEEE 754 bit-vector.
SMT-LIB: to_fp (indexed)
*)
| Fp_to_fp_from_fp
(*
Floating-point to_fp from floating-point.
SMT-LIB: to_fp (indexed)
*)
| Fp_to_fp_from_sbv
(*
Floating-point to_fp from signed bit-vector value.
SMT-LIB: to_fp (indexed)
*)
| Fp_to_fp_from_ubv
(*
Floating-point to_fp from unsigned bit-vector value.
SMT-LIB: to_fp_unsigned (indexed)
*)
| Fp_to_sbv
(*
Floating-point to_sbv.
SMT-LIB: fp.to_sbv (indexed)
*)
| Fp_to_ubv
(*
Floating-point to_ubv.
SMT-LIB: fp.to_ubv (indexed)
*)

The term kind.

val to_string : t -> string

to_string t get string representation of this kind.

returns
String representation of this kind.

package bitwuzla-cxx