/usr/share/why3/drivers/smt-libv2-bv-realization.gen is in why3 0.88.3-1ubuntu4.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 | (* Why3 driver checking compatibility of BV theories with SMT-LIB2 *)
theory bv.BV_Gen
syntax function bw_and "(bvand %1 %2)"
syntax function bw_or "(bvor %1 %2)"
syntax function bw_xor "(bvxor %1 %2)"
syntax function bw_not "(bvnot %1)"
syntax function add "(bvadd %1 %2)"
syntax function sub "(bvsub %1 %2)"
syntax function neg "(bvneg %1)"
syntax function mul "(bvmul %1 %2)"
syntax function udiv "(bvudiv %1 %2)"
syntax function urem "(bvurem %1 %2)"
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax predicate eq "(= %1 %2)"
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
syntax predicate sle "(bvsle %1 %2)"
syntax predicate sgt "(bvsgt %1 %2)"
syntax predicate sge "(bvsge %1 %2)"
(** Removing the axioms that should be proved instead
the one that are commented out are instead kept
*)
remove prop size_pos
remove prop nth_out_of_bound
remove prop Nth_zeros
remove prop Nth_ones
remove prop Nth_bw_and
remove prop Nth_bw_or
remove prop Nth_bw_xor
remove prop Nth_bw_not
remove prop Lsr_nth_low
remove prop Lsr_nth_high
remove prop lsr_zeros
remove prop Asr_nth_low
remove prop Asr_nth_high
remove prop asr_zeros
remove prop Lsl_nth_high
remove prop Lsl_nth_low
remove prop lsl_zeros
remove prop Nth_rotate_right
remove prop Nth_rotate_left
(* Conversions from/to integers *)
remove prop two_power_size_val
remove prop max_int_val
remove prop to_uint_extensionality
remove prop to_int_extensionality
remove prop to_uint_bounds
remove prop to_uint_of_int
remove prop to_uint_size_bv
remove prop to_uint_zeros
remove prop to_uint_ones
remove prop to_uint_one
(** Arithmetic operators *)
remove prop to_uint_add
remove prop to_uint_add_bounded
remove prop to_uint_sub
remove prop to_uint_sub_bounded
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_mul_bounded
remove prop to_uint_udiv
remove prop to_uint_urem
(* kept: Nth_bv_is_nth *)
(* kept: Nth_bv_is_nth2 *)
(* kept: lsr_bv_is_lsr *)
remove prop to_uint_lsr
(* kept: asr_bv_is_asr *)
(* kept: lsl_bv_is_lsl *)
remove prop to_uint_lsl
(* kept: rotate_left_bv_is_rotate_left *)
(* kept: rotate_right_bv_is_rotate_right *)
remove prop eq_sub_equiv
remove prop Extensionality
end
theory bv.BV64
syntax type t "(_ BitVec 64)"
syntax function zeros "#x0000000000000000"
syntax function ones "#xFFFFFFFFFFFFFFFF"
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 64)) (_ bv0 64)))"
(* possible alternative definition :
"(= ((_ extract 0 0) (bvlshr %1 %2)) (_ bv1 1))"
*)
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
end
theory bv.BV32
syntax type t "(_ BitVec 32)"
syntax function zeros "#x00000000"
syntax function ones "#xFFFFFFFF"
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 32)) (_ bv0 32)))"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
end
theory bv.BV16
syntax type t "(_ BitVec 16)"
syntax function zeros "#x0000"
syntax function ones "#xFFFF"
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 16)) (_ bv0 16)))"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
end
theory bv.BV8
syntax type t "(_ BitVec 8)"
syntax function zeros "#x00"
syntax function ones "#xFF"
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 8)) (_ bv0 8)))"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
end
theory bv.BVConverter_Gen
remove allprops
end
theory bv.BVConverter_32_64
syntax function toBig "((_ zero_extend 32) %1)"
syntax function toSmall "((_ extract 31 0) %1)"
end
theory bv.BVConverter_16_64
syntax function toBig "((_ zero_extend 48) %1)"
syntax function toSmall "((_ extract 15 0) %1)"
end
theory bv.BVConverter_8_64
syntax function toBig "((_ zero_extend 56) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
end
theory bv.BVConverter_16_32
syntax function toBig "((_ zero_extend 16) %1)"
syntax function toSmall "((_ extract 15 0) %1)"
end
theory bv.BVConverter_8_32
syntax function toBig "((_ zero_extend 24) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
end
theory bv.BVConverter_8_16
syntax function toBig "((_ zero_extend 8) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
end
theory bv.Pow2int
remove allprops
end
|