diff options
Diffstat (limited to 'abstract/enum_domain.ml')
| -rw-r--r-- | abstract/enum_domain.ml | 29 |
1 files changed, 28 insertions, 1 deletions
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml index ea2b053..4f6aacd 100644 --- a/abstract/enum_domain.ml +++ b/abstract/enum_domain.ml @@ -11,11 +11,15 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig (* construction *) val top : (id * item list) list -> t + val bottom : (id * item list) list -> t + val vtop : t -> t (* top with same vars *) + val is_bot : t -> bool (* variable management *) val vars : t -> (id * item list) list val forgetvar : t -> id -> t + val forgetvars : t -> id list -> t val project : t -> id -> item list (* set-theoretic operations *) @@ -27,6 +31,7 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig (* abstract operations *) val apply_cons : t -> enum_cons -> t list (* may disjunct *) + val apply_cl : t -> enum_cons list -> t (* join any disjunction ; may raise Bot *) val assign : t -> (id * id) list -> t (* pretty-printing *) @@ -47,11 +52,15 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct } let top vars = { vars; value = VarMap.empty } + let vtop x = { x with value = VarMap.empty } + let bottom vars = raise Bot (* we don't represent Bot *) + let is_bot x = false let vars x = x.vars let forgetvar x id = { x with value = VarMap.remove id x.value } + let forgetvars = List.fold_left forgetvar let project x id = try [VarMap.find id x.value] with Not_found -> List.assoc id x.vars @@ -108,7 +117,14 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct (List.filter (cc op s) (List.assoc id2 x.vars)) | Some s, Some t -> if cc op s t then [x] else [] - + + let apply_cl x l = + List.fold_left + (fun k c -> match apply_cons k c with + | [] -> raise Bot + | p::q -> List.fold_left join p q ) + x l + let assign x idl = let v = List.fold_left (fun v (id, id2) -> @@ -163,11 +179,15 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct let uniq x = uniq_sorted (sort x) let top vars = { vars; value = VarMap.empty } + let vtop x = { x with value = VarMap.empty } + let bottom vars = raise Bot (* we don't represent Bot *) + let is_bot x = false let vars x = x.vars let forgetvar x id = { x with value = VarMap.remove id x.value } + let forgetvars = List.fold_left forgetvar let project x id = try VarMap.find id x.value with Not_found -> List.assoc id x.vars @@ -220,6 +240,13 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct | [] -> l | _ -> { x with value = VarMap.add id2 v2 x.value }::l) [] v1 + + let apply_cl x l = + List.fold_left + (fun k c -> match apply_cons k c with + | [] -> raise Bot + | p::q -> List.fold_left join p q ) + x l let assign x idl = let v = List.fold_left |