Add interpretation for fp.div fp.sub fp.mul fp.abs

src_colibri2/tests/solve/smt_fp/sat/simple_add_float32.smt2

 (set-logic ALL)
 (declare-fun x () (_ FloatingPoint 8 24))
 (declare-fun y () (_ FloatingPoint 8 24))
-(assert (= (fp.add RNE x y) (fp.add RNE x y)))
+(assert (= (fp.add RNE x y) x))
 (check-sat)
\ No newline at end of file

src_colibri2/tests/solve/smt_fp/sat/simple_mul_float32.smt2

+(set-logic ALL)
+(declare-fun x () (_ FloatingPoint 8 24))
+(declare-fun y () (_ FloatingPoint 8 24))
+(assert (= (fp.mul RNE x y) x))
+(check-sat)
\ No newline at end of file

src_colibri2/theories/FP/float32.ml

@@ -43,25 +43,26 @@ let init_ty d =
 let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
 
 let compute_ground d t =
-
-  (* let mode = function
-     | Expr.RoundNearestTiesToEven -> Farith.NE
-     | Expr.RoundNearestTiesToAway -> Farith.NA
-     | Expr.RoundTowardPositive    -> Farith.UP
-     | Expr.RoundTowardNegative    -> Farith.DN
-     | Expr.RoundTowardZero        -> Farith.ZR
-     | _                           -> raise Impossible
-     in *)
-
   let (!>>) t = Rounding_mode.value (Rounding_mode.coerce_nodevalue (interp d t )) in
   let (!>) t = Float32.value (Float32.coerce_nodevalue (interp d t)) in
   let (!<) v = `Some (Float32.nodevalue (Float32.index v)) in
-
   match Ground.sem t with
   | { app = {builtin = Expr.Fp_add (8, 24); _}; args; _} ->
-    (* TODO: get the mode *)
     let m, a, b = IArray.extract3_exn args in
     !< (Farith.B32.add !>>m !>a !>b)
+  | { app = {builtin = Expr.Fp_sub (8, 24); _}; args; _} ->
+    let m, a, b = IArray.extract3_exn args in
+    !< (Farith.B32.sub !>>m !>a !>b)
+  | { app = {builtin = Expr.Fp_mul (8, 24); _}; args; _} ->
+    let m, a, b = IArray.extract3_exn args in
+    !< (Farith.B32.mul !>>m !>a !>b)
+  | { app = {builtin = Expr.Fp_abs (8, 24); _}; args; _} ->
+    let a = IArray.extract1_exn args in
+    !< (Farith.B32.abs !>a)
+  | { app = {builtin = Expr.Fp_div (8, 24); _}; args; _} ->
+    let m, a, b = IArray.extract3_exn args in
+    if Farith.B32.(eq !>b (zero true) || eq !>b (zero false)) then `Uninterp
+    else !< (Farith.B32.div !>>m !>a !>b)
   | _ -> `None
 
 let init_check d = Interp.Register.check d (fun d t ->
@@ -71,6 +72,9 @@ let init_check d = Interp.Register.check d (fun d t ->
     match compute_ground d t with
     | `None -> None
     | `Some v -> Some (check v)
+    | `Uninterp ->
+      (* TODO : Give the control to the Uniterpreted Symbols theory *)
+      None
   )
 
 let init env =

src_colibri2/theories/FP/fp.ml

@@ -25,6 +25,12 @@ let converter d f =
   match Ground.sem f with
   | { app = {builtin = Expr.Fp_add (_, _); _}; args; _ } ->
     IArray.iter ~f:reg args
+  | { app = {builtin = Expr.Fp_sub (_, _); _}; args; _ } ->
+    IArray.iter ~f:reg args
+  | { app = {builtin = Expr.Fp_div (_, _); _}; args; _ } ->
+    IArray.iter ~f:reg args
+  | { app = {builtin = Expr.Fp_mul (_, _); _}; args; _ } ->
+    IArray.iter ~f:reg args
   | _ -> ()
 
 let th_register env =

src_colibri2/theories/FP/fp_value.ml

@@ -53,4 +53,3 @@ let posint_sequence_without_zero =
 (** Generate the sequence of positive integers (without 0) *)
 let posint_sequence =
   Base.Sequence.shift_right posint_sequence_without_zero Z.zero
-

src_colibri2/theories/FP/rounding_mode.ml

@@ -82,7 +82,7 @@ let init_ty d =
 
 let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
 
-let compute_ground _ t =
+let compute_cst t =
   let (!<) v = `Some (Modes.nodevalue (Modes.index v)) in
   match Ground.sem t with
   | { app = {builtin = Expr.RoundNearestTiesToEven; _}; _} ->
@@ -101,7 +101,7 @@ let init_check d = Interp.Register.check d (fun d t ->
     let check r =
       Value.equal r (interp d (Ground.node t))
     in
-    match compute_ground d t with
+    match compute_cst t with
     | `None -> None
     | `Some v -> Some (check v)
   )