Fix the printing of bit-vectors and floating-point numbers

src/smtml/bitvector.ml

@@ -51,11 +51,28 @@ let to_int64 v =
     Fmt.failwith "call to Smtml.Bitvector.to_int32 on a bitvector of size %d"
       v.width
 
+type printer =
+  [ `Pretty  (** Human-readable format. *)
+  | `WithType  (** Print with type info. *)
+  ]
+
 (** Bitvector pretty printer. By default it prints signed bitvectors. *)
-let pp fmt bv =
+let pp_bv fmt bv =
   let value = to_signed bv in
   Z.pp_print fmt value
 
+let pp_wtype fmt bv =
+  let value = to_signed bv in
+  Fmt.pf fmt "(i%d %a)" bv.width Z.pp_print value
+
+let printer = ref pp_bv
+
+let set_default_printer = function
+  | `Pretty -> printer := pp_bv
+  | `WithType -> printer := pp_wtype
+
+let pp fmt e = !printer fmt e
+
 (* Unop *)
 let neg bv = make (Z.neg bv.value) bv.width
 

src/smtml/bitvector.mli

@@ -22,7 +22,17 @@ val equal : t -> t -> bool
 
 val compare : t -> t -> int
 
-val pp : Format.formatter -> t -> unit
+(** Representation options for value printing. *)
+type printer =
+  [ `Pretty  (** Human-readable format. *)
+  | `WithType  (** Print with type info. *)
+  ]
+
+(** [set_default_printer p] sets the default printer format for displaying
+    values. *)
+val set_default_printer : printer -> unit
+
+val pp : t Fmt.t
 
 val neg : t -> t
 

src/smtml/expr.ml

@@ -221,20 +221,27 @@ let rec pp fmt (hte : t) =
 let pp_list fmt (es : t list) = Fmt.hovbox (Fmt.list ~sep:Fmt.comma pp) fmt es
 
 let pp_smtml fmt (es : t list) : unit =
+  let def_num_printer = Num.get_default_printer () in
+  Num.set_default_printer `Hexadecimal;
+  Bitvector.set_default_printer `WithType;
   let pp_symbols fmt syms =
-    Fmt.list
+    Fmt.list ~sep:Fmt.cut
       (fun fmt sym ->
         let t = Symbol.type_of sym in
         Fmt.pf fmt "(let-const %a %a)" Symbol.pp sym Ty.pp t )
       fmt syms
   in
   let pp_asserts fmt es =
-    Fmt.list (fun fmt e -> Fmt.pf fmt "(assert @[<h 2>%a@])" pp e) fmt es
+    Fmt.list ~sep:Fmt.cut
+      (fun fmt e -> Fmt.pf fmt "(assert @[<h 2>%a@])" pp e)
+      fmt es
   in
   let syms = get_symbols es in
-  if List.length syms > 0 then Fmt.pf fmt "%a@\n" pp_symbols syms;
-  if List.length es > 0 then Fmt.pf fmt "%a@\n" pp_asserts es;
-  Fmt.string fmt "(check-sat)"
+  if List.length syms > 0 then Fmt.pf fmt "@[<v>%a@]@\n" pp_symbols syms;
+  if List.length es > 0 then Fmt.pf fmt "@[<v>%a@]@\n" pp_asserts es;
+  Fmt.string fmt "(check-sat)";
+  Num.set_default_printer def_num_printer;
+  Bitvector.set_default_printer `Pretty
 
 let to_string e = Fmt.str "%a" pp e
 

src/smtml/lexer.mll

@@ -269,8 +269,8 @@ let character = ['a'-'z' 'A'-'Z']
 let digits = '0' | [ '1'-'9' ] digit*
 let numeral = '-'? digits
 let decimal = '-'? digits '.' digit*
-let hexadec = "#x" (['a'-'f' 'A'-'F'] | digit)+
-let binary = "#b" ('0' | '1')+
+let hexadec = "0x" (['a'-'f' 'A'-'F'] | digit)+
+let binary = "0b" ('0' | '1')+
 let bool = "true" | "false"
 
 let symbols = ['~''!''@''$''%''^''&''*''_''-''+''=''<''>''.''?''/']
@@ -282,6 +282,8 @@ rule token = parse
   | ')' { RPAREN }
 
   | "nan" { DEC Float.nan }
+  | "inf" { DEC Float.infinity }
+  | "-inf" { DEC Float.neg_infinity }
   | numeral as s {
     match int_of_string_opt s with
     | Some i -> NUM i
@@ -293,7 +295,7 @@ rule token = parse
     | None -> assert false
   }
   | bool as s { BOOL (String.equal s "true") }
-  | hexadec { Fmt.failwith "TODO: Lexer(hexadec)" }
+  | hexadec as s { HEX s }
   | binary { Fmt.failwith "TODO: Lexer(binary)" }
   | '"' { string (Buffer.create 17) lexbuf }
 

src/smtml/num.ml

@@ -9,6 +9,7 @@ type t =
 type printer =
   [ `Pretty
   | `Hexadecimal
+  | `NoType
   ]
 
 let type_of (n : t) =
@@ -30,20 +31,24 @@ let pp_num fmt = function
   | F64 f -> Fmt.pf fmt "(f64 %F)" (Int64.float_of_bits f)
 
 let pp_hex fmt = function
-  | F32 f -> Fmt.pf fmt "(fp 0x%08lx)" f
-  | F64 f -> Fmt.pf fmt "(fp 0x%016Lx)" f
+  | F32 f -> Fmt.pf fmt "(f32 0x%08lx)" f
+  | F64 f -> Fmt.pf fmt "(f64 0x%016Lx)" f
 
 let pp_no_type fmt = function
   | F32 f -> Fmt.pf fmt "%F" (Int32.float_of_bits f)
   | F64 f -> Fmt.pf fmt "%F" (Int64.float_of_bits f)
 
-let printer = ref pp_num
+let printer = ref `NoType
 
-let set_default_printer = function
-  | `Pretty -> printer := pp_num
-  | `Hexadecimal -> printer := pp_hex
+let set_default_printer : printer -> unit = ( := ) printer
 
-let pp fmt v = !printer fmt v
+let get_default_printer () : printer = !printer
+
+let pp fmt v =
+  match !printer with
+  | `Pretty -> pp_num fmt v
+  | `Hexadecimal -> pp_hex fmt v
+  | `NoType -> pp_no_type fmt v
 
 let to_string (n : t) : string = Fmt.str "%a" pp n
 

src/smtml/num.mli

@@ -18,6 +18,7 @@ type t =
 type printer =
   [ `Pretty  (** Human-readable format. *)
   | `Hexadecimal  (** Hexadecimal representation. *)
+  | `NoType  (** Human-readable format with no type information. *)
   ]
 
 (** [type_of v] returns the type of the given value [v]. *)
@@ -38,6 +39,9 @@ val equal : t -> t -> bool
     values. *)
 val set_default_printer : printer -> unit
 
+(** [set_default_printer ()] gets the default printer. *)
+val get_default_printer : unit -> printer
+
 (** [pp] is a formatter for values of type [t], using the currently set printer.
 *)
 val pp : t Fmt.t

src/smtml/parser.mly

@@ -26,6 +26,7 @@ let get_bind x = Hashtbl.find_opt varmap x
 
 %token <int> NUM
 %token <float> DEC
+%token <string> HEX
 %token <bool> BOOL
 %token <string> STR
 %token <string> SYMBOL
@@ -104,3 +105,12 @@ let spec_constant :=
       | Ty_fp 64 -> Num (F64 (Int64.bits_of_float x))
       | _ -> Fmt.failwith "invalid fp type"
     }
+  | LPAREN; ty = TYPE; x = HEX; RPAREN;
+    {
+      match ty with
+      | Ty_bitv 32 -> Bitv (Bitvector.of_int32 (Int32.of_string x))
+      | Ty_bitv 64 -> Bitv (Bitvector.of_int64 (Int64.of_string x))
+      | Ty_fp 32 -> Num (F32 (Int32.of_string x))
+      | Ty_fp 64 -> Num (F64 (Int64.of_string x))
+      | _ -> Fmt.failwith "invalid type"
+    }

src/smtml/value.ml

@@ -89,7 +89,7 @@ let rec pp fmt = function
   | Unit -> Fmt.string fmt "unit"
   | Int x -> Fmt.int fmt x
   | Real x -> Fmt.pf fmt "%F" x
-  | Num x -> Num.pp_no_type fmt x
+  | Num x -> Num.pp fmt x
   | Bitv bv -> Bitvector.pp fmt bv
   | Str x -> Fmt.pf fmt "%S" x
   | List l -> (Fmt.hovbox ~indent:1 (Fmt.list ~sep:Fmt.comma pp)) fmt l

test/cli/smtml/test_qf_bv.smtml

@@ -0,0 +1,25 @@
+(let-const x i32)
+(let-const y i32)
+
+(assert (=
+  (i64.mul (i64.extend_i32_s y) (i64.extend_i32_s x))
+  (i64.add
+    (bool.ite
+      (bool.eq
+        (i64.and (i64.extend_i32_s y) (i64 9223372036))
+        (i64 1))
+        (i64.extend_i32_s x) (i64 0))
+    (i64.mul
+      (i64.div_s
+        (i64.sub
+          (i64.extend_i32_s y)
+          (i64.extend_i32_u
+            (i32.of_bool
+              (bool.eq
+                (i64.and (i64.extend_i32_s y) (i64 -36854775807))
+                (i64 1)))))
+        (i64 2))
+      (i64.shl (i64.extend_i32_s x) (i64 1))))
+))
+
+(check-sat)