diff options
Diffstat (limited to 'abstract/apron_domain.ml')
| -rw-r--r-- | abstract/apron_domain.ml | 38 |
1 files changed, 18 insertions, 20 deletions
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml index 369f4b7..7a823db 100644 --- a/abstract/apron_domain.ml +++ b/abstract/apron_domain.ml @@ -58,27 +58,23 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct in Tcons1.make (Texpr1.of_expr env (texpr_of_nexpr eq)) op (* implementation *) - let init = Abstract1.top manager (Environment.make [||] [||]) - let bottom = Abstract1.bottom manager (Environment.make [||] [||]) + 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 addvar x id isfloat = - let env = Abstract1.env x in - let env2 = if isfloat then - Environment.add env [||] [| Var.of_string id |] - else - Environment.add env [| Var.of_string id |] [||] - in - Abstract1.change_environment manager x env2 false let forgetvar x id = let v = [| Var.of_string id |] in Abstract1.forget_array manager x v false - let rmvar x id = - let v = [| Var.of_string id |] in - let env = Abstract1.env x in - let env2 = Environment.remove env v in - let y = Abstract1.forget_array manager x v false in - Abstract1.change_environment manager y env2 false let vars x = let (ivt, fvt) = Environment.vars (Abstract1.env x) in @@ -89,17 +85,19 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct let vbottom x = Abstract1.bottom manager (Abstract1.env x) - let var_itv x id = + let project x id = Abstract1.bound_variable manager x (Var.of_string id) (* Apply some formula to the environment *) - let rec apply_ncl x cons = + 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 @@ -119,7 +117,7 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct let eq = Abstract1.is_eq manager (* Pretty-printing *) - let print_all fmt x = + let print fmt x = Abstract1.minimize manager x; Abstract1.print fmt x; Format.fprintf fmt "@?" @@ -130,7 +128,7 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct 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_all fmt xx + print fmt xx let print_itv = Interval.print |