Hi,
The following simple patch adds support for rem, which was somehow removed in
56ac17d0ecdf686bbd10c230629700948a354296. It also slightly updates the heading
comment.
Floriandiff --git a/drivers/smt-libv2-floats.gen b/drivers/smt-libv2-floats.gen
index 23ee38434..7790d552b 100644
--- a/drivers/smt-libv2-floats.gen
+++ b/drivers/smt-libv2-floats.gen
@@ -11,6 +11,7 @@ theory ieee_float.GenericFloat
(* Part I *)
syntax function abs "(fp.abs %1)"
syntax function neg "(fp.neg %1)"
+ syntax function rem "(fp.rem %1 %2)"
syntax function add "(fp.add %1 %2 %3)"
syntax function sub "(fp.sub %1 %2 %3)"
diff --git a/theories/ieee_float.why b/theories/ieee_float.why
index 15b0cdb4a..c74a62479 100644
--- a/theories/ieee_float.why
+++ b/theories/ieee_float.why
@@ -5,15 +5,15 @@
A note on intended semantics: we use the same idea as the SMTLIB floating
point theory, that defers any inconsistencies to the "parent" document.
Hence, in doubt, the correct axiomatisation is one that implements
- [BTRW14] "An Automatable Formal Semantics for IEEE-754 Floating-Point
+ [BTRW15] "An Automatable Formal Semantics for IEEE-754 Floating-Point
Arithmetic", which in turn defers any inconsistencies to IEEE-754.
This theory is split into two parts: the first part talks about IEEE
operations and this is what you should use as a user, the second part is
internal only and is an axiomatisation for the provers that do not
natively support floating point. You should not use any symbols you find
- there in your verification conditions as solvers with native floating
- point support will leave them uninterpreted.
+ there in your verification conditions as drivers for solvers with native
+ floating point support will leave them uninterpreted.
*)
(** {2 Rounding Modes} *)
@@ -78,6 +78,7 @@ theory GenericFloat
function abs t : t (** Absolute value *)
function neg t : t (** Opposite *)
+ function rem t t : t (** Remainder *)
function fma mode t t t : t (** Fused multiply-add: x * y + z *)
function sqrt mode t : t (** Square root *)
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
