From e83e38382f958044f47078a498d56ce00f2cc1a4 Mon Sep 17 00:00:00 2001
From: hra687261 <hichem.ait-el-hara@ocamlpro.com>
Date: Mon, 5 Dec 2022 13:09:48 +0100
Subject: [PATCH] [LRA] Bump to ocplib-simplex.0.5
---
colibri2.opam | 2 +-
colibri2/theories/LRA/simplex.ml | 36 +++++++++++++++++---------------
dune-project | 2 +-
3 files changed, 21 insertions(+), 19 deletions(-)
diff --git a/colibri2.opam b/colibri2.opam
index 8c522e291..e6d656934 100644
--- a/colibri2.opam
+++ b/colibri2.opam
@@ -36,7 +36,7 @@ depends: [
"farith"
"ounit2" {>= "2.2.4" & with-test}
"ocaml" {>= "4.12"}
- "ocplib-simplex" {= "0.4"}
+ "ocplib-simplex" {>= "0.5"}
"odoc" {with-doc}
]
build: [
diff --git a/colibri2/theories/LRA/simplex.ml b/colibri2/theories/LRA/simplex.ml
index 3673a8f9e..6947d65f7 100644
--- a/colibri2/theories/LRA/simplex.ml
+++ b/colibri2/theories/LRA/simplex.ml
@@ -57,6 +57,7 @@ module Rat = struct
let mult = A.mul
let minus = A.neg
let is_m_one v = A.equal v m_one
+ let ceiling = ceil
end
module Sim = OcplibSimplex.Basic.Make (Var) (Rat) (Ex)
@@ -211,19 +212,19 @@ let of_bound_sup = function
| No -> None
| Large q ->
assert (A.is_real q);
- Some (q, A.zero)
+ Some Sim.Core.{ bvalue = R2.of_r q; explanation = () }
| Strict q ->
assert (A.is_real q);
- Some (q, A.minus_one)
+ Some Sim.Core.{ bvalue = R2.upper q; explanation = () }
let of_bound_inf = function
| No -> None
| Large q ->
assert (A.is_real q);
- Some (q, A.zero)
+ Some Sim.Core.{ bvalue = R2.of_r q; explanation = () }
| Strict q ->
assert (A.is_real q);
- Some (q, A.one)
+ Some Sim.Core.{ bvalue = R2.lower q; explanation = () }
let find_equalities d vars (env : Sim.Core.t) (s : Sim.Core.solution Lazy.t) =
(* Env must be sat *)
@@ -281,7 +282,7 @@ let find_equalities d vars (env : Sim.Core.t) (s : Sim.Core.solution Lazy.t) =
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 (A.of_int 2))) () None ()
+ Sim.Assert.poly env p ?min:(of_bound_inf (Large (A.of_int 2))) n
in
let env' = Sim.Solve.solve env' in
let s =
@@ -294,9 +295,10 @@ let find_equalities d vars (env : Sim.Core.t) (s : Sim.Core.solution Lazy.t) =
| Sim.Core.Max (m, s) ->
let m = Lazy.force m in
(* 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;
+ (if m.is_le then Delta.add_le else Delta.add_lt) d a m.max_v.bvalue.v b;
let notdistinct =
- if is_int then A.lt (A.abs m.max_v) A.one else A.equal m.max_v A.zero
+ if is_int then A.lt (A.abs m.max_v.bvalue.v) A.one
+ else A.equal m.max_v.bvalue.v A.zero
in
if notdistinct then (`NotDistinct, env, s) else (`Distinct, env, s)
in
@@ -341,28 +343,28 @@ let update_domains d env =
if Egraph.is_registered d n then
let inf =
Base.Option.map
- ~f:(fun (q1, q2) ->
- let s = A.sign q2 in
+ ~f:(fun { bvalue = { v; offset }; _ } ->
+ let s = A.sign offset in
let b =
if s = 0 then Bound.Large
else if s > 0 then Strict
else assert false
(* Why? *)
in
- (q1, b))
+ (v, b))
v.mini
in
let sup =
Base.Option.map
- ~f:(fun (q1, q2) ->
- let s = A.sign q2 in
+ ~f:(fun { bvalue = { v; offset }; _ } ->
+ let s = A.sign offset in
let b =
if s = 0 then Bound.Large
else if s < 0 then Strict
else assert false
(* Why? *)
in
- (q1, b))
+ (v, b))
v.maxi
in
let v = Dom_interval.D.from_convexe_hull (inf, sup) in
@@ -380,7 +382,7 @@ let simplex (d : Egraph.wt) =
Datastructure.Push.fold comparisons d ~f:(make_equations d)
~init:(Polynome.H.create 10, Node.S.empty)
in
- let env = Sim.Core.empty ~is_int:false ~check_invs:false ~debug:0 in
+ let env = Sim.Core.empty ~is_int:false ~check_invs:false in
let of_poly (p : Polynome.t) =
Node.M.fold
(fun n r acc -> fst (Sim.Core.P.accumulate n r acc))
@@ -400,7 +402,7 @@ let simplex (d : Egraph.wt) =
(conv inf, conv sup)
in
let env, _ =
- Sim.Assert.var env v (of_bound_inf inf) () (of_bound_sup sup) ()
+ Sim.Assert.var env v ?min:(of_bound_inf inf) ?max:(of_bound_sup sup)
in
env
in
@@ -415,7 +417,7 @@ let simplex (d : Egraph.wt) =
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
+ let env, _ = Sim.Assert.var env n ?min:inf ?max:sup in
(env, vars))
else
let inf = of_bound_inf eq.inf in
@@ -423,7 +425,7 @@ let simplex (d : Egraph.wt) =
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
+ let env, _ = Sim.Assert.poly env (of_poly p) n ?min:inf ?max:sup in
(env, vars)
in
let env, vars = Polynome.H.fold add_eqs eqs (env, vars) in
diff --git a/dune-project b/dune-project
index a268a6e45..37ef02e9f 100644
--- a/dune-project
+++ b/dune-project
@@ -78,6 +78,6 @@
"farith"
("ounit2" (and (>= "2.2.4") :with-test))
("ocaml" (>= "4.12"))
- ("ocplib-simplex" (= "0.4"))
+ ("ocplib-simplex" (>= "0.5"))
)
)
--
GitLab