Commit 975e611d authored by MARCHE Claude's avatar MARCHE Claude

more support for full floats

parent 112fa782
......@@ -36,7 +36,7 @@
expanded="true">
<goal
name="Round_single_01"
sum="4350d059bf72b21b36729eaccc394959"
sum="b356284ef3c67cc31bb22f6c7deae9f0"
proved="true"
expanded="true"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.99999ap-4">
......@@ -50,7 +50,7 @@
</goal>
<goal
name="Round_double_01"
sum="fc4b69caf28748e651e23f375e300b70"
sum="a981e04c08472362dcca34e0f3487b74"
proved="true"
expanded="true"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
......@@ -64,7 +64,7 @@
</goal>
<goal
name="Test00"
sum="d126875bf4fc484b4b44c2b52b9da437"
sum="532babe00b8785ec6f7286621c12a512"
proved="true"
expanded="true"
shape="ainfix <=aprefix -c3.0V0Iainfix <=aabsV0c2.0F">
......@@ -73,21 +73,21 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="gappa"
......@@ -99,7 +99,7 @@
</goal>
<goal
name="Test01"
sum="bcbfbae3da81b362e99b319253ef2a20"
sum="a2dc5970c8ef3c553ea90e0fc634da83"
proved="true"
expanded="true"
shape="ainfix <=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix <=avalueV0c2.0Aainfix <=aprefix -c2.0avalueV0F">
......@@ -113,7 +113,7 @@
</goal>
<goal
name="Test02"
sum="1d3e20e12a14b6bd91a25d057da3b098"
sum="eb102544c66926067fe7350ea3f1ba87"
proved="true"
expanded="true"
shape="ainfix <=aabsainfix -ainfix *avalueV1avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix =V1V0Iainfix <=aabsavalueV0c2.0F">
......@@ -127,7 +127,7 @@
</goal>
<goal
name="Test03"
sum="42c26c3443d67722883a37dfe8f9253c"
sum="3d36d4470fa7e12c3ba550960abf7a6c"
proved="true"
expanded="true"
shape="ainfix <=asqrtainfix *ainfix -avalueV2ainfix *avalueV0avalueV0ainfix -avalueV1ainfix *avalueV0avalueV0c0x1.p-52Iainfix =V2V1Iainfix =avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix <=aabsavalueV0c2.0F">
......
......@@ -81,7 +81,47 @@ theory GenFloat
axiom Round_up_neg:
forall x:real. round Up (-x) = - round Down x
end
theory Single
type single
function max_single : real = 0x1.FFFFFEp127
function max_int : int = 16777216 (* 2^24 *)
clone export GenFloat with
type t = single,
function max = max_single,
function max_representable_integer = max_int
end
theory Double
type double
function max_double : real = 0x1.FFFFFFFFFFFFFp1023
function max_int : int = 9007199254740992 (* 2^23 *)
clone export GenFloat with
type t = double,
function max = max_double,
function max_representable_integer = max_int
end
theory GenFloatFull
use import SpecialValues
use import Rounding
use import real.Real
clone export GenFloat
(* special values *)
function class t : class
......@@ -103,50 +143,55 @@ theory GenFloat
predicate is_gen_zero_plus (x:t) = is_gen_zero x /\ sign x = Pos
predicate is_gen_zero_minus (x:t) = is_gen_zero x /\ sign x = Neg
predicate le (x:t) (y:t) =
predicate le_full (x:t) (y:t) =
(is_finite x /\ is_finite y /\ value x <= value y)
\/ (is_minus_infinity x /\ is_not_NaN y)
\/ (is_not_NaN x /\ is_plus_infinity y)
predicate lt (x:t) (y:t) =
predicate lt_full (x:t) (y:t) =
(is_finite x /\ is_finite y /\ value x < value y)
\/ (is_minus_infinity x /\ is_not_NaN y /\ not (is_minus_infinity y))
\/ (is_not_NaN x /\ not (is_plus_infinity x) /\ is_plus_infinity y)
predicate ge (x:t) (y:t) = le y x
predicate ge_full (x:t) (y:t) = le_full y x
predicate gt (x:t) (y:t) = lt y x
predicate gt_full (x:t) (y:t) = lt_full y x
predicate eq (x:t) (y:t) =
predicate eq_full (x:t) (y:t) =
is_not_NaN x /\ is_not_NaN y /\
((is_finite x /\ is_finite y /\ value x = value y) \/
(is_infinite x /\ is_infinite y /\ same_sign x y))
predicate ne (x:t) (y:t) = not (eq x y)
predicate ne_full (x:t) (y:t) = not (eq_full x y)
lemma le_lt_trans: forall x y z:t. le x y /\ lt y z -> lt x z
lemma le_lt_full_trans:
forall x y z:t. le_full x y /\ lt_full y z -> lt_full x z
lemma lt_le_trans: forall x y z:t. lt x y /\ le y z -> lt x z
lemma lt_le_full_trans:
forall x y z:t. lt_full x y /\ le_full y z -> lt_full x z
lemma le_ge_asym: forall x y:t. le x y /\ ge x y -> eq x y
lemma le_ge_full_asym:
forall x y:t. le_full x y /\ ge_full x y -> eq_full x y
lemma not_lt_ge: forall x y:t.
not (lt x y) /\ is_not_NaN x /\ is_not_NaN y -> ge x y
lemma not_lt_ge_full: forall x y:t.
not (lt_full x y) /\ is_not_NaN x /\ is_not_NaN y -> ge_full x y
lemma not_gt_le: forall x y:t.
not (gt x y) /\ is_not_NaN x /\ is_not_NaN y -> le x y
lemma not_gt_le_full: forall x y:t.
not (gt_full x y) /\ is_not_NaN x /\ is_not_NaN y -> le_full x y
end
theory Single
theory SingleFull
type single
function max_single : real = 0x1.FFFFFEp127
function max_int : int = 16777216 (* 2^24 *)
clone export GenFloat with
clone export GenFloatFull with
type t = single,
function max = max_single,
function max_representable_integer = max_int
......@@ -155,18 +200,16 @@ end
theory Double
theory DoubleFull
type double
function max_double : real = 0x1.FFFFFFFFFFFFFp1023
function max_int : int = 9007199254740992 (* 2^23 *)
clone export GenFloat with
clone export GenFloatFull with
type t = double,
function max = max_double,
function max_representable_integer = max_int
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment