Support for FP constants as defined in smtlib2

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

 (rule (action (with-stdout-to oracle (echo "sat\n"))))
+(rule (action (with-stdout-to inf_pos_neg_neq_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:inf_pos_neg_neq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle inf_pos_neg_neq_float32.smt2.res)))
+(rule (action (with-stdout-to infm_eq_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:infm_eq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle infm_eq_float32.smt2.res)))
+(rule (action (with-stdout-to infp_eq_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:infp_eq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle infp_eq_float32.smt2.res)))
+(rule (action (with-stdout-to nan_neq_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:nan_neq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle nan_neq_float32.smt2.res)))
 (rule (action (with-stdout-to recognize_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:recognize_float32.smt2}))))
 (rule (alias runtest) (action (diff oracle recognize_float32.smt2.res)))
 (rule (action (with-stdout-to recognize_float64.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:recognize_float64.smt2}))))
@@ -11,3 +19,9 @@
 (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)))
+(rule (action (with-stdout-to zero_pos_neg_neq_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:zero_pos_neg_neq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle zero_pos_neg_neq_float32.smt2.res)))
+(rule (action (with-stdout-to zerom_eq_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:zerom_eq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle zerom_eq_float32.smt2.res)))
+(rule (action (with-stdout-to zerop_eq_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:zerop_eq_float32.smt2}))))
+(rule (alias runtest) (action (diff oracle zerop_eq_float32.smt2.res)))

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

+(set-logic ALL)
+(assert (not (fp.eq (_ +oo 8 24) (_ -oo 8 24))))
+(check-sat)
\ No newline at end of file

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

+(set-logic ALL)
+(assert (fp.eq (_ -oo 8 24) (_ -oo 8 24)))
+(check-sat)
\ No newline at end of file

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

+(set-logic ALL)
+(assert (fp.eq (_ +oo 8 24) (_ +oo 8 24)))
+(check-sat)
\ No newline at end of file

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

+(set-logic ALL)
+(assert (not (fp.eq (_ NaN 8 24) (_ NaN 8 24))))
+(check-sat)
\ No newline at end of file

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

+(set-logic ALL)
+(assert (fp.eq (_ +zero 8 24) (_ -zero 8 24)))
+(check-sat)
\ No newline at end of file

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

+(set-logic ALL)
+(assert (fp.eq (_ -zero 8 24) (_ -zero 8 24)))
+(check-sat)
\ No newline at end of file

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

+(set-logic ALL)
+(assert (fp.eq (_ +zero 8 24) (_ +zero 8 24)))
+(check-sat)
\ No newline at end of file

src_colibri2/theories/FP/dune

@@ -10,6 +10,7 @@
   colibri2.theories.helpers
   colibri2.core.structures
   colibri2.theories.bool
+  colibri2.theories.LRA
   colibri2.theories.LRA.stages
   colibri2.theories.quantifiers
   colibri2.core)

src_colibri2/theories/FP/float32.ml

@@ -19,6 +19,7 @@
 (*************************************************************************)
 
 open Fp_value
+open Colibri2_theories_LRA
 open Colibri2_popop_lib
 
 
@@ -49,11 +50,30 @@ let init_ty d =
 let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
 
 let compute_ground d t =
-  let (!>>) t = Rounding_mode.value (Rounding_mode.coerce_nodevalue (interp d t )) in
+  let (!>>>) t = RealValue.value (RealValue.coerce_nodevalue (interp d t)) 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
   let (!<<) v = `Some (Boolean.BoolValue.nodevalue (Boolean.BoolValue.index v)) in
   match Ground.sem t with
+  | { app = {builtin = Expr.Real_to_fp (8, 24); _}; args; _} ->
+    let m, r = IArray.extract2_exn args in
+    !< (Farith.B32.of_q !>>m !>>>r)
+  | { app = {builtin = Expr.Plus_infinity (8, 24); _}; args; _} ->
+    assert (IArray.is_empty args);
+    !< (Farith.B32.infp)
+  | { app = {builtin = Expr.Minus_infinity (8, 24); _}; args; _} ->
+    assert (IArray.is_empty args);
+    !< (Farith.B32.infm)
+  | { app = {builtin = Expr.NaN (8, 24); _}; args; _} ->
+    assert (IArray.is_empty args);
+    !< (Farith.B32.(nan true Z.one))
+  | { app = {builtin = Expr.Plus_zero (8, 24); _}; args; _} ->
+    assert (IArray.is_empty args);
+    !< (Farith.B32.zerop)
+  | { app = {builtin = Expr.Minus_zero (8, 24); _}; args; _} ->
+    assert (IArray.is_empty args);
+    !< (Farith.B32.zero true)
   | { app = {builtin = Expr.Fp_add (8, 24); _}; args; _} ->
     let m, a, b = IArray.extract3_exn args in
     !< (Farith.B32.add !>>m !>a !>b)
@@ -124,7 +144,7 @@ let attach d g =
 let converter d (f:Ground.t) =
   let r = Ground.node f in
   let reg n = Egraph.register d n in
-  (* let merge n = Egraph.register d n; Egraph.merge d r n in *)
+  let merge n = Egraph.register d n; Egraph.merge d r n in
 
   let open Monad in
   let get a = Monad.get Float32.key a in
@@ -139,6 +159,21 @@ 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.NaN (8, 24); _}; args; _} ->
+    assert (IArray.is_empty args);
+    merge (cst (Farith.B32.nan true Z.one))
+  | {app={builtin=Expr.Plus_infinity (8, 24); _}; args; _} ->
+    assert (IArray.is_empty args);
+    merge (cst (Farith.B32.infp))
+  | {app={builtin=Expr.Minus_infinity (8, 24); _}; args; _} ->
+    assert (IArray.is_empty args);
+    merge (cst (Farith.B32.infm))
+  | {app={builtin=Expr.Plus_zero (8, 24); _}; args; _} ->
+    assert (IArray.is_empty args);
+    merge (cst (Farith.B32.zerop))
+  | {app={builtin=Expr.Minus_zero (8, 24); _}; args; _} ->
+    assert (IArray.is_empty args);
+    merge (cst (Farith.B32.zero true))
   | {app={builtin=Expr.Fp_abs (8, 24); _}; args; _} ->
     let a = IArray.extract1_exn args in
     reg a; attach d f;

src_colibri2/theories/FP/fp.ml

@@ -20,6 +20,7 @@
 
 let th_register env =
   Rounding_mode.init env;
+  Dom_interval.init env;
   Float32.init env;
   Float64.init env