Commit d01e5acf authored by MARCHE Claude's avatar MARCHE Claude

add missing fil

parent 73e40c8c
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
have the same name for the function to_int *)
theory bv.BV64
syntax type t "(_ BitVec 64)"
syntax function zero "#x0000000000000000"
syntax function ones "#xFFFFFFFFFFFFFFFF"
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 converter of_int "(_ bv%1 64)"
syntax function to_uint "(bv2nat %1)"
remove prop to_uint_of_int
remove prop to_uint_extensionality
remove prop to_uint_bounds
syntax predicate eq "(= %1 %2)"
remove prop Extensionality
remove prop to_uint_add
remove prop to_uint_sub
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop to_uint_lsr
remove prop to_uint_lsl
remove prop Nth_zero
remove prop Nth_ones
remove prop Nth_bw_or
remove prop Nth_bw_and
remove prop Nth_bw_xor
remove prop Nth_bw_not
remove prop Nth_rotate_left
remove prop Nth_rotate_right
remove prop Nth_bv_is_nth
remove prop Lsr_nth_low
remove prop Lsr_nth_high
remove prop Asr_nth_low
remove prop Asr_nth_high
remove prop Lsl_nth_low
remove prop Lsl_nth_high
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)"
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 64)) (_ bv0 64)))"
syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
syntax function rotate_right "(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 zero "#x00000000"
syntax function ones "#xFFFFFFFF"
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 converter of_int "(_ bv%1 32)"
syntax function to_uint "(bv2nat %1)"
remove prop to_uint_of_int
remove prop to_uint_extensionality
remove prop to_uint_bounds
syntax predicate eq "(= %1 %2)"
remove prop Extensionality
remove prop to_uint_add
remove prop to_uint_sub
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop to_uint_lsr
remove prop to_uint_lsl
remove prop Nth_zero
remove prop Nth_ones
remove prop Nth_bw_or
remove prop Nth_bw_and
remove prop Nth_bw_xor
remove prop Nth_bw_not
remove prop Nth_rotate_left
remove prop Nth_rotate_right
remove prop Nth_bv_is_nth
remove prop Lsr_nth_low
remove prop Lsr_nth_high
remove prop Asr_nth_low
remove prop Asr_nth_high
remove prop Lsl_nth_low
remove prop Lsl_nth_high
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)"
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 32)) (_ bv0 32)))"
syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
syntax function rotate_right "(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 zero "#x0000"
syntax function ones "#xFFFF"
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 converter of_int "(_ bv%1 16)"
syntax function to_uint "(bv2nat %1)"
remove prop to_uint_of_int
remove prop to_uint_extensionality
remove prop to_uint_bounds
syntax predicate eq "(= %1 %2)"
remove prop Extensionality
remove prop to_uint_add
remove prop to_uint_sub
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop to_uint_lsr
remove prop to_uint_lsl
remove prop Nth_zero
remove prop Nth_ones
remove prop Nth_bw_or
remove prop Nth_bw_and
remove prop Nth_bw_xor
remove prop Nth_bw_not
remove prop Nth_rotate_left
remove prop Nth_rotate_right
remove prop Nth_bv_is_nth
remove prop Lsr_nth_low
remove prop Lsr_nth_high
remove prop Asr_nth_low
remove prop Asr_nth_high
remove prop Lsl_nth_low
remove prop Lsl_nth_high
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)"
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 16)) (_ bv0 16)))"
syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
syntax function rotate_right "(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 zero "#x00"
syntax function ones "#xFF"
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 converter of_int "(_ bv%1 8)"
syntax function to_uint "(bv2nat %1)"
remove prop to_uint_of_int
remove prop to_uint_extensionality
remove prop to_uint_bounds
syntax predicate eq "(= %1 %2)"
remove prop Extensionality
remove prop to_uint_add
remove prop to_uint_sub
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop to_uint_lsr
remove prop to_uint_lsl
remove prop Nth_zero
remove prop Nth_ones
remove prop Nth_bw_or
remove prop Nth_bw_and
remove prop Nth_bw_xor
remove prop Nth_bw_not
remove prop Nth_rotate_left
remove prop Nth_rotate_right
remove prop Nth_bv_is_nth
remove prop Lsr_nth_low
remove prop Lsr_nth_high
remove prop Asr_nth_low
remove prop Asr_nth_high
remove prop Lsl_nth_low
remove prop Lsl_nth_high
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)"
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 8)) (_ bv0 8)))"
syntax function rotate_left "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
syntax function rotate_right "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
end
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment