diff --git a/caisar.opam b/caisar.opam
index 195dfada29c8aced8f6d1971869ae2d31fdad923..7a4b2ab06acab3d4f17b51dee2c11dd82fca3483 100644
--- a/caisar.opam
+++ b/caisar.opam
@@ -20,7 +20,7 @@ depends: [
"odoc" {with-doc}
]
build: [
- ["dune" "subst"] {dev}
+ ["dune" "subst" "--root" "."] {dev}
[
"dune"
"build"
@@ -28,7 +28,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 8a88c457a02594f3ed71782c945dd02f79bed895..c47bfc6e23510227f20bf330c97ec0b2a99a1169 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 "why3"
+printer "pyrat"
filename "%f-%t-%g.why"
valid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Valid"
@@ -144,6 +144,22 @@ theory real.Real
end
+theory ieee_float.Float64
+
+ syntax function (.+) "(%1 + %2)"
+ syntax function (.-) "(%1 - %2)"
+ syntax function (.*) "(%1 * %2)"
+ syntax function (./) "(%1 / %2)"
+ syntax function (.-_) "(-%1)"
+
+ syntax predicate le "(%1 <= %2)"
+ syntax predicate lt "(%1 < %2)"
+ syntax predicate ge "(%1 >= %2)"
+ syntax predicate gt "(%1 > %2)"
+
+
+end
+
theory real.RealInfix
syntax function (+.) "(%1 + %2)"
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/main.ml b/src/main.ml
index 8d5bdaf6e8a2d530a59fe3a0f3404e081332c06b..879086e0214ab43f15df314e46765f8faf7deb8a 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -10,6 +10,8 @@ open Cmdliner
let caisar = "caisar"
let () = Transformations.init ()
+
+let () = Pyrat.init ()
(* -- Logs. *)
let pp_header =
diff --git a/src/printer/pyrat.ml b/src/printer/pyrat.ml
index 5ec59fe8d69e511d0760840c0b89a4411f03cd14..7f5db7d60f14a7e664ad010e919cf9b6e655a3e9 100644
--- a/src/printer/pyrat.ml
+++ b/src/printer/pyrat.ml
@@ -4,10 +4,103 @@
(* *)
(**************************************************************************)
-let print_task args ?old:_ fmt _task =
+type info = {
+ info_syn : Why3.Printer.syntax_map;
+ variables : string Why3.Term.Hls.t;
+}
+
+let number_format =
+ {
+ Why3.Number.long_int_support = `Default;
+ Why3.Number.negative_int_support = `Default;
+ Why3.Number.dec_int_support = `Default;
+ Why3.Number.hex_int_support = `Unsupported;
+ Why3.Number.oct_int_support = `Unsupported;
+ Why3.Number.bin_int_support = `Unsupported;
+ Why3.Number.negative_real_support = `Default;
+ Why3.Number.dec_real_support = `Default;
+ Why3.Number.hex_real_support = `Unsupported;
+ Why3.Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
+ }
+
+let rec print_term info fmt t =
+ match t.Why3.Term.t_node with
+ | Tconst c -> Why3.Constant.(print number_format unsupported_escape) fmt c
+ | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _ | Teps _ ->
+ Why3.Printer.unsupportedTerm t "Pyrat"
+ | Tapp (ls, l) -> (
+ match Why3.Printer.query_syntax info.info_syn ls.ls_name with
+ | Some s -> Why3.Printer.syntax_arguments s (print_term info) fmt l
+ | None -> (
+ match (Why3.Term.Hls.find_opt info.variables ls, l) with
+ | Some s, [] -> Fmt.string fmt s
+ | _ -> Why3.Printer.unsupportedTerm t "Unknown variables"))
+ | Tbinop ((Timplies | Tiff), _, _) | Tnot _ | Ttrue | Tfalse ->
+ Why3.Printer.unsupportedTerm t "Pyrat: Iff, Implies, not"
+ | Tbinop (Tand, _, _) -> Why3.Printer.unsupportedTerm t "Pyrat: Deep and"
+ | Tbinop (Tor, t1, t2) ->
+ Fmt.pf fmt "%a or %a" (print_term info) t1 (print_term info) t2
+
+let print_top_term info fmt t =
+ let print_term info fmt t =
+ (** don't print things we don't know *)
+ if Why3.Term.t_s_all (fun _ -> true)
+ (fun ls -> Why3.Ident.Mid.mem ls.ls_name info.info_syn ||
+ Why3.Term.Hls.mem info.variables ls)
+ t then
+ print_term info fmt t
+ in
+ match t.Why3.Term.t_node with
+ | Tquant _ -> ()
+ | Tbinop (Tand, t1, t2) ->
+ Fmt.pf fmt "%a@.%a" (print_term info) t1 (print_term info) t2
+ | _ -> Fmt.pf fmt "%a@." (print_term info) t
+
+let print_decl info fmt d =
+ let open Why3 in
+ match d.Decl.d_node with
+ | Dtype _ -> ()
+ | Ddata _ -> ()
+ | Dparam _ -> ()
+ | Dlogic _ -> ()
+ | Dind _ -> ()
+ | Dprop (Decl.Plemma, _, _) -> assert false
+ | Dprop (Decl.Paxiom, _, f) -> print_top_term info fmt f
+ | Dprop (Decl.Pgoal, _, f) -> print_top_term info fmt f
+
+let rec print_tdecl info fmt task =
+ let open Why3 in
+ match task with
+ | None -> ()
+ | Some { Task.task_prev; task_decl; _ } -> (
+ print_tdecl info fmt task_prev;
+ match task_decl.Theory.td_node with
+ | Decl d -> print_decl info fmt d
+ | Use _ | Clone _ -> ()
+ | Meta (meta, l) when Theory.meta_equal meta Transformations.meta_input -> (
+ match l with
+ | [ MAls ls; MAint i ] ->
+ Why3.Term.Hls.add info.variables ls (Fmt.str "x%i" i)
+ | _ -> assert false)
+ | Meta (meta, l) when Theory.meta_equal meta Transformations.meta_output
+ -> (
+ match l with
+ | [ MAls ls; MAint i ] ->
+ Why3.Term.Hls.add info.variables ls (Fmt.str "y%i" i)
+ | _ -> assert false)
+ | Meta (_, _) -> ())
+
+let print_task args ?old:_ fmt task =
let open Why3 in
- Printer.print_prelude fmt args.Printer.prelude
+ let info =
+ {
+ info_syn = Discriminate.get_syntax_map task;
+ variables = Why3.Term.Hls.create 10;
+ }
+ in
+ Printer.print_prelude fmt args.Printer.prelude;
+ print_tdecl info fmt task
-let () =
+let init () =
Why3.Printer.register_printer ~desc:"Printer for the PyRAT prover." "pyrat"
print_task
diff --git a/src/transformations.mli b/src/transformations.mli
index 0df41287e55f0f129b1160b22da6b0096c6e0cc3..dc209777c55661a0e0e5932354825354566e41e7 100644
--- a/src/transformations.mli
+++ b/src/transformations.mli
@@ -6,3 +6,9 @@
val init : unit -> unit
(** Register the transformations. *)
+
+val meta_input : Why3.Theory.meta
+(** Indicates the position of the input *)
+
+val meta_output : Why3.Theory.meta
+(** Indicates the position of the output *)
diff --git a/tests/simple.t b/tests/simple.t
index 45493a0151215a08a50567aba30b090fe681eb46..f0aab4989114b50d2f73ed94bbd341f8cf59f1ab 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -47,1161 +47,76 @@ 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
-
- (* 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))
- (* 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 *)
- type t19 = <float ...>
- function tqtreal t19 : real
- predicate tqtisFinite t19
- (* meta float_type type t19, function tqtreal, predicate tqtisFinite *)
- (* meta model_projection function tqtreal *)
- function pow2 int : int
- axiom Power_0 [@useraxiom] : (pow2 0 = 1)
- axiom Power_s [@useraxiom] : forall n:int. (0 <= n) -> (pow2
- (n + 1) = (2 * pow2 n))
- axiom Power_1 : (pow2 1 = 2)
- axiom Power_sum : forall n:int, m:int. (0 <= n) /\ (0 <= m) -> (pow2
- (n + m) = (pow2 n * pow2 m))
- axiom pow2pos : forall i:int. (0 <= i) -> (0 < pow2 i)
- axiom pow2_0 : (pow2 0 = 0x1)
- axiom pow2_1 : (pow2 1 = 0x2)
- axiom pow2_2 : (pow2 2 = 0x4)
- axiom pow2_3 : (pow2 3 = 0x8)
- axiom pow2_4 : (pow2 4 = 0x10)
- axiom pow2_5 : (pow2 5 = 0x20)
- axiom pow2_6 : (pow2 6 = 0x40)
- axiom pow2_7 : (pow2 7 = 0x80)
- axiom pow2_8 : (pow2 8 = 0x100)
- axiom pow2_9 : (pow2 9 = 0x200)
- axiom pow2_10 : (pow2 10 = 0x400)
- axiom pow2_11 : (pow2 11 = 0x800)
- axiom pow2_12 : (pow2 12 = 0x1000)
- axiom pow2_13 : (pow2 13 = 0x2000)
- axiom pow2_14 : (pow2 14 = 0x4000)
- axiom pow2_15 : (pow2 15 = 0x8000)
- axiom pow2_16 : (pow2 16 = 0x10000)
- axiom pow2_17 : (pow2 17 = 0x20000)
- axiom pow2_18 : (pow2 18 = 0x40000)
- axiom pow2_19 : (pow2 19 = 0x80000)
- axiom pow2_20 : (pow2 20 = 0x100000)
- axiom pow2_21 : (pow2 21 = 0x200000)
- axiom pow2_22 : (pow2 22 = 0x400000)
- axiom pow2_23 : (pow2 23 = 0x800000)
- axiom pow2_24 : (pow2 24 = 0x1000000)
- axiom pow2_25 : (pow2 25 = 0x2000000)
- axiom pow2_26 : (pow2 26 = 0x4000000)
- axiom pow2_27 : (pow2 27 = 0x8000000)
- axiom pow2_28 : (pow2 28 = 0x10000000)
- axiom pow2_29 : (pow2 29 = 0x20000000)
- axiom pow2_30 : (pow2 30 = 0x40000000)
- axiom pow2_31 : (pow2 31 = 0x80000000)
- axiom pow2_32 : (pow2 32 = 0x100000000)
- axiom pow2_33 : (pow2 33 = 0x200000000)
- axiom pow2_34 : (pow2 34 = 0x400000000)
- axiom pow2_35 : (pow2 35 = 0x800000000)
- axiom pow2_36 : (pow2 36 = 0x1000000000)
- axiom pow2_37 : (pow2 37 = 0x2000000000)
- axiom pow2_38 : (pow2 38 = 0x4000000000)
- axiom pow2_39 : (pow2 39 = 0x8000000000)
- axiom pow2_40 : (pow2 40 = 0x10000000000)
- axiom pow2_41 : (pow2 41 = 0x20000000000)
- axiom pow2_42 : (pow2 42 = 0x40000000000)
- axiom pow2_43 : (pow2 43 = 0x80000000000)
- axiom pow2_44 : (pow2 44 = 0x100000000000)
- axiom pow2_45 : (pow2 45 = 0x200000000000)
- axiom pow2_46 : (pow2 46 = 0x400000000000)
- axiom pow2_47 : (pow2 47 = 0x800000000000)
- axiom pow2_48 : (pow2 48 = 0x1000000000000)
- axiom pow2_49 : (pow2 49 = 0x2000000000000)
- axiom pow2_50 : (pow2 50 = 0x4000000000000)
- axiom pow2_51 : (pow2 51 = 0x8000000000000)
- axiom pow2_52 : (pow2 52 = 0x10000000000000)
- axiom pow2_53 : (pow2 53 = 0x20000000000000)
- axiom pow2_54 : (pow2 54 = 0x40000000000000)
- axiom pow2_55 : (pow2 55 = 0x80000000000000)
- axiom pow2_56 : (pow2 56 = 0x100000000000000)
-
- axiom pow2_57 : (pow2 57 = 0x200000000000000)
-
- axiom pow2_58 : (pow2 58 = 0x400000000000000)
-
- axiom pow2_59 : (pow2 59 = 0x800000000000000)
-
- axiom pow2_60 : (pow2 60 = 0x1000000000000000)
-
- axiom pow2_61 : (pow2 61 = 0x2000000000000000)
-
- axiom pow2_62 : (pow2 62 = 0x4000000000000000)
-
- axiom pow2_63 : (pow2 63 = 0x8000000000000000)
-
- axiom pow2_64 : (pow2 64 = 0x10000000000000000)
-
- (* use bv.Pow2int *)
-
- function abs (x:real) : real = if (0.0 <= x) then x else (-x)
-
- axiom Abs_le : forall x:real, y:real. (abs x <= y) <-> ((-y) <= x) /\
- (x <= y)
-
- axiom Abs_pos : forall x:real. (0.0 <= abs x)
-
- axiom Abs_sum : forall x:real, y:real. (abs (x + y) <= (abs x + abs y))
-
- axiom Abs_prod : forall x:real, y:real. (abs (x * y) = (abs x * abs y))
-
- axiom triangular_inequality : forall x:real, y:real, z:real. (abs
- (x - z) <= (abs (x - y) + abs (y - z)))
-
- (* use real.Abs *)
-
- function from_int int : real
-
- axiom Zero [@useraxiom] : (from_int 0 = 0.0)
-
- axiom One [@useraxiom] : (from_int 1 = 1.0)
-
- axiom Add [@useraxiom] : forall x:int, y:int. (from_int (x + y) = (from_int
- x + from_int y))
-
- axiom Sub [@useraxiom] : forall x:int, y:int. (from_int (x - y) = (from_int
- x - from_int y))
-
- axiom Mul [@useraxiom] : forall x:int, y:int. (from_int (x * y) = (from_int
- x * from_int y))
-
- axiom Neg [@useraxiom] : forall x:int. (from_int (-x) = (-from_int x))
-
- axiom Injective : forall x:int, y:int. (from_int x = from_int y) -> (x = y)
-
- axiom Monotonic [@useraxiom] : forall x:int, y:int. (x <= y) -> (from_int
- x <= from_int y)
-
- (* use real.FromInt *)
-
- function truncate real : int
-
- axiom Truncate_int [@useraxiom] : forall i:int. (truncate (from_int i) = i)
-
- axiom Truncate_down_pos [@useraxiom] : forall x:real. (0.0 <= x) -> (from_int
- (truncate x) <= x) /\ (x < from_int (truncate x + 1))
-
- axiom Truncate_up_neg [@useraxiom] : forall x:real. (x <= 0.0) -> (from_int
- (truncate x - 1) < x) /\ (x <= from_int (truncate x))
-
- axiom Real_of_truncate [@useraxiom] : forall x:real. ((x - 1.0) <= from_int
- (truncate x)) /\ (from_int (truncate x) <= (x + 1.0))
-
- axiom Truncate_monotonic [@useraxiom] : forall x:real, y:real. (x <= y) ->
- (truncate x <= truncate y)
-
- axiom Truncate_monotonic_int1 [@useraxiom] : forall x:real, i:int.
- (x <= from_int i) -> (truncate x <= i)
-
- axiom Truncate_monotonic_int2 [@useraxiom] : forall x:real, i:int. (from_int
- i <= x) -> (i <= truncate x)
-
- function floor real : int
-
- function ceil real : int
-
- axiom Floor_int [@useraxiom] : forall i:int. (floor (from_int i) = i)
-
- axiom Ceil_int [@useraxiom] : forall i:int. (ceil (from_int i) = i)
-
- axiom Floor_down [@useraxiom] : forall x:real. (from_int (floor x) <= x) /\
- (x < from_int (floor x + 1))
-
- axiom Ceil_up [@useraxiom] : forall x:real. (from_int (ceil x - 1) < x) /\
- (x <= from_int (ceil x))
-
- axiom Floor_monotonic [@useraxiom] : forall x:real, y:real. (x <= y) ->
- (floor x <= floor y)
-
- axiom Ceil_monotonic [@useraxiom] : forall x:real, y:real. (x <= y) -> (ceil
- x <= ceil y)
-
- (* use real.Truncate *)
-
- (* use real.RealInfix *)
-
- type mode =
- | RNE
- | RNA
- | RTP
- | RTN
- | RTZ
-
- predicate to_nearest (m:mode) = (m = RNE) \/ (m = RNA)
-
- (* use ieee_float.RoundingMode *)
-
- function zeroF : t19
-
- function add mode t19 t19 : t19
-
- function sub mode t19 t19 : t19
-
- function mul mode t19 t19 : t19
-
- function div mode t19 t19 : t19
-
- function abs1 t19 : t19
-
- function neg t19 : t19
-
- function fma mode t19 t19 t19 : t19
-
- function sqrt mode t19 : t19
-
- function roundToIntegral mode t19 : t19
-
- function min t19 t19 : t19
-
- function max t19 t19 : t19
-
- predicate le t19 t19
-
- predicate lt t19 t19
-
- predicate eq t19 t19
-
- predicate is_normal t19
-
- predicate is_subnormal t19
-
- predicate is_zero t19
-
- predicate is_infinite t19
-
- predicate is_nan t19
-
- predicate is_positive t19
-
- predicate is_negative t19
-
- predicate is_plus_infinity (x:t19) = is_infinite x /\ is_positive x
-
- predicate is_minus_infinity (x:t19) = is_infinite x /\ is_negative x
-
- predicate is_plus_zero (x:t19) = is_zero x /\ is_positive x
-
- predicate is_minus_zero (x:t19) = is_zero x /\ is_negative x
-
- function of_int mode int : t19
-
- function to_int mode t19 : int
-
- function round mode real : real
-
- function max_int : int
-
- predicate in_range (x:real) = ((-0x1.FFFFFFFFFFFFFp1023) <= x) /\
- (x <= 0x1.FFFFFFFFFFFFFp1023)
-
- predicate in_int_range (i:int) = ((-max_int) <= i) /\ (i <= max_int)
-
- predicate no_overflow (m:mode) (x:real) = in_range (round m x)
-
- predicate in_safe_int_range (i:int) = ((-9007199254740992) <= i) /\
- (i <= 9007199254740992)
-
- predicate same_sign (x:t19) (y:t19) = is_positive x /\ is_positive y \/
- is_negative x /\ is_negative y
-
- predicate diff_sign (x:t19) (y:t19) = is_positive x /\ is_negative y \/
- is_negative x /\ is_positive y
-
- predicate product_sign (z:t19) (x:t19) (y:t19) = (same_sign x y ->
- is_positive z) /\ (diff_sign x y -> is_negative z)
-
- 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 sign_zero_result (m:mode) (x:t19) = is_zero x ->
- match m with
- | RTN -> is_negative x
- | _ -> is_positive x
- end
-
- function sqr (x:real) : real = (x * 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 *)
-
- type input_type = t19
-
- (* use caisar.NNet *)
-
- type tuple5 'a 'a1 'a2 'a3 'a4 =
- | Tuple5 'a 'a1 'a2 'a3 'a4
-
- (* use why3.Tuple5.Tuple51 *)
-
- function nnet_apply t19 t19 t19 t19 t19 : tuple5 t19 t19 t19 t19 t19
-
- (* use AsTuple *)
-
- (* meta syntax_type type int, "int", 0 *)
-
- (* meta syntax_type type real, "real", 0 *)
-
- (* meta syntax_logic predicate infix_eq, "(%1 = %2)", 0 *)
-
- (* meta eliminate_algebraic "keep_enums" *)
-
- (* meta eliminate_algebraic "keep_recs" *)
-
- (* meta syntax_type type bool, "bool", 0 *)
-
- (* meta syntax_logic function True, "true", 0 *)
-
- (* meta syntax_logic function False, "false", 0 *)
-
- (* meta syntax_type type tuple0, "unit", 0 *)
-
- (* meta syntax_logic function Tuple01, "void", 0 *)
-
- (* meta syntax_logic function zero, "0", 0 *)
-
- (* meta syntax_logic function one1, "1", 0 *)
-
- (* meta syntax_logic function infix_pl, "(%1 + %2)", 0 *)
-
- (* meta syntax_logic function infix_mn3, "(%1 - %2)", 0 *)
-
- (* meta syntax_logic function infix_as, "(%1 * %2)", 0 *)
-
- (* meta syntax_logic function prefix_mn, "(-%1)", 0 *)
-
- (* meta invalid trigger predicate infix_lseq *)
-
- (* meta invalid trigger predicate infix_ls *)
-
- (* meta invalid trigger predicate infix_gteq *)
-
- (* 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
-
- (* meta caisar_input function x1, 0 *)
-
- function x2 [@introduced] : t19
-
- (* meta caisar_input function x2, 1 *)
-
- function x3 [@introduced] : t19
-
- (* meta caisar_input function x3, 2 *)
-
- function x4 [@introduced] : t19
-
- (* meta caisar_input function x4, 3 *)
-
- function x5 [@introduced] : t19
-
- (* meta caisar_input function x5, 4 *)
-
- axiom H [@introduced] : lt 0.0 x1
-
- axiom H1 [@introduced] : lt x1 0.5
-
- function y : t19
-
- (* meta caisar_output function y, 0 *)
-
- function y1 : t19
-
- (* meta caisar_output function y1, 1 *)
-
- function y2 : t19
-
- (* meta caisar_output function y2, 2 *)
-
- function y3 : t19
-
- (* meta caisar_output function y3, 3 *)
-
- function y4 : t19
-
- (* meta caisar_output function y4, 4 *)
-
- goal G : lt 0.0 y /\ lt y 0.5
-
- end
+ (0.0 < x0)
+ (x0 < 0.5)
+ (0.0 < y0)
+ (y0 < 0.5)