diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index fb7c5b65596e40857035a027327456753682af85..01bee760bc64463e08ad5866aea4f2186bc94c59 100644
--- a/config/caisar-detection-data.conf
+++ b/config/caisar-detection-data.conf
@@ -27,6 +27,6 @@ exec = "pyrat.py"
version_switch = "--version"
version_regexp = "PyRAT \\([0-9.]+\\)"
version_ok = "1.0"
-command = "%e --timeout %t %f"
-driver = "drivers/pyrat"
+command = "%e %f"
+driver = "caisar_drivers/pyrat.drv"
use_at_auto_level = 1
diff --git a/config/drivers/pyrat.drv b/config/drivers/pyrat.drv
index 0a07e0cfbfb0bf2e7d4d1736a5ad5c608d6146b3..6c21b2b1c93ad95f30422e0fba2a26ad54d6685b 100644
--- a/config/drivers/pyrat.drv
+++ b/config/drivers/pyrat.drv
@@ -1 +1,201 @@
(* Why3 drivers for PyRAT *)
+
+(* additional regexp for detection of answers, needed for alt-ergo <= 0.99 *)
+valid "^Inconsistent assumption$"
+
+
+printer "alt-ergo"
+filename "%f-%t-%g.why"
+
+valid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Valid"
+invalid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Invalid"
+unknown "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:I don't know" ""
+timeout "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Timeout"
+timeout "^Timeout$"
+steplimitexceeded "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Steps limit reached"
+outofmemory "Fatal error: out of memory"
+outofmemory "Fatal error: exception Stack_overflow"
+fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
+time "Valid (%s)"
+time "Valid (%s)"
+steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\))" 2
+steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\) steps)" 2
+time "why3cpulimit time : %s s"
+
+transformation "inline_trivial"
+
+transformation "eliminate_builtin"
+transformation "eliminate_recursion"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic"
+transformation "eliminate_literal"
+transformation "eliminate_epsilon"
+transformation "eliminate_let_term"
+transformation "split_premise_right"
+transformation "simplify_formula"
+
+theory BuiltIn
+ syntax type int "int"
+ syntax type real "real"
+
+ syntax predicate (=) "(%1 = %2)"
+
+ meta "eliminate_algebraic" "keep_enums"
+ meta "eliminate_algebraic" "keep_recs"
+
+end
+
+theory int.Int
+
+ prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"
+
+ syntax function zero "0"
+ syntax function one "1"
+
+ syntax function (+) "(%1 + %2)"
+ syntax function (-) "(%1 - %2)"
+ syntax function (*) "(%1 * %2)"
+ syntax function (-_) "(-%1)"
+
+ meta "invalid trigger" predicate (<=)
+ meta "invalid trigger" predicate (<)
+ meta "invalid trigger" predicate (>=)
+ meta "invalid trigger" predicate (>)
+
+ syntax predicate (<=) "(%1 <= %2)"
+ syntax predicate (<) "(%1 < %2)"
+ syntax predicate (>=) "(%1 >= %2)"
+ syntax predicate (>) "(%1 > %2)"
+
+ remove prop MulComm.Comm
+ remove prop MulAssoc.Assoc
+ remove prop Unit_def_l
+ remove prop Unit_def_r
+ remove prop Inv_def_l
+ remove prop Inv_def_r
+ remove prop Assoc
+ remove prop Mul_distr_l
+ remove prop Mul_distr_r
+ remove prop Comm
+ remove prop Unitary
+ remove prop Refl
+ remove prop Trans
+ remove prop Total
+ remove prop Antisymm
+ remove prop NonTrivialRing
+ remove prop CompatOrderAdd
+ remove prop ZeroLessOne
+
+end
+
+theory int.EuclideanDivision
+
+ syntax function div "(%1 / %2)"
+ syntax function mod "(%1 % %2)"
+
+end
+
+theory int.ComputerDivision
+
+ use for_drivers.ComputerOfEuclideanDivision
+
+end
+
+
+theory real.Real
+
+ prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"
+
+ syntax function zero "0.0"
+ syntax function one "1.0"
+
+ syntax function (+) "(%1 + %2)"
+ syntax function (-) "(%1 - %2)"
+ syntax function (*) "(%1 * %2)"
+ syntax function (/) "(%1 / %2)"
+ syntax function (-_) "(-%1)"
+ syntax function inv "(1.0 / %1)"
+
+ meta "invalid trigger" predicate (<=)
+ meta "invalid trigger" predicate (<)
+ meta "invalid trigger" predicate (>=)
+ meta "invalid trigger" predicate (>)
+
+ syntax predicate (<=) "(%1 <= %2)"
+ syntax predicate (<) "(%1 < %2)"
+ syntax predicate (>=) "(%1 >= %2)"
+ syntax predicate (>) "(%1 > %2)"
+
+ remove prop MulComm.Comm
+ remove prop MulAssoc.Assoc
+ remove prop Unit_def_l
+ remove prop Unit_def_r
+ remove prop Inv_def_l
+ remove prop Inv_def_r
+ remove prop Assoc
+ remove prop Mul_distr_l
+ remove prop Mul_distr_r
+ remove prop Comm
+ remove prop Unitary
+ remove prop Refl
+ remove prop Trans
+ remove prop Total
+ remove prop Antisymm
+ remove prop Inverse
+ remove prop NonTrivialRing
+ remove prop CompatOrderAdd
+ remove prop ZeroLessOne
+
+end
+
+theory real.RealInfix
+
+ syntax function (+.) "(%1 + %2)"
+ syntax function (-.) "(%1 - %2)"
+ syntax function ( *.) "(%1 * %2)"
+ syntax function (/.) "(%1 / %2)"
+ syntax function (-._) "(-%1)"
+
+ meta "invalid trigger" predicate (<=.)
+ meta "invalid trigger" predicate (<.)
+ meta "invalid trigger" predicate (>=.)
+ meta "invalid trigger" predicate (>.)
+
+ syntax predicate (<=.) "(%1 <= %2)"
+ syntax predicate (<.) "(%1 < %2)"
+ syntax predicate (>=.) "(%1 >= %2)"
+ syntax predicate (>.) "(%1 > %2)"
+
+end
+
+theory Bool
+ syntax type bool "bool"
+ syntax function True "true"
+ syntax function False "false"
+end
+
+theory Tuple0
+ syntax type tuple0 "unit"
+ syntax function Tuple0 "void"
+end
+
+theory algebra.AC
+ meta AC function op
+ remove prop Comm
+ remove prop Assoc
+end
+
+theory HighOrd
+ syntax type (->) "(%1,%2) farray"
+ syntax function (@) "(%1[%2])"
+end
+
+theory map.Map
+ syntax function get "(%1[%2])"
+ syntax function set "(%1[%2 <- %3])"
+end
+
+theory ieee_float.Float64
+ syntax predicate is_not_nan ""
+ remove allprops
+end
diff --git a/config/dune b/config/dune
index f1aaaab0addab9813c2381ff31de72070d539a85..bd74fc9e54339523e4580c0730c4728a9cc4e2d8 100644
--- a/config/dune
+++ b/config/dune
@@ -1,4 +1,6 @@
(install
(section (site (caisar config)))
- (files caisar-detection-data.conf)
+ (files caisar-detection-data.conf
+ (drivers/pyrat.drv as drivers/pyrat.drv)
+ )
(package caisar))
diff --git a/src/autodetection.ml b/src/autodetection.ml
index 80435a03342219d8ff8b3b35b58ffd5a1d7fc501..f3984ac7faccb559ac8ebcfb3db24d7694d330c9 100644
--- a/src/autodetection.ml
+++ b/src/autodetection.ml
@@ -19,7 +19,9 @@ let rec lookup_file dirs filename =
let autodetect ~debug () =
let open Why3 in
if debug then Debug.set_flag Autodetection.debug;
- let caisar_conf = lookup_file Dirs.Sites.config "caisar-detection-data.conf" in
+ let caisar_conf =
+ lookup_file Dirs.Sites.config "caisar-detection-data.conf"
+ in
let data = Autodetection.Prover_autodetection_data.from_file caisar_conf in
let config = Whyconf.init_config (Some null) in
let binaries = Autodetection.request_binaries_version config data in
diff --git a/src/main.ml b/src/main.ml
index c22b8dc970ede6879fb4c927055d1b9e9fe16e2b..c4ea8291114014035fd962818d426c2b233ef26f 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -59,8 +59,8 @@ let config detect () =
provers)
end
-let verify format loadpath files =
- List.iter ~f:(Verification.verify format loadpath) files
+let verify format loadpath files prover =
+ List.iter ~f:(fun x -> Verification.verify format loadpath x prover) files
let exec_cmd cmdname cmd =
Logs.debug (fun m -> m "Command `%s'." cmdname);
@@ -121,6 +121,10 @@ let verify_cmd =
let doc = "additional loadpath" in
Arg.(value & opt_all string [] & info [ "L" ] ~doc)
in
+ let prover =
+ let doc = "Prover to use" in
+ Arg.(required & opt (some string) None & info [ "prover" ] ~doc)
+ in
let doc = "Property verification of neural networks." in
let exits = Term.default_exits in
let man =
@@ -130,9 +134,10 @@ let verify_cmd =
in
( Term.(
ret
- (const (fun format loadpath files ->
- `Ok (exec_cmd cmdname (fun () -> verify format loadpath files)))
- $ format $ loadpath $ files)),
+ (const (fun format loadpath files prover ->
+ `Ok
+ (exec_cmd cmdname (fun () -> verify format loadpath files prover)))
+ $ format $ loadpath $ files $ prover)),
Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
let default_cmd =
diff --git a/src/verification.ml b/src/verification.ml
index f4ba6da943c70b5317ba43aa0caf6d48030383e7..54088494542baef589c6ff8e8d60a4ecf226a556 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -18,9 +18,9 @@ let create_env loadpath =
(loadpath @ stdlib @ Whyconf.loadpath (Whyconf.get_main config)),
config )
-let altergo = Why3.Whyconf.mk_filter_prover "Alt-Ergo"
+let mkfilter prover = Why3.Whyconf.mk_filter_prover prover
-let verify format loadpath file =
+let verify format loadpath file prover =
let open Why3 in
let env, config = create_env loadpath in
let _, mstr_theory =
@@ -34,7 +34,17 @@ let verify format loadpath file =
Wstdlib.Mstr.iter
(fun _ theory ->
let tasks = Task.split_theory theory None None in
- let prover = Whyconf.filter_one_prover config altergo in
- let driver = Whyconf.(load_driver (get_main config) env prover) in
+ let prover = Whyconf.filter_one_prover config (mkfilter prover) in
+ let driver =
+ match String.chop_prefix ~prefix:"caisar_drivers/" prover.driver with
+ | None -> Whyconf.(load_driver (get_main config) env prover)
+ | Some file ->
+ let file =
+ Caml.Filename.concat
+ (Caml.Filename.concat (List.hd_exn Dirs.Sites.config) "drivers")
+ file
+ in
+ Driver.load_driver_absolute env file prover.extra_drivers
+ in
List.iter tasks ~f:(Format.printf "%a" (Driver.print_task driver)))
mstr_theory
diff --git a/tests/autodetect.t b/tests/autodetect.t
index 13344dc8202dcd19199cb4781c5a689799c04822..6f08613f5314de89df20c7c404db55fdd0eb5077 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -1,5 +1,3 @@
Test autodetect
$ caisar config -d
[caisar] Alt-Ergo 2.4.0
- Marabou 1.0.+
- PyRAT 1.0
diff --git a/tests/simple.t b/tests/simple.t
index c5d8729b3373d9c0720660b62d0ce091a5892ad9..56a0a7502052c0afdb26e826bb70fec3f101e6c4 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -1,5 +1,19 @@
Test verify
- $ caisar verify -L . --format whyml - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9./]*/$TMPFILE/'
+ $ mkdir bin
+
+ $ cat - > bin/pyrat.py << EOF
+ > #!/bin/sh
+ > echo "PyRAT 1.0"
+ > EOF
+
+ $ chmod u+x bin/pyrat.py
+
+ $ bin/pyrat.py
+ PyRAT 1.0
+
+ $ PATH=$(pwd)/bin:$PATH
+
+ $ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9./]*/$TMPFILE/'
> theory T
> use TestNetwork.AsTuple
> use ieee_float.Float64
@@ -14,6 +28,9 @@ Test verify
<autodetect>0 prover(s) added
<autodetect>Generating strategies:
<autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
+ <autodetect>command 'Marabou --version' failed. Output:
+ sh: 1: Marabou: not found
+
<autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
<autodetect>Run: (alt-ergo-2.4.0 --version) > $TMPFILE 2>&1
<autodetect>command 'alt-ergo-2.4.0 --version' failed. Output:
@@ -21,10 +38,8 @@ Test verify
<autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Found prover Alt-Ergo version 2.4.0, OK.
- <autodetect>Found prover Marabou version 1.0.+, OK.
<autodetect>Found prover PyRAT version 1.0, OK.
- <autodetect>3 prover(s) added
- (* this is the prelude for Alt-Ergo, version >= 2.4.0 *)
+ <autodetect>2 prover(s) added
(* this is a prelude for Alt-Ergo integer arithmetic *)
(* this is a prelude for Alt-Ergo real arithmetic *)
type string
@@ -406,205 +421,30 @@ Test verify
predicate is_minus_zero(x: t) = (is_zero(x) and is_negative(x))
- predicate is_not_nan(x: t) = (tqtisFinite(x) or is_infinite(x))
-
- axiom is_not_nan1 : (forall x:t. (is_not_nan(x) -> (not is_nan(x))))
-
- axiom is_not_nan2 : (forall x:t. ((not is_nan(x)) -> is_not_nan(x)))
-
- axiom is_not_finite :
- (forall x:t. ((not tqtisFinite(x)) -> (is_infinite(x) or is_nan(x))))
-
- axiom is_not_finite1 :
- (forall x:t. ((is_infinite(x) or is_nan(x)) -> (not tqtisFinite(x))))
-
- axiom zeroF_is_positive : is_positive(zeroF)
-
- axiom zeroF_is_zero : is_zero(zeroF)
-
- axiom zero_to_real :
- (forall x:t [is_zero(x)]. (is_zero(x) -> tqtisFinite(x)))
-
- axiom zero_to_real1 :
- (forall x:t [is_zero(x)]. (is_zero(x) -> (tqtreal(x) = 0.0)))
-
- axiom zero_to_real2 :
- (forall x:t [is_zero(x)]. ((tqtisFinite(x) and (tqtreal(x) = 0.0)) ->
- is_zero(x)))
-
logic of_int : mode, int -> t
logic to_int : mode, t -> int
- axiom zero_of_int : (forall m:mode. (zeroF = of_int(m, 0)))
-
logic round : mode, real -> real
logic max_int1 : int
- axiom max_real_int : (0x1.FFFFFFFFFFFFFp1023 = from_int(max_int1))
-
predicate in_range(x: real) = (((-0x1.FFFFFFFFFFFFFp1023) <= x) and
(x <= 0x1.FFFFFFFFFFFFFp1023))
predicate in_int_range(i: int) = (((-max_int1) <= i) and (i <= max_int1))
- axiom is_finite : (forall x:t. (tqtisFinite(x) -> in_range(tqtreal(x))))
-
predicate no_overflow(m: mode, x: real) = in_range(round(m, x))
- axiom Bounded_real_no_overflow :
- (forall m:mode. forall x:real. (in_range(x) -> no_overflow(m, x)))
-
- axiom Round_monotonic :
- (forall m:mode. forall x:real. forall y:real. ((x <= y) -> (round(m,
- x) <= round(m, y))))
-
- axiom Round_idempotent :
- (forall m1:mode. forall m2:mode. forall x:real. (round(m1, round(m2,
- x)) = round(m2, x)))
-
- axiom Round_to_real :
- (forall m:mode. forall x:t. (tqtisFinite(x) -> (round(m,
- tqtreal(x)) = tqtreal(x))))
-
- axiom Round_down_le : (forall x:real. (round(RTN, x) <= x))
-
- axiom Round_up_ge : (forall x:real. (x <= round(RTP, x)))
-
- axiom Round_down_neg : (forall x:real. (round(RTN, (-x)) = (-round(RTP, x))))
-
- axiom Round_up_neg : (forall x:real. (round(RTP, (-x)) = (-round(RTN, x))))
-
predicate in_safe_int_range(i: int) = (((-9007199254740992) <= i) and
(i <= 9007199254740992))
- axiom Exact_rounding_for_integers :
- (forall m:mode. forall i:int. (in_safe_int_range(i) -> (round(m,
- from_int(i)) = from_int(i))))
-
predicate same_sign(x: t, y: t) = ((is_positive(x) and is_positive(y)) or
(is_negative(x) and is_negative(y)))
predicate diff_sign(x: t, y: t) = ((is_positive(x) and is_negative(y)) or
(is_negative(x) and is_positive(y)))
- axiom feq_eq :
- (forall x:t. forall y:t. (tqtisFinite(x) -> (tqtisFinite(y) ->
- ((not is_zero(x)) -> (eq(x, y) -> (x = y))))))
-
- axiom eq_feq :
- (forall x:t. forall y:t. (tqtisFinite(x) -> (tqtisFinite(y) -> ((x = y) ->
- eq(x, y)))))
-
- axiom eq_refl : (forall x:t. (tqtisFinite(x) -> eq(x, x)))
-
- axiom eq_sym : (forall x:t. forall y:t. (eq(x, y) -> eq(y, x)))
-
- axiom eq_trans :
- (forall x:t. forall y:t. forall z:t. (eq(x, y) -> (eq(y, z) -> eq(x, z))))
-
- axiom eq_zero : eq(zeroF, neg(zeroF))
-
- axiom eq_to_real_finite :
- (forall x:t. forall y:t. ((tqtisFinite(x) and tqtisFinite(y)) -> (eq(x,
- y) -> (tqtreal(x) = tqtreal(y)))))
-
- axiom eq_to_real_finite1 :
- (forall x:t. forall y:t. ((tqtisFinite(x) and tqtisFinite(y)) ->
- ((tqtreal(x) = tqtreal(y)) -> eq(x, y))))
-
- axiom eq_special : (forall x:t. forall y:t. (eq(x, y) -> is_not_nan(x)))
-
- axiom eq_special1 : (forall x:t. forall y:t. (eq(x, y) -> is_not_nan(y)))
-
- axiom eq_special2 :
- (forall x:t. forall y:t. (eq(x, y) -> ((tqtisFinite(x) and
- tqtisFinite(y)) or (is_infinite(x) and (is_infinite(y) and same_sign(x,
- y))))))
-
- axiom lt_finite :
- (forall x:t. forall y:t [lt(x, y)]. ((tqtisFinite(x) and tqtisFinite(y)) ->
- (lt(x, y) -> (tqtreal(x) < tqtreal(y)))))
-
- axiom lt_finite1 :
- (forall x:t. forall y:t [lt(x, y)]. ((tqtisFinite(x) and tqtisFinite(y)) ->
- ((tqtreal(x) < tqtreal(y)) -> lt(x, y))))
-
- axiom le_finite :
- (forall x:t. forall y:t [le(x, y)]. ((tqtisFinite(x) and tqtisFinite(y)) ->
- (le(x, y) -> (tqtreal(x) <= tqtreal(y)))))
-
- axiom le_finite1 :
- (forall x:t. forall y:t [le(x, y)]. ((tqtisFinite(x) and tqtisFinite(y)) ->
- ((tqtreal(x) <= tqtreal(y)) -> le(x, y))))
-
- axiom le_lt_trans :
- (forall x:t. forall y:t. forall z:t. ((le(x, y) and lt(y, z)) -> lt(x, z)))
-
- axiom lt_le_trans :
- (forall x:t. forall y:t. forall z:t. ((lt(x, y) and le(y, z)) -> lt(x, z)))
-
- axiom le_ge_asym :
- (forall x:t. forall y:t. ((le(x, y) and le(y, x)) -> eq(x, y)))
-
- axiom not_lt_ge :
- (forall x:t. forall y:t. (((not lt(x, y)) and (is_not_nan(x) and
- is_not_nan(y))) -> le(y, x)))
-
- axiom not_gt_le :
- (forall x:t. forall y:t. (((not lt(y, x)) and (is_not_nan(x) and
- is_not_nan(y))) -> le(x, y)))
-
- axiom le_special :
- (forall x:t. forall y:t [le(x, y)]. (le(x, y) -> ((tqtisFinite(x) and
- tqtisFinite(y)) or ((is_minus_infinity(x) and is_not_nan(y)) or
- (is_not_nan(x) and is_plus_infinity(y))))))
-
- axiom lt_special :
- (forall x:t. forall y:t [lt(x, y)]. (lt(x, y) -> ((tqtisFinite(x) and
- tqtisFinite(y)) or ((is_minus_infinity(x) and (is_not_nan(y) and
- (not is_minus_infinity(y)))) or (is_not_nan(x) and
- ((not is_plus_infinity(x)) and is_plus_infinity(y)))))))
-
- axiom lt_lt_finite :
- (forall x:t. forall y:t. forall z:t. (lt(x, y) -> (lt(y, z) ->
- tqtisFinite(y))))
-
- axiom positive_to_real :
- (forall x:t [is_positive(x)]. (tqtisFinite(x) -> (is_positive(x) ->
- (0.0 <= tqtreal(x)))))
-
- axiom to_real_positive :
- (forall x:t [is_positive(x)]. (tqtisFinite(x) -> ((0.0 < tqtreal(x)) ->
- is_positive(x))))
-
- axiom negative_to_real :
- (forall x:t [is_negative(x)]. (tqtisFinite(x) -> (is_negative(x) ->
- (tqtreal(x) <= 0.0))))
-
- axiom to_real_negative :
- (forall x:t [is_negative(x)]. (tqtisFinite(x) -> ((tqtreal(x) < 0.0) ->
- is_negative(x))))
-
- axiom negative_xor_positive :
- (forall x:t. (not (is_positive(x) and is_negative(x))))
-
- axiom negative_or_positive :
- (forall x:t. (is_not_nan(x) -> (is_positive(x) or is_negative(x))))
-
- axiom diff_sign_trans :
- (forall x:t. forall y:t. forall z:t. ((diff_sign(x, y) and diff_sign(y,
- z)) -> same_sign(x, z)))
-
- axiom diff_sign_product :
- (forall x:t. forall y:t. ((tqtisFinite(x) and (tqtisFinite(y) and
- ((tqtreal(x) * tqtreal(y)) < 0.0))) -> diff_sign(x, y)))
-
- axiom same_sign_product :
- (forall x:t. forall y:t. ((tqtisFinite(x) and (tqtisFinite(y) and
- same_sign(x, y))) -> (0.0 <= (tqtreal(x) * tqtreal(y)))))
-
predicate product_sign(z: t, x: t, y: t) = ((same_sign(x, y) ->
is_positive(z)) and (diff_sign(x, y) -> is_negative(z)))
@@ -623,180 +463,6 @@ Test verify
is_positive(x))) and ((m = RTN) -> is_negative(x))) and ((m = RTZ) ->
is_positive(x))))
- axiom add_finite :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. (tqtisFinite(x) ->
- (tqtisFinite(y) -> (no_overflow(m, (tqtreal(x) + tqtreal(y))) ->
- tqtisFinite(add(m, x, y))))))
-
- axiom add_finite1 :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. (tqtisFinite(x) ->
- (tqtisFinite(y) -> (no_overflow(m, (tqtreal(x) + tqtreal(y))) ->
- (tqtreal(add(m, x, y)) = round(m, (tqtreal(x) + tqtreal(y))))))))
-
- axiom add_finite_rev :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. (tqtisFinite(add(m,
- x, y)) -> tqtisFinite(x)))
-
- axiom add_finite_rev1 :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. (tqtisFinite(add(m,
- x, y)) -> tqtisFinite(y)))
-
- axiom add_finite_rev_n :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. (to_nearest(m) ->
- (tqtisFinite(add(m, x, y)) -> no_overflow(m, (tqtreal(x) + tqtreal(y))))))
-
- axiom add_finite_rev_n1 :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. (to_nearest(m) ->
- (tqtisFinite(add(m, x, y)) -> (tqtreal(add(m, x, y)) = round(m,
- (tqtreal(x) + tqtreal(y)))))))
-
- axiom sub_finite :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. (tqtisFinite(x) ->
- (tqtisFinite(y) -> (no_overflow(m, (tqtreal(x) - tqtreal(y))) ->
- tqtisFinite(sub(m, x, y))))))
-
- axiom sub_finite1 :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. (tqtisFinite(x) ->
- (tqtisFinite(y) -> (no_overflow(m, (tqtreal(x) - tqtreal(y))) ->
- (tqtreal(sub(m, x, y)) = round(m, (tqtreal(x) - tqtreal(y))))))))
-
- axiom sub_finite_rev :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. (tqtisFinite(sub(m,
- x, y)) -> tqtisFinite(x)))
-
- axiom sub_finite_rev1 :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. (tqtisFinite(sub(m,
- x, y)) -> tqtisFinite(y)))
-
- axiom sub_finite_rev_n :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. (to_nearest(m) ->
- (tqtisFinite(sub(m, x, y)) -> no_overflow(m, (tqtreal(x) - tqtreal(y))))))
-
- axiom sub_finite_rev_n1 :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. (to_nearest(m) ->
- (tqtisFinite(sub(m, x, y)) -> (tqtreal(sub(m, x, y)) = round(m,
- (tqtreal(x) - tqtreal(y)))))))
-
- axiom mul_finite :
- (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. (tqtisFinite(x) ->
- (tqtisFinite(y) -> (no_overflow(m, (tqtreal(x) * tqtreal(y))) ->
- tqtisFinite(mul(m, x, y))))))
-
- axiom mul_finite1 :
- (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. (tqtisFinite(x) ->
- (tqtisFinite(y) -> (no_overflow(m, (tqtreal(x) * tqtreal(y))) ->
- (tqtreal(mul(m, x, y)) = round(m, (tqtreal(x) * tqtreal(y))))))))
-
- axiom mul_finite_rev :
- (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. (tqtisFinite(mul(m,
- x, y)) -> tqtisFinite(x)))
-
- axiom mul_finite_rev1 :
- (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. (tqtisFinite(mul(m,
- x, y)) -> tqtisFinite(y)))
-
- axiom mul_finite_rev_n :
- (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. (to_nearest(m) ->
- (tqtisFinite(mul(m, x, y)) -> no_overflow(m, (tqtreal(x) * tqtreal(y))))))
-
- axiom mul_finite_rev_n1 :
- (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. (to_nearest(m) ->
- (tqtisFinite(mul(m, x, y)) -> (tqtreal(mul(m, x, y)) = round(m,
- (tqtreal(x) * tqtreal(y)))))))
-
- axiom div_finite :
- (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. (tqtisFinite(x) ->
- (tqtisFinite(y) -> ((not is_zero(y)) -> (no_overflow(m,
- (tqtreal(x) / tqtreal(y))) -> tqtisFinite(div(m, x, y)))))))
-
- axiom div_finite1 :
- (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. (tqtisFinite(x) ->
- (tqtisFinite(y) -> ((not is_zero(y)) -> (no_overflow(m,
- (tqtreal(x) / tqtreal(y))) -> (tqtreal(div(m, x, y)) = round(m,
- (tqtreal(x) / tqtreal(y)))))))))
-
- axiom div_finite_rev :
- (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. (tqtisFinite(div(m,
- x, y)) -> ((tqtisFinite(x) and (tqtisFinite(y) and (not is_zero(y)))) or
- (tqtisFinite(x) and (is_infinite(y) and (tqtreal(div(m, x, y)) = 0.0))))))
-
- axiom div_finite_rev_n :
- (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. (to_nearest(m) ->
- (tqtisFinite(div(m, x, y)) -> (tqtisFinite(y) -> no_overflow(m,
- (tqtreal(x) / tqtreal(y)))))))
-
- axiom div_finite_rev_n1 :
- (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. (to_nearest(m) ->
- (tqtisFinite(div(m, x, y)) -> (tqtisFinite(y) -> (tqtreal(div(m, x,
- y)) = round(m, (tqtreal(x) / tqtreal(y))))))))
-
- axiom neg_finite :
- (forall x:t [neg(x)]. (tqtisFinite(x) -> tqtisFinite(neg(x))))
-
- axiom neg_finite1 :
- (forall x:t [neg(x)]. (tqtisFinite(x) ->
- (tqtreal(neg(x)) = (-tqtreal(x)))))
-
- axiom neg_finite_rev :
- (forall x:t [neg(x)]. (tqtisFinite(neg(x)) -> tqtisFinite(x)))
-
- axiom neg_finite_rev1 :
- (forall x:t [neg(x)]. (tqtisFinite(neg(x)) ->
- (tqtreal(neg(x)) = (-tqtreal(x)))))
-
- axiom abs_finite :
- (forall x:t [abs1(x)]. (tqtisFinite(x) -> tqtisFinite(abs1(x))))
-
- axiom abs_finite1 :
- (forall x:t [abs1(x)]. (tqtisFinite(x) ->
- (tqtreal(abs1(x)) = abs(tqtreal(x)))))
-
- axiom abs_finite2 :
- (forall x:t [abs1(x)]. (tqtisFinite(x) -> is_positive(abs1(x))))
-
- axiom abs_finite_rev :
- (forall x:t [abs1(x)]. (tqtisFinite(abs1(x)) -> tqtisFinite(x)))
-
- axiom abs_finite_rev1 :
- (forall x:t [abs1(x)]. (tqtisFinite(abs1(x)) ->
- (tqtreal(abs1(x)) = abs(tqtreal(x)))))
-
- axiom abs_universal : (forall x:t [abs1(x)]. (not is_negative(abs1(x))))
-
- axiom fma_finite :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- (tqtisFinite(x) -> (tqtisFinite(y) -> (tqtisFinite(z) -> (no_overflow(m,
- ((tqtreal(x) * tqtreal(y)) + tqtreal(z))) -> tqtisFinite(fma(m, x, y,
- z)))))))
-
- axiom fma_finite1 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- (tqtisFinite(x) -> (tqtisFinite(y) -> (tqtisFinite(z) -> (no_overflow(m,
- ((tqtreal(x) * tqtreal(y)) + tqtreal(z))) -> (tqtreal(fma(m, x, y,
- z)) = round(m, ((tqtreal(x) * tqtreal(y)) + tqtreal(z)))))))))
-
- axiom fma_finite_rev :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- (tqtisFinite(fma(m, x, y, z)) -> tqtisFinite(x)))
-
- axiom fma_finite_rev1 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- (tqtisFinite(fma(m, x, y, z)) -> tqtisFinite(y)))
-
- axiom fma_finite_rev2 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- (tqtisFinite(fma(m, x, y, z)) -> tqtisFinite(z)))
-
- axiom fma_finite_rev_n :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- (to_nearest(m) -> (tqtisFinite(fma(m, x, y, z)) -> no_overflow(m,
- ((tqtreal(x) * tqtreal(y)) + tqtreal(z))))))
-
- axiom fma_finite_rev_n1 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- (to_nearest(m) -> (tqtisFinite(fma(m, x, y, z)) -> (tqtreal(fma(m, x, y,
- z)) = round(m, ((tqtreal(x) * tqtreal(y)) + tqtreal(z)))))))
-
function sqr(x: real) : real = (x * x)
logic sqrt1 : real -> real
@@ -815,550 +481,11 @@ Test verify
(forall x:real. forall y:real. (((0.0 <= x) and (x <= y)) ->
(sqrt1(x) <= sqrt1(y))))
- axiom sqrt_finite :
- (forall m:mode. forall x:t [sqrt(m, x)]. (tqtisFinite(x) ->
- ((0.0 <= tqtreal(x)) -> tqtisFinite(sqrt(m, x)))))
-
- axiom sqrt_finite1 :
- (forall m:mode. forall x:t [sqrt(m, x)]. (tqtisFinite(x) ->
- ((0.0 <= tqtreal(x)) -> (tqtreal(sqrt(m, x)) = round(m,
- sqrt1(tqtreal(x)))))))
-
- axiom sqrt_finite_rev :
- (forall m:mode. forall x:t [sqrt(m, x)]. (tqtisFinite(sqrt(m, x)) ->
- tqtisFinite(x)))
-
- axiom sqrt_finite_rev1 :
- (forall m:mode. forall x:t [sqrt(m, x)]. (tqtisFinite(sqrt(m, x)) ->
- (0.0 <= tqtreal(x))))
-
- axiom sqrt_finite_rev2 :
- (forall m:mode. forall x:t [sqrt(m, x)]. (tqtisFinite(sqrt(m, x)) ->
- (tqtreal(sqrt(m, x)) = round(m, sqrt1(tqtreal(x))))))
-
predicate same_sign_real(x: t, r: real) = ((is_positive(x) and (0.0 < r)) or
(is_negative(x) and (r < 0.0)))
- axiom add_special :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((is_nan(x) or
- is_nan(y)) -> is_nan(add(m, x, y))))
-
- axiom add_special1 :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((tqtisFinite(x) and
- is_infinite(y)) -> is_infinite(add(m, x, y))))
-
- axiom add_special2 :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((tqtisFinite(x) and
- is_infinite(y)) -> same_sign(add(m, x, y), y)))
-
- axiom add_special3 :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((is_infinite(x) and
- tqtisFinite(y)) -> is_infinite(add(m, x, y))))
-
- axiom add_special4 :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((is_infinite(x) and
- tqtisFinite(y)) -> same_sign(add(m, x, y), x)))
-
- axiom add_special5 :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((is_infinite(x) and
- (is_infinite(y) and same_sign(x, y))) -> is_infinite(add(m, x, y))))
-
- axiom add_special6 :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((is_infinite(x) and
- (is_infinite(y) and same_sign(x, y))) -> same_sign(add(m, x, y), x)))
-
- axiom add_special7 :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((is_infinite(x) and
- (is_infinite(y) and diff_sign(x, y))) -> is_nan(add(m, x, y))))
-
- axiom add_special8 :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((tqtisFinite(x) and
- (tqtisFinite(y) and (not no_overflow(m, (tqtreal(x) + tqtreal(y)))))) ->
- same_sign_real(add(m, x, y), (tqtreal(x) + tqtreal(y)))))
-
- axiom add_special9 :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((tqtisFinite(x) and
- (tqtisFinite(y) and (not no_overflow(m, (tqtreal(x) + tqtreal(y)))))) ->
- overflow_value(m, add(m, x, y))))
-
- axiom add_special10 :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((tqtisFinite(x) and
- tqtisFinite(y)) -> (same_sign(x, y) -> same_sign(add(m, x, y), x))))
-
- axiom add_special11 :
- (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((tqtisFinite(x) and
- tqtisFinite(y)) -> ((not same_sign(x, y)) -> sign_zero_result(m, add(m, x,
- y)))))
-
- axiom sub_special :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((is_nan(x) or
- is_nan(y)) -> is_nan(sub(m, x, y))))
-
- axiom sub_special1 :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((tqtisFinite(x) and
- is_infinite(y)) -> is_infinite(sub(m, x, y))))
-
- axiom sub_special2 :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((tqtisFinite(x) and
- is_infinite(y)) -> diff_sign(sub(m, x, y), y)))
-
- axiom sub_special3 :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((is_infinite(x) and
- tqtisFinite(y)) -> is_infinite(sub(m, x, y))))
-
- axiom sub_special4 :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((is_infinite(x) and
- tqtisFinite(y)) -> same_sign(sub(m, x, y), x)))
-
- axiom sub_special5 :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((is_infinite(x) and
- (is_infinite(y) and same_sign(x, y))) -> is_nan(sub(m, x, y))))
-
- axiom sub_special6 :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((is_infinite(x) and
- (is_infinite(y) and diff_sign(x, y))) -> is_infinite(sub(m, x, y))))
-
- axiom sub_special7 :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((is_infinite(x) and
- (is_infinite(y) and diff_sign(x, y))) -> same_sign(sub(m, x, y), x)))
-
- axiom sub_special8 :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((tqtisFinite(x) and
- (tqtisFinite(y) and (not no_overflow(m, (tqtreal(x) - tqtreal(y)))))) ->
- same_sign_real(sub(m, x, y), (tqtreal(x) - tqtreal(y)))))
-
- axiom sub_special9 :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((tqtisFinite(x) and
- (tqtisFinite(y) and (not no_overflow(m, (tqtreal(x) - tqtreal(y)))))) ->
- overflow_value(m, sub(m, x, y))))
-
- axiom sub_special10 :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((tqtisFinite(x) and
- tqtisFinite(y)) -> (diff_sign(x, y) -> same_sign(sub(m, x, y), x))))
-
- axiom sub_special11 :
- (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((tqtisFinite(x) and
- tqtisFinite(y)) -> ((not diff_sign(x, y)) -> sign_zero_result(m, sub(m, x,
- y)))))
-
- axiom mul_special :
- (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. ((is_nan(x) or
- is_nan(y)) -> is_nan(mul(m, x, y))))
-
- axiom mul_special1 :
- (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. ((is_zero(x) and
- is_infinite(y)) -> is_nan(mul(m, x, y))))
-
- axiom mul_special2 :
- (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. ((tqtisFinite(x) and
- (is_infinite(y) and (not is_zero(x)))) -> is_infinite(mul(m, x, y))))
-
- axiom mul_special3 :
- (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. ((is_infinite(x) and
- is_zero(y)) -> is_nan(mul(m, x, y))))
-
- axiom mul_special4 :
- (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. ((is_infinite(x) and
- (tqtisFinite(y) and (not is_zero(y)))) -> is_infinite(mul(m, x, y))))
-
- axiom mul_special5 :
- (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. ((is_infinite(x) and
- is_infinite(y)) -> is_infinite(mul(m, x, y))))
-
- axiom mul_special6 :
- (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. ((tqtisFinite(x) and
- (tqtisFinite(y) and (not no_overflow(m, (tqtreal(x) * tqtreal(y)))))) ->
- overflow_value(m, mul(m, x, y))))
-
- axiom mul_special7 :
- (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. (let r = mul(m, x,
- y) : t in ((not is_nan(r)) -> product_sign(r, x, y))))
-
- axiom div_special :
- (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. ((is_nan(x) or
- is_nan(y)) -> is_nan(div(m, x, y))))
-
- axiom div_special1 :
- (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. ((tqtisFinite(x) and
- is_infinite(y)) -> is_zero(div(m, x, y))))
-
- axiom div_special2 :
- (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. ((is_infinite(x) and
- tqtisFinite(y)) -> is_infinite(div(m, x, y))))
-
- axiom div_special3 :
- (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. ((is_infinite(x) and
- is_infinite(y)) -> is_nan(div(m, x, y))))
-
- axiom div_special4 :
- (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. ((tqtisFinite(x) and
- (tqtisFinite(y) and ((not is_zero(y)) and (not no_overflow(m,
- (tqtreal(x) / tqtreal(y))))))) -> overflow_value(m, div(m, x, y))))
-
- axiom div_special5 :
- (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. ((tqtisFinite(x) and
- (is_zero(y) and (not is_zero(x)))) -> is_infinite(div(m, x, y))))
-
- axiom div_special6 :
- (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. ((is_zero(x) and
- is_zero(y)) -> is_nan(div(m, x, y))))
-
- axiom div_special7 :
- (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. (let r = div(m, x,
- y) : t in ((not is_nan(r)) -> product_sign(r, x, y))))
-
- axiom neg_special : (forall x:t [neg(x)]. (is_nan(x) -> is_nan(neg(x))))
-
- axiom neg_special1 :
- (forall x:t [neg(x)]. (is_infinite(x) -> is_infinite(neg(x))))
-
- axiom neg_special2 :
- (forall x:t [neg(x)]. ((not is_nan(x)) -> diff_sign(x, neg(x))))
-
- axiom abs_special : (forall x:t [abs1(x)]. (is_nan(x) -> is_nan(abs1(x))))
-
- axiom abs_special1 :
- (forall x:t [abs1(x)]. (is_infinite(x) -> is_infinite(abs1(x))))
-
- axiom abs_special2 :
- (forall x:t [abs1(x)]. ((not is_nan(x)) -> is_positive(abs1(x))))
-
- axiom fma_special :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((is_nan(x) or (is_nan(y) or is_nan(z))) -> is_nan(fma(m, x, y, z))))
-
- axiom fma_special1 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((is_zero(x) and is_infinite(y)) -> is_nan(fma(m, x, y, z))))
-
- axiom fma_special2 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((is_infinite(x) and is_zero(y)) -> is_nan(fma(m, x, y, z))))
-
- axiom fma_special3 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((tqtisFinite(x) and ((not is_zero(x)) and (is_infinite(y) and
- tqtisFinite(z)))) -> is_infinite(fma(m, x, y, z))))
-
- axiom fma_special4 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((tqtisFinite(x) and ((not is_zero(x)) and (is_infinite(y) and
- tqtisFinite(z)))) -> product_sign(fma(m, x, y, z), x, y)))
-
- axiom fma_special5 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((tqtisFinite(x) and ((not is_zero(x)) and (is_infinite(y) and
- is_infinite(z)))) -> (product_sign(z, x, y) -> is_infinite(fma(m, x, y,
- z)))))
-
- axiom fma_special6 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((tqtisFinite(x) and ((not is_zero(x)) and (is_infinite(y) and
- is_infinite(z)))) -> (product_sign(z, x, y) -> same_sign(fma(m, x, y, z),
- z))))
-
- axiom fma_special7 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((tqtisFinite(x) and ((not is_zero(x)) and (is_infinite(y) and
- is_infinite(z)))) -> ((not product_sign(z, x, y)) -> is_nan(fma(m, x, y,
- z)))))
-
- axiom fma_special8 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((is_infinite(x) and (tqtisFinite(y) and ((not is_zero(y)) and
- tqtisFinite(z)))) -> is_infinite(fma(m, x, y, z))))
-
- axiom fma_special9 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((is_infinite(x) and (tqtisFinite(y) and ((not is_zero(y)) and
- tqtisFinite(z)))) -> product_sign(fma(m, x, y, z), x, y)))
-
- axiom fma_special10 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((is_infinite(x) and (tqtisFinite(y) and ((not is_zero(y)) and
- is_infinite(z)))) -> (product_sign(z, x, y) -> is_infinite(fma(m, x, y,
- z)))))
-
- axiom fma_special11 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((is_infinite(x) and (tqtisFinite(y) and ((not is_zero(y)) and
- is_infinite(z)))) -> (product_sign(z, x, y) -> same_sign(fma(m, x, y, z),
- z))))
-
- axiom fma_special12 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((is_infinite(x) and (tqtisFinite(y) and ((not is_zero(y)) and
- is_infinite(z)))) -> ((not product_sign(z, x, y)) -> is_nan(fma(m, x, y,
- z)))))
-
- axiom fma_special13 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((is_infinite(x) and (is_infinite(y) and tqtisFinite(z))) ->
- is_infinite(fma(m, x, y, z))))
-
- axiom fma_special14 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((is_infinite(x) and (is_infinite(y) and tqtisFinite(z))) ->
- product_sign(fma(m, x, y, z), x, y)))
-
- axiom fma_special15 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((tqtisFinite(x) and (tqtisFinite(y) and is_infinite(z))) ->
- is_infinite(fma(m, x, y, z))))
-
- axiom fma_special16 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((tqtisFinite(x) and (tqtisFinite(y) and is_infinite(z))) ->
- same_sign(fma(m, x, y, z), z)))
-
- axiom fma_special17 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((is_infinite(x) and (is_infinite(y) and is_infinite(z))) ->
- (product_sign(z, x, y) -> is_infinite(fma(m, x, y, z)))))
-
- axiom fma_special18 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((is_infinite(x) and (is_infinite(y) and is_infinite(z))) ->
- (product_sign(z, x, y) -> same_sign(fma(m, x, y, z), z))))
-
- axiom fma_special19 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((is_infinite(x) and (is_infinite(y) and is_infinite(z))) ->
- ((not product_sign(z, x, y)) -> is_nan(fma(m, x, y, z)))))
-
- axiom fma_special20 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((tqtisFinite(x) and (tqtisFinite(y) and (tqtisFinite(z) and
- (not no_overflow(m, ((tqtreal(x) * tqtreal(y)) + tqtreal(z))))))) ->
- same_sign_real(fma(m, x, y, z), ((tqtreal(x) * tqtreal(y)) + tqtreal(z)))))
-
- axiom fma_special21 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((tqtisFinite(x) and (tqtisFinite(y) and (tqtisFinite(z) and
- (not no_overflow(m, ((tqtreal(x) * tqtreal(y)) + tqtreal(z))))))) ->
- overflow_value(m, fma(m, x, y, z))))
-
- axiom fma_special22 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((tqtisFinite(x) and (tqtisFinite(y) and tqtisFinite(z))) ->
- (product_sign(z, x, y) -> same_sign(fma(m, x, y, z), z))))
-
- axiom fma_special23 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((tqtisFinite(x) and (tqtisFinite(y) and tqtisFinite(z))) ->
- ((not product_sign(z, x, y)) ->
- ((((tqtreal(x) * tqtreal(y)) + tqtreal(z)) = 0.0) -> ((m = RTN) ->
- is_negative(fma(m, x, y, z)))))))
-
- axiom fma_special24 :
- (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
- ((tqtisFinite(x) and (tqtisFinite(y) and tqtisFinite(z))) ->
- ((not product_sign(z, x, y)) ->
- ((((tqtreal(x) * tqtreal(y)) + tqtreal(z)) = 0.0) -> ((not (m = RTN)) ->
- is_positive(fma(m, x, y, z)))))))
-
- axiom sqrt_special :
- (forall m:mode. forall x:t [sqrt(m, x)]. (is_nan(x) -> is_nan(sqrt(m, x))))
-
- axiom sqrt_special1 :
- (forall m:mode. forall x:t [sqrt(m, x)]. (is_plus_infinity(x) ->
- is_plus_infinity(sqrt(m, x))))
-
- axiom sqrt_special2 :
- (forall m:mode. forall x:t [sqrt(m, x)]. (is_minus_infinity(x) ->
- is_nan(sqrt(m, x))))
-
- axiom sqrt_special3 :
- (forall m:mode. forall x:t [sqrt(m, x)]. ((tqtisFinite(x) and
- (tqtreal(x) < 0.0)) -> is_nan(sqrt(m, x))))
-
- axiom sqrt_special4 :
- (forall m:mode. forall x:t [sqrt(m, x)]. (is_zero(x) -> same_sign(sqrt(m,
- x), x)))
-
- axiom sqrt_special5 :
- (forall m:mode. forall x:t [sqrt(m, x)]. ((tqtisFinite(x) and
- (0.0 < tqtreal(x))) -> is_positive(sqrt(m, x))))
-
- axiom of_int_add_exact :
- (forall m:mode. forall n:mode. forall i:int. forall j:int.
- (in_safe_int_range(i) -> (in_safe_int_range(j) ->
- (in_safe_int_range((i + j)) -> eq(of_int(m, (i + j)), add(n, of_int(m, i),
- of_int(m, j)))))))
-
- axiom of_int_sub_exact :
- (forall m:mode. forall n:mode. forall i:int. forall j:int.
- (in_safe_int_range(i) -> (in_safe_int_range(j) ->
- (in_safe_int_range((i - j)) -> eq(of_int(m, (i - j)), sub(n, of_int(m, i),
- of_int(m, j)))))))
-
- axiom of_int_mul_exact :
- (forall m:mode. forall n:mode. forall i:int. forall j:int.
- (in_safe_int_range(i) -> (in_safe_int_range(j) ->
- (in_safe_int_range((i * j)) -> eq(of_int(m, (i * j)), mul(n, of_int(m, i),
- of_int(m, j)))))))
-
- axiom Min_r : (forall x:t. forall y:t. (le(y, x) -> eq(min(x, y), y)))
-
- axiom Min_l : (forall x:t. forall y:t. (le(x, y) -> eq(min(x, y), x)))
-
- axiom Max_r : (forall x:t. forall y:t. (le(y, x) -> eq(max(x, y), x)))
-
- axiom Max_l : (forall x:t. forall y:t. (le(x, y) -> eq(max(x, y), y)))
-
logic is_int : t -> prop
- axiom zeroF_is_int : is_int(zeroF)
-
- axiom of_int_is_int :
- (forall m:mode. forall x:int. (in_int_range(x) -> is_int(of_int(m, x))))
-
- axiom big_float_is_int :
- (forall m:mode. forall i:t. (tqtisFinite(i) -> ((le(i, neg(of_int(m,
- 9007199254740992))) or le(of_int(m, 9007199254740992), i)) -> is_int(i))))
-
- axiom roundToIntegral_is_int :
- (forall m:mode. forall x:t. (tqtisFinite(x) -> is_int(roundToIntegral(m,
- x))))
-
- axiom eq_is_int :
- (forall x:t. forall y:t. (eq(x, y) -> (is_int(x) -> is_int(y))))
-
- axiom add_int :
- (forall x:t. forall y:t. forall m:mode. (is_int(x) -> (is_int(y) ->
- (tqtisFinite(add(m, x, y)) -> is_int(add(m, x, y))))))
-
- axiom sub_int :
- (forall x:t. forall y:t. forall m:mode. (is_int(x) -> (is_int(y) ->
- (tqtisFinite(sub(m, x, y)) -> is_int(sub(m, x, y))))))
-
- axiom mul_int :
- (forall x:t. forall y:t. forall m:mode. (is_int(x) -> (is_int(y) ->
- (tqtisFinite(mul(m, x, y)) -> is_int(mul(m, x, y))))))
-
- axiom fma_int :
- (forall x:t. forall y:t. forall z:t. forall m:mode. (is_int(x) ->
- (is_int(y) -> (is_int(z) -> (tqtisFinite(fma(m, x, y, z)) -> is_int(fma(m,
- x, y, z)))))))
-
- axiom neg_int : (forall x:t. (is_int(x) -> is_int(neg(x))))
-
- axiom abs_int1 : (forall x:t. (is_int(x) -> is_int(abs1(x))))
-
- axiom is_int_of_int :
- (forall x:t. forall m:mode. forall mqt:mode. (is_int(x) -> eq(x,
- of_int(mqt, to_int(m, x)))))
-
- axiom is_int_to_int :
- (forall m:mode. forall x:t. (is_int(x) -> in_int_range(to_int(m, x))))
-
- axiom is_int_is_finite : (forall x:t. (is_int(x) -> tqtisFinite(x)))
-
- axiom int_to_real :
- (forall m:mode. forall x:t. (is_int(x) -> (tqtreal(x) = from_int(to_int(m,
- x)))))
-
- axiom truncate_int :
- (forall m:mode. forall i:t. (is_int(i) -> eq(roundToIntegral(m, i), i)))
-
- axiom truncate_neg :
- (forall x:t. (tqtisFinite(x) -> (is_negative(x) -> (roundToIntegral(RTZ,
- x) = roundToIntegral(RTP, x)))))
-
- axiom truncate_pos :
- (forall x:t. (tqtisFinite(x) -> (is_positive(x) -> (roundToIntegral(RTZ,
- x) = roundToIntegral(RTN, x)))))
-
- axiom ceil_le :
- (forall x:t. (tqtisFinite(x) -> le(x, roundToIntegral(RTP, x))))
-
- axiom ceil_lest :
- (forall x:t. forall y:t. ((le(x, y) and is_int(y)) ->
- le(roundToIntegral(RTP, x), y)))
-
- axiom ceil_to_real :
- (forall x:t. (tqtisFinite(x) -> (tqtreal(roundToIntegral(RTP,
- x)) = from_int(ceil(tqtreal(x))))))
-
- axiom ceil_to_int :
- (forall m:mode. forall x:t. (tqtisFinite(x) -> (to_int(m,
- roundToIntegral(RTP, x)) = ceil(tqtreal(x)))))
-
- axiom floor_le :
- (forall x:t. (tqtisFinite(x) -> le(roundToIntegral(RTN, x), x)))
-
- axiom floor_lest :
- (forall x:t. forall y:t. ((le(y, x) and is_int(y)) -> le(y,
- roundToIntegral(RTN, x))))
-
- axiom floor_to_real :
- (forall x:t. (tqtisFinite(x) -> (tqtreal(roundToIntegral(RTN,
- x)) = from_int(floor(tqtreal(x))))))
-
- axiom floor_to_int :
- (forall m:mode. forall x:t. (tqtisFinite(x) -> (to_int(m,
- roundToIntegral(RTN, x)) = floor(tqtreal(x)))))
-
- axiom RNA_down :
- (forall x:t. (lt(sub(RNE, x, roundToIntegral(RTN, x)), sub(RNE,
- roundToIntegral(RTP, x), x)) -> (roundToIntegral(RNA,
- x) = roundToIntegral(RTN, x))))
-
- axiom RNA_up :
- (forall x:t. (lt(sub(RNE, roundToIntegral(RTP, x), x), sub(RNE, x,
- roundToIntegral(RTN, x))) -> (roundToIntegral(RNA,
- x) = roundToIntegral(RTP, x))))
-
- axiom RNA_down_tie :
- (forall x:t. (eq(sub(RNE, x, roundToIntegral(RTN, x)), sub(RNE,
- roundToIntegral(RTP, x), x)) -> (is_negative(x) -> (roundToIntegral(RNA,
- x) = roundToIntegral(RTN, x)))))
-
- axiom RNA_up_tie :
- (forall x:t. (eq(sub(RNE, roundToIntegral(RTP, x), x), sub(RNE, x,
- roundToIntegral(RTN, x))) -> (is_positive(x) -> (roundToIntegral(RNA,
- x) = roundToIntegral(RTP, x)))))
-
- axiom to_int_roundToIntegral :
- (forall m:mode. forall x:t. (to_int(m, x) = to_int(m, roundToIntegral(m,
- x))))
-
- axiom to_int_monotonic :
- (forall m:mode. forall x:t. forall y:t. (tqtisFinite(x) ->
- (tqtisFinite(y) -> (le(x, y) -> (to_int(m, x) <= to_int(m, y))))))
-
- axiom to_int_of_int :
- (forall m:mode. forall i:int. (in_safe_int_range(i) -> (to_int(m, of_int(m,
- i)) = i)))
-
- axiom eq_to_int :
- (forall m:mode. forall x:t. forall y:t. (tqtisFinite(x) -> (eq(x, y) ->
- (to_int(m, x) = to_int(m, y)))))
-
- axiom neg_to_int :
- (forall m:mode. forall x:t. (is_int(x) -> (to_int(m, neg(x)) = (-to_int(m,
- x)))))
-
- axiom roundToIntegral_is_finite :
- (forall m:mode. forall x:t. (tqtisFinite(x) ->
- tqtisFinite(roundToIntegral(m, x))))
-
- axiom round_bound_ne :
- (forall x:real [round(RNE, x)]. (no_overflow(RNE, x) ->
- (((x - (0x1.0p-53 * abs(x))) - 0x1.0p-1075) <= round(RNE, x))))
-
- axiom round_bound_ne1 :
- (forall x:real [round(RNE, x)]. (no_overflow(RNE, x) -> (round(RNE,
- x) <= ((x + (0x1.0p-53 * abs(x))) + 0x1.0p-1075))))
-
- axiom round_bound :
- (forall m:mode. forall x:real [round(m, x)]. (no_overflow(m, x) ->
- (((x - (0x1.0p-52 * abs(x))) - 0x1.0p-1074) <= round(m, x))))
-
- axiom round_bound1 :
- (forall m:mode. forall x:real [round(m, x)]. (no_overflow(m, x) ->
- (round(m, x) <= ((x + (0x1.0p-52 * abs(x))) + 0x1.0p-1074))))
-
type ('a, 'a1, 'a2, 'a3, 'a4) tuple5 = { Tuple5_proj_1 : 'a; Tuple5_proj_2 :
'a1; Tuple5_proj_3 : 'a2; Tuple5_proj_4 : 'a3; Tuple5_proj_5 : 'a4
}