package bitwuzla-cxx
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=496fb480731b9a12db47a212d0c752b749c33f811ae684260c9643f69f257abb
sha512=f092f868a053526efdcb5b2a5a83e3672f64a12de9dff4fa13f174afc5b4ec8b083c70a12581cad52cb3889ce000d88080c8752242bc7e992c11357d848f4b23
doc/bitwuzla-cxx/Bitwuzla_cxx/Kind/index.html
Module Bitwuzla_cxx.KindSource
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.