diff options
Diffstat (limited to 'abstract/nonrelational.ml')
| -rw-r--r-- | abstract/nonrelational.ml | 48 |
1 files changed, 35 insertions, 13 deletions
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index f5c9a04..b83edc1 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -13,6 +13,7 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct type env = V.t VarMap.t type t = Env of env | Bot + type itv = Value_domain.itv let init = Env VarMap.empty let bottom = Bot @@ -63,6 +64,10 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct | Env env -> List.map (fun (k, _) -> (k, false)) (VarMap.bindings env) let vbottom _ = bottom + let var_itv x id = match x with + | Bot -> Value_domain.Bot + | Env env -> V.to_itv (get_var env id) + (* Set-theoretic operations *) let join a b = match a, b with | Bot, x | x, Bot -> x @@ -196,22 +201,39 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct (* pretty-printing *) let print_vars fmt env ids = match env with - | Bot -> Format.fprintf fmt "bottom" + | Bot -> Format.fprintf fmt "⊥" | Env env -> - Format.fprintf fmt "@[<hov 2>["; - let _ = List.fold_left - (fun nf id -> - let v = get_var env id in - if v <> V.top then begin - if nf then Format.fprintf fmt ",@ "; - Format.fprintf fmt "%s in %s" id (V.to_string (get_var env id)); - true - end else nf) - false - ids - in Format.fprintf fmt "]@]" + Format.fprintf fmt "@[<v 2>{ "; + let l = List.map (fun id -> (get_var env id, id)) ids in + let s = List.sort Pervasives.compare l in + let rec bl = function + | [] -> [] + | (v, id)::q when v <> V.top -> + begin match bl q with + | (vv, ids)::q when vv = v -> (v, id::ids)::q + | r -> (v, [id])::r + end + | _::q -> bl q + in + let sbl = bl s in + List.iteri + (fun j (v, ids) -> + if j > 0 then Format.fprintf fmt "@ "; + List.iteri + (fun i id -> + if i > 0 then Format.fprintf fmt ", "; + Format.fprintf fmt "%a" Formula_printer.print_id id) + ids; + match V.as_const v with + | Some i -> Format.fprintf fmt " = %d" i + | _ -> Format.fprintf fmt " ∊ %s" (V.to_string v)) + sbl; + Format.fprintf fmt " }@]" let print_all fmt x = print_vars fmt x (List.map fst (vars x)) + + let print_itv fmt x = + Format.fprintf fmt "%s" (string_of_itv x) end |