diff --git a/src/solver.ml b/src/solver.ml
index b5285101fbae8d9d014388b9af4eb845a8d9dcc7..6aba0226748dad1786cb750a4795a0462c7ccad6 100644
--- a/src/solver.ml
+++ b/src/solver.ml
@@ -849,15 +849,33 @@ module Delayed = struct
assert (t.env.current_delayed == t);
index_t t.env sem s
- let are_waiting_cl_change
- (type k) (type d) d cl (dem:(k,d) dem) : k list =
- Bag.fold_left (fun acc event ->
- match event with
- | Events.Wait.Event(dem',event) ->
- match Dem.Eq.eq_type dem dem' with
- | Some (Eqtype.Eq, Eqtype.Eq) -> (event:k)::acc
- | None -> acc
- ) [] (Cl.M.find_def Bag.empty cl d.env.event)
+ let attached_propa_cl
+ (type k) (type d) d cl (dem:(k,d) dem) : k Enum.t =
+ Enum.from_list
+ ~filter:(function
+ | Events.Wait.Event(dem',event) ->
+ Dem.equal dem dem'
+ )
+ ~map:(function
+ | Events.Wait.Event(dem',event) ->
+ match Dem.Eq.coerce_type dem dem' with
+ | Eqtype.Eq, Eqtype.Eq -> (event:k)
+ )
+ (Cl.M.find_def [] cl d.env.event_propa)
+
+ let attached_cl
+ (type k) (type d) d cl (dem:(k,d) dem) : k Enum.t =
+ Enum.from_bag
+ ~filter:(function
+ | Events.Wait.Event(dem',event) ->
+ Dem.equal dem dem'
+ )
+ ~map:(function
+ | Events.Wait.Event(dem',event) ->
+ match Dem.Eq.coerce_type dem dem' with
+ | Eqtype.Eq, Eqtype.Eq -> (event:k)
+ )
+ (Cl.M.find_def Bag.empty cl d.env.event)
(** *)
@@ -1375,9 +1393,12 @@ module type Ro = sig
val get_env : t -> 'a env -> 'a
val set_env: t -> 'a env -> 'a -> unit
- (** Register for events *)
- val are_waiting_cl_change:
- t -> Cl.t -> ('event,'d) dem -> 'event list
+
+ (** Registered for events *)
+ val attached_propa_cl:
+ t -> Cl.t -> ('event,'d) dem -> 'event Enum.t
+ val attached_cl:
+ t -> Cl.t -> ('event,'d) dem -> 'event Enum.t
end
type d = Delayed.t
diff --git a/src/solver.mli b/src/solver.mli
index 1858c185e4ba5e6d629abb6cbcb0193257ae32ef..34d44329076a0cf0d49a4df294732b690e1c40d2 100644
--- a/src/solver.mli
+++ b/src/solver.mli
@@ -107,9 +107,12 @@ module type Ro = sig
val get_env : t -> 'a env -> 'a
val set_env: t -> 'a env -> 'a -> unit
- (** Register for events *)
- val are_waiting_cl_change:
- t -> Cl.t -> ('event,'d) dem -> 'event list
+ (** Registered for events *)
+ val attached_propa_cl:
+ t -> Cl.t -> ('event,'d) dem -> 'event Enum.t
+ val attached_cl:
+ t -> Cl.t -> ('event,'d) dem -> 'event Enum.t
+
end
module Ro : Ro
diff --git a/src/util/bag.ml b/src/util/bag.ml
index 3096378799cbd0f26128a87493b3a742bbe74ecb..a8771a7320c8bdb00c5ead61b59c2b02e557cccc 100644
--- a/src/util/bag.ml
+++ b/src/util/bag.ml
@@ -113,6 +113,22 @@ let rec fold_right f t w = match t with
| List xs -> List.fold_right f xs w
| Concat(a,b) -> fold_right f a (fold_right f b w)
+let rec for_all f = function
+ | Empty -> true
+ | Elt x -> f x
+ | Add(x,t) -> f x && for_all f t
+ | App(t,x) -> for_all f t && f x
+ | List xs -> List.for_all f xs
+ | Concat(a,b) -> for_all f a && for_all f b
+
+let rec exists f = function
+ | Empty -> false
+ | Elt x -> f x
+ | Add(x,t) -> f x || exists f t
+ | App(t,x) -> exists f t || f x
+ | List xs -> List.exists f xs
+ | Concat(a,b) -> exists f a || exists f b
+
let rec filter f = function
| Empty -> Empty
| Elt x as e -> if f x then e else Empty
diff --git a/src/util/bag.mli b/src/util/bag.mli
index 8cdc7157bb7ee2ca766575c03d79cecdb935573a..8866a429904380578e38856571f630608414aa4c 100644
--- a/src/util/bag.mli
+++ b/src/util/bag.mli
@@ -40,6 +40,8 @@ val umap : ('a -> 'b t) -> 'a t -> 'b t
val iter : ('a -> unit) -> 'a t -> unit
val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
val fold_right : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+val for_all : ('a -> bool) -> 'a t -> bool
+val exists : ('a -> bool) -> 'a t -> bool
val filter : ('a -> bool) -> 'a t -> 'a t
val partition : ('a -> bool) -> 'a t -> 'a t * 'a t
diff --git a/src/util/enum.ml b/src/util/enum.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2803db944fbb4a53b9094ba6b139b19d761c4b79
--- /dev/null
+++ b/src/util/enum.ml
@@ -0,0 +1,80 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2013 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+type 'a t =
+ | List: (** content *) 'b list *
+ (** filter *) ('b -> bool) *
+ (** map *) ('b -> 'a) -> 'a t
+ | Bag: (** content *) 'b Bag.t *
+ (** filter *) ('b -> bool) *
+ (** map *) ('b -> 'a) -> 'a t
+
+let fold f acc t =
+ match t with
+ | List (content,filter,map) ->
+ List.fold_left
+ (fun acc x -> if filter x then f acc (map x) else acc)
+ acc content
+ | Bag (content,filter,map) ->
+ Bag.fold_left
+ (fun acc x -> if filter x then f acc (map x) else acc)
+ acc content
+
+let iter f t =
+ match t with
+ | List (content,filter,map) ->
+ List.iter (fun x -> if filter x then f (map x)) content
+ | Bag (content,filter,map) ->
+ Bag.iter (fun x -> if filter x then f (map x)) content
+
+let for_all f t =
+ match t with
+ | List (content,filter,map) ->
+ List.for_all (fun x -> not (filter x) || f (map x)) content
+ | Bag (content,filter,map) ->
+ Bag.for_all (fun x -> not (filter x) || f (map x)) content
+
+let exists f t =
+ match t with
+ | List (content,filter,map) ->
+ List.exists (fun x -> filter x && f (map x)) content
+ | Bag (content,filter,map) ->
+ Bag.exists (fun x -> filter x && f (map x)) content
+
+let is_empty t = exists (fun _ -> true) t
+
+let list_rev t =
+ match t with
+ | List (content,filter,map) ->
+ List.fold_left
+ (fun acc x -> if filter x then (map x)::acc else acc)
+ [] content
+ | Bag (content,filter,map) ->
+ Bag.fold_left
+ (fun acc x -> if filter x then (map x)::acc else acc)
+ [] content
+
+let from_list ?(filter=(fun _ -> true)) ~map content =
+ List(content,filter,map)
+
+let from_bag ?(filter=(fun _ -> true)) ~map content =
+ Bag(content,filter,map)
diff --git a/src/util/enum.mli b/src/util/enum.mli
new file mode 100644
index 0000000000000000000000000000000000000000..07008895a432f4685f7d918dc73e4285ade3192a
--- /dev/null
+++ b/src/util/enum.mli
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2013 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Use enum for deforesting *)
+
+type 'a t
+
+val for_all: ('a -> bool) -> 'a t -> bool
+val exists: ('a -> bool) -> 'a t -> bool
+val is_empty: 'a t -> bool
+
+val fold: ('acc -> 'a -> 'acc) -> 'acc -> 'a t -> 'acc
+val iter: ('a -> unit) -> 'a t -> unit
+
+val list_rev: 'a t -> 'a list
+(** return the enumeration in the reverse order *)
+
+(** Create Enum *)
+val from_list: ?filter:('b -> bool) -> map:('b -> 'a) -> 'b list -> 'a t
+val from_bag : ?filter:('b -> bool) -> map:('b -> 'a) -> 'b Bag.t -> 'a t