diff --git a/Makefile b/Makefile
index 3c0346bf7698ba83ffd3797c15cc3b3f59e3d6fd..e3d014f7edfcab48bc40e4b8e4978a9988f02898 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,8 @@
all:
- dune build @install caisar.opam nnet.opam
+ dune build --root=. @install caisar.opam nnet.opam
test:
- dune runtest
+ dune runtest --root=.
+
+promote:
+ dune promote --root=.
diff --git a/caisar.opam b/caisar.opam
index 6fce9b4897ea3c2f5c4218f6adfe6039cfd3d370..ab1d3143c8d58fc1df94a984b7be9b95e5f88125 100644
--- a/caisar.opam
+++ b/caisar.opam
@@ -19,7 +19,7 @@ depends: [
"odoc" {with-doc}
]
build: [
- ["dune" "subst"] {dev}
+ ["dune" "subst" "--root" "."] {dev}
[
"dune"
"build"
@@ -27,7 +27,8 @@ build: [
name
"-j"
jobs
- "--promote-install-files=false"
+ "--promote-install-files"
+ "false"
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
diff --git a/config/drivers/pyrat.drv b/config/drivers/pyrat.drv
index ec70c5839c35a75e1cc259b2c72ec082f6fcf5da..e035485889d5ec0fe9ac4aefc087e14285f25c3e 100644
--- a/config/drivers/pyrat.drv
+++ b/config/drivers/pyrat.drv
@@ -6,7 +6,7 @@ prelude "(* this is the prelude for PyRAT *)"
valid "^Inconsistent assumption$"
-printer "alt-ergo"
+printer "why3"
filename "%f-%t-%g.why"
valid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Valid"
@@ -25,16 +25,11 @@ steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\) steps)" 2
time "why3cpulimit time : %s s"
transformation "inline_trivial"
+transformation "introduce_premises"
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"
+transformation "caisar_native_prover"
theory BuiltIn
syntax type int "int"
diff --git a/nnet.opam b/nnet.opam
index ea6f2c5285c00613bc4df4880b74b71fc723ad96..4871796a4c568e4a3339f8a81b43c26d01c74ccd 100644
--- a/nnet.opam
+++ b/nnet.opam
@@ -9,7 +9,7 @@ depends: [
"odoc" {with-doc}
]
build: [
- ["dune" "subst"] {dev}
+ ["dune" "subst" "--root" "."] {dev}
[
"dune"
"build"
@@ -17,7 +17,8 @@ build: [
name
"-j"
jobs
- "--promote-install-files=false"
+ "--promote-install-files"
+ "false"
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
diff --git a/src/language.ml b/src/language.ml
index 177c1f749a7e7a7175c445a7fcb8bd2662896ab1..33bd73063a80b3d472aa03f7e4b9fcbbf9945c54 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -8,6 +8,10 @@ open Base
(* -- Support for the NNet neural network format. *)
+let loaded_nnets = Why3.Term.Hls.create 10
+
+let lookup_loaded_nnets = Why3.Term.Hls.find_opt loaded_nnets
+
let nnet_parser env _ filename _ =
let open Why3 in
let header = Nnet.parse filename in
@@ -30,6 +34,7 @@ let nnet_parser env _ filename _ =
(List.init header.n_inputs ~f)
(Ty.ty_tuple (List.init header.n_outputs ~f))
in
+ Why3.Term.Hls.add loaded_nnets ls_nnet_apply filename;
let th_uc =
Pmodule.add_pdecl ~vc:false th_uc
(Pdecl.create_pure_decl (Decl.create_param_decl ls_nnet_apply))
diff --git a/src/language.mli b/src/language.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5a8c544502e299eca9ebafb2421b9cf94fe6a573
--- /dev/null
+++ b/src/language.mli
@@ -0,0 +1,5 @@
+val lookup_loaded_nnets : Why3.Term.lsymbol -> string option
+(** Return the filename of an nnets Why3 representation *)
+
+val register_nnet_support : unit -> unit
+(** register nnet parser *)
diff --git a/src/main.ml b/src/main.ml
index 3c1254e22064d7059ff05c18acca5d9b06291412..3b9031d9dc797c4e0b2824585883fd8f8dfe39e1 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -10,6 +10,7 @@ module Format = Caml.Format
let caisar = "caisar"
+let () = Transformations.init ()
(* -- Logs. *)
let pp_header =
diff --git a/src/transformations.ml b/src/transformations.ml
new file mode 100644
index 0000000000000000000000000000000000000000..94877c2ca39fefb362bc642538e9f4401fb0a074
--- /dev/null
+++ b/src/transformations.ml
@@ -0,0 +1,31 @@
+open Base
+
+let get_input_variables =
+ let rec aux acc (term : Why3.Term.term) =
+ match term.t_node with
+ | Why3.Term.Tapp (ls, args) -> (
+ match Language.lookup_loaded_nnets ls with
+ | None -> acc
+ | Some _name ->
+ let add acc = function
+ | { Why3.Term.t_node = Tapp (vs, []); _ } -> Why3.Term.Sls.add vs acc
+ | arg ->
+ invalid_arg
+ (Fmt.str "No direct variable in application: %a"
+ Why3.Pretty.print_term arg)
+ in
+ List.fold ~init:acc ~f:add args)
+ | _ -> Why3.Term.t_fold aux acc term
+ in
+ Why3.Trans.fold_decl
+ (fun decl acc -> Why3.Decl.decl_fold aux acc decl)
+ Why3.Term.Sls.empty
+
+let simplify_goal _input_variables = Why3.Trans.identity
+
+let caisar_native_prover = Why3.Trans.bind get_input_variables simplify_goal
+
+let init () =
+ Why3.Trans.register_transform
+ ~desc:"Transformation for provers that support loading neural networks."
+ "caisar_native_prover" caisar_native_prover
diff --git a/src/transformations.mli b/src/transformations.mli
new file mode 100644
index 0000000000000000000000000000000000000000..1d3779c269fa019d0f01e8b827d7ce09dbf7567a
--- /dev/null
+++ b/src/transformations.mli
@@ -0,0 +1,2 @@
+val init : unit -> unit
+(** register the transformations *)
diff --git a/tests/simple.t b/tests/simple.t
index 2f22cd593564a0dee407d00725de98f6d9818a05..bcda3cab5f7a83e091a1f2d79c92a2ac77558351 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -29,6 +29,7 @@ Test verify
> use caisar.NNet
>
> goal G: forall x1 x2 x3 x4 x5.
+ > 0.0 <. t'real x1 <. 0.1 ->
> let (y1,_,_,_,_) = nnet_apply x1 x2 x3 x4 x5 in
> 0.0 <. t'real y1 <. 0.1
> end
@@ -47,461 +48,1133 @@ Test verify
<autodetect>Found prover PyRAT version 1.0, OK.
<autodetect>3 prover(s) added
(* this is the prelude for PyRAT *)
+ theory Task
(* this is a prelude for Alt-Ergo integer arithmetic *)
(* this is a prelude for Alt-Ergo real arithmetic *)
type string
- logic match_bool : bool, 'a, 'a -> 'a
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use why3.Bool.Bool *)
+
+ (* use why3.Tuple0.Tuple0 *)
+
+ type unit = unit
+
+ (* use why3.Unit.Unit *)
+
+ (* clone algebra.Assoc with type t = int, function op = infix_pl,
+ prop Assoc = Assoc1, *)(* clone algebra.Monoid with type t1 = int, function unit = zero,
+ function op1 = infix_pl, prop Unit_def_r = Unit_def_r1,
+ prop Unit_def_l = Unit_def_l1, prop Assoc2 = Assoc1, *)(* clone algebra.Group with type t2 = int, function inv = prefix_mn,
+ function unit1 = zero, function op2 = infix_pl,
+ prop Inv_def_r = Inv_def_r1, prop Inv_def_l = Inv_def_l1,
+ prop Unit_def_r2 = Unit_def_r1, prop Unit_def_l2 = Unit_def_l1,
+ prop Assoc3 = Assoc1, *)(* clone algebra.Comm with type t3 = int, function op3 = infix_pl,
+ prop Comm = Comm1, *)(* meta AC function infix_pl *)
+
+ (* clone algebra.CommutativeGroup with type t4 = int,
+ function inv1 = prefix_mn, function unit2 = zero, function op4 = infix_pl,
+ prop Comm2 = Comm1, prop Inv_def_r2 = Inv_def_r1,
+ prop Inv_def_l2 = Inv_def_l1, prop Unit_def_r3 = Unit_def_r1,
+ prop Unit_def_l3 = Unit_def_l1, prop Assoc4 = Assoc1, *)(* clone algebra.Assoc with type t = int, function op = infix_as,
+ prop Assoc = Assoc5, *)(* clone algebra.Ring with type t5 = int, function infix_as1 = infix_as,
+ function prefix_mn1 = prefix_mn, function infix_pl1 = infix_pl,
+ function zero1 = zero, prop Mul_distr_r = Mul_distr_r1,
+ prop Mul_distr_l = Mul_distr_l1, prop Assoc6 = Assoc5, prop Comm3 = Comm1,
+ prop Inv_def_r3 = Inv_def_r1, prop Inv_def_l3 = Inv_def_l1,
+ prop Unit_def_r4 = Unit_def_r1, prop Unit_def_l4 = Unit_def_l1,
+ prop Assoc7 = Assoc1, *)(* clone algebra.Comm with type t3 = int, function op3 = infix_as,
+ prop Comm = Comm4, *)(* meta AC function infix_as *)
+
+ (* clone algebra.CommutativeRing with type t6 = int,
+ function infix_as2 = infix_as, function prefix_mn2 = prefix_mn,
+ function infix_pl2 = infix_pl, function zero2 = zero, prop Comm5 = Comm4,
+ prop Mul_distr_r2 = Mul_distr_r1, prop Mul_distr_l2 = Mul_distr_l1,
+ prop Assoc8 = Assoc5, prop Comm6 = Comm1, prop Inv_def_r4 = Inv_def_r1,
+ prop Inv_def_l4 = Inv_def_l1, prop Unit_def_r5 = Unit_def_r1,
+ prop Unit_def_l5 = Unit_def_l1, prop Assoc9 = Assoc1, *)(* clone algebra.UnitaryCommutativeRing with type t7 = int,
+ function one = one1, function infix_as3 = infix_as,
+ function prefix_mn3 = prefix_mn, function infix_pl3 = infix_pl,
+ function zero3 = zero, prop NonTrivialRing = NonTrivialRing1,
+ prop Unitary = Unitary1, prop Comm7 = Comm4,
+ prop Mul_distr_r3 = Mul_distr_r1, prop Mul_distr_l3 = Mul_distr_l1,
+ prop Assoc10 = Assoc5, prop Comm8 = Comm1, prop Inv_def_r5 = Inv_def_r1,
+ prop Inv_def_l5 = Inv_def_l1, prop Unit_def_r6 = Unit_def_r1,
+ prop Unit_def_l6 = Unit_def_l1, prop Assoc11 = Assoc1, *)(* clone relations.EndoRelation with type t8 = int,
+ predicate rel = infix_lseq, *)(* clone relations.Reflexive with type t9 = int, predicate rel1 = infix_lseq,
+ prop Refl = Refl1, *)(* clone relations.EndoRelation with type t8 = int,
+ predicate rel = infix_lseq, *)(* clone relations.Transitive with type t10 = int,
+ predicate rel2 = infix_lseq, prop Trans = Trans1, *)(* clone relations.PreOrder with type t11 = int, predicate rel3 = infix_lseq,
+ prop Trans2 = Trans1, prop Refl2 = Refl1, *)(* clone relations.EndoRelation with type t8 = int,
+ predicate rel = infix_lseq, *)(* clone relations.Antisymmetric with type t12 = int,
+ predicate rel4 = infix_lseq, prop Antisymm = Antisymm1, *)(* clone relations.PartialOrder with type t13 = int,
+ predicate rel5 = infix_lseq, prop Antisymm2 = Antisymm1,
+ prop Trans3 = Trans1, prop Refl3 = Refl1, *)(* clone relations.EndoRelation with type t8 = int,
+ predicate rel = infix_lseq, *)(* clone relations.Total with type t14 = int, predicate rel6 = infix_lseq,
+ prop Total = Total1, *)(* clone relations.TotalOrder with type t15 = int,
+ predicate rel7 = infix_lseq, prop Total2 = Total1,
+ prop Antisymm3 = Antisymm1, prop Trans4 = Trans1, prop Refl4 = Refl1, *)axiom CompatOrderMult : forall x:int, y:int, z:int. (x <= y) -> (0 <= z) ->
+ ((x * z) <= (y * z))
+
+ (* clone algebra.OrderedUnitaryCommutativeRing with type t16 = int,
+ predicate infix_lseq1 = infix_lseq, function one2 = one1,
+ function infix_as4 = infix_as, function prefix_mn4 = prefix_mn,
+ function infix_pl4 = infix_pl, function zero4 = zero,
+ prop CompatOrderMult1 = CompatOrderMult,
+ prop CompatOrderAdd = CompatOrderAdd1, prop ZeroLessOne = ZeroLessOne1,
+ prop Total3 = Total1, prop Antisymm4 = Antisymm1, prop Trans5 = Trans1,
+ prop Refl5 = Refl1, prop NonTrivialRing2 = NonTrivialRing1,
+ prop Unitary2 = Unitary1, prop Comm9 = Comm4,
+ prop Mul_distr_r4 = Mul_distr_r1, prop Mul_distr_l4 = Mul_distr_l1,
+ prop Assoc12 = Assoc5, prop Comm10 = Comm1, prop Inv_def_r6 = Inv_def_r1,
+ prop Inv_def_l6 = Inv_def_l1, prop Unit_def_r7 = Unit_def_r1,
+ prop Unit_def_l7 = Unit_def_l1, prop Assoc13 = Assoc1, *)(* use int.Int *)
+
+ (* clone algebra.Assoc with type t = real, function op = infix_pl5,
+ prop Assoc = Assoc14, *)(* clone algebra.Monoid with type t1 = real, function unit = zero5,
+ function op1 = infix_pl5, prop Unit_def_r = Unit_def_r8,
+ prop Unit_def_l = Unit_def_l8, prop Assoc2 = Assoc14, *)(* clone algebra.Group with type t2 = real, function inv = prefix_mn5,
+ function unit1 = zero5, function op2 = infix_pl5,
+ prop Inv_def_r = Inv_def_r7, prop Inv_def_l = Inv_def_l7,
+ prop Unit_def_r2 = Unit_def_r8, prop Unit_def_l2 = Unit_def_l8,
+ prop Assoc3 = Assoc14, *)(* clone algebra.Comm with type t3 = real, function op3 = infix_pl5,
+ prop Comm = Comm11, *)(* meta AC function infix_pl5 *)
+
+ (* clone algebra.CommutativeGroup with type t4 = real,
+ function inv1 = prefix_mn5, function unit2 = zero5,
+ function op4 = infix_pl5, prop Comm2 = Comm11,
+ prop Inv_def_r2 = Inv_def_r7, prop Inv_def_l2 = Inv_def_l7,
+ prop Unit_def_r3 = Unit_def_r8, prop Unit_def_l3 = Unit_def_l8,
+ prop Assoc4 = Assoc14, *)(* clone algebra.Assoc with type t = real, function op = infix_as5,
+ prop Assoc = Assoc15, *)(* clone algebra.Ring with type t5 = real, function infix_as1 = infix_as5,
+ function prefix_mn1 = prefix_mn5, function infix_pl1 = infix_pl5,
+ function zero1 = zero5, prop Mul_distr_r = Mul_distr_r5,
+ prop Mul_distr_l = Mul_distr_l5, prop Assoc6 = Assoc15,
+ prop Comm3 = Comm11, prop Inv_def_r3 = Inv_def_r7,
+ prop Inv_def_l3 = Inv_def_l7, prop Unit_def_r4 = Unit_def_r8,
+ prop Unit_def_l4 = Unit_def_l8, prop Assoc7 = Assoc14, *)(* clone algebra.Comm with type t3 = real, function op3 = infix_as5,
+ prop Comm = Comm12, *)(* meta AC function infix_as5 *)
+
+ (* clone algebra.CommutativeRing with type t6 = real,
+ function infix_as2 = infix_as5, function prefix_mn2 = prefix_mn5,
+ function infix_pl2 = infix_pl5, function zero2 = zero5,
+ prop Comm5 = Comm12, prop Mul_distr_r2 = Mul_distr_r5,
+ prop Mul_distr_l2 = Mul_distr_l5, prop Assoc8 = Assoc15,
+ prop Comm6 = Comm11, prop Inv_def_r4 = Inv_def_r7,
+ prop Inv_def_l4 = Inv_def_l7, prop Unit_def_r5 = Unit_def_r8,
+ prop Unit_def_l5 = Unit_def_l8, prop Assoc9 = Assoc14, *)(* clone algebra.UnitaryCommutativeRing with type t7 = real,
+ function one = one3, function infix_as3 = infix_as5,
+ function prefix_mn3 = prefix_mn5, function infix_pl3 = infix_pl5,
+ function zero3 = zero5, prop NonTrivialRing = NonTrivialRing3,
+ prop Unitary = Unitary3, prop Comm7 = Comm12,
+ prop Mul_distr_r3 = Mul_distr_r5, prop Mul_distr_l3 = Mul_distr_l5,
+ prop Assoc10 = Assoc15, prop Comm8 = Comm11, prop Inv_def_r5 = Inv_def_r7,
+ prop Inv_def_l5 = Inv_def_l7, prop Unit_def_r6 = Unit_def_r8,
+ prop Unit_def_l6 = Unit_def_l8, prop Assoc11 = Assoc14, *)axiom add_div : forall x:real, y:real, z:real. not (z = 0.0) ->
+ (((x + y) / z) = ((x / z) + (y / z)))
+
+ axiom sub_div : forall x:real, y:real, z:real. not (z = 0.0) ->
+ (((x - y) / z) = ((x / z) - (y / z)))
+
+ axiom neg_div : forall x:real, y:real. not (y = 0.0) ->
+ (((-x) / y) = (-(x / y)))
+
+ axiom assoc_mul_div : forall x:real, y:real, z:real. not (z = 0.0) ->
+ (((x * y) / z) = (x * (y / z)))
+
+ axiom assoc_div_mul : forall x:real, y:real, z:real. not (y = 0.0) /\
+ not (z = 0.0) -> (((x / y) / z) = (x / (y * z)))
+
+ axiom assoc_div_div : forall x:real, y:real, z:real. not (y = 0.0) /\
+ not (z = 0.0) -> ((x / (y / z)) = ((x * z) / y))
+
+ (* clone algebra.Field with type t17 = real, function infix_sl = infix_sl1,
+ function infix_mn = infix_mn1, function inv2 = inv3, function one4 = one3,
+ function infix_as6 = infix_as5, function prefix_mn6 = prefix_mn5,
+ function infix_pl6 = infix_pl5, function zero6 = zero5,
+ prop assoc_div_div1 = assoc_div_div, prop assoc_div_mul1 = assoc_div_mul,
+ prop assoc_mul_div1 = assoc_mul_div, prop neg_div1 = neg_div,
+ prop sub_div1 = sub_div, prop add_div1 = add_div, prop Inverse = Inverse1,
+ prop NonTrivialRing4 = NonTrivialRing3, prop Unitary4 = Unitary3,
+ prop Comm13 = Comm12, prop Mul_distr_r6 = Mul_distr_r5,
+ prop Mul_distr_l6 = Mul_distr_l5, prop Assoc16 = Assoc15,
+ prop Comm14 = Comm11, prop Inv_def_r8 = Inv_def_r7,
+ prop Inv_def_l8 = Inv_def_l7, prop Unit_def_r9 = Unit_def_r8,
+ prop Unit_def_l9 = Unit_def_l8, prop Assoc17 = Assoc14, *)(* clone relations.EndoRelation with type t8 = real,
+ predicate rel = infix_lseq2, *)(* clone relations.Reflexive with type t9 = real,
+ predicate rel1 = infix_lseq2, prop Refl = Refl6, *)(* clone relations.EndoRelation with type t8 = real,
+ predicate rel = infix_lseq2, *)(* clone relations.Transitive with type t10 = real,
+ predicate rel2 = infix_lseq2, prop Trans = Trans6, *)(* clone relations.PreOrder with type t11 = real,
+ predicate rel3 = infix_lseq2, prop Trans2 = Trans6, prop Refl2 = Refl6, *)(* clone relations.EndoRelation with type t8 = real,
+ predicate rel = infix_lseq2, *)(* clone relations.Antisymmetric with type t12 = real,
+ predicate rel4 = infix_lseq2, prop Antisymm = Antisymm5, *)(* clone relations.PartialOrder with type t13 = real,
+ predicate rel5 = infix_lseq2, prop Antisymm2 = Antisymm5,
+ prop Trans3 = Trans6, prop Refl3 = Refl6, *)(* clone relations.EndoRelation with type t8 = real,
+ predicate rel = infix_lseq2, *)(* clone relations.Total with type t14 = real, predicate rel6 = infix_lseq2,
+ prop Total = Total4, *)(* clone relations.TotalOrder with type t15 = real,
+ predicate rel7 = infix_lseq2, prop Total2 = Total4,
+ prop Antisymm3 = Antisymm5, prop Trans4 = Trans6, prop Refl4 = Refl6, *)axiom CompatOrderMult2 : forall x:real, y:real, z:real. (x <= y) ->
+ (0.0 <= z) -> ((x * z) <= (y * z))
- axiom match_bool_True :
- (forall z:'a. forall z1:'a. (match_bool(true, z, z1) = z))
+ (* clone algebra.OrderedField with type t18 = real,
+ predicate infix_lseq3 = infix_lseq2, function infix_sl2 = infix_sl1,
+ function infix_mn2 = infix_mn1, function inv4 = inv3, function one5 = one3,
+ function infix_as7 = infix_as5, function prefix_mn7 = prefix_mn5,
+ function infix_pl7 = infix_pl5, function zero7 = zero5,
+ prop CompatOrderMult3 = CompatOrderMult2,
+ prop CompatOrderAdd2 = CompatOrderAdd3, prop ZeroLessOne2 = ZeroLessOne3,
+ prop Total5 = Total4, prop Antisymm6 = Antisymm5, prop Trans7 = Trans6,
+ prop Refl7 = Refl6, prop assoc_div_div2 = assoc_div_div,
+ prop assoc_div_mul2 = assoc_div_mul, prop assoc_mul_div2 = assoc_mul_div,
+ prop neg_div2 = neg_div, prop sub_div2 = sub_div, prop add_div2 = add_div,
+ prop Inverse2 = Inverse1, prop NonTrivialRing5 = NonTrivialRing3,
+ prop Unitary5 = Unitary3, prop Comm15 = Comm12,
+ prop Mul_distr_r7 = Mul_distr_r5, prop Mul_distr_l7 = Mul_distr_l5,
+ prop Assoc18 = Assoc15, prop Comm16 = Comm11, prop Inv_def_r9 = Inv_def_r7,
+ prop Inv_def_l9 = Inv_def_l7, prop Unit_def_r10 = Unit_def_r8,
+ prop Unit_def_l10 = Unit_def_l8, prop Assoc19 = Assoc14, *)(* use real.Real *)
- axiom match_bool_False :
- (forall z:'a. forall z1:'a. (match_bool(false, z, z1) = z1))
+ type t19 = <float ...>
- axiom CompatOrderMult :
- (forall x:int. forall y:int. forall z:int. ((x <= y) -> ((0 <= z) ->
- ((x * z) <= (y * z)))))
+ function tqtreal t19 : real
- axiom add_div :
- (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
- (((x + y) / z) = ((x / z) + (y / z)))))
+ predicate tqtisFinite t19
- axiom sub_div :
- (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
- (((x - y) / z) = ((x / z) - (y / z)))))
+ (* meta float_type type t19, function tqtreal, predicate tqtisFinite *)
- axiom neg_div :
- (forall x:real. forall y:real. ((not (y = 0.0)) ->
- (((-x) / y) = (-(x / y)))))
+ (* meta model_projection function tqtreal *)
- axiom assoc_mul_div :
- (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
- (((x * y) / z) = (x * (y / z)))))
+ function pow2 int : int
- axiom assoc_div_mul :
- (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
- (not (z = 0.0))) -> (((x / y) / z) = (x / (y * z)))))
+ axiom Power_0 [@useraxiom] : (pow2 0 = 1)
- axiom assoc_div_div :
- (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
- (not (z = 0.0))) -> ((x / (y / z)) = ((x * z) / y))))
+ axiom Power_s [@useraxiom] : forall n:int. (0 <= n) -> (pow2
+ (n + 1) = (2 * pow2 n))
- axiom CompatOrderMult1 :
- (forall x:real. forall y:real. forall z:real. ((x <= y) -> ((0.0 <= z) ->
- ((x * z) <= (y * z)))))
+ axiom Power_1 : (pow2 1 = 2)
- type t
+ axiom Power_sum : forall n:int, m:int. (0 <= n) /\ (0 <= m) -> (pow2
+ (n + m) = (pow2 n * pow2 m))
- logic tqtreal : t -> real
+ axiom pow2pos : forall i:int. (0 <= i) -> (0 < pow2 i)
- logic tqtisFinite : t -> prop
+ axiom pow2_0 : (pow2 0 = 0x1)
- axiom tqtaxiom :
- (forall x:t. (tqtisFinite(x) ->
- ((-179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0) <= tqtreal(x))))
+ axiom pow2_1 : (pow2 1 = 0x2)
- axiom tqtaxiom1 :
- (forall x:t. (tqtisFinite(x) ->
- (tqtreal(x) <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0)))
+ axiom pow2_2 : (pow2 2 = 0x4)
- logic pow2 : int -> int
+ axiom pow2_3 : (pow2 3 = 0x8)
- axiom Power_0 : (pow2(0) = 1)
+ axiom pow2_4 : (pow2 4 = 0x10)
- axiom Power_s : (forall n:int. ((0 <= n) -> (pow2((n + 1)) = (2 * pow2(n)))))
+ axiom pow2_5 : (pow2 5 = 0x20)
- axiom Power_1 : (pow2(1) = 2)
+ axiom pow2_6 : (pow2 6 = 0x40)
- axiom Power_sum :
- (forall n:int. forall m:int. (((0 <= n) and (0 <= m)) ->
- (pow2((n + m)) = (pow2(n) * pow2(m)))))
+ axiom pow2_7 : (pow2 7 = 0x80)
- axiom pow2pos : (forall i:int. ((0 <= i) -> (0 < pow2(i))))
+ axiom pow2_8 : (pow2 8 = 0x100)
- axiom pow2_0 : (pow2(0) = 1)
+ axiom pow2_9 : (pow2 9 = 0x200)
- axiom pow2_1 : (pow2(1) = 2)
+ axiom pow2_10 : (pow2 10 = 0x400)
- axiom pow2_2 : (pow2(2) = 4)
+ axiom pow2_11 : (pow2 11 = 0x800)
- axiom pow2_3 : (pow2(3) = 8)
+ axiom pow2_12 : (pow2 12 = 0x1000)
- axiom pow2_4 : (pow2(4) = 16)
+ axiom pow2_13 : (pow2 13 = 0x2000)
- axiom pow2_5 : (pow2(5) = 32)
+ axiom pow2_14 : (pow2 14 = 0x4000)
- axiom pow2_6 : (pow2(6) = 64)
+ axiom pow2_15 : (pow2 15 = 0x8000)
- axiom pow2_7 : (pow2(7) = 128)
+ axiom pow2_16 : (pow2 16 = 0x10000)
- axiom pow2_8 : (pow2(8) = 256)
+ axiom pow2_17 : (pow2 17 = 0x20000)
- axiom pow2_9 : (pow2(9) = 512)
+ axiom pow2_18 : (pow2 18 = 0x40000)
- axiom pow2_10 : (pow2(10) = 1024)
+ axiom pow2_19 : (pow2 19 = 0x80000)
- axiom pow2_11 : (pow2(11) = 2048)
+ axiom pow2_20 : (pow2 20 = 0x100000)
- axiom pow2_12 : (pow2(12) = 4096)
+ axiom pow2_21 : (pow2 21 = 0x200000)
- axiom pow2_13 : (pow2(13) = 8192)
+ axiom pow2_22 : (pow2 22 = 0x400000)
- axiom pow2_14 : (pow2(14) = 16384)
+ axiom pow2_23 : (pow2 23 = 0x800000)
- axiom pow2_15 : (pow2(15) = 32768)
+ axiom pow2_24 : (pow2 24 = 0x1000000)
- axiom pow2_16 : (pow2(16) = 65536)
+ axiom pow2_25 : (pow2 25 = 0x2000000)
- axiom pow2_17 : (pow2(17) = 131072)
+ axiom pow2_26 : (pow2 26 = 0x4000000)
- axiom pow2_18 : (pow2(18) = 262144)
+ axiom pow2_27 : (pow2 27 = 0x8000000)
- axiom pow2_19 : (pow2(19) = 524288)
+ axiom pow2_28 : (pow2 28 = 0x10000000)
- axiom pow2_20 : (pow2(20) = 1048576)
+ axiom pow2_29 : (pow2 29 = 0x20000000)
- axiom pow2_21 : (pow2(21) = 2097152)
+ axiom pow2_30 : (pow2 30 = 0x40000000)
- axiom pow2_22 : (pow2(22) = 4194304)
+ axiom pow2_31 : (pow2 31 = 0x80000000)
- axiom pow2_23 : (pow2(23) = 8388608)
+ axiom pow2_32 : (pow2 32 = 0x100000000)
- axiom pow2_24 : (pow2(24) = 16777216)
+ axiom pow2_33 : (pow2 33 = 0x200000000)
- axiom pow2_25 : (pow2(25) = 33554432)
+ axiom pow2_34 : (pow2 34 = 0x400000000)
- axiom pow2_26 : (pow2(26) = 67108864)
+ axiom pow2_35 : (pow2 35 = 0x800000000)
- axiom pow2_27 : (pow2(27) = 134217728)
+ axiom pow2_36 : (pow2 36 = 0x1000000000)
- axiom pow2_28 : (pow2(28) = 268435456)
+ axiom pow2_37 : (pow2 37 = 0x2000000000)
- axiom pow2_29 : (pow2(29) = 536870912)
+ axiom pow2_38 : (pow2 38 = 0x4000000000)
- axiom pow2_30 : (pow2(30) = 1073741824)
+ axiom pow2_39 : (pow2 39 = 0x8000000000)
- axiom pow2_31 : (pow2(31) = 2147483648)
+ axiom pow2_40 : (pow2 40 = 0x10000000000)
- axiom pow2_32 : (pow2(32) = 4294967296)
+ axiom pow2_41 : (pow2 41 = 0x20000000000)
- axiom pow2_33 : (pow2(33) = 8589934592)
+ axiom pow2_42 : (pow2 42 = 0x40000000000)
- axiom pow2_34 : (pow2(34) = 17179869184)
+ axiom pow2_43 : (pow2 43 = 0x80000000000)
- axiom pow2_35 : (pow2(35) = 34359738368)
+ axiom pow2_44 : (pow2 44 = 0x100000000000)
- axiom pow2_36 : (pow2(36) = 68719476736)
+ axiom pow2_45 : (pow2 45 = 0x200000000000)
- axiom pow2_37 : (pow2(37) = 137438953472)
+ axiom pow2_46 : (pow2 46 = 0x400000000000)
- axiom pow2_38 : (pow2(38) = 274877906944)
+ axiom pow2_47 : (pow2 47 = 0x800000000000)
- axiom pow2_39 : (pow2(39) = 549755813888)
+ axiom pow2_48 : (pow2 48 = 0x1000000000000)
- axiom pow2_40 : (pow2(40) = 1099511627776)
+ axiom pow2_49 : (pow2 49 = 0x2000000000000)
- axiom pow2_41 : (pow2(41) = 2199023255552)
+ axiom pow2_50 : (pow2 50 = 0x4000000000000)
- axiom pow2_42 : (pow2(42) = 4398046511104)
+ axiom pow2_51 : (pow2 51 = 0x8000000000000)
- axiom pow2_43 : (pow2(43) = 8796093022208)
+ axiom pow2_52 : (pow2 52 = 0x10000000000000)
- axiom pow2_44 : (pow2(44) = 17592186044416)
+ axiom pow2_53 : (pow2 53 = 0x20000000000000)
- axiom pow2_45 : (pow2(45) = 35184372088832)
+ axiom pow2_54 : (pow2 54 = 0x40000000000000)
- axiom pow2_46 : (pow2(46) = 70368744177664)
+ axiom pow2_55 : (pow2 55 = 0x80000000000000)
- axiom pow2_47 : (pow2(47) = 140737488355328)
+ axiom pow2_56 : (pow2 56 = 0x100000000000000)
- axiom pow2_48 : (pow2(48) = 281474976710656)
+ axiom pow2_57 : (pow2 57 = 0x200000000000000)
- axiom pow2_49 : (pow2(49) = 562949953421312)
+ axiom pow2_58 : (pow2 58 = 0x400000000000000)
- axiom pow2_50 : (pow2(50) = 1125899906842624)
+ axiom pow2_59 : (pow2 59 = 0x800000000000000)
- axiom pow2_51 : (pow2(51) = 2251799813685248)
+ axiom pow2_60 : (pow2 60 = 0x1000000000000000)
- axiom pow2_52 : (pow2(52) = 4503599627370496)
+ axiom pow2_61 : (pow2 61 = 0x2000000000000000)
- axiom pow2_53 : (pow2(53) = 9007199254740992)
+ axiom pow2_62 : (pow2 62 = 0x4000000000000000)
- axiom pow2_54 : (pow2(54) = 18014398509481984)
+ axiom pow2_63 : (pow2 63 = 0x8000000000000000)
- axiom pow2_55 : (pow2(55) = 36028797018963968)
+ axiom pow2_64 : (pow2 64 = 0x10000000000000000)
- axiom pow2_56 : (pow2(56) = 72057594037927936)
+ (* use bv.Pow2int *)
- axiom pow2_57 : (pow2(57) = 144115188075855872)
+ function abs (x:real) : real = if (0.0 <= x) then x else (-x)
- axiom pow2_58 : (pow2(58) = 288230376151711744)
+ axiom Abs_le : forall x:real, y:real. (abs x <= y) <-> ((-y) <= x) /\
+ (x <= y)
- axiom pow2_59 : (pow2(59) = 576460752303423488)
+ axiom Abs_pos : forall x:real. (0.0 <= abs x)
- axiom pow2_60 : (pow2(60) = 1152921504606846976)
+ axiom Abs_sum : forall x:real, y:real. (abs (x + y) <= (abs x + abs y))
- axiom pow2_61 : (pow2(61) = 2305843009213693952)
+ axiom Abs_prod : forall x:real, y:real. (abs (x * y) = (abs x * abs y))
- axiom pow2_62 : (pow2(62) = 4611686018427387904)
+ axiom triangular_inequality : forall x:real, y:real, z:real. (abs
+ (x - z) <= (abs (x - y) + abs (y - z)))
- axiom pow2_63 : (pow2(63) = 9223372036854775808)
+ (* use real.Abs *)
- axiom pow2_64 : (pow2(64) = 18446744073709551616)
+ function from_int int : real
- function abs(x: real) : real = (if (0.0 <= x) then x else (-x))
+ axiom Zero [@useraxiom] : (from_int 0 = 0.0)
- axiom Abs_le : (forall x:real. forall y:real. ((abs(x) <= y) -> ((-y) <= x)))
+ axiom One [@useraxiom] : (from_int 1 = 1.0)
- axiom Abs_le1 : (forall x:real. forall y:real. ((abs(x) <= y) -> (x <= y)))
+ axiom Add [@useraxiom] : forall x:int, y:int. (from_int (x + y) = (from_int
+ x + from_int y))
- axiom Abs_le2 :
- (forall x:real. forall y:real. ((((-y) <= x) and (x <= y)) ->
- (abs(x) <= y)))
+ axiom Sub [@useraxiom] : forall x:int, y:int. (from_int (x - y) = (from_int
+ x - from_int y))
- axiom Abs_pos : (forall x:real. (0.0 <= abs(x)))
+ axiom Mul [@useraxiom] : forall x:int, y:int. (from_int (x * y) = (from_int
+ x * from_int y))
- axiom Abs_sum :
- (forall x:real. forall y:real. (abs((x + y)) <= (abs(x) + abs(y))))
+ axiom Neg [@useraxiom] : forall x:int. (from_int (-x) = (-from_int x))
- axiom Abs_prod :
- (forall x:real. forall y:real. (abs((x * y)) = (abs(x) * abs(y))))
+ axiom Injective : forall x:int, y:int. (from_int x = from_int y) -> (x = y)
- axiom triangular_inequality :
- (forall x:real. forall y:real. forall z:real.
- (abs((x - z)) <= (abs((x - y)) + abs((y - z)))))
+ axiom Monotonic [@useraxiom] : forall x:int, y:int. (x <= y) -> (from_int
+ x <= from_int y)
- logic from_int : int -> real
+ (* use real.FromInt *)
- axiom Zero : (from_int(0) = 0.0)
+ function truncate real : int
- axiom One : (from_int(1) = 1.0)
+ axiom Truncate_int [@useraxiom] : forall i:int. (truncate (from_int i) = i)
- axiom Add :
- (forall x:int. forall y:int.
- (from_int((x + y)) = (from_int(x) + from_int(y))))
+ axiom Truncate_down_pos [@useraxiom] : forall x:real. (0.0 <= x) -> (from_int
+ (truncate x) <= x) /\ (x < from_int (truncate x + 1))
- axiom Sub :
- (forall x:int. forall y:int.
- (from_int((x - y)) = (from_int(x) - from_int(y))))
+ axiom Truncate_up_neg [@useraxiom] : forall x:real. (x <= 0.0) -> (from_int
+ (truncate x - 1) < x) /\ (x <= from_int (truncate x))
- axiom Mul :
- (forall x:int. forall y:int.
- (from_int((x * y)) = (from_int(x) * from_int(y))))
+ axiom Real_of_truncate [@useraxiom] : forall x:real. ((x - 1.0) <= from_int
+ (truncate x)) /\ (from_int (truncate x) <= (x + 1.0))
- axiom Neg : (forall x:int. (from_int((-x)) = (-from_int(x))))
+ axiom Truncate_monotonic [@useraxiom] : forall x:real, y:real. (x <= y) ->
+ (truncate x <= truncate y)
- axiom Injective :
- (forall x:int. forall y:int. ((from_int(x) = from_int(y)) -> (x = y)))
+ axiom Truncate_monotonic_int1 [@useraxiom] : forall x:real, i:int.
+ (x <= from_int i) -> (truncate x <= i)
- axiom Monotonic :
- (forall x:int. forall y:int. ((x <= y) -> (from_int(x) <= from_int(y))))
+ axiom Truncate_monotonic_int2 [@useraxiom] : forall x:real, i:int. (from_int
+ i <= x) -> (i <= truncate x)
- logic truncate : real -> int
+ function floor real : int
- axiom Truncate_int : (forall i:int. (truncate(from_int(i)) = i))
+ function ceil real : int
- axiom Truncate_down_pos :
- (forall x:real. ((0.0 <= x) -> (from_int(truncate(x)) <= x)))
+ axiom Floor_int [@useraxiom] : forall i:int. (floor (from_int i) = i)
- axiom Truncate_down_pos1 :
- (forall x:real. ((0.0 <= x) -> (x < from_int((truncate(x) + 1)))))
+ axiom Ceil_int [@useraxiom] : forall i:int. (ceil (from_int i) = i)
- axiom Truncate_up_neg :
- (forall x:real. ((x <= 0.0) -> (from_int((truncate(x) - 1)) < x)))
+ axiom Floor_down [@useraxiom] : forall x:real. (from_int (floor x) <= x) /\
+ (x < from_int (floor x + 1))
- axiom Truncate_up_neg1 :
- (forall x:real. ((x <= 0.0) -> (x <= from_int(truncate(x)))))
+ axiom Ceil_up [@useraxiom] : forall x:real. (from_int (ceil x - 1) < x) /\
+ (x <= from_int (ceil x))
- axiom Real_of_truncate :
- (forall x:real. ((x - 1.0) <= from_int(truncate(x))))
+ axiom Floor_monotonic [@useraxiom] : forall x:real, y:real. (x <= y) ->
+ (floor x <= floor y)
- axiom Real_of_truncate1 :
- (forall x:real. (from_int(truncate(x)) <= (x + 1.0)))
+ axiom Ceil_monotonic [@useraxiom] : forall x:real, y:real. (x <= y) -> (ceil
+ x <= ceil y)
- axiom Truncate_monotonic :
- (forall x:real. forall y:real. ((x <= y) -> (truncate(x) <= truncate(y))))
+ (* use real.Truncate *)
- axiom Truncate_monotonic_int1 :
- (forall x:real. forall i:int. ((x <= from_int(i)) -> (truncate(x) <= i)))
+ (* use real.RealInfix *)
- axiom Truncate_monotonic_int2 :
- (forall x:real. forall i:int. ((from_int(i) <= x) -> (i <= truncate(x))))
+ type mode =
+ | RNE
+ | RNA
+ | RTP
+ | RTN
+ | RTZ
- logic floor : real -> int
+ predicate to_nearest (m:mode) = (m = RNE) \/ (m = RNA)
- logic ceil : real -> int
+ (* use ieee_float.RoundingMode *)
- axiom Floor_int : (forall i:int. (floor(from_int(i)) = i))
+ function zeroF : t19
- axiom Ceil_int : (forall i:int. (ceil(from_int(i)) = i))
+ function add mode t19 t19 : t19
- axiom Floor_down : (forall x:real. (from_int(floor(x)) <= x))
+ function sub mode t19 t19 : t19
- axiom Floor_down1 : (forall x:real. (x < from_int((floor(x) + 1))))
+ function mul mode t19 t19 : t19
- axiom Ceil_up : (forall x:real. (from_int((ceil(x) - 1)) < x))
+ function div mode t19 t19 : t19
- axiom Ceil_up1 : (forall x:real. (x <= from_int(ceil(x))))
+ function abs1 t19 : t19
- axiom Floor_monotonic :
- (forall x:real. forall y:real. ((x <= y) -> (floor(x) <= floor(y))))
+ function neg t19 : t19
- axiom Ceil_monotonic :
- (forall x:real. forall y:real. ((x <= y) -> (ceil(x) <= ceil(y))))
+ function fma mode t19 t19 t19 : t19
- type mode = RNE | RNA | RTP | RTN | RTZ
+ function sqrt mode t19 : t19
- logic match_mode : mode, 'a, 'a, 'a, 'a, 'a -> 'a
+ function roundToIntegral mode t19 : t19
- axiom match_mode_RNE :
- (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
- (match_mode(RNE, z, z1, z2, z3, z4) = z))
+ function min t19 t19 : t19
- axiom match_mode_RNA :
- (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
- (match_mode(RNA, z, z1, z2, z3, z4) = z1))
+ function max t19 t19 : t19
- axiom match_mode_RTP :
- (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
- (match_mode(RTP, z, z1, z2, z3, z4) = z2))
+ predicate le t19 t19
- axiom match_mode_RTN :
- (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
- (match_mode(RTN, z, z1, z2, z3, z4) = z3))
+ predicate lt t19 t19
- axiom match_mode_RTZ :
- (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
- (match_mode(RTZ, z, z1, z2, z3, z4) = z4))
+ predicate eq t19 t19
- predicate to_nearest(m: mode) = ((m = RNE) or (m = RNA))
+ predicate is_normal t19
- logic zeroF : t
+ predicate is_subnormal t19
- logic add : mode, t, t -> t
+ predicate is_zero t19
- logic sub : mode, t, t -> t
+ predicate is_infinite t19
- logic mul : mode, t, t -> t
+ predicate is_nan t19
- logic div : mode, t, t -> t
+ predicate is_positive t19
- logic abs1 : t -> t
+ predicate is_negative t19
- logic neg : t -> t
+ predicate is_plus_infinity (x:t19) = is_infinite x /\ is_positive x
- logic fma : mode, t, t, t -> t
+ predicate is_minus_infinity (x:t19) = is_infinite x /\ is_negative x
- logic sqrt : mode, t -> t
+ predicate is_plus_zero (x:t19) = is_zero x /\ is_positive x
- logic roundToIntegral : mode, t -> t
+ predicate is_minus_zero (x:t19) = is_zero x /\ is_negative x
- logic min : t, t -> t
+ function of_int mode int : t19
- logic max : t, t -> t
+ function to_int mode t19 : int
- logic le : t, t -> prop
+ function round mode real : real
- logic lt : t, t -> prop
+ function max_int : int
- logic eq : t, t -> prop
+ predicate in_range (x:real) = ((-0x1.FFFFFFFFFFFFFp1023) <= x) /\
+ (x <= 0x1.FFFFFFFFFFFFFp1023)
- logic is_normal : t -> prop
+ predicate in_int_range (i:int) = ((-max_int) <= i) /\ (i <= max_int)
- logic is_subnormal : t -> prop
+ predicate no_overflow (m:mode) (x:real) = in_range (round m x)
- logic is_zero : t -> prop
+ predicate in_safe_int_range (i:int) = ((-9007199254740992) <= i) /\
+ (i <= 9007199254740992)
- logic is_infinite : t -> prop
+ predicate same_sign (x:t19) (y:t19) = is_positive x /\ is_positive y \/
+ is_negative x /\ is_negative y
- logic is_nan : t -> prop
+ predicate diff_sign (x:t19) (y:t19) = is_positive x /\ is_negative y \/
+ is_negative x /\ is_positive y
- logic is_positive : t -> prop
+ predicate product_sign (z:t19) (x:t19) (y:t19) = (same_sign x y ->
+ is_positive z) /\ (diff_sign x y -> is_negative z)
- logic is_negative : t -> prop
+ predicate overflow_value (m:mode) (x:t19) =
+ match m with
+ | RTN -> if is_positive x then tqtisFinite x /\ (tqtreal
+ x = 0x1.FFFFFFFFFFFFFp1023) else is_infinite x
+ | RTP -> if is_positive x then is_infinite x else tqtisFinite x /\ (tqtreal
+ x = (-0x1.FFFFFFFFFFFFFp1023))
+ | RTZ -> if is_positive x then tqtisFinite x /\ (tqtreal
+ x = 0x1.FFFFFFFFFFFFFp1023) else tqtisFinite x /\ (tqtreal
+ x = (-0x1.FFFFFFFFFFFFFp1023))
+ | RNA | RNE -> is_infinite x
+ end
- predicate is_plus_infinity(x: t) = (is_infinite(x) and is_positive(x))
+ predicate sign_zero_result (m:mode) (x:t19) = is_zero x ->
+ match m with
+ | RTN -> is_negative x
+ | _ -> is_positive x
+ end
- predicate is_minus_infinity(x: t) = (is_infinite(x) and is_negative(x))
+ function sqr (x:real) : real = (x * x)
- predicate is_plus_zero(x: t) = (is_zero(x) and is_positive(x))
+ function sqrt1 real : real
+
+ axiom Sqrt_positive [@useraxiom] : forall x:real. (0.0 <= x) -> (0.0 <= sqrt1
+ x)
+
+ axiom Sqrt_square [@useraxiom] : forall x:real. (0.0 <= x) -> (sqr (sqrt1
+ x) = x)
+
+ axiom Square_sqrt [@useraxiom] : forall x:real. (0.0 <= x) -> (sqrt1
+ (x * x) = x)
+
+ axiom Sqrt_mul [@useraxiom] : forall x:real, y:real. (0.0 <= x) /\
+ (0.0 <= y) -> (sqrt1 (x * y) = (sqrt1 x * sqrt1 y))
+
+ axiom Sqrt_le [@useraxiom] : forall x:real, y:real. (0.0 <= x) /\ (x <= y) ->
+ (sqrt1 x <= sqrt1 y)
+
+ (* use real.Square *)
+
+ predicate same_sign_real (x:t19) (r:real) = is_positive x /\ (0.0 < r) \/
+ is_negative x /\ (r < 0.0)
+
+ predicate is_int t19
+
+ (* clone ieee_float.GenericFloat with type t20 = t19,
+ predicate is_int1 = is_int, predicate same_sign_real1 = same_sign_real,
+ predicate sign_zero_result1 = sign_zero_result,
+ predicate overflow_value1 = overflow_value,
+ predicate product_sign1 = product_sign, predicate diff_sign1 = diff_sign,
+ predicate same_sign1 = same_sign,
+ predicate in_safe_int_range1 = in_safe_int_range,
+ function pow2sb = pow2sb1, predicate no_overflow1 = no_overflow,
+ predicate in_int_range1 = in_int_range, predicate in_range1 = in_range,
+ function emax = emax1, function max_int1 = max_int,
+ function max_real = max_real1, function round1 = round,
+ function to_int1 = to_int, function of_int1 = of_int,
+ function to_real = tqtreal, predicate is_not_nan = is_not_nan1,
+ predicate is_minus_zero1 = is_minus_zero,
+ predicate is_plus_zero1 = is_plus_zero,
+ predicate is_minus_infinity1 = is_minus_infinity,
+ predicate is_plus_infinity1 = is_plus_infinity,
+ predicate is_finite = tqtisFinite, predicate is_negative1 = is_negative,
+ predicate is_positive1 = is_positive, predicate is_nan1 = is_nan,
+ predicate is_infinite1 = is_infinite, predicate is_zero1 = is_zero,
+ predicate is_subnormal1 = is_subnormal, predicate is_normal1 = is_normal,
+ predicate infix_dteq = infix_dteq1, predicate infix_dtgt = infix_dtgt1,
+ predicate infix_dtgteq = infix_dtgteq1, predicate infix_dtls = infix_dtls1,
+ predicate infix_dtlseq = infix_dtlseq1, predicate eq1 = eq,
+ predicate gt = gt1, predicate ge = ge1, predicate lt1 = lt,
+ predicate le1 = le, function max1 = max, function min1 = min,
+ function roundToIntegral1 = roundToIntegral,
+ function infix_dtsl = infix_dtsl1, function infix_dtas = infix_dtas1,
+ function infix_dtmn = infix_dtmn1, function infix_dtpl = infix_dtpl1,
+ function prefix_dtmn = prefix_dtmn1, function sqrt2 = sqrt,
+ function fma1 = fma, function neg1 = neg, function abs2 = abs1,
+ function div1 = div, function mul1 = mul, function sub1 = sub,
+ function add1 = add, function zeroF1 = zeroF, function sb = tqtsb,
+ function eb = tqteb,
+ prop roundToIntegral_is_finite = roundToIntegral_is_finite1,
+ prop neg_to_int = neg_to_int1, prop eq_to_int = eq_to_int1,
+ prop to_int_of_int = to_int_of_int1,
+ prop to_int_monotonic = to_int_monotonic1,
+ prop to_int_roundToIntegral = to_int_roundToIntegral1,
+ prop RNA_up_tie = RNA_up_tie1, prop RNA_down_tie = RNA_down_tie1,
+ prop RNA_up = RNA_up1, prop RNA_down = RNA_down1,
+ prop floor_to_int = floor_to_int1, prop floor_to_real = floor_to_real1,
+ prop floor_lest = floor_lest1, prop floor_le = floor_le1,
+ prop ceil_to_int = ceil_to_int1, prop ceil_to_real = ceil_to_real1,
+ prop ceil_lest = ceil_lest1, prop ceil_le = ceil_le1,
+ prop truncate_pos = truncate_pos1, prop truncate_neg = truncate_neg1,
+ prop truncate_int = truncate_int1, prop int_to_real = int_to_real1,
+ prop is_int_is_finite = is_int_is_finite1,
+ prop is_int_to_int = is_int_to_int1, prop is_int_of_int = is_int_of_int1,
+ prop abs_int = abs_int1, prop neg_int = neg_int1, prop fma_int = fma_int1,
+ prop mul_int = mul_int1, prop sub_int = sub_int1, prop add_int = add_int1,
+ prop eq_is_int = eq_is_int1,
+ prop roundToIntegral_is_int = roundToIntegral_is_int1,
+ prop big_float_is_int = big_float_is_int1,
+ prop of_int_is_int = of_int_is_int1, prop zeroF_is_int = zeroF_is_int1,
+ prop Max_l = Max_l1, prop Max_r = Max_r1, prop Min_l = Min_l1,
+ prop Min_r = Min_r1, prop of_int_mul_exact = of_int_mul_exact1,
+ prop of_int_sub_exact = of_int_sub_exact1,
+ prop of_int_add_exact = of_int_add_exact1,
+ prop sqrt_special = sqrt_special1, prop fma_special = fma_special1,
+ prop abs_special = abs_special1, prop neg_special = neg_special1,
+ prop div_special = div_special1, prop mul_special = mul_special1,
+ prop sub_special = sub_special1, prop add_special = add_special1,
+ prop sqrt_finite_rev = sqrt_finite_rev1, prop sqrt_finite = sqrt_finite1,
+ prop fma_finite_rev_n = fma_finite_rev_n1,
+ prop fma_finite_rev = fma_finite_rev1, prop fma_finite = fma_finite1,
+ prop abs_universal = abs_universal1, prop abs_finite_rev = abs_finite_rev1,
+ prop abs_finite = abs_finite1, prop neg_finite_rev = neg_finite_rev1,
+ prop neg_finite = neg_finite1, prop div_finite_rev_n = div_finite_rev_n1,
+ prop div_finite_rev = div_finite_rev1, prop div_finite = div_finite1,
+ prop mul_finite_rev_n = mul_finite_rev_n1,
+ prop mul_finite_rev = mul_finite_rev1, prop mul_finite = mul_finite1,
+ prop sub_finite_rev_n = sub_finite_rev_n1,
+ prop sub_finite_rev = sub_finite_rev1, prop sub_finite = sub_finite1,
+ prop add_finite_rev_n = add_finite_rev_n1,
+ prop add_finite_rev = add_finite_rev1, prop add_finite = add_finite1,
+ prop same_sign_product = same_sign_product1,
+ prop diff_sign_product = diff_sign_product1,
+ prop diff_sign_trans = diff_sign_trans1,
+ prop negative_or_positive = negative_or_positive1,
+ prop negative_xor_positive = negative_xor_positive1,
+ prop to_real_negative = to_real_negative1,
+ prop negative_to_real = negative_to_real1,
+ prop to_real_positive = to_real_positive1,
+ prop positive_to_real = positive_to_real1,
+ prop lt_lt_finite = lt_lt_finite1, prop lt_special = lt_special1,
+ prop le_special = le_special1, prop not_gt_le = not_gt_le1,
+ prop not_lt_ge = not_lt_ge1, prop le_ge_asym = le_ge_asym1,
+ prop lt_le_trans = lt_le_trans1, prop le_lt_trans = le_lt_trans1,
+ prop le_finite = le_finite1, prop lt_finite = lt_finite1,
+ prop eq_special = eq_special1, prop eq_to_real_finite = eq_to_real_finite1,
+ prop eq_zero = eq_zero1, prop eq_trans = eq_trans1, prop eq_sym = eq_sym1,
+ prop eq_refl = eq_refl1, prop eq_feq = eq_feq1, prop feq_eq = feq_eq1,
+ prop Exact_rounding_for_integers = Exact_rounding_for_integers1,
+ prop pow2sb = pow2sb1, prop Round_up_neg = Round_up_neg1,
+ prop Round_down_neg = Round_down_neg1, prop Round_up_ge = Round_up_ge1,
+ prop Round_down_le = Round_down_le1, prop Round_to_real = Round_to_real1,
+ prop Round_idempotent = Round_idempotent1,
+ prop Round_monotonic = Round_monotonic1,
+ prop Bounded_real_no_overflow = Bounded_real_no_overflow1,
+ prop is_finite = is_finite1, prop max_real_int = max_real_int1,
+ prop max_int = max_int1, prop zero_of_int = zero_of_int1,
+ prop zero_to_real = zero_to_real1, prop zeroF_is_zero = zeroF_is_zero1,
+ prop zeroF_is_positive = zeroF_is_positive1,
+ prop is_not_finite = is_not_finite1, prop is_not_nan = is_not_nan1,
+ prop sb_gt_1 = sb_gt_11, prop eb_gt_1 = eb_gt_11, *)(* use ieee_float.Float64 *)
- predicate is_minus_zero(x: t) = (is_zero(x) and is_negative(x))
+ type input_type = t19
- logic of_int : mode, int -> t
+ (* use caisar.NNet *)
- logic to_int : mode, t -> int
+ type tuple5 'a 'a1 'a2 'a3 'a4 =
+ | Tuple5 'a 'a1 'a2 'a3 'a4
- logic round : mode, real -> real
+ (* use why3.Tuple5.Tuple51 *)
- logic max_int1 : int
+ function nnet_apply t19 t19 t19 t19 t19 : tuple5 t19 t19 t19 t19 t19
- predicate in_range(x: real) = (((-0x1.FFFFFFFFFFFFFp1023) <= x) and
- (x <= 0x1.FFFFFFFFFFFFFp1023))
+ (* use AsTuple *)
- predicate in_int_range(i: int) = (((-max_int1) <= i) and (i <= max_int1))
+ (* meta syntax_type type int, "int", 0 *)
- predicate no_overflow(m: mode, x: real) = in_range(round(m, x))
+ (* meta syntax_type type real, "real", 0 *)
- predicate in_safe_int_range(i: int) = (((-9007199254740992) <= i) and
- (i <= 9007199254740992))
+ (* meta syntax_logic predicate infix_eq, "(%1 = %2)", 0 *)
- predicate same_sign(x: t, y: t) = ((is_positive(x) and is_positive(y)) or
- (is_negative(x) and is_negative(y)))
+ (* meta eliminate_algebraic "keep_enums" *)
- predicate diff_sign(x: t, y: t) = ((is_positive(x) and is_negative(y)) or
- (is_negative(x) and is_positive(y)))
+ (* meta eliminate_algebraic "keep_recs" *)
- predicate product_sign(z: t, x: t, y: t) = ((same_sign(x, y) ->
- is_positive(z)) and (diff_sign(x, y) -> is_negative(z)))
+ (* meta syntax_type type bool, "bool", 0 *)
- predicate overflow_value(m: mode, x: t) = ((((((m = RNE) ->
- is_infinite(x)) and ((m = RNA) -> is_infinite(x))) and ((m = RTP) ->
- (if is_positive(x) then is_infinite(x) else (tqtisFinite(x) and
- (tqtreal(x) = (-0x1.FFFFFFFFFFFFFp1023)))))) and ((m = RTN) ->
- (if is_positive(x) then (tqtisFinite(x) and
- (tqtreal(x) = 0x1.FFFFFFFFFFFFFp1023)) else is_infinite(x)))) and
- ((m = RTZ) -> (if is_positive(x) then (tqtisFinite(x) and
- (tqtreal(x) = 0x1.FFFFFFFFFFFFFp1023)) else (tqtisFinite(x) and
- (tqtreal(x) = (-0x1.FFFFFFFFFFFFFp1023))))))
+ (* meta syntax_logic function True, "true", 0 *)
- predicate sign_zero_result(m: mode, x: t) = (is_zero(x) -> ((((((m = RNE) ->
- is_positive(x)) and ((m = RNA) -> is_positive(x))) and ((m = RTP) ->
- is_positive(x))) and ((m = RTN) -> is_negative(x))) and ((m = RTZ) ->
- is_positive(x))))
+ (* meta syntax_logic function False, "false", 0 *)
- function sqr(x: real) : real = (x * x)
+ (* meta syntax_type type tuple0, "unit", 0 *)
- logic sqrt1 : real -> real
+ (* meta syntax_logic function Tuple01, "void", 0 *)
- axiom Sqrt_positive : (forall x:real. ((0.0 <= x) -> (0.0 <= sqrt1(x))))
+ (* meta syntax_logic function zero, "0", 0 *)
- axiom Sqrt_square : (forall x:real. ((0.0 <= x) -> (sqr(sqrt1(x)) = x)))
+ (* meta syntax_logic function one1, "1", 0 *)
- axiom Square_sqrt : (forall x:real. ((0.0 <= x) -> (sqrt1((x * x)) = x)))
+ (* meta syntax_logic function infix_pl, "(%1 + %2)", 0 *)
- axiom Sqrt_mul :
- (forall x:real. forall y:real. (((0.0 <= x) and (0.0 <= y)) ->
- (sqrt1((x * y)) = (sqrt1(x) * sqrt1(y)))))
+ (* meta syntax_logic function infix_mn3, "(%1 - %2)", 0 *)
- axiom Sqrt_le :
- (forall x:real. forall y:real. (((0.0 <= x) and (x <= y)) ->
- (sqrt1(x) <= sqrt1(y))))
+ (* meta syntax_logic function infix_as, "(%1 * %2)", 0 *)
- predicate same_sign_real(x: t, r: real) = ((is_positive(x) and (0.0 < r)) or
- (is_negative(x) and (r < 0.0)))
+ (* meta syntax_logic function prefix_mn, "(-%1)", 0 *)
- logic is_int : t -> prop
+ (* meta invalid trigger predicate infix_lseq *)
- 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
- }
+ (* meta invalid trigger predicate infix_ls *)
- logic nnet_apply : t, t, t, t, t -> (t, t, t, t, t) tuple5
+ (* meta invalid trigger predicate infix_gteq *)
- goal G :
- (forall x1:t. forall x2:t. forall x3:t. forall x4:t. forall x5:t.
- (forall x:t. forall x6:t. forall x7:t. forall x8:t. forall x9:t.
- ((nnet_apply(x1, x2, x3, x4, x5) = { Tuple5_proj_1 = x; Tuple5_proj_2 = x6;
- Tuple5_proj_3 = x7; Tuple5_proj_4 = x8; Tuple5_proj_5 = x9 }) ->
- ((0.0 < tqtreal(x)) and (tqtreal(x) < 0.1)))))
+ (* meta invalid trigger predicate infix_gt *)
+
+ (* meta syntax_logic predicate infix_lseq, "(%1 <= %2)", 0 *)
+
+ (* meta syntax_logic predicate infix_ls, "(%1 < %2)", 0 *)
+
+ (* meta syntax_logic predicate infix_gteq, "(%1 >= %2)", 0 *)
+
+ (* meta syntax_logic predicate infix_gt, "(%1 > %2)", 0 *)
+
+ (* meta remove_prop prop Comm4 *)
+
+ (* meta remove_prop prop Assoc5 *)
+
+ (* meta remove_prop prop Unit_def_l1 *)
+
+ (* meta remove_prop prop Unit_def_r1 *)
+
+ (* meta remove_prop prop Inv_def_l1 *)
+
+ (* meta remove_prop prop Inv_def_r1 *)
+
+ (* meta remove_prop prop Assoc1 *)
+
+ (* meta remove_prop prop Mul_distr_l1 *)
+
+ (* meta remove_prop prop Mul_distr_r1 *)
+
+ (* meta remove_prop prop Comm1 *)
+
+ (* meta remove_prop prop Unitary1 *)
+
+ (* meta remove_prop prop Refl1 *)
+
+ (* meta remove_prop prop Trans1 *)
+
+ (* meta remove_prop prop Total1 *)
+
+ (* meta remove_prop prop Antisymm1 *)
+
+ (* meta remove_prop prop NonTrivialRing1 *)
+
+ (* meta remove_prop prop CompatOrderAdd1 *)
+
+ (* meta remove_prop prop ZeroLessOne1 *)
+
+ (* meta syntax_logic function zero5, "0.0", 0 *)
+
+ (* meta syntax_logic function one3, "1.0", 0 *)
+
+ (* meta syntax_logic function infix_pl5, "(%1 + %2)", 0 *)
+
+ (* meta syntax_logic function infix_mn1, "(%1 - %2)", 0 *)
+
+ (* meta syntax_logic function infix_as5, "(%1 * %2)", 0 *)
+
+ (* meta syntax_logic function infix_sl1, "(%1 / %2)", 0 *)
+
+ (* meta syntax_logic function prefix_mn5, "(-%1)", 0 *)
+
+ (* meta syntax_logic function inv3, "(1.0 / %1)", 0 *)
+
+ (* meta invalid trigger predicate infix_lseq2 *)
+
+ (* meta invalid trigger predicate infix_ls1 *)
+
+ (* meta invalid trigger predicate infix_gteq1 *)
+
+ (* meta invalid trigger predicate infix_gt1 *)
+
+ (* meta syntax_logic predicate infix_lseq2, "(%1 <= %2)", 0 *)
+
+ (* meta syntax_logic predicate infix_ls1, "(%1 < %2)", 0 *)
+
+ (* meta syntax_logic predicate infix_gteq1, "(%1 >= %2)", 0 *)
+
+ (* meta syntax_logic predicate infix_gt1, "(%1 > %2)", 0 *)
+
+ (* meta remove_prop prop Comm12 *)
+
+ (* meta remove_prop prop Assoc15 *)
+
+ (* meta remove_prop prop Unit_def_l8 *)
+
+ (* meta remove_prop prop Unit_def_r8 *)
+
+ (* meta remove_prop prop Inv_def_l7 *)
+
+ (* meta remove_prop prop Inv_def_r7 *)
+
+ (* meta remove_prop prop Assoc14 *)
+
+ (* meta remove_prop prop Mul_distr_l5 *)
+
+ (* meta remove_prop prop Mul_distr_r5 *)
+
+ (* meta remove_prop prop Comm11 *)
+
+ (* meta remove_prop prop Unitary3 *)
+
+ (* meta remove_prop prop Refl6 *)
+
+ (* meta remove_prop prop Trans6 *)
+
+ (* meta remove_prop prop Total4 *)
+
+ (* meta remove_prop prop Antisymm5 *)
+
+ (* meta remove_prop prop Inverse1 *)
+
+ (* meta remove_prop prop NonTrivialRing3 *)
+
+ (* meta remove_prop prop CompatOrderAdd3 *)
+
+ (* meta remove_prop prop ZeroLessOne3 *)
+
+ (* meta syntax_logic function infix_pldt, "(%1 + %2)", 0 *)
+
+ (* meta syntax_logic function infix_mndt, "(%1 - %2)", 0 *)
+
+ (* meta syntax_logic function infix_asdt, "(%1 * %2)", 0 *)
+
+ (* meta syntax_logic function infix_sldt, "(%1 / %2)", 0 *)
+
+ (* meta syntax_logic function prefix_mndt, "(-%1)", 0 *)
+
+ (* meta invalid trigger predicate infix_lseqdt *)
+
+ (* meta invalid trigger predicate infix_lsdt *)
+
+ (* meta invalid trigger predicate infix_gteqdt *)
+
+ (* meta invalid trigger predicate infix_gtdt *)
+
+ (* meta syntax_logic predicate infix_lseqdt, "(%1 <= %2)", 0 *)
+
+ (* meta syntax_logic predicate infix_lsdt, "(%1 < %2)", 0 *)
+
+ (* meta syntax_logic predicate infix_gteqdt, "(%1 >= %2)", 0 *)
+
+ (* meta syntax_logic predicate infix_gtdt, "(%1 > %2)", 0 *)
+
+ (* meta syntax_logic predicate is_not_nan1, "", 0 *)
+
+ (* meta remove_prop prop eb_gt_11 *)
+
+ (* meta remove_prop prop sb_gt_11 *)
+
+ (* meta remove_prop prop is_not_nan1 *)
+
+ (* meta remove_prop prop is_not_finite1 *)
+
+ (* meta remove_prop prop zeroF_is_positive1 *)
+
+ (* meta remove_prop prop zeroF_is_zero1 *)
+
+ (* meta remove_prop prop zero_to_real1 *)
+
+ (* meta remove_prop prop zero_of_int1 *)
+
+ (* meta remove_prop prop max_int1 *)
+
+ (* meta remove_prop prop max_real_int1 *)
+
+ (* meta remove_prop prop is_finite1 *)
+
+ (* meta remove_prop prop Bounded_real_no_overflow1 *)
+
+ (* meta remove_prop prop Round_monotonic1 *)
+
+ (* meta remove_prop prop Round_idempotent1 *)
+
+ (* meta remove_prop prop Round_to_real1 *)
+
+ (* meta remove_prop prop Round_down_le1 *)
+
+ (* meta remove_prop prop Round_up_ge1 *)
+
+ (* meta remove_prop prop Round_down_neg1 *)
+
+ (* meta remove_prop prop Round_up_neg1 *)
+
+ (* meta remove_prop prop pow2sb1 *)
+
+ (* meta remove_prop prop Exact_rounding_for_integers1 *)
+
+ (* meta remove_prop prop feq_eq1 *)
+
+ (* meta remove_prop prop eq_feq1 *)
+
+ (* meta remove_prop prop eq_refl1 *)
+
+ (* meta remove_prop prop eq_sym1 *)
+
+ (* meta remove_prop prop eq_trans1 *)
+
+ (* meta remove_prop prop eq_zero1 *)
+
+ (* meta remove_prop prop eq_to_real_finite1 *)
+
+ (* meta remove_prop prop eq_special1 *)
+
+ (* meta remove_prop prop lt_finite1 *)
+
+ (* meta remove_prop prop le_finite1 *)
+
+ (* meta remove_prop prop le_lt_trans1 *)
+
+ (* meta remove_prop prop lt_le_trans1 *)
+
+ (* meta remove_prop prop le_ge_asym1 *)
+
+ (* meta remove_prop prop not_lt_ge1 *)
+
+ (* meta remove_prop prop not_gt_le1 *)
+
+ (* meta remove_prop prop le_special1 *)
+
+ (* meta remove_prop prop lt_special1 *)
+
+ (* meta remove_prop prop lt_lt_finite1 *)
+
+ (* meta remove_prop prop positive_to_real1 *)
+
+ (* meta remove_prop prop to_real_positive1 *)
+
+ (* meta remove_prop prop negative_to_real1 *)
+
+ (* meta remove_prop prop to_real_negative1 *)
+
+ (* meta remove_prop prop negative_xor_positive1 *)
+
+ (* meta remove_prop prop negative_or_positive1 *)
+
+ (* meta remove_prop prop diff_sign_trans1 *)
+
+ (* meta remove_prop prop diff_sign_product1 *)
+
+ (* meta remove_prop prop same_sign_product1 *)
+
+ (* meta remove_prop prop add_finite1 *)
+
+ (* meta remove_prop prop add_finite_rev1 *)
+
+ (* meta remove_prop prop add_finite_rev_n1 *)
+
+ (* meta remove_prop prop sub_finite1 *)
+
+ (* meta remove_prop prop sub_finite_rev1 *)
+
+ (* meta remove_prop prop sub_finite_rev_n1 *)
+
+ (* meta remove_prop prop mul_finite1 *)
+
+ (* meta remove_prop prop mul_finite_rev1 *)
+
+ (* meta remove_prop prop mul_finite_rev_n1 *)
+
+ (* meta remove_prop prop div_finite1 *)
+
+ (* meta remove_prop prop div_finite_rev1 *)
+
+ (* meta remove_prop prop div_finite_rev_n1 *)
+
+ (* meta remove_prop prop neg_finite1 *)
+
+ (* meta remove_prop prop neg_finite_rev1 *)
+
+ (* meta remove_prop prop abs_finite1 *)
+
+ (* meta remove_prop prop abs_finite_rev1 *)
+
+ (* meta remove_prop prop abs_universal1 *)
+
+ (* meta remove_prop prop fma_finite1 *)
+
+ (* meta remove_prop prop fma_finite_rev1 *)
+
+ (* meta remove_prop prop fma_finite_rev_n1 *)
+
+ (* meta remove_prop prop sqrt_finite1 *)
+
+ (* meta remove_prop prop sqrt_finite_rev1 *)
+
+ (* meta remove_prop prop add_special1 *)
+
+ (* meta remove_prop prop sub_special1 *)
+
+ (* meta remove_prop prop mul_special1 *)
+
+ (* meta remove_prop prop div_special1 *)
+
+ (* meta remove_prop prop neg_special1 *)
+
+ (* meta remove_prop prop abs_special1 *)
+
+ (* meta remove_prop prop fma_special1 *)
+
+ (* meta remove_prop prop sqrt_special1 *)
+
+ (* meta remove_prop prop of_int_add_exact1 *)
+
+ (* meta remove_prop prop of_int_sub_exact1 *)
+
+ (* meta remove_prop prop of_int_mul_exact1 *)
+
+ (* meta remove_prop prop Min_r1 *)
+
+ (* meta remove_prop prop Min_l1 *)
+
+ (* meta remove_prop prop Max_r1 *)
+
+ (* meta remove_prop prop Max_l1 *)
+
+ (* meta remove_prop prop zeroF_is_int1 *)
+
+ (* meta remove_prop prop of_int_is_int1 *)
+
+ (* meta remove_prop prop big_float_is_int1 *)
+
+ (* meta remove_prop prop roundToIntegral_is_int1 *)
+
+ (* meta remove_prop prop eq_is_int1 *)
+
+ (* meta remove_prop prop add_int1 *)
+
+ (* meta remove_prop prop sub_int1 *)
+
+ (* meta remove_prop prop mul_int1 *)
+
+ (* meta remove_prop prop fma_int1 *)
+
+ (* meta remove_prop prop neg_int1 *)
+
+ (* meta remove_prop prop abs_int1 *)
+
+ (* meta remove_prop prop is_int_of_int1 *)
+
+ (* meta remove_prop prop is_int_to_int1 *)
+
+ (* meta remove_prop prop is_int_is_finite1 *)
+
+ (* meta remove_prop prop int_to_real1 *)
+
+ (* meta remove_prop prop truncate_int1 *)
+
+ (* meta remove_prop prop truncate_neg1 *)
+
+ (* meta remove_prop prop truncate_pos1 *)
+
+ (* meta remove_prop prop ceil_le1 *)
+
+ (* meta remove_prop prop ceil_lest1 *)
+
+ (* meta remove_prop prop ceil_to_real1 *)
+
+ (* meta remove_prop prop ceil_to_int1 *)
+
+ (* meta remove_prop prop floor_le1 *)
+
+ (* meta remove_prop prop floor_lest1 *)
+
+ (* meta remove_prop prop floor_to_real1 *)
+
+ (* meta remove_prop prop floor_to_int1 *)
+
+ (* meta remove_prop prop RNA_down1 *)
+
+ (* meta remove_prop prop RNA_up1 *)
+
+ (* meta remove_prop prop RNA_down_tie1 *)
+
+ (* meta remove_prop prop RNA_up_tie1 *)
+
+ (* meta remove_prop prop to_int_roundToIntegral1 *)
+
+ (* meta remove_prop prop to_int_monotonic1 *)
+
+ (* meta remove_prop prop to_int_of_int1 *)
+
+ (* meta remove_prop prop eq_to_int1 *)
+
+ (* meta remove_prop prop neg_to_int1 *)
+
+ (* meta remove_prop prop roundToIntegral_is_finite1 *)
+
+ (* meta remove_prop prop round_bound_ne *)
+
+ (* meta remove_prop prop round_bound *)
+
+ function x1 [@introduced] : t19
+
+ function x2 [@introduced] : t19
+
+ function x3 [@introduced] : t19
+
+ function x4 [@introduced] : t19
+
+ function x5 [@introduced] : t19
+
+ axiom H [@introduced] : (0.0 < tqtreal x1)
+
+ axiom H1 [@introduced] : (tqtreal x1 < 0.1)
+
+ goal G : match nnet_apply x1 x2 x3 x4 x5 with
+ | Tuple5 y1 _ _ _ _ -> (0.0 < tqtreal y1) /\ (tqtreal y1 < 0.1)
+ end
+
+ end