Plug into Apron Box domain for intervals.

1 files changed, 111 insertions, 73 deletions

diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index 58cd544..e1b3007 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -11,18 +11,16 @@ open Apron
   Mostly direct translation between the two.
 *)
 
-(* Polyhedra *)
-
-module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct
+module Common = struct
 
-    (* manager *)
-    type man = Polka.loose Polka.t
-    let manager = Polka.manager_alloc_loose ()
-
-    type itv = Interval.t
-
-    (* abstract elements *)
-    type t = man Abstract1.t
+    let v_env vars = 
+        let intv = List.map
+              (fun (s, _) -> Var.of_string s)
+              (List.filter (fun (_, n) -> not n) vars) in
+        let realv = List.map
+              (fun (s, _) -> Var.of_string s)
+              (List.filter (fun (_, n) -> n) vars) in
+        (Environment.make (Array.of_list intv) (Array.of_list realv))
 
     (* direct translation of numerical expressions into Apron tree expressions *)
     let rec texpr_of_nexpr = function
@@ -67,16 +65,107 @@ module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct
           | CONS_GE -> Tcons1.SUPEQ
         in Tcons1.make (Texpr1.of_expr env (texpr_of_nexpr eq)) op
 
+end
+
+(* Apron Boxes (intervals) *)
+
+module ND_Box : NUMERICAL_ENVIRONMENT_DOMAIN = struct
+
+    open Common
+
+    (* manager *)
+    type man = Box.t
+    let manager = Box.manager_alloc ()
+
+    type itv = Interval.t
+
+    (* abstract elements *)
+    type t = man Abstract1.t
+
     (* implementation *)
-    let v_env vars = 
-        let intv = List.map
-              (fun (s, _) -> Var.of_string s)
-              (List.filter (fun (_, n) -> not n) vars) in
-        let realv = List.map
-              (fun (s, _) -> Var.of_string s)
-              (List.filter (fun (_, n) -> n) vars) in
-        (Environment.make (Array.of_list intv) (Array.of_list realv))
+    let top vars =
+      Abstract1.top manager (v_env vars)
+    let bottom vars = Abstract1.bottom manager (v_env vars)
+    let is_bot = Abstract1.is_bottom manager
+    let is_top = Abstract1.is_top manager
+
+    let forgetvar x id =
+        let v = [| Var.of_string id |] in
+        Abstract1.forget_array manager x v false
+
+    let vars x =
+        let (ivt, fvt) = Environment.vars (Abstract1.env x) in
+        let ivl = List.map Var.to_string (Array.to_list ivt) in
+        let fvl = List.map Var.to_string (Array.to_list fvt) in
+        (List.map (fun x -> x, false) ivl) @ (List.map (fun x -> x, true) fvl)
+
+    let vbottom x =
+        Abstract1.bottom manager (Abstract1.env x)
+
+    let project x id =
+        Abstract1.bound_variable manager x (Var.of_string id)
+
+    (* Apply some formula to the environment *)
+    let apply_cl x cons =
+        let env = Abstract1.env x in
+        let tca = Array.of_list (List.map (tcons_of_cons env) cons) in
+        let ar = Tcons1.array_make env (Array.length tca) in
+        Array.iteri (Tcons1.array_set ar) tca;
+        Abstract1.meet_tcons_array manager x ar
+
+    let apply_cons x cons = apply_cl x [cons]
+
+
+    let assign x eqs =
+      let env = Abstract1.env x in
+      let vars = Array.of_list
+        (List.map (fun (id, _) -> Var.of_string id) eqs) in
+      let vals = Array.of_list
+        (List.map (fun (_, v) -> Texpr1.of_expr env (texpr_of_nexpr v)) eqs) in
+      Abstract1.assign_texpr_array manager x vars vals None
+
+    
+    (* Ensemblistic operations *)
+    let join = Abstract1.join manager
+    let meet = Abstract1.meet manager
+    let widen = Abstract1.widening manager
+
+    let subset = Abstract1.is_leq manager
+    let eq = Abstract1.is_eq manager
+
+    (* Pretty-printing *)
+    let print fmt x =
+        Abstract1.minimize manager x;
+        Format.fprintf fmt "%a@?" Abstract1.print x
+
+    let print_vars fmt x idl = 
+        let prevars = vars x in
+        let rm_vars_l = List.filter (fun (id, _) -> not (List.mem id idl)) prevars in
+        let rm_vars = Array.of_list
+          (List.map (fun (id, _) -> Var.of_string id) rm_vars_l) in
+        let xx = Abstract1.forget_array manager x rm_vars false in
+        print fmt xx
+
+    let print_itv = Interval.print
+
+end
+
+(* Polyhedra *)
+
+module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct
 
+    open Common
+
+    (* manager *)
+    type man = Polka.loose Polka.t
+    let manager = Polka.manager_alloc_loose ()
+
+    type itv = Interval.t
+
+    (* abstract elements *)
+    type t = man Abstract1.t
+
+    (* implementation *)
     let top vars =
       Abstract1.top manager (v_env vars)
     let bottom vars = Abstract1.bottom manager (v_env vars)
@@ -129,7 +218,7 @@ module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct
 
     (* Pretty-printing *)
     let print fmt x =
-        if not (Oct.manager_is_oct manager) then Abstract1.minimize manager x;
+        Abstract1.minimize manager x;
         Format.fprintf fmt "%a@?" Abstract1.print x
 
     let print_vars fmt x idl = 
@@ -149,6 +238,8 @@ end
 
 module ND_Oct : NUMERICAL_ENVIRONMENT_DOMAIN = struct
 
+    open Common
+
     (* manager *)
     type man = Oct.t
     let manager = Oct.manager_alloc()
@@ -158,59 +249,7 @@ module ND_Oct : NUMERICAL_ENVIRONMENT_DOMAIN = struct
     (* abstract elements *)
     type t = man Abstract1.t
 
-    (* direct translation of numerical expressions into Apron tree expressions *)
-    let rec texpr_of_nexpr = function
-        | NIdent id -> Texpr1.Var (Var.of_string id)
-        | NIntConst i -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_int i))
-        | NRealConst r -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_float r))
-        | NUnary(AST_UPLUS, e, is_real) ->
-            Texpr1.Unop(
-                Texpr1.Cast,
-                texpr_of_nexpr e,
-                (if is_real then Texpr1.Real else Texpr1.Int),
-                Texpr1.Rnd)
-        | NUnary(AST_UMINUS, e, is_real) ->
-            (* APRON bug ? Unary negate seems to not work correctly... *)
-            Texpr1.Binop(
-                Texpr1.Sub,
-                Texpr1.Cst(Coeff.s_of_mpqf (Mpqf.of_string "0")),
-                (texpr_of_nexpr e),
-                (if is_real then Texpr1.Real else Texpr1.Int),
-                Texpr1.Rnd)
-        | NBinary(op, e1, e2, is_real) ->
-            let f = match op with
-            | AST_PLUS -> Texpr1.Add
-            | AST_MINUS -> Texpr1.Sub
-            | AST_MUL -> Texpr1.Mul
-            | AST_DIV -> Texpr1.Div
-            | AST_MOD -> Texpr1.Mod
-            in
-            Texpr1.Binop(
-                  f,
-                  (texpr_of_nexpr e1),
-                  (texpr_of_nexpr e2),
-                  (if is_real then Texpr1.Real else Texpr1.Int),
-                  Texpr1.Rnd)
-    
-    (* direct translation of constraints into Apron constraints *)
-    let tcons_of_cons env (eq, op) =
-        let op = match op with
-          | CONS_EQ -> Tcons1.EQ
-          | CONS_NE -> Tcons1.DISEQ
-          | CONS_GT -> Tcons1.SUP
-          | CONS_GE -> Tcons1.SUPEQ
-        in Tcons1.make (Texpr1.of_expr env (texpr_of_nexpr eq)) op
-
     (* implementation *)
-    let v_env vars = 
-        let intv = List.map
-              (fun (s, _) -> Var.of_string s)
-              (List.filter (fun (_, n) -> not n) vars) in
-        let realv = List.map
-              (fun (s, _) -> Var.of_string s)
-              (List.filter (fun (_, n) -> n) vars) in
-        (Environment.make (Array.of_list intv) (Array.of_list realv))
-
     let top vars =
       Abstract1.top manager (v_env vars)
     let bottom vars = Abstract1.bottom manager (v_env vars)
@@ -263,7 +302,6 @@ module ND_Oct : NUMERICAL_ENVIRONMENT_DOMAIN = struct
 
     (* Pretty-printing *)
     let print fmt x =
-        if not (Oct.manager_is_oct manager) then Abstract1.minimize manager x;
         Format.fprintf fmt "%a@?" Abstract1.print x
 
     let print_vars fmt x idl =