Support FPA literals {+|-}{inf,zero} and NaN

Author: filipeom

src/smtml/logic.ml

@@ -11,6 +11,7 @@ type t =
   | QF_AX
   | QF_BV
   | QF_BVFP
+  | QF_FP
   | QF_IDL
   | QF_LIA
   | QF_LRA
@@ -40,6 +41,7 @@ let pp fmt = function
   | QF_AX -> Fmt.string fmt "QF_AX"
   | QF_BV -> Fmt.string fmt "QF_BV"
   | QF_BVFP -> Fmt.string fmt "QF_BVFP"
+  | QF_FP -> Fmt.string fmt "QF_FP"
   | QF_IDL -> Fmt.string fmt "QF_IDL"
   | QF_LIA -> Fmt.string fmt "QF_LIA"
   | QF_LRA -> Fmt.string fmt "QF_LRA"
@@ -70,6 +72,7 @@ let of_string logic =
   | "QF_AX" -> Ok QF_AX
   | "QF_BV" -> Ok QF_BV
   | "QF_BVFP" -> Ok QF_BVFP
+  | "QF_FP" -> Ok QF_FP
   | "QF_IDL" -> Ok QF_IDL
   | "QF_LIA" -> Ok QF_LIA
   | "QF_LRA" -> Ok QF_LRA

src/smtml/logic.mli

@@ -30,6 +30,7 @@ type t =
   | QF_AX  (** Quantifier-free array theory. *)
   | QF_BV  (** Quantifier-free bitvector theory. *)
   | QF_BVFP  (** Quantifier-free bitvectors and floating-point arithmetic. *)
+  | QF_FP  (** Quantifier-free floating-point arithmetic. *)
   | QF_IDL  (** Quantifier-free integer difference logic. *)
   | QF_LIA  (** Quantifier-free linear integer arithmetic. *)
   | QF_LRA  (** Quantifier-free linear real arithmetic. *)

src/smtml/rewrite.ml

@@ -23,12 +23,12 @@ let debug fmt k = if debug then k (Fmt.epr fmt)
 let rewrite_ty unknown_ty tys =
   debug "  rewrite_ty: %a@." (fun k -> k Ty.pp unknown_ty);
   match (unknown_ty, tys) with
-  | Ty.Ty_none, [ ty ] -> ty
-  | Ty.Ty_none, [ ty1; ty2 ] ->
+  | Ty_none, [ ty ] -> ty
+  | Ty_none, [ ty1; ty2 ] ->
     debug "  rewrite_ty: %a %a@." (fun k -> k Ty.pp ty1 Ty.pp ty2);
     assert (Ty.equal ty1 ty2);
     ty1
-  | Ty.Ty_none, _ -> assert false
+  | Ty_none, _ -> assert false
   | ty, _ -> ty
 
 (** Propagates types in [type_map] and inlines [Let_in] binders *)

src/smtml/smtlib.ml

@@ -12,9 +12,22 @@ let pp_loc fmt = function
   | None -> ()
   | Some loc -> Fmt.pf fmt "%a: " Loc.print_compact loc
 
+let z_of_string_opt str =
+  match Z.of_string str with
+  | exception Invalid_argument _ -> None
+  | z -> Some z
+
 module Term = struct
   type t = Expr.t
 
+  let fp_of_size f ebits sbits =
+    match (ebits, sbits) with
+    | "8", "24" -> Expr.value (Num (F32 (Int32.bits_of_float f)))
+    | "11", "53" -> Expr.value (Num (F64 (Int64.bits_of_float f)))
+    | _ ->
+      Fmt.failwith "fp_of_size: unsupported %a (fp %a %a)" Fmt.float f
+        Fmt.string ebits Fmt.string sbits
+
   let const ?loc (id : Symbol.t) : t =
     match (Symbol.namespace id, Symbol.name id) with
     | Sort, Simple name -> (
@@ -50,15 +63,24 @@ module Term = struct
       | "true" -> Expr.value True
       | "false" -> Expr.value False
       | _ -> Expr.symbol id )
-    | Term, Indexed { basename = base; indices } -> (
-      match String.(sub base 0 2, sub base 2 (length base - 2), indices) with
-      | "bv", str, [ numbits ] -> begin
-        match (int_of_string_opt str, int_of_string_opt numbits) with
-        | Some n, Some width ->
-          Expr.value (Bitv (Bitvector.make (Z.of_int n) width))
+    | Term, Indexed { basename = base; indices } -> begin
+      match (base, indices) with
+      | bv, [ numbits ] when String.starts_with ~prefix:"bv" bv -> begin
+        let str = String.sub bv 2 (String.length bv - 2) in
+        match (z_of_string_opt str, int_of_string_opt numbits) with
+        | Some z, Some width -> Expr.value (Bitv (Bitvector.make z width))
         | (None | Some _), _ -> assert false
       end
-      | _ -> Expr.symbol id )
+      | "+oo", [ ebits; sbits ] -> fp_of_size Float.infinity ebits sbits
+      | "-oo", [ ebits; sbits ] -> fp_of_size Float.neg_infinity ebits sbits
+      | "+zero", [ ebits; sbits ] -> fp_of_size Float.zero ebits sbits
+      | "-zero", [ ebits; sbits ] ->
+        fp_of_size (Float.neg Float.zero) ebits sbits
+      | "NaN", [ ebits; sbits ] -> fp_of_size Float.nan ebits sbits
+      | _ ->
+        Log.debug (fun k -> k "const: Unknown %a making app" Symbol.pp id);
+        Expr.symbol id
+    end
     | Attr, Simple _ -> Expr.symbol id
     | Attr, Indexed _ -> assert false
     | Var, _ -> Fmt.failwith "%acould not parse var: %a" pp_loc loc Symbol.pp id
@@ -94,6 +116,7 @@ module Term = struct
     match Expr.view symbol with
     | Symbol s ->
       (* Hack: var bindings are 1 argument lambdas *)
+      Log.debug (fun k -> k "colon: unknown '%a' making app" Expr.pp symbol);
       Expr.app s [ term ]
     | _ ->
       Fmt.failwith "%acould not parse colon: %a %a" pp_loc loc Expr.pp symbol
@@ -257,8 +280,11 @@ module Term = struct
       | "fp.geq", [ a; b ] -> Expr.raw_relop Ty_bool Ge a b
       | "fp.gt", [ a; b ] -> Expr.raw_relop Ty_bool Gt a b
       | "fp.eq", [ a; b ] -> Expr.raw_relop Ty_bool Eq a b
-      | _, l -> Expr.app symbol l )
+      | _, l ->
+        Log.debug (fun k -> k "apply: unknown %a making app" Symbol.pp symbol);
+        Expr.app symbol l )
     | Symbol ({ name = Simple _; namespace = Attr; _ } as attr) ->
+      Log.debug (fun k -> k "apply: unknown %a making app" Symbol.pp attr);
       Expr.app attr args
     | Symbol { name = Indexed { basename; indices }; _ } -> (
       match (basename, indices, args) with
@@ -291,7 +317,9 @@ module Term = struct
         Expr.raw_unop Ty_regexp (Regexp_loop (i1, i2)) a
       | _ ->
         Fmt.failwith "%acould not parse indexed app: %a" pp_loc loc Expr.pp id )
-    | Symbol id -> Expr.app id args
+    | Symbol id ->
+      Log.debug (fun k -> k "apply: unknown %a making app" Symbol.pp id);
+      Expr.app id args
     | _ ->
       (* Ids can only be symbols. Any other expr here is super wrong *)
       assert false

test/cli/smt2/dune

@@ -13,6 +13,7 @@
   test_exists.smt2
   test_forall.smt2
   test_fp.smt2
+  test_fp_literals.smt2
   test_lia.smt2
   test_lra.smt2
   test_string_all.smt2

test/cli/smt2/test_fp_literals.smt2

@@ -0,0 +1,16 @@
+(set-logic QF_FP)
+
+(declare-fun pos_inf () (_ FloatingPoint 8 24))
+(declare-fun neg_inf () (_ FloatingPoint 8 24))
+(declare-fun pos_zero () (_ FloatingPoint 8 24))
+(declare-fun neg_zero () (_ FloatingPoint 8 24))
+(declare-fun nan_val () (_ FloatingPoint 8 24))
+
+(assert (= pos_inf (_ +oo 8 24)))
+(assert (= neg_inf (_ -oo 8 24)))
+(assert (= pos_zero (_ +zero 8 24)))
+(assert (= neg_zero (_ -zero 8 24)))
+(assert (= nan_val (_ NaN 8 24)))
+
+(check-sat)
+(get-model)

test/cli/smt2/test_smt2.t

@@ -53,6 +53,14 @@ Test BitVector parsing:
 Test FloatingPoint parsing:
   $ smtml run test_fp.smt2
   sat
+  $ smtml run test_fp_literals.smt2
+  sat
+  (model
+    (nan_val f32 nan)
+    (neg_inf f32 neg_infinity)
+    (neg_zero f32 -0.)
+    (pos_inf f32 infinity)
+    (pos_zero f32 0.))
 
 Tests smt2 with the --from-file argument:
   $ cat <<EOF > test.list