diff options
author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-31 11:11:56 +0200 |
---|---|---|
committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-31 11:11:56 +0200 |
commit | 07c9b3e72062693c8dc3fb6b5455e9e0a1e6f890 (patch) | |
tree | 6da3db924d0839abf0e11153d79f080d7d627d89 /abstract/enum_domain.ml | |
parent | 1285d1ebe5025066feda9c9c182aad1daf542f1c (diff) | |
parent | ffa7da8b4343f2ce8fee6c0a4409f4de8f4e5024 (diff) | |
download | scade-analyzer-07c9b3e72062693c8dc3fb6b5455e9e0a1e6f890.tar.gz scade-analyzer-07c9b3e72062693c8dc3fb6b5455e9e0a1e6f890.zip |
Merge branch 'refactor'
Diffstat (limited to 'abstract/enum_domain.ml')
-rw-r--r-- | abstract/enum_domain.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml index 68b04f5..b035cc0 100644 --- a/abstract/enum_domain.ml +++ b/abstract/enum_domain.ml @@ -26,6 +26,7 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig val bottom : (id * item list) list -> t val vtop : t -> t (* top with same vars *) val is_bot : t -> bool + val is_top : t -> bool (* variable management *) val vars : t -> (id * item list) list @@ -67,6 +68,7 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct let vtop x = { x with value = VarMap.empty } let bottom vars = raise Bot (* we don't represent Bot *) let is_bot x = false + let is_top x = VarMap.is_empty x.value let vars x = x.vars @@ -197,6 +199,11 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct let vtop x = { x with value = VarMap.empty } let bottom vars = raise Bot (* we don't represent Bot *) let is_bot x = false + let is_top x = + VarMap.for_all + (fun k v -> List.for_all (fun vv -> List.mem vv v) + (List.assoc k x.vars)) + x.value let vars x = x.vars |