Extend the interface with a fold function (over the structure

of the formula).

diff --git a/src/auto/formula.ml b/src/auto/formula.ml
index 7128ba4..097114e 100644 (file)
--- a/src/auto/formula.ml
+++ b/src/auto/formula.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-09 11:12:54 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-09 11:16:29 CET by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -170,4 +170,13 @@ let and_ f1 f2 =
 
 let of_bool = function true -> true_ | false -> false_
 
+let fold f phi acc =
+  let rec loop phi acc =
+    match expr phi with
+    | And (phi1, phi2) | Or(phi1, phi2)  ->
+        loop phi2 (loop phi1 (f phi acc))
+    | _ -> f phi acc
+  in
+  loop phi acc
+
 end

diff --git a/src/auto/formula.mli b/src/auto/formula.mli
index 2421d51..d708c2d 100644 (file)
--- a/src/auto/formula.mli
+++ b/src/auto/formula.mli
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-09 11:13:06 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-09 11:16:45 CET by Kim Nguyen>
 *)
 
 module type ATOM =
@@ -84,4 +84,7 @@ sig
   val of_bool : bool -> t
   (** Convert an ocaml Boolean value to a formula *)
 
+  val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
+  (** [fold f phi acc] folds [f] over the formula structure *)
+
 end