diff --git a/libpoly/dune b/libpoly/dune
index 924c95c2c886f2ac00ac9efc289a81178c50876b..ff84f0ec1dd6d8abaf2953947e863797a72ba088 100644
--- a/libpoly/dune
+++ b/libpoly/dune
@@ -15,7 +15,7 @@
(progn
(chdir libpoly/build
(progn
- (run cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=install)
+ (run cmake .. -DCMAKE_BUILD_TYPE=Debug -DCMAKE_INSTALL_PREFIX=install)
(run make static_pic_poly poly)))
(copy libpoly/build/src/libpicpoly.a libpoly.a)
(copy libpoly/build/src/libpoly.so dllpoly.so)
diff --git a/libpoly/libpoly b/libpoly/libpoly
index 27094db6e7a34958a9762e4ff1803f0d25590a27..0e852f489a7148213e0a813417a96882062bceaa 160000
--- a/libpoly/libpoly
+++ b/libpoly/libpoly
@@ -1 +1 @@
-Subproject commit 27094db6e7a34958a9762e4ff1803f0d25590a27
+Subproject commit 0e852f489a7148213e0a813417a96882062bceaa
diff --git a/libpoly/ocaml_poly.ml b/libpoly/ocaml_poly.ml
index 53f46f5f1caca02b309fb32b913a1ef2334f90f4..5539f21f05536260426a9d2b13769266111a95c0 100644
--- a/libpoly/ocaml_poly.ml
+++ b/libpoly/ocaml_poly.ml
@@ -52,6 +52,8 @@ module A = struct
C.Function.mpz_clear mpz;
a
+ let of_int i = of_z (Z.of_int i)
+
let mpq_of_q (q : Q.t) =
let mpq = Ctypes.allocate_n C.Type.MPQ._struct 1 in
C.Function.ml_z_mpz_init_set_z (mpq |-> C.Type.MPQ.mp_num) q.num;
@@ -101,6 +103,7 @@ module A = struct
let neg = unop C.Function.lp_algebraic_number_neg
let inv = unop C.Function.lp_algebraic_number_inv
+ let abs a = if sign a < 0 then neg a else a
let add = binop C.Function.lp_algebraic_number_add
let sub = binop C.Function.lp_algebraic_number_sub
let mul = binop C.Function.lp_algebraic_number_mul
diff --git a/libpoly/ocaml_poly.mli b/libpoly/ocaml_poly.mli
index 6e4e4d5baae3f70130c6c8104645d8998d7a9328..afe21a80f1b287b100cdeeaed8eef62968c80518 100644
--- a/libpoly/ocaml_poly.mli
+++ b/libpoly/ocaml_poly.mli
@@ -28,12 +28,15 @@ module A : sig
val to_rational_approx : t -> Q.t
val to_string : t -> string
val to_double : t -> float
+ val of_int : int -> t
val of_z : Z.t -> t
val of_q : Q.t -> t
val add : t -> t -> t
val sub : t -> t -> t
+ val mul : t -> t -> t
val neg : t -> t
val inv : t -> t
+ val abs : t -> t
val div : t -> t -> t
val div_t : t -> t -> Z.t
val div_e : t -> t -> Z.t
diff --git a/src_colibri2/stdlib/std.ml b/src_colibri2/stdlib/std.ml
index b5996e1a892c84ab53a61f937117125e5999d63a..c666f604005085ca4485229c16a69abb79517766 100644
--- a/src_colibri2/stdlib/std.ml
+++ b/src_colibri2/stdlib/std.ml
@@ -185,10 +185,20 @@ module A = struct
let gt a b = compare a b > 0
let le a b = compare a b <= 0
let lt a b = compare a b < 0
+ let min a b = if lt a b then a else b
+ let max a b = if gt a b then a else b
let of_string_decimal s = Q (Q.of_string_decimal s)
+ let of_string s = Q (Q.of_string s)
+ let to_string = function Q q -> Q.to_string q | A a -> A.to_string a
let is_integer = function Q q -> Q.is_integer q | A _ -> false
(* by normalization *)
+ let is_real = function Q q -> Q.is_real q | A _ -> true
+ let to_z = function Q q -> q.Q.num | A _ -> assert false
+ let to_int = function Q q -> Q.to_int q | A _ -> assert false
+ let inf = Q Q.inf
+ let minus_inf = Q Q.minus_inf
+
let normalize (a : A.t) =
if A.is_rational a then Q (A.to_rational_approx a) else A a
@@ -198,12 +208,16 @@ module A = struct
| Q q -> Q.is_unsigned_integer size q
| A _ -> false
+ let of_q q = Q q
let of_z z = Q (Q.of_bigint z)
+ let of_int z = Q (Q.of_int z)
+ let of_bigint = of_z
let floor = function Q q -> Q (Q.floor q) | A a -> of_z (A.floor a)
let ceil = function Q q -> Q (Q.ceil q) | A a -> of_z (A.ceil a)
let truncate = function Q q -> Q (Q.truncate q) | A a -> of_z (A.truncate a)
let neg = function Q q -> Q (Q.neg q) | A a -> normalize (A.neg a)
let inv = function Q q -> Q (Q.inv q) | A a -> normalize (A.inv a)
+ let abs = function Q q -> Q (Q.abs q) | A a -> normalize (A.abs a)
let combine2 fq fa cv a b =
match (a, b) with Q a, Q b -> Q (fq a b) | _ -> cv (fa (to_a a) (to_a b))
@@ -212,6 +226,12 @@ module A = struct
let add = combine2 Q.add A.add normalize
let sub = combine2 Q.sub A.sub normalize
let mul = combine2 Q.mul A.add normalize
+ let ( + ) = add
+ let ( - ) = sub
+ let ( ~- ) = neg
+ let ( ~+ ) x = x
+ let ( * ) = mul
+ let ( / ) = div
let div_e = combine2 Q.div_e A.div_e of_z
let div_t = combine2 Q.div_t A.div_t of_z
let div_f = combine2 Q.div_f A.div_f of_z
@@ -226,20 +246,35 @@ module A = struct
let a_gen : A.t QCheck.Gen.t =
let open QCheck.Gen in
- let* coefs = list small_signed_int in
- let u = Ocaml_poly.UPolynomial.construct (List.map Z.of_int coefs) in
- let roots = Ocaml_poly.UPolynomial.roots_isolate u in
- oneofl roots
+ if false then
+ let rec aux s =
+ let coefs = small_list small_signed_int s in
+ let u = Ocaml_poly.UPolynomial.construct (List.map Z.of_int coefs) in
+ let roots = Ocaml_poly.UPolynomial.roots_isolate u in
+ match roots with [] -> aux s | _ -> oneofl roots s
+ in
+ aux
+ else fun s ->
+ let a = (triple small_signed_int small_nat small_nat) s in
+ let b = (triple small_signed_int small_nat small_nat) s in
+ let coefs = [ a; b ] in
+ List.fold_left
+ (fun acc (p, c, r) ->
+ A.add acc
+ (A.mul (A.of_int p) (A.positive_root (A.of_int c) Int.(r + 1))))
+ (A.zero ()) coefs
let gen =
let open QCheck.Gen in
- oneof [ map (fun q -> Q q) Q.gen; map (fun a -> !!a) a_gen ]
+ frequency [ (999, map (fun q -> Q q) Q.gen); (1, map (fun a -> !!a) a_gen) ]
let shrink q =
let open QCheck.Iter in
match q with
| Q q -> map (fun q -> Q q) (Q.shrink q)
- | A a -> if A.is_integer a then empty else return (of_z (A.truncate a))
+ | A _ ->
+ (* if A.is_integer a then empty else return (of_z (A.truncate a)) *)
+ empty
let pow q n = match q with Q q -> Q (Q.pow q n) | A a -> !!(A.pow a n)
end
diff --git a/src_colibri2/stdlib/std.mli b/src_colibri2/stdlib/std.mli
index c05caeebdea30ea223ffe501bdab61cee992863e..0a461204a0c75779b24988bbdc2cdd4dc80145ae 100644
--- a/src_colibri2/stdlib/std.mli
+++ b/src_colibri2/stdlib/std.mli
@@ -81,7 +81,7 @@ module Q : sig
end
module A : sig
- type t
+ type t = Q of Q.t | A of Ocaml_poly.A.t
val zero : t
val one : t
@@ -89,15 +89,29 @@ module A : sig
val minus_one : t
(** 0, 1, -1. *)
+ val of_bigint : Z.t -> t
+ val of_z : Z.t -> t
+ val of_int : int -> t
+ val to_z : t -> Z.t
+
+ val to_int : t -> int
+ (** suppose that it is an integer *)
+
+ val of_q : Q.t -> t
val sign : t -> int
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
+ val to_string : t -> string
val two : t
val ge : t -> t -> bool
val le : t -> t -> bool
val gt : t -> t -> bool
val lt : t -> t -> bool
+
+ val of_string : string -> t
+ (** integer *)
+
val of_string_decimal : string -> t
val floor : t -> t
val ceil : t -> t
@@ -106,6 +120,7 @@ module A : sig
val sub : t -> t -> t
val neg : t -> t
val inv : t -> t
+ val abs : t -> t
val mul : t -> t -> t
val div : t -> t -> t
val div_t : t -> t -> t
@@ -116,6 +131,9 @@ module A : sig
val mod_f : t -> t -> t
val pow : t -> int -> t
val is_integer : t -> bool
+ val is_real : t -> bool
+ val inf : t
+ val minus_inf : t
val is_unsigned_integer : int -> t -> bool
(** [is_unsigned_integer size q] checks that [q] is an integer that fits in
@@ -128,4 +146,12 @@ module A : sig
val is_not_zero : t -> bool
val gen : t QCheck.Gen.t
val shrink : t QCheck.Shrink.t
+ val ( ~- ) : t -> t
+ val ( ~+ ) : t -> t
+ val ( + ) : t -> t -> t
+ val ( - ) : t -> t -> t
+ val ( * ) : t -> t -> t
+ val ( / ) : t -> t -> t
+ val min : t -> t -> t
+ val max : t -> t -> t
end
diff --git a/src_colibri2/tests/tests_LRA.ml b/src_colibri2/tests/tests_LRA.ml
index d26a54428c5ca5079e83be14a3655bb371ace95d..4fc5a88e15ba232c6fc18e04b573c926cadff42b 100644
--- a/src_colibri2/tests/tests_LRA.ml
+++ b/src_colibri2/tests/tests_LRA.ml
@@ -36,9 +36,7 @@ let theories =
]
let run f = Scheduler.run_exn ~step_limit:3000 ~nodec:() ~theories f
-
let run_dec f = Scheduler.run_exn ~step_limit:3000 ?nodec:None ~theories f
-
let ( $$ ) f x = f x
(* The tests with rundec check only the result on a model satisfying
@@ -49,7 +47,7 @@ open Expr
let solve0a _ =
run @@ fun env ->
let a = fresh env Ty.real "ar" in
- let _1 = LRA.RealValue.cst Q.one in
+ let _1 = LRA.RealValue.cst A.one in
let a1 = LRA.add env a _1 in
register env a1;
register env _1;
@@ -59,11 +57,11 @@ let solve0a _ =
let solve0b _ =
run @@ fun env ->
let a = fresh env Ty.real "ar" in
- let _1 = LRA.RealValue.cst Q.one in
- let _2 = LRA.RealValue.cst Q.two in
- let _4 = LRA.RealValue.cst (Q.of_int 4) in
+ let _1 = LRA.RealValue.cst A.one in
+ let _2 = LRA.RealValue.cst A.two in
+ let _4 = LRA.RealValue.cst (A.of_int 4) in
let a1 = LRA.add env a _1 in
- let _2a2 = LRA.add' env Q.two a Q.one _2 in
+ let _2a2 = LRA.add' env A.two a A.one _2 in
List.iter (register env) [ a1; _1; _2; _4; _2a2 ];
merge env a1 _2;
fun env -> assert_bool "a+1 = 2 => 2*a+2 = 4" (is_equal env _2a2 _4)
@@ -72,7 +70,7 @@ let solve0c _ =
run @@ fun env ->
let a = fresh env Ty.real "ar" in
let b = fresh env Ty.real "br" in
- let _1 = LRA.RealValue.cst Q.one in
+ let _1 = LRA.RealValue.cst A.one in
let a1 = LRA.add env a _1 in
let b1 = LRA.add env b _1 in
register env a1;
@@ -83,10 +81,10 @@ let solve0c _ =
let solve1 _ =
run @@ fun env ->
let a, b = Shuffle.seq2 (fresh env Ty.real) ("ar", "br") in
- let _1 = LRA.RealValue.cst Q.one in
+ let _1 = LRA.RealValue.cst A.one in
let a1 = LRA.add env a _1 in
let b1 = LRA.add env b _1 in
- let _2 = LRA.RealValue.cst (Q.of_int 2) in
+ let _2 = LRA.RealValue.cst (A.of_int 2) in
let a2 = LRA.add env a _2 in
let b2 = LRA.add env b _2 in
Shuffle.seql' (register env) [ a1; b1; a2; b2 ];
@@ -96,10 +94,10 @@ let solve1 _ =
let solve2 _ =
run @@ fun env ->
let a, b = Shuffle.seq2 (fresh env Ty.real) ("ar", "br") in
- let _1 = LRA.RealValue.cst Q.one in
+ let _1 = LRA.RealValue.cst A.one in
let a1 = LRA.add env a _1 in
let b1 = LRA.add env b _1 in
- let _2 = LRA.RealValue.cst (Q.of_int 2) in
+ let _2 = LRA.RealValue.cst (A.of_int 2) in
let a2 = LRA.add env a _2 in
let b2 = LRA.add env b _2 in
Shuffle.seql' (register env) [ a1; b1; a2; b2 ];
@@ -109,11 +107,11 @@ let solve2 _ =
let solve3 _ =
run @@ fun env ->
let a, b = Shuffle.seq2 (fresh env Ty.real) ("ar", "br") in
- let _1 = LRA.RealValue.cst Q.one in
+ let _1 = LRA.RealValue.cst A.one in
let b1 = LRA.add env b _1 in
- let _2 = LRA.RealValue.cst (Q.of_int 2) in
+ let _2 = LRA.RealValue.cst (A.of_int 2) in
let a2 = LRA.add env a _2 in
- let _3 = LRA.RealValue.cst (Q.of_int 3) in
+ let _3 = LRA.RealValue.cst (A.of_int 3) in
Shuffle.seql
[
(fun () ->
@@ -131,15 +129,15 @@ let solve3 _ =
let solve4 _ =
run @@ fun env ->
let a, b, c = Shuffle.seq3 (fresh env Ty.real) ("ar", "br", "cr") in
- let t1 = LRA.RealValue.cst (Q.of_int 2) in
+ let t1 = LRA.RealValue.cst (A.of_int 2) in
let t1 = LRA.add env t1 c in
let t1 = LRA.add env a t1 in
- let t1' = LRA.RealValue.cst (Q.of_int 1) in
+ let t1' = LRA.RealValue.cst (A.of_int 1) in
let t1' = LRA.add env b t1' in
let t2 = a in
- let t2' = LRA.RealValue.cst (Q.of_int 2) in
+ let t2' = LRA.RealValue.cst (A.of_int 2) in
let t2' = LRA.add env t2' b in
- let t3' = LRA.RealValue.cst (Q.of_int (-3)) in
+ let t3' = LRA.RealValue.cst (A.of_int (-3)) in
Shuffle.seql
[
(fun () ->
@@ -160,9 +158,9 @@ let solve5 _ =
let c = fresh env Ty.real "cr" in
let t1 = LRA.sub env b c in
let t1 = LRA.add env a t1 in
- let t1' = LRA.RealValue.cst (Q.of_int 2) in
+ let t1' = LRA.RealValue.cst (A.of_int 2) in
let t2 = a in
- let t2' = LRA.RealValue.cst (Q.of_int 2) in
+ let t2' = LRA.RealValue.cst (A.of_int 2) in
let t3 = LRA.add env b c in
let t3' = LRA.add env b b in
Shuffle.seql
@@ -189,9 +187,9 @@ let mult0 _ =
let t1 = LRA.sub env a b in
let t1' = LRA.mult env a b in
let t2 = a in
- let t2' = LRA.RealValue.cst (Q.of_int 1) in
- let t3 = LRA.mult_cst env (Q.of_int 2) b in
- let t3' = LRA.RealValue.cst (Q.of_int 1) in
+ let t2' = LRA.RealValue.cst (A.of_int 1) in
+ let t3 = LRA.mult_cst env (A.of_int 2) b in
+ let t3' = LRA.RealValue.cst (A.of_int 1) in
Shuffle.seql
[
(fun () ->
@@ -216,9 +214,9 @@ let mult1 _ =
let t1' = LRA.add env b c in
let t1' = LRA.mult env t1' a in
let t2 = a in
- let t2' = LRA.RealValue.cst (Q.of_int 2) in
+ let t2' = LRA.RealValue.cst (A.of_int 2) in
let t3 = c in
- let t3' = LRA.RealValue.cst (Q.of_int 1) in
+ let t3' = LRA.RealValue.cst (A.of_int 1) in
Shuffle.seql
[
(fun () ->
diff --git a/src_colibri2/theories/FP/fp_value.ml b/src_colibri2/theories/FP/fp_value.ml
index b0d616b7db9c4ce84b4b97c9b18ce2c1439b4e01..85f19507a2204d601e65b7096b993981d3b8715a 100644
--- a/src_colibri2/theories/FP/fp_value.ml
+++ b/src_colibri2/theories/FP/fp_value.ml
@@ -36,7 +36,6 @@ module Float = Value.Register (F)
include Float
let cst' c = index c
-
let cst c = node (cst' c)
let debug =
@@ -93,7 +92,8 @@ let compute_ground d t =
match Ground.sem t with
| { app = { builtin = Expr.Real_to_fp (ew, prec); _ }; args; _ } ->
let m, r = IArray.extract2_exn args in
- !<(F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m !>>>r)
+ let r = match !>>>r with Q q -> q | A _ -> assert false (* TODO *) in
+ !<(F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m r)
| { app = { builtin = Expr.Fp_to_fp (_ew1, _prec1, ew2, prec2); _ }; args; _ }
->
let m, f1 = IArray.extract2_exn args in
@@ -125,7 +125,7 @@ let compute_ground d t =
(Colibri2_theories_LRA.RealValue.unsigned_bitv (ew + prec) !>>>bv))
| { app = { builtin = Expr.To_real (_ew, _prec); _ }; args; _ } ->
let r = IArray.extract1_exn args in
- !<<<(F.to_q !>r)
+ !<<<(A.of_q (F.to_q !>r))
| { app = { builtin = Expr.Plus_infinity (ew, prec); _ }; args; _ } ->
assert (IArray.is_empty args);
!<(F.inf ~ew ~mw:(prec - 1) false)
@@ -254,8 +254,11 @@ let converter d (f : Ground.t) =
Debug.dprintf2 debug "[FP] assign a value to %a" Node.pp a;
attach d
(set r
- (let+ va = getq a in
- F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m va))
+ (let* va = getq a in
+ match va with
+ | Q va -> Some (F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m va)
+ | A _ -> None
+ (* TODO *)))
| { app = { builtin = Expr.NaN (ew, prec); _ }; args; _ } ->
assert (IArray.is_empty args);
merge (cst (F.nan ~ew ~mw:(prec - 1)))
diff --git a/src_colibri2/theories/LRA/LRA.mli b/src_colibri2/theories/LRA/LRA.mli
index 5c4bcd55d4a7bc319fb1d2b25c54ccf4a4547e7d..f408dfea11252abea55132f01df1a4b0d5630ab6 100644
--- a/src_colibri2/theories/LRA/LRA.mli
+++ b/src_colibri2/theories/LRA/LRA.mli
@@ -19,12 +19,10 @@
(*************************************************************************)
module RealValue : sig
- include Value.S with type s = Q.t
-
- val cst' : Q.t -> t
-
- val cst : Q.t -> Node.t
+ include Value.S with type s = A.t
+ val cst' : A.t -> t
+ val cst : A.t -> Node.t
val zero : Node.t
end
@@ -32,24 +30,14 @@ val th_register : Egraph.wt -> unit
(** helpers to remove *)
-val add' : _ Egraph.t -> Q.t -> Node.t -> Q.t -> Node.t -> Node.t
-
+val add' : _ Egraph.t -> A.t -> Node.t -> A.t -> Node.t -> Node.t
val add : _ Egraph.t -> Node.t -> Node.t -> Node.t
-
val sub : _ Egraph.t -> Node.t -> Node.t -> Node.t
-
-val mult_cst : _ Egraph.t -> Q.t -> Node.t -> Node.t
-
+val mult_cst : _ Egraph.t -> A.t -> Node.t -> Node.t
val mult : _ Egraph.t -> Node.t -> Node.t -> Node.t
-
val gt_zero : _ Egraph.t -> Node.t -> Node.t
-
val ge_zero : _ Egraph.t -> Node.t -> Node.t
-
val lt : _ Egraph.t -> Node.t -> Node.t -> Node.t
-
val le : _ Egraph.t -> Node.t -> Node.t -> Node.t
-
val gt : _ Egraph.t -> Node.t -> Node.t -> Node.t
-
val ge : _ Egraph.t -> Node.t -> Node.t -> Node.t
diff --git a/src_colibri2/theories/LRA/delta.ml b/src_colibri2/theories/LRA/delta.ml
index b508b5a5b01a482c7c27cfbabbb1604262be844d..130c89299f8f0432bdaeb09c1e2e58f0e61b0c61 100644
--- a/src_colibri2/theories/LRA/delta.ml
+++ b/src_colibri2/theories/LRA/delta.ml
@@ -22,62 +22,50 @@
doesn't compute distances *)
module Edge = struct
-
module T = struct
- type t = {
- src: Node.t;
- dst: Node.t;
- }
- [@@deriving ord, eq, hash]
-
-
- let pp fmt t =
- Fmt.pf fmt "%a -> %a" Node.pp t.src Node.pp t.dst
+ type t = { src : Node.t; dst : Node.t } [@@deriving ord, eq, hash]
+ let pp fmt t = Fmt.pf fmt "%a -> %a" Node.pp t.src Node.pp t.dst
end
include T
- include Colibri2_popop_lib.Popop_stdlib.MkDatatype(T)
-
+ include Colibri2_popop_lib.Popop_stdlib.MkDatatype (T)
end
module Dist = struct
- type t = { q: Q.t; bound: Bound.t }
- [@@deriving show]
+ type t = { q : A.t; bound : Bound.t } [@@deriving show]
let min d1 d2 =
- let c = Q.compare d1.q d2.q in
+ let c = A.compare d1.q d2.q in
if c = 0 then
- let bound = match d1.bound, d2.bound with
- | Large, Large -> Bound.Large
- | _ -> Strict
+ let bound =
+ match (d1.bound, d2.bound) with
+ | Large, Large -> Bound.Large
+ | _ -> Strict
in
{ q = d1.q; bound }
- else if c < 0 then d1 else d2
+ else if c < 0 then d1
+ else d2
let included d1 d2 =
- let c = Q.compare d1.q d2.q in
+ let c = A.compare d1.q d2.q in
if c = 0 then
- match d1.bound, d2.bound with
- | Large, Strict -> false
- | _ -> true
+ match (d1.bound, d2.bound) with Large, Strict -> false | _ -> true
else c < 0
-
end
-module HEdge = Datastructure.Hashtbl(Edge)
+module HEdge = Datastructure.Hashtbl (Edge)
let edges = HEdge.create Dist.pp "Delta.edges"
(* src - dst <= q *)
let ty_real = Ground.Ty.convert Expr.Ty.Var.M.empty Expr.Ty.real
-
let a = Expr.Term.Var.mk "a" Expr.Ty.real
let ta = Expr.Term.of_var a
-let floor_pattern = (* Other floor functions? *)
- Colibri2_theories_quantifiers.Pattern.of_term
- ~subst:Ground.Subst.empty
+let floor_pattern =
+ (* Other floor functions? *)
+ Colibri2_theories_quantifiers.Pattern.of_term ~subst:Ground.Subst.empty
(Expr.Term.Real.floor_to_int ta)
(* let ceiling_patterns =
@@ -85,52 +73,57 @@ let floor_pattern = (* Other floor functions? *)
* (Expr.Term.Real.ceiling ta) *)
let ceiling_pattern =
- Colibri2_theories_quantifiers.Pattern.of_term
- ~subst:Ground.Subst.empty
- (Expr.Term.Int.minus (Expr.Term.Real.floor_to_int (Expr.Term.Real.minus ta)))
-
+ Colibri2_theories_quantifiers.Pattern.of_term ~subst:Ground.Subst.empty
+ (Expr.Term.Int.minus
+ (Expr.Term.Real.floor_to_int (Expr.Term.Real.minus ta)))
let event d src dst =
- match HEdge.find_opt edges d { src; dst },
- HEdge.find_opt edges d { dst; src } with
- | Some d1, Some d2 ->
+ match
+ (HEdge.find_opt edges d { src; dst }, HEdge.find_opt edges d { dst; src })
+ with
+ | Some d1, Some d2 ->
let aux src dst d1 d2 =
- if Dist.included d1 { q = Q.one; bound = Strict } &&
- Dist.included d2 { q = Q.zero; bound = Large } then
+ if
+ Dist.included d1 { q = A.one; bound = Strict }
+ && Dist.included d2 { q = A.zero; bound = Large }
+ then
if Dom_interval.is_integer d src then
(* 0 <= src - dst < 1 => src:Int => src = ceil(dst) *)
let s =
Colibri2_theories_quantifiers.Pattern.check_term_exists d
- { Ground.Subst.empty with term = Expr.Term.Var.M.singleton a dst }
- ceiling_pattern in
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.singleton a dst;
+ }
+ ceiling_pattern
+ in
Node.S.iter (Egraph.merge d src) s
else if Dom_interval.is_integer d dst then
(* 0 <= src - dst < 1 => dst:Int => dst = floor(src) *)
let s =
Colibri2_theories_quantifiers.Pattern.check_term_exists d
- { Ground.Subst.empty with term = Expr.Term.Var.M.singleton a src }
- floor_pattern in
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.singleton a src;
+ }
+ floor_pattern
+ in
Node.S.iter (Egraph.merge d dst) s
in
aux src dst d1 d2;
aux dst src d2 d1
- | _ -> ()
+ | _ -> ()
let add d src q bound dst =
let d' = { Dist.q; bound } in
HEdge.change
- (function
- | Some d ->
- Some (Dist.min d d')
- | None -> Some d')
- edges d {src;dst};
+ (function Some d -> Some (Dist.min d d') | None -> Some d')
+ edges d { src; dst };
(* Could be only when a change append *)
event d src dst
-
let add_le d src q dst = add d src q Large dst
let add_lt d src q dst = add d src q Strict dst
let add_ge d src q dst = add d dst q Large src
let add_gt d src q dst = add d dst q Strict src
-
let th_register _ = ()
diff --git a/src_colibri2/theories/LRA/delta.mli b/src_colibri2/theories/LRA/delta.mli
index b54fef6b21f8b05b415ad95ed21d4314b748cac5..6e0459004f67360c485d3146e3c3c3adb046ad74 100644
--- a/src_colibri2/theories/LRA/delta.mli
+++ b/src_colibri2/theories/LRA/delta.mli
@@ -20,21 +20,25 @@
(** Distance Graph *)
-
-val add_le: Egraph.wt -> Node.t -> Q.t -> Node.t -> unit
+val add_le : Egraph.wt -> Node.t -> A.t -> Node.t -> unit
(* [add_le d n1 q n2] n1 - n2 <= q *)
-val add_lt: Egraph.wt -> Node.t -> Q.t -> Node.t -> unit
+val add_lt : Egraph.wt -> Node.t -> A.t -> Node.t -> unit
(* [add_lt d n1 q n2] n1 - n2 < q *)
-val add_ge: Egraph.wt -> Node.t -> Q.t -> Node.t -> unit
+val add_ge : Egraph.wt -> Node.t -> A.t -> Node.t -> unit
(* [add_ge d n1 q n2] n1 - n2 >= q *)
-val add_gt: Egraph.wt -> Node.t -> Q.t -> Node.t -> unit
+val add_gt : Egraph.wt -> Node.t -> A.t -> Node.t -> unit
(* [add_gt d n1 q n2] n1 - n2 > q *)
-val add: Egraph.wt -> Node.t -> Q.t -> Colibri2_theories_LRA_stages_def.Bound.t -> Node.t -> unit
+val add :
+ Egraph.wt ->
+ Node.t ->
+ A.t ->
+ Colibri2_theories_LRA_stages_def.Bound.t ->
+ Node.t ->
+ unit
(* [add d n1 q bound n2] n1 - n2 <= q or < q *)
-val th_register: Egraph.wt -> unit
-
+val th_register : Egraph.wt -> unit
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index 4cd18bef6ab46015d381ca27447c7432e6d14d7d..84cc524771ad33ad890da9f18dd2a8abe969aab3 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -40,7 +40,6 @@ include Dom.Lattice (struct
include D
let key = dom
-
let inter _ d1 d2 = inter d1 d2
let is_singleton _ d =
@@ -62,7 +61,7 @@ let is_zero_or_positive d n =
let is_not_zero d n =
match Egraph.get_dom d dom n with
| None -> false
- | Some p -> D.absent Q.zero p
+ | Some p -> D.absent A.zero p
let is_strictly_positive d n =
match Egraph.get_dom d dom n with
@@ -80,9 +79,8 @@ let is_strictly_negative d n =
| D.Gt -> true
| D.Eq | D.Le | D.Ge | D.Lt | D.Uncomparable -> false)
-let assume_negative d n = upd_dom d n (D.lt Q.zero)
-
-let assume_positive d n = upd_dom d n (D.gt Q.zero)
+let assume_negative d n = upd_dom d n (D.lt A.zero)
+let assume_positive d n = upd_dom d n (D.gt A.zero)
let zero_is d n =
let r =
@@ -125,9 +123,7 @@ module ChoLRA = struct
end
let choice = ChoLRA.choice
-
let neg_cmp = function `Lt -> `Ge | `Le -> `Gt | `Ge -> `Lt | `Gt -> `Le
-
let com_cmp = function `Lt -> `Gt | `Le -> `Ge | `Ge -> `Le | `Gt -> `Lt
let backward = function
@@ -141,11 +137,8 @@ module Propagate = struct
open Monad
let setb = setv Boolean.dom
-
let getb = getv Boolean.dom
-
let set = updd upd_dom
-
let get = getd dom
let sub d ~r ~a ~b =
@@ -233,10 +226,10 @@ module Propagate = struct
attach d
(set r
(let+ va = get a in
- D.mult_cst Q.minus_one va)
+ D.mult_cst A.minus_one va)
&& set a
(let+ vr = get r in
- D.mult_cst Q.minus_one vr))
+ D.mult_cst A.minus_one vr))
| { app = { builtin = Expr.Lt }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
cmp d `Lt ~r ~a ~b
@@ -276,7 +269,7 @@ let init env =
(if D.is_integer inter then
Interp.SeqLim.of_seq d
(Base.Sequence.filter_map RealValue.int_sequence ~f:(fun z ->
- let q = Q.of_bigint z in
+ let q = A.of_bigint z in
if D.mem q inter then Some RealValue.(nodevalue (cst' q))
else None))
else
diff --git a/src_colibri2/theories/LRA/dom_interval.mli b/src_colibri2/theories/LRA/dom_interval.mli
index 108d1a0636ca4d9a29d9339c096bb4037bfe8457..8c230330ac716b16c0a5850092a6cf1eac6d35de 100644
--- a/src_colibri2/theories/LRA/dom_interval.mli
+++ b/src_colibri2/theories/LRA/dom_interval.mli
@@ -23,31 +23,20 @@ val init : Egraph.wt -> unit
module D : sig
include Colibri2_theories_LRA_stages_def.Interval_sig.S
- val get_convexe_hull : t -> (Q.t * Bound.t) option * (Q.t * Bound.t) option
-
- val from_convexe_hull : (Q.t * Bound.t) option * (Q.t * Bound.t) option -> t
+ val get_convexe_hull : t -> (A.t * Bound.t) option * (A.t * Bound.t) option
+ val from_convexe_hull : (A.t * Bound.t) option * (A.t * Bound.t) option -> t
end
val dom : D.t Dom.Kind.t
-
val get_dom : _ Egraph.t -> Node.t -> D.t option
-
val upd_dom : Egraph.wt -> Node.t -> D.t -> unit
-
val is_zero_or_positive : _ Egraph.t -> Node.t -> bool
-
val is_not_zero : _ Egraph.t -> Node.t -> bool
-
val is_strictly_positive : _ Egraph.t -> Node.t -> bool
-
val is_strictly_negative : _ Egraph.t -> Node.t -> bool
-
val is_integer : _ Egraph.t -> Node.t -> bool
-
val zero_is : _ Egraph.t -> Node.t -> D.is_comparable
-
val assume_positive : Egraph.wt -> Node.t -> unit
-
val assume_negative : Egraph.wt -> Node.t -> unit
module Propagate : sig
diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml
index db5b7dfdffadc70460d32d0caa0a8231972fccc5..e6b5dcfd2054e17ee52384c08e278381a994a789 100644
--- a/src_colibri2/theories/LRA/dom_polynome.ml
+++ b/src_colibri2/theories/LRA/dom_polynome.ml
@@ -60,12 +60,10 @@ include Pivot.Total (struct
let name = "LRA.polynome"
- type data = Q.t
+ type data = A.t
let nodes p = p.poly
-
- let of_one_node n = monome Q.one n
-
+ let of_one_node n = monome A.one n
let subst p n q = fst (subst p n q)
let normalize p ~f =
@@ -90,12 +88,12 @@ include Pivot.Total (struct
| Cst c ->
(* 0 = cst <> 0 *)
Debug.dprintf2 Debug.contradiction
- "[LRA/Poly] Found 0 = %a when merging" Q.pp c;
+ "[LRA/Poly] Found 0 = %a when merging" A.pp c;
Contradiction
| Var (q, x, p') ->
- assert (not (Q.equal Q.zero q));
+ assert (not (A.equal A.zero q));
(* diff = qx + p' *)
- Subst (x, Polynome.mult_cst (Q.div Q.one (Q.neg q)) p')
+ Subst (x, Polynome.mult_cst (A.div A.one (A.neg q)) p')
end)
let node_of_polynome d p =
@@ -119,17 +117,17 @@ let converter d (f : Ground.t) =
let a, b = IArray.extract2_exn args in
reg a;
reg b;
- assume_equality d res (Polynome.of_list Q.zero [ (a, Q.one); (b, Q.one) ])
+ assume_equality d res (Polynome.of_list A.zero [ (a, A.one); (b, A.one) ])
| { app = { builtin = Expr.Sub }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
reg a;
reg b;
assume_equality d res
- (Polynome.of_list Q.zero [ (a, Q.one); (b, Q.minus_one) ])
+ (Polynome.of_list A.zero [ (a, A.one); (b, A.minus_one) ])
| { app = { builtin = Expr.Minus }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
reg a;
- assume_equality d res (Polynome.of_list Q.zero [ (a, Q.minus_one) ])
+ assume_equality d res (Polynome.of_list A.zero [ (a, A.minus_one) ])
| _ -> ()
let init env =
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index 5fac1540159d6ae44cb7c8f273c6f3dc7831e9e5..1b61a57f466445fcf24be0c77459427e8527d60d 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/src_colibri2/theories/LRA/dom_product.ml
@@ -86,11 +86,8 @@ let set d cl ~old_abs ~old_sign abs sign =
module rec SolveAbs : sig
val assume_equality : Egraph.wt -> Node.t -> Product.t -> unit
-
val init : Egraph.wt -> unit
-
val get_repr : _ Egraph.t -> Node.t -> Product.t option
-
val iter_eqs : _ Egraph.t -> Node.t -> f:(Product.t -> unit) -> unit
val attach_repr_change :
@@ -104,7 +101,6 @@ end = Pivot.WithUnsolved (struct
include Product
let pp fmt p = Fmt.pf fmt "|%a|" pp p
-
let of_one_node _ n = Product.monome n Q.one
let subst p n q =
@@ -178,11 +174,8 @@ end)
and SolveSign : sig
val assume_equality : Egraph.wt -> Node.t -> Sign_product.t -> unit
-
val init : Egraph.wt -> unit
-
val get_repr : _ Egraph.t -> Node.t -> Sign_product.t option
-
val iter_eqs : _ Egraph.t -> Node.t -> f:(Sign_product.t -> unit) -> unit
val attach_repr_change :
@@ -262,15 +255,15 @@ let factorize res a coef b d _ =
| ONE, PLUS_ONE -> (Q.add v cst, acc)
| ONE, MINUS_ONE -> (Q.sub v cst, acc)
| NODE n, NODE n' when Egraph.is_equal d n n' ->
- (cst, (n, v) :: acc)
+ (cst, (n, A.of_q v) :: acc)
| _ ->
let n = node_of_product d abs sign in
Egraph.register d n;
- (cst, (n, v) :: acc))
+ (cst, (n, A.of_q v) :: acc))
(Q.zero, [])
[ (pa, sa, Q.one); (pb, sb, coef) ]
in
- let p = Polynome.of_list cst l in
+ let p = Polynome.of_list (A.of_q cst) l in
let n = Dom_polynome.node_of_polynome d p in
let pp_coef fmt coef =
if Q.equal Q.one coef then Fmt.pf fmt "+" else Fmt.pf fmt "-"
@@ -349,9 +342,9 @@ let init env =
match Dom_polynome.get_repr d n with
| None -> ()
| Some p ->
- if Q.equal p.cst Q.zero && Node.M.is_num_elt 1 p.poly then
+ if A.equal p.cst A.zero && Node.M.is_num_elt 1 p.poly then
let cl, q = Node.M.choose p.poly in
- if Q.equal q Q.one then (
+ if A.equal q A.one then (
let p1 = Product.of_list [ (cl, Q.one) ] in
Debug.dprintf4 debug "[Polynome->Product] propagate %a is %a"
Node.pp n Node.pp cl;
@@ -366,7 +359,7 @@ let init env =
SolveSign.iter_eqs d n ~f:(fun p ->
match Sign_product.is_one_node p with
| Some cl' when Egraph.is_equal d cl cl' ->
- let p1 = Polynome.of_list Q.zero [ (cl, Q.one) ] in
+ let p1 = Polynome.of_list A.zero [ (cl, A.one) ] in
Debug.dprintf4 debug
"[Product->Polynome] propagate %a is %a" Node.pp n Node.pp
cl;
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 1ddd70a4b0878554656c70a1387257d92992280b..57a14ad7851ba03f1643aba69097a58cceac6270 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -30,7 +30,6 @@ let debug =
Debug.register_info_flag ~desc:"Reasoning about <= < in LRA" "fourier"
let stats_run = Debug.register_stats_int "Fourier.run"
-
let stats_time = Debug.register_stats_time "Fourier.time"
type eq = { p : Polynome.t; bound : Bound.t; origins : Ground.S.t }
@@ -40,7 +39,7 @@ type eq = { p : Polynome.t; bound : Bound.t; origins : Ground.S.t }
let divide d (p : Polynome.t) =
try
(match Polynome.is_cst p with None -> () | Some _ -> raise Exit);
- if Q.sign p.cst <> 0 then raise Exit;
+ if A.sign p.cst <> 0 then raise Exit;
let l = Node.M.bindings p.poly in
let l =
List.fold_left
@@ -55,7 +54,7 @@ let divide d (p : Polynome.t) =
[] l
in
(* Debug.dprintf4 debug "@[eq:%a@ %a@]" Polynome.pp p
- * Fmt.(list ~sep:(any "+") (using CCPair.swap (pair Q.pp Product.pp)))
+ * Fmt.(list ~sep:(any "+") (using CCPair.swap (pair A.pp Product.pp)))
* l; *)
match l with
| [] -> raise Exit
@@ -85,17 +84,17 @@ let divide d (p : Polynome.t) =
let abs = Product.div abs common in
let pos, sign = Sign_product.extract_cst sign in
let v =
- match pos with Zero -> Q.zero | Pos -> v | Neg -> Q.neg v
+ match pos with Zero -> A.zero | Pos -> v | Neg -> A.neg v
in
match (Product.classify abs, Sign_product.classify sign) with
| _, MINUS_ONE -> assert false
- | ONE, PLUS_ONE -> (Q.add v cst, acc)
+ | ONE, PLUS_ONE -> (A.add v cst, acc)
| NODE n, NODE n' when Egraph.is_equal d n n' ->
(cst, (n, v) :: acc)
| _ ->
let n = Dom_product.node_of_product d abs sign in
(cst, (n, v) :: acc))
- (Q.zero, []) l
+ (A.zero, []) l
in
Some (Polynome.of_list cst l, common)
with Exit -> None
@@ -104,10 +103,10 @@ let delta d eq =
(* add info to delta *)
if Node.M.is_num_elt 2 eq.p.poly then
match Node.M.bindings eq.p.poly with
- | [ (src, a); (dst, b) ] when Q.equal Q.one a && Q.equal Q.minus_one b ->
- Delta.add d src (Q.neg eq.p.cst) eq.bound dst
- | [ (dst, b); (src, a) ] when Q.equal Q.one a && Q.equal Q.minus_one b ->
- Delta.add d src (Q.neg eq.p.cst) eq.bound dst
+ | [ (src, a); (dst, b) ] when A.equal A.one a && A.equal A.minus_one b ->
+ Delta.add d src (A.neg eq.p.cst) eq.bound dst
+ | [ (dst, b); (src, a) ] when A.equal A.one a && A.equal A.minus_one b ->
+ Delta.add d src (A.neg eq.p.cst) eq.bound dst
| _ -> ()
let apply d ~f truth g =
@@ -140,7 +139,7 @@ let add_eq d eqs p bound origins =
let eq = { p; bound; origins } in
delta d eq;
eq :: eqs
- | Some p, Bound.Large when Q.sign p = 0 ->
+ | Some p, Bound.Large when A.sign p = 0 ->
Ground.S.iter
(fun g ->
let truth = Base.Option.value_exn (Boolean.is d (Ground.node g)) in
@@ -150,8 +149,8 @@ let add_eq d eqs p bound origins =
| Strict
when Dom_interval.is_integer d a
&& Dom_interval.is_integer d b ->
- Polynome.of_list Q.minus_one [ (b, Q.one) ]
- | Large -> Polynome.monome Q.one b
+ Polynome.of_list A.minus_one [ (b, A.one) ]
+ | Large -> Polynome.monome A.one b
| Strict -> assert false
in
Debug.dprintf4 debug "[LRA/Fourier] Found %a = %a" Node.pp a
@@ -159,30 +158,30 @@ let add_eq d eqs p bound origins =
Dom_polynome.assume_equality d a p))
origins;
eqs
- | Some p, _ when Q.sign p < 0 ->
+ | Some p, _ when A.sign p < 0 ->
Debug.dprintf2 debug "[Fourier] discard %a" Ground.S.pp origins;
eqs
| Some p, bound ->
- Debug.dprintf6 Debug.contradiction "[LRA/Fourier] Found %a%a0 by %a" Q.pp
+ Debug.dprintf6 Debug.contradiction "[LRA/Fourier] Found %a%a0 by %a" A.pp
p Bound.pp bound Ground.S.pp origins;
Egraph.contradiction d
let mk_eq d bound a b =
let ( ! ) n =
match Dom_polynome.get_repr d n with
- | None -> Polynome.monome Q.one (Egraph.find_def d n)
+ | None -> Polynome.monome A.one (Egraph.find_def d n)
| Some p -> p
in
let p, bound' =
match bound with
| Bound.Strict
when Dom_interval.is_integer d a && Dom_interval.is_integer d b ->
- (Polynome.add_cst (Polynome.sub !a !b) Q.one, Bound.Large)
+ (Polynome.add_cst (Polynome.sub !a !b) A.one, Bound.Large)
| _ -> (Polynome.sub !a !b, bound)
in
( p,
bound',
- Polynome.sub (Polynome.monome Q.one a) (Polynome.monome Q.one b),
+ Polynome.sub (Polynome.monome A.one a) (Polynome.monome A.one b),
bound )
let make_equations d (eqs, vars) g =
@@ -218,7 +217,7 @@ let fm (d : Egraph.wt) =
match Node.M.find_opt n eq.p.poly with
| None -> split n positive negative (eq :: absent) l
| Some q ->
- if Q.sign q > 0 then split n ((q, eq) :: positive) negative absent l
+ if A.sign q > 0 then split n ((q, eq) :: positive) negative absent l
else split n positive ((q, eq) :: negative) absent l)
in
let rec aux eqs vars =
@@ -233,8 +232,8 @@ let fm (d : Egraph.wt) =
let eqs =
Lists.fold_product
(fun eqs (pq, peq) (nq, neq) ->
- let q = Q.div pq (Q.neg nq) in
- let p = Polynome.cx_p_cy Q.one peq.p q neq.p in
+ let q = A.div pq (A.neg nq) in
+ let p = Polynome.cx_p_cy A.one peq.p q neq.p in
let bound =
match (peq.bound, neq.bound) with
| Large, Large -> Bound.Large
@@ -287,7 +286,6 @@ module Daemon = struct
type runable = unit
let print_runable = Unit.pp
-
let run d () = fm d
end
diff --git a/src_colibri2/theories/LRA/polynome.ml b/src_colibri2/theories/LRA/polynome.ml
index d9aca9efd583d65b53008fa6e7094c89d2bc1b71..e8d19adbcabb6529448c067a97441fc39e28d2b8 100644
--- a/src_colibri2/theories/LRA/polynome.ml
+++ b/src_colibri2/theories/LRA/polynome.ml
@@ -23,11 +23,11 @@ open Colibri2_core
let print_poly fmt poly =
let print_not_1 first fmt q =
- if (not first) && Q.compare q Q.zero >= 0 then
+ if (not first) && A.compare q A.zero >= 0 then
Format.pp_print_string fmt "+";
- if Q.equal q Q.zero then Format.pp_print_string fmt "!0!"
- else if Q.equal Q.minus_one q then Format.pp_print_string fmt "-"
- else if not (Q.equal Q.one q) then Q.pp fmt q
+ if A.equal q A.zero then Format.pp_print_string fmt "!0!"
+ else if A.equal A.minus_one q then Format.pp_print_string fmt "-"
+ else if not (A.equal A.one q) then A.pp fmt q
in
let print_mono k v (fmt, first) =
Format.fprintf fmt "@[%a%a@]@," (print_not_1 first) v Node.pp k;
@@ -37,14 +37,14 @@ let print_poly fmt poly =
first
module T = struct
- type t = { cst : Q.t; poly : Q.t Node.M.t } [@@deriving eq, ord, hash]
+ type t = { cst : A.t; poly : A.t Node.M.t } [@@deriving eq, ord, hash]
let pp fmt v =
let print_not_0 first fmt q =
- if first then Q.pp fmt q
- else if not (Q.equal Q.zero q) then (
- if Q.compare q Q.zero > 0 then Format.pp_print_string fmt "+";
- Q.pp fmt q)
+ if first then A.pp fmt q
+ else if not (A.equal A.zero q) then (
+ if A.compare q A.zero > 0 then Format.pp_print_string fmt "+";
+ A.pp fmt q)
in
Format.fprintf fmt "@[";
@@ -57,22 +57,20 @@ include Popop_stdlib.MkDatatype (T)
(** different invariant *)
-let invariant p = Node.M.for_all (fun _ q -> not (Q.equal q Q.zero)) p.poly
+let invariant p = Node.M.for_all (fun _ q -> not (A.equal q A.zero)) p.poly
(** constructor *)
let cst q = { cst = q; poly = Node.M.empty }
-let zero = cst Q.zero
-
+let zero = cst A.zero
let is_cst p = if Node.M.is_empty p.poly then Some p.cst else None
+let is_zero p = A.equal p.cst A.zero && Node.M.is_empty p.poly
-let is_zero p = Q.equal p.cst Q.zero && Node.M.is_empty p.poly
-
-type extract = Zero | Cst of Q.t | Var of Q.t * Node.t * t
+type extract = Zero | Cst of A.t | Var of A.t * Node.t * t
let extract p =
if Node.M.is_empty p.poly then
- if Q.equal p.cst Q.zero then Zero else Cst p.cst
+ if A.equal p.cst A.zero then Zero else Cst p.cst
else
(* max binding is more interesting than choose (min binding) because it
force results to be choosen as pivot*)
@@ -83,80 +81,79 @@ let extract p =
type kind = ZERO | CST | VAR
let classify p =
- if Node.M.is_empty p.poly then if Q.equal p.cst Q.zero then ZERO else CST
+ if Node.M.is_empty p.poly then if A.equal p.cst A.zero then ZERO else CST
else VAR
let monome c x =
- if Q.equal Q.zero c then cst Q.zero
- else { cst = Q.zero; poly = Node.M.singleton x c }
+ if A.equal A.zero c then cst A.zero
+ else { cst = A.zero; poly = Node.M.singleton x c }
let is_one_node p =
(* cst = 0 and one empty monome *)
- if Q.equal Q.zero p.cst && Node.M.is_num_elt 1 p.poly then
+ if A.equal A.zero p.cst && Node.M.is_num_elt 1 p.poly then
let node, k = Node.M.choose p.poly in
- if Q.equal Q.one k then Some node else None
+ if A.equal A.one k then Some node else None
else None
-let sub_cst p q = { p with cst = Q.sub p.cst q }
-
-let add_cst p q = { p with cst = Q.add p.cst q }
+let sub_cst p q = { p with cst = A.sub p.cst q }
+let add_cst p q = { p with cst = A.add p.cst q }
let mult_cst c p1 =
- if Q.equal Q.one c then p1
+ if A.equal A.one c then p1
else
- let poly_mult c m = Node.M.map (fun c1 -> Q.mul c c1) m in
- if Q.equal Q.zero c then cst Q.zero
- else { cst = Q.mul c p1.cst; poly = poly_mult c p1.poly }
+ let poly_mult c m = Node.M.map (fun c1 -> A.mul c c1) m in
+ if A.equal A.zero c then cst A.zero
+ else { cst = A.mul c p1.cst; poly = poly_mult c p1.poly }
-let none_zero c = if Q.equal Q.zero c then None else Some c
+let none_zero c = if A.equal A.zero c then None else Some c
(** Warning Node.M.union can be used only for defining an operation [op]
that verifies [op 0 p = p] and [op p 0 = p] *)
let add p1 p2 =
let poly_add m1 m2 =
- Node.M.union (fun _ c1 c2 -> none_zero (Q.add c1 c2)) m1 m2
+ Node.M.union (fun _ c1 c2 -> none_zero (A.add c1 c2)) m1 m2
in
- { cst = Q.add p1.cst p2.cst; poly = poly_add p1.poly p2.poly }
+ { cst = A.add p1.cst p2.cst; poly = poly_add p1.poly p2.poly }
let sub p1 p2 =
let poly_sub m1 m2 =
Node.M.union_merge
(fun _ c1 c2 ->
match c1 with
- | None -> Some (Q.neg c2)
- | Some c1 -> none_zero (Q.sub c1 c2))
+ | None -> Some (A.neg c2)
+ | Some c1 -> none_zero (A.sub c1 c2))
m1 m2
in
- { cst = Q.sub p1.cst p2.cst; poly = poly_sub p1.poly p2.poly }
+ { cst = A.sub p1.cst p2.cst; poly = poly_sub p1.poly p2.poly }
let x_p_cy p1 c p2 =
- assert (not (Q.equal c Q.zero));
- let f a b = Q.add a (Q.mul c b) in
+ assert (not (A.equal c A.zero));
+ let f a b = A.add a (A.mul c b) in
let poly m1 m2 =
Node.M.union_merge
(fun _ c1 c2 ->
match c1 with
- | None -> Some (Q.mul c c2)
+ | None -> Some (A.mul c c2)
| Some c1 -> none_zero (f c1 c2))
m1 m2
in
{ cst = f p1.cst p2.cst; poly = poly p1.poly p2.poly }
let cx_p_cy c1 p1 c2 p2 =
- let c1_iszero = Q.equal c1 Q.zero in
- let c2_iszero = Q.equal c2 Q.zero in
+ let c1_iszero = A.equal c1 A.zero in
+ let c2_iszero = A.equal c2 A.zero in
if c1_iszero && c2_iszero then zero
else if c1_iszero then p2
else if c2_iszero then p1
else
- let f e1 e2 = Q.add (Q.mul c1 e1) (Q.mul c2 e2) in
+ let f e1 e2 = A.add (A.mul c1 e1) (A.mul c2 e2) in
let poly m1 m2 =
Node.M.merge
(fun _ e1 e2 ->
match (e1, e2) with
| None, None -> assert false
- | None, Some e2 -> Some (Q.mul c2 e2)
- | Some e1, None -> Some (Q.mul c1 e1)
+ | None, Some e2 -> Some (A.mul c2 e2)
+ | Some e1, None -> Some (A.mul c1 e1)
| Some e1, Some e2 -> none_zero (f e1 e2))
m1 m2
in
@@ -165,33 +162,32 @@ let cx_p_cy c1 p1 c2 p2 =
let subst_node p x y =
let poly, qo = Node.M.find_remove x p.poly in
match qo with
- | None -> (p, Q.zero)
+ | None -> (p, A.zero)
| Some q ->
let poly =
Node.M.change
- (function None -> qo | Some q' -> none_zero (Q.add q q'))
+ (function None -> qo | Some q' -> none_zero (A.add q q'))
y poly
in
({ p with poly }, q)
let subst p x s =
let poly, q = Node.M.find_remove x p.poly in
- match q with None -> (p, Q.zero) | Some q -> (x_p_cy { p with poly } q s, q)
+ match q with None -> (p, A.zero) | Some q -> (x_p_cy { p with poly } q s, q)
let fold f acc p = Node.M.fold_left f acc p.poly
-
let iter f p = Node.M.iter f p.poly
let of_list cst l =
let fold acc (node, q) =
Node.M.change
- (function None -> Some q | Some q' -> none_zero (Q.add q q'))
+ (function None -> Some q | Some q' -> none_zero (A.add q q'))
node acc
in
{ cst; poly = List.fold_left fold Node.M.empty l }
let of_map cst poly =
- assert (Node.M.for_all (fun _ q -> not (Q.equal Q.zero q)) poly);
+ assert (Node.M.for_all (fun _ q -> not (A.equal A.zero q)) poly);
{ cst; poly }
module ClM = Extmap.Make (Node)
@@ -206,19 +202,23 @@ let get_tree p =
p.cst )
let normalize p =
- if Node.M.is_empty p.poly then cst (Q.of_int (Q.sign p.cst))
+ if Node.M.is_empty p.poly then cst (A.of_int (A.sign p.cst))
else
let init =
- if Q.equal Q.zero p.cst then snd (Node.M.choose p.poly) else p.cst
+ if A.equal A.zero p.cst then snd (Node.M.choose p.poly) else p.cst
in
let num, den =
Node.M.fold_left
- (fun (num, den) _ q -> (Z.gcd num q.Q.num, Z.gcd den q.Q.den))
- (init.Q.num, init.Q.den) p.poly
+ (fun (num, den) _ (q : A.t) ->
+ ( (match q with Q q -> Z.gcd num q.num | A _ -> num),
+ match q with Q q -> Z.gcd den q.den | A _ -> den ))
+ ( (match init with Q q -> q.num | A _ -> Z.one),
+ match init with Q q -> q.den | A _ -> Z.one )
+ p.poly
in
if Z.equal Z.one num && Z.equal Z.one den then p
else
- let conv q = Q.make (Z.divexact q.Q.num num) (Z.divexact q.Q.den den) in
+ let conv q = A.mul (A.of_z den) (A.div (A.of_z num) q) in
{ poly = Node.M.map conv p.poly; cst = conv p.cst }
let print_poly fmt poly =
diff --git a/src_colibri2/theories/LRA/polynome.mli b/src_colibri2/theories/LRA/polynome.mli
index 2d5aa6c3981b464ae33aad58a73c0ee404af6263..0f82ee508d6f5d5c47c924c49a89a0bfc9662cea 100644
--- a/src_colibri2/theories/LRA/polynome.mli
+++ b/src_colibri2/theories/LRA/polynome.mli
@@ -23,66 +23,47 @@ open Colibri2_popop_lib
open Colibri2_core
(** Polynome *)
-type t = private { cst : Q.t; poly : Q.t Node.M.t }
+type t = private { cst : A.t; poly : A.t Node.M.t }
include Popop_stdlib.Datatype with type t := t
val invariant : t -> bool
-
val zero : t
-
val is_zero : t -> bool
-
-val cst : Q.t -> t
-
-val is_cst : t -> Q.t option
-
-val monome : Q.t -> Node.t -> t
-
+val cst : A.t -> t
+val is_cst : t -> A.t option
+val monome : A.t -> Node.t -> t
val is_one_node : t -> Node.t option
type extract =
| Zero (** p = 0 *)
- | Cst of Q.t (** p = q *)
- | Var of Q.t * Node.t * t (** p = qx + p' *)
+ | Cst of A.t (** p = q *)
+ | Var of A.t * Node.t * t (** p = qx + p' *)
val extract : t -> extract
type kind = ZERO | CST | VAR
val classify : t -> kind
-
-val sub_cst : t -> Q.t -> t
-
-val add_cst : t -> Q.t -> t
-
-val mult_cst : Q.t -> t -> t
-
+val sub_cst : t -> A.t -> t
+val add_cst : t -> A.t -> t
+val mult_cst : A.t -> t -> t
val add : t -> t -> t
-
val sub : t -> t -> t
-
-val of_list : Q.t -> (Node.t * Q.t) list -> t
-
-val of_map : Q.t -> Q.t Node.M.t -> t
-
-val x_p_cy : t -> Q.t -> t -> t
-
-val cx_p_cy : Q.t -> t -> Q.t -> t -> t
-
-val subst : t -> Node.t -> t -> t * Q.t
-
-val subst_node : t -> Node.t -> Node.t -> t * Q.t
-
-val fold : ('a -> Node.t -> Q.t -> 'a) -> 'a -> t -> 'a
-
-val iter : (Node.t -> Q.t -> unit) -> t -> unit
+val of_list : A.t -> (Node.t * A.t) list -> t
+val of_map : A.t -> A.t Node.M.t -> t
+val x_p_cy : t -> A.t -> t -> t
+val cx_p_cy : A.t -> t -> A.t -> t -> t
+val subst : t -> Node.t -> t -> t * A.t
+val subst_node : t -> Node.t -> Node.t -> t * A.t
+val fold : ('a -> Node.t -> A.t -> 'a) -> 'a -> t -> 'a
+val iter : (Node.t -> A.t -> unit) -> t -> unit
type 'a tree = Empty | Node of 'a tree * Node.t * 'a * 'a tree * int
-val get_tree : t -> Q.t tree * Q.t
+val get_tree : t -> A.t tree * A.t
val normalize : t -> t
(** divide by the pgcd *)
-val print_poly : Q.t Node.M.t Fmt.t
+val print_poly : A.t Node.M.t Fmt.t
diff --git a/src_colibri2/theories/LRA/product.ml b/src_colibri2/theories/LRA/product.ml
index 87cef75a21c1dea5ab8e0afbcf0bfcbce4a64eb4..2652156e8e8dae84b6fe49b0c37793c221461bfa 100644
--- a/src_colibri2/theories/LRA/product.ml
+++ b/src_colibri2/theories/LRA/product.ml
@@ -182,7 +182,6 @@ let subst p x s =
match q with None -> (p, Q.zero) | Some q -> (x_m_yc { poly } s q, q)
let fold f acc p = Node.M.fold_left f acc p.poly
-
let iter f p = Node.M.iter f p.poly
let of_list (* cst *) l =
diff --git a/src_colibri2/theories/LRA/product.mli b/src_colibri2/theories/LRA/product.mli
index 32c5916cf3f6f2a293eba5fe6227ca6259bb2fc2..042123e4a42132a429177c31b97f5ba353e523e5 100644
--- a/src_colibri2/theories/LRA/product.mli
+++ b/src_colibri2/theories/LRA/product.mli
@@ -28,13 +28,9 @@ type t = private { (* cst : Q.t; *) poly : Q.t Node.M.t }
include Popop_stdlib.Datatype with type t := t
val invariant : t -> bool
-
val one : t
-
val monome : Node.t -> Q.t -> t
-
val is_one_node : t -> Node.t option
-
val remove : Node.t -> t -> t
type extract =
@@ -46,27 +42,16 @@ val extract : t -> extract
type kind = ONE | NODE of Node.t | PRODUCT
val classify : t -> kind
-
val power_cst : Q.t -> t -> t
-
val of_list : (Node.t * Q.t) list -> t
-
val mul : t -> t -> t
-
val div : t -> t -> t
-
val x_m_yc : t -> t -> Q.t -> t
-
val xc_m_yc : t -> Q.t -> t -> Q.t -> t
-
val subst : t -> Node.t -> t -> t * Q.t
-
val subst_node : t -> Node.t -> Node.t -> t * Q.t
-
val fold : ('a -> Node.t -> Q.t -> 'a) -> 'a -> t -> 'a
-
val iter : (Node.t -> Q.t -> unit) -> t -> unit
-
val of_map : Q.t Node.M.t -> t
val common : t -> t -> t
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index a33543f22766f4c910ba939796dead289f1d14d8..5b4b7bedc712842b3e092749f8f1183b555578e8 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -146,9 +146,9 @@ module Builtin = struct
end
module RealValue = Value.Register (struct
- include Q
+ include A
- let name = "Q"
+ let name = "A"
end)
include RealValue
@@ -156,13 +156,16 @@ include RealValue
let () =
Interp.Register.print_value_smt RealValue.key (fun _ fmt v ->
let v = RealValue.value v in
- if Z.equal v.den Z.one then Z.pp_print fmt v.num
- else Fmt.pf fmt "(/ %a %a)" Z.pp_print v.num Z.pp_print v.den)
+ match v with
+ | Q v ->
+ if Z.equal v.den Z.one then Z.pp_print fmt v.num
+ else Fmt.pf fmt "(/ %a %a)" Z.pp_print v.num Z.pp_print v.den
+ | A v -> Fmt.pf fmt "(epsilon x. %s)" (Ocaml_poly.A.to_string v))
-let cst' c = index ~basename:(Format.asprintf "%aR" Q.pp c) c
+let cst' c = index ~basename:(Format.asprintf "%aR" A.pp c) c
let cst c = node (cst' c)
-let zero = cst Q.zero
-let one = cst Q.one
+let zero = cst A.zero
+let one = cst A.one
let positive_int_sequence =
let open Base.Sequence.Generator in
@@ -182,7 +185,8 @@ let int_sequence = Base.Sequence.shift_right int_sequence_without_zero Z.zero
let q_sequence d =
let open Interp.SeqLim in
let+ num = of_seq d int_sequence and* den = of_seq d positive_int_sequence in
- Q.make num den
+ (** algebraic non rational are not generated *)
+ A.of_q (Q.make num den)
let init_ty d =
Interp.Register.ty d (fun d ty ->
@@ -190,20 +194,20 @@ let init_ty d =
| { app = { builtin = Expr.Int; _ }; _ } ->
Some
(Interp.SeqLim.map (Interp.SeqLim.of_seq d int_sequence)
- ~f:(fun i -> nodevalue (cst' (Q.of_bigint i))))
+ ~f:(fun i -> nodevalue (cst' (A.of_bigint i))))
| { app = { builtin = Expr.Real; _ }; _ } ->
let seq = q_sequence d in
let seq =
- Interp.SeqLim.unfold_with seq ~init:Q.S.empty ~f:(fun s v ->
- if Q.S.mem v s then Skip s
- else Yield (nodevalue (cst' v), Q.S.add v s))
+ Interp.SeqLim.unfold_with seq ~init:A.S.empty ~f:(fun s v ->
+ if A.S.mem v s then Skip s
+ else Yield (nodevalue (cst' v), A.S.add v s))
in
Some seq
| { app = { builtin = Expr.Bitv n; _ }; _ } ->
let open Base.Sequence.Generator in
let rec loop i =
if Z.numbits i <= n then
- yield (nodevalue (cst' (Q.of_bigint i))) >>= fun () ->
+ yield (nodevalue (cst' (A.of_bigint i))) >>= fun () ->
loop (Z.succ i)
else return ()
in
@@ -214,8 +218,8 @@ let init_ty d =
exception Wrong_arg
let unsigned_bitv n t =
- if not (Q.is_unsigned_integer n t) then raise Wrong_arg;
- t.Q.num
+ if not (A.is_unsigned_integer n t) then raise Wrong_arg;
+ A.to_z t
let signed_bitv n t = Z.signed_extract (unsigned_bitv n t) 0 n
@@ -231,14 +235,14 @@ module Check = struct
let r = if b then Boolean.values_true else Boolean.values_false in
`Some r
in
- let extract n t = !<(Q.of_bigint (Z.extract t 0 n)) in
+ let extract n t = !<(A.of_bigint (Z.extract t 0 n)) in
let from_bitv n t =
- let t' = Q.of_bigint t in
- if not (Q.is_unsigned_integer n t') then
+ let t' = A.of_bigint t in
+ if not (A.is_unsigned_integer n t') then
Fmt.epr "@[[BV] %s(%a) is not of size %i@]@."
(Z.format (Fmt.str "%%0+#%ib" n) t)
Z.pp_print t n;
- assert (Q.is_unsigned_integer n t');
+ assert (A.is_unsigned_integer n t');
!<t'
in
match Ground.sem t with
@@ -259,92 +263,92 @@ module Check = struct
!<(!>a)
| { app = { builtin = Expr.Integer s }; tyargs = []; args; ty = _ } ->
assert (IArray.is_empty args);
- !<(Q.of_string s)
+ !<(A.of_string s)
| { app = { builtin = Expr.Decimal s }; tyargs = []; args; ty = _ } ->
assert (IArray.is_empty args);
- !<(Q.of_string_decimal s)
+ !<(A.of_string_decimal s)
| { app = { builtin = Expr.Rational s }; tyargs = []; args; ty = _ } ->
assert (IArray.is_empty args);
- !<(Q.of_string_decimal s)
+ !<(A.of_string_decimal s)
| { app = { builtin = Expr.Add }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
- !<(Q.add !>a !>b)
+ !<(A.add !>a !>b)
| { app = { builtin = Expr.Sub }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
- !<(Q.sub !>a !>b)
+ !<(A.sub !>a !>b)
| { app = { builtin = Expr.Minus }; tyargs = []; args; ty = _ } ->
let a = IArray.extract1_exn args in
- !<(Q.neg !>a)
+ !<(A.neg !>a)
| { app = { builtin = Expr.Mul }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
- !<(Q.mul !>a !>b)
+ !<(A.mul !>a !>b)
| { app = { builtin = Expr.Div }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
- if Q.is_zero !>b then `Uninterp else !<(Q.div !>a !>b)
+ if A.is_zero !>b then `Uninterp else !<(A.div !>a !>b)
| { app = { builtin = Expr.Div_e }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
let b = !>b in
- let s = Q.sign b in
- if s = 0 then `Uninterp else !<(Q.div_e !>a b)
+ let s = A.sign b in
+ if s = 0 then `Uninterp else !<(A.div_e !>a b)
| { app = { builtin = Expr.Div_f }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
let b = !>b in
- let s = Q.sign b in
- if s = 0 then `Uninterp else !<(Q.div_f !>a b)
+ let s = A.sign b in
+ if s = 0 then `Uninterp else !<(A.div_f !>a b)
| { app = { builtin = Expr.Div_t }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
let b = !>b in
- let s = Q.sign b in
- if s = 0 then `Uninterp else !<(Q.div_t !>a b)
+ let s = A.sign b in
+ if s = 0 then `Uninterp else !<(A.div_t !>a b)
| { app = { builtin = Expr.Modulo_e }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
let b = !>b in
- let s = Q.sign b in
- if s = 0 then `Uninterp else !<(Q.mod_e !>a b)
+ let s = A.sign b in
+ if s = 0 then `Uninterp else !<(A.mod_e !>a b)
| { app = { builtin = Expr.Modulo_f }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
let b = !>b in
- let s = Q.sign b in
- if s = 0 then `Uninterp else !<(Q.mod_f !>a b)
+ let s = A.sign b in
+ if s = 0 then `Uninterp else !<(A.mod_f !>a b)
| { app = { builtin = Expr.Modulo_t }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
let b = !>b in
- let s = Q.sign b in
- if s = 0 then `Uninterp else !<(Q.mod_t !>a b)
+ let s = A.sign b in
+ if s = 0 then `Uninterp else !<(A.mod_t !>a b)
| { app = { builtin = Builtin.Pow_int_int }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
let a = !>a in
let b = !>b in
- if Q.sign b < 0 then `Uninterp else !<(Q.pow a (Q.to_int b))
+ if A.sign b < 0 then `Uninterp else !<(A.pow a (A.to_int b))
| { app = { builtin = Builtin.Pow_real_int }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
let a = !>a in
let b = !>b in
- if Q.sign b < 0 then `Uninterp else !<(Q.pow a (Q.to_int b))
+ if A.sign b < 0 then `Uninterp else !<(A.pow a (A.to_int b))
| { app = { builtin = Expr.Lt }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
- !<<(Q.lt !>a !>b)
+ !<<(A.lt !>a !>b)
| { app = { builtin = Expr.Leq }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
- !<<(Q.leq !>a !>b)
+ !<<(A.le !>a !>b)
| { app = { builtin = Expr.Gt }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
- !<<(Q.gt !>a !>b)
+ !<<(A.gt !>a !>b)
| { app = { builtin = Expr.Geq }; tyargs = []; args; ty = _ } ->
let a, b = IArray.extract2_exn args in
- !<<(Q.geq !>a !>b)
+ !<<(A.ge !>a !>b)
| { app = { builtin = Expr.Floor_to_int }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
- !<(Q.floor !>a)
+ !<(A.floor !>a)
| { app = { builtin = Expr.Abs }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
- !<(Q.abs !>a)
+ !<(A.abs !>a)
| { app = { builtin = Expr.Ceiling }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
- !<(Q.ceil !>a)
+ !<(A.ceil !>a)
| { app = { builtin = Expr.Floor }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
- !<(Q.floor !>a)
+ !<(A.floor !>a)
| { app = { builtin = Expr.Bitvec s }; tyargs = []; args; ty = _ } ->
assert (IArray.is_empty args);
from_bitv (String.length s) (Z.of_string_base 2 s)
@@ -493,10 +497,10 @@ module Check = struct
!<<(Z.geq (signed_bitv n a) (signed_bitv n b))
| { app = { builtin = Builtin.BV2Nat n }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
- !<(Q.of_bigint (bitv n a))
+ !<(A.of_bigint (bitv n a))
| { app = { builtin = Builtin.Int2BV n }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
- extract n !>a.num
+ extract n (A.to_z (!>a))
| _ -> `None
let init d =
@@ -507,11 +511,11 @@ module Check = struct
with
| { builtin = Expr.Int; _ }, None -> Wrong
| { builtin = Expr.Int; _ }, Some v
- when not (Q.is_integer (RealValue.value v)) ->
+ when not (A.is_integer (RealValue.value v)) ->
Wrong
| { builtin = Expr.Bitv _; _ }, None -> Wrong
| { builtin = Expr.Bitv n; _ }, Some v
- when not (Q.is_unsigned_integer n (RealValue.value v)) ->
+ when not (A.is_unsigned_integer n (RealValue.value v)) ->
Wrong
| _ -> (
let check r = Value.equal r (interp d (Ground.node t)) in
@@ -586,13 +590,13 @@ let converter d (f : Ground.t) =
Check.attach d f
| { app = { builtin = Expr.Integer s }; tyargs = []; args; _ } ->
assert (IArray.is_empty args);
- merge (cst (Q.of_string s))
+ merge (cst (A.of_string s))
| { app = { builtin = Expr.Decimal s }; tyargs = []; args; _ } ->
assert (IArray.is_empty args);
- merge (cst (Q.of_string_decimal s))
+ merge (cst (A.of_string_decimal s))
| { app = { builtin = Expr.Rational s }; tyargs = []; args; _ } ->
assert (IArray.is_empty args);
- merge (cst (Q.of_string_decimal s))
+ merge (cst (A.of_string_decimal s))
| { app = { builtin = Expr.Add }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
reg a;
@@ -601,13 +605,13 @@ let converter d (f : Ground.t) =
attach d
(set r
(let+ va = get a and+ vb = get b in
- Q.add va vb)
+ A.add va vb)
&& set a
(let+ vb = get b and+ vr = get r in
- Q.sub vr vb)
+ A.sub vr vb)
&& set b
(let+ va = get a and+ vr = get r in
- Q.sub vr va))
+ A.sub vr va))
| { app = { builtin = Expr.Sub }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
reg a;
@@ -616,13 +620,13 @@ let converter d (f : Ground.t) =
attach d
(set r
(let+ va = get a and+ vb = get b in
- Q.sub va vb)
+ A.sub va vb)
&& set a
(let+ vb = get b and+ vr = get r in
- Q.add vr vb)
+ A.add vr vb)
&& set b
(let+ va = get a and+ vr = get r in
- Q.sub va vr))
+ A.sub va vr))
| { app = { builtin = Expr.Mul }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
reg a;
@@ -631,13 +635,13 @@ let converter d (f : Ground.t) =
attach d
(set r
(let+ va = get a and+ vb = get b in
- Q.mul va vb)
+ A.mul va vb)
&& set a
(let* vb = get b and+ vr = get r in
- if Q.is_zero vb then None else Some (Q.div vr vb))
+ if A.is_zero vb then None else Some (A.div vr vb))
&& set b
(let* va = get a and+ vr = get r in
- if Q.is_zero va then None else Some (Q.div vr va)))
+ if A.is_zero va then None else Some (A.div vr va)))
| { app = { builtin = Expr.Div }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
reg a;
@@ -646,14 +650,14 @@ let converter d (f : Ground.t) =
attach d
(set r
(let* va = get a and+ vb = get b in
- if Q.is_zero vb then None else Some (Q.div va vb))
+ if A.is_zero vb then None else Some (A.div va vb))
&& set a
(let* vb = get b and+ vr = get r in
- if Q.is_zero vb then None else Some (Q.mul vr vb))
+ if A.is_zero vb then None else Some (A.mul vr vb))
&& (* if va is 0, and vr is not 0, b can't be not zero because vr would be 0. So b is 0. *)
set b
(let* va = get a and+ vr = get r in
- if Q.is_zero vr then None else Some (Q.div va vr)))
+ if A.is_zero vr then None else Some (A.div va vr)))
| { app = { builtin = Expr.Minus }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
reg a;
@@ -661,25 +665,25 @@ let converter d (f : Ground.t) =
attach d
(set r
(let+ va = get a in
- Q.neg va)
+ A.neg va)
&& set a
(let+ vr = get r in
- Q.neg vr))
+ A.neg vr))
| { app = { builtin = Expr.Lt }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
- cmp Q.lt a b;
+ cmp A.lt a b;
Check.attach d f
| { app = { builtin = Expr.Leq }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
- cmp Q.le a b;
+ cmp A.le a b;
Check.attach d f
| { app = { builtin = Expr.Gt }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
- cmp Q.gt a b;
+ cmp A.gt a b;
Check.attach d f
| { app = { builtin = Expr.Geq }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
- cmp Q.ge a b;
+ cmp A.ge a b;
Check.attach d f
| { app = { builtin = Expr.Floor_to_int }; tyargs = []; args; _ } ->
let a = IArray.extract1_exn args in
@@ -691,7 +695,7 @@ let converter d (f : Ground.t) =
Check.attach d f
| { app = { builtin = Expr.Bitvec s }; tyargs = []; args; ty = _ } ->
assert (IArray.is_empty args);
- merge (cst (Q.of_bigint (Z.of_string_base 2 s)))
+ merge (cst (A.of_bigint (Z.of_string_base 2 s)))
| { app = { builtin = Expr.Bitv_concat (_n, _m) }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
reg a;
diff --git a/src_colibri2/theories/LRA/realValue.mli b/src_colibri2/theories/LRA/realValue.mli
index 9b8794bd712213fdbb28597448c0881f2a9ace83..092aab0c570a44b9bd31e29d1000474801c94b4a 100644
--- a/src_colibri2/theories/LRA/realValue.mli
+++ b/src_colibri2/theories/LRA/realValue.mli
@@ -22,26 +22,17 @@ module Builtin : sig
type _ Expr.t += BV2Nat of int
val abs_real : Colibri2_core.Expr.Term.Const.t
-
val abs_int : Colibri2_core.Expr.Term.Const.t
-
val bv2nat : int -> Colibri2_core.Expr.Term.Const.t
end
-include Value.S with type s = Q.t
-
-val cst' : Q.t -> t
-
-val cst : Q.t -> Node.t
+include Value.S with type s = A.t
+val cst' : A.t -> t
+val cst : A.t -> Node.t
val zero : Node.t
-
val init : Egraph.wt -> unit
-
val int_sequence : Z.t Base.Sequence.t
-
-val q_sequence : _ Egraph.t -> Q.t Interp.SeqLim.t
-
-val unsigned_bitv : int -> Q.t -> Z.t
-
-val signed_bitv : int -> Q.t -> Z.t
+val q_sequence : _ Egraph.t -> A.t Interp.SeqLim.t
+val unsigned_bitv : int -> A.t -> Z.t
+val signed_bitv : int -> A.t -> Z.t
diff --git a/src_colibri2/theories/LRA/simplex.ml b/src_colibri2/theories/LRA/simplex.ml
index 534aae787d467c8262731da08d32cd0d846eb79f..56edb11b5cfa9078b59d10cb173b86ec3148d1b5 100644
--- a/src_colibri2/theories/LRA/simplex.ml
+++ b/src_colibri2/theories/LRA/simplex.ml
@@ -31,16 +31,13 @@ let debug =
Debug.register_info_flag ~desc:"Reasoning about <= < in LRA" "simplex"
let stats_run = Debug.register_stats_int "Simplex.run"
-
let stats_maximization = Debug.register_stats_int "Simplex.maximization"
-
let stats_time = Debug.register_stats_time "Simplex.time"
module Var = struct
include Node
let is_int _ = false
-
let print = pp
end
@@ -48,45 +45,36 @@ module Ex = struct
type t = unit
let print fmt () = Fmt.pf fmt "()"
-
let empty = ()
-
let union () () = ()
end
module Rat = struct
- include Q
-
- let m_one = Q.of_int (-1)
-
- let print fmt t = Fmt.pf fmt "%s" (Q.to_string t)
-
- let is_int x = Z.equal Z.one x.Q.den
-
- let is_zero v = Q.equal v Q.zero
-
- let is_one v = Q.equal v Q.one
-
- let mult = Q.mul
-
- let minus = Q.neg
-
- let is_m_one v = Q.equal v m_one
+ include A
+
+ let m_one = A.minus_one
+ let print = A.pp
+ let is_int = A.is_integer
+ let is_zero v = A.equal v A.zero
+ let is_one v = A.equal v A.one
+ let mult = A.mul
+ let minus = A.neg
+ let is_m_one v = A.equal v m_one
end
module Sim = OcplibSimplex.Basic.Make (Var) (Rat) (Ex)
-type bound = No | Large of Q.t | Strict of Q.t
+type bound = No | Large of A.t | Strict of A.t
let pp_bound_inf fmt = function
| No -> ()
- | Large q -> Fmt.pf fmt "%a ≤" Q.pp q
- | Strict q -> Fmt.pf fmt "%a <" Q.pp q
+ | Large q -> Fmt.pf fmt "%a ≤" A.pp q
+ | Strict q -> Fmt.pf fmt "%a <" A.pp q
let pp_bound_sup fmt = function
| No -> ()
- | Large q -> Fmt.pf fmt "≤ %a" Q.pp q
- | Strict q -> Fmt.pf fmt "< %a" Q.pp q
+ | Large q -> Fmt.pf fmt "≤ %a" A.pp q
+ | Strict q -> Fmt.pf fmt "< %a" A.pp q
let to_bound = function
| None -> No
@@ -97,21 +85,21 @@ let inter_inf inf1 inf2 =
match (inf1, inf2) with
| No, inf | inf, No -> inf
| (Large q1, (Strict q2 as inf) | (Strict q2 as inf), Large q1)
- when Q.equal q1 q2 ->
+ when A.equal q1 q2 ->
inf
| ((Large q1 | Strict q1) as inf1), ((Strict q2 | Large q2) as inf2) ->
- if Q.leq q2 q1 then inf1 else inf2
+ if A.le q2 q1 then inf1 else inf2
let inter_sup inf1 inf2 =
match (inf1, inf2) with
| No, inf | inf, No -> inf
| (Large q1, (Strict q2 as inf) | (Strict q2 as inf), Large q1)
- when Q.equal q1 q2 ->
+ when A.equal q1 q2 ->
inf
| ((Large q1 | Strict q1) as inf1), ((Strict q2 | Large q2) as inf2) ->
- if Q.leq q2 q1 then inf2 else inf1
+ if A.le q2 q1 then inf2 else inf1
-type eq = { inf : bound; p : Q.t Node.M.t; sup : bound }
+type eq = { inf : bound; p : A.t Node.M.t; sup : bound }
let pp_eq fmt { inf; p; sup } =
Fmt.pf fmt "%a%a%a" pp_bound_inf inf Polynome.print_poly p pp_bound_sup sup
@@ -126,16 +114,16 @@ let delta d eq =
(* add info to delta *)
if Node.M.is_num_elt 2 eq.p then
match Node.M.bindings eq.p with
- | [ (src, a); (dst, b) ] when Q.equal Q.one a && Q.equal Q.minus_one b ->
+ | [ (src, a); (dst, b) ] when A.equal A.one a && A.equal A.minus_one b ->
add d src eq.sup dst;
add d dst eq.inf src
- | [ (dst, b); (src, a) ] when Q.equal Q.one a && Q.equal Q.minus_one b ->
+ | [ (dst, b); (src, a) ] when A.equal A.one a && A.equal A.minus_one b ->
add d src eq.sup dst;
add d dst eq.inf src
| _ -> ()
let add_eq _ eqs eq =
- let p = Polynome.of_map Q.zero eq.p in
+ let p = Polynome.of_map A.zero eq.p in
Polynome.H.change
(function
| None -> Some eq
@@ -152,14 +140,14 @@ let add_eq _ eqs eq =
let mk_eq _ p dom =
assert (not (Node.M.is_empty p.Polynome.poly));
let _, q = Node.M.choose p.poly in
- assert (not (Q.equal q Q.zero));
- let p = Polynome.mult_cst (Q.inv q) p in
+ assert (not (A.equal q A.zero));
+ let p = Polynome.mult_cst (A.inv q) p in
let inf, sup = Dom_interval.D.get_convexe_hull dom in
- let inf, sup = if Q.sign q < 0 then (sup, inf) else (inf, sup) in
+ let inf, sup = if A.sign q < 0 then (sup, inf) else (inf, sup) in
let translate = function
| No -> No
- | Strict c -> Strict (Q.sub (Q.div c q) p.cst)
- | Large c -> Large (Q.sub (Q.div c q) p.cst)
+ | Strict c -> Strict (A.sub (A.div c q) p.cst)
+ | Large c -> Large (A.sub (A.div c q) p.cst)
in
let inf = translate @@ to_bound inf in
let sup = translate @@ to_bound sup in
@@ -173,7 +161,7 @@ let make_equations d (eqs, vars) n =
| Some dom ->
let p =
match Dom_polynome.get_repr d n with
- | None -> Polynome.monome Q.one (Egraph.find_def d n)
+ | None -> Polynome.monome A.one (Egraph.find_def d n)
| Some p -> p
in
if Node.M.is_empty p.poly then (eqs, vars)
@@ -223,20 +211,20 @@ end
let of_bound_sup = function
| No -> None
| Large q ->
- assert (Q.is_real q);
- Some (q, Q.zero)
+ assert (A.is_real q);
+ Some (q, A.zero)
| Strict q ->
- assert (Q.is_real q);
- Some (q, Q.minus_one)
+ assert (A.is_real q);
+ Some (q, A.minus_one)
let of_bound_inf = function
| No -> None
| Large q ->
- assert (Q.is_real q);
- Some (q, Q.zero)
+ assert (A.is_real q);
+ Some (q, A.zero)
| Strict q ->
- assert (Q.is_real q);
- Some (q, Q.one)
+ assert (A.is_real q);
+ Some (q, A.one)
let find_equalities d vars (env : Sim.Core.t) (s : Sim.Core.solution Lazy.t) =
(* Env must be sat *)
@@ -257,7 +245,7 @@ let find_equalities d vars (env : Sim.Core.t) (s : Sim.Core.solution Lazy.t) =
(fun to_ ->
let is_int_to = Dom_interval.is_integer d to_ in
Edge.H.add_new Impossible under_approx { Edge.from; to_ }
- (is_int_from, is_int_to, Q.inf, Q.minus_inf))
+ (is_int_from, is_int_to, A.inf, A.minus_inf))
acc;
acc)
vars vars
@@ -266,22 +254,22 @@ let find_equalities d vars (env : Sim.Core.t) (s : Sim.Core.solution Lazy.t) =
let h = val_of_sol s in
Edge.H.filter_mapi
(fun { from; to_ } (is_int_from, is_int_to, inf, sup) ->
- let dist = Q.sub (Node.H.find h to_) (Node.H.find h from) in
+ let dist = A.sub (Node.H.find h to_) (Node.H.find h from) in
(* Debug.dprintf10 debug "[Simplex] under_approx: %a <= %a - %a <= %a : %a"
- * Q.pp inf Node.pp to_ Node.pp from Q.pp sup Q.pp dist; *)
- let inf = Q.min inf dist in
- let sup = Q.max sup dist in
+ * A.pp inf Node.pp to_ Node.pp from A.pp sup A.pp dist; *)
+ let inf = A.min inf dist in
+ let sup = A.max sup dist in
if is_int_from || is_int_to then
- if Q.le inf Q.minus_one || Q.le Q.one sup then None
+ if A.le inf A.minus_one || A.le A.one sup then None
else Some (is_int_from, is_int_to, inf, sup)
- else if Q.lt inf Q.zero || Q.lt Q.zero sup then None
+ else if A.lt inf A.zero || A.lt A.zero sup then None
else Some (is_int_from, is_int_to, inf, sup))
under_approx
in
let one_dist env is_int a b =
Debug.incr stats_maximization;
Debug.dprintf4 debug "Check max %a - %a" Node.pp a Node.pp b;
- let p = Sim.Core.P.from_list [ (a, Q.one); (b, Q.minus_one) ] in
+ let p = Sim.Core.P.from_list [ (a, A.one); (b, A.minus_one) ] in
let env, opt = Sim.Solve.maximize env p in
match Sim.Result.get opt env with
| Sim.Core.Unknown -> assert false
@@ -291,10 +279,10 @@ let find_equalities d vars (env : Sim.Core.t) (s : Sim.Core.solution Lazy.t) =
update_under_approx s;
(* s is often not interesting for the update; all at zero, so the
distance is pushed a little further *)
- let p' = Polynome.of_list Q.zero [ (a, Q.one); (b, Q.minus_one) ] in
+ let p' = Polynome.of_list A.zero [ (a, A.one); (b, A.minus_one) ] in
let n = Dom_polynome.node_of_polynome d p' in
let env', _ =
- Sim.Assert.poly env p n (of_bound_inf (Large (Q.of_int 2))) () None ()
+ Sim.Assert.poly env p n (of_bound_inf (Large (A.of_int 2))) () None ()
in
let env' = Sim.Solve.solve env' in
let s =
@@ -306,10 +294,10 @@ let find_equalities d vars (env : Sim.Core.t) (s : Sim.Core.solution Lazy.t) =
(`Distinct, env, s)
| Sim.Core.Max (m, s) ->
let m = Lazy.force m in
- (* Debug.dprintf2 debug "Max %a" Q.pp m.max_v; *)
+ (* Debug.dprintf2 debug "Max %a" A.pp m.max_v; *)
(if m.is_le then Delta.add_le else Delta.add_lt) d a m.max_v b;
let notdistinct =
- if is_int then Q.lt (Q.abs m.max_v) Q.one else Q.equal m.max_v Q.zero
+ if is_int then A.lt (A.abs m.max_v) A.one else A.equal m.max_v A.zero
in
if notdistinct then (`NotDistinct, env, s) else (`Distinct, env, s)
in
@@ -355,7 +343,7 @@ let update_domains d env =
let inf =
Base.Option.map
~f:(fun (q1, q2) ->
- let s = Q.sign q2 in
+ let s = A.sign q2 in
let b =
if s = 0 then Bound.Large
else if s > 0 then Strict
@@ -368,7 +356,7 @@ let update_domains d env =
let sup =
Base.Option.map
~f:(fun (q1, q2) ->
- let s = Q.sign q2 in
+ let s = A.sign q2 in
let b =
if s = 0 then Bound.Large
else if s < 0 then Strict
@@ -426,7 +414,7 @@ let simplex (d : Egraph.wt) =
Debug.dprintf2 debug "%a@." pp_eq eq;
if Node.M.is_num_elt 1 eq.p then (
let n, q = Node.M.choose eq.p in
- assert (Q.equal q Q.one);
+ assert (A.equal q A.one);
let inf = of_bound_inf eq.inf in
let sup = of_bound_sup eq.sup in
let env, _ = Sim.Assert.var env n inf () sup () in
@@ -434,7 +422,7 @@ let simplex (d : Egraph.wt) =
else
let inf = of_bound_inf eq.inf in
let sup = of_bound_sup eq.sup in
- let p = Polynome.of_map Q.zero eq.p in
+ let p = Polynome.of_map A.zero eq.p in
let n = Dom_polynome.node_of_polynome d p in
let vars = Node.S.add n vars in
let env, _ = Sim.Assert.poly env (of_poly p) n inf () sup () in
@@ -478,7 +466,6 @@ module DaemonSimplex = struct
type runable = unit
let print_runable = Unit.pp
-
let run d () = simplex d
end
@@ -532,7 +519,7 @@ let converter d (f : Ground.t) =
if Node.compare a b < 0 then (a, b, builtin)
else (b, a, ord_inv builtin)
in
- let p = Polynome.of_list Q.zero [ (a, Q.one); (b, Q.minus_one) ] in
+ let p = Polynome.of_list A.zero [ (a, A.one); (b, A.minus_one) ] in
let n = Dom_polynome.node_of_polynome d p in
if not (Node.HC.mem seen d n) then (
diff --git a/src_colibri2/theories/LRA/stages/dune b/src_colibri2/theories/LRA/stages/dune
index c5ba75543ee95a95ce7067351debe9fb7504ecfc..adbc8699013467fa4c2941a543124fca8a99c71e 100644
--- a/src_colibri2/theories/LRA/stages/dune
+++ b/src_colibri2/theories/LRA/stages/dune
@@ -2,7 +2,7 @@
(name colibri2_theories_LRA_stages)
(public_name colibri2.theories.LRA.stages)
(virtual_modules interval_domain)
- (libraries colibri2.popop_lib colibri2.theories.LRA.stages.def)
+ (libraries colibri2.popop_lib colibri2.theories.LRA.stages.def colibri2.stdlib)
(modules interval_domain)
)
@@ -10,7 +10,7 @@
(name colibri2_theories_LRA_stages_def)
(public_name colibri2.theories.LRA.stages.def)
(modules interval_sig bound)
- (libraries colibri2.popop_lib containers)
+ (libraries colibri2.popop_lib containers colibri2.stdlib)
(preprocess
(pps ppx_deriving.std ppx_hash))
)
diff --git a/src_colibri2/theories/LRA/stages/interval_sig.ml b/src_colibri2/theories/LRA/stages/interval_sig.ml
index f0894e63eefa33f3414b56584e2f9ea93cd63f88..b096d67b03e08af82b1e14c9bd16660a6932cf80 100644
--- a/src_colibri2/theories/LRA/stages/interval_sig.ml
+++ b/src_colibri2/theories/LRA/stages/interval_sig.ml
@@ -19,6 +19,7 @@
(*************************************************************************)
open Colibri2_popop_lib
+open Colibri2_stdlib.Std
module type S = sig
include Popop_stdlib.Datatype
@@ -28,51 +29,35 @@ module type S = sig
type is_comparable = Gt | Lt | Ge | Le | Eq | 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 mult_cst : A.t -> t -> t
+ val add_cst : A.t -> t -> t
val add : t -> t -> t
-
val minus : t -> t -> t
+ val mem : A.t -> t -> bool
- val mem : Q.t -> t -> bool
+ val singleton : A.t -> t
+ (** from A.t *)
- val singleton : Q.t -> t
- (** from Q.t *)
+ val is_singleton : t -> A.t option
+ val except : t -> A.t -> t option
- val is_singleton : t -> Q.t option
-
- val except : t -> Q.t -> t option
-
- type split_heuristic = Singleton of Q.t | Splitted of t * t | NotSplitted
+ type split_heuristic = Singleton of A.t | Splitted of t * t | NotSplitted
val split_heuristic : t -> split_heuristic
-
- val absent : Q.t -> t -> bool
-
+ val absent : A.t -> t -> bool
val is_integer : t -> bool
-
val integers : t
+ val gt : A.t -> t
+ val ge : A.t -> t
+ val lt : A.t -> t
- val gt : Q.t -> t
-
- val ge : Q.t -> t
-
- val lt : Q.t -> t
-
- val le : Q.t -> t
+ val le : A.t -> t
(** > q, >= q, < q, <= q *)
val le' : t -> t
-
val lt' : t -> t
-
val ge' : t -> t
-
val gt' : t -> t
val union : t -> t -> t
@@ -84,23 +69,21 @@ module type S = sig
*)
val zero : t
-
val reals : t
val is_reals : t -> bool
(** R *)
- val choose : t -> Q.t
+ val choose : t -> A.t
(** Nothing smart in this choosing *)
val invariant : t -> bool
- (* val choose_rnd : (int -> int) -> t -> Q.t
+ (* val choose_rnd : (int -> int) -> t -> A.t
* (\** choose an element randomly (but non-uniformly), the given function is
* the random generator *\)
*)
- val get_convexe_hull : t -> (Q.t * Bound.t) option * (Q.t * Bound.t) option
-
- val from_convexe_hull : (Q.t * Bound.t) option * (Q.t * Bound.t) option -> t
+ val get_convexe_hull : t -> (A.t * Bound.t) option * (A.t * Bound.t) option
+ val from_convexe_hull : (A.t * Bound.t) option * (A.t * Bound.t) option -> t
end
diff --git a/src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.ml b/src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.ml
index 4d538b1a900082d78b4f1faee7bcbc2a6ab99647..d7c1aebd54a36ba89c73965625c1e746a3b07790 100644
--- a/src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.ml
+++ b/src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.ml
@@ -49,7 +49,7 @@ include Colibri2_popop_lib.Popop_stdlib.MkDatatype (T)
let invariant t = Sign_domain.invariant t.sign
-type split_heuristic = Singleton of Q.t | Splitted of t * t | NotSplitted
+type split_heuristic = Singleton of A.t | Splitted of t * t | NotSplitted
let split_heuristic t =
match Sign_domain.split_heuristic t.sign with
@@ -61,16 +61,12 @@ let split_heuristic t =
| NotSplitted -> NotSplitted
let absent q t =
- ((not t.noninteger) && not (Q.is_integer q)) || Sign_domain.absent q t.sign
+ ((not t.noninteger) && not (A.is_integer q)) || Sign_domain.absent q t.sign
let le' t = { noninteger = true; sign = Sign_domain.le' t.sign }
-
let lt' t = { noninteger = true; sign = Sign_domain.lt' t.sign }
-
let ge' t = { noninteger = true; sign = Sign_domain.ge' t.sign }
-
let gt' t = { noninteger = true; sign = Sign_domain.gt' t.sign }
-
let is_distinct t1 t2 = Sign_domain.is_distinct t1.sign t2.sign
type is_comparable = Sign_domain.is_comparable =
@@ -89,7 +85,7 @@ let is_included t1 t2 =
let mult_cst q t =
{
- noninteger = t.noninteger && Q.is_not_zero q;
+ noninteger = t.noninteger && A.is_not_zero q;
sign = Sign_domain.mult_cst q t.sign;
}
@@ -108,10 +104,10 @@ let minus t1 t2 =
sign = Sign_domain.minus t1.sign t2.sign;
}
-let mem q t = (Q.is_integer q || t.noninteger) && Sign_domain.mem q t.sign
+let mem q t = (A.is_integer q || t.noninteger) && Sign_domain.mem q t.sign
let singleton q =
- { noninteger = not (Q.is_integer q); sign = Sign_domain.singleton q }
+ { noninteger = not (A.is_integer q); sign = Sign_domain.singleton q }
let is_singleton t = Sign_domain.is_singleton t.sign
@@ -121,11 +117,8 @@ let except t q =
| Some sign -> Some { noninteger = t.noninteger; sign }
let gt q = { noninteger = true; sign = Sign_domain.gt q }
-
let ge q = { noninteger = true; sign = Sign_domain.ge q }
-
let lt q = { noninteger = true; sign = Sign_domain.lt q }
-
let le q = { noninteger = true; sign = Sign_domain.le q }
let union t1 t2 =
@@ -140,15 +133,10 @@ let inter t1 t2 =
| None -> None
let zero = { noninteger = false; sign = Sign_domain.zero }
-
let reals = { noninteger = true; sign = Sign_domain.reals }
-
let integers = { noninteger = false; sign = Sign_domain.reals }
-
let is_reals t = t.noninteger && Sign_domain.is_reals t.sign
-
let choose t = Sign_domain.choose t.sign
-
let is_integer t = not t.noninteger
let get_convexe_hull t =
@@ -156,10 +144,10 @@ let get_convexe_hull t =
let checkint dir = function
| x when t.noninteger -> x
| None -> None
- | Some (z, Bound.Strict) when Q.is_zero z -> Some (dir, Large)
+ | Some (z, Bound.Strict) when A.is_zero z -> Some (dir, Large)
| x -> x
in
- (checkint Q.one inf, checkint Q.minus_one sup)
+ (checkint A.one inf, checkint A.minus_one sup)
let from_convexe_hull ch =
{ sign = Sign_domain.from_convexe_hull ch; noninteger = true }
diff --git a/src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.mli b/src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.mli
index 265e418b6ee3ed1051d1590b76e83cff5fac6818..f011060db037a4b5cf8ea609c7dfecd66f7db142 100644
--- a/src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.mli
+++ b/src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.mli
@@ -20,19 +20,13 @@
include Interval_sig.S
-type split_heuristic =
- | Singleton of Q.t
- | Splitted of t * t
- | NotSplitted
+type split_heuristic = Singleton of A.t | Splitted of t * t | NotSplitted
-val split_heuristic: t -> split_heuristic
-
-val absent: Q.t -> t -> bool
-
-val le': t -> t
-val lt': t -> t
-val ge': t -> t
-val gt': t -> t
-
-val is_integer: t -> bool
-val integers: t
+val split_heuristic : t -> split_heuristic
+val absent : A.t -> t -> bool
+val le' : t -> t
+val lt' : t -> t
+val ge' : t -> t
+val gt' : t -> t
+val is_integer : t -> bool
+val integers : t
diff --git a/src_colibri2/theories/LRA/stages/stage0/sign_domain.ml b/src_colibri2/theories/LRA/stages/stage0/sign_domain.ml
index 0b1574fab8f7a5d1bb6903c05339313341b0afbd..dc25fc92ab2b553ca71e9cc27d2ab69d838d62c2 100644
--- a/src_colibri2/theories/LRA/stages/stage0/sign_domain.ml
+++ b/src_colibri2/theories/LRA/stages/stage0/sign_domain.ml
@@ -50,34 +50,22 @@ include T
include Colibri2_popop_lib.Popop_stdlib.MkDatatype (T)
let invariant t = t.neg || t.zero || t.pos
-
let top = { pos = true; zero = true; neg = true }
-
let pos_or_zero = { pos = true; zero = true; neg = false }
-
let pos = { pos = true; zero = false; neg = false }
-
let neg_or_zero = { pos = false; zero = true; neg = true }
-
let neg = { pos = false; zero = false; neg = true }
-
let zero = { pos = false; zero = true; neg = false }
-
let one = { pos = true; zero = false; neg = false }
-
let non_zero = { pos = true; zero = false; neg = true }
-
let ge_zero v = not v.neg
-
let le_zero v = not v.pos
(* Bottom is a special value (`Bottom) in Eva, and need not be part of
the lattice. Here, we have a value which is equivalent to it, defined
there only for commodity. *)
let empty = { pos = false; zero = false; neg = false }
-
let is_empty t = equal t empty
-
let is_reals t = equal t top
(* Inclusion: test inclusion of each field. *)
@@ -103,20 +91,20 @@ let narrow v1 v2 =
if is_empty r then None else Some r
let mem q v =
- let c = Q.sign q in
+ let c = A.sign q in
(c = 0 && v.zero) || (c < 0 && v.neg) || (c > 0 && v.pos)
let absent q v =
- let c = Q.sign q in
+ let c = A.sign q in
(c = 0 && not v.zero) || (c < 0 && not v.neg) || (c > 0 && not v.pos)
let reals = top
(* [singleton] creates an abstract value corresponding to the singleton [i]. *)
let singleton i =
- if Q.lt i Q.zero then neg else if Q.gt i Q.zero then pos else zero
+ if A.lt i A.zero then neg else if A.gt i A.zero then pos else zero
-let is_singleton v = if equal v zero then Some Q.zero else None
+let is_singleton v = if equal v zero then Some A.zero else None
(** {2 Forward transfer functions} *)
@@ -126,7 +114,6 @@ let is_singleton v = if equal v zero then Some Q.zero else None
the functions [truncate_integer] and [rewrap_integer]. *)
let neg_unop v = { v with neg = v.pos; pos = v.neg }
-
let logical_not v = { pos = v.zero; neg = false; zero = v.pos || v.neg }
let add v1 v2 =
@@ -139,7 +126,7 @@ let add v1 v2 =
{ neg; pos; zero }
let add_cst q v =
- let c = Q.sign q in
+ let c = A.sign q in
if c = 0 then v
else if c > 0 then
{ neg = v.neg; zero = v.zero && v.neg; pos = v.pos || v.zero || v.neg }
@@ -154,7 +141,7 @@ let mul v1 v2 =
let minus v1 v2 = add v1 { neg = v2.pos; zero = v2.zero; pos = v2.neg }
let mult_cst q v =
- let c = Q.sign q in
+ let c = A.sign q in
if c = 0 then zero
else if c > 0 then v
else { neg = v.pos; zero = v.zero; pos = v.neg }
@@ -334,35 +321,34 @@ let is_included x y =
Bool.(x.neg <= y.neg && x.zero <= y.zero && x.pos <= y.pos)
let union = join
-
let inter = narrow
-type split_heuristic = Singleton of Q.t | Splitted of t * t | NotSplitted
+type split_heuristic = Singleton of A.t | Splitted of t * t | NotSplitted
let split_heuristic _ = NotSplitted
let except t x =
- if Q.sign x = 0 && t.zero then
+ if A.sign x = 0 && t.zero then
let t = { t with zero = false } in
if is_empty t then None else Some t
else Some t
-let choose t = if t.zero then Q.zero else if t.pos then Q.one else Q.minus_one
+let choose t = if t.zero then A.zero else if t.pos then A.one else A.minus_one
let le q =
- let c = Q.sign q in
+ let c = A.sign q in
if c < 0 then neg else if c = 0 then neg_or_zero else top
let lt q =
- let c = Q.sign q in
+ let c = A.sign q in
if c <= 0 then neg else top
let ge q =
- let c = Q.sign q in
+ let c = A.sign q in
if c < 0 then top else if c = 0 then pos_or_zero else pos
let gt q =
- let c = Q.sign q in
+ let c = A.sign q in
if c >= 0 then pos else top
let le' v =
@@ -374,25 +360,23 @@ let ge' v =
{ neg = v.neg; zero = v.zero || v.neg; pos = v.pos || v.zero || v.neg }
let gt' v = { neg = v.neg; zero = v.neg; pos = v.pos || v.zero || v.neg }
-
let integers = reals
-
let is_integer _ = false
let get_convexe_hull v =
let inf =
match (v.neg, v.zero, v.pos) with
| true, _, _ -> None
- | false, true, _ -> Some (Q.zero, Bound.Large)
- | false, false, true -> Some (Q.zero, Bound.Strict)
+ | false, true, _ -> Some (A.zero, Bound.Large)
+ | false, false, true -> Some (A.zero, Bound.Strict)
| false, false, false -> assert false
(* absurd: bottom *)
in
let sup =
match (v.neg, v.zero, v.pos) with
| _, _, true -> None
- | _, true, false -> Some (Q.zero, Bound.Large)
- | true, false, false -> Some (Q.zero, Bound.Strict)
+ | _, true, false -> Some (A.zero, Bound.Large)
+ | true, false, false -> Some (A.zero, Bound.Strict)
| false, false, false -> assert false
(* absurd: bottom *)
in
@@ -403,7 +387,7 @@ let from_convexe_hull (inf, sup) =
match inf with
| None -> reals
| Some (q, b) ->
- let s = Q.sign q in
+ let s = A.sign q in
if s > 0 then pos
else if s = 0 then
match b with Bound.Large -> pos_or_zero | Strict -> pos
@@ -413,7 +397,7 @@ let from_convexe_hull (inf, sup) =
match sup with
| None -> reals
| Some (q, b) ->
- let s = Q.sign q in
+ let s = A.sign q in
if s < 0 then neg
else if s = 0 then
match b with Bound.Large -> neg_or_zero | Strict -> neg
diff --git a/src_colibri2/theories/LRA/stages/stage2/union.ml b/src_colibri2/theories/LRA/stages/stage2/union.ml
index 2a71230d2c520bbe079f90dda832dbf6ace49a17..f15769f19f1ceee79e37b063df53ec6a45611141 100644
--- a/src_colibri2/theories/LRA/stages/stage2/union.ml
+++ b/src_colibri2/theories/LRA/stages/stage2/union.ml
@@ -21,8 +21,12 @@
open Colibri2_popop_lib
open Colibri2_stdlib.Std
+let compare_ord a b : Colibrics_lib.Ord.t =
+ let c = A.compare a b in
+ Int.(if c = 0 then Eq else if c <= 0 then Lt else Gt)
+
module P = Colibrics_lib.Interval.Union.Make (struct
- include Q
+ include A
let infix_eq = equal
let infix_lseq = le
@@ -31,22 +35,18 @@ module P = Colibrics_lib.Interval.Union.Make (struct
let infix_mn = sub
let infix_as = mul
let infix_sl = div
-
- let compare a b : Colibrics_lib.Ord.t =
- let c = Q.compare a b in
- Int.(if c = 0 then Eq else if c <= 0 then Lt else Gt)
-
- let of_int = Q.of_bigint
- let floor a = Z.fdiv a.num a.den
- let ceil a = Z.cdiv a.num a.den
+ let compare = compare_ord
+ let of_int = A.of_bigint
+ let floor a = A.to_z (A.floor a)
+ let ceil a = A.to_z (A.ceil a)
end)
open P
include struct
- type q = Q.t [@@deriving eq, ord, hash]
+ type q = A.t [@@deriving eq, ord, hash]
- let gen_q = Q.gen
+ let gen_q = A.gen
type bound = Colibrics_lib.Interval.Bound.t = Strict | Large
[@@deriving eq, ord, hash, qcheck]
@@ -70,7 +70,7 @@ include struct
let l =
List.sort_uniq l ~cmp:(fun a b ->
let extract = function `Sin q -> q | `End (q, _) -> q in
- -Q.compare (extract a) (extract b))
+ -A.compare (extract a) (extract b))
in
let rec convert acc = function
| [] -> acc
@@ -92,21 +92,21 @@ let print_bound fmt = function
let rec pp_on fmt = function
| Sin (q, on) ->
- Format.fprintf fmt "%a[∪]%a;" Q.pp q Q.pp q;
+ Format.fprintf fmt "%a[∪]%a;" A.pp q A.pp q;
pp_on fmt on
| End (q, b, off) ->
- Format.fprintf fmt "%a%a" Q.pp q print_bound b;
+ Format.fprintf fmt "%a%a" A.pp q print_bound b;
pp_off ~first:false fmt off
| Inf -> Format.fprintf fmt "+∞["
and pp_off ~first fmt = function
| Sin (q, off) ->
if not first then Format.fprintf fmt "∪";
- Format.fprintf fmt "{%a}" Q.pp q;
+ Format.fprintf fmt "{%a}" A.pp q;
pp_off ~first:false fmt off
| End (q, b, on) ->
if not first then Format.fprintf fmt "∪";
- Format.fprintf fmt "%a%a;" print_bound b Q.pp q;
+ Format.fprintf fmt "%a%a;" print_bound b A.pp q;
pp_on fmt on
| Inf -> ()
@@ -188,7 +188,7 @@ let to_bound : Bound.t -> Colibrics_lib.Interval.Bound.t = function
| Large -> Large
(** type invariant *)
-let get_convexe_hull : t -> (Q.t * Bound.t) option * (Q.t * Bound.t) option =
+let get_convexe_hull : t -> (A.t * Bound.t) option * (A.t * Bound.t) option =
fun t ->
let inf, sup = get_convexe_hull t.u in
let conv c = Base.Option.map ~f:(fun (q, b) -> (q, of_bound b)) c in
@@ -196,10 +196,10 @@ let get_convexe_hull : t -> (Q.t * Bound.t) option * (Q.t * Bound.t) option =
match (b, t.integrability) with
| x, MaybeReal -> x
| None, _ -> None
- | Some (z, Bound.Strict), _ when Q.is_integer z ->
- Some (Q.add (if dir then Q.one else Q.minus_one) z, Large)
- | Some (z, Bound.Large), _ when Q.is_integer z -> b
- | Some (z, _), _ -> Some ((if dir then Q.ceil else Q.floor) z, Large)
+ | Some (z, Bound.Strict), _ when A.is_integer z ->
+ Some (A.add (if dir then A.one else A.minus_one) z, Large)
+ | Some (z, Bound.Large), _ when A.is_integer z -> b
+ | Some (z, _), _ -> Some ((if dir then A.ceil else A.floor) z, Large)
in
(checkint true (conv inf), checkint false (conv sup))
@@ -208,22 +208,22 @@ let from_convexe_hull (c1, c2) : t =
let ch = (conv c1, conv c2) in
{ u = from_convexe_hull ch; integrability = MaybeReal }
-type split_heuristic = Singleton of Q.t | Splitted of t * t | NotSplitted
+type split_heuristic = Singleton of A.t | Splitted of t * t | NotSplitted
let split_heuristic _ = NotSplitted
-let choose : t -> Q.t =
+let choose : t -> A.t =
let get_first_on = function
- | Sin (q, _) | End (q, Strict, _) -> Q.sub q Q.one
+ | Sin (q, _) | End (q, Strict, _) -> A.sub q A.one
| End (q, Large, off) -> q
- | Inf -> Q.zero
+ | Inf -> A.zero
in
let get_after_on q' = function
| Sin (q, _) | End (q, Strict, _) ->
- let p = Q.sub q Q.one in
- if Q.lt q' p then p else Q.div_2exp (Q.add q' q) 1
+ let p = A.sub q A.one in
+ if A.lt q' p then p else A.div (A.add q' q) A.two
| End (q, Large, _) -> q
- | Inf -> Q.add q' Q.one
+ | Inf -> A.add q' A.one
in
let get_first_off = function
| Sin (q, _) | End (q, Large, _) -> q
@@ -243,7 +243,7 @@ let is_integer = function
let reals = { u = On Inf; integrability = MaybeReal }
let integers = { u = On Inf; integrability = Integer }
-let zero = { u = Off (Sin (Q.zero, Inf)); integrability = Integer }
+let zero = { u = Off (Sin (A.zero, Inf)); integrability = Integer }
let gt q = { u = gt q; integrability = MaybeReal }
let ge q = { u = ge q; integrability = MaybeReal }
let lt q = { u = lt q; integrability = MaybeReal }
@@ -285,14 +285,14 @@ let add t1 t2 =
}
let mem q t =
- (match t.integrability with Integer -> Q.is_integer q | MaybeReal -> true)
+ (match t.integrability with Integer -> A.is_integer q | MaybeReal -> true)
&& mem q t.u
let absent q t = not (mem q t)
let except t q =
match t.integrability with
- | Integer when not (Q.is_integer q) -> Some t
+ | Integer when not (A.is_integer q) -> Some t
| _ -> (
match except t.u q with
| Some u -> Some { integrability = t.integrability; u }
@@ -303,25 +303,26 @@ let add_cst q t =
u = add_cst t.u q;
integrability =
(match t.integrability with
- | Integer when Q.is_integer q -> Integer
+ | Integer when A.is_integer q -> Integer
| _ -> MaybeReal);
}
let singleton q =
{
u = singleton q;
- integrability = (if Q.is_integer q then Integer else MaybeReal);
+ integrability = (if A.is_integer q then Integer else MaybeReal);
}
let is_singleton t = is_singleton t.u
+let count = 20
-let%test "singleton" =
+let%test_unit "singleton" =
+ (* Ocaml_poly.PolyUtils.trace_enable "algebraic_number"; *)
let test =
- QCheck.Test.make_cell ~count:1000 (QCheck.make Q.gen) (fun q ->
- Option.is_some (is_singleton (singleton q)))
+ QCheck.Test.make_cell ~count (QCheck.make ~print:A.to_string A.gen)
+ (fun q -> Option.is_some (is_singleton (singleton q)))
in
- let res = QCheck.Test.check_cell test in
- QCheck.TestResult.is_success res
+ QCheck.Test.check_cell_exn test
let interesting_values acc =
let add q acc = q :: acc in
@@ -348,14 +349,14 @@ let%test_unit "gen_compare" =
let+ q =
oneofl
(interesting_values
- (interesting_values [ Q.zero; Q.one; Q.minus_one ] t2)
+ (interesting_values [ A.zero; A.one; A.minus_one ] t2)
t1)
in
(true_true, false_true, true_false, false_false, t1, t2, q)
in
let pp fmt (true_true, false_true, true_false, false_false, t1, t2, q) =
Fmt.pf fmt "%b %b %b %b: %a and %a at %a" true_true false_true true_false
- false_false pp_t' t1 pp_t' t2 Q.pp q
+ false_false pp_t' t1 pp_t' t2 A.pp q
in
let shrink (true_true, false_true, true_false, false_false, t1, t2, q) =
let open QCheck.Iter in
@@ -371,7 +372,7 @@ let%test_unit "gen_compare" =
in
let print x = Fmt.str "%a" pp x in
let test =
- QCheck.Test.make_cell ~name:"on interesting values" ~count:5000
+ QCheck.Test.make_cell ~name:"on interesting values" ~count
(QCheck.make ~small ~shrink ~print gen) ~max_fail:10
(fun (true_true, false_true, true_false, false_false, t1, t2, q) ->
let b1 = P.mem q t1 in
@@ -387,7 +388,7 @@ let%test_unit "gen_compare" =
let b' = test b1 b2 in
(* Format.printf "b = %b; b' = %b; b1 = %b; b2 = %b; %b; r=%a@." b b' b1
* b2
- * (Q.lt (Q.of_int 4) q)
+ * (A.lt (A.of_int 4) q)
* pp r; *)
(not b) || b')
in
@@ -418,29 +419,29 @@ let is_comparable t1 t2 =
if equal_integrability t1.integrability t2.integrability then Eq
else Uncomparable
-let rec mult_cst_pos (x : Q.t) (l : t'') : t'' =
+let rec mult_cst_pos (x : A.t) (l : t'') : t'' =
match l with
- | Sin (q, l') -> Sin (Q.(x * q), mult_cst_pos x l')
- | End (q, bv, l') -> End (Q.(x * q), bv, mult_cst_pos x l')
+ | Sin (q, l') -> Sin (A.(x * q), mult_cst_pos x l')
+ | End (q, bv, l') -> End (A.(x * q), bv, mult_cst_pos x l')
| Inf -> Inf
-let rec mult_cst_neg if_ (x : Q.t) (l0 : t'') (l : t'') : t' =
+let rec mult_cst_neg if_ (x : A.t) (l0 : t'') (l : t'') : t' =
match l with
- | Sin (q, l') -> mult_cst_neg if_ x (Sin (Q.(x * q), l0)) l'
+ | Sin (q, l') -> mult_cst_neg if_ x (Sin (A.(x * q), l0)) l'
| End (q, bv, l') ->
mult_cst_neg (not if_) x
- (End (Q.(x * q), Colibrics_lib__Interval__Bound.inv_bound bv, l0))
+ (End (A.(x * q), Colibrics_lib__Interval__Bound.inv_bound bv, l0))
l'
| Inf -> if if_ then On l0 else Off l0
let mult_cst x l =
let integrability =
match l.integrability with
- | Integer -> if Q.is_integer x then Integer else MaybeReal
+ | Integer -> if A.is_integer x then Integer else MaybeReal
| MaybeReal -> MaybeReal
in
- match Colibrics_lib__Q_extra.compare x Q.(of_int 0) with
- | Eq -> singleton Q.(of_int 0)
+ match compare_ord x A.(of_int 0) with
+ | Eq -> singleton A.(of_int 0)
| Lt -> (
match l.u with
| On l -> { u = mult_cst_neg true x Inf l; integrability }
@@ -452,33 +453,33 @@ let mult_cst x l =
let l = mult_cst_pos x l in
{ u = Off l; integrability })
-let minus a b = add a (mult_cst Q.minus_one b)
+let minus a b = add a (mult_cst A.minus_one b)
let%test_unit "mult_cst" =
let gen =
let open QCheck.Gen in
- let* t1 = gen and* cst = Q.gen in
+ let* t1 = gen and* cst = A.gen in
let+ q =
- oneofl (interesting_values [ Q.zero; Q.one; Q.minus_one; cst ] t1.u)
+ oneofl (interesting_values [ A.zero; A.one; A.minus_one; cst ] t1.u)
in
(t1, cst, q)
in
let print' fmt (t1, cst, q) =
- Fmt.pf fmt "%a and %a at %a" pp t1 Q.pp cst Q.pp q
+ Fmt.pf fmt "%a and %a at %a" pp t1 A.pp cst A.pp q
in
let shrink (t1, cst, q) =
let open QCheck.Iter in
map (fun (t1, cst) -> (t1, cst, q))
- @@ QCheck.Shrink.pair shrink_t Q.shrink (t1, cst)
+ @@ QCheck.Shrink.pair shrink_t A.shrink (t1, cst)
in
let small (t1, cst, q) = List.length (interesting_values [] t1.u) in
let print x = Fmt.str "%a" print' x in
let test =
- QCheck.Test.make_cell ~name:"on interesting values" ~count:5000
- (QCheck.make ~small ~shrink ~print gen) ~max_fail:10 (fun (t1, cst, q) ->
+ QCheck.Test.make_cell ~name:"on interesting values" ~count
+ (QCheck.make ~small ~shrink ~print gen) ~max_fail:1 (fun (t1, cst, q) ->
let b1 = mem q t1 in
let t2 = mult_cst cst t1 in
- let b2 = mem Q.(cst * q) t2 in
+ let b2 = mem (A.mul cst q) t2 in
(not b1) || b2)
in
QCheck.Test.check_cell_exn test
diff --git a/src_colibri2/theories/LRA/stages/stage2/union.mli b/src_colibri2/theories/LRA/stages/stage2/union.mli
index fc4ced47ccf8dcc8d27b409b3f62b8a3d6ccaf19..390d58a04769659fcc8d34d0a8ad0169750d31ac 100644
--- a/src_colibri2/theories/LRA/stages/stage2/union.mli
+++ b/src_colibri2/theories/LRA/stages/stage2/union.mli
@@ -20,6 +20,6 @@
include Interval_sig.S
-type split_heuristic = Singleton of Q.t | Splitted of t * t | NotSplitted
+type split_heuristic = Singleton of A.t | Splitted of t * t | NotSplitted
val split_heuristic : t -> split_heuristic
diff --git a/src_common/dune b/src_common/dune
index 71901f3d15fbdc52a7e3be4d359760308b347d46..d0906686a7421be386c527f572f56923e5f0a702 100644
--- a/src_common/dune
+++ b/src_common/dune
@@ -27,13 +27,13 @@
interval.Convexe interval.Bound))
(mode promote))
-(rule
- (targets interval_with_divider__T.ml)
- (deps q.mlw modulo.mlw interval.mlw interval_with_divider.mlw)
- (action
- (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L .
- interval_with_divider.T))
- (mode promote))
+; (rule
+; (targets interval_with_divider__T.ml)
+; (deps q.mlw modulo.mlw interval.mlw interval_with_divider.mlw)
+; (action
+; (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L .
+; interval_with_divider.T))
+; (mode promote))
(rule
(targets union__Union.ml)
diff --git a/src_common/interval.mlw b/src_common/interval.mlw
index f5f8ef4c01e4b82a7c7333fd6486336a83c7b910..0005a66092792a65bad17ed1398c0555ec26f3f3 100644
--- a/src_common/interval.mlw
+++ b/src_common/interval.mlw
@@ -9,10 +9,13 @@ end
module Convexe
use bool.Bool
use option.Option
- use q.Q as Q
use Bound
use real.RealInfix
+ scope Make
+ clone q.Intf as Q
+ with axiom equal_is_eq
+
type t =
| Finite Q.t Bound.t Q.t Bound.t
| InfFinite Q.t Bound.t
@@ -550,7 +553,7 @@ module Convexe
ensures { result <-> (forall q. mem q e -> exists z. q = FromInt.from_int z) }
=
match e.a with
- | Finite v1 Large v2 Large -> andb Q.(v1 = v2) Int.(v1.Q.den = 1)
+ | Finite v1 Large v2 Large -> andb Q.(v1 = v2) (Q.is_integer v1)
| Inf
| InfFinite _ _
| FiniteInf _ _
@@ -567,10 +570,10 @@ module Convexe
| FiniteInf v Large
| Finite v Large _ _
| Finite _ _ v Large -> v
- | InfFinite v Strict -> Q.(v - (of_int 1))
+ | 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
+ let half = Q.((of_int 1) / (of_int 2)) in
Q.(v1 * half + v2 * half)
end
@@ -618,10 +621,10 @@ module Convexe
| _, _, Ord.Eq, Large, _ ->
Splitted { a = Finite v1 b1 qzero Strict } zero
| _ ->
- let half = Q.make 1 2 in
+ let half = Q.((of_int 1) / (of_int 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
end
diff --git a/src_common/interval__Convexe.ml b/src_common/interval__Convexe.ml
index 44427230b1e06aa369eff2f7ed5d4e1f2f02b85e..12c681205d8275a573d25f141e481b649ede93b7 100644
--- a/src_common/interval__Convexe.ml
+++ b/src_common/interval__Convexe.ml
@@ -1,560 +1,591 @@
-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
- | Eq
- | 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
+module Make(Q: sig
+ type t
+ val infix_eq : t -> t -> bool
+ val infix_lseq : t -> t -> bool
+ val infix_ls : t -> t -> bool
+ val abs : t -> t
+ val compare : t -> t -> Ord.t
+ val infix_pl : t -> t -> t
+ val infix_mn : t -> t -> t
+ val infix_as : t -> t -> t
+ val infix_sl : t -> t -> t
+ val of_int : Z.t -> t
+ val floor : t -> Z.t
+ val ceil : t -> Z.t
+ val is_integer : t -> bool end) =
+struct
+ 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.infix_eq 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.infix_eq v x
+ then Some (InfFinite (v, Interval__Bound.Strict))
+ else Some e
+ | FiniteInf (v,
+ Interval__Bound.Large) ->
+ if Q.infix_eq 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.infix_eq 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.infix_eq 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.infix_eq v x in let is_max = Q.infix_eq 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
+ | Eq
+ | 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.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
- | 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
+ | ((Finite (_, _, v1, b1), FiniteInf (v2,
+ b2)) | ((InfFinite (v1, b1), FiniteInf (v2, b2)) | (InfFinite (v1,
+ b1), Finite (v2, b2, _, _)))) ->
+ begin match Q.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
- | 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, Ord.Eq) -> Eq
- | (Ord.Eq,
- _) ->
- begin match (b1', b2) with
- | (Interval__Bound.Large, Interval__Bound.Large) -> Le
- | _ -> Lt
+ | (Finite (v1,
+ b1,
+ v1',
+ b1'),
+ Finite (v2,
+ b2,
+ v2',
+ b2')) ->
+ begin match (Q.compare v1' v2, Q.compare v1 v2') with
+ | (Ord.Eq, Ord.Eq) -> Eq
+ | (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
- | (_,
- Ord.Eq) ->
- begin match (b1, b2') with
- | (Interval__Bound.Large, Interval__Bound.Large) -> Ge
- | _ -> Gt
+
+ let is_distinct (e1: t') (e2: t') : bool =
+ match is_comparable e1 e2 with
+ | (Uncomparable | (Le | (Ge | Eq))) -> 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.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
- | (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 | Eq))) -> 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
+ | ((FiniteInf (v1, b1), FiniteInf (v2, b2)) | (Finite (v1, b1, _, _),
+ FiniteInf (v2, b2))) ->
+ begin match Q.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
- | 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
+ | (Finite (v1,
+ b1,
+ v1',
+ b1'),
+ Finite (v2,
+ b2,
+ v2',
+ b2')) ->
+ begin match (Q.compare v2 v1, Q.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
- | 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 absent (x: Q.t) (e: t') : bool = not (mem x e)
-
-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 gt' (c: t') : t' =
- match c with
- | Finite (v, _, _, _) -> FiniteInf (v, Interval__Bound.Strict)
- | InfFinite (_, _) -> Inf
- | FiniteInf (_, Interval__Bound.Strict) -> c
- | FiniteInf (v,
- Interval__Bound.Large) ->
- FiniteInf (v, Interval__Bound.Strict)
- | Inf -> Inf
-
-let ge' (c: t') : t' =
- match c with
- | Finite (v, b, _, _) -> FiniteInf (v, b)
- | InfFinite (_, _) -> Inf
- | FiniteInf (_, _) -> c
- | Inf -> Inf
-
-let lt' (c: t') : t' =
- match c with
- | Finite (_, _, v, _) -> InfFinite (v, Interval__Bound.Strict)
- | InfFinite (_, Interval__Bound.Strict) -> c
- | InfFinite (v,
- Interval__Bound.Large) ->
- InfFinite (v, Interval__Bound.Strict)
- | FiniteInf (_, _) -> Inf
- | Inf -> Inf
-
-let le' (c: t') : t' =
- match c with
- | Finite (_, _, v, b) -> InfFinite (v, b)
- | InfFinite (_, _) -> c
- | FiniteInf (_, _) -> Inf
- | Inf -> Inf
-
-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
+
+ let cmp (x: Q.t) (b: Interval__Bound.t) (y: Q.t) : bool =
+ match b with
+ | Interval__Bound.Large -> Q.infix_lseq x y
+ | Interval__Bound.Strict -> Q.infix_ls 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 absent (x: Q.t) (e: t') : bool = not (mem x e)
+
+ let mult_pos (q: Q.t) (e: t') : t' =
+ match e with
+ | Inf -> Inf
+ | InfFinite (v, b) -> InfFinite (Q.infix_as q v, b)
+ | FiniteInf (v, b) -> FiniteInf (Q.infix_as q v, b)
+ | Finite (v,
+ b,
+ v',
+ b') ->
+ Finite (Q.infix_as q v, b, Q.infix_as q v', b')
+
+ let mult_neg (q: Q.t) (e: t') : t' =
+ match e with
+ | Inf -> Inf
+ | InfFinite (v, b) -> FiniteInf (Q.infix_as q v, b)
+ | FiniteInf (v, b) -> InfFinite (Q.infix_as q v, b)
+ | Finite (v,
+ b,
+ v',
+ b') ->
+ Finite (Q.infix_as q v', b', Q.infix_as q v, b)
+
+ let mult_cst (c: Q.t) (e: t') : t' =
+ if Q.infix_eq c (Q.of_int Z.zero)
+ then singleton (Q.of_int Z.zero)
+ else
+ begin
+ if Q.infix_ls (Q.of_int 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.infix_pl q v, b)
+ | FiniteInf (v, b) -> FiniteInf (Q.infix_pl q v, b)
+ | Finite (v,
+ b,
+ v',
+ b') ->
+ Finite (Q.infix_pl q v, b, Q.infix_pl 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) ->
- 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 integers = reals
-
-let is_integer (e: t') : bool =
- match e with
- | Finite (v1,
- Interval__Bound.Large,
- v2,
- Interval__Bound.Large) ->
- (Q.equal v1 v2) && Z.equal (v1.Q.den) Z.one
- | (Inf | (InfFinite (_, _) | (FiniteInf (_, _) | Finite (_, _, _, _)))) ->
- 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.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.infix_pl v1 v2, add_bound b1 b2)
+ | ((FiniteInf (v1, b1),
+ (FiniteInf (v2, b2) | Finite (v2, b2, _, _))) | (Finite (v2, b2, _,
+ _), FiniteInf (v1, b1))) ->
+ FiniteInf (Q.infix_pl v1 v2, add_bound b1 b2)
+ | (Finite (v1,
+ b1,
+ v1',
+ b1'),
+ Finite (v2,
+ b2,
+ v2',
+ b2')) ->
+ Finite (Q.infix_pl v1 v2,
+ add_bound b1 b2,
+ Q.infix_pl v1' v2',
+ add_bound b1' b2')
+
+ let minus (e1: t') (e2: t') : t' =
+ add e1 (mult_neg (Q.of_int (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 gt' (c: t') : t' =
+ match c with
+ | Finite (v, _, _, _) -> FiniteInf (v, Interval__Bound.Strict)
+ | InfFinite (_, _) -> Inf
+ | FiniteInf (_, Interval__Bound.Strict) -> c
+ | FiniteInf (v,
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
+ FiniteInf (v, Interval__Bound.Strict)
+ | Inf -> Inf
+
+ let ge' (c: t') : t' =
+ match c with
+ | Finite (v, b, _, _) -> FiniteInf (v, b)
+ | InfFinite (_, _) -> Inf
+ | FiniteInf (_, _) -> c
+ | Inf -> Inf
+
+ let lt' (c: t') : t' =
+ match c with
+ | Finite (_, _, v, _) -> InfFinite (v, Interval__Bound.Strict)
+ | InfFinite (_, Interval__Bound.Strict) -> c
+ | InfFinite (v,
+ Interval__Bound.Large) ->
+ InfFinite (v, Interval__Bound.Strict)
+ | FiniteInf (_, _) -> Inf
+ | Inf -> Inf
+
+ let le' (c: t') : t' =
+ match c with
+ | Finite (_, _, v, b) -> InfFinite (v, b)
+ | InfFinite (_, _) -> c
+ | FiniteInf (_, _) -> Inf
+ | Inf -> Inf
+
+ 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.compare v1 v2, b1, b2) with
| (Ord.Eq,
+ Interval__Bound.Large,
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
+ (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.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.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.compare v1 v2, b1, b2) with
| (Ord.Eq,
Interval__Bound.Large,
- _,
- _,
- _) ->
- Splitted (zero, Finite (qzero, Interval__Bound.Strict, v2, b2))
- | (_,
- _,
- Ord.Eq,
+ 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.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_int 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 integers = reals
+
+ let is_integer (e: t') : bool =
+ match e with
+ | Finite (v1,
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
+ v2,
+ Interval__Bound.Large) ->
+ Q.infix_eq v1 v2 && Q.is_integer v1
+ | (Inf | (InfFinite (_, _) | (FiniteInf (_, _) | Finite (_, _, _, _)))) ->
+ false
+
+ let choose (e: t') : Q.t =
+ match e with
+ | Inf -> Q.of_int 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.infix_mn v (Q.of_int Z.one)
+ | FiniteInf (v, Interval__Bound.Strict) -> Q.infix_pl v (Q.of_int Z.one)
+ | Finite (v1,
+ Interval__Bound.Strict,
+ v2,
+ Interval__Bound.Strict) ->
+ (let half = Q.infix_sl (Q.of_int Z.one) (Q.of_int (Z.of_string "2")) in
+ Q.infix_pl (Q.infix_as v1 half) (Q.infix_as 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_int 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.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.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.compare v1 qzero, b1, Q.compare v2 qzero, b2, Q.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.infix_sl (Q.of_int Z.one) (Q.of_int (Z.of_string "2")) in
+ let m = Q.infix_pl (Q.infix_as half v1) (Q.infix_as half v2) in
+ Splitted (Finite (v1, b1, m, Interval__Bound.Strict),
+ Finite (m, Interval__Bound.Large, v2, b2)))
+ end
+end
diff --git a/src_common/interval_with_divider.mlw b/src_common/interval_with_divider.mlw
index e36702d2b835c8c0a95e7d0c157e355f6130d25f..0e7500a6827ed2d191e0100b9d92f5fb0c3a94b3 100644
--- a/src_common/interval_with_divider.mlw
+++ b/src_common/interval_with_divider.mlw
@@ -6,9 +6,14 @@ module T
use q.Q as Q
use option.Option
use interval.Bound
- use interval.Convexe
use modulo.Divisible
+ scope Make
+ clone q.Intf as Q
+ with axiom equal_is_eq
+
+ clone interval.Convexe with type Q.t = Q.t ..
+
predicate best_convexe (c: Convexe.t') (d:real) =
match c.a with
| Inf -> true
diff --git a/src_common/interval_with_divider__T.ml b/src_common/interval_with_divider__T.ml
deleted file mode 100644
index 7863d6252b54589cc9d1590a7f8f8939c1ddd5f2..0000000000000000000000000000000000000000
--- a/src_common/interval_with_divider__T.ml
+++ /dev/null
@@ -1,88 +0,0 @@
-type t = {
- c: Interval__Convexe.t';
- divider: (Q.t) option;
- }
-
-let is_singleton (e: t) : (Q.t) option = Interval__Convexe.is_singleton e.c
-
-let singleton (q: Q.t) : t =
- { c = Interval__Convexe.singleton q; divider = Some (Q.abs q) }
-
-let round_down_to (v: Q.t) (b: Interval__Bound.t) (d: Q.t) : Q.t =
- let v' = Modulo__Divisible.round_down_to v d in
- match b with
- | Interval__Bound.Strict ->
- if (Q.equal v v') then let v'' = (Q.(-) v d) in v'' else v'
- | Interval__Bound.Large -> v'
-
-let round_up_to (v: Q.t) (b: Interval__Bound.t) (d: Q.t) : Q.t =
- let v' = Modulo__Divisible.round_up_to v d in
- match b with
- | Interval__Bound.Strict ->
- if (Q.equal v v') then let v'' = (Q.(+) v d) in v'' else v'
- | Interval__Bound.Large -> v'
-
-let tighten_bounds (c: Interval__Convexe.t') (d: Q.t) : t option =
- let qzero = (Q.of_bigint Z.zero) in
- if (Q.equal d qzero)
- then
- if Interval__Convexe.mem qzero c then Some (singleton qzero) else None
- else
- begin match c with
- | Interval__Convexe.Inf -> Some { c = c; divider = Some d }
- | Interval__Convexe.InfFinite (v,
- b) ->
- (let r = round_down_to v b d in
- let c1 = Interval__Convexe.InfFinite (r, Interval__Bound.Large) in
- Some { c = c1; divider = Some d })
- | Interval__Convexe.FiniteInf (v,
- b) ->
- (let r = round_up_to v b d in
- let c1 = Interval__Convexe.FiniteInf (r, Interval__Bound.Large) in
- Some { c = c1; divider = Some d })
- | Interval__Convexe.Finite (v1,
- b1,
- v2,
- b2) ->
- (let v11 = round_up_to v1 b1 d in let v21 = round_down_to v2 b2 d in
- match
- Interval__Convexe.mk_finite v11
- Interval__Bound.Large
- v21
- Interval__Bound.Large
- with
- | None -> None
- | Some c1 -> Some { c = c1; divider = Some d })
- end
-
-let except (e: t) (x: Q.t) : t option =
- match Interval__Convexe.except e.c x with
- | None -> None
- | Some o ->
- begin match e.divider with
- | Some d -> tighten_bounds o d
- | None -> Some { c = o; divider = None }
- end
-
-let is_comparable (e1: t) (e2: t) : Interval__Convexe.is_comparable =
- Interval__Convexe.is_comparable e1.c e2.c
-
-let is_distinct (e1: t) (e2: t) : bool =
- Interval__Convexe.is_distinct e1.c e2.c
-
-let is_included (e1: t) (e2: t) : bool =
- Interval__Convexe.is_included e1.c e2.c && begin
- match
- (e1.divider, e2.divider)
- with
- | (_, None) -> true
- | (None, Some _) -> false
- | (Some d1, Some d2) -> (let b = Modulo__Divisible.divisible d1 d2 in b)
- end
-
-let mem (x: Q.t) (e: t) : bool =
- Interval__Convexe.mem x e.c && begin match e.divider with
- | None -> true
- | Some d -> (let b = Modulo__Divisible.divisible x d in b)
- end
-
diff --git a/src_common/q.mlw b/src_common/q.mlw
index db92cea2d26a34c0e30cae723cbce2a64afadf62..4c8ce8d4b75a473ea7464c6b9632248a603b3647 100644
--- a/src_common/q.mlw
+++ b/src_common/q.mlw
@@ -367,6 +367,7 @@ module Q
let ceil (a:t) : int
ensures { result = ceil a.real } =
Z.cdiv a.num a.den
+
end
module Intf
@@ -435,4 +436,7 @@ module Intf
val ceil (a:t) : int
ensures { result = ceil a.real }
+
+ val is_integer (a:t) : bool
+ ensures { result = (exists z. a = FromInt.from_int z) }
end
diff --git a/src_common/union__Union.ml b/src_common/union__Union.ml
index acff0205b71b5073686a89f47eeb840acd8f1fa8..810eda2ded05d8387aac6065f61cb8a96b344b63 100644
--- a/src_common/union__Union.ml
+++ b/src_common/union__Union.ml
@@ -11,7 +11,8 @@ module Make(Q: sig
val infix_sl : t -> t -> t
val of_int : Z.t -> t
val floor : t -> Z.t
- val ceil : t -> Z.t end) =
+ val ceil : t -> Z.t
+ val is_integer : t -> bool end) =
struct
type t'' =
| Sin of Q.t * t''