diff --git a/src_colibri2/tests/solve/smt_fp/sat/dune.inc b/src_colibri2/tests/solve/smt_fp/sat/dune.inc
index 0a776eab81b6bd13f4f5a1c7a787873ac7be0bda..f0216026c8d36e97ea490cf09e2b42bc28de066b 100644
--- a/src_colibri2/tests/solve/smt_fp/sat/dune.inc
+++ b/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
diff --git a/src_colibri2/tests/solve/smt_fp/sat/recognize_float64.smt2 b/src_colibri2/tests/solve/smt_fp/sat/recognize_float64.smt2
deleted file mode 100644
index 51b3b30b78cb09def79d66167969933518883501..0000000000000000000000000000000000000000
--- a/src_colibri2/tests/solve/smt_fp/sat/recognize_float64.smt2
+++ /dev/null
@@ -1,5 +0,0 @@
-(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
diff --git a/src_colibri2/theories/FP/dom_interval.ml b/src_colibri2/theories/FP/dom_interval.ml
index bc154d4da8e30f09f26ba81c55200966f1295413..bf782cf774db272ff07f7accf088a6a4a760dbc0 100644
--- a/src_colibri2/theories/FP/dom_interval.ml
+++ b/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
diff --git a/src_colibri2/theories/FP/dom_interval/extracted.ml b/src_colibri2/theories/FP/dom_interval/extracted.ml
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src_colibri2/theories/FP/dom_interval/interval_32.ml b/src_colibri2/theories/FP/dom_interval/interval_32.ml
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src_colibri2/theories/FP/dune b/src_colibri2/theories/FP/dune
index cbb3f787cb459924a1feec6571f6578d90eac56b..09f9db029f87ace159cb599eaecaa0f73d3533cb 100644
--- a/src_colibri2/theories/FP/dune
+++ b/src_colibri2/theories/FP/dune
@@ -5,6 +5,7 @@
(libraries
containers
farith
+ farith2
colibri2.stdlib
colibri2.popop_lib
colibri2.theories.bool
diff --git a/src_colibri2/theories/FP/float64.ml b/src_colibri2/theories/FP/float64.ml
deleted file mode 100644
index 803b353b0fa34c8ce90c3ae5040c1bb11b9e871c..0000000000000000000000000000000000000000
--- a/src_colibri2/theories/FP/float64.ml
+++ /dev/null
@@ -1,46 +0,0 @@
-(*************************************************************************)
-(* 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
diff --git a/src_colibri2/theories/FP/float64.mli b/src_colibri2/theories/FP/float64.mli
deleted file mode 100644
index 908b52f61c02a6f79cab51f3bae8fa5156861146..0000000000000000000000000000000000000000
--- a/src_colibri2/theories/FP/float64.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-(*************************************************************************)
-(* 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
diff --git a/src_colibri2/theories/FP/fp.ml b/src_colibri2/theories/FP/fp.ml
index edd102b7cf47e01221870a9610de44a6e8a5ea3c..cdee9a24e8412d4a20c0fa92862ef8269b595902 100644
--- a/src_colibri2/theories/FP/fp.ml
+++ b/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 () =
diff --git a/src_colibri2/theories/FP/interval_32.ml b/src_colibri2/theories/FP/interval32.ml
similarity index 94%
rename from src_colibri2/theories/FP/interval_32.ml
rename to src_colibri2/theories/FP/interval32.ml
index 7d3103857bd3c53ffa94b528a0997301970c3fda..de62cbbfc05cf8465ba35cd71d98f7acf3ec8d05 100644
--- a/src_colibri2/theories/FP/interval_32.ml
+++ b/src_colibri2/theories/FP/interval32.ml
@@ -1,4 +1,4 @@
-(** 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)