Add fold_left/right functions to the set interface (iterate in

increasing/decreasing order of keys).

diff --git a/src/common_sig.ml b/src/common_sig.ml
index 1bb80a9..0e53b92 100644 (file)
--- a/src/common_sig.ml
+++ b/src/common_sig.ml
@@ -88,6 +88,8 @@ sig
   val subset : t -> t -> bool
   val iter : (elt -> unit) -> t -> unit
   val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+  val fold_left : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+  val fold_right : (elt -> 'a -> 'a) -> t -> 'a -> 'a
   val for_all : (elt -> bool) -> t -> bool
   val exists : (elt -> bool) -> t -> bool
   val filter : (elt -> bool) -> t -> t

diff --git a/src/finiteCofinite.ml b/src/finiteCofinite.ml
index 019ae65..9963e1f 100644 (file)
--- a/src/finiteCofinite.ml
+++ b/src/finiteCofinite.ml
@@ -141,6 +141,14 @@ struct
     | Finite s -> E.fold f s a
     | CoFinite _ -> raise exn
 
+  let fold_left f t a = match t.node with
+    | Finite s -> E.fold_left f s a
+    | CoFinite _ -> raise exn
+
+  let fold_right f t a = match t.node with
+    | Finite s -> E.fold_right f s a
+    | CoFinite _ -> raise exn
+
   let iter f t = match t.node with
     | Finite t -> E.iter f t
     | CoFinite _ -> raise exn
@@ -202,12 +210,12 @@ struct
     | CoFinite _ -> raise exn
 
   let positive t = match t.node with
-      | Finite x -> x
-      | CoFinite _ -> E.empty
+    | Finite x -> x
+    | CoFinite _ -> E.empty
 
   let negative t = match t.node with
-      | CoFinite x -> x
-      | Finite _ -> E.empty
+    | CoFinite x -> x
+    | Finite _ -> E.empty
 
   let inj_positive t = finite t
   let inj_negative t = cofinite t

diff --git a/src/ptset.ml b/src/ptset.ml
index 87ca2a5..08332b3 100644 (file)
--- a/src/ptset.ml
+++ b/src/ptset.ml
@@ -289,11 +289,17 @@ struct
   | Leaf k -> f k
   | Branch (_,_,t0,t1) -> iter f t0; iter f t1
 
-  let rec fold f s accu = match s.Node.node with
+  let rec fold_left f s accu = match s.Node.node with
   | Empty -> accu
   | Leaf k -> f k accu
-  | Branch (_,_,t0,t1) -> fold f t1 (fold f t0 accu)
+  | Branch (_,_,t0,t1) -> fold_left f t1 (fold_left f t0 accu)
 
+  let rec fold_right f s accu = match s.Node.node with
+  | Empty -> accu
+  | Leaf k -> f k accu
+  | Branch (_,_,t0,t1) -> fold_right f t0 (fold_right f t1 accu)
+
+  let fold f s accu = fold_left f s accu
 
   let rec for_all p n = match n.Node.node with
   | Empty -> true

diff --git a/src/run.ml b/src/run.ml
index e356128..53cecb4 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -465,9 +465,9 @@ DEFINE AND_(t1,t2) =
           cache.(T.preorder tree node).NodeStatus.node.sat
     in
     loop (T.root tree);
-    List.rev (StateSet.fold
-                (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
-                (Ata.get_selecting_states auto) [])
+    (StateSet.fold_right
+       (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
+       (Ata.get_selecting_states auto) [])
 
   let prepare_run run list =
     let tree = run.tree in