diff options
| -rw-r--r-- | abstract/abs_domain.ml | 21 | ||||
| -rw-r--r-- | abstract/abs_interp.ml | 8 | ||||
| -rw-r--r-- | tests/source/half.scade | 2 |
3 files changed, 22 insertions, 9 deletions
diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml index a30713a..64eefc7 100644 --- a/abstract/abs_domain.ml +++ b/abstract/abs_domain.ml @@ -223,8 +223,23 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct let var_itv x id = if List.mem_assoc id x.nvars - then IN (VMap.map (fun v -> ND.var_itv v id) x.value) - else not_implemented "var_itv for enum variable" + then + let x = List.fold_left + (fun x (v, _) -> + if v.[0] = 'N' || (String.length v > 3 && String.sub v 0 3 = "pre") + then forgetvar x v else x) + x x.evars in + IN (VMap.map (fun v -> ND.var_itv v id) x.value) + else + let all = List.fold_left (fun a b -> SSet.add b a) SSet.empty + (List.assoc id x.evars) in + IE + (VMap.fold + (fun enum _ s -> + try SSet.add (VarMap.find id enum) s + with Not_found -> all) + x.value + SSet.empty) let set_disjunct x id p = { x with @@ -356,7 +371,7 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct { x with value = VMap.empty } let print_all fmt x = - Format.fprintf fmt "@[<v 0>"; + Format.fprintf fmt "@[<v>"; VMap.iter (fun enum num -> Format.fprintf fmt "@[<hv 2>{ %a ∧@ %a }@]@ " diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 7a53134..e55f199 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -127,14 +127,12 @@ end = struct let do_prog widen_delay rp = let st = init_state widen_delay rp in - let final, final_c = loop st st.env in + let final_nc, final = loop st st.env in Format.printf "@[<hov>F %a@]@.@." - E.print_all final; - (* + E.print_all final_nc; Format.printf "@[<hov>F' %a@]@.@." - E.print_all final_c; - *) + E.print_all final; let check_guarantee (id, f) = let cl = Formula.conslist_of_f f in diff --git a/tests/source/half.scade b/tests/source/half.scade index da90586..541e81c 100644 --- a/tests/source/half.scade +++ b/tests/source/half.scade @@ -1,4 +1,4 @@ -node test(i: int) returns (a, b, probe c: int; exit: bool) +node test(i: int) returns (probe a, probe b, probe c: int; exit: bool) var la, lb: int; half: bool; |