package bitwuzla-cxx

  1. Overview
  2. Docs
SMT solver for AUFBVFP (C++ API)

Install 

dune-project
 Dependency

bitwuzla.github.io Readme Changelog MIT License Edit opam file Versions (9)

Authors

  1. F
    Frédéric Recoules

Maintainers

  1. F
    Frédéric Recoules <frederic.recoules@cea.fr>

Sources

bitwuzla-cxx-0.7.0.tbz
sha256=496fb480731b9a12db47a212d0c752b749c33f811ae684260c9643f69f257abb
sha512=f092f868a053526efdcb5b2a5a83e3672f64a12de9dff4fa13f174afc5b4ec8b083c70a12581cad52cb3889ce000d88080c8752242bc7e992c11357d848f4b23

doc/bitwuzla-cxx/Bitwuzla_cxx/Kind/index.html

Module Bitwuzla_cxx.KindSource

Sourcetype t =
  1. | Constant
    (*

    First order constant.

    *)
  2. | Const_array
    (*

    Constant array.

    *)
  3. | Value
    (*

    Value.

    *)
  4. | Variable
    (*

    Bound variable.

    *)
  5. | And
    (*

    Boolean and.

    SMT-LIB: and

    *)
  6. | Distinct
    (*

    Disequality.

    SMT-LIB: distinct

    *)
  7. | Equal
    (*

    Equality.

    SMT-LIB: =

    *)
  8. | Iff
    (*

    Boolean if and only if.

    SMT-LIB: =

    *)
  9. | Implies
    (*

    Boolean implies.

    SMT-LIB: =>

    *)
  10. | Not
    (*

    Boolean not.

    SMT-LIB: not

    *)
  11. | Or
    (*

    Boolean or.

    SMT-LIB: or

    *)
  12. | Xor
    (*

    Boolean xor.

    SMT-LIB: xor

    *)
  13. | Ite
    (*

    If-then-else.

    SMT-LIB: ite

    *)
  14. | Exists
    (*

    Existential quantification.

    SMT-LIB: exists

    *)
  15. | Forall
    (*

    Universal quantification.

    SMT-LIB: forall

    *)
  16. | Apply
    (*

    Function application.

    *)
  17. | Lambda
    (*

    Lambda.

    *)
  18. | Select
    (*

    Array select.

    SMT-LIB: select

    *)
  19. | Store
    (*

    Array store.

    SMT-LIB: store

    *)
  20. | Bv_add
    (*

    Bit-vector addition.

    SMT-LIB: bvadd

    *)
  21. | Bv_and
    (*

    Bit-vector and.

    SMT-LIB: bvand

    *)
  22. | Bv_ashr
    (*

    Bit-vector arithmetic right shift.

    SMT-LIB: bvashr

    *)
  23. | Bv_comp
    (*

    Bit-vector comparison.

    SMT-LIB: bvcomp

    *)
  24. | Bv_concat
    (*

    Bit-vector concat.

    SMT-LIB: concat

    *)
  25. | Bv_dec
    (*

    Bit-vector decrement.

    Decrement by one.

    *)
  26. | Bv_inc
    (*

    Bit-vector increment.

    Increment by one.

    *)
  27. | Bv_mul
    (*

    Bit-vector multiplication.

    SMT-LIB: bvmul

    *)
  28. | Bv_nand
    (*

    Bit-vector nand.

    SMT-LIB: bvnand

    *)
  29. | Bv_neg
    (*

    Bit-vector negation (two's complement).

    SMT-LIB: bvneg

    *)
  30. | Bv_nego
    (*

    Bit-vector negation overflow test.

    Predicate indicating if bit-vector negation produces an overflow.

    SMT-LIB: bvnego

    *)
  31. | Bv_nor
    (*

    Bit-vector nor.

    SMT-LIB: bvnor

    *)
  32. | Bv_not
    (*

    Bit-vector not (one's complement).

    SMT-LIB: bvnot

    *)
  33. | Bv_or
    (*

    Bit-vector or.

    SMT-LIB: bvor

    *)
  34. | 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.

    *)
  35. | 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.

    *)
  36. | 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.

    *)
  37. | Bv_rol
    (*

    Bit-vector rotate left (not indexed).

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

    *)
  38. | Bv_ror
    (*

    Bit-vector rotate right.

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

    *)
  39. | Bv_saddo
    (*

    Bit-vector signed addition overflow test.

    Single bit to indicate if signed addition produces an overflow.

    *)
  40. | Bv_sdivo
    (*

    Bit-vector signed division overflow test.

    Single bit to indicate if signed division produces an overflow.

    *)
  41. | Bv_sdiv
    (*

    Bit-vector signed division.

    SMT-LIB: bvsdiv

    *)
  42. | Bv_sge
    (*

    Bit-vector signed greater than or equal.

    SMT-LIB: bvsge

    *)
  43. | Bv_sgt
    (*

    Bit-vector signed greater than.

    SMT-LIB: bvsgt

    *)
  44. | Bv_shl
    (*

    Bit-vector logical left shift.

    SMT-LIB: bvshl

    *)
  45. | Bv_shr
    (*

    Bit-vector logical right shift.

    SMT-LIB: bvshr

    *)
  46. | Bv_sle
    (*

    Bit-vector signed less than or equal.

    SMT-LIB: bvsle

    *)
  47. | Bv_slt
    (*

    Bit-vector signed less than.

    SMT-LIB: bvslt

    *)
  48. | Bv_smod
    (*

    Bit-vector signed modulo.

    SMT-LIB: bvsmod

    *)
  49. | Bv_smulo
    (*

    Bit-vector signed multiplication overflow test.

    SMT-LIB: bvsmod

    *)
  50. | Bv_srem
    (*

    Bit-vector signed remainder.

    SMT-LIB: bvsrem

    *)
  51. | Bv_ssubo
    (*

    Bit-vector signed subtraction overflow test.

    Single bit to indicate if signed subtraction produces an overflow.

    *)
  52. | Bv_sub
    (*

    Bit-vector subtraction.

    SMT-LIB: bvsub

    *)
  53. | Bv_uaddo
    (*

    Bit-vector unsigned addition overflow test.

    Single bit to indicate if unsigned addition produces an overflow.

    *)
  54. | Bv_udiv
    (*

    Bit-vector unsigned division.

    SMT-LIB: bvudiv

    *)
  55. | Bv_uge
    (*

    Bit-vector unsigned greater than or equal.

    SMT-LIB: bvuge

    *)
  56. | Bv_ugt
    (*

    Bit-vector unsigned greater than.

    SMT-LIB: bvugt

    *)
  57. | Bv_ule
    (*

    Bit-vector unsigned less than or equal.

    SMT-LIB: bvule

    *)
  58. | Bv_ult
    (*

    Bit-vector unsigned less than.

    SMT-LIB: bvult

    *)
  59. | Bv_umulo
    (*

    Bit-vector unsigned multiplication overflow test.

    Single bit to indicate if unsigned multiplication produces an overflow.

    *)
  60. | Bv_urem
    (*

    Bit-vector unsigned remainder.

    SMT-LIB: bvurem

    *)
  61. | Bv_usubo
    (*

    Bit-vector unsigned subtraction overflow test.

    Single bit to indicate if unsigned subtraction produces an overflow.

    *)
  62. | Bv_xnor
    (*

    Bit-vector xnor.

    SMT-LIB: bvxnor

    *)
  63. | Bv_xor
    (*

    Bit-vector xor.

    SMT-LIB: bvxor

    *)
  64. | Bv_extract
    (*

    Bit-vector extract.

    SMT-LIB: extract (indexed)

    *)
  65. | Bv_repeat
    (*

    Bit-vector repeat.

    SMT-LIB: repeat (indexed)

    *)
  66. | Bv_roli
    (*

    Bit-vector rotate left by integer.

    SMT-LIB: rotate_left (indexed)

    *)
  67. | Bv_rori
    (*

    Bit-vector rotate right by integer.

    SMT-LIB: rotate_right (indexed)

    *)
  68. | Bv_sign_extend
    (*

    Bit-vector sign extend.

    SMT-LIB: sign_extend (indexed)

    *)
  69. | Bv_zero_extend
    (*

    Bit-vector zero extend.

    SMT-LIB: zero_extend (indexed)

    *)
  70. | Fp_abs
    (*

    Floating-point absolute value.

    SMT-LIB: fp.abs

    *)
  71. | Fp_add
    (*

    Floating-point addition.

    SMT-LIB: fp.add

    *)
  72. | Fp_div
    (*

    Floating-point division.

    SMT-LIB: fp.div

    *)
  73. | Fp_equal
    (*

    Floating-point equality.

    SMT-LIB: fp.eq

    *)
  74. | Fp_fma
    (*

    Floating-point fused multiplcation and addition.

    SMT-LIB: fp.fma

    *)
  75. | Fp_fp
    (*

    Floating-point IEEE 754 value.

    SMT-LIB: fp

    *)
  76. | Fp_geq
    (*

    Floating-point greater than or equal.

    SMT-LIB: fp.geq

    *)
  77. | Fp_gt
    (*

    Floating-point greater than.

    SMT-LIB: fp.gt

    *)
  78. | Fp_is_inf
    (*

    Floating-point is infinity tester.

    SMT-LIB: fp.isInfinite

    *)
  79. | Fp_is_nan
    (*

    Floating-point is Nan tester.

    SMT-LIB: fp.isNaN

    *)
  80. | Fp_is_neg
    (*

    Floating-point is negative tester.

    SMT-LIB: fp.isNegative

    *)
  81. | Fp_is_normal
    (*

    Floating-point is normal tester.

    SMT-LIB: fp.isNormal

    *)
  82. | Fp_is_pos
    (*

    Floating-point is positive tester.

    SMT-LIB: fp.isPositive

    *)
  83. | Fp_is_subnormal
    (*

    Floating-point is subnormal tester.

    SMT-LIB: fp.isSubnormal

    *)
  84. | Fp_is_zero
    (*

    Floating-point is zero tester.

    SMT-LIB: fp.isZero

    *)
  85. | Fp_leq
    (*

    Floating-point less than or equal.

    SMT-LIB: fp.leq

    *)
  86. | Fp_lt
    (*

    Floating-point less than.

    SMT-LIB: fp.lt

    *)
  87. | Fp_max
    (*

    Floating-point max.

    SMT-LIB: fp.max

    *)
  88. | Fp_min
    (*

    Floating-point min.

    SMT-LIB: fp.min

    *)
  89. | Fp_mul
    (*

    Floating-point multiplcation.

    SMT-LIB: fp.mul

    *)
  90. | Fp_neg
    (*

    Floating-point negation.

    SMT-LIB: fp.neg

    *)
  91. | Fp_rem
    (*

    Floating-point remainder.

    SMT-LIB: fp.rem

    *)
  92. | Fp_rti
    (*

    Floating-point round to integral.

    SMT-LIB: fp.roundToIntegral

    *)
  93. | Fp_sqrt
    (*

    Floating-point round to square root.

    SMT-LIB: fp.sqrt

    *)
  94. | Fp_sub
    (*

    Floating-point round to subtraction.

    SMT-LIB: fp.sqrt

    *)
  95. | Fp_to_fp_from_bv
    (*

    Floating-point to_fp from IEEE 754 bit-vector.

    SMT-LIB: to_fp (indexed)

    *)
  96. | Fp_to_fp_from_fp
    (*

    Floating-point to_fp from floating-point.

    SMT-LIB: to_fp (indexed)

    *)
  97. | Fp_to_fp_from_sbv
    (*

    Floating-point to_fp from signed bit-vector value.

    SMT-LIB: to_fp (indexed)

    *)
  98. | Fp_to_fp_from_ubv
    (*

    Floating-point to_fp from unsigned bit-vector value.

    SMT-LIB: to_fp_unsigned (indexed)

    *)
  99. | Fp_to_sbv
    (*

    Floating-point to_sbv.

    SMT-LIB: fp.to_sbv (indexed)

    *)
  100. | Fp_to_ubv
    (*

    Floating-point to_ubv.

    SMT-LIB: fp.to_ubv (indexed)

    *)

The term kind.

Sourceval to_string : t -> string

to_string t get string representation of this kind.

  • returns

    String representation of this kind.