diff options
Diffstat (limited to 'abstract/nonrelational.ml')
| -rw-r--r-- | abstract/nonrelational.ml | 34 |
1 files changed, 19 insertions, 15 deletions
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index 3e978ce..b3129c0 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -201,21 +201,25 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct | _::q -> bl q in let sbl = bl s in - Format.fprintf fmt "@[<v 2>{ "; - List.iteri - (fun j (v, ids) -> - if j > 0 then Format.fprintf fmt "@ "; - Format.fprintf fmt "@[<hov 4>"; - 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 " }@]" + if sbl = [] then + Format.fprintf fmt "⊤" + else begin + Format.fprintf fmt "@[<v 2>{ "; + List.iteri + (fun j (v, ids) -> + if j > 0 then Format.fprintf fmt "@ "; + Format.fprintf fmt "@[<hov 4>"; + 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 " }@]" + end let print fmt x = print_vars fmt x (List.map fst (vars x)) |