diff --git a/src_colibri2/stdlib/std.ml b/src_colibri2/stdlib/std.ml
index 1bdb9f52d8f453e718f322ed354aacbf8d1ee2cd..b61fc8fc9469ab3f7104f3b45dc8f96d056c3bbe 100644
--- a/src_colibri2/stdlib/std.ml
+++ b/src_colibri2/stdlib/std.ml
@@ -76,7 +76,7 @@ module Q = struct
let two = Q.of_int 2
let ge = Q.geq
let le = Q.leq
-
+
let of_string_decimal =
let decimal = Str.regexp "\\(+\\|-\\)?\\([0-9]+\\)\\([.]\\([0-9]*\\)\\)?" in
fun s ->
diff --git a/src_colibri2/stdlib/std.mli b/src_colibri2/stdlib/std.mli
index e4100647a86f0536591dea6e08d5329a4a3a8a39..f5993258054b65c1e3fa6d51889148303e67cd29 100644
--- a/src_colibri2/stdlib/std.mli
+++ b/src_colibri2/stdlib/std.mli
@@ -51,7 +51,7 @@ module Goption : sig
end
module Q : sig
- include module type of Q
+ include module type of Q with type t = Q.t
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
val two : t
val ge : t -> t -> bool
diff --git a/src_colibri2/theories/LRA/dune b/src_colibri2/theories/LRA/dune
index 5a2ed7841d09ff5c9d32f4cafc88b19722b96696..0dade57c5cf443398ec7916c8b74b9404bdb5e8c 100644
--- a/src_colibri2/theories/LRA/dune
+++ b/src_colibri2/theories/LRA/dune
@@ -5,7 +5,8 @@
(libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
colibri2.core.structures colibri2.core colibri2.theories.bool)
(preprocess
- (pps ppx_deriving.std))
+ (pps ppx_deriving.std ppx_hash
+ ))
(flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
Containers -open Colibri2_stdlib -open Std -open Colibri2_core -open
Colibri2_theories_bool)
diff --git a/src_colibri2/theories/LRA/interval.ml b/src_colibri2/theories/LRA/interval.ml
index f512a3cc2aca5d58ab239f3b25dfc4433da502e1..699636932696478e1f020a9d8abbb352004634c0 100644
--- a/src_colibri2/theories/LRA/interval.ml
+++ b/src_colibri2/theories/LRA/interval.ml
@@ -352,6 +352,187 @@ module Convexe = struct
end
+module ConvexeWithDivider = struct
+
+ (** modulo = 0 -> no modulo *)
+ type t = { c: Convexe.t; divider: Q.t }
+ [@@ deriving eq, ord, hash]
+
+ let pp fmt t =
+ Format.fprintf fmt "%a%t"
+ Convexe.pp t.c
+ (fun fmt ->
+ if not (Q.equal t.divider Q.zero)
+ then Format.fprintf fmt "%%%a" Q.pp t.divider
+ )
+
+
+ include Popop_stdlib.MkDatatype(struct
+ type nonrec t = t
+ let equal = equal let compare = compare
+ let hash = hash let pp = pp
+ end)
+
+ let invariant e =
+ Convexe.invariant e.c &&
+ match Q.classify e.divider with
+ | Q.ZERO -> true
+ | Q.NZERO ->
+ let large_finite_bound b v inf =
+ match b with
+ | Strict -> Q.equal v inf
+ | Large -> true
+ in
+ large_finite_bound e.c.minb e.c.minv Q.minus_inf &&
+ large_finite_bound e.c.maxb e.c.maxv Q.inf
+ | Q.INF | Q.MINF | Q.UNDEF -> false
+
+ let tighten_bounds e =
+ if Q.equal e.divider Q.zero then Some e
+ else
+ let round ~add ~divisible_up_to ~minus_inf ~minv ~minb =
+ if Q.equal minv minus_inf
+ then minb, minv
+ else
+ let minv' = divisible_up_to minv e.divider in
+ Large, begin match minb with
+ | Strict when Q.equal minv' minv -> add minv e.divider
+ | _ -> minv'
+ end
+ in
+ let minb,minv =
+ round ~add:Q.add ~divisible_up_to:Colibrics_lib.Q.divisible_up_to
+ ~minus_inf:Q.minus_inf ~minv:e.c.Convexe.minv ~minb:e.c.Convexe.minb
+ in
+ let maxb,maxv =
+ round ~add:Q.sub ~divisible_up_to:Colibrics_lib.Q.divisible_down_to
+ ~minus_inf:Q.inf ~minv:e.c.Convexe.maxv ~minb:e.c.Convexe.maxb
+ in
+ if Q.lt maxv minv
+ then None
+ else Some { c = { minv; minb; maxv; maxb }; divider = e.divider }
+
+ let is_singleton e = Convexe.is_singleton e.c
+
+ let singleton s = { c = Convexe.singleton s; divider = s }
+
+ let except e x =
+ (Convexe.except e.c x)
+ |> Opt.map (fun c -> { e with c })
+ |> function
+ | None -> None
+ | Some s -> tighten_bounds s
+
+ let lower_min_max e1 e2 = Convexe.lower_min_max e1.c e2.c
+
+ let bigger_min_max e1 e2 = Convexe.bigger_min_max e1.c e2.c
+
+ let is_comparable e1 e2 = Convexe.is_comparable e1.c e2.c
+
+ let is_distinct e1 e2 = Convexe.is_distinct e1.c e2.c
+
+ let divisible q d =
+ Q.equal d Q.zero ||
+ Colibrics_lib.Q.divisible q d
+
+ let is_included e1 e2 =
+ Convexe.is_included e1.c e2.c &&
+ begin
+ Q.equal e2.divider Q.zero ||
+ (not (Q.equal e1.divider Q.zero) &&
+ divisible e1.divider e2.divider
+ )
+ end
+
+ let mem x e = Convexe.mem x e.c && begin
+ divisible x e.divider
+ end
+
+ let mult_cst q e =
+ assert (Q.is_real q);
+ { c = Convexe.mult_cst q e.c;
+ divider = Q.abs (Colibrics_lib.Q.mult_cst_divisible e.divider q) }
+
+ let add_cst q e =
+ if Q.equal q Q.zero then e
+ else
+ let divider = Colibrics_lib.Q.union_divisible q e.divider in
+ { c = Convexe.add_cst q e.c; divider }
+
+ let add e1 e2 =
+ { c = Convexe.add e1.c e2.c;
+ divider = Colibrics_lib.Q.union_divisible e1.divider e2.divider }
+
+ let minus e1 e2 =
+ { c = Convexe.minus e1.c e2.c;
+ divider = Colibrics_lib.Q.union_divisible e1.divider e2.divider }
+
+ let div_unknown c = { c; divider = Q.zero }
+
+ let gt q = div_unknown (Convexe.gt q)
+
+ let ge q = div_unknown (Convexe.ge q)
+
+ let lt q = div_unknown (Convexe.lt q)
+
+ let le q = div_unknown (Convexe.le q)
+
+ let union e1 e2 =
+ { c = Convexe.union e1.c e2.c;
+ divider = Colibrics_lib.Q.union_divisible e1.divider e2.divider }
+
+ let inter e1 e2 =
+ match Convexe.inter e1.c e2.c with
+ | None -> None
+ | Some c ->
+ tighten_bounds
+ { c; divider = Colibrics_lib.Q.inter_divisible e1.divider e2.divider }
+
+ (** intersection set.
+ if the two arguments are equals, return the second
+ *)
+
+ let zero = div_unknown Convexe.zero
+ let reals = div_unknown Convexe.reals
+ let () = assert (invariant reals)
+
+ let is_reals e = Convexe.is_reals e.c && Q.equal e.divider Q.zero
+
+ let choose e =
+ let q = Convexe.choose e.c in
+ if Q.equal e.divider Q.zero
+ then q
+ else Colibrics_lib.Q.divisible_down_to q e.divider
+
+ let split_heuristic e =
+ let rec aux divider c =
+ match Convexe.split_heuristic c with
+ | `Singleton c -> `Singleton c
+ | `NotSplitted -> `NotSplitted
+ | `Splitted (a,b) ->
+ match tighten_bounds { c = a; divider },
+ tighten_bounds { c = b; divider } with
+ | Some a, Some b -> `Splitted (a,b)
+ | None, None -> assert false
+ | None, Some a -> aux divider a.c
+ | Some a, None -> aux divider a.c
+ in
+ aux e.divider e.c
+
+ let nb_incr = 100
+ let z_nb_incr = Z.of_int nb_incr
+ let choose_rnd _ = assert false
+
+ let get_convexe_hull e = Convexe.get_convexe_hull e.c
+
+ let is_Large = function
+ | Large -> true
+ | Strict -> false
+
+ let divided_by divider = { c = Convexe.reals; divider }
+
+end
+
module ConvexeWithExceptions = struct
type t = {con: Convexe.t; exc: Q.S.t}
diff --git a/src_colibri2/theories/LRA/interval.mli b/src_colibri2/theories/LRA/interval.mli
index c6daa364c2470b3d064bdde60e56ad1f6b8e0816..ee38207b26145960a4a505254aea026e117eb67e 100644
--- a/src_colibri2/theories/LRA/interval.mli
+++ b/src_colibri2/theories/LRA/interval.mli
@@ -38,6 +38,16 @@ module Convexe: sig
val inter_with_integer: t -> t option
end
+module ConvexeWithDivider: sig
+ include Interval_sig.S
+ val split_heuristic: t ->
+ [ `Singleton of Q.t
+ | `Splitted of t * t
+ | `NotSplitted ]
+
+ val divided_by: Q.t -> t
+end
+
module ConvexeWithExceptions: Interval_sig.S
module Union : Interval_sig.S
diff --git a/src_common/colibrics_lib.ml b/src_common/colibrics_lib.ml
index f6a0382e2767a7989617bbfd4bff465ea3000dc3..cec78e906cb51c9f31ffd397873a48c314f2d458 100644
--- a/src_common/colibrics_lib.ml
+++ b/src_common/colibrics_lib.ml
@@ -2,7 +2,32 @@ module Q = struct
(** Add some useful function to Q of zarith *)
let floor = Q__Q.floor
+ (** [floor a] return the greatest integer smaller or equal than [a] *)
+
let ceil = Q__Q.ceil
- let modulo_down_to = Modulo__Modulo.round_down_to
- let modulo_up_to = Modulo__Modulo.round_up_to
+ (** [ceil a] return the smallest integer greater or equal than [a] *)
+
+ let divisible_down_to = Modulo__Divisible.round_down_to
+ (** [divisible_down_to a m] return the greatest multiple of [m] smaller or equal
+ than [a] *)
+
+ let divisible_up_to = Modulo__Divisible.round_up_to
+ (** [divisible_down_to a m] return the smallest multiple of [m] greater or equal
+ than [a] *)
+
+ let divisible = Modulo__Divisible.divisible
+ (** [divisible a b] test if a is divisible by b *)
+
+ let mult_cst_divisible = Modulo__Divisible.mult_cst_divisible
+ (** [mult_cst_divisible a b] *)
+
+ let union_divisible a b =
+ if Q.equal a Q.zero || Q.equal b Q.zero then Q.zero
+ else Modulo__Divisible.union_divisible a b
+
+ let inter_divisible a b =
+ if Q.equal a Q.zero then b else
+ if Q.equal b Q.zero then a
+ else Modulo__Divisible.inter_divisible a b
+
end
diff --git a/src_common/common.drv b/src_common/common.drv
index bf681af869c90d120cf1f01c38a7db8796aefc77..b52a71c5b40ac595fc151a2e65fa3e52f38f2e6c 100644
--- a/src_common/common.drv
+++ b/src_common/common.drv
@@ -2,6 +2,9 @@ module q.Q
syntax type t "Q.t"
+ syntax val num "%1.Q.num"
+ syntax val den "%1.Q.den"
+
syntax val ZERO "Q.ZERO"
syntax val MINF "Q.MINF"
syntax val INF "Q.INF"
@@ -17,11 +20,17 @@ module q.Q
syntax val to_int "Q.to_bigint %1"
syntax val of_int "Q.of_bigint %1"
syntax val (=) "Q.equal %1 %2"
+ syntax val make "Q.make %1 %2"
+ syntax val make_exact "{ Q.num = %1; Q.den = %2 }"
end
module q.Z
syntax val fdiv "Z.fdiv %1 %2"
syntax val cdiv "Z.cdiv %1 %2"
+ syntax val divisible "Z.divisible %1 %2"
+
+ syntax val gcd "Z.gcd %1 %2"
+ syntax val lcm "Z.lcm %1 %2"
end
diff --git a/src_common/dune b/src_common/dune
index 1118fad81479aab7dcbd767a9bc7a0c725f520c5..7a405b4363708a17aca65ed1dfc19dfee558e13b 100644
--- a/src_common/dune
+++ b/src_common/dune
@@ -5,23 +5,52 @@
)
(rule
- (targets modulo__Modulo.ml q__Q.ml)
+ (targets modulo__Divisible.ml q__Q.ml)
(deps q.mlw modulo.mlw)
- (action (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L . modulo.Modulo q.Q))
+ (action (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L . modulo.Divisible q.Q))
(mode promote)
)
+(rule
+ (alias runproof)
+ (deps (source_tree q) q.mlw)
+ (action (run why3 replay -L . q))
+)
+
(rule
(alias runproof)
(deps (source_tree modulo) modulo.mlw q.mlw)
(action (run why3 replay -L . modulo))
)
+; (rule
+; (alias runproof)
+; (deps (source_tree modulo) interval.mlw modulo.mlw q.mlw)
+; (action (run why3 replay -L . interval))
+; )
+
+; (rule
+; (alias ide:q)
+; (deps (universe) q.mlw)
+; (action (run why3 ide -L . q.mlw))
+; )
+
+; (rule
+; (alias ide:modulo)
+; (deps (universe) q.mlw modulo.mlw)
+; (action (run why3 ide -L . modulo.mlw))
+; )
+
+; (rule
+; (alias ide:interval)
+; (deps (universe) q.mlw modulo.mlw interval.mlw)
+; (action (run why3 ide -L . interval.mlw))
+; )
(rule
- (alias runproof)
+ (alias runsmokedetector)
(deps (source_tree q) q.mlw)
- (action (run why3 replay -L . q))
+ (action (run why3 replay -L . q --smoke-detector deep))
)
(rule
@@ -30,9 +59,8 @@
(action (run why3 replay -L . modulo --smoke-detector deep))
)
-
(rule
(alias runsmokedetector)
- (deps (source_tree q) q.mlw)
- (action (run why3 replay -L . q --smoke-detector deep))
+ (deps (source_tree modulo) interval.mlw modulo.mlw q.mlw)
+ (action (run why3 replay -L . interval --smoke-detector deep))
)
diff --git a/src_common/interval.mlw b/src_common/interval.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..fefa2748ab7839783ab7aa1288aa23f7f8d39a80
--- /dev/null
+++ b/src_common/interval.mlw
@@ -0,0 +1,299 @@
+module Bound
+ type t = Strict | Large
+
+ (* let compare_inf b1 b2 = match b1,b2 with *)
+ (* | Large, Strict -> -1 *)
+ (* | Strict, Large -> 1 *)
+ (* | Large, Large | Strict, Strict -> 0 *)
+
+ (* let compare_inf_sup b1 b2 = match b1,b2 with *)
+ (* | Large, Strict -> 1 *)
+ (* | Strict, Large -> 1 *)
+ (* | Large, Large -> 0 *)
+ (* | Strict, Strict -> 1 *)
+
+ (* let compare_sup b1 b2 = - (compare_inf b1 b2) *)
+
+end
+
+module Convexe
+ use option.Option
+ use q.Q as Q
+ use Bound as Bound
+
+ type t = { minb : Bound.t; minv: Q.t; maxv: Q.t; maxb: Bound.t }
+ invariant { not (Q.is_nan minv) }
+ invariant { not (Q.is_nan maxv) }
+ invariant { not (Q.is_plus_inf minv) }
+ invariant { not (Q.is_minus_inf maxv) }
+ invariant {
+ if Q.(equal minv maxv)
+ then minb = Bound.Large /\ maxb = Bound.Large
+ else Q.(minv < maxv)
+ }
+ by { minb = Bound.Large; minv = Q.of_int 0; maxv = Q.of_int 0; maxb = Bound.Large }
+
+ predicate mem (x:Q.t) (e:t) =
+ (match e.minb with
+ | Bound.Strict -> Q.(e.minv < x)
+ | Bound.Large -> Q.(e.minv <= x)
+ end)
+ &&
+ (match e.maxb with
+ | Bound.Strict -> Q.(x < e.maxv)
+ | Bound.Large -> Q.(x <= e.maxv)
+ end)
+
+ let is_singleton e
+ ensures { forall q. mem q e -> (forall q'. mem q' e -> Q.equal q q') -> result = Some q }
+ ensures { (exists q q'. not (Q.equal q q') /\ mem q e /\ mem q' e) -> result = None }
+ =
+ if Q.(e.minv = e.maxv) then Some e.minv else begin
+ ghost (if e.minb = Bound.Strict then begin assert { forall q. mem q e -> Q.(e.minv < q) }; assert { forall q. mem q e -> Q.(e.maxv < q) }; absurd end );
+ assert { e.minb = Bound.Large };
+ assert { e.maxb = Bound.Large };
+ None
+ end
+
+ let singleton q
+ ensures { mem q result }
+ ensures { forall q'. mem q' result -> Q.equal q q' }
+ =
+ {minb=Bound.Large; minv = q; maxv = q; maxb=Bound.Large}
+
+(*
+ let except e x =
+ let is_min = Q.equal e.minv x in
+ let is_max = Q.equal e.maxv x in
+ if is_min && is_max then None
+ else if is_min
+ then Some {e with minb=Strict}
+ else if Q.equal e.maxv x
+ then Some {e with maxb=Strict}
+ else Some e
+
+ let lower_min_max e1 e2 =
+ let c = Q.compare e1.minv e2.minv in
+ match e1.minb, e2.minb with
+ | Strict, Large when c = 0 -> e2,e1, false
+ | _ when c <= 0 -> e1,e2, true
+ | _ -> e2,e1, false
+
+ let bigger_min_max e1 e2 =
+ let c = Q.compare e1.maxv e2.maxv in
+ match e1.maxb, e2.maxb with
+ | Strict, Large when c = 0 -> e1,e2, true
+ | _ when c >= 0 -> e2,e1, false
+ | _ -> e1,e2, true
+
+
+ let is_comparable e1 e2 =
+ (** x1 in e1, x2 in e2 *)
+ (** order by the minimum *)
+ let emin,emax,same = lower_min_max e1 e2 in (** emin.minv <= emax.minv *)
+ (** look for inclusion *)
+ let c = Q.compare emin.maxv emax.minv in
+ match emin.maxb, emax.minb with
+ (** emin.minv <? e1 <? emin.maxv < emax.minv <? e2 <? emax.maxv *)
+ | _ when c < 0 -> if same then `Lt else `Gt
+ (** emin.minv <? e1 < emin.maxv = emax.minv < e2 <? emax.maxv *)
+ (** emin.minv <? e1 < emin.maxv = emax.minv <= e2 <? emax.maxv *)
+ (** emin.minv <? e1 <= emin.maxv = emax.minv < e2 <? emax.maxv *)
+ | Strict, Strict | Strict, Large | Large, Strict
+ when c = 0 ->
+ if same then `Lt else `Gt
+ | _ -> `Uncomparable
+
+ let is_distinct e1 e2 =
+ match is_comparable e1 e2 with
+ | `Uncomparable -> false
+ | _ -> true
+
+ let is_included e1 e2 =
+ assert (invariant e1);
+ assert (invariant e2);
+ compare_bounds_inf (e2.minv,e2.minb) (e1.minv,e1.minb) <= 0 &&
+ compare_bounds_sup (e1.maxv,e1.maxb) (e2.maxv,e2.maxb) <= 0
+
+ let mem x e =
+ (match e.minb with
+ | Strict -> Q.lt e.minv x
+ | Large -> Q.le e.minv x)
+ &&
+ (match e.maxb with
+ | Strict -> Q.lt x e.maxv
+ | Large -> Q.le x e.maxv)
+
+ let mult_pos q e =
+ {e with minv = Q.mul e.minv q; maxv = Q.mul e.maxv q}
+
+ let mult_neg q e =
+ { minb = e.maxb; maxb = e.minb;
+ minv = Q.mul e.maxv q;
+ maxv = Q.mul e.minv q }
+
+ let mult_cst q e =
+ assert (Q.is_real q);
+ let c = Q.sign q in
+ if c = 0 then singleton Q.zero
+ else if c > 0 then mult_pos q e
+ else mult_neg q e
+
+ let add_cst q e =
+ {e with minv = Q.add e.minv q; maxv = Q.add e.maxv q}
+
+ let mult_bound b1 b2 =
+ match b1, b2 with
+ | Large , Large -> Large
+ | _ -> Strict
+
+ let add e1 e2 =
+ let t = {minb = mult_bound e1.minb e2.minb;
+ minv = Q.add e1.minv e2.minv;
+ maxv = Q.add e1.maxv e2.maxv;
+ maxb = mult_bound e1.maxb e2.maxb} in
+ assert (invariant t); t
+
+ let minus e1 e2 =
+ add e1 (mult_neg Q.minus_one e2)
+
+ let gt q =
+ let t = {minb=Strict; minv = q; maxv = Q.inf; maxb= Strict} in
+ assert (invariant t); t
+
+ let ge q =
+ let t = {minb=Large; minv = q; maxv = Q.inf; maxb= Strict} in
+ assert (invariant t); t
+
+ let lt q =
+ let t = {minb=Strict; minv = Q.minus_inf; maxv = q; maxb= Strict} in
+ assert (invariant t); t
+
+ let le q =
+ let t = {minb=Strict; minv = Q.minus_inf; maxv = q; maxb= Large} in
+ assert (invariant t); t
+
+ let union e1 e2 =
+ let emin,_,_ = lower_min_max e1 e2 in
+ let _,emax,_ = bigger_min_max e1 e2 in
+ {minb = emin.minb; minv = emin.minv;
+ maxv = emax.maxv; maxb = emax.maxb}
+
+ let inter e1 e2 =
+ let (minv,minb) as min =
+ if compare_bounds_inf (e1.minv,e1.minb) (e2.minv,e2.minb) < 0
+ then (e2.minv,e2.minb) else (e1.minv,e1.minb)
+ in
+ let (maxv,maxb) as max =
+ if compare_bounds_sup (e1.maxv,e1.maxb) (e2.maxv,e2.maxb) < 0
+ then (e1.maxv,e1.maxb) else (e2.maxv,e2.maxb)
+ in
+ if compare_bounds_inf_sup min max > 0
+ then None
+ else if Q.equal minv maxv && equal_bound minb Large && equal_bound maxb Large
+ then Some (singleton minv)
+ else Some {minv;minb;maxv;maxb}
+
+ let inter e1 e2 =
+ let r = inter e1 e2 in
+ assert (Opt.for_all invariant r);
+ r
+
+ (** intersection set.
+ if the two arguments are equals, return the second
+ *)
+
+ let zero = singleton Q.zero
+ let reals = {minb=Strict; minv=Q.minus_inf; maxb=Strict; maxv=Q.inf}
+ let () = assert (invariant reals)
+
+ let is_reals = function
+ | {minb=Strict; minv; maxb=Strict; maxv}
+ when Q.equal minv Q.minus_inf &&
+ Q.equal maxv Q.inf -> true
+ | _ -> false
+
+ let choose = function
+ | {minb=Large;minv} -> minv
+ | {maxb=Large;maxv} -> maxv
+ | {minv;maxv} when Q.equal Q.minus_inf minv && Q.equal Q.inf maxv ->
+ Q.zero
+ | {minv;maxv} when Q.equal Q.minus_inf minv ->
+ Q.make (Z.sub (Q.to_bigint maxv) Z.one) Z.one
+ | {minv;maxv} when Q.equal Q.inf maxv ->
+ Q.make (Z.add (Q.to_bigint minv) Z.one) Z.one
+ | {minv;maxv} ->
+ let q = Q.make (Z.add Z.one (Q.to_bigint minv)) Z.one in
+ if Q.lt q maxv then q
+ else Q.add maxv (Q.div_2exp (Q.sub minv maxv) 1)
+
+ let split_heuristic c =
+ match is_singleton c with
+ | Some s -> `Singleton s
+ | None ->
+ let split_at mid =
+ let left,right =
+ if Q.equal mid c.maxv
+ then inter (lt mid) c, inter (ge mid) c
+ else inter (le mid) c, inter (gt mid) c
+ in
+ match left, right with
+ | Some left, Some right ->
+ `Splitted(left,right)
+ | _ -> assert false
+ in
+ if Q.equal Q.minus_inf c.minv || Q.equal Q.inf c.maxv then
+ if mem Q.zero c then split_at Q.zero
+ else `NotSplitted
+ else
+ let mid = Q.div_2exp (Q.add c.minv c.maxv) (-1) in
+ split_at mid
+
+ let nb_incr = 100
+ let z_nb_incr = Z.of_int nb_incr
+ let choose_rnd rnd = function
+ | {minv;maxv} when Q.equal Q.minus_inf minv ->
+ Q.make (Z.sub (Z.of_int (rnd nb_incr)) (Q.to_bigint maxv)) Z.one
+ | {minv;maxv} when Q.equal Q.inf maxv ->
+ Q.make (Z.add (Z.of_int (rnd nb_incr)) (Q.to_bigint minv)) Z.one
+ | {minv;maxv} when Q.equal minv maxv -> minv
+ | {minv;maxv} ->
+ let d = Q.sub maxv minv in
+ let i = 1 + rnd (nb_incr - 2) in
+ let x = Q.make (Z.of_int i) (Z.of_int 100) in
+ let q = Q.add minv (Q.mul x d) in
+ assert (Q.lt minv q);
+ assert (Q.lt q maxv);
+ q
+
+ let get_convexe_hull e =
+ let mk v b =
+ match Q.classify v with
+ | Q.ZERO | Q.NZERO -> Some (v,b)
+ | Q.INF | Q.MINF -> None
+ | Q.UNDEF -> assert false in
+ mk e.minv e.minb, mk e.maxv e.maxb
+
+ let is_Large = function
+ | Large -> true
+ | Strict -> false
+
+ let inter_with_integer t =
+ let t = {
+ minb = if Q.equal Q.minus_inf t.minv then Large else Strict;
+ minv =
+ if is_Large t.minb && Q.is_integer t.minv
+ then Q.add t.minv Q.one
+ else Q.ceil t.minv;
+ maxb = if Q.equal Q.inf t.maxv then Large else Strict;
+ maxv =
+ if is_Large t.maxb && Q.is_integer t.maxv
+ then Q.sub t.maxv Q.one
+ else Q.floor t.maxv;
+ } in
+ if Q.lt t.maxv t.minv then None else begin
+ assert (invariant t);
+ Some t
+ end
+*)
+end
diff --git a/src_common/modulo.mlw b/src_common/modulo.mlw
index 4f74c4ca0583d5be0445e6f82d68fc333a148197..5721f2dc0fa9259b9abf5dc72f42046bee24725c 100644
--- a/src_common/modulo.mlw
+++ b/src_common/modulo.mlw
@@ -1,13 +1,14 @@
-module Modulo
+module Divisible
use bool.Bool
+ use q.Z as Z
use q.Q as Q
use int.Int
use real.RealInfix
use real.Truncate
use real.FromInt
- exception ModuloFinitePositiveExpected
+ exception FinitePositiveExpected
let lemma round_modulo (a:real) (m:real): unit
requires { 0. <. m }
@@ -21,13 +22,15 @@ module Modulo
assert { f <=. d <. from_int (t + 1) };
assert { f <=. d <. f +. 1. };
assert { (a /. m) -. 1. <. f <=. a /. m };
+ assert { ((a /. m) -. 1.) *. m <. f *. m <=. (a /. m) *. m };
+ assert { ((a /. m) *. m) -. m <. f *. m };
assert { a -. m <. f *. m <=. a };
assert { -. a <=. -. f *. m <. -. a +. m };
assert { 0. <=. a -. f *. m <. m }
let round_down_to (a:Q.t) (m:Q.t) : (r:Q.t)
requires { Q.not_NaN a } requires { Q.not_NaN m }
- raises { ModuloFinitePositiveExpected -> not (Q.is_real m /\ 0. <. Q.real m ) }
+ raises { FinitePositiveExpected -> not (Q.is_real m /\ 0. <. Q.real m ) }
ensures { Q.not_NaN r }
ensures { a.Q.value = Q.PlusInf -> r.Q.value = Q.PlusInf }
ensures { Q.( r <= a) }
@@ -36,8 +39,8 @@ module Modulo
ensures { a.Q.is_real -> Q.( r.real <. a.real) -> forall q. not Q.(r.real <. (from_int q) *. m.real <=. a.real ) }
=
match Q.classify m with
- | Q.ZERO | Q.MINF | Q.INF | Q.UNDEF -> raise ModuloFinitePositiveExpected
- | Q.NZERO -> if Q.( m <= (of_int 0) ) then raise ModuloFinitePositiveExpected
+ | Q.ZERO | Q.MINF | Q.INF | Q.UNDEF -> raise FinitePositiveExpected
+ | Q.NZERO -> if Q.( m <= (of_int 0) ) then raise FinitePositiveExpected
end;
match Q.classify a with
| Q.MINF | Q.INF | Q.UNDEF | Q.ZERO -> a
@@ -50,7 +53,7 @@ module Modulo
let round_up_to (a:Q.t) (m:Q.t) : (r:Q.t)
requires { Q.not_NaN a } requires { Q.not_NaN m }
- raises { ModuloFinitePositiveExpected -> not (Q.is_real m /\ 0. <. Q.real m ) }
+ raises { FinitePositiveExpected -> not (Q.is_real m /\ 0. <. Q.real m ) }
ensures { Q.not_NaN r }
ensures { a.Q.value = Q.MinusInf -> r.Q.value = Q.MinusInf }
ensures { Q.(a <= r) }
@@ -61,8 +64,166 @@ module Modulo
let res = round_down_to Q.((of_int 0) - a) m in
assert { a.Q.value = Q.MinusInf -> res.Q.value = Q.PlusInf };
Q.((of_int 0) - res)
-
+ let lemma simple_mul_div (a b : real)
+ requires { b <> 0. }
+ ensures { (a /. b) *. b = a } =
+ ()
+ predicate ddivisible_using (a b:real) (d:int) =
+ a = (from_int d) *. b
+
+ predicate ddivisible (a b: real) =
+ exists d. ddivisible_using a b d
+
+
+ let lemma remove_product_right (a b c:int) : unit
+ requires { b <> 0 }
+ requires { a * b = c * b }
+ ensures { a = c } =
+ ()
+
+ let lemma divisible_to_z (a b:Q.t) (d:int) : (dnum:int, dden: int)
+ requires { a.Q.is_real } requires { b.Q.is_real } requires { b.Q.real <> 0. }
+ requires { ddivisible_using a.Q.real b.Q.real d }
+ ensures { Z.ddivisible_using a.Q.num b.Q.num dnum }
+ ensures { Z.ddivisible_using b.Q.den a.Q.den dden }
+ ensures { d = dnum * dden } =
+ assert { b.Q.den * a.Q.num = d * b.Q.num * a.Q.den
+ by from_int b.Q.den *. from_int a.Q.num = from_int d *. from_int b.Q.num *. from_int a.Q.den
+ by (from_int a.Q.num /. from_int a.Q.den) *. from_int a.Q.den *. from_int b.Q.den = (from_int d *. (from_int b.Q.num /. from_int b.Q.den)) *. from_int a.Q.den *. from_int b.Q.den
+ by from_int a.Q.num /. from_int a.Q.den = from_int d *. (from_int b.Q.num /. from_int b.Q.den)
+ };
+ let dnum = Z.prime_to_one_another_mul b.Q.num (d * a.Q.den) b.Q.den a.Q.num in
+ assert { Z.ddivisible_using a.Q.num b.Q.num dnum };
+ let dden = Z.prime_to_one_another_mul a.Q.num b.Q.den a.Q.den (d * b.Q.num) in
+ assert { Z.ddivisible_using b.Q.den a.Q.den dden };
+ assert { dnum * dden * b.Q.num * a.Q.den = d * b.Q.num * a.Q.den };
+ remove_product_right (dnum * dden * b.Q.num) a.Q.den (d * b.Q.num);
+ remove_product_right (dnum * dden) b.Q.num d;
+ (dnum,dden)
+
+ let lemma divisible_from_z (a b:Q.t) (dnum:int) (dden:int) : unit
+ requires { a.Q.is_real } requires { b.Q.is_real }
+ requires { Z.ddivisible_using a.Q.num b.Q.num dnum }
+ requires { Z.ddivisible_using b.Q.den a.Q.den dden }
+ ensures { ddivisible_using a.Q.real b.Q.real (dnum*dden) }
+ =
+ ghost (simple_mul_div (from_int a.Q.num) (from_int a.Q.den);
+ simple_mul_div (from_int b.Q.num) (from_int b.Q.den););
+ let ghost d = dnum * dden in
+ assert { a.Q.real = (from_int d) *. b.Q.real
+ by from_int a.Q.num /. from_int a.Q.den = from_int d *. (from_int b.Q.num /. from_int b.Q.den)
+ by (from_int a.Q.num /. from_int a.Q.den) *. (from_int b.Q.den /. from_int b.Q.den) = from_int d *. (from_int b.Q.num /. from_int b.Q.den) *. (from_int a.Q.den /. from_int a.Q.den)
+ by (from_int a.Q.num *. from_int b.Q.den) /. from_int a.Q.den /. from_int b.Q.den = (from_int d *. from_int b.Q.num *. from_int a.Q.den) /. from_int a.Q.den /. from_int b.Q.den
+ by from_int a.Q.num *. from_int b.Q.den = from_int d *. from_int b.Q.num *. from_int a.Q.den
+ by from_int a.Q.num *. from_int b.Q.den = from_int dnum *. from_int dden *. from_int b.Q.num *. from_int a.Q.den
+ by from_int a.Q.num *. from_int b.Q.den = from_int (dnum * b.Q.num) *. from_int (dden * a.Q.den)
+ }
+
+
+ let divisible (a:Q.t) (b:Q.t) : (r:bool,ghost d: int)
+ requires { a.Q.is_real } requires { b.Q.is_real } requires { b.Q.real <> 0. }
+ ensures { not r -> forall d. not (ddivisible_using a.Q.real b.Q.real d) }
+ ensures { r -> ddivisible_using a.Q.real b.Q.real d } =
+ let b1,dnum = Z.divisible a.Q.num b.Q.num in
+ if b1 then
+ let b2,dden = Z.divisible b.Q.den a.Q.den in
+ if b2 then
+ (true,dnum*dden)
+ else begin
+ let ghost () = if pure { exists d. ddivisible_using a.Q.real b.Q.real d } then
+ let d = any (d:int) ensures { ddivisible_using a.Q.real b.Q.real d } in
+ let _dnum, dden = divisible_to_z a b d in
+ assert { Z.ddivisible_using a.Q.den b.Q.den dden };
+ absurd
+ in
+ (false,ghost 0)
+ end
+ else begin
+ let ghost () = if pure { exists d. ddivisible_using a.Q.real b.Q.real d } then
+ let d = any (d:int) ensures { ddivisible_using a.Q.real b.Q.real d } in
+ let dnum, _dden = divisible_to_z a b d in
+ assert { Z.ddivisible_using a.Q.num b.Q.num dnum };
+ absurd
+ in
+ (false,ghost 0)
+ end
+
+ let mult_cst_divisible (a:Q.t) (q:Q.t) : (a':Q.t)
+ requires { q.Q.is_real } requires { a.Q.is_real }
+ ensures { a'.Q.is_real }
+ ensures { forall r. ddivisible r a.Q.real -> ddivisible (r *. q.Q.real ) a'.Q.real } =
+ let a' = Q.(a*q) in
+ let lemma post (r:real) : unit
+ requires { ddivisible r a.Q.real }
+ ensures { ddivisible (r *. q.Q.real) a'.Q.real } =
+ let d = any int ensures { ddivisible_using r a.Q.real result } in
+ assert {ddivisible_using (r *. q.Q.real) a'.Q.real d }
+ in
+ a'
+
+
+ let union_divisible (a:Q.t) (b:Q.t) : (u:Q.t)
+ requires { a.Q.is_real } requires { b.Q.is_real } requires { a.Q.real <> 0. } requires { b.Q.real <> 0. }
+ ensures { u.Q.is_real }
+ ensures { forall r. r.Q.is_real -> ddivisible r.Q.real a.Q.real -> ddivisible r.Q.real u.Q.real }
+ ensures { forall r. r.Q.is_real -> ddivisible r.Q.real b.Q.real -> ddivisible r.Q.real u.Q.real } =
+ let n,na',nb' = Z.gcd a.Q.num b.Q.num in
+ let d,da',db',_fa = Z.lcm a.Q.den b.Q.den in
+ assert { Z.prime_to_one_another a.Q.num a.Q.den };
+ assert { Z.prime_to_one_another b.Q.num b.Q.den };
+ assert { Z.prime_to_one_another n a.Q.den };
+ assert { Z.prime_to_one_another n b.Q.den };
+ assert { Z.prime_to_one_another n d };
+ let u = Q.make_exact n d in
+ let lemma post (r:Q.t) : unit
+ requires { a.Q.is_real } requires { r.Q.is_real }
+ requires { ddivisible r.Q.real a.Q.real }
+ ensures { ddivisible r.Q.real u.Q.real } =
+ let dd = any int ensures { ddivisible_using r.Q.real a.Q.real result } in
+ let dnum,dden = divisible_to_z r a dd in
+ assert { Z.ddivisible_using r.Q.num a.Q.num dnum };
+ assert { Z.ddivisible_using r.Q.num n (na'*dnum) };
+ assert { Z.ddivisible_using a.Q.den r.Q.den dden };
+ assert { Z.ddivisible_using d r.Q.den (dden*da') };
+ divisible_from_z r u (na'*dnum) (da'*dden);
+ assert { ddivisible_using r.Q.real u.Q.real (na'*dnum*da'*dden) }
+ in
+ let lemma post (r:Q.t) : unit
+ requires { b.Q.is_real } requires { r.Q.is_real }
+ requires { ddivisible r.Q.real b.Q.real }
+ ensures { ddivisible r.Q.real u.Q.real } =
+ let dd = any int ensures { ddivisible_using r.Q.real b.Q.real result } in
+ let dnum,dden = divisible_to_z r b dd in
+ assert { Z.ddivisible_using r.Q.num b.Q.num dnum };
+ assert { Z.ddivisible_using r.Q.num n (nb'*dnum) };
+ assert { Z.ddivisible_using b.Q.den r.Q.den dden };
+ assert { Z.ddivisible_using d r.Q.den (dden*db') };
+ divisible_from_z r u (nb'*dnum) (db'*dden);
+ assert { ddivisible_using r.Q.real u.Q.real (nb'*dnum*db'*dden) }
+ in
+ u
+
+
+ let inter_divisible (a:Q.t) (b:Q.t) : (u:Q.t)
+ requires { a.Q.is_real } requires { b.Q.is_real } requires { 0. <> a.Q.real } requires { 0. <> b.Q.real }
+ ensures { u.Q.is_real }
+ ensures { forall r. r.Q.is_real -> ddivisible r.Q.real a.Q.real -> ddivisible r.Q.real b.Q.real -> ddivisible r.Q.real u.Q.real } =
+ let n,na',_ = Z.gcd a.Q.den b.Q.den in
+ let d,_,_,fa = Z.lcm a.Q.num b.Q.num in
+ let u = Q.make_exact d n in
+ let lemma post (r:Q.t) : unit
+ requires { r.Q.is_real }
+ requires { ddivisible r.Q.real a.Q.real }
+ requires { ddivisible r.Q.real b.Q.real }
+ ensures { ddivisible r.Q.real u.Q.real } =
+ let dda = any int ensures { ddivisible_using r.Q.real a.Q.real result } in
+ let ddb = any int ensures { ddivisible_using r.Q.real b.Q.real result } in
+ let dnuma,ddena = divisible_to_z r a dda in
+ let _,_ = divisible_to_z r b ddb in
+ divisible_from_z r u (fa dnuma) (na'*ddena)
+ in
+ u
end
diff --git a/src_common/modulo/why3session.xml b/src_common/modulo/why3session.xml
index 45cc0fa2fdf81f845b246709ae8767f8977d2ff9..06503a0cc92046c3f0fb824602ce501787574a8e 100644
--- a/src_common/modulo/why3session.xml
+++ b/src_common/modulo/why3session.xml
@@ -5,148 +5,164 @@
<prover id="0" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.3.3" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.7" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="1000"/>
<file format="whyml" proved="true">
<path name=".."/><path name="modulo.mlw"/>
-<theory name="Modulo" proved="true">
+<theory name="Divisible" proved="true">
<goal name="round_modulo'vc" expl="VC for round_modulo" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_modulo'vc.0" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="3796"/></proof>
+ <proof prover="2"><result status="valid" time="0.04" steps="4325"/></proof>
</goal>
<goal name="round_modulo'vc.1" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.01" steps="4408"/></proof>
+ <proof prover="2"><result status="valid" time="0.04" steps="4971"/></proof>
</goal>
<goal name="round_modulo'vc.2" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="3878"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="4407"/></proof>
</goal>
<goal name="round_modulo'vc.3" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="3909"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="4438"/></proof>
</goal>
<goal name="round_modulo'vc.4" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.59" steps="343273"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="round_modulo'vc.4.0" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.68" steps="2347462"/></proof>
+ </goal>
+ <goal name="round_modulo'vc.4.1" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="15493"/></proof>
+ </goal>
+ </transf>
</goal>
<goal name="round_modulo'vc.5" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4007"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="4533"/></proof>
</goal>
<goal name="round_modulo'vc.6" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4045"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="round_modulo'vc.6.0" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="15693"/></proof>
+ </goal>
+ <goal name="round_modulo'vc.6.1" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="15672"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="round_modulo'vc.7" expl="assertion" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="4597"/></proof>
</goal>
- <goal name="round_modulo'vc.7" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.01" steps="4049"/></proof>
+ <goal name="round_modulo'vc.8" expl="assertion" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="4635"/></proof>
</goal>
- <goal name="round_modulo'vc.8" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.87" steps="464410"/></proof>
+ <goal name="round_modulo'vc.9" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="4639"/></proof>
+ </goal>
+ <goal name="round_modulo'vc.10" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="37531"/></proof>
</goal>
</transf>
</goal>
<goal name="round_down_to'vc" expl="VC for round_down_to" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.0" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4118"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="4642"/></proof>
</goal>
<goal name="round_down_to'vc.1" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="5036"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="5592"/></proof>
</goal>
<goal name="round_down_to'vc.2" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="5036"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="5592"/></proof>
</goal>
<goal name="round_down_to'vc.3" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4899"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="5455"/></proof>
</goal>
<goal name="round_down_to'vc.4" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="9843"/></proof>
+ <proof prover="2"><result status="valid" time="0.23" steps="72038"/></proof>
</goal>
<goal name="round_down_to'vc.5" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="9745"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="17121"/></proof>
</goal>
<goal name="round_down_to'vc.6" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="11376"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="17317"/></proof>
</goal>
<goal name="round_down_to'vc.7" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4362"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="4886"/></proof>
</goal>
<goal name="round_down_to'vc.8" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.00" steps="4775"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="5299"/></proof>
</goal>
<goal name="round_down_to'vc.9" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.01" steps="4812"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="5336"/></proof>
</goal>
<goal name="round_down_to'vc.10" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="8343"/></proof>
+ <proof prover="2"><result status="valid" time="0.04" steps="8869"/></proof>
</goal>
<goal name="round_down_to'vc.11" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="8526"/></proof>
+ <proof prover="2"><result status="valid" time="0.04" steps="9052"/></proof>
</goal>
<goal name="round_down_to'vc.12" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.12.0" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="5249"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="5805"/></proof>
</goal>
<goal name="round_down_to'vc.12.1" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="5176"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="5732"/></proof>
</goal>
<goal name="round_down_to'vc.12.2" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="5122"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="5678"/></proof>
</goal>
<goal name="round_down_to'vc.12.3" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="11331"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="18490"/></proof>
</goal>
<goal name="round_down_to'vc.12.4" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.12.4.0" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="round_down_to'vc.12.4.0.0" expl="postcondition" proved="true">
- <proof prover="0" timelimit="10" memlimit="4000"><result status="valid" time="0.02" steps="27177"/></proof>
- <proof prover="1"><result status="valid" time="0.04" steps="72"/></proof>
- </goal>
- </transf>
+ <proof prover="0" timelimit="5"><result status="valid" time="0.02" steps="29698"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="round_down_to'vc.13" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="7644"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="8170"/></proof>
</goal>
<goal name="round_down_to'vc.14" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.14.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.14.0.0" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4285"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="4809"/></proof>
</goal>
<goal name="round_down_to'vc.14.0.1" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4279"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="4803"/></proof>
</goal>
<goal name="round_down_to'vc.14.0.2" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4285"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="4809"/></proof>
</goal>
<goal name="round_down_to'vc.14.0.3" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4292"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="4816"/></proof>
</goal>
<goal name="round_down_to'vc.14.0.4" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="25822"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="28336"/></proof>
</goal>
</transf>
</goal>
<goal name="round_down_to'vc.14.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.14.1.0" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="5415"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="5971"/></proof>
</goal>
<goal name="round_down_to'vc.14.1.1" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="5344"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="5900"/></proof>
</goal>
<goal name="round_down_to'vc.14.1.2" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="5214"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="5770"/></proof>
</goal>
<goal name="round_down_to'vc.14.1.3" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="9956"/></proof>
+ <proof prover="2"><result status="valid" time="0.23" steps="72151"/></proof>
</goal>
<goal name="round_down_to'vc.14.1.4" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.14.1.4.0" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="25935"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="28455"/></proof>
</goal>
</transf>
</goal>
@@ -157,25 +173,21 @@
<goal name="round_down_to'vc.15" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.15.0" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4388"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="4912"/></proof>
</goal>
<goal name="round_down_to'vc.15.1" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="4382"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="4906"/></proof>
</goal>
<goal name="round_down_to'vc.15.2" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4388"/></proof>
+ <proof prover="2"><result status="valid" time="0.04" steps="4912"/></proof>
</goal>
<goal name="round_down_to'vc.15.3" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4395"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="4919"/></proof>
</goal>
<goal name="round_down_to'vc.15.4" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="round_down_to'vc.15.4.0" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="round_down_to'vc.15.4.0.0" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.04" steps="82"/></proof>
- </goal>
- </transf>
+ <proof prover="1"><result status="valid" time="0.03" steps="82"/></proof>
</goal>
</transf>
</goal>
@@ -184,8 +196,414 @@
</transf>
</goal>
<goal name="round_up_to'vc" expl="VC for round_up_to" proved="true">
- <proof prover="0" obsolete="true"><result status="timeout" time="1.00" steps="9136696"/></proof>
- <proof prover="2"><result status="valid" time="0.06" steps="16599"/></proof>
+ <proof prover="2"><result status="valid" time="0.06" steps="17210"/></proof>
+ </goal>
+ <goal name="simple_mul_div'vc" expl="VC for simple_mul_div" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="5217"/></proof>
+ </goal>
+ <goal name="remove_product_right'vc" expl="VC for remove_product_right" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="20036"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc" expl="VC for divisible_to_z" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="divisible_to_z'vc.0" expl="assertion" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="divisible_to_z'vc.0.0" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.0.1" expl="VC for divisible_to_z" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.0.2" expl="VC for divisible_to_z" proved="true">
+ <proof prover="1"><result status="valid" time="0.05" steps="123"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.0.3" expl="VC for divisible_to_z" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="5054"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="divisible_to_z'vc.1" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.04" steps="18064"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.2" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="5040"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.3" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.4" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.5" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="20"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.6" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="22"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.7" expl="assertion" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="divisible_to_z'vc.7.0" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="divisible_to_z'vc.8" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="26"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.9" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="26"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.10" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.05" steps="92"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.11" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.12" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="5133"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.13" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="5136"/></proof>
+ </goal>
+ <goal name="divisible_to_z'vc.14" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="divisible_from_z'vc" expl="VC for divisible_from_z" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="divisible_from_z'vc.0" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.23" steps="96129"/></proof>
+ </goal>
+ <goal name="divisible_from_z'vc.1" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="24056"/></proof>
+ </goal>
+ <goal name="divisible_from_z'vc.2" expl="assertion" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="divisible_from_z'vc.2.0" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="18"/></proof>
+ </goal>
+ <goal name="divisible_from_z'vc.2.1" expl="VC for divisible_from_z" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="20"/></proof>
+ </goal>
+ <goal name="divisible_from_z'vc.2.2" expl="VC for divisible_from_z" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="20"/></proof>
+ </goal>
+ <goal name="divisible_from_z'vc.2.3" expl="VC for divisible_from_z" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="divisible_from_z'vc.2.4" expl="VC for divisible_from_z" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="divisible_from_z'vc.2.5" expl="VC for divisible_from_z" proved="true">
+ <proof prover="1"><result status="valid" time="1.32" steps="192"/></proof>
+ </goal>
+ <goal name="divisible_from_z'vc.2.6" expl="VC for divisible_from_z" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="divisible_from_z'vc.3" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="23904"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="divisible'vc" expl="VC for divisible" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="divisible'vc.0" expl="witness existence" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+ </goal>
+ <goal name="divisible'vc.1" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="22"/></proof>
+ </goal>
+ <goal name="divisible'vc.2" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="22"/></proof>
+ </goal>
+ <goal name="divisible'vc.3" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="22"/></proof>
+ </goal>
+ <goal name="divisible'vc.4" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="22"/></proof>
+ </goal>
+ <goal name="divisible'vc.5" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="30"/></proof>
+ </goal>
+ <goal name="divisible'vc.6" expl="unreachable point" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="30"/></proof>
+ </goal>
+ <goal name="divisible'vc.7" expl="witness existence" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="7075"/></proof>
+ </goal>
+ <goal name="divisible'vc.8" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="6266"/></proof>
+ </goal>
+ <goal name="divisible'vc.9" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="6269"/></proof>
+ </goal>
+ <goal name="divisible'vc.10" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="6270"/></proof>
+ </goal>
+ <goal name="divisible'vc.11" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="6275"/></proof>
+ </goal>
+ <goal name="divisible'vc.12" expl="assertion" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="6322"/></proof>
+ </goal>
+ <goal name="divisible'vc.13" expl="unreachable point" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="7136"/></proof>
+ </goal>
+ <goal name="divisible'vc.14" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="divisible'vc.14.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="divisible'vc.14.0.0" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="6361"/></proof>
+ </goal>
+ <goal name="divisible'vc.14.0.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="divisible'vc.14.1" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="7127"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="divisible'vc.15" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="24"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="mult_cst_divisible'vc" expl="VC for mult_cst_divisible" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="mult_cst_divisible'vc.0" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
+ </goal>
+ <goal name="mult_cst_divisible'vc.1" expl="witness existence" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="160"/></proof>
+ </goal>
+ <goal name="mult_cst_divisible'vc.2" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="30"/></proof>
+ </goal>
+ <goal name="mult_cst_divisible'vc.3" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="103"/></proof>
+ </goal>
+ <goal name="mult_cst_divisible'vc.4" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="mult_cst_divisible'vc.5" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="23"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="union_divisible'vc" expl="VC for union_divisible" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="union_divisible'vc.0" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.29" steps="101388"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.1" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.45" steps="144831"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.2" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.3" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="30"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.4" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="32"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.5" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="71"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.6" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="36"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.7" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="7017"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.8" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="36"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.9" expl="witness existence" proved="true">
+ <proof prover="1"><result status="valid" time="0.08" steps="95"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.10" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="48"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.11" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="7103"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.12" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="7104"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.13" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="7109"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.14" expl="assertion" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="7156"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.15" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="56"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.16" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="56"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.17" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="58"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.18" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="7204"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.19" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="58"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.20" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="58"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.21" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="59"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.22" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="60"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.23" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="8803"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.24" expl="witness existence" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="95"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.25" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.26" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.27" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.28" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.29" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="54"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.30" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="56"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.31" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="56"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.32" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="58"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.33" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="58"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.34" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="58"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.35" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="58"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.36" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="59"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.37" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="60"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.38" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.19" steps="152"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.39" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="8073"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.40" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="8394"/></proof>
+ </goal>
+ <goal name="union_divisible'vc.41" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="51"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter_divisible'vc" expl="VC for inter_divisible" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter_divisible'vc.0" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="58"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.1" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="60"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.2" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.3" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="32786"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.4" expl="witness existence" proved="true">
+ <proof prover="1"><result status="valid" time="0.04" steps="92"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.5" expl="witness existence" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="104"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.6" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="42"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.7" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="42"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="7071"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.8" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="42"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="7081"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.9" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="42"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="7089"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.10" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="48"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="7124"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.11" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="48"/></proof>
+ <proof prover="2"><result status="valid" time="0.04" steps="7127"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.12" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="7137"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.13" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="48"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="7145"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.14" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="54"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="7172"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.15" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="54"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.16" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="56"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.17" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="58"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.18" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="8811"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.19" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="34"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="7891"/></proof>
+ </goal>
+ <goal name="inter_divisible'vc.20" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="43"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="8228"/></proof>
+ </goal>
+ </transf>
</goal>
</theory>
</file>
diff --git a/src_common/modulo__Divisible.ml b/src_common/modulo__Divisible.ml
new file mode 100644
index 0000000000000000000000000000000000000000..55b55551601c15fba14444f668212913bff046d1
--- /dev/null
+++ b/src_common/modulo__Divisible.ml
@@ -0,0 +1,36 @@
+exception FinitePositiveExpected
+
+let round_down_to (a: Q.t) (m: Q.t) : Q.t =
+ begin match Q.classify m with
+ | (Q.ZERO | (Q.MINF | (Q.INF | Q.UNDEF))) -> raise FinitePositiveExpected
+ | Q.NZERO ->
+ if (Q.(<=) m (Q.of_bigint Z.zero)) then raise FinitePositiveExpected
+ end;
+ match Q.classify a with
+ | (Q.MINF | (Q.INF | (Q.UNDEF | Q.ZERO))) -> a
+ | Q.NZERO -> (Q.( * ) (Q.of_bigint (Q__Q.floor (Q.(/) a m))) m)
+
+let round_up_to (a: Q.t) (m: Q.t) : Q.t =
+ let res = round_down_to (Q.(-) (Q.of_bigint Z.zero) a) m in
+ (Q.(-) (Q.of_bigint Z.zero) res)
+
+let divisible (a: Q.t) (b: Q.t) : bool =
+ let b1 =
+ (Z.divisible (a.Q.num) (b.Q.num)) in
+ if b1
+ then
+ let b2 = (Z.divisible (b.Q.den) (a.Q.den)) in if b2 then true else false
+ else false
+
+let mult_cst_divisible (a: Q.t) (q: Q.t) : Q.t = (Q.( * ) a q)
+
+let union_divisible (a: Q.t) (b: Q.t) : Q.t =
+ let n =
+ (Z.gcd (a.Q.num) (b.Q.num)) in
+ let d = (Z.lcm (a.Q.den) (b.Q.den)) in ({ Q.num = n; Q.den = d })
+
+let inter_divisible (a: Q.t) (b: Q.t) : Q.t =
+ let n1 =
+ (Z.gcd (a.Q.den) (b.Q.den)) in
+ let d1 = (Z.lcm (a.Q.num) (b.Q.num)) in ({ Q.num = d1; Q.den = n1 })
+
diff --git a/src_common/modulo__Modulo.ml b/src_common/modulo__Modulo.ml
deleted file mode 100644
index 89741aa2a877cd54d69f861879f22d156b1b8959..0000000000000000000000000000000000000000
--- a/src_common/modulo__Modulo.ml
+++ /dev/null
@@ -1,18 +0,0 @@
-exception ModuloFinitePositiveExpected
-
-let round_down_to (a: Q.t) (m: Q.t) : Q.t =
- begin match Q.classify m with
- | (Q.ZERO | (Q.MINF | (Q.INF | Q.UNDEF))) ->
- raise ModuloFinitePositiveExpected
- | Q.NZERO ->
- if (Q.(<=) m (Q.of_bigint Z.zero))
- then raise ModuloFinitePositiveExpected
- end;
- match Q.classify a with
- | (Q.MINF | (Q.INF | (Q.UNDEF | Q.ZERO))) -> a
- | Q.NZERO -> (Q.( * ) (Q.of_bigint (Q__Q.floor (Q.(/) a m))) m)
-
-let round_up_to (a: Q.t) (m: Q.t) : Q.t =
- let res = round_down_to (Q.(-) (Q.of_bigint Z.zero) a) m in
- (Q.(-) (Q.of_bigint Z.zero) res)
-
diff --git a/src_common/q.mlw b/src_common/q.mlw
index 0f66682a820f4702e7d77aea227bc9c35c5d6397..c19c1afba43bb732e515166800c60d4ed73c86e8 100644
--- a/src_common/q.mlw
+++ b/src_common/q.mlw
@@ -10,6 +10,55 @@ module Z
requires { 0 < b }
ensures { 0 <= d*b - a < b }
+ predicate ddivisible_using (a:int) (b:int) (c:int) =
+ a = c * b
+
+ predicate ddivisible (a:int) (b:int) =
+ exists d. ddivisible_using a b d
+
+ val divisible (a:int) (b:int) : (r:bool,ghost d: int)
+ ensures { (not r) -> forall c. not (ddivisible_using a b c) }
+ ensures { r -> ddivisible_using a b d }
+
+ function gcd (a b:int): int
+
+ val gcd (a b:int) : (c:int,ghost a':int,ghost b':int)
+ ensures { gcd a b = c }
+ ensures { c * a' = a }
+ ensures { c * b' = b }
+ ensures { forall r d. ddivisible_using r a d -> ddivisible_using r c (d*a')}
+ ensures { forall r d. ddivisible_using r b d -> ddivisible_using r c (d*b')}
+ ensures { forall r da db. ddivisible_using a r da -> ddivisible_using b r db
+ -> ddivisible_using c r (da*a')}
+
+ function lcm (a b:int): int
+
+ val lcm (a b:int) : (c:int, ghost a':int, ghost b':int, ghost fa : int -> int)
+ requires { a <> 0 } requires { b <> 0 }
+ ensures { c <> 0 } ensures { lcm a b = c }
+ ensures { c = a' * a } ensures { c = b' * b }
+ ensures { forall r da db. ddivisible_using r a da -> ddivisible_using r b db ->
+ (da = a' * fa da /\ ddivisible_using r c (fa da)) }
+ ensures { forall r da. ddivisible_using a r da -> ddivisible_using c r (da*a') }
+ ensures { forall r db. ddivisible_using a r db -> ddivisible_using c r (db*b') }
+
+
+ predicate prime_to_one_another (a b:int) (* = (gcd a b = 1) *)
+
+ val ghost prime_to_one_another_mul (a m b n: int) : (q:int)
+ requires { prime_to_one_another a b }
+ requires { a * m = b * n } (* a * b * q = b * a * q *)
+ ensures { ddivisible_using m b q (* m = b * q *) }
+ ensures { ddivisible_using n a q (* n = a * q *) }
+
+ axiom GCD1: forall a b c. prime_to_one_another a b -> prime_to_one_another (gcd a c) b
+ axiom GCD2: forall a b c. prime_to_one_another a b -> prime_to_one_another a (gcd b c)
+ axiom GCD3: forall a b c. prime_to_one_another a b -> prime_to_one_another a c
+ -> prime_to_one_another a (lcm b c)
+ axiom GCD4: forall a b c. prime_to_one_another a b -> prime_to_one_another c b
+ -> prime_to_one_another (lcm a c) b
+ axiom GCD_comm: forall a b. gcd a b = gcd b a
+
end
module Q
@@ -17,6 +66,7 @@ module Q
use real.RealInfix
use int.Int
use real.FromInt
+ use Z as Z
type value =
| MinusInf
@@ -30,10 +80,20 @@ module Q
ghost value: value;
}
invariant { value = Real -> 0 < den }
+ invariant { value = Real -> Z.prime_to_one_another num den }
predicate is_real (q:t) =
q.value = Real
+ predicate is_minus_inf (q:t) =
+ q.value = MinusInf
+
+ predicate is_plus_inf (q:t) =
+ q.value = PlusInf
+
+ predicate is_nan (q:t) =
+ q.value = NaN
+
predicate not_NaN (q:t) = q.value <> NaN
function real (q:t) : real
@@ -55,11 +115,14 @@ module Q
end
}
+ predicate equal (a b:t) =
+ if a.is_real /\ b.is_real then a.real = b.real else a.value = b.value
+
val (=) (a:t) (b:t) : bool
- ensures { not a.is_real -> not b.is_real -> result = (a.value = b.value) }
- ensures { a.is_real -> b.is_real -> result = (a.real = b.real) }
+ ensures { equal a b = result }
function (<=) (a:t) (b:t) : bool
+ function (<) (a:t) (b:t) : bool = a <= b /\ not (equal a b)
axiom le_def: forall a b. a.is_real -> b.is_real -> ((a <= b) <-> (a.real <=. b.real))
axiom le_def_full: forall a b [a <= b].
@@ -74,6 +137,11 @@ module Q
| PlusInf, _ -> not (a <= b)
end
+ (* lemma le_anti_refl: forall a b. a <= b -> b <= a -> equal a b *)
+ (* lemma le_trans: forall a b c. a <= b -> b <= c -> a <= c *)
+ (* lemma le_lt_trans: forall a b c. a <= b -> b < c -> a < c *)
+ (* lemma lt_le_trans: forall a b c. a < b -> b <= c -> a < c *)
+
val (<=) (a:t) (b:t) : bool
requires { not_NaN a /\ not_NaN b }
ensures { result = (a <= b) }
@@ -120,8 +188,8 @@ module Q
| MinusInf, MinusInf | PlusInf, PlusInf -> result.value = PlusInf
end
}
- ensures { is_real a -> is_real b -> b.real <> 0. -> is_real result }
- ensures { is_real a -> is_real b -> b.real <> 0. -> a.real *. b.real = result.real }
+ ensures { is_real a -> is_real b -> is_real result }
+ ensures { is_real a -> is_real b -> a.real *. b.real = result.real }
val (/) (a b:t) : t
requires { not_NaN a /\ not_NaN b }
@@ -142,7 +210,16 @@ module Q
ensures { is_real a -> is_real b -> b.real <> 0. -> is_real result }
ensures { is_real a -> is_real b -> b.real <> 0. -> a.real /. b.real = result.real }
+ val make (num den: int): t
+ requires { den <> 0 }
+ ensures { result.is_real }
+ ensures { result.real = (from_int num) /. (from_int den) }
+ val make_exact (num den: int): t
+ requires { den <> 0 } requires { Z.prime_to_one_another num den }
+ ensures { result.is_real }
+ ensures { result.num = num }
+ ensures { result.den = den }
use real.Truncate
@@ -154,17 +231,30 @@ module Q
ensures { is_real result }
ensures { result.real = from_int a }
- use Z
-
let floor (a:t) : int
requires { is_real a }
ensures { result = floor a.real } =
- fdiv a.num a.den
+ assert { from_int (floor a.real) <=. a.real <. from_int (floor a.real) +. 1. };
+ assert { 0. <=. a.real -. from_int (floor a.real) <. 1. };
+ let r = Z.fdiv a.num a.den in
+ assert { Int.(0 <= a.num - r*a.den < a.den) };
+ assert { 0. <=. (from_int a.num) -. (from_int r)*.(from_int a.den) <. (from_int a.den) };
+ assert { ((from_int a.num) -. (from_int r)*.(from_int a.den))/.(from_int a.den) <. (from_int a.den)/.(from_int a.den) };
+ assert { 0. <=. a.real -. from_int r <. 1. };
+ r
+
let ceil (a:t) : int
requires { is_real a }
ensures { result = ceil a.real } =
- cdiv a.num a.den
+ assert { from_int (ceil a.real) -. 1. <. a.real <=. from_int (ceil a.real) };
+ assert { 0. <=. from_int (ceil a.real) -. a.real <. 1. };
+ let r = Z.cdiv a.num a.den in
+ assert { Int.(0 <= r*a.den - a.num < a.den) };
+ assert { 0. <=. (from_int r)*.(from_int a.den) -. (from_int a.num) <. (from_int a.den) };
+ assert { ((from_int r)*.(from_int a.den) -. (from_int a.num))/.(from_int a.den) <. (from_int a.den)/.(from_int a.den) };
+ assert { 0. <=. from_int r -. a.real <. 1. };
+ r
end
diff --git a/src_common/q/why3session.xml b/src_common/q/why3session.xml
index 108fcf269299912bee56c712ec85df578e20b137..6d000bfc6c449ef54d6b015aad1395359057ae71 100644
--- a/src_common/q/why3session.xml
+++ b/src_common/q/why3session.xml
@@ -3,29 +3,74 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="CVC4" version="1.7" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="2" name="Alt-Ergo" version="2.3.3" timelimit="5" steplimit="0" memlimit="1000"/>
<file format="whyml" proved="true">
<path name=".."/><path name="q.mlw"/>
<theory name="Q" proved="true">
<goal name="t'vc" expl="VC for t" proved="true">
- <proof prover="0"><result status="valid" time="0.04" steps="1502"/></proof>
+ <proof prover="0"><result status="valid" time="0.04" steps="17812"/></proof>
</goal>
<goal name="floor'vc" expl="VC for floor" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="floor'vc.0" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.04" steps="7201"/></proof>
+ <goal name="floor'vc.0" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="4863"/></proof>
</goal>
- <goal name="floor'vc.1" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.41" steps="191862"/></proof>
+ <goal name="floor'vc.1" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="4386"/></proof>
+ </goal>
+ <goal name="floor'vc.2" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.15" steps="51614"/></proof>
+ </goal>
+ <goal name="floor'vc.3" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="4450"/></proof>
+ </goal>
+ <goal name="floor'vc.4" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="4501"/></proof>
+ </goal>
+ <goal name="floor'vc.5" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="19745"/></proof>
+ </goal>
+ <goal name="floor'vc.6" expl="assertion" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="floor'vc.6.0" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.06" steps="231992"/></proof>
+ </goal>
+ <goal name="floor'vc.6.1" expl="assertion" proved="true">
+ <proof prover="2"><result status="valid" time="0.14" steps="372"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="floor'vc.7" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.76" steps="707"/></proof>
</goal>
</transf>
</goal>
<goal name="ceil'vc" expl="VC for ceil" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="ceil'vc.0" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.07" steps="7201"/></proof>
+ <goal name="ceil'vc.0" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="4880"/></proof>
+ </goal>
+ <goal name="ceil'vc.1" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="4396"/></proof>
+ </goal>
+ <goal name="ceil'vc.2" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.07" steps="51628"/></proof>
+ </goal>
+ <goal name="ceil'vc.3" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="4492"/></proof>
+ </goal>
+ <goal name="ceil'vc.4" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="4543"/></proof>
+ </goal>
+ <goal name="ceil'vc.5" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="19673"/></proof>
+ </goal>
+ <goal name="ceil'vc.6" expl="assertion" proved="true">
+ <proof prover="2"><result status="valid" time="0.15" steps="512"/></proof>
</goal>
- <goal name="ceil'vc.1" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.57" steps="203328"/></proof>
+ <goal name="ceil'vc.7" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="5645"/></proof>
</goal>
</transf>
</goal>
diff --git a/src_common/q__Q.ml b/src_common/q__Q.ml
index 2a88cf5ba0a15a4b496a6b38c0f6820e5ffac93c..f134cf4a7a4d473d0e1c05228d71a474f1161575 100644
--- a/src_common/q__Q.ml
+++ b/src_common/q__Q.ml
@@ -4,11 +4,6 @@ type value =
| NaN
| Real
-type t = {
- num: Z.t;
- den: Z.t;
- }
-
type kind =
| ZERO
| NZERO
@@ -16,7 +11,7 @@ type kind =
| MINF
| UNDEF
-let floor (a: Q.t) : Z.t = (Z.fdiv (a.num) (a.den))
+let floor (a: Q.t) : Z.t = (Z.fdiv (a.Q.num) (a.Q.den))
-let ceil (a: Q.t) : Z.t = (Z.cdiv (a.num) (a.den))
+let ceil (a: Q.t) : Z.t = (Z.cdiv (a.Q.num) (a.Q.den))