Implement with error in OCaml ConvexeWithDivider

src_colibri2/stdlib/std.ml

@@ -76,7 +76,7 @@ module Q = struct
   let two = Q.of_int 2
   let ge = Q.geq
   let le = Q.leq
-    
+
   let of_string_decimal =
     let decimal = Str.regexp "\\(+\\|-\\)?\\([0-9]+\\)\\([.]\\([0-9]*\\)\\)?" in
     fun s ->

src_colibri2/stdlib/std.mli

@@ -51,7 +51,7 @@ module Goption : sig
 end
 
 module Q : sig
-  include module type of Q
+  include module type of Q with type t = Q.t
   include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
   val two : t
   val ge  : t -> t -> bool

src_colibri2/theories/LRA/dune

@@ -5,7 +5,8 @@
  (libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
    colibri2.core.structures colibri2.core colibri2.theories.bool)
  (preprocess
-  (pps ppx_deriving.std))
+  (pps ppx_deriving.std ppx_hash
+ ))
  (flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
    Containers -open Colibri2_stdlib -open Std -open Colibri2_core -open
    Colibri2_theories_bool)

src_colibri2/theories/LRA/interval.ml

@@ -352,6 +352,187 @@ module Convexe = struct
 
 end
 
+module ConvexeWithDivider = struct
+
+  (** modulo = 0 -> no modulo *)
+  type t = { c: Convexe.t; divider: Q.t }
+  [@@ deriving eq, ord, hash]
+
+  let pp fmt t =
+    Format.fprintf fmt "%a%t"
+      Convexe.pp t.c
+      (fun fmt ->
+        if not (Q.equal t.divider Q.zero)
+        then Format.fprintf fmt "%%%a" Q.pp t.divider
+      )
+
+
+  include Popop_stdlib.MkDatatype(struct
+      type nonrec t = t
+      let equal = equal let compare = compare
+      let hash = hash let pp = pp
+    end)
+
+  let invariant e =
+    Convexe.invariant e.c &&
+    match Q.classify e.divider with
+    | Q.ZERO -> true
+    | Q.NZERO ->
+      let large_finite_bound b v inf =
+        match b with
+        | Strict -> Q.equal v inf
+        | Large -> true
+      in
+      large_finite_bound e.c.minb e.c.minv Q.minus_inf &&
+      large_finite_bound e.c.maxb e.c.maxv Q.inf
+    | Q.INF | Q.MINF | Q.UNDEF -> false
+
+  let tighten_bounds e =
+    if Q.equal e.divider Q.zero then Some e
+    else
+      let round ~add ~divisible_up_to ~minus_inf ~minv ~minb =
+        if Q.equal minv minus_inf
+        then minb, minv
+        else
+          let minv' = divisible_up_to minv e.divider in
+          Large, begin match minb with
+          | Strict when Q.equal minv' minv -> add minv e.divider
+          | _ -> minv'
+          end
+      in
+      let minb,minv =
+        round ~add:Q.add ~divisible_up_to:Colibrics_lib.Q.divisible_up_to
+          ~minus_inf:Q.minus_inf ~minv:e.c.Convexe.minv ~minb:e.c.Convexe.minb
+      in
+      let maxb,maxv =
+        round ~add:Q.sub ~divisible_up_to:Colibrics_lib.Q.divisible_down_to
+          ~minus_inf:Q.inf ~minv:e.c.Convexe.maxv ~minb:e.c.Convexe.maxb
+      in
+      if Q.lt maxv minv
+      then None
+      else Some { c = { minv; minb; maxv; maxb }; divider = e.divider }
+
+  let is_singleton e = Convexe.is_singleton e.c
+
+  let singleton s = { c = Convexe.singleton s; divider = s }
+
+  let except e x =
+    (Convexe.except e.c x)
+    |> Opt.map (fun c -> { e with c })
+    |> function
+    | None -> None
+    | Some s -> tighten_bounds s
+
+  let lower_min_max e1 e2 = Convexe.lower_min_max e1.c e2.c
+
+  let bigger_min_max e1 e2 = Convexe.bigger_min_max e1.c e2.c
+
+  let is_comparable e1 e2 = Convexe.is_comparable e1.c e2.c
+
+  let is_distinct e1 e2 = Convexe.is_distinct e1.c e2.c
+
+  let divisible q d =
+    Q.equal d Q.zero ||
+    Colibrics_lib.Q.divisible q d
+
+  let is_included e1 e2 =
+    Convexe.is_included e1.c e2.c &&
+    begin
+      Q.equal e2.divider Q.zero ||
+      (not (Q.equal e1.divider Q.zero) &&
+       divisible e1.divider e2.divider
+      )
+    end
+
+  let mem x e = Convexe.mem x e.c && begin
+      divisible x e.divider
+      end
+
+  let mult_cst q e =
+    assert (Q.is_real q);
+    { c = Convexe.mult_cst q e.c;
+      divider = Q.abs (Colibrics_lib.Q.mult_cst_divisible e.divider q) }
+
+  let add_cst q e =
+    if Q.equal q Q.zero then e
+    else
+      let divider = Colibrics_lib.Q.union_divisible q e.divider in
+      { c = Convexe.add_cst q e.c; divider }
+
+  let add e1 e2 =
+    { c = Convexe.add e1.c e2.c;
+      divider = Colibrics_lib.Q.union_divisible e1.divider e2.divider }
+
+  let minus e1 e2 =
+    { c = Convexe.minus e1.c e2.c;
+      divider = Colibrics_lib.Q.union_divisible e1.divider e2.divider }
+
+  let div_unknown c = { c; divider = Q.zero }
+
+  let gt q = div_unknown (Convexe.gt q)
+
+  let ge q = div_unknown (Convexe.ge q)
+
+  let lt q = div_unknown (Convexe.lt q)
+
+  let le q = div_unknown (Convexe.le q)
+
+  let union e1 e2 =
+    { c = Convexe.union e1.c e2.c;
+      divider = Colibrics_lib.Q.union_divisible e1.divider e2.divider }
+
+  let inter e1 e2 =
+    match Convexe.inter e1.c e2.c with
+    | None -> None
+    | Some c ->
+      tighten_bounds
+        { c; divider = Colibrics_lib.Q.inter_divisible e1.divider e2.divider }
+
+  (** intersection set.
+      if the two arguments are equals, return the second
+  *)
+
+  let zero = div_unknown Convexe.zero
+  let reals = div_unknown Convexe.reals
+  let () = assert (invariant reals)
+
+  let is_reals e = Convexe.is_reals e.c && Q.equal e.divider Q.zero
+
+  let choose e =
+    let q = Convexe.choose e.c in
+    if Q.equal e.divider Q.zero
+    then q
+    else Colibrics_lib.Q.divisible_down_to q e.divider
+
+  let split_heuristic e =
+    let rec aux divider c  =
+      match Convexe.split_heuristic c with
+      | `Singleton c -> `Singleton c
+      | `NotSplitted -> `NotSplitted
+      | `Splitted (a,b) ->
+        match tighten_bounds { c = a; divider },
+              tighten_bounds { c = b; divider } with
+        | Some a, Some b -> `Splitted (a,b)
+        | None, None -> assert false
+        | None, Some a -> aux divider a.c
+        | Some a, None -> aux divider a.c
+    in
+    aux e.divider e.c
+
+  let nb_incr = 100
+  let z_nb_incr = Z.of_int nb_incr
+  let choose_rnd _ = assert false
+
+  let get_convexe_hull e = Convexe.get_convexe_hull e.c
+
+  let is_Large = function
+    | Large -> true
+    | Strict -> false
+
+  let divided_by divider = { c = Convexe.reals; divider }
+
+end
+
 module ConvexeWithExceptions = struct
 
   type t = {con: Convexe.t; exc: Q.S.t}

src_colibri2/theories/LRA/interval.mli

@@ -38,6 +38,16 @@ module Convexe: sig
   val inter_with_integer: t -> t option
 end
 
+module ConvexeWithDivider: sig
+  include Interval_sig.S
+  val split_heuristic: t ->
+    [ `Singleton of Q.t
+    | `Splitted of t * t
+    | `NotSplitted ]
+
+  val divided_by: Q.t -> t
+end
+
 module ConvexeWithExceptions: Interval_sig.S
 
 module Union : Interval_sig.S

src_common/colibrics_lib.ml

@@ -2,7 +2,32 @@ module Q = struct
   (** Add some useful function to Q of zarith *)
 
   let floor = Q__Q.floor
+  (** [floor a] return the greatest integer smaller or equal than [a] *)
+
   let ceil = Q__Q.ceil
-  let modulo_down_to = Modulo__Modulo.round_down_to
-  let modulo_up_to = Modulo__Modulo.round_up_to
+  (** [ceil a] return the smallest integer greater or equal than [a] *)
+
+  let divisible_down_to = Modulo__Divisible.round_down_to
+  (** [divisible_down_to a m] return the greatest multiple of [m] smaller or equal
+      than [a] *)
+
+  let divisible_up_to = Modulo__Divisible.round_up_to
+  (** [divisible_down_to a m] return the smallest multiple of [m] greater or equal
+      than [a] *)
+
+  let divisible = Modulo__Divisible.divisible
+  (** [divisible a b] test if a is divisible by b *)
+
+  let mult_cst_divisible = Modulo__Divisible.mult_cst_divisible
+  (** [mult_cst_divisible a b] *)
+
+  let union_divisible a b =
+    if Q.equal a Q.zero || Q.equal b Q.zero then Q.zero
+    else Modulo__Divisible.union_divisible a b
+
+  let inter_divisible a b =
+    if Q.equal a Q.zero then b else
+    if Q.equal b Q.zero then a
+    else Modulo__Divisible.inter_divisible a b
+
 end

src_common/common.drv

@@ -2,6 +2,9 @@ module q.Q
 
    syntax type t "Q.t"
 
+   syntax val num "%1.Q.num"
+   syntax val den "%1.Q.den"
+
    syntax val ZERO "Q.ZERO"
    syntax val MINF "Q.MINF"
    syntax val INF "Q.INF"
@@ -17,11 +20,17 @@ module q.Q
    syntax val to_int "Q.to_bigint %1"
    syntax val of_int "Q.of_bigint %1"
    syntax val (=) "Q.equal %1 %2"
+   syntax val make "Q.make %1 %2"
+   syntax val make_exact "{ Q.num = %1; Q.den = %2 }"
 end
 
 module q.Z
 
    syntax val fdiv "Z.fdiv %1 %2"
    syntax val cdiv "Z.cdiv %1 %2"
+   syntax val divisible "Z.divisible %1 %2"
+
+   syntax val gcd "Z.gcd %1 %2"
+   syntax val lcm "Z.lcm %1 %2"
 
 end

src_common/dune

@@ -5,23 +5,52 @@
 )
 
 (rule
- (targets modulo__Modulo.ml q__Q.ml)
+ (targets modulo__Divisible.ml q__Q.ml)
  (deps q.mlw modulo.mlw)
- (action (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L . modulo.Modulo q.Q))
+ (action (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L . modulo.Divisible q.Q))
  (mode promote)
 )
 
+(rule
+ (alias runproof)
+ (deps (source_tree q) q.mlw)
+ (action (run why3 replay -L . q))
+)
+
 (rule
  (alias runproof)
  (deps (source_tree modulo) modulo.mlw q.mlw)
  (action (run why3 replay -L . modulo))
 )
 
+; (rule
+;  (alias runproof)
+;  (deps (source_tree modulo) interval.mlw modulo.mlw q.mlw)
+;  (action (run why3 replay -L . interval))
+; )
+
+; (rule
+;  (alias ide:q)
+;  (deps (universe) q.mlw)
+;  (action (run why3 ide -L . q.mlw))
+; )
+
+; (rule
+;  (alias ide:modulo)
+;  (deps (universe) q.mlw modulo.mlw)
+;  (action (run why3 ide -L . modulo.mlw))
+; )
+
+; (rule
+;  (alias ide:interval)
+;  (deps (universe) q.mlw modulo.mlw interval.mlw)
+;  (action (run why3 ide -L . interval.mlw))
+; )
 
 (rule
- (alias runproof)
+ (alias runsmokedetector)
  (deps (source_tree q) q.mlw)
- (action (run why3 replay -L . q))
+ (action (run why3 replay -L . q --smoke-detector deep))
 )
 
 (rule
@@ -30,9 +59,8 @@
  (action (run why3 replay -L . modulo --smoke-detector deep))
 )
 
-
 (rule
  (alias runsmokedetector)
- (deps (source_tree q) q.mlw)
- (action (run why3 replay -L . q --smoke-detector deep))
+ (deps (source_tree modulo) interval.mlw modulo.mlw q.mlw)
+ (action (run why3 replay -L . interval --smoke-detector deep))
 )

src_common/interval.mlw

+module Bound
+     type t = Strict | Large
+
+     (* let compare_inf b1 b2 = match b1,b2 with *)
+     (*   | Large, Strict -> -1 *)
+     (*   | Strict, Large -> 1 *)
+     (*   | Large, Large | Strict, Strict -> 0 *)
+
+     (* let compare_inf_sup b1 b2 = match b1,b2 with *)
+     (*   | Large, Strict -> 1 *)
+     (*   | Strict, Large -> 1 *)
+     (*   | Large, Large -> 0 *)
+     (*   | Strict, Strict -> 1 *)
+
+     (* let compare_sup b1 b2 = - (compare_inf b1 b2) *)
+
+end
+
+module Convexe
+  use option.Option
+  use q.Q as Q
+  use Bound as Bound
+
+  type t = { minb : Bound.t; minv: Q.t; maxv: Q.t; maxb: Bound.t }
+   invariant { not (Q.is_nan minv) }
+   invariant { not (Q.is_nan maxv) }
+   invariant { not (Q.is_plus_inf minv) }
+   invariant { not (Q.is_minus_inf maxv) }
+   invariant {
+     if Q.(equal minv maxv)
+     then minb = Bound.Large /\ maxb = Bound.Large
+     else Q.(minv < maxv)
+   }
+   by { minb = Bound.Large; minv = Q.of_int 0; maxv = Q.of_int 0; maxb = Bound.Large }
+
+   predicate mem (x:Q.t) (e:t) =
+    (match e.minb with
+     | Bound.Strict -> Q.(e.minv < x)
+     | Bound.Large  -> Q.(e.minv <= x)
+     end)
+    &&
+    (match e.maxb with
+     | Bound.Strict -> Q.(x < e.maxv)
+     | Bound.Large  -> Q.(x <= e.maxv)
+     end)
+
+  let is_singleton e
+      ensures { forall q. mem q e -> (forall q'. mem q' e -> Q.equal q q') -> result = Some q }
+      ensures { (exists q q'. not (Q.equal q q') /\ mem q e /\ mem q' e) -> result = None }
+  =
+    if Q.(e.minv = e.maxv) then Some e.minv else begin
+     ghost (if e.minb = Bound.Strict then begin assert { forall q. mem q e -> Q.(e.minv < q) }; assert { forall q. mem q e -> Q.(e.maxv < q) }; absurd end );
+     assert { e.minb = Bound.Large };
+     assert { e.maxb = Bound.Large };
+     None
+    end
+
+  let singleton q
+      ensures { mem q result }
+      ensures { forall q'. mem q' result -> Q.equal q q' }
+  =
+    {minb=Bound.Large; minv = q; maxv = q; maxb=Bound.Large}
+
+(*
+  let except e x =
+    let is_min = Q.equal e.minv x in
+    let is_max = Q.equal e.maxv x in
+    if is_min && is_max then None
+    else if is_min
+    then Some {e with minb=Strict}
+    else if Q.equal e.maxv x
+    then Some {e with maxb=Strict}
+    else Some e
+
+  let lower_min_max e1 e2 =
+    let c = Q.compare e1.minv e2.minv in
+    match e1.minb, e2.minb with
+    | Strict, Large when c =  0 -> e2,e1, false
+    | _             when c <= 0 -> e1,e2, true
+    | _                         -> e2,e1, false
+
+  let bigger_min_max e1 e2 =
+    let c = Q.compare e1.maxv e2.maxv in
+    match e1.maxb, e2.maxb with
+    | Strict, Large when c =  0 -> e1,e2, true
+    | _             when c >= 0 -> e2,e1, false
+    | _                         -> e1,e2, true
+
+
+  let is_comparable e1 e2 =
+    (** x1 in e1, x2 in e2 *)
+    (** order by the minimum *)
+    let emin,emax,same = lower_min_max e1 e2 in (** emin.minv <= emax.minv *)
+    (** look for inclusion *)
+    let c = Q.compare emin.maxv emax.minv in
+    match emin.maxb, emax.minb with
+    (** emin.minv <? e1 <? emin.maxv < emax.minv <? e2 <? emax.maxv *)
+    | _ when c <  0 -> if same then `Lt else `Gt
+    (** emin.minv <? e1 <  emin.maxv = emax.minv <  e2 <? emax.maxv *)
+    (** emin.minv <? e1 <  emin.maxv = emax.minv <= e2 <? emax.maxv *)
+    (** emin.minv <? e1 <= emin.maxv = emax.minv <  e2 <? emax.maxv *)
+    | Strict, Strict | Strict, Large | Large, Strict
+      when c = 0 ->
+      if same then `Lt else `Gt
+    | _ -> `Uncomparable
+
+  let is_distinct e1 e2 =
+    match is_comparable e1 e2 with
+    | `Uncomparable -> false
+    | _ -> true
+
+  let is_included e1 e2 =
+    assert (invariant e1);
+    assert (invariant e2);
+    compare_bounds_inf (e2.minv,e2.minb) (e1.minv,e1.minb) <= 0 &&
+    compare_bounds_sup (e1.maxv,e1.maxb) (e2.maxv,e2.maxb) <= 0
+
+  let mem x e =
+    (match e.minb with
+     | Strict -> Q.lt e.minv x
+     | Large  -> Q.le e.minv x)
+    &&
+    (match e.maxb with
+     | Strict -> Q.lt x e.maxv
+     | Large  -> Q.le x e.maxv)
+
+  let mult_pos q e =
+    {e with minv = Q.mul e.minv q; maxv = Q.mul e.maxv q}
+
+  let mult_neg q e =
+    { minb = e.maxb; maxb = e.minb;
+      minv = Q.mul e.maxv q;
+      maxv = Q.mul e.minv q }
+
+  let mult_cst q e =
+    assert (Q.is_real q);
+    let c = Q.sign q in
+    if c = 0      then singleton Q.zero
+    else if c > 0 then mult_pos q e
+    else               mult_neg q e
+
+  let add_cst q e =
+    {e with minv = Q.add e.minv q; maxv = Q.add e.maxv q}
+
+  let mult_bound b1 b2 =
+    match b1, b2 with
+    | Large , Large  -> Large
+    | _              -> Strict
+
+  let add e1 e2 =
+    let t = {minb = mult_bound e1.minb e2.minb;
+             minv = Q.add e1.minv e2.minv;
+             maxv = Q.add e1.maxv e2.maxv;
+             maxb = mult_bound e1.maxb e2.maxb} in
+    assert (invariant t); t
+
+  let minus e1 e2 =
+    add e1 (mult_neg Q.minus_one e2)
+
+  let gt q =
+    let t = {minb=Strict; minv = q; maxv = Q.inf; maxb= Strict} in
+    assert (invariant t); t
+
+  let ge q =
+    let t = {minb=Large; minv = q; maxv = Q.inf; maxb= Strict} in
+    assert (invariant t); t
+
+  let lt q =
+    let t = {minb=Strict; minv = Q.minus_inf; maxv = q; maxb= Strict} in
+    assert (invariant t); t
+
+  let le q =
+    let t = {minb=Strict; minv = Q.minus_inf; maxv = q; maxb= Large} in
+    assert (invariant t); t
+
+  let union e1 e2 =
+    let emin,_,_ = lower_min_max  e1 e2 in
+    let _,emax,_ = bigger_min_max e1 e2 in
+    {minb = emin.minb; minv = emin.minv;
+     maxv = emax.maxv; maxb = emax.maxb}
+
+  let inter e1 e2 =
+    let (minv,minb) as min =
+      if compare_bounds_inf (e1.minv,e1.minb) (e2.minv,e2.minb) < 0
+      then (e2.minv,e2.minb) else (e1.minv,e1.minb)
+    in
+    let (maxv,maxb) as max =
+      if compare_bounds_sup (e1.maxv,e1.maxb) (e2.maxv,e2.maxb) < 0
+      then (e1.maxv,e1.maxb) else (e2.maxv,e2.maxb)
+    in
+    if compare_bounds_inf_sup min max > 0
+    then None
+    else if Q.equal minv maxv && equal_bound minb Large && equal_bound maxb Large
+    then Some (singleton minv)
+    else Some {minv;minb;maxv;maxb}
+
+  let inter e1 e2 =
+    let r = inter e1 e2 in
+    assert (Opt.for_all invariant r);
+    r
+
+  (** intersection set.
+      if the two arguments are equals, return the second
+  *)
+
+  let zero = singleton Q.zero
+  let reals = {minb=Strict; minv=Q.minus_inf; maxb=Strict; maxv=Q.inf}
+  let () = assert (invariant reals)
+
+  let is_reals = function
+    | {minb=Strict; minv; maxb=Strict; maxv}
+      when Q.equal minv Q.minus_inf &&
+           Q.equal maxv Q.inf     -> true
+    | _ -> false
+
+  let choose = function
+    | {minb=Large;minv} -> minv
+    | {maxb=Large;maxv} -> maxv
+    | {minv;maxv} when Q.equal Q.minus_inf minv && Q.equal Q.inf maxv ->
+      Q.zero
+    | {minv;maxv} when Q.equal Q.minus_inf minv ->
+      Q.make (Z.sub (Q.to_bigint maxv) Z.one) Z.one
+    | {minv;maxv} when Q.equal Q.inf maxv ->
+      Q.make (Z.add (Q.to_bigint minv) Z.one) Z.one
+    | {minv;maxv} ->
+      let q = Q.make (Z.add Z.one (Q.to_bigint minv)) Z.one in
+      if Q.lt q maxv then q
+      else Q.add maxv (Q.div_2exp (Q.sub minv maxv) 1)
+
+  let split_heuristic c =
+    match is_singleton c with
+    | Some s -> `Singleton s
+    | None ->
+      let split_at mid =
+        let left,right =
+          if Q.equal mid c.maxv
+          then inter (lt mid) c, inter (ge mid) c
+          else inter (le mid) c, inter (gt mid) c
+        in
+        match left, right with
+        | Some left, Some right ->
+          `Splitted(left,right)
+        | _ -> assert false
+      in
+      if Q.equal Q.minus_inf c.minv || Q.equal Q.inf c.maxv then
+        if mem Q.zero c then split_at Q.zero
+        else `NotSplitted
+      else
+        let mid = Q.div_2exp (Q.add c.minv c.maxv) (-1) in
+        split_at mid
+
+  let nb_incr = 100
+  let z_nb_incr = Z.of_int nb_incr
+  let choose_rnd rnd = function
+    | {minv;maxv} when Q.equal Q.minus_inf minv ->
+      Q.make (Z.sub (Z.of_int (rnd nb_incr)) (Q.to_bigint maxv)) Z.one
+    | {minv;maxv} when Q.equal Q.inf maxv ->
+      Q.make (Z.add (Z.of_int (rnd nb_incr)) (Q.to_bigint minv)) Z.one
+    | {minv;maxv} when Q.equal minv maxv -> minv
+    | {minv;maxv} ->
+      let d = Q.sub maxv minv in
+      let i = 1 + rnd (nb_incr - 2) in
+      let x = Q.make (Z.of_int i) (Z.of_int 100) in
+      let q = Q.add minv (Q.mul x d) in
+      assert (Q.lt minv q);
+      assert (Q.lt q maxv);
+      q
+
+  let get_convexe_hull e =
+    let mk v b =
+      match Q.classify v with
+      | Q.ZERO | Q.NZERO -> Some (v,b)
+      | Q.INF | Q.MINF -> None
+      | Q.UNDEF -> assert false in
+    mk e.minv e.minb, mk e.maxv e.maxb
+
+  let is_Large = function
+    | Large -> true
+    | Strict -> false
+
+  let inter_with_integer t =
+    let t = {
+    minb = if Q.equal Q.minus_inf t.minv then Large else Strict;
+    minv =
+      if is_Large t.minb && Q.is_integer t.minv
+      then Q.add t.minv Q.one
+      else Q.ceil t.minv;
+    maxb = if Q.equal Q.inf t.maxv then Large else Strict;
+    maxv =
+      if is_Large t.maxb && Q.is_integer t.maxv
+      then Q.sub t.maxv Q.one
+      else Q.floor t.maxv;
+  } in
+    if Q.lt t.maxv t.minv then None else begin
+      assert (invariant t);
+      Some t
+    end
+*)
+end

src_common/modulo.mlw

-module Modulo
+module Divisible
 
        use bool.Bool
+       use q.Z as Z
        use q.Q as Q
        use int.Int
        use real.RealInfix
        use real.Truncate
        use real.FromInt
 
-       exception ModuloFinitePositiveExpected
+       exception FinitePositiveExpected
 
        let lemma round_modulo (a:real) (m:real): unit
            requires { 0. <. m }
@@ -21,13 +22,15 @@ module Modulo
            assert { f <=. d <. from_int (t + 1) };
            assert { f <=. d <. f +. 1. };
            assert { (a /. m) -. 1. <. f <=. a /. m };
+           assert { ((a /. m) -. 1.) *. m <. f *. m <=. (a /. m) *. m };
+           assert { ((a /. m) *. m) -. m <. f *. m };
            assert { a -. m <. f *. m  <=. a };
            assert { -. a <=. -. f *. m  <. -. a +. m };
            assert { 0. <=. a -. f *. m  <. m }
 
        let round_down_to (a:Q.t) (m:Q.t) : (r:Q.t)
            requires { Q.not_NaN a } requires { Q.not_NaN m }
-           raises { ModuloFinitePositiveExpected -> not (Q.is_real m /\ 0. <. Q.real m ) }
+           raises { FinitePositiveExpected -> not (Q.is_real m /\ 0. <. Q.real m ) }
            ensures { Q.not_NaN r }
            ensures { a.Q.value = Q.PlusInf -> r.Q.value = Q.PlusInf }
            ensures { Q.( r <= a) }
@@ -36,8 +39,8 @@ module Modulo
            ensures { a.Q.is_real -> Q.( r.real <. a.real) -> forall q. not Q.(r.real <. (from_int q) *. m.real <=. a.real ) }
          =
            match Q.classify m with
-           | Q.ZERO | Q.MINF | Q.INF | Q.UNDEF -> raise ModuloFinitePositiveExpected
-           | Q.NZERO -> if Q.( m <= (of_int 0) ) then raise ModuloFinitePositiveExpected
+           | Q.ZERO | Q.MINF | Q.INF | Q.UNDEF -> raise FinitePositiveExpected
+           | Q.NZERO -> if Q.( m <= (of_int 0) ) then raise FinitePositiveExpected
            end;
            match Q.classify a with
            | Q.MINF | Q.INF | Q.UNDEF | Q.ZERO -> a
@@ -50,7 +53,7 @@ module Modulo
 
        let round_up_to (a:Q.t) (m:Q.t) : (r:Q.t)
            requires { Q.not_NaN a } requires { Q.not_NaN m }
-           raises { ModuloFinitePositiveExpected -> not (Q.is_real m /\ 0. <. Q.real m ) }
+           raises { FinitePositiveExpected -> not (Q.is_real m /\ 0. <. Q.real m ) }
            ensures { Q.not_NaN r }
            ensures { a.Q.value = Q.MinusInf -> r.Q.value = Q.MinusInf }
            ensures { Q.(a <= r) }
@@ -61,8 +64,166 @@ module Modulo
            let res = round_down_to Q.((of_int 0) - a) m in
            assert { a.Q.value = Q.MinusInf -> res.Q.value = Q.PlusInf };
            Q.((of_int 0) - res)
-           
 
+        let lemma simple_mul_div (a b : real)
+            requires { b <> 0. }
+            ensures { (a /. b) *. b = a } =
+            ()
 
+        predicate ddivisible_using (a b:real) (d:int) =
+           a = (from_int d) *. b
+
+        predicate ddivisible (a b: real) =
+          exists d. ddivisible_using a b d
+
+
+        let lemma remove_product_right (a b c:int) : unit
+           requires { b <> 0 }
+           requires { a * b = c * b }
+           ensures { a = c } =
+           () 
+
+        let lemma divisible_to_z (a b:Q.t) (d:int) : (dnum:int, dden: int)
+          requires { a.Q.is_real } requires { b.Q.is_real } requires { b.Q.real <> 0. }
+          requires { ddivisible_using a.Q.real b.Q.real d }
+          ensures { Z.ddivisible_using a.Q.num b.Q.num dnum }
+          ensures { Z.ddivisible_using b.Q.den a.Q.den dden }
+          ensures { d = dnum * dden } =
+             assert { b.Q.den * a.Q.num = d * b.Q.num * a.Q.den
+                 by from_int b.Q.den *. from_int a.Q.num = from_int d *. from_int b.Q.num *. from_int a.Q.den
+                 by (from_int a.Q.num /. from_int a.Q.den) *. from_int a.Q.den *. from_int b.Q.den = (from_int d *. (from_int b.Q.num /. from_int b.Q.den)) *. from_int a.Q.den *. from_int b.Q.den
+                 by from_int a.Q.num /. from_int a.Q.den = from_int d *. (from_int b.Q.num /. from_int b.Q.den) 
+             };
+             let dnum = Z.prime_to_one_another_mul b.Q.num (d * a.Q.den) b.Q.den a.Q.num in
+             assert { Z.ddivisible_using a.Q.num b.Q.num dnum };
+             let dden = Z.prime_to_one_another_mul a.Q.num b.Q.den a.Q.den (d * b.Q.num) in
+             assert { Z.ddivisible_using b.Q.den a.Q.den dden };
+             assert { dnum * dden * b.Q.num * a.Q.den = d * b.Q.num * a.Q.den };
+             remove_product_right (dnum * dden * b.Q.num) a.Q.den (d * b.Q.num);
+             remove_product_right (dnum * dden) b.Q.num d;
+             (dnum,dden)
+
+        let lemma divisible_from_z (a b:Q.t) (dnum:int) (dden:int) : unit
+          requires { a.Q.is_real } requires { b.Q.is_real }
+          requires { Z.ddivisible_using a.Q.num b.Q.num dnum }
+          requires { Z.ddivisible_using b.Q.den a.Q.den dden }
+          ensures { ddivisible_using a.Q.real b.Q.real (dnum*dden) }
+         =
+           ghost (simple_mul_div (from_int a.Q.num) (from_int a.Q.den);
+                  simple_mul_div (from_int b.Q.num) (from_int b.Q.den););
+           let ghost d = dnum * dden in
+           assert { a.Q.real = (from_int d) *. b.Q.real
+              by from_int a.Q.num /. from_int a.Q.den = from_int d *. (from_int b.Q.num /. from_int b.Q.den)
+              by (from_int a.Q.num /. from_int a.Q.den) *. (from_int b.Q.den /. from_int b.Q.den)  = from_int d *. (from_int b.Q.num /. from_int b.Q.den) *. (from_int a.Q.den /. from_int a.Q.den)
+              by (from_int a.Q.num *. from_int b.Q.den) /. from_int a.Q.den /. from_int b.Q.den  = (from_int d *. from_int b.Q.num *. from_int a.Q.den) /. from_int a.Q.den /. from_int b.Q.den
+              by from_int a.Q.num *. from_int b.Q.den = from_int d *. from_int b.Q.num *. from_int a.Q.den
+              by from_int a.Q.num *. from_int b.Q.den = from_int dnum *. from_int dden *. from_int b.Q.num *. from_int a.Q.den
+              by from_int a.Q.num *. from_int b.Q.den = from_int (dnum * b.Q.num) *. from_int (dden * a.Q.den)
+            }
+
+
+        let divisible (a:Q.t) (b:Q.t) : (r:bool,ghost d: int)
+         requires { a.Q.is_real } requires { b.Q.is_real } requires { b.Q.real <> 0. }
+         ensures { not r -> forall d. not (ddivisible_using a.Q.real b.Q.real d) }
+         ensures { r -> ddivisible_using a.Q.real b.Q.real d } =
+            let b1,dnum = Z.divisible a.Q.num b.Q.num in
+            if b1 then
+              let b2,dden = Z.divisible b.Q.den a.Q.den in
+              if b2 then
+                (true,dnum*dden)
+              else begin
+                let ghost () = if pure { exists d. ddivisible_using a.Q.real b.Q.real d } then
+                   let d = any (d:int) ensures { ddivisible_using a.Q.real b.Q.real d } in
+                   let _dnum, dden = divisible_to_z a b d in
+                   assert { Z.ddivisible_using a.Q.den b.Q.den dden };
+                   absurd
+                in
+                (false,ghost 0)
+              end
+            else begin
+              let ghost () = if pure { exists d. ddivisible_using a.Q.real b.Q.real d } then
+                 let d = any (d:int) ensures { ddivisible_using a.Q.real b.Q.real d } in
+                 let dnum, _dden = divisible_to_z a b d in
+                 assert { Z.ddivisible_using a.Q.num b.Q.num  dnum };
+                 absurd
+              in
+              (false,ghost 0)
+            end
+
+       let mult_cst_divisible (a:Q.t) (q:Q.t) : (a':Q.t)
+          requires { q.Q.is_real } requires { a.Q.is_real } 
+          ensures { a'.Q.is_real }
+          ensures { forall r. ddivisible r a.Q.real -> ddivisible (r *. q.Q.real ) a'.Q.real } =
+           let a' = Q.(a*q) in
+           let lemma post (r:real) : unit
+             requires { ddivisible r a.Q.real }
+             ensures { ddivisible (r *. q.Q.real) a'.Q.real } =
+              let d = any int ensures { ddivisible_using r a.Q.real result } in
+              assert {ddivisible_using (r *. q.Q.real) a'.Q.real d }
+           in
+           a'
+
+
+       let union_divisible (a:Q.t) (b:Q.t) : (u:Q.t)
+          requires { a.Q.is_real } requires { b.Q.is_real } requires { a.Q.real <> 0. } requires { b.Q.real <> 0. }
+          ensures { u.Q.is_real }
+          ensures { forall r. r.Q.is_real -> ddivisible r.Q.real a.Q.real -> ddivisible r.Q.real u.Q.real }
+          ensures { forall r. r.Q.is_real -> ddivisible r.Q.real b.Q.real -> ddivisible r.Q.real u.Q.real } =
+           let n,na',nb' = Z.gcd a.Q.num b.Q.num in
+           let d,da',db',_fa = Z.lcm a.Q.den b.Q.den in
+           assert { Z.prime_to_one_another a.Q.num a.Q.den };
+           assert { Z.prime_to_one_another b.Q.num b.Q.den };
+           assert { Z.prime_to_one_another n a.Q.den };
+           assert { Z.prime_to_one_another n b.Q.den };
+           assert { Z.prime_to_one_another n d };
+           let u = Q.make_exact n d in
+           let lemma post (r:Q.t) : unit
+             requires { a.Q.is_real } requires { r.Q.is_real }
+             requires { ddivisible r.Q.real a.Q.real }
+             ensures { ddivisible r.Q.real u.Q.real } =
+              let dd = any int ensures { ddivisible_using r.Q.real a.Q.real result } in
+              let dnum,dden = divisible_to_z r a dd in
+              assert { Z.ddivisible_using r.Q.num a.Q.num dnum };
+              assert { Z.ddivisible_using r.Q.num n (na'*dnum) };
+              assert { Z.ddivisible_using a.Q.den r.Q.den dden };
+              assert { Z.ddivisible_using d r.Q.den (dden*da') };
+              divisible_from_z r u (na'*dnum) (da'*dden);
+              assert { ddivisible_using r.Q.real u.Q.real (na'*dnum*da'*dden) }
+           in
+           let lemma post (r:Q.t) : unit
+             requires { b.Q.is_real } requires { r.Q.is_real }
+             requires { ddivisible r.Q.real b.Q.real }
+             ensures { ddivisible r.Q.real u.Q.real } =
+              let dd = any int ensures { ddivisible_using r.Q.real b.Q.real result } in
+              let dnum,dden = divisible_to_z r b dd in
+              assert { Z.ddivisible_using r.Q.num b.Q.num dnum };
+              assert { Z.ddivisible_using r.Q.num n (nb'*dnum) };
+              assert { Z.ddivisible_using b.Q.den r.Q.den dden };
+              assert { Z.ddivisible_using d r.Q.den (dden*db') };
+              divisible_from_z r u (nb'*dnum) (db'*dden);
+              assert { ddivisible_using r.Q.real u.Q.real (nb'*dnum*db'*dden) }
+           in
+           u
+
+
+       let inter_divisible (a:Q.t) (b:Q.t) : (u:Q.t)
+          requires { a.Q.is_real } requires { b.Q.is_real } requires { 0. <> a.Q.real } requires { 0. <> b.Q.real }
+          ensures { u.Q.is_real }
+          ensures { forall r. r.Q.is_real -> ddivisible r.Q.real a.Q.real -> ddivisible r.Q.real b.Q.real -> ddivisible r.Q.real u.Q.real } =
+           let n,na',_ = Z.gcd a.Q.den b.Q.den in
+           let d,_,_,fa = Z.lcm a.Q.num b.Q.num in
+           let u = Q.make_exact d n in
+           let lemma post (r:Q.t) : unit
+             requires { r.Q.is_real }
+             requires { ddivisible r.Q.real a.Q.real }
+             requires { ddivisible r.Q.real b.Q.real }
+             ensures { ddivisible r.Q.real u.Q.real } =
+              let dda = any int ensures { ddivisible_using r.Q.real a.Q.real result } in
+              let ddb = any int ensures { ddivisible_using r.Q.real b.Q.real result } in
+              let dnuma,ddena = divisible_to_z r a dda in
+              let _,_ = divisible_to_z r b ddb in
+              divisible_from_z r u (fa dnuma) (na'*ddena)
+           in
+           u
 
 end

src_common/modulo__Modulo.ml → src_common/modulo__Divisible.ml

-exception ModuloFinitePositiveExpected
+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 ModuloFinitePositiveExpected
+  | (Q.ZERO | (Q.MINF | (Q.INF | Q.UNDEF))) -> raise FinitePositiveExpected
   | Q.NZERO ->
-    if (Q.(<=) m (Q.of_bigint Z.zero))
-    then raise ModuloFinitePositiveExpected
+    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
@@ -16,3 +14,23 @@ let round_up_to (a: Q.t) (m: Q.t) : Q.t =
   let res = round_down_to (Q.(-) (Q.of_bigint Z.zero) a) m in
   (Q.(-) (Q.of_bigint Z.zero) res)
 
+let divisible (a: Q.t) (b: Q.t) : bool =
+  let b1 =
+  (Z.divisible (a.Q.num) (b.Q.num)) in
+  if b1
+  then
+    let b2 = (Z.divisible (b.Q.den) (a.Q.den)) in if b2 then true else false
+  else false
+
+let mult_cst_divisible (a: Q.t) (q: Q.t) : Q.t = (Q.( * ) a q)
+
+let union_divisible (a: Q.t) (b: Q.t) : Q.t =
+  let n =
+  (Z.gcd (a.Q.num) (b.Q.num)) in
+  let d = (Z.lcm (a.Q.den) (b.Q.den)) in ({ Q.num = n; Q.den = d })
+
+let inter_divisible (a: Q.t) (b: Q.t) : Q.t =
+  let n1 =
+  (Z.gcd (a.Q.den) (b.Q.den)) in
+  let d1 = (Z.lcm (a.Q.num) (b.Q.num)) in ({ Q.num = d1; Q.den = n1 })
+

src_common/q.mlw

@@ -10,6 +10,55 @@ module Z
          requires { 0 < b }
          ensures { 0 <= d*b - a < b }
 
+       predicate ddivisible_using (a:int) (b:int) (c:int) =
+          a = c * b
+
+       predicate ddivisible (a:int) (b:int) =
+          exists d. ddivisible_using a b d
+
+       val divisible (a:int) (b:int) : (r:bool,ghost d: int)
+         ensures { (not r) -> forall c. not (ddivisible_using a b c) }
+         ensures { r -> ddivisible_using a b d }
+
+       function gcd (a b:int): int
+
+       val gcd (a b:int) : (c:int,ghost a':int,ghost b':int)
+         ensures { gcd a b = c }
+         ensures { c * a' = a }
+         ensures { c * b' = b }
+         ensures { forall r d. ddivisible_using r a d -> ddivisible_using r c (d*a')}
+         ensures { forall r d. ddivisible_using r b d -> ddivisible_using r c (d*b')}
+         ensures { forall r da db. ddivisible_using a r da -> ddivisible_using b r db
+                                  -> ddivisible_using c r (da*a')}
+
+       function lcm (a b:int): int
+
+       val lcm (a b:int) : (c:int, ghost a':int, ghost b':int, ghost fa : int -> int)
+         requires { a <> 0 } requires { b <> 0 }
+         ensures { c <> 0 } ensures { lcm a b = c }
+         ensures { c = a' * a } ensures { c = b' * b }
+         ensures { forall r da db. ddivisible_using r a da -> ddivisible_using r b db ->
+                    (da = a' * fa da /\ ddivisible_using r c (fa da))  }
+         ensures { forall r da. ddivisible_using a r da -> ddivisible_using c r (da*a') }
+         ensures { forall r db. ddivisible_using a r db -> ddivisible_using c r (db*b') }
+
+
+       predicate prime_to_one_another (a b:int) (* = (gcd a b = 1) *)
+
+       val ghost prime_to_one_another_mul (a m b n: int) : (q:int)
+          requires { prime_to_one_another a b }
+          requires { a * m = b * n } (* a * b * q = b * a * q *)
+          ensures { ddivisible_using m b q  (* m = b * q *) }
+          ensures { ddivisible_using n a q  (* n = a * q *) }
+
+       axiom GCD1: forall a b c. prime_to_one_another a b -> prime_to_one_another (gcd a c) b
+       axiom GCD2: forall a b c. prime_to_one_another a b -> prime_to_one_another a (gcd b c)
+       axiom GCD3: forall a b c. prime_to_one_another a b -> prime_to_one_another a c
+                                 -> prime_to_one_another a (lcm b c)
+       axiom GCD4: forall a b c. prime_to_one_another a b -> prime_to_one_another c b
+                                 -> prime_to_one_another (lcm a c) b
+       axiom GCD_comm: forall a b. gcd a b = gcd b a
+
 end
 
 module Q
@@ -17,6 +66,7 @@ module Q
    use real.RealInfix
    use int.Int
    use real.FromInt
+   use Z as Z
 
    type value =
       | MinusInf
@@ -30,10 +80,20 @@ module Q
        ghost value: value;
     }
     invariant { value = Real -> 0 < den }
+    invariant { value = Real -> Z.prime_to_one_another num den }
 
     predicate is_real (q:t) =
         q.value = Real
 
+    predicate is_minus_inf (q:t) =
+        q.value = MinusInf
+
+    predicate is_plus_inf (q:t) =
+        q.value = PlusInf
+
+    predicate is_nan (q:t) =
+        q.value = NaN
+
     predicate not_NaN (q:t) = q.value <> NaN
 
     function real (q:t) : real
@@ -55,11 +115,14 @@ module Q
              end
       }
 
+    predicate equal (a b:t) =
+      if a.is_real /\ b.is_real then a.real = b.real else a.value = b.value
+
     val (=) (a:t) (b:t) : bool
-     ensures { not a.is_real -> not b.is_real -> result = (a.value = b.value) }
-      ensures { a.is_real -> b.is_real -> result = (a.real = b.real) }
+     ensures { equal a b = result }
 
     function (<=) (a:t) (b:t) : bool
+    function (<) (a:t) (b:t) : bool = a <= b /\ not (equal a b)
 
     axiom le_def: forall a b. a.is_real -> b.is_real -> ((a <= b) <-> (a.real <=. b.real))
     axiom le_def_full: forall a b [a <= b].
@@ -74,6 +137,11 @@ module Q
             | PlusInf, _  -> not (a <= b)
          end
 
+    (* lemma le_anti_refl: forall a b. a <= b -> b <= a -> equal a b *)
+    (* lemma le_trans: forall a b c. a <= b -> b <= c -> a <= c *)
+    (* lemma le_lt_trans: forall a b c. a <= b -> b < c -> a < c *)
+    (* lemma lt_le_trans: forall a b c. a < b -> b <= c -> a < c *)
+
     val (<=) (a:t) (b:t) : bool
      requires { not_NaN a /\ not_NaN b }
      ensures { result = (a <= b) }
@@ -120,8 +188,8 @@ module Q
                 | MinusInf, MinusInf | PlusInf, PlusInf -> result.value = PlusInf
                 end
               }
-      ensures { is_real a -> is_real b -> b.real <> 0. -> is_real result }
-      ensures { is_real a -> is_real b -> b.real <> 0. -> a.real *. b.real = result.real }
+      ensures { is_real a -> is_real b -> is_real result }
+      ensures { is_real a -> is_real b -> a.real *. b.real = result.real }
 
      val (/) (a b:t) : t
       requires { not_NaN a /\ not_NaN b }
@@ -142,7 +210,16 @@ module Q
       ensures { is_real a -> is_real b -> b.real <> 0. -> is_real result }
       ensures { is_real a -> is_real b -> b.real <> 0. -> a.real /. b.real = result.real }
 
+     val make (num den: int): t
+       requires { den <> 0 }
+       ensures { result.is_real }
+       ensures { result.real = (from_int num) /. (from_int den) }
 
+     val make_exact (num den: int): t
+       requires { den <> 0 } requires { Z.prime_to_one_another num den }
+       ensures { result.is_real }
+       ensures { result.num = num }
+       ensures { result.den = den }
 
      use real.Truncate
 
@@ -154,17 +231,30 @@ module Q
       ensures { is_real result }
       ensures { result.real = from_int a }
 
-     use Z
-
      let floor (a:t) : int
        requires { is_real a }
        ensures { result = floor a.real } =
-       fdiv a.num a.den
+        assert { from_int (floor a.real) <=. a.real <. from_int (floor a.real) +. 1. };
+        assert { 0. <=. a.real -. from_int (floor a.real) <. 1. };
+        let r = Z.fdiv a.num a.den in
+        assert { Int.(0 <= a.num - r*a.den < a.den) };
+        assert { 0. <=. (from_int a.num) -. (from_int r)*.(from_int a.den) <. (from_int a.den) };
+        assert { ((from_int a.num) -. (from_int r)*.(from_int a.den))/.(from_int a.den) <. (from_int a.den)/.(from_int a.den) };
+        assert { 0. <=. a.real -. from_int r <. 1. };
+        r
+
 
      let ceil (a:t) : int
        requires { is_real a }
        ensures { result = ceil a.real } =
-       cdiv a.num a.den
+        assert { from_int (ceil a.real) -. 1. <. a.real <=. from_int (ceil a.real) };
+        assert { 0. <=. from_int (ceil a.real) -. a.real  <. 1. };
+        let r = Z.cdiv a.num a.den in
+        assert { Int.(0 <= r*a.den - a.num < a.den) };
+        assert { 0. <=. (from_int r)*.(from_int a.den) -. (from_int a.num) <. (from_int a.den) };
+        assert { ((from_int r)*.(from_int a.den) -. (from_int a.num))/.(from_int a.den) <. (from_int a.den)/.(from_int a.den) };
+        assert { 0. <=. from_int r -. a.real <. 1. };
+        r
 
 
 end

src_common/q/why3session.xml

@@ -3,29 +3,74 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="6">
 <prover id="0" name="CVC4" version="1.7" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="2" name="Alt-Ergo" version="2.3.3" timelimit="5" steplimit="0" memlimit="1000"/>
 <file format="whyml" proved="true">
 <path name=".."/><path name="q.mlw"/>
 <theory name="Q" proved="true">
  <goal name="t&#39;vc" expl="VC for t" proved="true">
- <proof prover="0"><result status="valid" time="0.04" steps="1502"/></proof>
+ <proof prover="0"><result status="valid" time="0.04" steps="17812"/></proof>
  </goal>
  <goal name="floor&#39;vc" expl="VC for floor" proved="true">
  <transf name="split_vc" proved="true" >
-  <goal name="floor&#39;vc.0" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.04" steps="7201"/></proof>
+  <goal name="floor&#39;vc.0" expl="assertion" proved="true">
+  <proof prover="0"><result status="valid" time="0.03" steps="4863"/></proof>
   </goal>
-  <goal name="floor&#39;vc.1" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.41" steps="191862"/></proof>
+  <goal name="floor&#39;vc.1" expl="assertion" proved="true">
+  <proof prover="0"><result status="valid" time="0.02" steps="4386"/></proof>
+  </goal>
+  <goal name="floor&#39;vc.2" expl="precondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.15" steps="51614"/></proof>
+  </goal>
+  <goal name="floor&#39;vc.3" expl="assertion" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="4450"/></proof>
+  </goal>
+  <goal name="floor&#39;vc.4" expl="assertion" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="4501"/></proof>
+  </goal>
+  <goal name="floor&#39;vc.5" expl="assertion" proved="true">
+  <proof prover="1"><result status="valid" time="0.01" steps="19745"/></proof>
+  </goal>
+  <goal name="floor&#39;vc.6" expl="assertion" proved="true">
+  <transf name="split_vc" proved="true" >
+   <goal name="floor&#39;vc.6.0" expl="assertion" proved="true">
+   <proof prover="1"><result status="valid" time="0.06" steps="231992"/></proof>
+   </goal>
+   <goal name="floor&#39;vc.6.1" expl="assertion" proved="true">
+   <proof prover="2"><result status="valid" time="0.14" steps="372"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="floor&#39;vc.7" expl="postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.76" steps="707"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="ceil&#39;vc" expl="VC for ceil" proved="true">
  <transf name="split_vc" proved="true" >
-  <goal name="ceil&#39;vc.0" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.07" steps="7201"/></proof>
+  <goal name="ceil&#39;vc.0" expl="assertion" proved="true">
+  <proof prover="0"><result status="valid" time="0.03" steps="4880"/></proof>
+  </goal>
+  <goal name="ceil&#39;vc.1" expl="assertion" proved="true">
+  <proof prover="0"><result status="valid" time="0.03" steps="4396"/></proof>
+  </goal>
+  <goal name="ceil&#39;vc.2" expl="precondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.07" steps="51628"/></proof>
+  </goal>
+  <goal name="ceil&#39;vc.3" expl="assertion" proved="true">
+  <proof prover="0"><result status="valid" time="0.02" steps="4492"/></proof>
+  </goal>
+  <goal name="ceil&#39;vc.4" expl="assertion" proved="true">
+  <proof prover="0"><result status="valid" time="0.02" steps="4543"/></proof>
+  </goal>
+  <goal name="ceil&#39;vc.5" expl="assertion" proved="true">
+  <proof prover="1"><result status="valid" time="0.01" steps="19673"/></proof>
+  </goal>
+  <goal name="ceil&#39;vc.6" expl="assertion" proved="true">
+  <proof prover="2"><result status="valid" time="0.15" steps="512"/></proof>
   </goal>
-  <goal name="ceil&#39;vc.1" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.57" steps="203328"/></proof>
+  <goal name="ceil&#39;vc.7" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.02" steps="5645"/></proof>
   </goal>
  </transf>
  </goal>

src_common/q__Q.ml

@@ -4,11 +4,6 @@ type value =
   | NaN
   | Real
 
-type t = {
-  num: Z.t;
-  den: Z.t;
-  }
-
 type kind =
   | ZERO
   | NZERO
@@ -16,7 +11,7 @@ type kind =
   | MINF
   | UNDEF
 
-let floor (a: Q.t) : Z.t = (Z.fdiv (a.num) (a.den))
+let floor (a: Q.t) : Z.t = (Z.fdiv (a.Q.num) (a.Q.den))
 
-let ceil (a: Q.t) : Z.t = (Z.cdiv (a.num) (a.den))
+let ceil (a: Q.t) : Z.t = (Z.cdiv (a.Q.num) (a.Q.den))