Add computations for fp.le|lt|ge|gt|eq

src_colibri2/tests/solve/smt_fp/sat/dune.inc

@@ -7,5 +7,7 @@
 (rule (alias runtest) (action (diff oracle recognize_rounding_mode.smt2.res)))
 (rule (action (with-stdout-to simple_add_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_add_float32.smt2}))))
 (rule (alias runtest) (action (diff oracle simple_add_float32.smt2.res)))
+(rule (action (with-stdout-to simple_eq_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_eq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle simple_eq_float32.smt2.res)))
 (rule (action (with-stdout-to simple_mul_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_mul_float32.smt2}))))
 (rule (alias runtest) (action (diff oracle simple_mul_float32.smt2.res)))

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

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

src_colibri2/theories/FP/float32.ml

@@ -47,6 +47,7 @@ let compute_ground d t =
   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
+  let (!<<) v = `Some (Boolean.BoolValue.nodevalue (Boolean.BoolValue.index v)) in
   match Ground.sem t with
   | { app = {builtin = Expr.Fp_add (8, 24); _}; args; _} ->
     let m, a, b = IArray.extract3_exn args in
@@ -64,6 +65,21 @@ let compute_ground d t =
     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)
+  | { app = {builtin = Expr.Fp_eq (8, 24); _}; args; _} ->
+    let a, b = IArray.extract2_exn args in
+    !<< (Farith.B32.eq !>a !>b)
+  | { app = {builtin = Expr.Fp_leq (8, 24); _}; args; _} ->
+    let a, b = IArray.extract2_exn args in
+    !<< (Farith.B32.le !>a !>b)
+  | { app = {builtin = Expr.Fp_lt (8, 24); _}; args; _} ->
+    let a, b = IArray.extract2_exn args in
+    !<< (Farith.B32.lt !>a !>b)
+  | { app = {builtin = Expr.Fp_geq (8, 24); _}; args; _} ->
+    let a, b = IArray.extract2_exn args in
+    !<< (Farith.B32.ge !>a !>b)
+  | { app = {builtin = Expr.Fp_gt (8, 24); _}; args; _} ->
+    let a, b = IArray.extract2_exn args in
+    !<< (Farith.B32.gt !>a !>b)
   | _ -> `None
 
 let init_check d = Interp.Register.check d (fun d t ->
@@ -155,6 +171,13 @@ let converter d (f:Ground.t) =
     List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a;b]
   in
   match Ground.sem f with
+  | {app={builtin=Expr.Fp_abs (8, 24); _}; args; _} ->
+    let a = IArray.extract1_exn args in
+    reg a; attach d f;
+    let wait =
+      set r (let+ va = get a in Farith.B32.abs va)
+    in
+    List.iter (fun n -> wait_for_this_node_get_a_value d n wait) [a; r]
   | {app={builtin=Expr.Fp_add (8, 24); _}; args; _} ->
     let m, a, b = IArray.extract3_exn args in
     reg m; reg a; reg b; attach d f;

src_colibri2/theories/FP/fp_value.mli

@@ -26,7 +26,7 @@ val posint_sequence : Z.t Base.Sequence.t
 (** Names (string) wrapped in a module *)
 module type FloatName = sig val name : string end
 
-(** 
+(**
    Helper to extend a module of type [Farith.S] into a module of
    type [ValueKind.Value]
 *)