Add SMTLIB parsing for FPs

src/bitwuzla_mappings.default.ml

@@ -64,6 +64,10 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
 
   let or_ t1 t2 = mk_term2 Kind.Or t1 t2
 
+  let logand ts = mk_term Kind.And (Array.of_list ts)
+
+  let logor ts = mk_term Kind.Or (Array.of_list ts)
+
   let xor t1 t2 = mk_term2 Kind.Xor t1 t2
 
   let eq t1 t2 = mk_term2 Kind.Equal t1 t2

src/cvc5_mappings.default.ml

@@ -54,6 +54,10 @@ module Fresh_cvc5 () = struct
 
   let or_ t1 t2 = Term.mk_term tm Kind.Or [| t1; t2 |]
 
+  let logand ts = Term.mk_term tm Kind.And (Array.of_list ts)
+
+  let logor ts = Term.mk_term tm Kind.Or (Array.of_list ts)
+
   let xor t1 t2 = Term.mk_term tm Kind.Xor [| t1; t2 |]
 
   let eq t1 t2 = Term.mk_term tm Kind.Equal [| t1; t2 |]
@@ -182,11 +186,9 @@ module Fresh_cvc5 () = struct
     let is_suffix t1 ~suffix =
       Term.mk_term tm Kind.String_suffix [| t1; suffix |]
 
-    let lt _ =
-      Fmt.failwith "Cvc5_mappings: String.lt not implemented"
+    let lt _ = Fmt.failwith "Cvc5_mappings: String.lt not implemented"
 
-    let le _ =
-      Fmt.failwith "Cvc5_mappings: String.le not implemented"
+    let le _ = Fmt.failwith "Cvc5_mappings: String.le not implemented"
 
     let sub s ~pos ~len = Term.mk_term tm Kind.String_substr [| s; pos; len |]
 

src/mappings.ml

@@ -120,6 +120,14 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
           Fmt.failwith {|Bool: Unsupported Z3 relop operator "%a"|} Ty.pp_relop
             op
 
+      let naryop op l =
+        match op with
+        | Logand -> M.logand l
+        | Logor -> M.logor l
+        | _ ->
+          Fmt.failwith {|Bool: Unsupported Z3 naryop operator "%a"|}
+            Ty.pp_naryop op
+
       let cvtop _op _e = assert false
     end
 
@@ -584,6 +592,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
 
     let naryop = function
       | Ty.Ty_str -> String_impl.naryop
+      | Ty.Ty_bool -> Bool_impl.naryop
       | ty -> Fmt.failwith "Naryop for type \"%a\" not implemented" Ty.pp ty
 
     let rec encode_expr ctx (hte : Expr.t) : symbol_ctx * M.term =

src/mappings.nop.ml

@@ -50,6 +50,10 @@ module Nop = struct
 
     let or_ _ = assert false
 
+    let logand _ = assert false
+
+    let logor _ = assert false
+
     let xor _ = assert false
 
     let eq _ = assert false

src/mappings_intf.ml

@@ -55,6 +55,10 @@ module type M = sig
 
   val or_ : term -> term -> term
 
+  val logand : term list -> term
+
+  val logor : term list -> term
+
   val xor : term -> term -> term
 
   val eq : term -> term -> term

src/parser/smtlib.ml

@@ -16,13 +16,19 @@ module Term = struct
       | "Real" -> Expr.symbol { id with ty = Ty_real }
       | "Bool" -> Expr.symbol { id with ty = Ty_bool }
       | "String" -> Expr.symbol { id with ty = Ty_str }
+      | "Float32" -> Expr.symbol { id with ty = Ty_fp 32 }
+      | "Float64" -> Expr.symbol { id with ty = Ty_fp 64 }
       | _ -> Fmt.failwith "Could not parse sort: %a" Symbol.pp id )
     | Sort, Indexed { basename; indices } -> (
       match (basename, indices) with
       | "BitVec", [ n ] -> (
         match int_of_string n with
         | Some n -> Expr.symbol { id with ty = Ty_bitv n }
         | None -> Fmt.failwith "Invalid bitvector size" )
+      | "FloatingPoint", [ e; s ] -> (
+        match (int_of_string e, int_of_string s) with
+        | Some e, Some s -> Expr.symbol { id with ty = Ty_fp (e + s) }
+        | _ -> Fmt.failwith "Invalid floating point size" )
       | _ ->
         Fmt.failwith "%acould not parse indexed sort:%a %a@." pp_loc loc
           Fmt.string basename
@@ -60,7 +66,14 @@ module Term = struct
 
   let hexa ?loc:_ (_ : string) = assert false
 
-  let binary ?loc:_ (_ : string) = assert false
+  let binary ?loc:_ (b : string) =
+    let set (s : string) (i : int) (n : char) =
+      let bs = Bytes.of_string s in
+      Bytes.set bs i n;
+      Bytes.to_string bs
+    in
+    let bv = set b 0 '0' in
+    Expr.value (Str bv)
 
   let colon ?loc (symbol : t) (term : t) : t =
     match Expr.view symbol with
@@ -71,6 +84,22 @@ module Term = struct
       Fmt.failwith "%acould not parse colon: %a %a" pp_loc loc Expr.pp symbol
         Expr.pp term
 
+  let combine_to_int64 sign_bit exponent_bit mantissa_bit =
+    let sign = Int64.of_string sign_bit in
+    let exponent = Int64.of_string exponent_bit in
+    let mantissa = Int64.of_string mantissa_bit in
+    let sign_shifted = Int64.shift_left sign 63 in
+    let exponent_shifted = Int64.shift_left exponent 52 in
+    Int64.logor sign_shifted (Int64.logor exponent_shifted mantissa)
+
+  let combine_to_int32 sign_bit exponent_bit mantissa_bit =
+    let sign = Int32.of_string sign_bit in
+    let exponent = Int32.of_string exponent_bit in
+    let mantissa = Int32.of_string mantissa_bit in
+    let sign_shifted = Int32.shift_left sign 31 in
+    let exponent_shifted = Int32.shift_left exponent 23 in
+    Int32.logor sign_shifted (Int32.logor exponent_shifted mantissa)
+
   let apply ?loc (id : t) (args : t list) : t =
     match Expr.view id with
     | Symbol { namespace = Term; name = Simple name; _ } -> (
@@ -131,6 +160,71 @@ module Term = struct
       | "bvsge", [ a; b ] -> Expr.relop' Ty_none Ge a b
       | "bvuge", [ a; b ] -> Expr.relop' Ty_none GeU a b
       | "concat", [ a; b ] -> Expr.concat' a b
+      | "fp", [ s; e; m ] -> (
+        match (Expr.view s, Expr.view e, Expr.view m) with
+        | Val (Str s'), Val (Str e'), Val (Str m') -> (
+          match (String.length s', String.length e', String.length m') with
+          | 3, 10, 25 -> Expr.value (Num (F32 (combine_to_int32 s' e' m')))
+          | 3, 13, 54 -> Expr.value (Num (F64 (combine_to_int64 s' e' m')))
+          | _ -> Fmt.failwith "%afp size not supported" pp_loc loc )
+        | _ ->
+          Fmt.failwith "%acould not parse fp: %a %a %a" pp_loc loc Expr.pp s
+            Expr.pp e Expr.pp m )
+      | "fp.abs", [ a ] -> Expr.unop' Ty_none Abs a
+      | "fp.neg", [ a ] -> Expr.unop' Ty_none Neg a
+      | ( "fp.add"
+        , [ { node = Symbol { name = Simple "roundNearestTiesToEven"; _ }; _ }
+          ; a
+          ; b
+          ] ) ->
+        Expr.binop' Ty_none Add a b
+      | ( "fp.sub"
+        , [ { node = Symbol { name = Simple "roundNearestTiesToEven"; _ }; _ }
+          ; a
+          ; b
+          ] ) ->
+        Expr.binop' Ty_none Sub a b
+      | ( "fp.mul"
+        , [ { node = Symbol { name = Simple "roundNearestTiesToEven"; _ }; _ }
+          ; a
+          ; b
+          ] ) ->
+        Expr.binop' Ty_none Mul a b
+      | ( "fp.div"
+        , [ { node = Symbol { name = Simple "roundNearestTiesToEven"; _ }; _ }
+          ; a
+          ; b
+          ] ) ->
+        Expr.binop' Ty_none Div a b
+      | ( "fp.sqrt"
+        , [ { node = Symbol { name = Simple "roundNearestTiesToEven"; _ }; _ }
+          ; a
+          ] ) ->
+        Expr.unop' Ty_none Sqrt a
+      | "fp.rem", [ a; b ] -> Expr.binop' Ty_none Rem a b
+      | ( "fp.roundToIntegral"
+        , [ { node = Symbol { name = Simple "roundNearestTiesToEven"; _ }; _ }
+          ; a
+          ] ) ->
+        Expr.unop' Ty_none Nearest a
+      | ( "fp.roundToIntegral"
+        , [ { node = Symbol { name = Simple "roundTowardPositive"; _ }; _ }; a ]
+        ) ->
+        Expr.unop' Ty_none Ceil a
+      | ( "fp.roundToIntegral"
+        , [ { node = Symbol { name = Simple "roundTowardNegative"; _ }; _ }; a ]
+        ) ->
+        Expr.unop' Ty_none Floor a
+      | ( "fp.roundToIntegral"
+        , [ { node = Symbol { name = Simple "roundTowardZero"; _ }; _ }; a ] )
+        ->
+        Expr.unop' Ty_none Trunc a
+      | "fp.min", [ a; b ] -> Expr.binop' Ty_none Min a b
+      | "fp.max", [ a; b ] -> Expr.binop' Ty_none Max a b
+      | "fp.leq", [ a; b ] -> Expr.relop' Ty_bool Le a b
+      | "fp.lt", [ a; b ] -> Expr.relop' Ty_bool Lt a b
+      | "fp.geq", [ a; b ] -> Expr.relop' Ty_bool Ge a b
+      | "fp.gt", [ a; b ] -> Expr.relop' Ty_bool Gt a b
       | _ -> Fmt.failwith "%acould not parse term app: %s" pp_loc loc name )
     | Symbol ({ name = Simple _; namespace = Attr; _ } as attr) ->
       Expr.app attr args

src/z3_mappings.default.ml

@@ -59,6 +59,10 @@ module M = struct
 
     let or_ e1 e2 = Boolean.mk_or ctx [ e1; e2 ]
 
+    let logand es = Boolean.mk_and ctx es
+
+    let logor es = Boolean.mk_or ctx es
+
     let xor e1 e2 = Boolean.mk_xor ctx e1 e2
 
     let eq e1 e2 = Boolean.mk_eq ctx e1 e2

test/smt2/dune

@@ -10,6 +10,7 @@
   test_core_const.smt2
   test_core_true.smt2
   test_empty.smt2
+  test_fp.smt2
   test_lia.smt2
   test_lra.smt2
   test_string_all.smt2

test/smt2/test_fp.smt2

@@ -0,0 +1,16 @@
+(set-logic QF_FP)
+(set-info :status unsat)
+(declare-fun x () Float64)
+(declare-fun y () Float64)
+(declare-fun r () Float64)
+(declare-fun u () (_ FloatingPoint 8 24))
+(assert (= x (fp #b0 #b01011100111 #b1111110000101111001101101000100010000000100100100111)))
+(assert (= r (fp #b0 #b01101110011 #b0110100010101111111010000110100110010010111011011000)))
+(assert
+  (let ((?x2 (fp #b0 #b10000000 #b00000000000000000000000)))
+  (let ((?x4 (fp #b0 #b10000001 #b00000000000000000000000)))
+  (= (fp.sqrt roundNearestTiesToEven ?x4) ?x2))))
+(assert (not (= (fp.max x y) r)))
+(assert (not (= (fp.add roundNearestTiesToEven x y) r)))
+(check-sat)
+(exit)

test/smt2/test_smt2.t

@@ -49,3 +49,7 @@ Test BitVector parsing:
   sat
   $ smtml run test_bitv_funs.smt2
   sat
+
+Test FloatingPoint parsing:
+  $ smtml run test_fp.smt2
+  sat