Commit 6b6e68e3 authored by MARCHE Claude's avatar MARCHE Claude

removed remaining converters from drivers

parent 2c88c700
......@@ -138,8 +138,7 @@ module matrix.Matrix
end
module mach.int.Int31
syntax val of_int "(fun x -> x)"
syntax converter of_int "%1"
syntax val of_int "%1"
syntax function to_int "(%1)"
......@@ -157,8 +156,7 @@ module mach.int.Int31
syntax val (>) "(>)"
end
module mach.int.Int63
syntax val of_int "(fun x -> x)"
syntax converter of_int "%1"
syntax val of_int "%1"
syntax function to_int "(%1)"
......@@ -234,4 +232,3 @@ module mach.matrix.Matrix63
syntax val make "Array.make_matrix"
syntax val copy "(Array.map Array.copy)"
end
......@@ -206,7 +206,6 @@ module mach.int.Int63
syntax type int63 "int"
syntax literal int63 "%1"
syntax converter of_int "%1"
syntax val of_int "Z.to_int %1"
syntax val to_int "Z.of_int %1"
......@@ -311,8 +310,6 @@ module mach.onetime.OneTime
syntax val eq "%1 = %2"
syntax val ne "%1 <> %2"
syntax converter to_peano "%1"
syntax val transfer "%1"
syntax val neg "-%1"
syntax val abs "abs %1"
......
......@@ -76,30 +76,3 @@ theory real.Trigonometry
end
*)
(* REMOVED: we do not use BV theory from Z3 in 4.3.2 but starting from 4.4.0
(* bitvector modules, is not in smt-libv2.gen since cvc4 and z3 don't
have the same name for the function to_uint *)
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_uint "(bv2int %1)"
end
*)
\ No newline at end of file
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