summaryrefslogtreecommitdiff
path: root/abstract/apron_domain.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/apron_domain.ml')
-rw-r--r--abstract/apron_domain.ml184
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 =
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-09 16:08:01 +0000