diff --git a/src_colibri2/stdlib/std.ml b/src_colibri2/stdlib/std.ml
index b61fc8fc9469ab3f7104f3b45dc8f96d056c3bbe..8fc5cbdaf816b0a54da9d3d977f5a15537650b34 100644
--- a/src_colibri2/stdlib/std.ml
+++ b/src_colibri2/stdlib/std.ml
@@ -101,7 +101,7 @@ module Q = struct
let is_integer q = Z.equal Z.one q.Q.den
- let floor x = Q.of_bigint (Colibrics_lib.Q.floor x)
- let ceil x = Q.of_bigint (Colibrics_lib.Q.ceil x)
+ let floor x = Q.of_bigint (Colibrics_lib.QUtils.floor x)
+ let ceil x = Q.of_bigint (Colibrics_lib.QUtils.ceil x)
end
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index 4df100dd5dd40ffcdd5a706ff243c06038e9165d..28201477d874b8ae4c48cb8b8ac0c0f514baa0cc 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -38,7 +38,7 @@ let cst' c = RealValue.index ~basename:(Format.asprintf "%aR" Q.pp c) c
let cst c = RealValue.node (cst' c)
let debug_todo = debug
-type bound = Interval_sig.bound = Strict | Large
+type bound = Colibrics_lib.Interval.Bound.t = Strict | Large
[@@deriving eq,ord,show]
module S = struct
module T = struct
@@ -59,7 +59,7 @@ module S = struct
then Format.fprintf fmt "%a - %a" pp (q1,cl1) Node.pp cl2
else Format.fprintf fmt "%a + %a" pp (q1,cl1) pp (q2,cl2)
| GZero (node,b) ->
- Format.fprintf fmt "0 %a %a" Interval.pp_bound b Node.pp node
+ Format.fprintf fmt "0 %a %a" Interval.Bound.pp b Node.pp node
let hash = function
| Add (q1,cl1,q2,cl2) ->
@@ -444,10 +444,10 @@ module ChoLRA = struct
let choose_decision node env =
let v = Opt.get_def D.reals (Egraph.get_dom env dom node) in
match D.split_heuristic v with
- | `Singleton _ -> Egraph.DecNo
- | `Splitted (v1,v2) ->
+ | Singleton _ -> Egraph.DecNo
+ | Splitted (v1,v2) ->
DecTodo (List.map (make_decision node) (Shuffle.shufflel [v1;v2]))
- | `NotSplitted ->
+ | NotSplitted ->
DecTodo [make_decision node (D.singleton (D.choose v))]
let choice n = {
diff --git a/src_colibri2/theories/LRA/interval.ml b/src_colibri2/theories/LRA/interval.ml
index 699636932696478e1f020a9d8abbb352004634c0..a48123e6e8f36ba331f7bc24ffd52e9f1a8f3ddd 100644
--- a/src_colibri2/theories/LRA/interval.ml
+++ b/src_colibri2/theories/LRA/interval.ml
@@ -21,77 +21,66 @@
open Colibri2_popop_lib
open Colibri2_stdlib.Std
-type bound = Interval_sig.bound = Strict | Large [@@deriving eq]
+module Bound = struct
+ type t = Colibrics_lib.Interval.Bound.t =
+ | Strict | Large [@@deriving eq, ord, hash]
-let pp_bound fmt = function
- | Strict -> Format.string fmt "<"
- | Large -> Format.string fmt "≤"
+ let pp fmt = function
+ | Strict -> Format.string fmt "<"
+ | Large -> Format.string fmt "≤"
-let compare_inf b1 b2 = match b1,b2 with
- | Large, Strict -> -1
- | Strict, Large -> 1
- | Large, Large | Strict, Strict -> 0
+ 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_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)
+ let compare_sup b1 b2 = - (compare_inf b1 b2)
-let compare_bounds_inf = Ord.pair Q.compare compare_inf
-let compare_bounds_sup = Ord.pair Q.compare compare_sup
-let compare_bounds_inf_sup = Ord.pair Q.compare compare_inf_sup
+ let compare_bounds_inf = Ord.pair Q.compare compare_inf
+ let compare_bounds_sup = Ord.pair Q.compare compare_sup
+ let compare_bounds_inf_sup = Ord.pair Q.compare compare_inf_sup
+
+end
module Convexe = struct
- type t = { minb : bound; minv: Q.t; maxv: Q.t; maxb: bound }
+ include Colibrics_lib.Interval.Convexe
+
+ include (struct
+ type t = Colibrics_lib.Interval.Convexe.t = private
+ | Finite of Q.t * Bound.t * Q.t * Bound.t
+ | InfFinite of Q.t * Bound.t
+ | FiniteInf of Q.t * Bound.t
+ | Inf
+ [@@ deriving eq, ord, hash]
+ end)
let pp fmt t =
let print_bound_left fmt = function
- | Large -> Format.fprintf fmt "["
+ | Bound.Large -> Format.fprintf fmt "["
| Strict -> Format.fprintf fmt "]" in
let print_bound_right fmt = function
- | Large -> Format.fprintf fmt "]"
+ | Bound.Large -> Format.fprintf fmt "]"
| Strict -> Format.fprintf fmt "[" in
- match t.minb, t.maxb with
- | Large, Large when Q.equal t.minv t.maxv
- -> Format.fprintf fmt "{%a}" Q.pp t.minv
- | _
- -> Format.fprintf fmt "%a%a;%a%a"
- print_bound_left t.minb
- Q.pp t.minv
- Q.pp t.maxv
- print_bound_right t.maxb
-
- let compare e1 e2 =
- let compare_bound b1 b2 = match b1, b2 with
- | Strict, Large -> 1
- | Large, Strict -> -1
- | _ -> 0
- in
- let c = Q.compare e1.minv e2.minv in
- if c = 0 then c else
- let c = compare_bound e1.minb e2.minb in
- if c = 0 then c else
- let c = Q.compare e1.maxv e2.maxv in
- if c = 0 then c else
- let c = compare_bound e1.maxb e2.maxb in
- c
-
- let equal e1 e2 =
- Equal.physical e1.minb e2.minb && Equal.physical e1.maxb e2.maxb &&
- Q.equal e1.minv e2.minv && Q.equal e1.maxv e2.maxv
-
- let hash e =
- let hash_bound = function
- | Large -> 1
- | Strict -> 3 in
- Hashcons.combine3
- (hash_bound e.minb) (hash_bound e.maxb)
- (Hashtbl.hash e.minv) (Hashtbl.hash e.maxv)
-
+ match t with
+ | Finite (q1,b1,q2,b2) ->
+ Format.fprintf fmt "%a%a;%a%a"
+ print_bound_left b1 Q.pp q1
+ Q.pp q2 print_bound_right b2
+ | InfFinite (q1,b1) ->
+ Format.fprintf fmt "]-∞;%a%a"
+ Q.pp q1 print_bound_right b1
+ | FiniteInf(q1,b1) ->
+ Format.fprintf fmt "%a%a;+∞["
+ print_bound_left b1 Q.pp q1
+ | Inf ->
+ Format.fprintf fmt "]-∞;+∞["
include Popop_stdlib.MkDatatype(struct
type nonrec t = t
@@ -99,259 +88,57 @@ module Convexe = struct
let hash = hash let pp = pp
end)
- let invariant e =
- not (Q.equal e.minv Q.inf) &&
- not (Q.equal e.maxv Q.minus_inf) &&
- let c = Q.compare e.minv e.maxv in
- if c = 0
- then equal_bound e.minb Large && equal_bound e.maxb Large
- else c < 0
-
- let is_singleton = function
- | {minv;maxv} when Q.equal minv maxv -> Some minv
- | _ -> None
-
- let singleton q =
- let t = {minb=Large; minv = q; maxv = q; maxb= Large} in
- assert (invariant t);
- t
-
- 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
+ let invariant _ = true (* proved in why3 *)
+
+ (* 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
-
+(*
module ConvexeWithDivider = struct
(** modulo = 0 -> no modulo *)
@@ -401,11 +188,12 @@ module ConvexeWithDivider = struct
end
in
let minb,minv =
- round ~add:Q.add ~divisible_up_to:Colibrics_lib.Q.divisible_up_to
+ round ~add:Q.add
+ ~divisible_up_to:Colibrics_lib.QUtils.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
+ round ~add:Q.sub ~divisible_up_to:Colibrics_lib.QUtils.divisible_down_to
~minus_inf:Q.inf ~minv:e.c.Convexe.maxv ~minb:e.c.Convexe.maxb
in
if Q.lt maxv minv
@@ -433,7 +221,7 @@ module ConvexeWithDivider = struct
let divisible q d =
Q.equal d Q.zero ||
- Colibrics_lib.Q.divisible q d
+ Colibrics_lib.QUtils.divisible q d
let is_included e1 e2 =
Convexe.is_included e1.c e2.c &&
@@ -451,21 +239,21 @@ module ConvexeWithDivider = struct
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) }
+ divider = Q.abs (Colibrics_lib.QUtils.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
+ let divider = Colibrics_lib.QUtils.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 }
+ divider = Colibrics_lib.QUtils.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 }
+ divider = Colibrics_lib.QUtils.union_divisible e1.divider e2.divider }
let div_unknown c = { c; divider = Q.zero }
@@ -479,14 +267,14 @@ module ConvexeWithDivider = struct
let union e1 e2 =
{ c = Convexe.union e1.c e2.c;
- divider = Colibrics_lib.Q.union_divisible e1.divider e2.divider }
+ divider = Colibrics_lib.QUtils.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 }
+ { c; divider = Colibrics_lib.QUtils.inter_divisible e1.divider e2.divider }
(** intersection set.
if the two arguments are equals, return the second
@@ -502,7 +290,7 @@ module ConvexeWithDivider = struct
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
+ else Colibrics_lib.QUtils.divisible_down_to q e.divider
let split_heuristic e =
let rec aux divider c =
@@ -1206,3 +994,4 @@ module ConvexeInfo (Info: sig
mk e.minv e.minb, mk e.maxv e.maxb
end
+*)
diff --git a/src_colibri2/theories/LRA/interval.mli b/src_colibri2/theories/LRA/interval.mli
index ee38207b26145960a4a505254aea026e117eb67e..92d6acbc9d22a7c07d1d57056c86d21c80d06064 100644
--- a/src_colibri2/theories/LRA/interval.mli
+++ b/src_colibri2/theories/LRA/interval.mli
@@ -18,26 +18,30 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-open Colibri2_popop_lib
+module Bound : sig
+ type t = Colibrics_lib.Interval.Bound.t =
+ | Strict | Large
+ [@@deriving eq, ord, hash]
-type bound = Interval_sig.bound = Strict | Large
+ val pp: t Format.printer
-val pp_bound: bound Format.printer
-
-val compare_bounds_inf: Q.t * bound -> Q.t * bound -> int
-val compare_bounds_sup: Q.t * bound -> Q.t * bound -> int
-val compare_bounds_inf_sup: Q.t * bound -> Q.t * bound -> int
+ val compare_bounds_inf: Q.t * t -> Q.t * t -> int
+ val compare_bounds_sup: Q.t * t -> Q.t * t -> int
+ val compare_bounds_inf_sup: Q.t * t -> Q.t * t -> int
+end
module Convexe: sig
include Interval_sig.S
- val split_heuristic: t ->
- [ `Singleton of Q.t
- | `Splitted of t * t
- | `NotSplitted ]
- val inter_with_integer: t -> t option
-end
+ type split_heuristic =
+ | Singleton of Q.t
+ | Splitted of t * t
+ | NotSplitted
+ val split_heuristic: t -> split_heuristic
+
+end
+(*
module ConvexeWithDivider: sig
include Interval_sig.S
val split_heuristic: t ->
@@ -111,3 +115,4 @@ module ConvexeInfo(Info: sig
val get_convexe_hull: t -> (Q.t * bound) option * (Q.t * bound) option
end
+*)
diff --git a/src_colibri2/theories/LRA/interval_sig.ml b/src_colibri2/theories/LRA/interval_sig.ml
index 0b16c1049e5ccd959cc6bef6fecde2ba6eb27a7e..741b47a969d492ccecff27c4270dc74f9e58b211 100644
--- a/src_colibri2/theories/LRA/interval_sig.ml
+++ b/src_colibri2/theories/LRA/interval_sig.ml
@@ -20,58 +20,19 @@
open Colibri2_popop_lib
-type bound = Strict | Large
+type bound = Colibrics_lib.Interval.Bound.t
module type S = sig
include Popop_stdlib.Datatype
- val invariant: t -> bool
-
- val is_distinct: t -> t -> bool
- val is_comparable: t -> t -> [`Uncomparable | `Lt | `Gt]
- val is_included: t -> t -> bool
-
- val mult_cst: Q.t -> t -> t
- val add_cst : Q.t -> t -> t
- val add: t -> t -> t
- val minus: t -> t -> t
-
- val mem: Q.t -> t -> bool
-
- (** from Q.t *)
- val singleton: Q.t -> t
- val is_singleton: t -> Q.t option
-
- val except: t -> Q.t -> t option
-
- val gt: Q.t -> t
- val ge: Q.t -> t
- val lt: Q.t -> t
- val le: Q.t -> t
- (** > q, >= q, < q, <= q *)
+ include (Colibrics_lib.Interval.S with type t := t)
- val union: t -> t -> t
- (** union set *)
-
- val inter: t -> t -> t option
- (** intersection set.
- if the two arguments are equals, return the second
- *)
-
-
- val zero: t
- val reals: t
- (** R *)
- val is_reals: t -> bool
-
- val choose: t -> Q.t
- (** Nothing smart in this choosing *)
-
-
- val choose_rnd : (int -> int) -> t -> Q.t
- (** choose an element randomly (but non-uniformly), the given function is
- the random generator *)
+ val invariant: t -> bool
- val get_convexe_hull: t -> (Q.t * bound) option * (Q.t * bound) option
+ (* val choose_rnd : (int -> int) -> t -> Q.t
+ * (\** choose an element randomly (but non-uniformly), the given function is
+ * the random generator *\)
+ *
+ * val get_convexe_hull: t -> (Q.t * bound) option * (Q.t * bound) option *)
end
diff --git a/src_common/colibrics_lib.ml b/src_common/colibrics_lib.ml
index cec78e906cb51c9f31ffd397873a48c314f2d458..494a4d71bf4ea76b3b09a1be3761e9476cf90405 100644
--- a/src_common/colibrics_lib.ml
+++ b/src_common/colibrics_lib.ml
@@ -1,4 +1,4 @@
-module Q = struct
+module QUtils = struct
(** Add some useful function to Q of zarith *)
let floor = Q__Q.floor
@@ -31,3 +31,75 @@ module Q = struct
else Modulo__Divisible.inter_divisible a b
end
+
+module Interval = struct
+ module Bound = Interval__Bound
+ module type S = sig
+ type t
+
+ val is_distinct: t -> t -> bool
+ type is_comparable =
+ | Gt
+ | Lt
+ | Ge
+ | Le
+ | Uncomparable
+
+ val is_comparable: t -> t -> is_comparable
+ val is_included: t -> t -> bool
+
+ val mult_cst: Q.t -> t -> t
+ val add_cst : Q.t -> t -> t
+ val add: t -> t -> t
+ val minus: t -> t -> t
+
+ val mem: Q.t -> t -> bool
+
+ (** from Q.t *)
+ val singleton: Q.t -> t
+ val is_singleton: t -> Q.t option
+
+ val except: t -> Q.t -> t option
+
+ val gt: Q.t -> t
+ val ge: Q.t -> t
+ val lt: Q.t -> t
+ val le: Q.t -> t
+ (** > q, >= q, < q, <= q *)
+
+ val union: t -> t -> t
+ (** union set *)
+
+ val inter: t -> t -> t option
+ (** intersection set.
+ if the two arguments are equals, return the second
+ *)
+
+
+ val zero: t
+ val reals: t
+ (** R *)
+ val is_reals: t -> bool
+
+ val choose: t -> Q.t
+ (** Nothing smart in this choosing *)
+
+ end
+ module Convexe : sig
+ type t = private
+ | Finite of Q.t * Bound.t * Q.t * Bound.t
+ | InfFinite of Q.t * Bound.t
+ | FiniteInf of Q.t * Bound.t
+ | Inf
+ include (S with type t := t )
+
+ type split_heuristic =
+ | Singleton of Q.t
+ | Splitted of t * t
+ | NotSplitted
+
+ val split_heuristic: t -> split_heuristic
+
+ end = Interval__Convexe
+
+end
diff --git a/src_common/common.drv b/src_common/common.drv
index b52a71c5b40ac595fc151a2e65fa3e52f38f2e6c..784a059be51a5cd873b54883d8eabf53adbacf6b 100644
--- a/src_common/common.drv
+++ b/src_common/common.drv
@@ -1,3 +1,9 @@
+module q.Ord
+ syntax val Eq "Ord.Eq"
+ syntax val Lt "Ord.Lt"
+ syntax val Gt "Ord.Gt"
+end
+
module q.Q
syntax type t "Q.t"
@@ -5,6 +11,27 @@ module q.Q
syntax val num "%1.Q.num"
syntax val den "%1.Q.den"
+ syntax val (<=) "Q.(<=) %1 %2"
+ syntax val (<) "Q.(<) %1 %2"
+ syntax val (+) "Q.(+) %1 %2"
+ syntax val (-) "Q.(-) %1 %2"
+ syntax val (/) "Q.(/) %1 %2"
+ syntax val (*) "Q.( * ) %1 %2"
+ 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 }"
+ syntax val compare "Q_extra.compare %1 %2"
+end
+
+module q.QWithInf
+
+ 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"
diff --git a/src_common/dune b/src_common/dune
index 7a405b4363708a17aca65ed1dfc19dfee558e13b..36f99d7146feeae3b359b5fbbd655db0c5925093 100644
--- a/src_common/dune
+++ b/src_common/dune
@@ -2,12 +2,28 @@
(public_name colibrics.lib)
(name colibrics_lib)
(libraries zarith)
+ (flags -w -27)
)
(rule
- (targets modulo__Divisible.ml q__Q.ml)
+ (targets q__Q.ml)
+ (deps q.mlw)
+ (action (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L . q.Q))
+ (mode promote)
+)
+
+
+(rule
+ (targets modulo__Divisible.ml)
(deps q.mlw modulo.mlw)
- (action (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L . modulo.Divisible q.Q))
+ (action (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L . modulo.Divisible))
+ (mode promote)
+)
+
+(rule
+ (targets interval__Convexe.ml interval__Bound.ml)
+ (deps q.mlw modulo.mlw interval.mlw)
+ (action (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L . interval.Convexe interval.Bound))
(mode promote)
)
@@ -23,11 +39,11 @@
(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 runproof)
+ (deps (source_tree modulo) interval.mlw modulo.mlw q.mlw)
+ (action (run why3 replay -L . interval))
+)
; (rule
; (alias ide:q)
diff --git a/src_common/interval.mlw b/src_common/interval.mlw
index fefa2748ab7839783ab7aa1288aa23f7f8d39a80..903a2003581abed580e6fb0a1b948e0e17dcb59f 100644
--- a/src_common/interval.mlw
+++ b/src_common/interval.mlw
@@ -1,299 +1,553 @@
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 bool.Bool
use option.Option
use q.Q as Q
- use Bound as Bound
+ use Bound
+ use real.RealInfix
- 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) }
+ type t =
+ | Finite Q.t Bound.t Q.t Bound.t
+ | InfFinite Q.t Bound.t
+ | FiniteInf Q.t Bound.t
+ | Inf
+
+ type t' = { a: t }
invariant {
- if Q.(equal minv maxv)
- then minb = Bound.Large /\ maxb = Bound.Large
- else Q.(minv < maxv)
+ match a with
+ | Inf | InfFinite _ _ | FiniteInf _ _ -> true
+ | Finite minv minb maxv maxb ->
+ if Q.(equal minv maxv)
+ then minb = Bound.Large /\ maxb = Bound.Large
+ else Q.(minv < maxv)
+ end
}
- 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)
+
+ predicate cmp (x:real) (b:Bound.t) (y:real) =
+ match b with
+ | Bound.Large -> x <=. y
+ | Bound.Strict -> x <. y
+ end
+
+ predicate mem (x:real) (e:t') =
+ match e.a with
+ | Inf -> true
+ | InfFinite v b -> cmp x b v
+ | FiniteInf v b -> cmp v b x
+ | Finite v b v' b' -> cmp v b x /\ cmp x b' v'
+ end
+
+ let lemma exists_mem (e:t') : real
+ ensures { mem result e } =
+ match e.a with
+ | Inf -> 0.
+ | InfFinite v _ -> v.Q.real -. 1.
+ | FiniteInf v _ -> v.Q.real +. 1.
+ | Finite v _ v' _ ->
+ 0.75 *. v.Q.real +. 0.25 *. v'.Q.real
+ end
let is_singleton e
- ensures { forall q. mem q e -> (forall q'. mem q' e -> Q.equal q q') -> result = Some q }
+ ensures { forall q. mem q e -> (forall q'. mem q' e -> q = q') -> match result with | Some q'' -> mem q'' e | None -> false end }
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
+ match e.a with
+ | Inf -> assert { mem 0. e }; assert { mem 1. e }; None
+ | InfFinite v _ -> assert { mem (v.Q.real -. 2.) e }; assert { mem (v.Q.real -. 1.) e }; None
+ | FiniteInf v _ -> assert { mem (v.Q.real +. 2.) e }; assert { mem (v.Q.real +. 1.) e }; None
+ | Finite v b v' b' -> if Q.(v = v') then begin
+ assert { b = Bound.Large /\ b' = Bound.Large };
+ assert { forall q. mem q e -> q = v.Q.real };
+ Some v
+ end else begin
+ let ghost c = 0.75 *. v.Q.real +. 0.25 *. v'.Q.real in
+ let ghost c' = 0.25 *. v.Q.real +. 0.75 *. v'.Q.real in
+ assert { cmp v b c }; assert { cmp c b' v'};
+ assert { cmp v b c' }; assert { cmp c' b' v'};
+ assert { mem c e }; assert { mem c' e };
+ None
+ end
+ end
let singleton q
ensures { mem q result }
- ensures { forall q'. mem q' result -> Q.equal q q' }
+ ensures { forall q'. mem q' result -> q.Q.real = q' }
+ =
+ { a = Finite q Bound.Large q Bound.Large }
+
+
+ let except e x
+ ensures {
+ forall q. mem q e -> q <> x.Q.real ->
+ match result with
+ | Some res -> mem q res
+ | None -> false
+ end
+ }
+ =
+ match e.a with
+ | Inf
+ | InfFinite _ Strict
+ | FiniteInf _ Strict -> Some e
+ | InfFinite v Large -> if Q.(v = x) then Some {a=InfFinite v Strict} else Some e
+ | FiniteInf v Large -> if Q.(v = x) then Some {a=FiniteInf v Strict} else Some e
+ | Finite _ Strict _ Strict -> Some e
+ | Finite v Strict v' Large -> if Q.(v' = x) then Some {a=Finite v Strict v' Strict} else Some e
+ | Finite v Large v' Strict -> if Q.(v = x) then Some {a=Finite v Strict v' Strict} else Some e
+ | Finite v Large v' Large ->
+ let is_min = Q.(v = x) in
+ let is_max = Q.(v' = x) in
+ if is_min && is_max then None
+ else if is_min
+ then Some {a = Finite v Strict v' Large }
+ else if is_max
+ then Some {a = Finite v Large v' Strict }
+ else Some e
+ end
+
+ type is_comparable =
+ | Gt
+ | Lt
+ | Ge
+ | Le
+ | Uncomparable
+
+ use q.Ord as Ord
+
+ let is_comparable e1 e2
+ ensures {
+ match result with
+ | Uncomparable -> true
+ | Lt -> forall q1 q2. mem q1 e1 -> mem q2 e2 -> q1 <. q2
+ | Gt -> forall q1 q2. mem q1 e1 -> mem q2 e2 -> q1 >. q2
+ | Le -> forall q1 q2. mem q1 e1 -> mem q2 e2 -> q1 <=. q2
+ | Ge -> forall q1 q2. mem q1 e1 -> mem q2 e2 -> q1 >=. q2
+ end
+ }
+ =
+ match e1.a, e2.a with
+ | Inf, Inf
+ | Inf, _
+ | _, Inf
+ | InfFinite _ _, InfFinite _ _
+ | FiniteInf _ _, FiniteInf _ _ -> Uncomparable
+ | FiniteInf v1 b1, InfFinite v2 b2
+ | Finite v1 b1 _ _, InfFinite v2 b2
+ | FiniteInf v1 b1, Finite _ _ v2 b2 ->
+ match Q.compare v1 v2 with
+ | Ord.Eq ->
+ match b1, b2 with
+ | Large, Large -> Ge
+ | _ -> Gt
+ end
+ | Ord.Lt -> Uncomparable
+ | Ord.Gt -> Gt
+ end
+ | Finite _ _ v1 b1, FiniteInf v2 b2
+ | InfFinite v1 b1, FiniteInf v2 b2
+ | InfFinite v1 b1, Finite v2 b2 _ _ ->
+ match Q.compare v1 v2 with
+ | Ord.Eq ->
+ match b1, b2 with
+ | Large, Large -> Le
+ | _ -> Lt
+ end
+ | Ord.Lt -> Lt
+ | Ord.Gt -> Uncomparable
+ end
+ | Finite v1 b1 v1' b1', Finite v2 b2 v2' b2' ->
+ match Q.compare v1' v2, Q.compare v1 v2' with
+ | Ord.Eq, _ ->
+ match b1', b2 with
+ | Large, Large -> Le
+ | _ -> Lt
+ end
+ | _, Ord.Eq ->
+ match b1, b2' with
+ | Large, Large -> Ge
+ | _ -> Gt
+ end
+ | Ord.Lt, _ -> Lt
+ | _, Ord.Gt -> Gt
+ | _ -> Uncomparable
+ end
+ end
+
+
+
+ let is_distinct e1 e2
+ ensures { result -> (forall q1 q2. mem q1 e1 -> mem q2 e2 -> q1 <> q2) }
=
- {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
+ | Uncomparable | Le | Ge -> false
| _ -> true
+ end
+
- 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 =
+ let is_included e1 e2
+ ensures { result -> (forall q. mem q e1 -> mem q e2) }
+ =
+ match e1.a, e2.a with
+ | Inf, Inf -> true
+ | Inf, _
+ | InfFinite _ _ , (FiniteInf _ _ | Finite _ _ _ _)
+ | FiniteInf _ _ , (InfFinite _ _ | Finite _ _ _ _) -> false
+ | _, Inf -> true
+ | InfFinite v1 b1, InfFinite v2 b2
+ | Finite _ _ v1 b1, InfFinite v2 b2 ->
+ match Q.compare v1 v2 with
+ | Ord.Eq ->
+ match b1, b2 with
+ | Large, Strict -> false
+ | _ -> true
+ end
+ | Ord.Lt -> true
+ | Ord.Gt -> false
+ end
+ | FiniteInf v1 b1, FiniteInf v2 b2
+ | Finite v1 b1 _ _, FiniteInf v2 b2 ->
+ match Q.compare v1 v2 with
+ | Ord.Eq ->
+ match b1, b2 with
+ | Large, Strict -> false
+ | _ -> true
+ end
+ | Ord.Lt -> false
+ | Ord.Gt -> true
+ end
+ | Finite v1 b1 v1' b1', Finite v2 b2 v2' b2' ->
+ match Q.compare v2 v1, Q.compare v1' v2', b1, b2, b1', b2' with
+ | Ord.Eq, _, Large, Strict, _,_ -> false
+ | _, Ord.Eq, _,_, Large, Strict -> false
+ | (Ord.Lt | Ord.Eq), (Ord.Lt | Ord.Eq), _, _, _, _ -> true
+ | _ -> false
+ end
+ end
+
+ let cmp (x:Q.t) (b:Bound.t) (y:Q.t) =
+ match b with
+ | Bound.Large -> Q.(x <= y)
+ | Bound.Strict -> Q.(x < y)
+ end
+
+ let mem (x:Q.t) (e:t')
+ ensures { result = mem x.Q.real e } =
+ match e.a with
+ | Inf -> true
+ | InfFinite v b -> cmp x b v
+ | FiniteInf v b -> cmp v b x
+ | Finite v b v' b' -> andb (cmp v b x) (cmp x b' v')
+ end
+
+ let mult_pos q e
+ requires { Q.(0. <. q.real) }
+ ensures { forall q'. mem q' e -> mem (q.Q.real *. q') result }
+ =
+ assert { forall a b. (q.Q.real *. a) <. (q.Q.real *. b) <-> a <. b };
+ assert { forall a b. (q.Q.real *. a) <=. (q.Q.real *. b) <-> a <=. b };
+ match e.a with
+ | Inf -> { a = Inf }
+ | InfFinite v b -> { a = InfFinite Q.(q*v) b }
+ | FiniteInf v b -> { a = FiniteInf Q.(q*v) b }
+ | Finite v b v' b' ->
+ { a = Finite Q.(q*v) b Q.(q*v') b' }
+ end
+
+ let mult_neg q e
+ requires { Q.(q.real <. 0.) }
+ ensures { forall q'. mem q' e -> mem (q.Q.real *. q') result }
+ =
+ assert { forall a b. (q.Q.real *. a) >. (q.Q.real *. b) <-> a <. b };
+ assert { forall a b. (q.Q.real *. a) >=. (q.Q.real *. b) <-> a <=. b };
+ match e.a with
+ | Inf -> { a = Inf }
+ | InfFinite v b -> { a = FiniteInf Q.(q*v) b }
+ | FiniteInf v b -> { a = InfFinite Q.(q*v) b }
+ | Finite v b v' b' -> { a = Finite Q.(q*v') b' Q.(q*v) b }
+ end
+
+ let mult_cst c e
+ ensures { forall q. mem q e -> mem (c.Q.real *. q) result }
+ =
+ if Q.(c = (of_int 0)) then singleton (Q.of_int 0)
+ else if Q.(of_int 0 < c) then mult_pos c e
+ else mult_neg c e
+
+ let add_cst q e
+ ensures { forall q'. mem q' e -> mem (q.Q.real +. q') result }
+ =
+ match e.a with
+ | Inf -> { a = Inf }
+ | InfFinite v b -> { a = InfFinite Q.(q+v) b }
+ | FiniteInf v b -> { a = FiniteInf Q.(q+v) b }
+ | Finite v b v' b' -> { a = Finite Q.(q+v) b Q.(q+v') b' }
+ end
+
+ let add_bound b1 b2
+ ensures { forall c d c' d'. cmp c b1 d -> cmp c' b2 d' -> cmp (c+.c') result (d +. d') }
+ ensures { b1 = Large -> b2 = Large -> result = Large }
+ =
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
+ | Large, Large -> Large
+ | Large, Strict -> Strict
+ | Strict, Large -> Strict
+ | Strict, Strict -> Strict
+ end
+
+ let add e1 e2
+ ensures { forall q1 q2. mem q1 e1 -> mem q2 e2 -> mem (q1 +. q2) result }
+ =
+ match e1.a, e2.a with
+ | Inf, _ | _, Inf -> { a = Inf }
+ | InfFinite _ _, FiniteInf _ _ | FiniteInf _ _, InfFinite _ _ -> { a = Inf }
+ | InfFinite v1 b1, (InfFinite v2 b2 | Finite _ _ v2 b2)
+ | Finite _ _ v2 b2, InfFinite v1 b1
+ -> { a = InfFinite Q.(v1+v2) (add_bound b1 b2) }
+ | FiniteInf v1 b1, (FiniteInf v2 b2 | Finite v2 b2 _ _)
+ | Finite v2 b2 _ _, FiniteInf v1 b1
+ -> { a = FiniteInf Q.(v1+v2) (add_bound b1 b2) }
+ | Finite v1 b1 v1' b1', Finite v2 b2 v2' b2' ->
+ { a = Finite Q.(v1+v2) (add_bound b1 b2) Q.(v1'+v2') (add_bound b1' b2') }
+ end
+
+ let minus e1 e2
+ ensures { forall q1 q2. mem q1 e1 -> mem q2 e2 -> mem (q1 -. q2) result }
+ =
+ add e1 (mult_neg Q.(of_int (-1)) e2)
+
+ let gt c
+ ensures { forall q. mem q result <-> q >. c }
+ =
+ { a = FiniteInf c Strict }
+
+ let ge c
+ ensures { forall q. mem q result <-> q >=. c }
+ =
+ { a = FiniteInf c Large }
+
+ let lt c
+ ensures { forall q. mem q result <-> q <. c }
+ =
+ { a = InfFinite c Strict }
+
+ let le c
+ ensures { forall q. mem q result <-> q <=. c }
+ =
+ { a = InfFinite c Large }
+
+ let min_bound_sup v1 b1 v2 b2: (v3:Q.t,b3:Bound.t)
+ ensures { forall q. (cmp q b1 v1 /\ cmp q b2 v2) <-> cmp q b3 v3 }
+ ensures { Q.(v3 <= v1) } ensures { Q.(v3 <= v2) }
+ ensures { b1 = Large -> b2 = Large -> b3 = Large }
+ =
+ match Q.compare v1 v2, b1, b2 with
+ | Ord.Eq, Large, Large -> (v1,Large)
+ | Ord.Eq, _ ,_ -> (v1,Strict)
+ | Ord.Lt, _, _ -> (v1,b1)
+ | Ord.Gt, _ ,_ -> (v2,b2)
+ end
+
+ let min_bound_inf v1 b1 v2 b2: (v3:Q.t,b3:Bound.t)
+ ensures { forall q. (cmp v1 b1 q \/ cmp v2 b2 q) <-> cmp v3 b3 q }
+ ensures { Q.(v3 <= v1) } ensures { Q.(v3 <= v2) }
+ ensures { b1 = Large -> b2 = Large -> b3 = Large }
+ =
+ match Q.compare v1 v2, b1, b2 with
+ | Ord.Eq, Strict, Strict -> (v1,Strict)
+ | Ord.Eq, _, _ -> (v1,Large)
+ | Ord.Lt, _, _ -> (v1,b1)
+ | Ord.Gt, _, _ -> (v2,b2)
end
-*)
+
+ let max_bound_sup v1 b1 v2 b2: (v3:Q.t,b3:Bound.t)
+ ensures { forall q. (cmp q b1 v1 \/ cmp q b2 v2) <-> cmp q b3 v3 }
+ ensures { Q.(v1 <= v3) } ensures { Q.(v2 <= v3) }
+ ensures { b1 = Large -> b2 = Large -> b3 = Large }
+ =
+ match Q.compare v1 v2, b1, b2 with
+ | Ord.Eq, Strict, Strict -> (v1,Strict)
+ | Ord.Eq, _, _ -> (v1,Large)
+ | Ord.Lt, _, _ -> (v2,b2)
+ | Ord.Gt, _, _ -> (v1,b1)
+ end
+
+ let max_bound_inf v1 b1 v2 b2: (v3:Q.t,b3:Bound.t)
+ ensures { forall q. (cmp v1 b1 q /\ cmp v2 b2 q) <-> cmp v3 b3 q }
+ ensures { Q.(v1 <= v3) } ensures { Q.(v2 <= v3) }
+ ensures { b1 = Large -> b2 = Large -> b3 = Large }
+ =
+ match Q.compare v1 v2, b1, b2 with
+ | Ord.Eq, Large, Large -> (v1,Large)
+ | Ord.Eq, _, _ -> (v1,Strict)
+ | Ord.Lt, _, _ -> (v2,b2)
+ | Ord.Gt, _, _ -> (v1,b1)
+ end
+
+ let union e1 e2
+ ensures { forall q. mem q e1 -> mem q result }
+ ensures { forall q. mem q e2 -> mem q result }
+ =
+ match e1.a, e2.a with
+ | Inf, _ | _, Inf -> { a = Inf }
+ | InfFinite _ _, FiniteInf _ _ | FiniteInf _ _, InfFinite _ _ -> { a = Inf }
+ | InfFinite v1 b1, (InfFinite v2 b2 | Finite _ _ v2 b2)
+ | Finite _ _ v2 b2, InfFinite v1 b1
+ ->
+ let v3,b3 = max_bound_sup v1 b1 v2 b2 in
+ { a = InfFinite v3 b3 }
+ | FiniteInf v1 b1, (FiniteInf v2 b2 | Finite v2 b2 _ _)
+ | Finite v2 b2 _ _, FiniteInf v1 b1
+ -> let v3,b3 = min_bound_inf v1 b1 v2 b2 in
+ { a = FiniteInf v3 b3 }
+ | Finite v1 b1 v1' b1', Finite v2 b2 v2' b2' ->
+ let v3,b3 = min_bound_inf v1 b1 v2 b2 in
+ let v4,b4 = max_bound_sup v1' b1' v2' b2' in
+ { a = Finite v3 b3 v4 b4 }
+ end
+
+ predicate mem_bottom (q:real) (e:option t') =
+ match e with
+ | Some e -> mem q e
+ | None -> false
+ end
+
+ lemma mem_bottom_som: forall q e [mem_bottom q (Some e)]. mem_bottom q (Some e) = mem q e
+
+ let mk_finite v1 b1 v2 b2
+ ensures { forall q. (cmp v1 b1 q /\ cmp q b2 v2) <-> mem_bottom q result }
+ =
+ match Q.compare v1 v2 with
+ | Ord.Eq ->
+ match b1, b2 with
+ | Large, Large ->
+ assert { forall q. cmp v1 b1 q -> cmp q b2 v2 -> q = v1.Q.real};
+ Some { a = Finite v1 Large v2 Large }
+ | _ -> None
+ end
+ | Ord.Lt -> Some { a = Finite v1 b1 v2 b2 }
+ | Ord.Gt -> None
+ end
+
+ let inter e1 e2
+ ensures { forall q. (mem q e1 /\ mem q e2) <-> mem_bottom q result }
+ =
+ match e1.a, e2.a with
+ | Inf, _ -> Some e2
+ | _, Inf -> Some e1
+ | InfFinite v1 b1, FiniteInf v2 b2
+ | FiniteInf v2 b2, InfFinite v1 b1 ->
+ mk_finite v2 b2 v1 b1
+ | InfFinite v1 b1, InfFinite v2 b2 ->
+ let v3,b3 = min_bound_sup v1 b1 v2 b2 in
+ Some { a = InfFinite v3 b3 }
+ | InfFinite v1 b1, Finite v2 b2 v3 b3
+ | Finite v2 b2 v3 b3, InfFinite v1 b1
+ ->
+ let v4,b4 = min_bound_sup v1 b1 v3 b3 in
+ mk_finite v2 b2 v4 b4
+ | FiniteInf v1 b1, FiniteInf v2 b2 ->
+ let v3,b3 = max_bound_inf v1 b1 v2 b2 in
+ let r = { a = FiniteInf v3 b3 } in
+ assert { forall q. mem q r -> cmp v3 b3 q };
+ assert { forall q. cmp v3 b3 q -> cmp v1 b1 q };
+ assert { forall q. cmp v1 b1 q -> mem q e1 };
+ Some r
+ | FiniteInf v1 b1, Finite v2 b2 v3 b3
+ | Finite v2 b2 v3 b3, FiniteInf v1 b1
+ ->
+ let v4,b4 = max_bound_inf v1 b1 v2 b2 in
+ mk_finite v4 b4 v3 b3
+ | Finite v1 b1 v1' b1', Finite v2 b2 v2' b2' ->
+ let v3,b3 = max_bound_inf v1 b1 v2 b2 in
+ let v4,b4 = min_bound_sup v1' b1' v2' b2' in
+ assert { forall q. mem q e1 -> mem q e2 -> cmp v3 b3 q };
+ assert { forall q. mem q e1 -> mem q e2 -> cmp q b4 v4 };
+ mk_finite v3 b3 v4 b4
+ end
+
+ let zero = let r = singleton Q.(of_int 0) in assert { forall q. mem q r <-> q = 0. }; r
+
+ let reals = let r = {a=Inf} in assert { forall q. mem q r }; r
+
+ let is_reals e
+ ensures { result = (forall q. mem q e) }
+ =
+ match e.a with
+ | Inf -> true
+ | InfFinite v _ -> assert { not (mem (v.Q.real +. 1.) e) }; false
+ | FiniteInf v _ -> assert { not (mem (v.Q.real -. 1.) e) }; false
+ | Finite v _ _ _ -> assert { not (mem (v.Q.real -. 1.) e) }; false
+ end
+
+
+ let choose e
+ ensures { mem result e }
+ =
+ match e.a with
+ | Inf -> Q.(of_int 0)
+ | InfFinite v Large
+ | FiniteInf v Large
+ | Finite v Large _ _
+ | Finite _ _ v Large -> v
+ | InfFinite v Strict -> Q.(v - (of_int 1))
+ | FiniteInf v Strict -> Q.(v + (of_int 1))
+ | Finite v1 Strict v2 Strict ->
+ let half = Q.make 1 2 in
+ Q.(v1 * half + v2 * half)
+ end
+
+ type split_heuristic =
+ | Singleton Q.t
+ | Splitted t' t'
+ | NotSplitted
+
+ let split_heuristic c
+ ensures { forall q. mem q c -> match result with
+ | Singleton q' -> q = q'
+ | Splitted c1 c2 -> mem q c1 \/ mem q c2
+ | NotSplitted -> true
+ end
+ }
+ =
+ let qzero = Q.of_int 0 in
+ let zero = singleton qzero in
+ match c.a with
+ | Inf -> Splitted { a = InfFinite qzero Strict } { a = FiniteInf qzero Large }
+ | InfFinite v b ->
+ match Q.compare qzero v, b with
+ | Ord.Eq, Large ->
+ Splitted { a = InfFinite qzero Strict } zero
+ | Ord.Eq, Strict
+ | Ord.Gt, _ -> NotSplitted
+ | Ord.Lt, _ ->
+ Splitted { a = InfFinite qzero Strict } { a = Finite qzero Large v b }
+ end
+ | FiniteInf v b ->
+ match Q.compare v qzero, b with
+ | Ord.Eq, Large ->
+ Splitted zero { a = FiniteInf v Strict }
+ | Ord.Eq, Strict
+ | Ord.Gt, _ -> NotSplitted
+ | Ord.Lt, _ ->
+ Splitted { a = Finite v b qzero Strict } { a = FiniteInf qzero Large }
+ end
+ | Finite v1 b1 v2 b2 ->
+ match Q.compare v1 qzero, b1, Q.compare v2 qzero, b2, Q.compare v1 v2 with
+ | _, _, _, _, Ord.Eq ->
+ Singleton v1
+ | Ord.Eq, Large, _, _, _ ->
+ Splitted zero { a = Finite qzero Strict v2 b2 }
+ | _, _, Ord.Eq, Large, _ ->
+ Splitted { a = Finite v1 b1 qzero Strict } zero
+ | _ ->
+ let half = Q.make 1 2 in
+ let m = Q.(half * v1 + half * v2) in
+ Splitted { a = Finite v1 b1 m Strict } { a = Finite m Large v2 b2 }
+ end
+ end
+
end
diff --git a/src_common/interval/why3session.xml b/src_common/interval/why3session.xml
new file mode 100644
index 0000000000000000000000000000000000000000..04acfc6637590f0dac1575aee40708fc7e0fd45b
--- /dev/null
+++ b/src_common/interval/why3session.xml
@@ -0,0 +1,1293 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="6">
+<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"/>
+<file format="whyml" proved="true">
+<path name=".."/><path name="interval.mlw"/>
+<theory name="Convexe" proved="true">
+ <goal name="t''vc" expl="VC for t'" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="15710"/></proof>
+ </goal>
+ <goal name="exists_mem'vc" expl="VC for exists_mem" proved="true">
+ <proof prover="1"><result status="valid" time="0.54" steps="3253"/></proof>
+ </goal>
+ <goal name="is_singleton'vc" expl="VC for is_singleton" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="is_singleton'vc.0" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="27812"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.1" expl="assertion" proved="true">
+ <proof prover="2"><result status="valid" time="0.06" steps="7112"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.2" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.15" steps="831"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.3" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.13" steps="867"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.4" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.13" steps="834"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.5" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.14" steps="851"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.6" expl="assertion" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="7657"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.7" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="197"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.8" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.13" steps="150"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.9" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="63"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.10" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="63"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.11" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="66"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.12" expl="assertion" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="7320"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.13" expl="assertion" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="7337"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.14" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="is_singleton'vc.14.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="is_singleton'vc.14.0.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.14.0.1" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="32003"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.14.0.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.14.0.3" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="119"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="is_singleton'vc.14.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="is_singleton'vc.14.1.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.14.1.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.14.1.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.14.1.3" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="109"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="is_singleton'vc.15" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="is_singleton'vc.15.0" expl="postcondition" proved="true">
+ <proof prover="2" timelimit="5"><result status="valid" time="0.02" steps="7017"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.15.1" expl="postcondition" proved="true">
+ <proof prover="2" timelimit="5"><result status="valid" time="0.02" steps="7055"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.15.2" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="7047"/></proof>
+ </goal>
+ <goal name="is_singleton'vc.15.3" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="41007"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="8566"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="singleton'vc" expl="VC for singleton" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="30166"/></proof>
+ </goal>
+ <goal name="except'vc" expl="VC for except" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="except'vc.0" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+ </goal>
+ <goal name="except'vc.1" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+ </goal>
+ <goal name="except'vc.2" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
+ </goal>
+ <goal name="except'vc.3" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
+ </goal>
+ <goal name="except'vc.4" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="55"/></proof>
+ </goal>
+ <goal name="except'vc.5" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="53"/></proof>
+ </goal>
+ <goal name="except'vc.6" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="except'vc.6.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="except'vc.6.0.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
+ </goal>
+ <goal name="except'vc.6.0.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="except'vc.6.0.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="1.05" steps="3161"/></proof>
+ </goal>
+ <goal name="except'vc.6.0.3" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="except'vc.6.0.4" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.44" steps="1651"/></proof>
+ </goal>
+ <goal name="except'vc.6.0.5" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="except'vc.6.0.6" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.42" steps="1778"/></proof>
+ </goal>
+ <goal name="except'vc.6.0.7" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.47" steps="1928"/></proof>
+ </goal>
+ <goal name="except'vc.6.0.8" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.62" steps="2794"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="except'vc.6.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="except'vc.6.1.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="except'vc.6.1.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="except'vc.6.1.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="101"/></proof>
+ </goal>
+ <goal name="except'vc.6.1.3" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="except'vc.6.1.4" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="101"/></proof>
+ </goal>
+ <goal name="except'vc.6.1.5" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="except'vc.6.1.6" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="119"/></proof>
+ </goal>
+ <goal name="except'vc.6.1.7" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="119"/></proof>
+ </goal>
+ <goal name="except'vc.6.1.8" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.09" steps="639"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="is_comparable'vc" expl="VC for is_comparable" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="is_comparable'vc.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.3" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.4" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="1.38" steps="4390"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.5" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="2.25" steps="6812"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.6" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.7" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.8" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="2.68" steps="5274"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.9" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="1.39" steps="4469"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.10" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.11" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="2.17" steps="5644"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.12" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="1.37" steps="4491"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.13" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="is_comparable'vc.13.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.29" steps="2122"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.13.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.44" steps="1731"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.13.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.11" steps="1491"/></proof>
+ </goal>
+ <goal name="is_comparable'vc.13.3" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.23" steps="1034"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="is_distinct'vc" expl="VC for is_distinct" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="83"/></proof>
+ </goal>
+ <goal name="is_included'vc" expl="VC for is_included" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="is_included'vc.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.04" steps="390"/></proof>
+ </goal>
+ <goal name="is_included'vc.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.07" steps="644"/></proof>
+ </goal>
+ <goal name="is_included'vc.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="is_included'vc.3" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="is_included'vc.4" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.23" steps="1371"/></proof>
+ </goal>
+ <goal name="is_included'vc.5" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.15" steps="1095"/></proof>
+ </goal>
+ <goal name="is_included'vc.6" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="is_included'vc.7" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="is_included'vc.8" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="is_included'vc.9" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="is_included'vc.9.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.3" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.4" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="1.30" steps="4664"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.5" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.6" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.7" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.8" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.9" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.10" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.11" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.40" steps="1169"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.12" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.35" steps="1087"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.13" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.14" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.15" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.16" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.17" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.18" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.93" steps="3262"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.19" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.77" steps="2520"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.20" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.21" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.22" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.23" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.40" steps="1169"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.24" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.25" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.26" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.45" steps="998"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.27" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.28" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.29" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.30" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.35" steps="1206"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.31" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.46" steps="1239"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.32" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.33" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.46" steps="998"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.34" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.30" steps="884"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.35" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.36" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.37" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.54" steps="1462"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.38" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.49" steps="1470"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.39" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.40" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.41" steps="1333"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.41" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.36" steps="1327"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.42" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.43" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.44" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.45" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="2.17" steps="6550"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.46" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.47" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.48" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.69" steps="2458"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.49" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.50" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.51" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.52" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.50" steps="1473"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.53" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.39" steps="1341"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.54" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.55" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.43" steps="1459"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.56" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.52" steps="1324"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.57" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.58" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.59" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="1.53" steps="8083"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.60" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.79" steps="2989"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.61" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.62" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="1.48" steps="6612"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.63" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.87" steps="2600"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.64" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="is_included'vc.9.65" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="is_included'vc.10" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="is_included'vc.11" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="is_included'vc.12" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.29" steps="1490"/></proof>
+ </goal>
+ <goal name="is_included'vc.13" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.29" steps="1281"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="mem'vc" expl="VC for mem" proved="true">
+ <proof prover="1"><result status="valid" time="1.20" steps="5065"/></proof>
+ </goal>
+ <goal name="mult_pos'vc" expl="VC for mult_pos" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="mult_pos'vc.0" expl="assertion" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="mult_pos'vc.0.0" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.60" steps="1606789"/></proof>
+ </goal>
+ <goal name="mult_pos'vc.0.1" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.58" steps="1635162"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="mult_pos'vc.1" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="52"/></proof>
+ </goal>
+ <goal name="mult_pos'vc.2" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+ </goal>
+ <goal name="mult_pos'vc.3" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="mult_pos'vc.4" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="mult_pos'vc.5" expl="precondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="mult_pos'vc.5.0" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.05" steps="86"/></proof>
+ </goal>
+ <goal name="mult_pos'vc.5.1" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.05" steps="86"/></proof>
+ </goal>
+ <goal name="mult_pos'vc.5.2" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="41497"/></proof>
+ <proof prover="1"><result status="valid" time="0.05" steps="84"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="mult_pos'vc.6" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="mult_pos'vc.6.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.30" steps="1168"/></proof>
+ <proof prover="2"><result status="valid" time="0.05" steps="8301"/></proof>
+ </goal>
+ <goal name="mult_pos'vc.6.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="1.70" steps="4259"/></proof>
+ </goal>
+ <goal name="mult_pos'vc.6.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="1.84" steps="6042"/></proof>
+ </goal>
+ <goal name="mult_pos'vc.6.3" expl="postcondition" proved="true">
+ <proof prover="1" timelimit="30"><result status="valid" time="12.73" steps="27754"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="mult_neg'vc" expl="VC for mult_neg" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="mult_neg'vc.0" expl="assertion" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="mult_neg'vc.0.0" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.61" steps="1718062"/></proof>
+ </goal>
+ <goal name="mult_neg'vc.0.1" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.13" steps="543713"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="mult_neg'vc.1" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="52"/></proof>
+ </goal>
+ <goal name="mult_neg'vc.2" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+ </goal>
+ <goal name="mult_neg'vc.3" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="mult_neg'vc.4" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="mult_neg'vc.5" expl="precondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="mult_neg'vc.5.0" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.07" steps="86"/></proof>
+ </goal>
+ <goal name="mult_neg'vc.5.1" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.07" steps="86"/></proof>
+ </goal>
+ <goal name="mult_neg'vc.5.2" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.08" steps="84"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="mult_neg'vc.6" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="mult_neg'vc.6.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.17" steps="957"/></proof>
+ </goal>
+ <goal name="mult_neg'vc.6.1" expl="postcondition" proved="true">
+ <proof prover="1" timelimit="30"><result status="valid" time="5.14" steps="20219"/></proof>
+ </goal>
+ <goal name="mult_neg'vc.6.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="3.87" steps="10904"/></proof>
+ </goal>
+ <goal name="mult_neg'vc.6.3" expl="postcondition" proved="true">
+ <proof prover="1" timelimit="30"><result status="valid" time="13.26" steps="26368"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="mult_cst'vc" expl="VC for mult_cst" proved="true">
+ <proof prover="1"><result status="valid" time="0.25" steps="999"/></proof>
+ </goal>
+ <goal name="add_cst'vc" expl="VC for add_cst" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_cst'vc.0" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="6893"/></proof>
+ </goal>
+ <goal name="add_cst'vc.1" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="6939"/></proof>
+ </goal>
+ <goal name="add_cst'vc.2" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="6939"/></proof>
+ </goal>
+ <goal name="add_cst'vc.3" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.06" steps="482"/></proof>
+ </goal>
+ <goal name="add_cst'vc.4" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_cst'vc.4.0" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="7972"/></proof>
+ </goal>
+ <goal name="add_cst'vc.4.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="2.82" steps="9119"/></proof>
+ </goal>
+ <goal name="add_cst'vc.4.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="2.35" steps="5101"/></proof>
+ </goal>
+ <goal name="add_cst'vc.4.3" expl="postcondition" proved="true">
+ <proof prover="1" timelimit="30"><result status="valid" time="7.34" steps="26197"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_bound'vc" expl="VC for add_bound" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="31953"/></proof>
+ </goal>
+ <goal name="add'vc" expl="VC for add" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add'vc.0" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+ </goal>
+ <goal name="add'vc.1" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="7036"/></proof>
+ </goal>
+ <goal name="add'vc.2" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+ </goal>
+ <goal name="add'vc.3" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+ </goal>
+ <goal name="add'vc.4" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="add'vc.5" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="add'vc.6" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+ </goal>
+ <goal name="add'vc.7" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+ </goal>
+ <goal name="add'vc.8" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
+ </goal>
+ <goal name="add'vc.9" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="add'vc.10" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
+ </goal>
+ <goal name="add'vc.11" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="add'vc.12" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
+ </goal>
+ <goal name="add'vc.13" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="40553"/></proof>
+ </goal>
+ <goal name="add'vc.14" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add'vc.14.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.04" steps="417"/></proof>
+ </goal>
+ <goal name="add'vc.14.1" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="8156"/></proof>
+ </goal>
+ <goal name="add'vc.14.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.05" steps="442"/></proof>
+ </goal>
+ <goal name="add'vc.14.3" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.05" steps="465"/></proof>
+ </goal>
+ <goal name="add'vc.14.4" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="35698"/></proof>
+ </goal>
+ <goal name="add'vc.14.5" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="36661"/></proof>
+ </goal>
+ <goal name="add'vc.14.6" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.06" steps="441"/></proof>
+ </goal>
+ <goal name="add'vc.14.7" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.07" steps="465"/></proof>
+ </goal>
+ <goal name="add'vc.14.8" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="35698"/></proof>
+ </goal>
+ <goal name="add'vc.14.9" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="36805"/></proof>
+ </goal>
+ <goal name="add'vc.14.10" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.08" steps="495"/></proof>
+ </goal>
+ <goal name="add'vc.14.11" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="36819"/></proof>
+ </goal>
+ <goal name="add'vc.14.12" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="36675"/></proof>
+ </goal>
+ <goal name="add'vc.14.13" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="43886"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="minus'vc" expl="VC for minus" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="33927"/></proof>
+ </goal>
+ <goal name="gt'vc" expl="VC for gt" proved="true">
+ <proof prover="1"><result status="valid" time="0.19" steps="1087"/></proof>
+ </goal>
+ <goal name="ge'vc" expl="VC for ge" proved="true">
+ <proof prover="1"><result status="valid" time="0.21" steps="1269"/></proof>
+ </goal>
+ <goal name="lt'vc" expl="VC for lt" proved="true">
+ <proof prover="1"><result status="valid" time="0.20" steps="1080"/></proof>
+ </goal>
+ <goal name="le'vc" expl="VC for le" proved="true">
+ <proof prover="1"><result status="valid" time="0.19" steps="1080"/></proof>
+ </goal>
+ <goal name="min_bound_sup'vc" expl="VC for min_bound_sup" proved="true">
+ <proof prover="1"><result status="valid" time="0.10" steps="1263"/></proof>
+ </goal>
+ <goal name="min_bound_inf'vc" expl="VC for min_bound_inf" proved="true">
+ <proof prover="1"><result status="valid" time="0.20" steps="1546"/></proof>
+ </goal>
+ <goal name="max_bound_sup'vc" expl="VC for max_bound_sup" proved="true">
+ <proof prover="1"><result status="valid" time="0.09" steps="1310"/></proof>
+ </goal>
+ <goal name="max_bound_inf'vc" expl="VC for max_bound_inf" proved="true">
+ <proof prover="1"><result status="valid" time="0.15" steps="1447"/></proof>
+ </goal>
+ <goal name="union'vc" expl="VC for union" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="98815"/></proof>
+ </goal>
+ <goal name="mem_bottom_som" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="8585"/></proof>
+ </goal>
+ <goal name="mk_finite'vc" expl="VC for mk_finite" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="mk_finite'vc.0" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="35156"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
+ </goal>
+ <goal name="mk_finite'vc.1" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
+ </goal>
+ <goal name="mk_finite'vc.2" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
+ </goal>
+ <goal name="mk_finite'vc.3" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="mk_finite'vc.3.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="mk_finite'vc.3.0.0" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="38371"/></proof>
+ <proof prover="1"><result status="valid" time="4.74" steps="9146"/></proof>
+ </goal>
+ <goal name="mk_finite'vc.3.0.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+ </goal>
+ <goal name="mk_finite'vc.3.0.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="52"/></proof>
+ </goal>
+ <goal name="mk_finite'vc.3.0.3" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="34844"/></proof>
+ </goal>
+ <goal name="mk_finite'vc.3.0.4" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="51"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="mk_finite'vc.3.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.13" steps="1063"/></proof>
+ </goal>
+ <goal name="mk_finite'vc.3.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.12" steps="1059"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc" expl="VC for inter" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.0" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+ </goal>
+ <goal name="inter'vc.1" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="78"/></proof>
+ </goal>
+ <goal name="inter'vc.2" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
+ </goal>
+ <goal name="inter'vc.3" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.60" steps="2213"/></proof>
+ </goal>
+ <goal name="inter'vc.4" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+ </goal>
+ <goal name="inter'vc.5" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="103"/></proof>
+ </goal>
+ <goal name="inter'vc.6" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="105"/></proof>
+ </goal>
+ <goal name="inter'vc.7" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.7.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.7.0.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="inter'vc.7.0.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="19"/></proof>
+ </goal>
+ <goal name="inter'vc.7.0.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="inter'vc.7.0.3" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="171"/></proof>
+ </goal>
+ <goal name="inter'vc.7.0.4" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.90" steps="3447"/></proof>
+ </goal>
+ <goal name="inter'vc.7.0.5" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.04" steps="203"/></proof>
+ </goal>
+ <goal name="inter'vc.7.0.6" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="inter'vc.7.0.7" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="171"/></proof>
+ </goal>
+ <goal name="inter'vc.7.0.8" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.98" steps="2979"/></proof>
+ </goal>
+ <goal name="inter'vc.7.0.9" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.04" steps="202"/></proof>
+ </goal>
+ <goal name="inter'vc.7.0.10" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
+ </goal>
+ <goal name="inter'vc.7.0.11" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.04" steps="202"/></proof>
+ </goal>
+ <goal name="inter'vc.7.0.12" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.04" steps="203"/></proof>
+ </goal>
+ <goal name="inter'vc.7.0.13" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="103"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.7.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.7.1.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="426"/></proof>
+ </goal>
+ <goal name="inter'vc.7.1.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
+ </goal>
+ <goal name="inter'vc.7.1.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.04" steps="437"/></proof>
+ </goal>
+ <goal name="inter'vc.7.1.3" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.07" steps="523"/></proof>
+ </goal>
+ <goal name="inter'vc.7.1.4" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="83"/></proof>
+ </goal>
+ <goal name="inter'vc.7.1.5" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.55" steps="1645"/></proof>
+ </goal>
+ <goal name="inter'vc.7.1.6" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.06" steps="436"/></proof>
+ </goal>
+ <goal name="inter'vc.7.1.7" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.08" steps="524"/></proof>
+ </goal>
+ <goal name="inter'vc.7.1.8" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.86" steps="2816"/></proof>
+ </goal>
+ <goal name="inter'vc.7.1.9" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.50" steps="1796"/></proof>
+ </goal>
+ <goal name="inter'vc.7.1.10" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.07" steps="481"/></proof>
+ </goal>
+ <goal name="inter'vc.7.1.11" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.13" steps="717"/></proof>
+ </goal>
+ <goal name="inter'vc.7.1.12" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.14" steps="715"/></proof>
+ </goal>
+ <goal name="inter'vc.7.1.13" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.70" steps="3410"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.7.2" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.7.2.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="inter'vc.7.2.1" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.04" steps="469"/></proof>
+ </goal>
+ <goal name="inter'vc.7.2.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="inter'vc.7.2.3" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.07" steps="524"/></proof>
+ </goal>
+ <goal name="inter'vc.7.2.4" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.11" steps="618"/></proof>
+ </goal>
+ <goal name="inter'vc.7.2.5" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.13" steps="715"/></proof>
+ </goal>
+ <goal name="inter'vc.7.2.6" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="inter'vc.7.2.7" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.07" steps="523"/></proof>
+ </goal>
+ <goal name="inter'vc.7.2.8" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.92" steps="3021"/></proof>
+ </goal>
+ <goal name="inter'vc.7.2.9" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.13" steps="717"/></proof>
+ </goal>
+ <goal name="inter'vc.7.2.10" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
+ </goal>
+ <goal name="inter'vc.7.2.11" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.51" steps="1731"/></proof>
+ </goal>
+ <goal name="inter'vc.7.2.12" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.49" steps="1564"/></proof>
+ </goal>
+ <goal name="inter'vc.7.2.13" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.40" steps="1207"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="zero'vc" expl="VC for zero" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
+ </goal>
+ <goal name="reals'vc" expl="VC for reals" proved="true">
+ <proof prover="1"><result status="valid" time="0.04" steps="359"/></proof>
+ </goal>
+ <goal name="is_reals'vc" expl="VC for is_reals" proved="true">
+ <proof prover="1"><result status="valid" time="0.52" steps="2960"/></proof>
+ </goal>
+ <goal name="choose'vc" expl="VC for choose" proved="true">
+ <proof prover="1"><result status="valid" time="3.36" steps="8124"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc" expl="VC for split_heuristic" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="split_heuristic'vc.0" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.1" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.2" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.3" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.4" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.5" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.6" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.7" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.8" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.9" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.10" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.11" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.12" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="86"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.13" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="119"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.14" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="83"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.15" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="116"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.16" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.17" expl="precondition" proved="true">
+ <proof prover="1" timelimit="30"><result status="valid" time="12.99" steps="5200"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.18" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="60644"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.19" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.20" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="58842"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.21" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="60260"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.22" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="112"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.23" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.24" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="58686"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.25" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="61675"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.26" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.27" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="58613"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.28" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="59832"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="split_heuristic'vc.29.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="split_heuristic'vc.29.0.0" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="11264"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.1" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="12449"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.2" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="12438"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="split_heuristic'vc.29.0.3.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.09" steps="292"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.1" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.54" steps="132892"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.2" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.05" steps="11096"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.3" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.52" steps="132896"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.4" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.14" steps="390"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.5" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="46219"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.6" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="11096"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.7" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.06" steps="11290"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.8" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="11429"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.9" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.06" steps="10821"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.10" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="11026"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.11" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="10921"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.12" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="11026"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.13" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="48763"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.14" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="10876"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.15" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="10921"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.16" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.05" steps="10882"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.0.3.17" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="10922"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="split_heuristic'vc.29.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="split_heuristic'vc.29.1.0" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="43714"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="split_heuristic'vc.29.1.1.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.21" steps="1289"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.1.1" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="9272"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.1.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.30" steps="1920"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.1.3" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="26"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.1.4" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="40477"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.1.5" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="45546"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.2" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="split_heuristic'vc.29.1.2.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.21" steps="1328"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.2.1" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="9272"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.2.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.43" steps="2232"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.2.3" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="40420"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.2.4" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="26"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.2.5" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="45522"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="split_heuristic'vc.29.1.3.0" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.07" steps="10777"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.1" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="10870"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.2" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="11027"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.3" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="42200"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.4" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="42888"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.5" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="10976"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.6" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="11027"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.7" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="11167"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.8" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.05" steps="11024"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.9" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.06" steps="12177"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.10" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.55" steps="1517"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.11" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.63" steps="2077"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.12" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="49104"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.13" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="59890"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.14" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="60808"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.15" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="49100"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.16" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="60803"/></proof>
+ </goal>
+ <goal name="split_heuristic'vc.29.1.3.17" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="60738"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/src_common/interval__Bound.ml b/src_common/interval__Bound.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c743dbf27d9d032cecdbc5c1afd692153cf036c6
--- /dev/null
+++ b/src_common/interval__Bound.ml
@@ -0,0 +1,4 @@
+type t =
+ | Strict
+ | Large
+
diff --git a/src_common/interval__Convexe.ml b/src_common/interval__Convexe.ml
new file mode 100644
index 0000000000000000000000000000000000000000..94f3de4d9df7a9fc092dacf9a6824d3d5c794a21
--- /dev/null
+++ b/src_common/interval__Convexe.ml
@@ -0,0 +1,510 @@
+type t =
+ | Finite of Q.t * Interval__Bound.t * Q.t * Interval__Bound.t
+ | InfFinite of Q.t * Interval__Bound.t
+ | FiniteInf of Q.t * Interval__Bound.t
+ | Inf
+
+type t' = t
+
+let is_singleton (e: t') : (Q.t) option =
+ match e with
+ | Inf -> None
+ | InfFinite (v, _) -> None
+ | FiniteInf (v, _) -> None
+ | Finite (v, b, v', b') -> if (Q.equal v v') then Some v else None
+
+let singleton (q: Q.t) : t' =
+ Finite (q, Interval__Bound.Large, q, Interval__Bound.Large)
+
+let except (e: t') (x: Q.t) : t' option =
+ match e with
+ | (Inf | (InfFinite (_, Interval__Bound.Strict) | FiniteInf (_,
+ Interval__Bound.Strict))) ->
+ Some e
+ | InfFinite (v,
+ Interval__Bound.Large) ->
+ if (Q.equal v x)
+ then Some (InfFinite (v, Interval__Bound.Strict))
+ else Some e
+ | FiniteInf (v,
+ Interval__Bound.Large) ->
+ if (Q.equal v x)
+ then Some (FiniteInf (v, Interval__Bound.Strict))
+ else Some e
+ | Finite (_, Interval__Bound.Strict, _, Interval__Bound.Strict) -> Some e
+ | Finite (v,
+ Interval__Bound.Strict,
+ v',
+ Interval__Bound.Large) ->
+ if (Q.equal v' x)
+ then
+ Some (Finite (v, Interval__Bound.Strict, v', Interval__Bound.Strict))
+ else Some e
+ | Finite (v,
+ Interval__Bound.Large,
+ v',
+ Interval__Bound.Strict) ->
+ if (Q.equal v x)
+ then
+ Some (Finite (v, Interval__Bound.Strict, v', Interval__Bound.Strict))
+ else Some e
+ | Finite (v,
+ Interval__Bound.Large,
+ v',
+ Interval__Bound.Large) ->
+ (let is_min = (Q.equal v x) in let is_max = (Q.equal v' x) in
+ if is_min && is_max
+ then None
+ else
+ begin
+ if is_min
+ then
+ Some (Finite (v, Interval__Bound.Strict, v',
+ Interval__Bound.Large))
+ else
+ begin
+ if is_max
+ then
+ Some (Finite (v, Interval__Bound.Large, v',
+ Interval__Bound.Strict))
+ else Some e end end)
+
+type is_comparable =
+ | Gt
+ | Lt
+ | Ge
+ | Le
+ | Uncomparable
+
+let is_comparable (e1: t') (e2: t') : is_comparable =
+ match (e1, e2) with
+ | ((Inf,
+ Inf) | ((Inf,
+ _) | ((_,
+ Inf) | ((InfFinite (_, _), InfFinite (_,
+ _)) | (FiniteInf (_, _), FiniteInf (_, _)))))) ->
+ Uncomparable
+ | ((FiniteInf (v1, b1), InfFinite (v2,
+ b2)) | ((Finite (v1, b1, _, _), InfFinite (v2, b2)) | (FiniteInf (v1,
+ b1), Finite (_, _, v2, b2)))) ->
+ begin match (Q_extra.compare v1 v2) with
+ | Ord.Eq ->
+ begin match (b1, b2) with
+ | (Interval__Bound.Large, Interval__Bound.Large) -> Ge
+ | _ -> Gt
+ end
+ | Ord.Lt -> Uncomparable
+ | Ord.Gt -> Gt
+ end
+ | ((Finite (_, _, v1, b1), FiniteInf (v2,
+ b2)) | ((InfFinite (v1, b1), FiniteInf (v2, b2)) | (InfFinite (v1, b1),
+ Finite (v2, b2, _, _)))) ->
+ begin match (Q_extra.compare v1 v2) with
+ | Ord.Eq ->
+ begin match (b1, b2) with
+ | (Interval__Bound.Large, Interval__Bound.Large) -> Le
+ | _ -> Lt
+ end
+ | Ord.Lt -> Lt
+ | Ord.Gt -> Uncomparable
+ end
+ | (Finite (v1,
+ b1,
+ v1',
+ b1'),
+ Finite (v2,
+ b2,
+ v2',
+ b2')) ->
+ begin match ((Q_extra.compare v1' v2), (Q_extra.compare v1 v2')) with
+ | (Ord.Eq,
+ _) ->
+ begin match (b1', b2) with
+ | (Interval__Bound.Large, Interval__Bound.Large) -> Le
+ | _ -> Lt
+ end
+ | (_,
+ Ord.Eq) ->
+ begin match (b1, b2') with
+ | (Interval__Bound.Large, Interval__Bound.Large) -> Ge
+ | _ -> Gt
+ end
+ | (Ord.Lt, _) -> Lt
+ | (_, Ord.Gt) -> Gt
+ | _ -> Uncomparable
+ end
+
+let is_distinct (e1: t') (e2: t') : bool =
+ match is_comparable e1 e2 with
+ | (Uncomparable | (Le | Ge)) -> false
+ | _ -> true
+
+let is_included (e1: t') (e2: t') : bool =
+ match (e1, e2) with
+ | (Inf, Inf) -> true
+ | ((Inf,
+ _) | ((InfFinite (_, _),
+ (FiniteInf (_, _) | Finite (_, _, _, _))) | (FiniteInf (_, _),
+ (InfFinite (_, _) | Finite (_, _, _, _))))) ->
+ false
+ | (_, Inf) -> true
+ | ((InfFinite (v1, b1), InfFinite (v2, b2)) | (Finite (_, _, v1, b1),
+ InfFinite (v2, b2))) ->
+ begin match (Q_extra.compare v1 v2) with
+ | Ord.Eq ->
+ begin match (b1, b2) with
+ | (Interval__Bound.Large, Interval__Bound.Strict) -> false
+ | _ -> true
+ end
+ | Ord.Lt -> true
+ | Ord.Gt -> false
+ end
+ | ((FiniteInf (v1, b1), FiniteInf (v2, b2)) | (Finite (v1, b1, _, _),
+ FiniteInf (v2, b2))) ->
+ begin match (Q_extra.compare v1 v2) with
+ | Ord.Eq ->
+ begin match (b1, b2) with
+ | (Interval__Bound.Large, Interval__Bound.Strict) -> false
+ | _ -> true
+ end
+ | Ord.Lt -> false
+ | Ord.Gt -> true
+ end
+ | (Finite (v1,
+ b1,
+ v1',
+ b1'),
+ Finite (v2,
+ b2,
+ v2',
+ b2')) ->
+ begin
+ match
+ ((Q_extra.compare v2 v1), (Q_extra.compare v1' v2'), b1, b2, b1', b2')
+ with
+ | (Ord.Eq,
+ _,
+ Interval__Bound.Large,
+ Interval__Bound.Strict,
+ _,
+ _) ->
+ false
+ | (_,
+ Ord.Eq,
+ _,
+ _,
+ Interval__Bound.Large,
+ Interval__Bound.Strict) ->
+ false
+ | ((Ord.Lt | Ord.Eq), (Ord.Lt | Ord.Eq), _, _, _, _) -> true
+ | _ -> false
+ end
+
+let cmp (x: Q.t) (b: Interval__Bound.t) (y: Q.t) : bool =
+ match b with
+ | Interval__Bound.Large -> (Q.(<=) x y)
+ | Interval__Bound.Strict -> (Q.(<) x y)
+
+let mem (x: Q.t) (e: t') : bool =
+ match e with
+ | Inf -> true
+ | InfFinite (v, b) -> cmp x b v
+ | FiniteInf (v, b) -> cmp v b x
+ | Finite (v, b, v', b') -> cmp v b x && cmp x b' v'
+
+let mult_pos (q: Q.t) (e: t') : t' =
+ match e with
+ | Inf -> Inf
+ | InfFinite (v, b) -> InfFinite ((Q.( * ) q v), b)
+ | FiniteInf (v, b) -> FiniteInf ((Q.( * ) q v), b)
+ | Finite (v, b, v', b') -> Finite ((Q.( * ) q v), b, (Q.( * ) q v'), b')
+
+let mult_neg (q: Q.t) (e: t') : t' =
+ match e with
+ | Inf -> Inf
+ | InfFinite (v, b) -> FiniteInf ((Q.( * ) q v), b)
+ | FiniteInf (v, b) -> InfFinite ((Q.( * ) q v), b)
+ | Finite (v, b, v', b') -> Finite ((Q.( * ) q v'), b', (Q.( * ) q v), b)
+
+let mult_cst (c: Q.t) (e: t') : t' =
+ if (Q.equal c (Q.of_bigint Z.zero))
+ then singleton (Q.of_bigint Z.zero)
+ else
+ begin
+ if (Q.(<) (Q.of_bigint Z.zero) c) then mult_pos c e else mult_neg c e end
+
+let add_cst (q: Q.t) (e: t') : t' =
+ match e with
+ | Inf -> Inf
+ | InfFinite (v, b) -> InfFinite ((Q.(+) q v), b)
+ | FiniteInf (v, b) -> FiniteInf ((Q.(+) q v), b)
+ | Finite (v, b, v', b') -> Finite ((Q.(+) q v), b, (Q.(+) q v'), b')
+
+let add_bound (b1: Interval__Bound.t) (b2: Interval__Bound.t) :
+ Interval__Bound.t =
+ match (b1, b2) with
+ | (Interval__Bound.Large, Interval__Bound.Large) -> Interval__Bound.Large
+ | (Interval__Bound.Large, Interval__Bound.Strict) -> Interval__Bound.Strict
+ | (Interval__Bound.Strict, Interval__Bound.Large) -> Interval__Bound.Strict
+ | (Interval__Bound.Strict,
+ Interval__Bound.Strict) ->
+ Interval__Bound.Strict
+
+let add (e1: t') (e2: t') : t' =
+ match (e1, e2) with
+ | ((Inf, _) | (_, Inf)) -> Inf
+ | ((InfFinite (_, _), FiniteInf (_, _)) | (FiniteInf (_, _), InfFinite (_,
+ _))) ->
+ Inf
+ | ((InfFinite (v1, b1),
+ (InfFinite (v2, b2) | Finite (_, _, v2, b2))) | (Finite (_, _, v2, b2),
+ InfFinite (v1, b1))) ->
+ InfFinite ((Q.(+) v1 v2), add_bound b1 b2)
+ | ((FiniteInf (v1, b1),
+ (FiniteInf (v2, b2) | Finite (v2, b2, _, _))) | (Finite (v2, b2, _, _),
+ FiniteInf (v1, b1))) ->
+ FiniteInf ((Q.(+) v1 v2), add_bound b1 b2)
+ | (Finite (v1,
+ b1,
+ v1',
+ b1'),
+ Finite (v2,
+ b2,
+ v2',
+ b2')) ->
+ Finite ((Q.(+) v1 v2),
+ add_bound b1 b2,
+ (Q.(+) v1' v2'),
+ add_bound b1' b2')
+
+let minus (e1: t') (e2: t') : t' =
+ add e1 (mult_neg (Q.of_bigint (Z.of_string "-1")) e2)
+
+let gt (c: Q.t) : t' = FiniteInf (c, Interval__Bound.Strict)
+
+let ge (c: Q.t) : t' = FiniteInf (c, Interval__Bound.Large)
+
+let lt (c: Q.t) : t' = InfFinite (c, Interval__Bound.Strict)
+
+let le (c: Q.t) : t' = InfFinite (c, Interval__Bound.Large)
+
+let min_bound_sup (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t)
+ (b2: Interval__Bound.t) : (Q.t) * Interval__Bound.t =
+ match ((Q_extra.compare v1 v2), b1, b2) with
+ | (Ord.Eq,
+ Interval__Bound.Large,
+ Interval__Bound.Large) ->
+ (v1, Interval__Bound.Large)
+ | (Ord.Eq, _, _) -> (v1, Interval__Bound.Strict)
+ | (Ord.Lt, _, _) -> (v1, b1)
+ | (Ord.Gt, _, _) -> (v2, b2)
+
+let min_bound_inf (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t)
+ (b2: Interval__Bound.t) : (Q.t) * Interval__Bound.t =
+ match ((Q_extra.compare v1 v2), b1, b2) with
+ | (Ord.Eq,
+ Interval__Bound.Strict,
+ Interval__Bound.Strict) ->
+ (v1, Interval__Bound.Strict)
+ | (Ord.Eq, _, _) -> (v1, Interval__Bound.Large)
+ | (Ord.Lt, _, _) -> (v1, b1)
+ | (Ord.Gt, _, _) -> (v2, b2)
+
+let max_bound_sup (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t)
+ (b2: Interval__Bound.t) : (Q.t) * Interval__Bound.t =
+ match ((Q_extra.compare v1 v2), b1, b2) with
+ | (Ord.Eq,
+ Interval__Bound.Strict,
+ Interval__Bound.Strict) ->
+ (v1, Interval__Bound.Strict)
+ | (Ord.Eq, _, _) -> (v1, Interval__Bound.Large)
+ | (Ord.Lt, _, _) -> (v2, b2)
+ | (Ord.Gt, _, _) -> (v1, b1)
+
+let max_bound_inf (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t)
+ (b2: Interval__Bound.t) : (Q.t) * Interval__Bound.t =
+ match ((Q_extra.compare v1 v2), b1, b2) with
+ | (Ord.Eq,
+ Interval__Bound.Large,
+ Interval__Bound.Large) ->
+ (v1, Interval__Bound.Large)
+ | (Ord.Eq, _, _) -> (v1, Interval__Bound.Strict)
+ | (Ord.Lt, _, _) -> (v2, b2)
+ | (Ord.Gt, _, _) -> (v1, b1)
+
+let union (e1: t') (e2: t') : t' =
+ match (e1, e2) with
+ | ((Inf, _) | (_, Inf)) -> Inf
+ | ((InfFinite (_, _), FiniteInf (_, _)) | (FiniteInf (_, _), InfFinite (_,
+ _))) ->
+ Inf
+ | ((InfFinite (v1, b1),
+ (InfFinite (v2, b2) | Finite (_, _, v2, b2))) | (Finite (_, _, v2, b2),
+ InfFinite (v1, b1))) ->
+ (let (v3, b3) = max_bound_sup v1 b1 v2 b2 in InfFinite (v3, b3))
+ | ((FiniteInf (v1, b1),
+ (FiniteInf (v2, b2) | Finite (v2, b2, _, _))) | (Finite (v2, b2, _, _),
+ FiniteInf (v1, b1))) ->
+ (let (v31, b31) = min_bound_inf v1 b1 v2 b2 in FiniteInf (v31, b31))
+ | (Finite (v1,
+ b1,
+ v1',
+ b1'),
+ Finite (v2,
+ b2,
+ v2',
+ b2')) ->
+ (let (v32, b32) = min_bound_inf v1 b1 v2 b2 in
+ let (v4,
+ b4) =
+ max_bound_sup v1' b1' v2' b2' in
+ Finite (v32, b32, v4, b4))
+
+let mk_finite (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t)
+ (b2: Interval__Bound.t) : t' option =
+ match (Q_extra.compare v1 v2) with
+ | Ord.Eq ->
+ begin match (b1, b2) with
+ | (Interval__Bound.Large,
+ Interval__Bound.Large) ->
+ Some (Finite (v1, Interval__Bound.Large, v2, Interval__Bound.Large))
+ | _ -> None
+ end
+ | Ord.Lt -> Some (Finite (v1, b1, v2, b2))
+ | Ord.Gt -> None
+
+let inter (e1: t') (e2: t') : t' option =
+ match (e1, e2) with
+ | (Inf, _) -> Some e2
+ | (_, Inf) -> Some e1
+ | ((InfFinite (v1, b1), FiniteInf (v2, b2)) | (FiniteInf (v2, b2),
+ InfFinite (v1, b1))) ->
+ mk_finite v2 b2 v1 b1
+ | (InfFinite (v1,
+ b1),
+ InfFinite (v2,
+ b2)) ->
+ (let (v33, b33) = min_bound_sup v1 b1 v2 b2 in
+ Some (InfFinite (v33, b33)))
+ | ((InfFinite (v1, b1), Finite (v2, b2, v34, b34)) | (Finite (v2, b2, v34,
+ b34), InfFinite (v1, b1))) ->
+ (let (v41, b41) = min_bound_sup v1 b1 v34 b34 in mk_finite v2 b2 v41 b41)
+ | (FiniteInf (v1,
+ b1),
+ FiniteInf (v2,
+ b2)) ->
+ (let (v34, b34) = max_bound_inf v1 b1 v2 b2 in
+ let r = FiniteInf (v34, b34) in Some r)
+ | ((FiniteInf (v1, b1), Finite (v2, b2, v35, b35)) | (Finite (v2, b2, v35,
+ b35), FiniteInf (v1, b1))) ->
+ (let (v42, b42) = max_bound_inf v1 b1 v2 b2 in mk_finite v42 b42 v35 b35)
+ | (Finite (v1,
+ b1,
+ v1',
+ b1'),
+ Finite (v2,
+ b2,
+ v2',
+ b2')) ->
+ (let (v35, b35) = max_bound_inf v1 b1 v2 b2 in
+ let (v43,
+ b43) =
+ min_bound_sup v1' b1' v2' b2' in
+ mk_finite v35 b35 v43 b43)
+
+let zero = singleton (Q.of_bigint Z.zero)
+
+let reals = Inf
+
+let is_reals (e: t') : bool =
+ match e with
+ | Inf -> true
+ | InfFinite (v, _) -> false
+ | FiniteInf (v, _) -> false
+ | Finite (v, _, _, _) -> false
+
+let choose (e: t') : Q.t =
+ match e with
+ | Inf -> (Q.of_bigint Z.zero)
+ | (InfFinite (v,
+ Interval__Bound.Large) | (FiniteInf (v,
+ Interval__Bound.Large) | (Finite (v,
+ Interval__Bound.Large,
+ _, _) | Finite (_,
+ _, v,
+ Interval__Bound.Large)))) ->
+ v
+ | InfFinite (v, Interval__Bound.Strict) -> (Q.(-) v (Q.of_bigint Z.one))
+ | FiniteInf (v, Interval__Bound.Strict) -> (Q.(+) v (Q.of_bigint Z.one))
+ | Finite (v1,
+ Interval__Bound.Strict,
+ v2,
+ Interval__Bound.Strict) ->
+ (let half = (Q.make Z.one (Z.of_string "2")) in
+ (Q.(+) (Q.( * ) v1 half) (Q.( * ) v2 half)))
+
+type split_heuristic =
+ | Singleton of Q.t
+ | Splitted of t' * t'
+ | NotSplitted
+
+let split_heuristic (c: t') : split_heuristic =
+ let qzero = (Q.of_bigint Z.zero) in
+ let zero = singleton qzero in
+ match c with
+ | Inf ->
+ Splitted (InfFinite (qzero, Interval__Bound.Strict),
+ FiniteInf (qzero, Interval__Bound.Large))
+ | InfFinite (v,
+ b) ->
+ begin match ((Q_extra.compare qzero v), b) with
+ | (Ord.Eq,
+ Interval__Bound.Large) ->
+ Splitted (InfFinite (qzero, Interval__Bound.Strict), zero)
+ | ((Ord.Eq, Interval__Bound.Strict) | (Ord.Gt, _)) -> NotSplitted
+ | (Ord.Lt,
+ _) ->
+ Splitted (InfFinite (qzero, Interval__Bound.Strict),
+ Finite (qzero, Interval__Bound.Large, v, b))
+ end
+ | FiniteInf (v,
+ b) ->
+ begin match ((Q_extra.compare v qzero), b) with
+ | (Ord.Eq,
+ Interval__Bound.Large) ->
+ Splitted (zero, FiniteInf (v, Interval__Bound.Strict))
+ | ((Ord.Eq, Interval__Bound.Strict) | (Ord.Gt, _)) -> NotSplitted
+ | (Ord.Lt,
+ _) ->
+ Splitted (Finite (v, b, qzero, Interval__Bound.Strict),
+ FiniteInf (qzero, Interval__Bound.Large))
+ end
+ | Finite (v1,
+ b1,
+ v2,
+ b2) ->
+ begin
+ match
+ ((Q_extra.compare v1 qzero), b1, (Q_extra.compare v2 qzero), b2,
+ (Q_extra.compare v1 v2))
+ with
+ | (_, _, _, _, Ord.Eq) -> Singleton v1
+ | (Ord.Eq,
+ Interval__Bound.Large,
+ _,
+ _,
+ _) ->
+ Splitted (zero, Finite (qzero, Interval__Bound.Strict, v2, b2))
+ | (_,
+ _,
+ Ord.Eq,
+ Interval__Bound.Large,
+ _) ->
+ Splitted (Finite (v1, b1, qzero, Interval__Bound.Strict), zero)
+ | _ ->
+ (let half = (Q.make Z.one (Z.of_string "2")) in
+ let m = (Q.(+) (Q.( * ) half v1) (Q.( * ) half v2)) in
+ Splitted (Finite (v1, b1, m, Interval__Bound.Strict),
+ Finite (m, Interval__Bound.Large, v2, b2)))
+ end
+
diff --git a/src_common/modulo.mlw b/src_common/modulo.mlw
index 5721f2dc0fa9259b9abf5dc72f42046bee24725c..db985774f228684e802e363e60f19cfc98c5bbdb 100644
--- a/src_common/modulo.mlw
+++ b/src_common/modulo.mlw
@@ -29,22 +29,14 @@ module Divisible
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 { 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 }
+ raises { FinitePositiveExpected -> not (0. <. Q.real m ) }
ensures { Q.( r <= a) }
- ensures { a.Q.is_real -> r.Q.is_real }
- ensures { a.Q.is_real -> Q.(0. <=. (a.real -. r.real) <. m.real) }
- ensures { a.Q.is_real -> Q.( r.real <. a.real) -> forall q. not Q.(r.real <. (from_int q) *. m.real <=. a.real ) }
+ ensures { Q.(0. <=. (a.real -. r.real) <. m.real) }
+ ensures { 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 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
- | Q.NZERO ->
+ if Q.(m <= (Q.of_int 0)) then raise FinitePositiveExpected;
+ if Q.(a = (Q.of_int 0)) then a
+ else begin
round_modulo pure { a.Q.real } pure { m.Q.real };
(** it is surely possible to improve this computation *)
let r = Q.(of_int (floor (a / m)) * m) in
@@ -52,17 +44,12 @@ module Divisible
end
let round_up_to (a:Q.t) (m:Q.t) : (r:Q.t)
- requires { Q.not_NaN a } requires { Q.not_NaN 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 }
+ raises { FinitePositiveExpected -> not (0. <. Q.real m) }
ensures { Q.(a <= r) }
- ensures { a.Q.is_real -> r.Q.is_real }
- ensures { a.Q.is_real -> Q.(0. <=. (r.real -. a.real) <. m.real) }
- ensures { a.Q.is_real -> Q.( r.real <. a.real) -> forall q. not Q.(a.real <=. (from_int q) *. m.real <. r.real ) }
+ ensures { Q.(0. <=. (r.real -. a.real) <. m.real) }
+ ensures { Q.( r.real <. a.real) -> forall q. not Q.(a.real <=. (from_int q) *. m.real <. r.real ) }
=
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)
@@ -84,7 +71,7 @@ module Divisible
()
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 { 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 }
@@ -104,7 +91,6 @@ module Divisible
(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) }
@@ -123,7 +109,7 @@ module Divisible
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. }
+ 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
@@ -151,8 +137,6 @@ module Divisible
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
@@ -165,10 +149,9 @@ module Divisible
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 } =
+ requires { a.Q.real <> 0. } requires { b.Q.real <> 0. }
+ ensures { forall r. ddivisible r.Q.real a.Q.real -> ddivisible r.Q.real u.Q.real }
+ ensures { forall r. 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 };
@@ -178,7 +161,6 @@ module Divisible
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
@@ -191,7 +173,6 @@ module Divisible
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
@@ -207,14 +188,12 @@ module Divisible
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 } =
+ requires { 0. <> a.Q.real } requires { 0. <> b.Q.real }
+ ensures { forall r. 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 } =
diff --git a/src_common/modulo/why3session.xml b/src_common/modulo/why3session.xml
index 06503a0cc92046c3f0fb824602ce501787574a8e..7fb72ce5f8e891c640c403c63aa3721d11f2aad1 100644
--- a/src_common/modulo/why3session.xml
+++ b/src_common/modulo/why3session.xml
@@ -12,157 +12,100 @@
<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.04" steps="4325"/></proof>
+ <proof prover="2"><result status="valid" time="0.04" steps="2577"/></proof>
</goal>
<goal name="round_modulo'vc.1" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.04" steps="4971"/></proof>
+ <proof prover="2"><result status="valid" time="0.04" steps="3138"/></proof>
</goal>
<goal name="round_modulo'vc.2" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="4407"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="2659"/></proof>
</goal>
<goal name="round_modulo'vc.3" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="4438"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="2690"/></proof>
</goal>
<goal name="round_modulo'vc.4" expl="assertion" proved="true">
<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>
+ <proof prover="0"><result status="valid" time="0.68" steps="2340433"/></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>
+ <proof prover="0"><result status="valid" time="0.00" steps="8464"/></proof>
</goal>
</transf>
</goal>
<goal name="round_modulo'vc.5" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4533"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="2785"/></proof>
</goal>
<goal name="round_modulo'vc.6" expl="assertion" proved="true">
<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>
+ <proof prover="0"><result status="valid" time="0.03" steps="8681"/></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>
+ <proof prover="0"><result status="valid" time="0.01" steps="8660"/></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>
+ <proof prover="2"><result status="valid" time="0.03" steps="2849"/></proof>
</goal>
<goal name="round_modulo'vc.8" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4635"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="2887"/></proof>
</goal>
<goal name="round_modulo'vc.9" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="4639"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="2891"/></proof>
</goal>
<goal name="round_modulo'vc.10" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="37531"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="30206"/></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="4642"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="7283"/></proof>
</goal>
- <goal name="round_down_to'vc.1" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="5592"/></proof>
+ <goal name="round_down_to'vc.1" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="10725"/></proof>
</goal>
- <goal name="round_down_to'vc.2" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="5592"/></proof>
+ <goal name="round_down_to'vc.2" expl="precondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="3558"/></proof>
</goal>
- <goal name="round_down_to'vc.3" expl="exceptional postcondition" proved="true">
- <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.23" steps="72038"/></proof>
- </goal>
- <goal name="round_down_to'vc.5" expl="exceptional postcondition" proved="true">
- <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="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="4886"/></proof>
- </goal>
- <goal name="round_down_to'vc.8" expl="precondition" proved="true">
- <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.02" steps="5336"/></proof>
- </goal>
- <goal name="round_down_to'vc.10" expl="postcondition" proved="true">
- <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.04" steps="9052"/></proof>
- </goal>
- <goal name="round_down_to'vc.12" expl="postcondition" proved="true">
+ <goal name="round_down_to'vc.3" 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.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="5732"/></proof>
- </goal>
- <goal name="round_down_to'vc.12.2" expl="postcondition" proved="true">
- <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="0"><result status="valid" time="0.01" steps="18490"/></proof>
- </goal>
- <goal name="round_down_to'vc.12.4" expl="postcondition" proved="true">
+ <goal name="round_down_to'vc.3.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="round_down_to'vc.12.4.0" expl="postcondition" proved="true">
- <proof prover="0" timelimit="5"><result status="valid" time="0.02" steps="29698"/></proof>
+ <goal name="round_down_to'vc.3.0.0" expl="postcondition" proved="true">
+ <proof prover="0" timelimit="5"><result status="valid" time="0.02" steps="5029"/></proof>
</goal>
</transf>
</goal>
+ <goal name="round_down_to'vc.3.1" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="80935"/></proof>
+ </goal>
</transf>
</goal>
- <goal name="round_down_to'vc.13" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="8170"/></proof>
- </goal>
- <goal name="round_down_to'vc.14" expl="postcondition" proved="true">
+ <goal name="round_down_to'vc.4" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="round_down_to'vc.14.0" expl="postcondition" proved="true">
+ <goal name="round_down_to'vc.4.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="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="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="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="4816"/></proof>
+ <goal name="round_down_to'vc.4.0.0" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="2957"/></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="28336"/></proof>
+ <goal name="round_down_to'vc.4.0.1" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="15052"/></proof>
</goal>
</transf>
</goal>
- <goal name="round_down_to'vc.14.1" expl="postcondition" proved="true">
+ <goal name="round_down_to'vc.4.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="5971"/></proof>
+ <goal name="round_down_to'vc.4.1.0" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.05" steps="12398"/></proof>
</goal>
- <goal name="round_down_to'vc.14.1.1" expl="postcondition" proved="true">
- <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.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.23" steps="72151"/></proof>
- </goal>
- <goal name="round_down_to'vc.14.1.4" expl="postcondition" proved="true">
+ <goal name="round_down_to'vc.4.1.1" 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="28455"/></proof>
+ <goal name="round_down_to'vc.4.1.1.0" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="81315"/></proof>
</goal>
</transf>
</goal>
@@ -170,24 +113,15 @@
</goal>
</transf>
</goal>
- <goal name="round_down_to'vc.15" expl="postcondition" proved="true">
+ <goal name="round_down_to'vc.5" 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="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="4906"/></proof>
- </goal>
- <goal name="round_down_to'vc.15.2" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.04" steps="4912"/></proof>
+ <goal name="round_down_to'vc.5.0" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="3067"/></proof>
</goal>
- <goal name="round_down_to'vc.15.3" expl="postcondition" proved="true">
- <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">
+ <goal name="round_down_to'vc.5.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="round_down_to'vc.15.4.0" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.03" steps="82"/></proof>
+ <goal name="round_down_to'vc.5.1.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="52"/></proof>
</goal>
</transf>
</goal>
@@ -196,412 +130,341 @@
</transf>
</goal>
<goal name="round_up_to'vc" expl="VC for round_up_to" proved="true">
- <proof prover="2"><result status="valid" time="0.06" steps="17210"/></proof>
+ <proof prover="2"><result status="valid" time="0.06" steps="7767"/></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>
+ <proof prover="2"><result status="valid" time="0.02" steps="3339"/></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>
+ <proof prover="0"><result status="valid" time="0.01" steps="25451"/></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>
+ <proof prover="1"><result status="valid" time="0.01" steps="10"/></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>
+ <proof prover="1"><result status="valid" time="0.00" steps="10"/></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>
+ <proof prover="1"><result status="valid" time="0.05" steps="115"/></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>
+ <proof prover="2"><result status="valid" time="0.02" steps="3290"/></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>
+ <proof prover="0"><result status="valid" time="0.04" steps="11392"/></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>
+ <proof prover="2"><result status="valid" time="0.02" steps="3276"/></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>
+ <proof prover="1"><result status="valid" time="0.00" steps="14"/></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>
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></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>
+ <proof prover="1"><result status="valid" time="0.00" steps="16"/></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>
+ <proof prover="1"><result status="valid" time="0.00" steps="18"/></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>
+ <proof prover="1"><result status="valid" time="0.01" steps="20"/></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>
+ <proof prover="1"><result status="valid" time="0.01" steps="22"/></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>
+ <proof prover="1"><result status="valid" time="0.01" steps="22"/></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>
+ <proof prover="1"><result status="valid" time="0.05" steps="86"/></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>
+ <proof prover="1"><result status="valid" time="0.01" steps="24"/></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>
+ <proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="3369"/></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>
+ <proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="3372"/></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>
+ <proof prover="1"><result status="valid" time="0.01" steps="24"/></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>
+ <proof prover="2"><result status="valid" time="0.04" steps="12764"/></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>
+ <proof prover="0"><result status="valid" time="0.01" steps="17379"/></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>
+ <proof prover="1"><result status="valid" time="0.02" steps="14"/></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>
+ <proof prover="1"><result status="valid" time="0.03" steps="16"/></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>
+ <proof prover="1"><result status="valid" time="0.03" steps="16"/></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>
+ <proof prover="1"><result status="valid" time="0.01" steps="14"/></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>
+ <proof prover="1"><result status="valid" time="1.32" steps="182"/></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>
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></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>
+ <proof prover="0"><result status="valid" time="0.01" steps="17166"/></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>
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="divisible'vc.1" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="22"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="4518"/></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>
+ <proof prover="2"><result status="valid" time="0.02" steps="4523"/></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 name="divisible'vc.3" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
- <goal name="divisible'vc.8" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="6266"/></proof>
+ <goal name="divisible'vc.4" expl="unreachable point" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="5230"/></proof>
</goal>
- <goal name="divisible'vc.9" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="6269"/></proof>
+ <goal name="divisible'vc.5" expl="witness existence" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="5079"/></proof>
</goal>
- <goal name="divisible'vc.10" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="6270"/></proof>
+ <goal name="divisible'vc.6" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
- <goal name="divisible'vc.11" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="6275"/></proof>
+ <goal name="divisible'vc.7" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
- <goal name="divisible'vc.12" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="6322"/></proof>
+ <goal name="divisible'vc.8" expl="assertion" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="4498"/></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 name="divisible'vc.9" expl="unreachable point" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
- <goal name="divisible'vc.14" expl="postcondition" proved="true">
+ <goal name="divisible'vc.10" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="divisible'vc.14.0" expl="postcondition" proved="true">
+ <goal name="divisible'vc.10.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 name="divisible'vc.10.0.0" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="18"/></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 name="divisible'vc.10.0.1" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.02" steps="5216"/></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 name="divisible'vc.10.1" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="5131"/></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 name="divisible'vc.11" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.00" steps="20"/></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 name="mult_cst_divisible'vc.0" expl="witness existence" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="39"/></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 name="mult_cst_divisible'vc.1" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="12"/></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 name="mult_cst_divisible'vc.2" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="53"/></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>
+ <proof prover="1"><result status="valid" time="0.02" steps="10"/></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>
+ <proof prover="2"><result status="valid" time="0.03" steps="13363"/></proof>
</goal>
<goal name="union_divisible'vc.1" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.45" steps="144831"/></proof>
+ <proof prover="2"><result status="valid" time="0.04" steps="21085"/></proof>
</goal>
<goal name="union_divisible'vc.2" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="union_divisible'vc.3" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="30"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="union_divisible'vc.4" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="32"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="union_divisible'vc.5" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="71"/></proof>
+ <proof prover="1"><result status="valid" time="0.02" steps="67"/></proof>
</goal>
<goal name="union_divisible'vc.6" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="36"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="union_divisible'vc.7" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="7017"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="5193"/></proof>
</goal>
<goal name="union_divisible'vc.8" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="36"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="32"/></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>
+ <proof prover="1"><result status="valid" time="0.08" steps="85"/></proof>
</goal>
<goal name="union_divisible'vc.10" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.00" steps="48"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="5255"/></proof>
</goal>
<goal name="union_divisible'vc.11" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02" steps="7103"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="5260"/></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 name="union_divisible'vc.12" expl="assertion" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="5313"/></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 name="union_divisible'vc.13" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="48"/></proof>
</goal>
<goal name="union_divisible'vc.14" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.03" steps="7156"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
</goal>
<goal name="union_divisible'vc.15" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="56"/></proof>
+ <proof prover="1"><result status="valid" time="0.02" steps="50"/></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 name="union_divisible'vc.16" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="50"/></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 name="union_divisible'vc.17" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="51"/></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 name="union_divisible'vc.18" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="52"/></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 name="union_divisible'vc.19" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.75" steps="144"/></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 name="union_divisible'vc.20" expl="witness existence" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="85"/></proof>
</goal>
<goal name="union_divisible'vc.21" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.03" steps="59"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="40"/></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 name="union_divisible'vc.22" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="40"/></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 name="union_divisible'vc.23" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="46"/></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 name="union_divisible'vc.24" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="48"/></proof>
</goal>
- <goal name="union_divisible'vc.25" expl="precondition" proved="true">
+ <goal name="union_divisible'vc.25" expl="assertion" 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 name="union_divisible'vc.26" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="50"/></proof>
</goal>
<goal name="union_divisible'vc.27" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="50"/></proof>
</goal>
<goal name="union_divisible'vc.28" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="48"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="51"/></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>
+ <proof prover="1"><result status="valid" time="0.01" steps="52"/></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 name="union_divisible'vc.30" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="6733"/></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 name="union_divisible'vc.31" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="42"/></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 name="union_divisible'vc.32" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="6351"/></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>
+ <proof prover="1"><result status="valid" time="0.02" steps="52"/></proof>
</goal>
<goal name="inter_divisible'vc.1" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="60"/></proof>
+ <proof prover="1"><result status="valid" time="0.02" steps="54"/></proof>
</goal>
<goal name="inter_divisible'vc.2" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="inter_divisible'vc.3" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="32786"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="28139"/></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>
+ <proof prover="1"><result status="valid" time="0.04" steps="82"/></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>
+ <proof prover="1"><result status="valid" time="0.03" steps="94"/></proof>
</goal>
<goal name="inter_divisible'vc.6" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.02" steps="42"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="34"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="5235"/></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>
+ <proof prover="1"><result status="valid" time="0.02" steps="34"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="5243"/></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>
+ <proof prover="1"><result status="valid" time="0.01" steps="40"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="5291"/></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>
+ <proof prover="1"><result status="valid" time="0.02" steps="40"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="5299"/></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 name="inter_divisible'vc.11" expl="precondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.02" steps="50"/></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 name="inter_divisible'vc.12" expl="postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.03" steps="6481"/></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 name="inter_divisible'vc.13" expl="postcondition" proved="true">
+ <proof prover="1"><result status="valid" time="0.03" steps="34"/></proof>
+ <proof prover="2"><result status="valid" time="0.03" steps="6188"/></proof>
</goal>
</transf>
</goal>
diff --git a/src_common/modulo__Divisible.ml b/src_common/modulo__Divisible.ml
index 55b55551601c15fba14444f668212913bff046d1..514c15a4b67065eb36a09fa4dd4cae6e1b4b218b 100644
--- a/src_common/modulo__Divisible.ml
+++ b/src_common/modulo__Divisible.ml
@@ -1,14 +1,10 @@
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)
+ if (Q.(<=) m (Q.of_bigint Z.zero)) then raise FinitePositiveExpected;
+ if (Q.equal a (Q.of_bigint Z.zero))
+ then a
+ else (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
diff --git a/src_common/ord.ml b/src_common/ord.ml
new file mode 100644
index 0000000000000000000000000000000000000000..49f954b3d91582cbe37bd514e460f9d92822f2d9
--- /dev/null
+++ b/src_common/ord.ml
@@ -0,0 +1,4 @@
+type t =
+ | Eq
+ | Lt
+ | Gt
diff --git a/src_common/q.mlw b/src_common/q.mlw
index c19c1afba43bb732e515166800c60d4ed73c86e8..a833a43bf528a2b84a74d82059764be2d3c14fa8 100644
--- a/src_common/q.mlw
+++ b/src_common/q.mlw
@@ -1,3 +1,12 @@
+module Ord
+
+ type t =
+ | Eq
+ | Lt
+ | Gt
+
+end
+
module Z
use int.Int
@@ -44,6 +53,8 @@ module Z
predicate prime_to_one_another (a b:int) (* = (gcd a b = 1) *)
+
+ axiom prime_to_one_another_refl: forall a:int. prime_to_one_another a a
val ghost prime_to_one_another_mul (a m b n: int) : (q:int)
requires { prime_to_one_another a b }
@@ -61,7 +72,7 @@ module Z
end
-module Q
+module QWithInf
use real.RealInfix
use int.Int
@@ -146,6 +157,10 @@ module Q
requires { not_NaN a /\ not_NaN b }
ensures { result = (a <= b) }
+ val (<) (a:t) (b:t) : bool
+ requires { not_NaN a /\ not_NaN b }
+ ensures { result = (a < b) }
+
val (+) (a b:t) : t
requires { not_NaN a /\ not_NaN b }
ensures { match a.value, b.value with
@@ -258,3 +273,107 @@ module Q
end
+
+module Q
+
+ use real.RealInfix
+ use int.Int
+ use real.FromInt
+ use Z as Z
+
+
+ type t = private {
+ num: int;
+ den: int;
+ }
+ invariant { 0 < den }
+ invariant { Z.prime_to_one_another num den }
+ by { num = 1; den = 1 }
+
+
+ function real (q:t) : real = ((from_int q.num) /. (from_int q.den))
+
+ meta coercion function real
+
+ predicate equal (a b:t) = (a.real = b.real)
+
+ val (=) (a:t) (b:t) : bool
+ ensures { equal a b = result }
+
+ axiom equal_is_eq: forall a b. equal a b -> a = b
+
+ predicate (<=) (a:t) (b:t) = (a.real <=. b.real)
+ predicate (<) (a:t) (b:t) = (a.real <. b.real)
+
+ val (<=) (a:t) (b:t) : bool
+ ensures { result = (a <= b) }
+
+ val (<) (a:t) (b:t) : bool
+ ensures { result = (a < b) }
+
+ use Ord as Ord
+ val compare (a:t) (b:t) : Ord.t
+ ensures { match result with
+ | Ord.Eq -> equal a b
+ | Ord.Lt -> a < b
+ | Ord.Gt -> b < a
+ end
+ }
+
+ val function (+) (a b:t) : t
+ ensures { a.real +. b.real = result.real }
+
+ val function (-) (a b:t) : t
+ ensures { a.real -. b.real = result.real }
+
+ val function (*) (a b:t) : t
+ ensures { a.real *. b.real = result.real }
+
+ val function (/) (a b:t) : t
+ requires { b.real <> 0. }
+ ensures { a.real /. b.real = result.real }
+
+ function make (num den:int): t
+ axiom make_def:
+ forall num den: int. den <> 0 -> (make num den).real = (from_int num) /. (from_int den)
+
+ val make (num den: int): t
+ requires { den <> 0 }
+ ensures { result = make num den }
+
+ val make_exact (num den: int): t
+ requires { den <> 0 } requires { Z.prime_to_one_another num den }
+ ensures { result.num = num }
+ ensures { result.den = den }
+
+ use real.Truncate
+
+ val to_int (a:t) : int
+ ensures { result = truncate a.real }
+
+ val of_int (a:int) : t
+ ensures { result.real = from_int a }
+
+ let floor (a:t) : int
+ ensures { result = floor a.real } =
+ 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
+ ensures { result = ceil a.real } =
+ 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 6d000bfc6c449ef54d6b015aad1395359057ae71..5fc416f38693c3f478c30e202ea7bcd87b96caa2 100644
--- a/src_common/q/why3session.xml
+++ b/src_common/q/why3session.xml
@@ -7,37 +7,37 @@
<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">
+<theory name="QWithInf" proved="true">
<goal name="t'vc" expl="VC for t" proved="true">
- <proof prover="0"><result status="valid" time="0.04" steps="17812"/></proof>
+ <proof prover="0"><result status="valid" time="0.04" steps="17867"/></proof>
</goal>
<goal name="floor'vc" expl="VC for floor" proved="true">
<transf name="split_vc" proved="true" >
<goal name="floor'vc.0" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.03" steps="4863"/></proof>
+ <proof prover="0"><result status="valid" time="0.03" steps="5232"/></proof>
</goal>
<goal name="floor'vc.1" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="4386"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="4693"/></proof>
</goal>
<goal name="floor'vc.2" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.15" steps="51614"/></proof>
+ <proof prover="0"><result status="valid" time="0.15" steps="52166"/></proof>
</goal>
<goal name="floor'vc.3" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="4450"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="4757"/></proof>
</goal>
<goal name="floor'vc.4" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="4501"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="4808"/></proof>
</goal>
<goal name="floor'vc.5" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="19745"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="20883"/></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>
+ <proof prover="1"><result status="valid" time="0.06" steps="235283"/></proof>
</goal>
<goal name="floor'vc.6.1" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.14" steps="372"/></proof>
+ <proof prover="2"><result status="valid" time="0.14" steps="371"/></proof>
</goal>
</transf>
</goal>
@@ -49,28 +49,96 @@
<goal name="ceil'vc" expl="VC for ceil" proved="true">
<transf name="split_vc" proved="true" >
<goal name="ceil'vc.0" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.03" steps="4880"/></proof>
+ <proof prover="0"><result status="valid" time="0.03" steps="5249"/></proof>
+ </goal>
+ <goal name="ceil'vc.1" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.03" steps="4703"/></proof>
+ </goal>
+ <goal name="ceil'vc.2" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.07" steps="52180"/></proof>
+ </goal>
+ <goal name="ceil'vc.3" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="4799"/></proof>
+ </goal>
+ <goal name="ceil'vc.4" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="4850"/></proof>
+ </goal>
+ <goal name="ceil'vc.5" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="20811"/></proof>
+ </goal>
+ <goal name="ceil'vc.6" expl="assertion" proved="true">
+ <proof prover="2"><result status="valid" time="0.15" steps="501"/></proof>
+ </goal>
+ <goal name="ceil'vc.7" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="6014"/></proof>
+ </goal>
+ </transf>
+ </goal>
+</theory>
+<theory name="Q" proved="true">
+ <goal name="t'vc" expl="VC for t" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="t'vc.0" expl="type invariant" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="2245"/></proof>
+ </goal>
+ <goal name="t'vc.1" expl="type invariant" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="2557"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="floor'vc" expl="VC for floor" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="floor'vc.0" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="3021"/></proof>
+ </goal>
+ <goal name="floor'vc.1" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="2630"/></proof>
+ </goal>
+ <goal name="floor'vc.2" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="4830"/></proof>
+ </goal>
+ <goal name="floor'vc.3" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="2694"/></proof>
+ </goal>
+ <goal name="floor'vc.4" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="2745"/></proof>
+ </goal>
+ <goal name="floor'vc.5" expl="assertion" proved="true">
+ <proof prover="1"><result status="valid" time="0.01" steps="13265"/></proof>
+ </goal>
+ <goal name="floor'vc.6" expl="assertion" proved="true">
+ <proof prover="2"><result status="valid" time="0.10" steps="506"/></proof>
+ </goal>
+ <goal name="floor'vc.7" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.02" steps="3708"/></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="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.01" steps="3038"/></proof>
</goal>
<goal name="ceil'vc.1" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.03" steps="4396"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="2640"/></proof>
</goal>
<goal name="ceil'vc.2" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.07" steps="51628"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="4844"/></proof>
</goal>
<goal name="ceil'vc.3" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="4492"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="2736"/></proof>
</goal>
<goal name="ceil'vc.4" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="4543"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="2787"/></proof>
</goal>
<goal name="ceil'vc.5" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="19673"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="13192"/></proof>
</goal>
<goal name="ceil'vc.6" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.15" steps="512"/></proof>
+ <proof prover="2"><result status="valid" time="0.11" steps="497"/></proof>
</goal>
<goal name="ceil'vc.7" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="5645"/></proof>
+ <proof prover="0"><result status="valid" time="0.01" steps="3718"/></proof>
</goal>
</transf>
</goal>
diff --git a/src_common/q__Q.ml b/src_common/q__Q.ml
index f134cf4a7a4d473d0e1c05228d71a474f1161575..681a7ad987545cbf5bcb1d1d22d9e53328fb65fe 100644
--- a/src_common/q__Q.ml
+++ b/src_common/q__Q.ml
@@ -1,16 +1,3 @@
-type value =
- | MinusInf
- | PlusInf
- | NaN
- | Real
-
-type kind =
- | ZERO
- | NZERO
- | INF
- | MINF
- | UNDEF
-
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.Q.num) (a.Q.den))
diff --git a/src_common/q_extra.ml b/src_common/q_extra.ml
new file mode 100644
index 0000000000000000000000000000000000000000..250af5939872ecaf57befda7465f0586ed07cb1b
--- /dev/null
+++ b/src_common/q_extra.ml
@@ -0,0 +1,8 @@
+open Ord
+
+let compare a b =
+ let c = compare a b in
+ if c = 0 then Eq
+ else if c <= 0
+ then Lt
+ else Gt