[LRA] Bump to ocplib-simplex.0.5

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: [

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

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"))
          )
 )