compatibility layer btw farith & farith2

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

@@ -17,9 +17,6 @@
 --dont-print-result %{dep:recognize_float32.smt2})))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:recognize_float32.smt2})))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
---dont-print-result %{dep:recognize_float64.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:recognize_float64.smt2})))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:recognize_rounding_mode.smt2})))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:recognize_rounding_mode.smt2})))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status sat 

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

-(set-logic ALL)
-(declare-fun x () (_ FloatingPoint 11 53))
-(declare-fun y () (_ FloatingPoint 11 53))
-(assert (= x y))
-(check-sat)
\ No newline at end of file

src_colibri2/theories/FP/dom_interval.ml

@@ -26,7 +26,7 @@ let debug = Debug.register_info_flag
   ~desc:"for intervals for the arithmetic theory"
   "LRA.interval"
 
-module D = Interval_32.Intv32
+module D = Interval32
 
 let dom = Dom.Kind.create (module struct type t = D.t let name = "ARITH" end)
 
@@ -160,7 +160,7 @@ let converter d (f:Ground.t) =
     let m, a, b = IArray.extract3_exn args in
     reg m; reg a; reg b;
     attach d (
-      set r (let+ vm = getm m and+ va = get a and+ vb = get b in D.add vm va vb)
+      set r (let+ vm = getm m and+ va = get a and+ vb = get b in D.add (D.to_mode vm) va vb)
     )
   (* | { app = {builtin = Expr.Fp_sub (8, 24); _}; args; _} ->
     let m, a, b = IArray.extract3_exn args in

src_colibri2/theories/FP/dune

@@ -5,6 +5,7 @@
  (libraries
   containers
   farith
+  farith2
   colibri2.stdlib
   colibri2.popop_lib
   colibri2.theories.bool

src_colibri2/theories/FP/float64.ml

-(*************************************************************************)
-(*  This file is part of Colibri2.                                       *)
-(*                                                                       *)
-(*  Copyright (C) 2014-2021                                              *)
-(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
-(*           alternatives)                                               *)
-(*                                                                       *)
-(*  you can redistribute it and/or modify it under the terms of the GNU  *)
-(*  Lesser General Public License as published by the Free Software      *)
-(*  Foundation, version 2.1.                                             *)
-(*                                                                       *)
-(*  It is distributed in the hope that it will be useful,                *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
-(*  GNU Lesser General Public License for more details.                  *)
-(*                                                                       *)
-(*  See the GNU Lesser General Public License version 2.1                *)
-(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
-(*************************************************************************)
-
-open Fp_value
-module N64 = struct let name = "Float64" end
-module Float64 = Value.Register(MakeFloat(Farith.B64)(N64))
-
-include Float64
-
-(** Initialise type interpretation
-    TODO : fix bounds (there is a finite set of 64 bits floats)
-*)
-let init_ty d =
-  Interp.Register.ty d (fun d ty ->
-      match ty with
-      | {app={builtin = Builtin.Float(11, 53);_};_} ->
-        let seq =
-          let open Interp.SeqLim in
-          let+ e = of_seq d posint_sequence in
-          (Farith.B64.of_bits e |> index |> nodevalue)
-        in
-        Some seq
-      | _ -> None)
-
-(* TO DO : Initialise check *)
-(* let init_check d = Interp.Register.check d (...) *)
-
-let init env =
-  init_ty env

src_colibri2/theories/FP/float64.mli

-(*************************************************************************)
-(*  This file is part of Colibri2.                                       *)
-(*                                                                       *)
-(*  Copyright (C) 2014-2021                                              *)
-(*    CEA   (Commissariat à l'énergie atomique et aux énergies           *)
-(*           alternatives)                                               *)
-(*                                                                       *)
-(*  you can redistribute it and/or modify it under the terms of the GNU  *)
-(*  Lesser General Public License as published by the Free Software      *)
-(*  Foundation, version 2.1.                                             *)
-(*                                                                       *)
-(*  It is distributed in the hope that it will be useful,                *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of       *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        *)
-(*  GNU Lesser General Public License for more details.                  *)
-(*                                                                       *)
-(*  See the GNU Lesser General Public License version 2.1                *)
-(*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
-(*************************************************************************)
-
-include Value.S with type s = Farith.B64.t
-
-val init : Egraph.wt -> unit

src_colibri2/theories/FP/fp.ml

@@ -21,8 +21,7 @@
 let th_register env =
   Rounding_mode.init env;
   Dom_interval.init env;
-  Float32.init env;
-  Float64.init env
+  Float32.init env
 
 (* Add the theory to defaults *)
 let () =

src_colibri2/theories/FP/interval_32.ml → src_colibri2/theories/FP/interval32.ml

-(** val negb : bool -> bool **)
+(* * val negb : bool -> bool *
 
 let negb = function
 | true -> false
@@ -1009,4 +1009,46 @@ end =
           Farith.B32.pp (b_to_B32 a)
           Farith.B32.pp (b_to_B32 b)
  end
+ *)
 
+ (* let b_of_B32 (f : Farith.B32.t) =
+    match Farith.B32.classify f with
+    | Farith.Zero s -> B754_zero s
+    | Farith.Infinity s -> B754_infinity s
+    | Farith.NaN (_, _) -> B754_nan
+    | Farith.Finite (s, m, e) -> B754_finite (s, _, _) *)
+
+include Farith2.Intv32.Intv32
+  
+let b_to_B32 f = 
+  (Farith.B32.of_bits (Farith2.B32.B32.to_bits f))
+
+let b_of_B32 f =
+  (Farith2.B32.B32.of_bits (Farith.B32.to_bits f))
+
+let to_mode (m : Farith.mode) : Farith2.Farith_Big.mode =
+  match m with
+  | Farith.NE -> Farith2.Farith_Big.NE
+  | Farith.ZR -> Farith2.Farith_Big.ZR
+  | Farith.DN -> Farith2.Farith_Big.DN
+  | Farith.UP -> Farith2.Farith_Big.UP
+  | Farith.NA -> Farith2.Farith_Big.NA
+
+let is_singleton = function
+  | Farith2.Interval.Inan -> Some Farith.B32.default_nan
+  | Intv (a, b, n) ->
+    if (&&) (Farith2.BinarySingleNaN.coq_Beqb prec emax a b) (not n)
+    then Some (b_to_B32 a)
+    else None
+
+let to_string = function
+  | Farith2.Interval.Inan -> "{ NaN }"
+  | Intv (a, b, nan) ->
+    if nan then
+      Format.sprintf "[%a, %a] + NaN"
+        Farith.B32.pp (b_to_B32 a)
+        Farith.B32.pp (b_to_B32 b)
+    else
+      Format.sprintf "[%a, %a]"
+        Farith.B32.pp (b_to_B32 a)
+        Farith.B32.pp (b_to_B32 b)