Print bitvectors and fps in hexadecimal

By printing bitvectors and fps in hexadecimal
we provide a more faithful representation of the
underlying value representation of the value.

lib/num.ml

@@ -55,17 +55,11 @@ let type_of (n : t) =
 
 let pp fmt (n : t) =
   match n with
-  | I8 i -> Format.fprintf fmt "(i8 %d)" i
-  | I32 i -> Format.fprintf fmt "(i32 %ld)" i
-  | I64 i -> Format.fprintf fmt "(i64 %Ld)" i
-  | F32 f -> Format.fprintf fmt "(f32 %F)" (Int32.float_of_bits f)
-  | F64 f -> Format.fprintf fmt "(f64 %F)" (Int64.float_of_bits f)
-
-let pp_hex fmt (n : t) =
-  match n with
-  | I8 i -> Format.fprintf fmt "0x%x" i
-  | I32 i | F32 i -> Format.fprintf fmt "0x%lx" i
-  | I64 i | F64 i -> Format.fprintf fmt "0x%Lx" i
+  | I8 i -> Format.fprintf fmt "0x%02x" (i land 0xff)
+  | I32 i -> Format.fprintf fmt "0x%08lx" i
+  | I64 i -> Format.fprintf fmt "0x%016Lx" i
+  | F32 f -> Format.fprintf fmt "(fp 0x%08lx)" f
+  | F64 f -> Format.fprintf fmt "(fp 0x%16Lx)" f
 
 let to_string (n : t) : string = Format.asprintf "%a" pp n
 

lib/num.mli

@@ -31,8 +31,6 @@ val type_of : t -> Ty.t
 
 val pp : Format.formatter -> t -> unit
 
-val pp_hex : Format.formatter -> t -> unit
-
 val to_string : t -> string
 
 val num_of_bool : bool -> t

lib/value.ml

@@ -84,7 +84,4 @@ let rec pp fmt (v : t) =
       vs
   | _ -> assert false
 
-let pp_num fmt (v : t) =
-  match v with Num x -> Num.pp_hex fmt x | _ -> pp fmt v
-
 let to_string v = Format.asprintf "%a" pp v

lib/value.mli

@@ -34,6 +34,4 @@ val type_of : t -> Ty.t
 
 val pp : Format.formatter -> t -> unit
 
-val pp_num : Format.formatter -> t -> unit
-
 val to_string : t -> string

test/parser/test_qf_fp.t

@@ -4,20 +4,20 @@ Test fp parsing:
   sat
   sat
   (model
-    (v (f32 -0.))
-    (w (f32 -0.))
-    (x (f32 0.504000008106))
-    (z (f32 1.)))
+    (v (fp 0x80000000))
+    (w (fp 0x80000000))
+    (x (fp 0x3f010625))
+    (z (fp 0x3f800000)))
   sat
   (model
-    (v (f32 -2.))
-    (w (f32 -3.))
-    (x (f32 -2.70000004768))
-    (z (f32 -2.)))
+    (v (fp 0xc0000000))
+    (w (fp 0xc0400000))
+    (x (fp 0xc02ccccd))
+    (z (fp 0xc0000000)))
   sat
   (model
-    (r (f64 infinity))
-    (s (f64 -3.38460706455e+125))
-    (u (f64 nan))
-    (x (f32 -2.70000004768))
-    (y (f64 314159265359.)))
+    (r (fp 0x7ff0000000000000))
+    (s (fp 0xda00000028000800))
+    (u (fp 0x7ff8000000000001))
+    (x (fp 0xc02ccccd))
+    (y (fp 0x425249567d93c000)))

test/test_z3.expected

@@ -1,5 +1,5 @@
 (model
-  (w (i32 4))
-  (x (i32 1))
-  (y (i32 2))
-  (z (i32 3)))
+  (w 0x00000004)
+  (x 0x00000001)
+  (y 0x00000002)
+  (z 0x00000003))