Commit 73e40c8c authored by MARCHE Claude's avatar MARCHE Claude

fix mistakes in renaming bitvec to bv

parent c1a8a7bb
......@@ -64,280 +64,4 @@ theory int.ComputerDivision
end
*)
(* 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
import "cvc4_bv.gen"
......@@ -16,7 +16,7 @@ prelude "(set-logic AUFBVDTLIRA)"
prelude ";; Enable model construction"
prelude "(set-option :produce-models true)"
(* Counterexamples: makes it possible to get rid of more quantifiers while introducing premises *)
(* Counterexamples: makes it possible to get rid of more quantifiers while introducing premises *)
(* transformation "split_intro" *)
(* Counterexamples: get rid of some quantifiers - makes it possible to query model values of the variables in premises *)
......@@ -27,6 +27,7 @@ transformation "intro_projections_counterexmp"
model_parser "cvc4_z3"
import "smt-libv2.drv"
import "smt-libv2-bv.gen"
import "discrimination.gen"
transformation "inline_trivial"
......@@ -77,264 +78,4 @@ theory int.ComputerDivision
end
*)
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
have the same name for the function to_int *)
theory bitvec.BitVector64
syntax type t "(_ BitVec 64)"
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 "(bvlshr %1 %2)"
syntax function lsl "(bvshl %1 %2)"
syntax function asr "(bvashr %1 %2)"
syntax converter of_int "(_ bv%1 64)"
syntax function to_int "(bv2nat %1)"
remove prop to_int_of_int
remove prop to_int_extensionality
remove prop to_int_bounds
syntax predicate eq "(= %1 %2)"
remove prop Extensionality
remove prop to_int_add
remove prop to_int_sub
remove prop to_int_neg
remove prop to_int_mul
remove prop to_int_udiv
remove prop to_int_urem
remove prop to_int_lsr
remove prop to_int_lsl
remove prop nth_ext
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 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 function nth
"(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 bitvec.BitVector32
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 "(bvlshr %1 %2)"
syntax function lsl "(bvshl %1 %2)"
syntax function asr "(bvashr %1 %2)"
syntax converter of_int "(_ bv%1 32)"
syntax function to_int "(bv2nat %1)"
remove prop to_int_of_int
remove prop to_int_extensionality
remove prop to_int_bounds
syntax predicate eq "(= %1 %2)"
remove prop Extensionality
remove prop to_int_add
remove prop to_int_sub
remove prop to_int_neg
remove prop to_int_mul
remove prop to_int_udiv
remove prop to_int_urem
remove prop to_int_lsr
remove prop to_int_lsl
remove prop nth_ext
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 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 function nth
"(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 bitvec.BitVector16
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 "(bvlshr %1 %2)"
syntax function lsl "(bvshl %1 %2)"
syntax function asr "(bvashr %1 %2)"
syntax converter of_int "(_ bv%1 16)"
syntax function to_int "(bv2nat %1)"
remove prop to_int_of_int
remove prop to_int_extensionality
remove prop to_int_bounds
syntax predicate eq "(= %1 %2)"
remove prop Extensionality
remove prop to_int_add
remove prop to_int_sub
remove prop to_int_neg
remove prop to_int_mul
remove prop to_int_udiv
remove prop to_int_urem
remove prop to_int_lsr
remove prop to_int_lsl
remove prop nth_ext
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 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 function nth
"(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 bitvec.BitVector8
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 "(bvlshr %1 %2)"
syntax function lsl "(bvshl %1 %2)"
syntax function asr "(bvashr %1 %2)"
syntax converter of_int "(_ bv%1 8)"
syntax function to_int "(bv2nat %1)"
remove prop to_int_of_int
remove prop to_int_extensionality
remove prop to_int_bounds
syntax predicate eq "(= %1 %2)"
remove prop Extensionality
remove prop to_int_add
remove prop to_int_sub
remove prop to_int_neg
remove prop to_int_mul
remove prop to_int_udiv
remove prop to_int_urem
remove prop to_int_lsr
remove prop to_int_lsl
remove prop nth_ext
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 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 function nth
"(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
import "cvc4_bv.gen"
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