From e0248499da9094733c71a7b6177002565482208c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 10 Jan 2022 10:28:52 +0100
Subject: [PATCH] [FP] Add interpretation of fp functions
---
dolmen | 2 +-
farith2/extract/dune | 3 +-
farith2/extracted/BinarySingleNaN.ml | 93 +++++++++++++++
farith2/extracted/BinarySingleNaN.mli | 14 +++
farith2/extracted/GenericFloat.ml | 58 ++++++++++
farith2/extracted/GenericFloat.mli | 12 ++
farith2/extracted/Qextended.ml | 20 ++++
farith2/extracted/Qextended.mli | 8 ++
farith2/extracted/Zaux.ml | 14 +++
farith2/extracted/Zaux.mli | 8 ++
farith2/extracted/dune | 4 +
farith2/farith2.ml | 25 ++++
farith2/farith2.mli | 18 +++
farith2/thry/GenericFloat.v | 141 +++++++++++++++++++++++
src_colibri2/stdlib/std.ml | 6 +
src_colibri2/stdlib/std.mli | 2 +
src_colibri2/theories/FP/fp_value.ml | 65 +++++++++++
src_colibri2/theories/LRA/dom_product.ml | 7 +-
src_colibri2/theories/LRA/realValue.ml | 90 ++++++++++++---
src_colibri2/theories/LRA/realValue.mli | 10 +-
20 files changed, 572 insertions(+), 28 deletions(-)
diff --git a/dolmen b/dolmen
index b3a925b8c..1e57fe56d 160000
--- a/dolmen
+++ b/dolmen
@@ -1 +1 @@
-Subproject commit b3a925b8c352497a06fe4565ed57d98ab1d8f85a
+Subproject commit 1e57fe56df0f098dfd18860ee6b2ac83429a8fba
diff --git a/farith2/extract/dune b/farith2/extract/dune
index 5645e6984..009772716 100644
--- a/farith2/extract/dune
+++ b/farith2/extract/dune
@@ -1,5 +1,6 @@
(coq.extraction
(prelude extraction)
(extracted_modules BinNums Bool Qextended Utils Binary BinPosDef Datatypes Round Zaux BinarySingleNaN
- BinPos Interval SpecFloat Zbool BinInt Bits Specif Zpower Assert GenericFloat Version)
+ BinPos Interval SpecFloat Zbool BinInt Bits Specif Zpower Assert GenericFloat Version
+ Defs Operations)
(theories Farith2))
diff --git a/farith2/extracted/BinarySingleNaN.ml b/farith2/extracted/BinarySingleNaN.ml
index f3f6d10d7..9ba0ae9bf 100644
--- a/farith2/extracted/BinarySingleNaN.ml
+++ b/farith2/extracted/BinarySingleNaN.ml
@@ -1,8 +1,11 @@
open BinInt
open Bool
open Datatypes
+open Defs
+open Operations
open Round
open SpecFloat
+open Zaux
type binary_float =
| B754_zero of bool
@@ -28,6 +31,15 @@ let coq_B2SF _ _ = function
| B754_nan -> S754_nan
| B754_finite (s, m, e) -> S754_finite (s, m, e)
+(** val coq_Bsign :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> bool **)
+
+let coq_Bsign _ _ = function
+| B754_zero s -> s
+| B754_infinity s -> s
+| B754_nan -> false
+| B754_finite (s, _, _) -> s
+
(** val is_nan :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> bool **)
@@ -251,6 +263,87 @@ let coq_Bminus prec emax m x y =
| Farith_Big.DN -> true
| _ -> false))
+(** val coq_Bfma_szero :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
+ binary_float -> binary_float -> binary_float -> bool **)
+
+let coq_Bfma_szero prec emax m x y z =
+ let s_xy = xorb (coq_Bsign prec emax x) (coq_Bsign prec emax y) in
+ if eqb s_xy (coq_Bsign prec emax z)
+ then s_xy
+ else (match m with
+ | Farith_Big.DN -> true
+ | _ -> false)
+
+(** val coq_Bfma :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
+ binary_float -> binary_float -> binary_float -> binary_float **)
+
+let coq_Bfma prec emax m x y z =
+ match x with
+ | B754_zero _ ->
+ (match y with
+ | B754_zero _ ->
+ (match z with
+ | B754_zero _ -> B754_zero (coq_Bfma_szero prec emax m x y z)
+ | B754_nan -> B754_nan
+ | _ -> z)
+ | B754_finite (_, _, _) ->
+ (match z with
+ | B754_zero _ -> B754_zero (coq_Bfma_szero prec emax m x y z)
+ | B754_nan -> B754_nan
+ | _ -> z)
+ | _ -> B754_nan)
+ | B754_infinity sx ->
+ (match y with
+ | B754_infinity sy ->
+ let s = xorb sx sy in
+ (match z with
+ | B754_infinity sz -> if eqb s sz then z else B754_nan
+ | B754_nan -> B754_nan
+ | _ -> B754_infinity s)
+ | B754_finite (sy, _, _) ->
+ let s = xorb sx sy in
+ (match z with
+ | B754_infinity sz -> if eqb s sz then z else B754_nan
+ | B754_nan -> B754_nan
+ | _ -> B754_infinity s)
+ | _ -> B754_nan)
+ | B754_nan -> B754_nan
+ | B754_finite (sx, mx, ex) ->
+ (match y with
+ | B754_zero _ ->
+ (match z with
+ | B754_zero _ -> B754_zero (coq_Bfma_szero prec emax m x y z)
+ | B754_nan -> B754_nan
+ | _ -> z)
+ | B754_infinity sy ->
+ let s = xorb sx sy in
+ (match z with
+ | B754_infinity sz -> if eqb s sz then z else B754_nan
+ | B754_nan -> B754_nan
+ | _ -> B754_infinity s)
+ | B754_nan -> B754_nan
+ | B754_finite (sy, my, ey) ->
+ (match z with
+ | B754_zero _ ->
+ let x0 = { coq_Fnum = (cond_Zopp sx mx); coq_Fexp = ex } in
+ let y0 = { coq_Fnum = (cond_Zopp sy my); coq_Fexp = ey } in
+ let { coq_Fnum = mr; coq_Fexp = er } = coq_Fmult radix2 x0 y0 in
+ binary_normalize prec emax m mr er
+ (coq_Bfma_szero prec emax m x y z)
+ | B754_infinity _ -> z
+ | B754_nan -> B754_nan
+ | B754_finite (sz, mz, ez) ->
+ let x0 = { coq_Fnum = (cond_Zopp sx mx); coq_Fexp = ex } in
+ let y0 = { coq_Fnum = (cond_Zopp sy my); coq_Fexp = ey } in
+ let z0 = { coq_Fnum = (cond_Zopp sz mz); coq_Fexp = ez } in
+ let { coq_Fnum = mr; coq_Fexp = er } =
+ coq_Fplus radix2 (coq_Fmult radix2 x0 y0) z0
+ in
+ binary_normalize prec emax m mr er
+ (coq_Bfma_szero prec emax m x y z)))
+
(** val coq_Bdiv :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
binary_float -> binary_float -> binary_float **)
diff --git a/farith2/extracted/BinarySingleNaN.mli b/farith2/extracted/BinarySingleNaN.mli
index 5a6d651e3..de93041fe 100644
--- a/farith2/extracted/BinarySingleNaN.mli
+++ b/farith2/extracted/BinarySingleNaN.mli
@@ -1,8 +1,11 @@
open BinInt
open Bool
open Datatypes
+open Defs
+open Operations
open Round
open SpecFloat
+open Zaux
type binary_float =
| B754_zero of bool
@@ -16,6 +19,9 @@ val coq_SF2B :
val coq_B2SF :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> spec_float
+val coq_Bsign :
+ Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> bool
+
val is_nan : Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> bool
val coq_Babs :
@@ -75,6 +81,14 @@ val coq_Bminus :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> binary_float
-> binary_float -> binary_float
+val coq_Bfma_szero :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> binary_float
+ -> binary_float -> binary_float -> bool
+
+val coq_Bfma :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> binary_float
+ -> binary_float -> binary_float -> binary_float
+
val coq_Bdiv :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode -> binary_float
-> binary_float -> binary_float
diff --git a/farith2/extracted/GenericFloat.ml b/farith2/extracted/GenericFloat.ml
index 6e801d44f..205f97e0d 100644
--- a/farith2/extracted/GenericFloat.ml
+++ b/farith2/extracted/GenericFloat.ml
@@ -4,6 +4,7 @@ open BinarySingleNaN
open Bits
open Datatypes
open Interval
+open Qextended
open SpecFloat
type __ = Obj.t
@@ -177,6 +178,18 @@ module GenericFloat =
(coq_Bdiv (cprec x.mw) (cemax x.ew) m x.value
(same_format_cast (prec x) (emax x) (prec y) (emax y) y.value)))
+ (** val fma : Farith_Big.mode -> t -> t -> t -> t **)
+
+ let fma m x y z =
+ (fun x f -> assert x; f ()) ((&&) (same_format x y) (same_format x z))
+ (fun _ ->
+ mk_with x
+ (coq_Bfma (cprec x.mw) (cemax x.ew) m x.value
+ (same_format_cast (cprec x.mw) (cemax x.ew) (cprec y.mw)
+ (cemax y.ew) y.value)
+ (same_format_cast (cprec x.mw) (cemax x.ew) (cprec z.mw)
+ (cemax z.ew) z.value)))
+
(** val sqrt : Farith_Big.mode -> t -> t **)
let sqrt m x =
@@ -187,6 +200,51 @@ module GenericFloat =
let abs x =
mk_with x (coq_Babs (cprec x.mw) (cemax x.ew) x.value)
+ (** val neg : t -> t **)
+
+ let neg x =
+ mk_with x
+ (match x.value with
+ | B754_zero s -> B754_zero (Pervasives.not s)
+ | B754_infinity s -> B754_infinity (Pervasives.not s)
+ | B754_nan -> B754_nan
+ | B754_finite (s, m, e) -> B754_finite ((Pervasives.not s), m, e))
+
+ (** val least_bit_Pnat : Farith_Big.big_int -> Farith_Big.big_int **)
+
+ let rec least_bit_Pnat n =
+ Farith_Big.positive_case
+ (fun _ -> Farith_Big.zero)
+ (fun p -> Farith_Big.succ (least_bit_Pnat p))
+ (fun _ -> Farith_Big.zero)
+ n
+
+ (** val shiftr_pos :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
+
+ let shiftr_pos a p =
+ Farith_Big.nat_rect a (fun _ -> Farith_Big.div2_floor) p
+
+ (** val to_q : t -> Q.t **)
+
+ let to_q f =
+ match f.value with
+ | B754_zero _ -> coq_Qx_zero
+ | B754_infinity b -> if b then coq_Qx_minus_inf else coq_Qx_inf
+ | B754_nan -> coq_Qx_undef
+ | B754_finite (b, m, e) ->
+ let e' = least_bit_Pnat m in
+ let m' = if b then Farith_Big.opp m else m in
+ let e'' = Farith_Big.add e (Farith_Big.identity e') in
+ (Farith_Big.z_case
+ (fun _ -> Farith_Big.q_mk ((shiftr_pos m' e'),
+ Farith_Big.one))
+ (fun _ -> Farith_Big.q_mk ((Farith_Big.shiftl m' e),
+ Farith_Big.one))
+ (fun p -> Farith_Big.q_mk ((shiftr_pos m' e'),
+ (Farith_Big.shiftl Farith_Big.one p)))
+ e'')
+
(** val le : t -> t -> bool **)
let le x y =
diff --git a/farith2/extracted/GenericFloat.mli b/farith2/extracted/GenericFloat.mli
index b0387b211..08ef796a9 100644
--- a/farith2/extracted/GenericFloat.mli
+++ b/farith2/extracted/GenericFloat.mli
@@ -4,6 +4,7 @@ open BinarySingleNaN
open Bits
open Datatypes
open Interval
+open Qextended
open SpecFloat
type __ = Obj.t
@@ -79,10 +80,21 @@ module GenericFloat :
val div : Farith_Big.mode -> t -> t -> t
+ val fma : Farith_Big.mode -> t -> t -> t -> t
+
val sqrt : Farith_Big.mode -> t -> t
val abs : t -> t
+ val neg : t -> t
+
+ val least_bit_Pnat : Farith_Big.big_int -> Farith_Big.big_int
+
+ val shiftr_pos :
+ Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int
+
+ val to_q : t -> Q.t
+
val le : t -> t -> bool
val lt : t -> t -> bool
diff --git a/farith2/extracted/Qextended.ml b/farith2/extracted/Qextended.ml
index 139597f9c..4d9bfaa92 100644
--- a/farith2/extracted/Qextended.ml
+++ b/farith2/extracted/Qextended.ml
@@ -1,2 +1,22 @@
+(** val coq_Qx_zero : Q.t **)
+
+let coq_Qx_zero =
+ Farith_Big.q_mk (Farith_Big.zero, Farith_Big.one)
+
+(** val coq_Qx_undef : Q.t **)
+
+let coq_Qx_undef =
+ Farith_Big.q_mk (Farith_Big.zero, Farith_Big.zero)
+
+(** val coq_Qx_inf : Q.t **)
+
+let coq_Qx_inf =
+ Farith_Big.q_mk (Farith_Big.one, Farith_Big.zero)
+
+(** val coq_Qx_minus_inf : Q.t **)
+
+let coq_Qx_minus_inf =
+ Farith_Big.q_mk ((Farith_Big.opp Farith_Big.one), Farith_Big.zero)
+
diff --git a/farith2/extracted/Qextended.mli b/farith2/extracted/Qextended.mli
index 139597f9c..7698b1e58 100644
--- a/farith2/extracted/Qextended.mli
+++ b/farith2/extracted/Qextended.mli
@@ -1,2 +1,10 @@
+val coq_Qx_zero : Q.t
+
+val coq_Qx_undef : Q.t
+
+val coq_Qx_inf : Q.t
+
+val coq_Qx_minus_inf : Q.t
+
diff --git a/farith2/extracted/Zaux.ml b/farith2/extracted/Zaux.ml
index 139597f9c..d575ac647 100644
--- a/farith2/extracted/Zaux.ml
+++ b/farith2/extracted/Zaux.ml
@@ -1,2 +1,16 @@
+type radix =
+ Farith_Big.big_int
+ (* singleton inductive, whose constructor was Build_radix *)
+
+(** val radix_val : radix -> Farith_Big.big_int **)
+
+let radix_val r =
+ r
+
+(** val radix2 : radix **)
+
+let radix2 =
+ (Farith_Big.double Farith_Big.one)
+
diff --git a/farith2/extracted/Zaux.mli b/farith2/extracted/Zaux.mli
index 139597f9c..200260b8d 100644
--- a/farith2/extracted/Zaux.mli
+++ b/farith2/extracted/Zaux.mli
@@ -1,2 +1,10 @@
+type radix =
+ Farith_Big.big_int
+ (* singleton inductive, whose constructor was Build_radix *)
+
+val radix_val : radix -> Farith_Big.big_int
+
+val radix2 : radix
+
diff --git a/farith2/extracted/dune b/farith2/extracted/dune
index a607f0d77..13d1e5a86 100644
--- a/farith2/extracted/dune
+++ b/farith2/extracted/dune
@@ -40,3 +40,7 @@
(rule (action (copy ../extract/GenericFloat.mli GenericFloat.mli)) (mode promote))
(rule (action (copy ../extract/Version.ml Version.ml)) (mode promote))
(rule (action (copy ../extract/Version.mli Version.mli)) (mode promote))
+(rule (action (copy ../extract/Defs.ml Defs.ml)) (mode promote))
+(rule (action (copy ../extract/Defs.mli Defs.mli)) (mode promote))
+(rule (action (copy ../extract/Operations.ml Operations.ml)) (mode promote))
+(rule (action (copy ../extract/Operations.mli Operations.mli)) (mode promote))
diff --git a/farith2/farith2.ml b/farith2/farith2.ml
index 7573c9a30..d9c295fc8 100644
--- a/farith2/farith2.ml
+++ b/farith2/farith2.ml
@@ -100,6 +100,31 @@ module F = struct
let inf ~mw ~ew b = inf (Z.of_int mw) (Z.of_int ew) b
let is_zero t = match t.value with B754_zero _ -> true | _ -> false
+
+ let is_infinite t = match t.value with B754_infinity _ -> true | _ -> false
+
+ let is_nan t = match t.value with B754_nan -> true | _ -> false
+
+ let is_negative t =
+ match t.value with
+ | B754_zero true | B754_finite (true, _, _) -> true
+ | _ -> false
+
+ let is_positive t =
+ match t.value with
+ | B754_zero false | B754_finite (false, _, _) -> true
+ | _ -> false
+
+ let is_normal t =
+ match t.value with
+ | B754_zero _ -> true
+ | B754_finite (_, e, _) when Z.sign e <> 0 -> true
+ | _ -> false
+
+ let is_subnormal t =
+ match t.value with
+ | B754_finite (_, e, _) when Z.sign e = 0 -> true
+ | _ -> false
end
module I = struct
diff --git a/farith2/farith2.mli b/farith2/farith2.mli
index c48254902..ce6176e45 100644
--- a/farith2/farith2.mli
+++ b/farith2/farith2.mli
@@ -48,6 +48,8 @@ module F : sig
val of_q : mw:int -> ew:int -> mode:mode -> Q.t -> t
+ val to_q : t -> Q.t
+
val add : mode -> t -> t -> t
val sub : mode -> t -> t -> t
@@ -56,10 +58,14 @@ module F : sig
val div : mode -> t -> t -> t
+ val fma : mode -> t -> t -> t -> t
+
val sqrt : mode -> t -> t
val abs : t -> t
+ val neg : t -> t
+
val of_bits : mw:int -> ew:int -> Z.t -> t
val to_bits : t -> Z.t
@@ -81,6 +87,18 @@ module F : sig
val inf : mw:int -> ew:int -> bool -> t
val is_zero : t -> bool
+
+ val is_infinite : t -> bool
+
+ val is_nan : t -> bool
+
+ val is_negative : t -> bool
+
+ val is_positive : t -> bool
+
+ val is_normal : t -> bool
+
+ val is_subnormal : t -> bool
end
module I : sig
diff --git a/farith2/thry/GenericFloat.v b/farith2/thry/GenericFloat.v
index d8a92271a..4556a5a74 100644
--- a/farith2/thry/GenericFloat.v
+++ b/farith2/thry/GenericFloat.v
@@ -186,12 +186,153 @@ Module GenericFloat.
Definition div (m : mode) (x y : t) : t :=
AssertF.assert (same_format x y) (fun H => mk_with x (@Bdiv _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast H (value y)))).
+ Program Definition fma (m : mode) (x y z : t) : t :=
+ AssertF.assert (andb (same_format x y) (same_format x z)) (fun H => mk_with x (@Bfma _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast _ (value y)) (same_format_cast _ (value z)))).
+ Next Obligation.
+ rewrite !Bool.andb_true_iff in H.
+ exact (proj1 H).
+ Defined.
+ Next Obligation.
+ rewrite !Bool.andb_true_iff in H.
+ exact (proj2 H).
+ Defined.
+
Definition sqrt (m : mode) (x : t) : t :=
mk_with x (@Bsqrt _ _ (Hprec x) (Hemax x) m (value x)).
Definition abs (x : t) : t :=
mk_with x (@Babs _ _ (value x)).
+ Definition neg (x : t) : t :=
+ mk_with x (match value x with
+ | B754_nan => B754_nan
+ | B754_zero s => B754_zero (negb s)
+ | B754_infinity s => B754_infinity (negb s)
+ | B754_finite s m e H => B754_finite (negb s) m e H
+ end).
+
+ Fixpoint least_bit_Pnat (n : positive) :=
+ match n with
+ | xH => O
+ | xO p => S (least_bit_Pnat p)
+ | xI p => O
+ end.
+
+
+ Definition shiftr_pos a p := Wf_nat.iter_nat p _ Z.div2 a.
+
+ Lemma shiftr_pos_is_shiftr :
+ forall a p, shiftr_pos a p = Z.shiftr a (Z.of_nat p).
+ Proof.
+ intros.
+ destruct p.
+ reflexivity.
+ unfold shiftr_pos, Z.shiftr, Z.shiftl, Z.of_nat, Z.opp.
+ rewrite Pos2Nat.inj_iter.
+ rewrite SuccNat2Pos.id_succ.
+ reflexivity.
+ Qed.
+
+ Lemma least_bit_shiftr_pos :
+ forall m (b:bool),
+ let e' := least_bit_Pnat m in
+ let m' := if b then Z.neg m else Z.pos m in
+ let m'' := shiftr_pos m' e' in
+ Z.odd m'' = true.
+ Proof.
+ induction m; intro b.
+ - destruct b;reflexivity.
+ - assert (H:= IHm b);
+ destruct b;
+ replace (least_bit_Pnat m~0) with (S (least_bit_Pnat m)) in * by reflexivity;
+ intros e' m';
+ replace (shiftr_pos m' e') with (shiftr_pos (Z.div2 m') (least_bit_Pnat m)) by
+ (unfold shiftr_pos, e'; rewrite nat_rect_succ_r; reflexivity).
+ * replace (Z.div2 m') with (Z.neg m) by reflexivity.
+ exact H.
+ * replace (Z.div2 m') with (Z.pos m) by reflexivity.
+ exact H.
+ - destruct b; reflexivity.
+ Qed.
+
+
+ Lemma gcd_odd_pow_2:
+ forall (m:positive) n,
+ match m with xO _ => False | _ => True end ->
+ Pos.gcd m (Pos.shiftl 1%positive (Npos n)) = 1%positive.
+ Proof.
+ destruct m as [p|p|]; intros n H; destruct H; simpl.
+ - induction n using Pos.peano_ind.
+ * compute [Pos.iter Z.mul Pos.mul].
+ unfold Pos.gcd.
+ replace (Pos.size_nat 2) with (2)%nat by reflexivity.
+ simpl.
+ replace (Pos.size_nat p + 2)%nat with (S (S (Pos.size_nat p))) by auto with *.
+ reflexivity.
+ * rewrite Pos.iter_succ.
+ unfold Pos.gcd.
+ simpl.
+ replace (Pos.size_nat p + S (Pos.size_nat (Pos.iter xO 1%positive n)))%nat
+ with (S (Pos.size_nat p + Pos.size_nat (Pos.iter xO 1%positive n))) by auto with *.
+ exact IHn.
+ - unfold Pos.gcd.
+ reflexivity.
+ Qed.
+
+ Lemma to_q (f:t) : Qx.
+ Proof.
+ refine (match value f with
+ | B754_zero _ => Qx_zero
+ | B754_infinity b => if b then Qx_minus_inf else Qx_inf
+ | B754_nan => Qx_undef
+ | B754_finite b m e _ =>
+ let e' := least_bit_Pnat m in
+ let m' := if b then Z.neg m else Z.pos m in
+ let e'' := (e + (Z.of_nat e'))%Z in
+ match e'' with
+ | Z0 => Qxmake (shiftr_pos m' e') 1%Z (refl_equal _) _
+ | Z.pos _ => Qxmake (Z.shiftl m' e)%Z 1%Z (refl_equal _) _
+ | Z.neg p => Qxmake (shiftr_pos m' e') (Z.shiftl 1%Z (Z.pos p)) _ _
+ end
+ end
+ ).
+ - rewrite Z.gcd_1_r.
+ reflexivity.
+ - rewrite Z.gcd_1_r.
+ reflexivity.
+ - rewrite Z.shiftl_1_l.
+ apply Z.leb_le.
+ apply Z.lt_le_incl.
+ apply Zpower_pos_gt_0.
+ reflexivity.
+ - assert (Z.shiftl 1 (Z.pos p) =? 0 = false)%Z by
+ (rewrite Z.shiftl_1_l;
+ apply Z.eqb_neq;
+ apply Z.neq_sym;
+ apply Z.lt_neq;
+ exact (Zpower_pos_gt_0 2%Z p (refl_equal _))).
+ rewrite H.
+ assert (Z.odd (shiftr_pos m' e') = true) by (exact (least_bit_shiftr_pos m b)).
+ destruct (shiftr_pos m' e'); clear H e0 e' m' e''.
+ discriminate H0.
+ rewrite <- (shift_equiv _ _ (Pos2Z.is_nonneg _)).
+ replace (shift (Z.pos p) 1) with (shift_pos p 1%positive) by reflexivity.
+ rewrite shift_pos_equiv.
+ compute [Z.gcd].
+ rewrite gcd_odd_pow_2.
+ reflexivity.
+ unfold Z.odd in H0.
+ destruct p0; [exact I| discriminate H0| exact I].
+ rewrite <- (shift_equiv _ _ (Pos2Z.is_nonneg _)).
+ replace (shift (Z.pos p) 1) with (shift_pos p 1%positive) by reflexivity.
+ rewrite shift_pos_equiv.
+ compute [Z.gcd].
+ rewrite gcd_odd_pow_2.
+ reflexivity.
+ unfold Z.odd in H0.
+ destruct p0; [exact I| discriminate H0| exact I].
+ Defined.
+
Definition le (x y : t) : bool :=
AssertB.assert (same_format x y) (fun H => (@Bleb _ _ (value x) (same_format_cast H (value y)))).
diff --git a/src_colibri2/stdlib/std.ml b/src_colibri2/stdlib/std.ml
index 3b063ca17..99146f602 100644
--- a/src_colibri2/stdlib/std.ml
+++ b/src_colibri2/stdlib/std.ml
@@ -152,4 +152,10 @@ module Q = struct
@@ let+ num = int (Z.to_int (Q.num q))
and+ den = int (Z.to_int (Q.den q)) in
Q.make (Z.of_int num) (Z.of_int den)
+
+ let pow q n =
+ if Int.(n < 0) then (
+ assert (Int.(Q.sign q <> 0));
+ Q.make (Z.pow q.den Int.(-n)) (Z.pow q.num Int.(-n)))
+ else Q.make (Z.pow q.num n) (Z.pow q.den n)
end
diff --git a/src_colibri2/stdlib/std.mli b/src_colibri2/stdlib/std.mli
index cf7a9e7c2..7101e0df8 100644
--- a/src_colibri2/stdlib/std.mli
+++ b/src_colibri2/stdlib/std.mli
@@ -80,6 +80,8 @@ module Q : sig
val mod_f : t -> t -> t
+ val pow : t -> int -> t
+
val is_integer : t -> bool
val is_unsigned_integer : int -> t -> bool
diff --git a/src_colibri2/theories/FP/fp_value.ml b/src_colibri2/theories/FP/fp_value.ml
index 2f7852995..b0d616b7d 100644
--- a/src_colibri2/theories/FP/fp_value.ml
+++ b/src_colibri2/theories/FP/fp_value.ml
@@ -87,10 +87,45 @@ let compute_ground d t =
let ( !<< ) v =
`Some (Boolean.BoolValue.nodevalue (Boolean.BoolValue.index v))
in
+ let ( !<<< ) v =
+ `Some Colibri2_theories_LRA.RealValue.(nodevalue (index v))
+ in
match Ground.sem t with
| { app = { builtin = Expr.Real_to_fp (ew, prec); _ }; args; _ } ->
let m, r = IArray.extract2_exn args in
!<(F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m !>>>r)
+ | { app = { builtin = Expr.Fp_to_fp (_ew1, _prec1, ew2, prec2); _ }; args; _ }
+ ->
+ let m, f1 = IArray.extract2_exn args in
+ !<(F.of_q ~ew:ew2 ~mw:(prec2 - 1) ~mode:!>>m (F.to_q !>f1))
+ | { app = { builtin = Expr.Sbv_to_fp (n, ew, prec); _ }; args; _ } ->
+ let m, bv = IArray.extract2_exn args in
+ !<(F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m
+ (Q.of_bigint (Colibri2_theories_LRA.RealValue.signed_bitv n !>>>bv)))
+ | { app = { builtin = Expr.Ubv_to_fp (n, ew, prec); _ }; args; _ } ->
+ let m, bv = IArray.extract2_exn args in
+ !<(F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m
+ (Q.of_bigint
+ (Colibri2_theories_LRA.RealValue.unsigned_bitv n !>>>bv)))
+ | { app = { builtin = Expr.Fp (ew, prec); _ }; args; _ } ->
+ let bvs, bve, bvm = IArray.extract3_exn args in
+ !<(F.of_bits ~ew ~mw:(prec - 1)
+ (Z.logor
+ (Z.logor
+ (Z.shift_left
+ (Colibri2_theories_LRA.RealValue.unsigned_bitv 1 !>>>bvs)
+ (ew + prec - 1))
+ (Z.shift_left
+ (Colibri2_theories_LRA.RealValue.unsigned_bitv ew !>>>bve)
+ (prec - 1)))
+ (Colibri2_theories_LRA.RealValue.unsigned_bitv (prec - 1) !>>>bvm)))
+ | { app = { builtin = Expr.Ieee_format_to_fp (ew, prec); _ }; args; _ } ->
+ let bv = IArray.extract1_exn args in
+ !<(F.of_bits ~ew ~mw:(prec - 1)
+ (Colibri2_theories_LRA.RealValue.unsigned_bitv (ew + prec) !>>>bv))
+ | { app = { builtin = Expr.To_real (_ew, _prec); _ }; args; _ } ->
+ let r = IArray.extract1_exn args in
+ !<<<(F.to_q !>r)
| { app = { builtin = Expr.Plus_infinity (ew, prec); _ }; args; _ } ->
assert (IArray.is_empty args);
!<(F.inf ~ew ~mw:(prec - 1) false)
@@ -118,9 +153,18 @@ let compute_ground d t =
| { app = { builtin = Expr.Fp_abs (_ew, _prec); _ }; args; _ } ->
let a = IArray.extract1_exn args in
!<(F.abs !>a)
+ | { app = { builtin = Expr.Fp_neg (_ew, _prec); _ }; args; _ } ->
+ let a = IArray.extract1_exn args in
+ !<(F.neg !>a)
+ | { app = { builtin = Expr.Fp_sqrt (_ew, _prec); _ }; args; _ } ->
+ let m, a = IArray.extract2_exn args in
+ !<(F.sqrt !>>m !>a)
| { app = { builtin = Expr.Fp_div (_ew, _prec); _ }; args; _ } ->
let m, a, b = IArray.extract3_exn args in
!<(F.div !>>m !>a !>b)
+ | { app = { builtin = Expr.Fp_fma (_ew, _prec); _ }; args; _ } ->
+ let m, a, b, c = IArray.extract4_exn args in
+ !<(F.fma !>>m !>a !>b !>c)
| { app = { builtin = Expr.Fp_eq (_ew, _prec); _ }; args; _ } ->
let a, b = IArray.extract2_exn args in
!<<(F.eq !>a !>b)
@@ -136,6 +180,27 @@ let compute_ground d t =
| { app = { builtin = Expr.Fp_gt (_ew, _prec); _ }; args; _ } ->
let a, b = IArray.extract2_exn args in
!<<(F.gt !>a !>b)
+ | { app = { builtin = Expr.Fp_isInfinite (_ew, _prec); _ }; args; _ } ->
+ let a = IArray.extract1_exn args in
+ !<<(F.is_infinite !>a)
+ | { app = { builtin = Expr.Fp_isZero (_ew, _prec); _ }; args; _ } ->
+ let a = IArray.extract1_exn args in
+ !<<(F.is_zero !>a)
+ | { app = { builtin = Expr.Fp_isNaN (_ew, _prec); _ }; args; _ } ->
+ let a = IArray.extract1_exn args in
+ !<<(F.is_nan !>a)
+ | { app = { builtin = Expr.Fp_isNegative (_ew, _prec); _ }; args; _ } ->
+ let a = IArray.extract1_exn args in
+ !<<(F.is_negative !>a)
+ | { app = { builtin = Expr.Fp_isPositive (_ew, _prec); _ }; args; _ } ->
+ let a = IArray.extract1_exn args in
+ !<<(F.is_positive !>a)
+ | { app = { builtin = Expr.Fp_isNormal (_ew, _prec); _ }; args; _ } ->
+ let a = IArray.extract1_exn args in
+ !<<(F.is_normal !>a)
+ | { app = { builtin = Expr.Fp_isSubnormal (_ew, _prec); _ }; args; _ } ->
+ let a = IArray.extract1_exn args in
+ !<<(F.is_subnormal !>a)
| _ -> `None
let init_check d =
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index 0d6af37fa..5fac15401 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/src_colibri2/theories/LRA/dom_product.ml
@@ -332,12 +332,7 @@ let converter d (f : Ground.t) =
reg a;
reg b;
propagate_a_cb d ~res ~a ~b ~c:Q.minus_one
- | {
- app = { builtin = Expr.Abs | RealValue.Builtin.Abs_real };
- tyargs = [];
- args;
- _;
- } ->
+ | { app = { builtin = Expr.Abs }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
reg a;
SolveAbs.assume_equality d res (Product.of_list [ (a, Q.one) ]);
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index 18a8e58ba..7e052a918 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -23,13 +23,38 @@ open Colibri2_popop_lib
open Colibri2_stdlib.Std
module Builtin = struct
- type _ Expr.t += Abs_real | BV2Nat of int
+ type _ Expr.t += BV2Nat of int | Pow_int_int
let abs_real =
- Expr.Id.mk ~name:"colibri_abs_real" ~builtin:Abs_real
- (Dolmen_std.Path.global "Abs")
+ Expr.Id.mk ~name:"colibri_abs_real" ~builtin:Expr.Abs
+ (Dolmen_std.Path.global "colibri_abs_real")
(Expr.Ty.arrow [ Expr.Ty.real ] Expr.Ty.real)
+ let abs_int =
+ Expr.Id.mk ~name:"colibri_abs_int" ~builtin:Expr.Abs
+ (Dolmen_std.Path.global "colibri_abs_int")
+ (Expr.Ty.arrow [ Expr.Ty.int ] Expr.Ty.int)
+
+ let colibri_ceil =
+ Expr.Id.mk ~name:"colibri_ceil" ~builtin:Expr.Ceiling
+ (Dolmen_std.Path.global "colibri_ceil")
+ (Expr.Ty.arrow [ Expr.Ty.int ] Expr.Ty.int)
+
+ let colibri_pow_int_int =
+ Expr.Id.mk ~name:"colibri_pow_int_int" ~builtin:Pow_int_int
+ (Dolmen_std.Path.global "colibri_pow_int_int")
+ (Expr.Ty.arrow [ Expr.Ty.int; Expr.Ty.int ] Expr.Ty.int)
+
+ let colibri_cdiv =
+ Expr.Id.mk ~name:"colibri_cdiv" ~builtin:Expr.Div_t
+ (Dolmen_std.Path.global "colibri_cdiv")
+ (Expr.Ty.arrow [ Expr.Ty.int; Expr.Ty.int ] Expr.Ty.int)
+
+ let colibri_crem =
+ Expr.Id.mk ~name:"colibri_crem" ~builtin:Expr.Modulo_t
+ (Dolmen_std.Path.global "colibri_crem")
+ (Expr.Ty.arrow [ Expr.Ty.int; Expr.Ty.int ] Expr.Ty.int)
+
let bv2nat =
Popop_stdlib.DInt.H.memo
(fun n ->
@@ -44,15 +69,35 @@ module Builtin = struct
| { ty_descr = Expr.TyApp ({ builtin = Builtin.Bitv i; _ }, _) } -> i
| _ -> raise (Expr.Term.Wrong_type (t, Expr.Ty.bitv 0))
in
+ let app1 env s f =
+ `Term
+ (Dolmen_type.Base.term_app1
+ (module Dolmen_loop.Typer.T)
+ env s
+ (fun a -> Expr.Term.apply_cst f [] [ a ]))
+ in
+ let app2 env s f =
+ `Term
+ (Dolmen_type.Base.term_app2
+ (module Dolmen_loop.Typer.T)
+ env s
+ (fun a b -> Expr.Term.apply_cst f [] [ a; b ]))
+ in
Expr.add_builtins (fun env s ->
match s with
| Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "colibri_abs_real" }
->
- `Term
- (Dolmen_type.Base.term_app1
- (module Dolmen_loop.Typer.T)
- env s
- (fun a -> Expr.Term.apply_cst abs_real [] [ a ]))
+ app1 env s abs_real
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "colibri_abs_int" }
+ ->
+ app1 env s abs_int
+ | Dolmen_loop.Typer.T.Id
+ { ns = Term; name = Simple "colibri_pow_int_int" } ->
+ app2 env s colibri_pow_int_int
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "colibri_cdiv" } ->
+ app2 env s colibri_cdiv
+ | Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "colibri_crem" } ->
+ app2 env s colibri_crem
| Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "bv2nat" } ->
`Term
(Dolmen_type.Base.term_app1
@@ -132,19 +177,21 @@ let init_ty d =
Some seq
| _ -> None)
+exception Wrong_arg
+
+let unsigned_bitv n t =
+ if not (Q.is_unsigned_integer n t) then raise Wrong_arg;
+ t.Q.num
+
+let signed_bitv n t = Z.signed_extract (unsigned_bitv n t) 0 n
+
module Check = struct
let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
- exception Wrong_arg
-
let compute_ground d t =
let ( !> ) t = RealValue.value (RealValue.coerce_nodevalue (interp d t)) in
- let bitv n t =
- let t = !>t in
- if not (Q.is_unsigned_integer n t) then raise Wrong_arg;
- t.Q.num
- in
- let signed_bitv n t = Z.signed_extract (bitv n t) 0 n in
+ let bitv n t = unsigned_bitv n !>t in
+ let signed_bitv n t = signed_bitv n !>t in
let ( !< ) v = `Some (RealValue.nodevalue (RealValue.index v)) in
let ( !<< ) b =
let r = if b then Boolean.values_true else Boolean.values_false in
@@ -230,6 +277,12 @@ module Check = struct
let b = !>b in
let s = Q.sign b in
if s = 0 then `Uninterp else !<(Q.mod_t !>a b)
+ | { app = { builtin = Builtin.Pow_int_int }; tyargs = []; args; ty = _ } ->
+ let a, b = IArray.extract2_exn args in
+ let a = !>a in
+ let b = !>b in
+ if Q.sign b < 0 && Q.sign a = 0 then `Uninterp
+ else !<(Q.pow a (Q.to_int b))
| { app = { builtin = Expr.Lt }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
!<<(Q.lt !>a !>b)
@@ -245,8 +298,7 @@ module Check = struct
| { app = { builtin = Expr.Floor_to_int }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
!<(Q.floor !>a)
- | { app = { builtin = Expr.Abs | Builtin.Abs_real }; tyargs = []; args; _ }
- ->
+ | { app = { builtin = Expr.Abs }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
!<(Q.abs !>a)
| { app = { builtin = Expr.Bitvec s }; tyargs = []; args; ty = _ } ->
@@ -586,7 +638,7 @@ let converter d (f : Ground.t) =
let a = IArray.extract1_exn args in
reg a;
Check.attach d f
- | { app = { builtin = Expr.Abs | Builtin.Abs_real }; tyargs = []; args; _ } ->
+ | { app = { builtin = Expr.Abs }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
reg a;
Check.attach d f
diff --git a/src_colibri2/theories/LRA/realValue.mli b/src_colibri2/theories/LRA/realValue.mli
index 2cefb591c..9b8794bd7 100644
--- a/src_colibri2/theories/LRA/realValue.mli
+++ b/src_colibri2/theories/LRA/realValue.mli
@@ -19,9 +19,13 @@
(*************************************************************************)
module Builtin : sig
- type _ Expr.t += Abs_real
+ type _ Expr.t += BV2Nat of int
val abs_real : Colibri2_core.Expr.Term.Const.t
+
+ val abs_int : Colibri2_core.Expr.Term.Const.t
+
+ val bv2nat : int -> Colibri2_core.Expr.Term.Const.t
end
include Value.S with type s = Q.t
@@ -37,3 +41,7 @@ val init : Egraph.wt -> unit
val int_sequence : Z.t Base.Sequence.t
val q_sequence : _ Egraph.t -> Q.t Interp.SeqLim.t
+
+val unsigned_bitv : int -> Q.t -> Z.t
+
+val signed_bitv : int -> Q.t -> Z.t
--
GitLab