Print floats in OCaml syntax (Closes #49)

lib/num.ml

@@ -26,8 +26,8 @@ let pp fmt (n : t) =
   | 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)
+  | 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

lib/value.ml

@@ -26,14 +26,14 @@ let type_of (v : t) : Ty.t =
   | Num n -> Num.type_of n
 
 let pp fmt (v : t) =
-  let pp_string = Format.pp_print_string in
+  let open Format in
   match v with
-  | True -> pp_string fmt "true"
-  | False -> pp_string fmt "false"
-  | Int x -> pp_string fmt @@ Int.to_string x
-  | Real x -> pp_string fmt @@ Float.to_string x
+  | True -> pp_print_string fmt "true"
+  | False -> pp_print_string fmt "false"
+  | Int x -> pp_print_int fmt x
+  | Real x -> fprintf fmt "%F" x
   | Num x -> Num.pp fmt x
-  | Str x -> Format.fprintf fmt {|"%s"|} x
+  | Str x -> Format.fprintf fmt "%S" x
 
 let pp_num fmt (v : t) =
   match v with Num x -> Num.pp_hex fmt x | _ -> pp fmt v

test/test_qf_bvfp.expected

@@ -0,0 +1,6 @@
+(model
+  (y f64 (f64 nan))
+  (z f64 (f64 infinity))
+  (w f64 (f64 -3.38460706455e+125))
+  (v f64 (f64 1.))
+  (x f64 (f64 314159265359.)))

test/test_qf_bvfp.ml

@@ -1,6 +1,8 @@
 open Encoding
 open Expr
 module Z3 = Solver.Z3_batch
+module F32 = Fpa.F32
+module F64 = Fpa.F64
 
 let () =
   let module I8 = Bitv.I8 in
@@ -16,32 +18,42 @@ let () =
   let not_nan = Unop (Not, Unop (Is_nan, x) @: Ty_fp S32) @: Ty_bool in
   let is_nan = Unop (Is_nan, x) @: Ty_fp S32 in
   assert (not @@ Z3.check solver [ not_nan; is_nan ]);
-  let nan = Val (Num (F32 (Int32.bits_of_float nan))) @: Ty_fp S32 in
-  let ne_nan = Relop (Ne, x, nan) @: Ty_fp S32 in
+  let ne_nan = Relop (Ne, x, F32.v nan) @: Ty_fp S32 in
   assert (Z3.check solver [ ne_nan; is_nan ])
 
 let () =
   let solver = Z3.create ~logic:QF_BVFP () in
-  let x = mk_symbol Symbol.("x" @: Ty_fp S32) in
-  let const = Val (Num (F32 (Int32.bits_of_float 50.0))) @: Ty_fp S32 in
-  assert (Z3.check solver [ Relop (Eq, x, const) @: Ty_fp S32 ]);
+  let x = F32.sym "x" in
+  let const = F32.v 50.0 in
+  assert (Z3.check solver F32.[ x = const ]);
   assert (Z3.get_value solver x = const);
-  let solver = Z3.create ~logic:QF_BVFP () in
-  let x = mk_symbol Symbol.("x" @: Ty_fp S64) in
-  let const = Val (Num (F64 (Int64.bits_of_float 50.0))) @: Ty_fp S64 in
-  assert (Z3.check solver [ Relop (Eq, x, const) @: Ty_fp S64 ]);
+  let x = F64.sym "x" in
+  let const = F64.v 50.0 in
+  assert (Z3.check solver F64.[ x = const ]);
   assert (Z3.get_value solver x = const)
 
 let () =
   let solver = Z3.create ~logic:QF_BVFP () in
-  let x = mk_symbol Symbol.("x" @: Ty_fp S32) in
-  let zero = Val (Num (F32 (Int32.bits_of_float 0.0))) @: Ty_fp S32 in
-  let one = Val (Num (F32 (Int32.bits_of_float 1.0))) @: Ty_fp S32 in
-  let half = Val (Num (F32 (Int32.bits_of_float 0.504))) @: Ty_fp S32 in
-  Z3.add solver [ Relop (Eq, x, half) @: Ty_fp S32 ];
-  assert (
-    Z3.check solver
-      [ Relop (Eq, Unop (Ty.Ceil, x) @: Ty_fp S32, one) @: Ty_fp S32 ] );
-  assert (
-    Z3.check solver
-      [ Relop (Eq, Unop (Ty.Floor, x) @: Ty_fp S32, zero) @: Ty_fp S32 ] )
+  let x = F32.sym "x" in
+  let zero = F32.v 0.0 in
+  let one = F32.v 1.0 in
+  let half = F32.v 0.504 in
+  Z3.add solver F32.[ x = half ];
+  assert (Z3.check solver F32.[ one = Unop (Ceil, x) @: Ty_fp S32 ]);
+  assert (Z3.check solver F32.[ zero = Unop (Floor, x) @: Ty_fp S32 ])
+
+let () =
+  let solver = Z3.create ~logic:QF_BVFP () in
+  Z3.add solver F64.[ sym "x" = v 314159265359.000 ];
+  Z3.add solver F64.[ Unop (Is_nan, sym "y") @: Ty_fp S64 ];
+  Z3.add solver F64.[ sym "z" = Binop (Div, v 1.0, v 0.0) @: Ty_fp S64 ];
+  let big_float =
+    F64.v
+      (-338460706455329128135018695364373065576360054171204343201037173805357995568625611429596369334345869072216864991017687935090688.000000
+      )
+  in
+  Z3.add solver F64.[ sym "w" = big_float ];
+  Z3.add solver F64.[ sym "v" = v 1.0 ];
+  assert (Z3.check solver []);
+  let model = Z3.model solver in
+  Option.iter (Model.pp Format.std_formatter) model