Add fp.fma operator

Author: filipeom

src/smtml/bitwuzla_mappings.default.ml

@@ -386,6 +386,8 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
 
     let max t1 t2 = mk_term2 Kind.Fp_max t1 t2
 
+    let fma ~rm a b c = mk_term Kind.Fp_fma [| rm; a; b; c |]
+
     let rem t1 t2 = mk_term2 Kind.Fp_rem t1 t2
 
     let eq t1 t2 = mk_term2 Kind.Fp_equal t1 t2

src/smtml/cvc5_mappings.default.ml

@@ -373,6 +373,8 @@ module Fresh_cvc5 () = struct
 
     let max t1 t2 = Term.mk_term tm Kind.Floatingpoint_max [| t1; t2 |]
 
+    let fma ~rm a b c = Term.mk_term Kind.Floatingpoint_fma [| rm; a; b; c |]
+
     let rem t1 t2 = Term.mk_term tm Kind.Floatingpoint_rem [| t1; t2 |]
 
     let eq t1 t2 = Term.mk_term tm Kind.Floatingpoint_eq [| t1; t2 |]

src/smtml/dolmenexpr_to_expr.ml

@@ -325,6 +325,8 @@ module DolmenIntf = struct
 
     let div ~rm t1 t2 = DTerm.Float.div rm t1 t2
 
+    let fma ~rm a b c = DTerm.Float.fma rm a b c
+
     let le = DTerm.Float.leq
 
     let ge = DTerm.Float.geq

src/smtml/dolmenexpr_to_expr.mli

@@ -302,6 +302,8 @@ module DolmenIntf : sig
 
     val rem : term -> term -> term
 
+    val fma : rm:term -> term -> term -> term -> term
+
     val eq : term -> term -> term
 
     val lt : term -> term -> term

src/smtml/mappings.ml

@@ -699,6 +699,12 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         let ctx, b = encode_expr ctx b in
         let rm = get_rounding_mode rm in
         (ctx, M.Float.div ~rm a b)
+      | App ({ name = Simple "fp.fma"; _ }, [ rm; a; b; c ]) ->
+        let ctx, a = encode_expr ctx a in
+        let ctx, b = encode_expr ctx b in
+        let ctx, c = encode_expr ctx c in
+        let rm = get_rounding_mode rm in
+        (ctx, M.Float.fma ~rm a b c)
       | App ({ name = Simple "fp.sqrt"; _ }, [ rm; a ]) ->
         let ctx, a = encode_expr ctx a in
         let rm = get_rounding_mode rm in

src/smtml/mappings.nop.ml

@@ -299,6 +299,8 @@ module Nop = struct
 
       let rem _ = assert false
 
+      let fma ~rm:_ = assert false
+
       let eq _ = assert false
 
       let lt _ = assert false

src/smtml/mappings_intf.ml

@@ -527,6 +527,9 @@ module type M = sig
         [t2]. *)
     val max : term -> term -> term
 
+    (** [fma ~rm a b c] *)
+    val fma : rm:term -> term -> term -> term -> term
+
     (** [rem t1 t2] constructs the remainder of the floating-point terms [t1]
         and [t2]. *)
     val rem : term -> term -> term

src/smtml/rewrite.ml

@@ -28,6 +28,11 @@ let rewrite_ty unknown_ty tys =
     debug "  rewrite_ty: %a %a@." (fun k -> k Ty.pp ty1 Ty.pp ty2);
     assert (Ty.equal ty1 ty2);
     ty1
+  | Ty_none, ty1 :: ty2 :: [ ty3 ] ->
+    debug "  rewrite_ty: %a %a %a@." (fun k -> k Ty.pp ty1 Ty.pp ty2 Ty.pp ty3);
+    assert (Ty.equal ty1 ty2);
+    assert (Ty.equal ty2 ty3);
+    ty1
   | Ty_none, _ -> assert false
   | ty, _ -> ty
 
@@ -54,6 +59,12 @@ let rec rewrite_expr (type_map, expr_map) hte =
     let b = rewrite_expr (type_map, expr_map) b in
     let ty = rewrite_ty Ty_none [ Expr.ty a; Expr.ty b ] in
     Expr.app { sym with ty } [ rm; a; b ]
+  | App (({ name = Simple "fp.fma"; _ } as sym), [ rm; a; b; c ]) ->
+    let a = rewrite_expr (type_map, expr_map) a in
+    let b = rewrite_expr (type_map, expr_map) b in
+    let c = rewrite_expr (type_map, expr_map) c in
+    let ty = rewrite_ty Ty_none [ Expr.ty a; Expr.ty b; Expr.ty c ] in
+    Expr.app { sym with ty } [ rm; a; b; c ]
   | App
       ( ({ name = Simple ("fp.sqrt" | "fp.roundToIntegral"); _ } as sym)
       , [ rm; a ] ) ->

src/smtml/z3_mappings.default.ml

@@ -363,6 +363,8 @@ module M = struct
 
       let max e1 e2 = Z3.FloatingPoint.mk_max ctx e1 e2
 
+      let fma ~rm a b c = Z3.FloatingPoint.mk_fma ctx rm a b c
+
       let rem e1 e2 = Z3.FloatingPoint.mk_rem ctx e1 e2
 
       let eq e1 e2 = Z3.FloatingPoint.mk_eq ctx e1 e2