From 8f9eddf3b1319d828d5c70e49fabadfa8f03604c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 28 Apr 2021 14:51:51 +0200
Subject: [PATCH] Define properly stage0 and stage1
q.mlw proved only by colibri2_stage0
---
src_colibri2/bin/dune | 41 ++++++++++-
src_colibri2/stdlib/dune | 2 +-
src_colibri2/stdlib/std.ml | 5 +-
src_colibri2/tests/dune | 4 +-
src_colibri2/theories/LRA/delta.ml | 4 +-
src_colibri2/theories/LRA/delta.mli | 3 +-
src_colibri2/theories/LRA/dom_interval.ml | 2 +-
src_colibri2/theories/LRA/dune | 7 +-
src_colibri2/theories/LRA/fourier.ml | 18 ++---
src_colibri2/theories/LRA/stages/bound.ml | 30 ++++++++
src_colibri2/theories/LRA/stages/bound.mli | 7 ++
src_colibri2/theories/LRA/stages/dune | 16 +++++
.../theories/LRA/stages/interval_domain.mli | 1 +
.../theories/LRA/{ => stages}/interval_sig.ml | 66 +++++++++++++++++-
src_colibri2/theories/LRA/stages/stage0/dune | 11 +++
.../theories/LRA/stages/stage0/impl/dune | 7 ++
.../LRA/stages/stage0/impl/interval_domain.ml | 1 +
.../stage0}/integer_sign_domain.ml | 0
.../stage0}/integer_sign_domain.mli | 0
.../LRA/{ => stages/stage0}/sign_domain.ml | 3 +
.../LRA/{ => stages/stage0}/sign_domain.mli | 14 ----
src_colibri2/theories/LRA/stages/stage1/dune | 13 ++++
.../theories/LRA/stages/stage1/impl/dune | 6 ++
.../LRA/stages/stage1/impl/interval_domain.ml | 1 +
.../LRA/{ => stages/stage1}/interval.ml | 43 +++---------
.../LRA/{ => stages/stage1}/interval.mli | 12 ----
src_common/colibrics_lib.ml | 68 +------------------
src_common/dune | 46 ++++++++-----
src_common/interval.mlw | 62 +++++++++++++++++
src_common/interval__Convexe.ml | 48 +++++++++++++
src_common/q.mlw | 1 +
src_common/q/why3session.xml | 46 ++++++-------
src_common/why3.conf | 65 ------------------
33 files changed, 397 insertions(+), 256 deletions(-)
create mode 100644 src_colibri2/theories/LRA/stages/bound.ml
create mode 100644 src_colibri2/theories/LRA/stages/bound.mli
create mode 100644 src_colibri2/theories/LRA/stages/dune
create mode 100644 src_colibri2/theories/LRA/stages/interval_domain.mli
rename src_colibri2/theories/LRA/{ => stages}/interval_sig.ml (61%)
create mode 100644 src_colibri2/theories/LRA/stages/stage0/dune
create mode 100644 src_colibri2/theories/LRA/stages/stage0/impl/dune
create mode 100644 src_colibri2/theories/LRA/stages/stage0/impl/interval_domain.ml
rename src_colibri2/theories/LRA/{ => stages/stage0}/integer_sign_domain.ml (100%)
rename src_colibri2/theories/LRA/{ => stages/stage0}/integer_sign_domain.mli (100%)
rename src_colibri2/theories/LRA/{ => stages/stage0}/sign_domain.ml (99%)
rename src_colibri2/theories/LRA/{ => stages/stage0}/sign_domain.mli (87%)
create mode 100644 src_colibri2/theories/LRA/stages/stage1/dune
create mode 100644 src_colibri2/theories/LRA/stages/stage1/impl/dune
create mode 100644 src_colibri2/theories/LRA/stages/stage1/impl/interval_domain.ml
rename src_colibri2/theories/LRA/{ => stages/stage1}/interval.ml (96%)
rename src_colibri2/theories/LRA/{ => stages/stage1}/interval.mli (91%)
delete mode 100644 src_common/why3.conf
diff --git a/src_colibri2/bin/dune b/src_colibri2/bin/dune
index 8f7666420..c79742e17 100644
--- a/src_colibri2/bin/dune
+++ b/src_colibri2/bin/dune
@@ -1,7 +1,41 @@
(executable
- (name main)
+ (name colibri2_stage0)
(public_name colibri2)
+ (package colibri2)
(flags -linkall)
+ (libraries
+ colibri2_main
+ colibri2.theories.LRA.stages.stage0)
+ (modules colibri2_stage0)
+)
+
+(rule
+ (target colibri2_stage0.ml)
+ (action
+ (with-outputs-to
+ %{target}
+ (run true))))
+
+(executable
+ (name colibri2_stage1)
+; (public_name colibri2)
+; (package colibri2)
+ (flags -linkall)
+ (libraries
+ colibri2_main
+ colibri2.theories.LRA.stages.stage1)
+ (modules colibri2_stage1)
+)
+
+(rule
+ (target colibri2_stage1.ml)
+ (action
+ (with-outputs-to
+ %{target}
+ (run true))))
+
+(library
+ (name colibri2_main)
(libraries
; external deps
cmdliner
@@ -19,7 +53,10 @@
colibri2.theories.LRA
colibri2.theories.quantifiers
colibri2.theories.adt)
- (package colibri2))
+ (modules
+ main options
+ )
+)
; Rule to generate a man page for colibrics
diff --git a/src_colibri2/stdlib/dune b/src_colibri2/stdlib/dune
index c5c2832ad..28cd38ea6 100644
--- a/src_colibri2/stdlib/dune
+++ b/src_colibri2/stdlib/dune
@@ -2,7 +2,7 @@
(name colibri2_stdlib)
(public_name colibri2.stdlib)
(synopsis "Stdlib for colibri2")
- (libraries zarith containers colibri2_popop_lib colibrics_lib fmt)
+ (libraries zarith containers colibri2_popop_lib fmt)
(preprocess
(pps ppx_optcomp ppx_deriving.std ppx_hash))
(flags :standard -w +a-4-42-44-48-50-58-60-40-9@8 -color always -open
diff --git a/src_colibri2/stdlib/std.ml b/src_colibri2/stdlib/std.ml
index f3764175d..d13939c1b 100644
--- a/src_colibri2/stdlib/std.ml
+++ b/src_colibri2/stdlib/std.ml
@@ -102,8 +102,9 @@ module Q = struct
let is_integer q = Z.equal Z.one q.Q.den
- let floor x = Q.of_bigint (Colibrics_lib.QUtils.floor x)
- let ceil x = Q.of_bigint (Colibrics_lib.QUtils.ceil x)
+
+ let floor x = Q.of_bigint (Z.fdiv (x.Q.num) (x.Q.den))
+ let ceil x = Q.of_bigint (Z.cdiv (x.Q.num) (x.Q.den))
let none_zero c = if Q.equal Q.zero c then None else Some c
diff --git a/src_colibri2/tests/dune b/src_colibri2/tests/dune
index 2cb73042e..98b5bcc99 100644
--- a/src_colibri2/tests/dune
+++ b/src_colibri2/tests/dune
@@ -2,7 +2,9 @@
(modes byte exe)
(name tests)
(libraries containers colibri2.core colibri2.theories.bool
- colibri2.theories.LRA colibri2.theories.quantifiers ounit2 colibri2.solver colibri2.stdlib)
+ colibri2.theories.LRA colibri2.theories.quantifiers ounit2 colibri2.solver colibri2.stdlib
+ colibri2.theories.LRA.stages.stage0
+ )
(flags :standard -w +a-4-42-44-48-50-58-60-9@8 -color always)
(ocamlopt_flags :standard -O3 -unbox-closures -unbox-closures-factor 20))
diff --git a/src_colibri2/theories/LRA/delta.ml b/src_colibri2/theories/LRA/delta.ml
index dc3448d58..b508b5a5b 100644
--- a/src_colibri2/theories/LRA/delta.ml
+++ b/src_colibri2/theories/LRA/delta.ml
@@ -42,14 +42,14 @@ module Edge = struct
end
module Dist = struct
- type t = { q: Q.t; bound: Interval.Bound.t }
+ type t = { q: Q.t; bound: Bound.t }
[@@deriving show]
let min d1 d2 =
let c = Q.compare d1.q d2.q in
if c = 0 then
let bound = match d1.bound, d2.bound with
- | Large, Large -> Interval.Bound.Large
+ | Large, Large -> Bound.Large
| _ -> Strict
in
{ q = d1.q; bound }
diff --git a/src_colibri2/theories/LRA/delta.mli b/src_colibri2/theories/LRA/delta.mli
index ff733676e..2c3be78f8 100644
--- a/src_colibri2/theories/LRA/delta.mli
+++ b/src_colibri2/theories/LRA/delta.mli
@@ -33,7 +33,8 @@ val add_ge: Egraph.t -> Node.t -> Q.t -> Node.t -> unit
val add_gt: Egraph.t -> Node.t -> Q.t -> Node.t -> unit
(* [add_gt d n1 q n2] n1 - n2 > q *)
-val add: Egraph.t -> Node.t -> Q.t -> Interval.Bound.t -> Node.t -> unit
+val add: Egraph.t -> Node.t -> Q.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.t -> unit
+
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index 863fd7a35..9c45b9d40 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -26,7 +26,7 @@ let debug = Debug.register_info_flag
~desc:"for intervals for the arithmetic theory"
"LRA.interval"
-module D = Integer_sign_domain
+module D = Colibri2_theories_LRA_stages.Interval_domain
let dom = DomKind.create_key (module struct type t = D.t let name = "ARITH" end)
diff --git a/src_colibri2/theories/LRA/dune b/src_colibri2/theories/LRA/dune
index a24f08eaa..76aaed910 100644
--- a/src_colibri2/theories/LRA/dune
+++ b/src_colibri2/theories/LRA/dune
@@ -4,11 +4,14 @@
(synopsis "theories for colibri2")
(libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
colibri2.core.structures colibri2.core colibri2.theories.bool
- colibri2.theories.quantifiers)
+ colibri2.theories.quantifiers
+ colibri2.theories.LRA.stages )
(preprocess
(pps ppx_deriving.std ppx_hash))
(flags :standard -w +a-4-42-44-48-50-58-32-60-40-9@8 -color always -open
Containers -open Colibri2_stdlib -open Std -open Colibri2_core -open
- Colibri2_theories_bool)
+ Colibri2_theories_bool
+ -open Colibri2_theories_LRA_stages_def
+ )
(ocamlopt_flags :standard -O3 -bin-annot -unbox-closures
-unbox-closures-factor 20))
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 118bcebca..103be8d66 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -29,7 +29,7 @@ let debug = Debug.register_info_flag ~desc:"Reasoning about <= < in LRA" "fourie
let stats_run = Debug.register_stats_int ~name:"Fourier.run" ~init:0
-type eq = { p: Polynome.t; bound: Interval.Bound.t; origins: Ground.S.t }
+type eq = { p: Polynome.t; bound: Bound.t; origins: Ground.S.t }
[@@deriving show]
(** p <= 0 or p < 0 *)
@@ -95,14 +95,14 @@ let delta d eq =
let apply d ~f truth g =
let aux d bound a b =
- let bound = if truth then bound else match bound with | Interval.Bound.Large -> Strict | Strict -> Large in
+ let bound = if truth then bound else match bound with | Bound.Large -> Strict | Strict -> Large in
let a,b = if truth then a,b else b,a in
f d bound a b
in
match Ground.sem g with
| { app = {builtin = Expr.Lt}; tyargs = []; args; _ } ->
let a,b = IArray.extract2_exn args in
- aux d Interval.Bound.Strict a b
+ aux d Bound.Strict a b
| { app = {builtin = Expr.Leq}; tyargs = []; args; _ } ->
let a,b = IArray.extract2_exn args in
aux d Large a b
@@ -121,7 +121,7 @@ let add_eq d eqs p bound origins =
let eq = { p; bound; origins } in
delta d eq;
eq::eqs
- | Some p, Interval.Bound.Large when Q.sign p = 0 ->
+ | Some p, Bound.Large when Q.sign p = 0 ->
Ground.S.iter (fun g ->
let truth = Option.get_exn (Boolean.is d (Ground.node g)) in
apply d truth g ~f:(fun d bound a b ->
@@ -146,8 +146,8 @@ let mk_eq d bound a b =
| Some p -> p in
let p,bound' =
match bound with
- | Interval.Bound.Strict when Dom_interval.is_integer d a && Dom_interval.is_integer d b ->
- Polynome.add_cst (Polynome.sub (!a) (!b)) Q.one, Interval.Bound.Large
+ | 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.sub (!a) (!b), bound
in
p,bound',
@@ -162,7 +162,7 @@ let make_equations d (eqs,vars) g =
let p,bound,p_non_norm,bound_non_norm =
apply d ~f:mk_eq truth g
in
- Debug.dprintf6 debug "[Fourier] %a(%a)%a0" Polynome.pp p Polynome.pp p_non_norm Interval.Bound.pp bound;
+ Debug.dprintf6 debug "[Fourier] %a(%a)%a0" Polynome.pp p Polynome.pp p_non_norm Bound.pp bound;
let eqs, vars =
(add_eq d eqs p bound (Ground.S.singleton g),
Node.M.union_merge (fun _ _ _ -> Some ()) vars p.Polynome.poly)
@@ -206,8 +206,8 @@ let fm (d:Egraph.t) =
let p = Polynome.cx_p_cy Q.one peq.p q neq.p in
let bound =
match peq.bound, neq.bound with
- | Large, Large -> Interval.Bound.Large
- | _ -> Interval.Bound.Strict in
+ | Large, Large -> Bound.Large
+ | _ -> Bound.Strict in
add_eq d eqs p bound (Ground.S.union peq.origins neq.origins)
) absent positive negative
in
diff --git a/src_colibri2/theories/LRA/stages/bound.ml b/src_colibri2/theories/LRA/stages/bound.ml
new file mode 100644
index 000000000..b2169edcd
--- /dev/null
+++ b/src_colibri2/theories/LRA/stages/bound.ml
@@ -0,0 +1,30 @@
+module T = struct
+ type t =
+ | Strict | Large
+ [@@deriving eq, ord, hash]
+
+ let pp fmt = function
+ | Strict -> CCFormat.string fmt "<"
+ | Large -> CCFormat.string fmt "≤"
+
+end
+
+include T
+include Colibri2_popop_lib.Popop_stdlib.MkDatatype(T)
+
+let compare_inf b1 b2 = match b1,b2 with
+ | Large, Strict -> -1
+ | Strict, Large -> 1
+ | Large, Large | Strict, Strict -> 0
+
+let compare_inf_sup b1 b2 = match b1,b2 with
+ | Large, Strict -> 1
+ | Strict, Large -> 1
+ | Large, Large -> 0
+ | Strict, Strict -> 1
+
+let compare_sup b1 b2 = - (compare_inf b1 b2)
+
+let compare_bounds_inf = CCOrd.pair Q.compare compare_inf
+let compare_bounds_sup = CCOrd.pair Q.compare compare_sup
+let compare_bounds_inf_sup = CCOrd.pair Q.compare compare_inf_sup
diff --git a/src_colibri2/theories/LRA/stages/bound.mli b/src_colibri2/theories/LRA/stages/bound.mli
new file mode 100644
index 000000000..a27a1d33d
--- /dev/null
+++ b/src_colibri2/theories/LRA/stages/bound.mli
@@ -0,0 +1,7 @@
+type t = | Strict | Large
+
+val compare_bounds_inf: Q.t * t -> Q.t * t -> int
+val compare_bounds_sup: Q.t * t -> Q.t * t -> int
+val compare_bounds_inf_sup: Q.t * t -> Q.t * t -> int
+
+include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
diff --git a/src_colibri2/theories/LRA/stages/dune b/src_colibri2/theories/LRA/stages/dune
new file mode 100644
index 000000000..c5ba75543
--- /dev/null
+++ b/src_colibri2/theories/LRA/stages/dune
@@ -0,0 +1,16 @@
+(library
+ (name colibri2_theories_LRA_stages)
+ (public_name colibri2.theories.LRA.stages)
+ (virtual_modules interval_domain)
+ (libraries colibri2.popop_lib colibri2.theories.LRA.stages.def)
+ (modules interval_domain)
+)
+
+(library
+ (name colibri2_theories_LRA_stages_def)
+ (public_name colibri2.theories.LRA.stages.def)
+ (modules interval_sig bound)
+ (libraries colibri2.popop_lib containers)
+ (preprocess
+ (pps ppx_deriving.std ppx_hash))
+)
diff --git a/src_colibri2/theories/LRA/stages/interval_domain.mli b/src_colibri2/theories/LRA/stages/interval_domain.mli
new file mode 100644
index 000000000..91205fb47
--- /dev/null
+++ b/src_colibri2/theories/LRA/stages/interval_domain.mli
@@ -0,0 +1 @@
+include Colibri2_theories_LRA_stages_def.Interval_sig.S
diff --git a/src_colibri2/theories/LRA/interval_sig.ml b/src_colibri2/theories/LRA/stages/interval_sig.ml
similarity index 61%
rename from src_colibri2/theories/LRA/interval_sig.ml
rename to src_colibri2/theories/LRA/stages/interval_sig.ml
index b318a09f2..1715ca252 100644
--- a/src_colibri2/theories/LRA/interval_sig.ml
+++ b/src_colibri2/theories/LRA/stages/interval_sig.ml
@@ -20,12 +20,72 @@
open Colibri2_popop_lib
-type bound = Colibrics_lib.Interval.Bound.t
-
module type S = sig
include Popop_stdlib.Datatype
- include (Colibrics_lib.Interval.S with type t := t)
+ val is_distinct: t -> t -> bool
+ type is_comparable =
+ | Gt
+ | Lt
+ | Ge
+ | Le
+ | Uncomparable
+
+ val is_comparable: t -> t -> is_comparable
+ val is_included: t -> t -> bool
+
+ val mult_cst: Q.t -> t -> t
+ val add_cst : Q.t -> t -> t
+ val add: t -> t -> t
+ val minus: t -> t -> t
+
+ val mem: Q.t -> t -> bool
+
+ (** from Q.t *)
+ val singleton: Q.t -> t
+ val is_singleton: t -> Q.t option
+
+ val except: t -> Q.t -> t option
+
+ type split_heuristic =
+ | Singleton of Q.t
+ | Splitted of t * t
+ | NotSplitted
+
+ val split_heuristic: t -> split_heuristic
+
+ val absent: Q.t -> t -> bool
+ val is_integer: t -> bool
+ val integers: t
+
+ val gt: Q.t -> t
+ val ge: Q.t -> t
+ val lt: Q.t -> t
+ val le: Q.t -> t
+ (** > q, >= q, < q, <= q *)
+
+ val le': t -> t
+ val lt': t -> t
+ val ge': t -> t
+ val gt': t -> t
+
+ val union: t -> t -> t
+ (** union set *)
+
+ val inter: t -> t -> t option
+ (** intersection set.
+ if the two arguments are equals, return the second
+ *)
+
+
+ val zero: t
+ val reals: t
+
+ (** R *)
+ val is_reals: t -> bool
+
+ val choose: t -> Q.t
+ (** Nothing smart in this choosing *)
val invariant: t -> bool
diff --git a/src_colibri2/theories/LRA/stages/stage0/dune b/src_colibri2/theories/LRA/stages/stage0/dune
new file mode 100644
index 000000000..a84e03e54
--- /dev/null
+++ b/src_colibri2/theories/LRA/stages/stage0/dune
@@ -0,0 +1,11 @@
+(library
+ (name colibri2_theories_LRA_stages_stage0_sign_domain)
+ (public_name colibri2.theories.LRA.stages.stage0.sign_domain)
+ (libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
+ colibri2.core.structures colibri2.core colibri2.theories.bool
+ colibri2.theories.quantifiers colibri2.theories.LRA.stages.def)
+ (preprocess
+ (pps ppx_deriving.std ppx_hash))
+ (flags -open Colibri2_theories_LRA_stages_def -open Colibri2_stdlib -open Std)
+ (synopsis "Sign domain")
+)
diff --git a/src_colibri2/theories/LRA/stages/stage0/impl/dune b/src_colibri2/theories/LRA/stages/stage0/impl/dune
new file mode 100644
index 000000000..b343094b1
--- /dev/null
+++ b/src_colibri2/theories/LRA/stages/stage0/impl/dune
@@ -0,0 +1,7 @@
+(library
+ (name colibri2_theories_LRA_stages_stage0)
+ (public_name colibri2.theories.LRA.stages.stage0)
+ (libraries colibri2.theories.LRA.stages.stage0.sign_domain)
+ (synopsis "")
+ (implements colibri2.theories.LRA.stages)
+)
diff --git a/src_colibri2/theories/LRA/stages/stage0/impl/interval_domain.ml b/src_colibri2/theories/LRA/stages/stage0/impl/interval_domain.ml
new file mode 100644
index 000000000..f949de4db
--- /dev/null
+++ b/src_colibri2/theories/LRA/stages/stage0/impl/interval_domain.ml
@@ -0,0 +1 @@
+include Colibri2_theories_LRA_stages_stage0_sign_domain.Integer_sign_domain
diff --git a/src_colibri2/theories/LRA/integer_sign_domain.ml b/src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.ml
similarity index 100%
rename from src_colibri2/theories/LRA/integer_sign_domain.ml
rename to src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.ml
diff --git a/src_colibri2/theories/LRA/integer_sign_domain.mli b/src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.mli
similarity index 100%
rename from src_colibri2/theories/LRA/integer_sign_domain.mli
rename to src_colibri2/theories/LRA/stages/stage0/integer_sign_domain.mli
diff --git a/src_colibri2/theories/LRA/sign_domain.ml b/src_colibri2/theories/LRA/stages/stage0/sign_domain.ml
similarity index 99%
rename from src_colibri2/theories/LRA/sign_domain.ml
rename to src_colibri2/theories/LRA/stages/stage0/sign_domain.ml
index a4df04b23..ce6a59679 100644
--- a/src_colibri2/theories/LRA/sign_domain.ml
+++ b/src_colibri2/theories/LRA/stages/stage0/sign_domain.ml
@@ -383,3 +383,6 @@ let gt' v =
zero = v.neg ;
pos = v.pos || v.zero || v.neg;
}
+
+let integers = reals
+let is_integer _ = false
diff --git a/src_colibri2/theories/LRA/sign_domain.mli b/src_colibri2/theories/LRA/stages/stage0/sign_domain.mli
similarity index 87%
rename from src_colibri2/theories/LRA/sign_domain.mli
rename to src_colibri2/theories/LRA/stages/stage0/sign_domain.mli
index f8a18f2a9..8d9f52f99 100644
--- a/src_colibri2/theories/LRA/sign_domain.mli
+++ b/src_colibri2/theories/LRA/stages/stage0/sign_domain.mli
@@ -25,17 +25,3 @@ type t = private {
}
include Interval_sig.S with type t := t
-
-type split_heuristic =
- | Singleton of Q.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
diff --git a/src_colibri2/theories/LRA/stages/stage1/dune b/src_colibri2/theories/LRA/stages/stage1/dune
new file mode 100644
index 000000000..89ee0c1fb
--- /dev/null
+++ b/src_colibri2/theories/LRA/stages/stage1/dune
@@ -0,0 +1,13 @@
+(library
+ (name colibri2_theories_LRA_stages_stage1_interval_domain)
+ (public_name colibri2.theories.LRA.stages.stage1.interval_domain)
+ (libraries containers ocamlgraph colibri2.stdlib colibri2.popop_lib
+ colibri2.core.structures colibri2.core colibri2.theories.bool
+ colibri2.theories.quantifiers colibri2.theories.LRA.stages.def
+ colibrics.lib
+ )
+ (preprocess
+ (pps ppx_deriving.std ppx_hash))
+ (flags -open Colibri2_theories_LRA_stages_def -open Colibri2_stdlib -open Std -open Containers)
+ (synopsis "Interval domain")
+)
diff --git a/src_colibri2/theories/LRA/stages/stage1/impl/dune b/src_colibri2/theories/LRA/stages/stage1/impl/dune
new file mode 100644
index 000000000..72417483f
--- /dev/null
+++ b/src_colibri2/theories/LRA/stages/stage1/impl/dune
@@ -0,0 +1,6 @@
+(library
+ (name colibri2_theories_LRA_stages_stage1)
+ (public_name colibri2.theories.LRA.stages.stage1)
+ (libraries colibri2.theories.LRA.stages.stage1.interval_domain)
+ (implements colibri2.theories.LRA.stages)
+)
diff --git a/src_colibri2/theories/LRA/stages/stage1/impl/interval_domain.ml b/src_colibri2/theories/LRA/stages/stage1/impl/interval_domain.ml
new file mode 100644
index 000000000..8bff072fd
--- /dev/null
+++ b/src_colibri2/theories/LRA/stages/stage1/impl/interval_domain.ml
@@ -0,0 +1 @@
+include Colibri2_theories_LRA_stages_stage1_interval_domain.Interval.Convexe
diff --git a/src_colibri2/theories/LRA/interval.ml b/src_colibri2/theories/LRA/stages/stage1/interval.ml
similarity index 96%
rename from src_colibri2/theories/LRA/interval.ml
rename to src_colibri2/theories/LRA/stages/stage1/interval.ml
index e18159736..febd3c046 100644
--- a/src_colibri2/theories/LRA/interval.ml
+++ b/src_colibri2/theories/LRA/stages/stage1/interval.ml
@@ -21,52 +21,29 @@
open Colibri2_popop_lib
open Colibri2_stdlib.Std
-module Bound = struct
- type t = Colibrics_lib.Interval.Bound.t =
- | Strict | Large [@@deriving eq, ord, hash]
-
- let pp fmt = function
- | Strict -> Format.string fmt "<"
- | Large -> Format.string fmt "≤"
-
- let compare_inf b1 b2 = match b1,b2 with
- | Large, Strict -> -1
- | Strict, Large -> 1
- | Large, Large | Strict, Strict -> 0
-
- let compare_inf_sup b1 b2 = match b1,b2 with
- | Large, Strict -> 1
- | Strict, Large -> 1
- | Large, Large -> 0
- | Strict, Strict -> 1
-
- let compare_sup b1 b2 = - (compare_inf b1 b2)
-
- let compare_bounds_inf = Ord.pair Q.compare compare_inf
- let compare_bounds_sup = Ord.pair Q.compare compare_sup
- let compare_bounds_inf_sup = Ord.pair Q.compare compare_inf_sup
-
-end
-
module Convexe = struct
include Colibrics_lib.Interval.Convexe
include (struct
+ type bound = Colibrics_lib.Interval.Bound.t =
+ | Strict | Large
+ [@@deriving eq, ord, hash]
+
type t = Colibrics_lib.Interval.Convexe.t = private
- | Finite of Q.t * Bound.t * Q.t * Bound.t
- | InfFinite of Q.t * Bound.t
- | FiniteInf of Q.t * Bound.t
+ | Finite of Q.t * bound * Q.t * bound
+ | InfFinite of Q.t * bound
+ | FiniteInf of Q.t * bound
| Inf
- [@@ deriving eq, ord, hash]
+ [@@ deriving eq, ord, hash]
end)
let pp fmt t =
let print_bound_left fmt = function
- | Bound.Large -> Format.fprintf fmt "["
+ | Large -> Format.fprintf fmt "["
| Strict -> Format.fprintf fmt "]" in
let print_bound_right fmt = function
- | Bound.Large -> Format.fprintf fmt "]"
+ | Large -> Format.fprintf fmt "]"
| Strict -> Format.fprintf fmt "[" in
match t with
| Finite (q1,b1,q2,b2) ->
diff --git a/src_colibri2/theories/LRA/interval.mli b/src_colibri2/theories/LRA/stages/stage1/interval.mli
similarity index 91%
rename from src_colibri2/theories/LRA/interval.mli
rename to src_colibri2/theories/LRA/stages/stage1/interval.mli
index 6625bb4ce..c97378b34 100644
--- a/src_colibri2/theories/LRA/interval.mli
+++ b/src_colibri2/theories/LRA/stages/stage1/interval.mli
@@ -18,18 +18,6 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-module Bound : sig
- type t = Colibrics_lib.Interval.Bound.t =
- | Strict | Large
- [@@deriving eq, ord, hash]
-
- val pp: t Format.printer
-
- val compare_bounds_inf: Q.t * t -> Q.t * t -> int
- val compare_bounds_sup: Q.t * t -> Q.t * t -> int
- val compare_bounds_inf_sup: Q.t * t -> Q.t * t -> int
-end
-
module Convexe: sig
include Interval_sig.S
diff --git a/src_common/colibrics_lib.ml b/src_common/colibrics_lib.ml
index 494a4d71b..b4591ef05 100644
--- a/src_common/colibrics_lib.ml
+++ b/src_common/colibrics_lib.ml
@@ -34,72 +34,6 @@ end
module Interval = struct
module Bound = Interval__Bound
- module type S = sig
- type t
-
- val is_distinct: t -> t -> bool
- type is_comparable =
- | Gt
- | Lt
- | Ge
- | Le
- | Uncomparable
-
- val is_comparable: t -> t -> is_comparable
- val is_included: t -> t -> bool
-
- val mult_cst: Q.t -> t -> t
- val add_cst : Q.t -> t -> t
- val add: t -> t -> t
- val minus: t -> t -> t
-
- val mem: Q.t -> t -> bool
-
- (** from Q.t *)
- val singleton: Q.t -> t
- val is_singleton: t -> Q.t option
-
- val except: t -> Q.t -> t option
-
- val gt: Q.t -> t
- val ge: Q.t -> t
- val lt: Q.t -> t
- val le: Q.t -> t
- (** > q, >= q, < q, <= q *)
-
- val union: t -> t -> t
- (** union set *)
-
- val inter: t -> t -> t option
- (** intersection set.
- if the two arguments are equals, return the second
- *)
-
-
- val zero: t
- val reals: t
- (** R *)
- val is_reals: t -> bool
-
- val choose: t -> Q.t
- (** Nothing smart in this choosing *)
-
- end
- module Convexe : sig
- type t = private
- | Finite of Q.t * Bound.t * Q.t * Bound.t
- | InfFinite of Q.t * Bound.t
- | FiniteInf of Q.t * Bound.t
- | Inf
- include (S with type t := t )
-
- type split_heuristic =
- | Singleton of Q.t
- | Splitted of t * t
- | NotSplitted
-
- val split_heuristic: t -> split_heuristic
-
- end = Interval__Convexe
+ module Convexe = Interval__Convexe
end
diff --git a/src_common/dune b/src_common/dune
index 52f3ee552..ef1e5168e 100644
--- a/src_common/dune
+++ b/src_common/dune
@@ -38,29 +38,43 @@
(rule
(alias runproof)
(deps
+ ../src_colibri2/bin/colibri2_stage0.exe
(source_tree q)
- q.mlw)
+ q.mlw
+ why3.conf
+ colibri2.drv
+ )
(action
- (run why3 replay -L . q)))
+ (run why3 replay -C why3.conf -L . q)))
(rule
- (alias runproof)
+ (target why3.conf)
(deps
- (source_tree modulo)
- modulo.mlw
- q.mlw)
+ ../src_colibri2/bin/colibri2_stage0.exe)
(action
- (run why3 replay -L . modulo)))
+ (progn (run touch why3.conf)
+ (system "why3 config add-prover -C why3.conf Colibri2 $(realpath ../src_colibri2/bin/colibri2_stage0.exe)")
+ )))
+
+; (rule
+; (alias runproof)
+; (deps
+; (source_tree modulo)
+; modulo.mlw
+; q.mlw)
+; (action
+; (run why3 replay -L . modulo)))
+
+; (rule
+; (alias runproof)
+; (deps
+; (source_tree modulo)
+; interval.mlw
+; modulo.mlw
+; q.mlw)
+; (action
+; (run why3 replay -L . interval)))
-(rule
- (alias runproof)
- (deps
- (source_tree modulo)
- interval.mlw
- modulo.mlw
- q.mlw)
- (action
- (run why3 replay -L . interval)))
; (rule
; (alias ide:q)
diff --git a/src_common/interval.mlw b/src_common/interval.mlw
index 2748ef3f9..f348f33a3 100644
--- a/src_common/interval.mlw
+++ b/src_common/interval.mlw
@@ -244,6 +244,10 @@ module Convexe
| Finite v b v' b' -> andb (cmp v b x) (cmp x b' v')
end
+ let absent (x:Q.t) (e:t')
+ ensures { result = not (mem x.Q.real e) } =
+ notb (mem x e)
+
let mult_pos q e
requires { Q.(0. <. q.real) }
ensures { forall q'. mem q' e -> mem (q.Q.real *. q') result }
@@ -340,6 +344,48 @@ module Convexe
=
{ a = InfFinite c Large }
+ let gt' c
+ ensures { forall q. mem q result <-> (exists c. mem c result /\ q >. c) }
+ =
+ match c.a with
+ | Finite v _ _ _ -> { a = FiniteInf v Strict }
+ | InfFinite _ _ -> { a = Inf }
+ | FiniteInf _ Strict -> c
+ | FiniteInf v Large -> { a = FiniteInf v Strict }
+ | Inf -> { a = Inf }
+ end
+
+ let ge' c
+ ensures { forall q. mem q result <-> (exists c. mem c result /\ q >=. c) }
+ =
+ match c.a with
+ | Finite v b _ _ -> { a = FiniteInf v b }
+ | InfFinite _ _ -> { a = Inf }
+ | FiniteInf _ _-> c
+ | Inf -> { a = Inf }
+ end
+
+ let lt' c
+ ensures { forall q. mem q result <-> (exists c. mem c result /\ q <. c) }
+ =
+ match c.a with
+ | Finite _ _ v _ -> { a = InfFinite v Strict }
+ | InfFinite _ Strict -> c
+ | InfFinite v Large -> { a = InfFinite v Strict }
+ | FiniteInf _ _-> { a = Inf }
+ | Inf -> { a = Inf }
+ end
+
+ let le' c
+ ensures { forall q. mem q result <-> (exists c. mem c result /\ q <=. c) }
+ =
+ match c.a with
+ | Finite _ _ v b -> { a = InfFinite v b }
+ | InfFinite _ _ -> c
+ | FiniteInf _ _-> { a = Inf }
+ | Inf -> { a = Inf }
+ end
+
let min_bound_sup v1 b1 v2 b2: (v3:Q.t,b3:Bound.t)
ensures { forall q. (cmp q b1 v1 /\ cmp q b2 v2) <-> cmp q b3 v3 }
ensures { Q.(v3 <= v1) } ensures { Q.(v3 <= v2) }
@@ -488,6 +534,22 @@ module Convexe
| Finite v _ _ _ -> assert { not (mem (v.Q.real -. 1.) e) }; false
end
+ let integers = reals
+
+ use int.Int as Int
+ use real.FromInt as FromInt
+
+ let is_integer e
+ 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)
+ | Inf
+ | InfFinite _ _
+ | FiniteInf _ _
+ | Finite _ _ _ _ -> false
+ end
+
let choose e
ensures { mem result e }
diff --git a/src_common/interval__Convexe.ml b/src_common/interval__Convexe.ml
index c39991c03..d552b1acd 100644
--- a/src_common/interval__Convexe.ml
+++ b/src_common/interval__Convexe.ml
@@ -212,6 +212,8 @@ let mem (x: Q.t) (e: t') : bool =
| 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
@@ -288,6 +290,40 @@ 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
@@ -423,6 +459,18 @@ let is_reals (e: t') : bool =
| 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)
diff --git a/src_common/q.mlw b/src_common/q.mlw
index 35099ad0c..743b4eb48 100644
--- a/src_common/q.mlw
+++ b/src_common/q.mlw
@@ -92,6 +92,7 @@ module QWithInf
}
invariant { value = Real -> 0 < den }
invariant { value = Real -> Z.prime_to_one_another num den }
+ by { num = 1; den = 1; value = Real }
predicate is_real (q:t) =
q.value = Real
diff --git a/src_common/q/why3session.xml b/src_common/q/why3session.xml
index 4e716d8f9..6ef2aa09b 100644
--- a/src_common/q/why3session.xml
+++ b/src_common/q/why3session.xml
@@ -2,77 +2,73 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
-<prover id="0" name="CVC4" version="1.7" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="1" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="2" name="Alt-Ergo" version="2.3.3" timelimit="5" steplimit="0" memlimit="1000"/>
-<prover id="3" name="Colibri2" version="0.0.1" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Colibri2" version="0.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file format="whyml" proved="true">
<path name=".."/><path name="q.mlw"/>
<theory name="QWithInf" proved="true">
<goal name="t'vc" expl="VC for t" proved="true">
- <proof prover="0"><result status="valid" time="0.04" steps="17867"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="floor'vc" expl="VC for floor" proved="true">
<transf name="split_vc" proved="true" >
<goal name="floor'vc.0" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.03" steps="5232"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="floor'vc.1" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="4693"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="floor'vc.2" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.15" steps="52166"/></proof>
- <proof prover="3"><result status="valid" time="0.59"/></proof>
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="floor'vc.3" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="4757"/></proof>
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="floor'vc.4" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="4808"/></proof>
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="floor'vc.5" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="20883"/></proof>
+ <proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="floor'vc.6" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="floor'vc.6.0" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.06" steps="235283"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="floor'vc.6.1" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.14" steps="371"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="floor'vc.7" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.76" steps="707"/></proof>
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
<goal name="ceil'vc" expl="VC for ceil" proved="true">
<transf name="split_vc" proved="true" >
<goal name="ceil'vc.0" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.03" steps="5249"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceil'vc.1" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.03" steps="4703"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="ceil'vc.2" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.07" steps="52180"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="ceil'vc.3" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="4799"/></proof>
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="ceil'vc.4" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="4850"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="ceil'vc.5" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.01" steps="20811"/></proof>
+ <proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="ceil'vc.6" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="0.15" steps="501"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="ceil'vc.7" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="6014"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
@@ -81,10 +77,10 @@
<goal name="t'vc" expl="VC for t" proved="true">
<transf name="split_vc" proved="true" >
<goal name="t'vc.0" expl="type invariant" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="2245"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="t'vc.1" expl="type invariant" proved="true">
- <proof prover="0"><result status="valid" time="0.02" steps="2557"/></proof>
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
diff --git a/src_common/why3.conf b/src_common/why3.conf
deleted file mode 100644
index 9c2fdf85a..000000000
--- a/src_common/why3.conf
+++ /dev/null
@@ -1,65 +0,0 @@
-[editor pvs]
-command = "%l/why3-call-pvs %l/pvs pvs %f"
-name = "PVS"
-
-[editor proofgeneral-coq]
-command = "emacs --eval \"(setq coq-load-path '((\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
-name = "Emacs/ProofGeneral/Coq"
-
-[editor isabelle-jedit]
-command = "isabelle why3 -i %f"
-name = "Isabelle/jEdit"
-
-[editor coqide]
-command = "coqide -R %l/coq Why3 %f"
-name = "CoqIDE"
-
-[editor altgr-ergo]
-command = "altgr-ergo %f"
-name = "AltGr-Ergo"
-
-[ide]
-allow_source_editing = true
-auto_next = true
-current_tab = 0
-error_color_bg = "white"
-error_color_fg = "red"
-error_color_msg_zone_bg = "yellow"
-error_color_msg_zone_fg = "red"
-error_line_color = "yellow"
-font_size = 10
-goal_color = "gold"
-iconset = "fatcow"
-max_boxes = 16
-neg_premise_color = "pink"
-premise_color = "chartreuse"
-print_attributes = false
-print_coercions = true
-print_locs = false
-print_time_limit = false
-saving_policy = 2
-search_color = "lightblue"
-show_full_context = true
-task_height = 664
-tree_width = 512
-verbose = 0
-window_height = 1032
-window_width = 1872
-
-[main]
-default_editor = "emacs %f"
-magic = 14
-memlimit = 1000
-running_provers_max = 8
-timelimit = 5
-
-[prover]
-alternative = "noBV"
-command = "colibri2 %f"
-driver = "./colibri2.drv"
-editor = ""
-in_place = false
-interactive = false
-name = "Colibri2"
-shortcut = "colibri2"
-version = "0.0.1"
--
GitLab