Add floating-point operator Copysign (Closes #185)

src/eval.ml

@@ -681,6 +681,7 @@ module F32 = struct
       | Rem -> Float.rem
       | Min -> Float.min
       | Max -> Float.max
+      | Copysign -> Float.copy_sign
       | _ ->
         Fmt.failwith {|binop: Unsupported f32 operator "%a"|} Ty.Binop.pp op
     in
@@ -743,6 +744,7 @@ module F64 = struct
       | Rem -> Float.rem
       | Min -> Float.min
       | Max -> Float.max
+      | Copysign -> Float.copy_sign
       | _ ->
         Fmt.failwith {|binop: Unsupported f32 operator "%a"|} Ty.Binop.pp op
     in

src/mappings.ml

@@ -431,6 +431,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
 
       val sb : int
 
+      val zero : unit -> M.term
+
       val v : elt -> M.term
       (* TODO: *)
       (* val to_string : Z3.FuncDecl.func_decl *)
@@ -451,8 +453,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         | Floor -> Float.round_to_integral ~rm:Float.Rounding_mode.rtn e
         | Trunc -> Float.round_to_integral ~rm:Float.Rounding_mode.rtz e
         | Nearest -> Float.round_to_integral ~rm:Float.Rounding_mode.rne e
-        | _ ->
-          Fmt.failwith {|Fp: Unsupported Z3 unary operator "%a"|} Unop.pp op
+        | _ -> Fmt.failwith {|Fp: Unsupported unary operator "%a"|} Unop.pp op
 
       let binop op e1 e2 =
         match op with
@@ -463,11 +464,13 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         | Min -> Float.min e1 e2
         | Max -> Float.max e1 e2
         | Rem -> Float.rem e1 e2
-        | _ ->
-          Fmt.failwith {|Fp: Unsupported Z3 binop operator "%a"|} Binop.pp op
+        | Copysign ->
+          let abs_float = Float.abs e1 in
+          M.ite (Float.ge e2 (F.zero ())) abs_float (Float.neg abs_float)
+        | _ -> Fmt.failwith {|Fp: Unsupported binop operator "%a"|} Binop.pp op
 
       let triop op _ =
-        Fmt.failwith {|Fp: Unsupported Z3 triop operator "%a"|} Triop.pp op
+        Fmt.failwith {|Fp: Unsupported triop operator "%a"|} Triop.pp op
 
       let relop op e1 e2 =
         match op with
@@ -477,8 +480,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         | Le -> Float.le e1 e2
         | Gt -> Float.gt e1 e2
         | Ge -> Float.ge e1 e2
-        | _ ->
-          Fmt.failwith {|Fp: Unsupported Z3 relop operator "%a"|} Relop.pp op
+        | _ -> Fmt.failwith {|Fp: Unsupported relop operator "%a"|} Relop.pp op
 
       let cvtop op e =
         match op with
@@ -495,8 +497,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         | OfString ->
           (* TODO: FuncDecl.apply of_string [ e ] *)
           assert false
-        | _ ->
-          Fmt.failwith {|Fp: Unsupported Z3 cvtop operator "%a"|} Cvtop.pp op
+        | _ -> Fmt.failwith {|Fp: Unsupported cvtop operator "%a"|} Cvtop.pp op
     end
 
     module Float32_impl = Float_impl (struct
@@ -508,6 +509,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
 
       let v f = M.Float.v (Int32.float_of_bits f) eb sb
 
+      let zero () = v (Int32.bits_of_float 0.0)
+
       (* TODO: *)
       (* let to_string = *)
       (*   Z3.FuncDecl.mk_func_decl_s ctx "F32ToString" [ fp32_sort ] str_sort *)
@@ -524,6 +527,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
 
       let v f = M.Float.v (Int64.float_of_bits f) eb sb
 
+      let zero () = v (Int64.bits_of_float 0.0)
+
       (* TODO: *)
       (* let to_string = *)
       (*   Z3.FuncDecl.mk_func_decl_s ctx "F64ToString" [ fp64_sort ] str_sort *)

src/ty.ml

@@ -187,6 +187,7 @@ module Binop = struct
     | Pow
     | Min
     | Max
+    | Copysign
     | Rotl
     | Rotr
     | At
@@ -219,6 +220,7 @@ module Binop = struct
     | Pow, Pow
     | Min, Min
     | Max, Max
+    | Copysign, Copysign
     | Rotl, Rotl
     | Rotr, Rotr
     | At, At
@@ -232,7 +234,7 @@ module Binop = struct
     | Regexp_range, Regexp_range ->
       true
     | ( ( Add | Sub | Mul | Div | DivU | Rem | RemU | Shl | ShrA | ShrL | And
-        | Or | Xor | Pow | Min | Max | Rotl | Rotr | At | List_cons
+        | Or | Xor | Pow | Min | Max | Copysign | Rotl | Rotr | At | List_cons
         | List_append | String_prefix | String_suffix | String_contains
         | String_last_index | String_in_re | Regexp_range )
       , _ ) ->
@@ -255,6 +257,7 @@ module Binop = struct
     | Pow -> Fmt.string fmt "pow"
     | Min -> Fmt.string fmt "min"
     | Max -> Fmt.string fmt "max"
+    | Copysign -> Fmt.string fmt "copysign"
     | Rotl -> Fmt.string fmt "rotl"
     | Rotr -> Fmt.string fmt "rotr"
     | At -> Fmt.string fmt "at"

src/ty.mli

@@ -82,6 +82,7 @@ module Binop : sig
     | Pow
     | Min
     | Max
+    | Copysign
     | Rotl
     | Rotr
     | At

test/solver/test_fp.ml

@@ -31,4 +31,21 @@ module Make (M : Mappings_intf.S) = struct
     Solver.add solver F32.[ Expr.unop (Ty_fp 32) Sqrt x = F32.v 2.0 ];
     assert_sat (Solver.check solver []);
     assert (Expr.equal (Solver.get_value solver x) (F32.v 4.0))
+
+  (* Copysign *)
+  let () =
+    let solver = Solver.create ~logic:QF_BVFP () in
+    let x = F32.sym "x" in
+    let y = F32.sym "y" in
+    Solver.add solver F32.[ x > v 0.0; y < v 0.0 ];
+    Solver.add solver F32.[ Expr.binop (Ty_fp 32) Copysign x y < v 0.0 ];
+    assert_sat (Solver.check solver [])
+
+  let () =
+    let solver = Solver.create ~logic:QF_BVFP () in
+    let x = F64.sym "x" in
+    let y = F64.sym "y" in
+    Solver.add solver F64.[ x > v 0.0; y < v 0.0 ];
+    Solver.add solver F64.[ Expr.binop (Ty_fp 64) Copysign x y < v 0.0 ];
+    assert_sat (Solver.check solver [])
 end

test/unit/test_binop.ml

@@ -19,6 +19,10 @@ let int32 x = value (Num (I32 x))
 
 let int64 x = value (Num (I64 x))
 
+let float32 x = value (Num (F32 (Int32.bits_of_float x)))
+
+let float64 x = value (Num (F64 (Int64.bits_of_float x)))
+
 let list x = value (List x)
 
 (* int *)
@@ -105,6 +109,22 @@ let () =
   assert (binop (Ty_bitv 64) Rotl (int64 Int64.min_int) (int64 2L) = int64 2L);
   assert (binop (Ty_bitv 64) Rotr (int64 2L) (int64 2L) = int64 Int64.min_int)
 
+(* f32 *)
+let () =
+  let ty = Ty_fp 32 in
+  assert (binop ty Copysign (float32 (-4.2)) (float32 2.0) = float32 4.2);
+  assert (binop ty Copysign (float32 4.2) (float32 (-2.0)) = float32 (-4.2));
+  assert (binop ty Copysign (float32 4.2) (float32 2.0) = float32 4.2);
+  assert (binop ty Copysign (float32 (-4.2)) (float32 (-2.0)) = float32 (-4.2))
+
+(* f64 *)
+let () =
+  let ty = Ty_fp 64 in
+  assert (binop ty Copysign (float64 (-4.2)) (float64 2.0) = float64 4.2);
+  assert (binop ty Copysign (float64 4.2) (float64 (-2.0)) = float64 (-4.2));
+  assert (binop ty Copysign (float64 4.2) (float64 2.0) = float64 4.2);
+  assert (binop ty Copysign (float64 (-4.2)) (float64 (-2.0)) = float64 (-4.2))
+
 (* ptr *)
 let () =
   let p0 = ptr 0l (int32 0l) in