From c711ac43406b5d9bcb4856b0cb68789f48f461e7 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= <kn@lri.fr>
Date: Sat, 9 Mar 2013 11:19:21 +0100
Subject: [PATCH] Extend the interface with a fold function (over the structure
 of the formula).

---
 src/auto/formula.ml  | 11 ++++++++++-
 src/auto/formula.mli |  5 ++++-
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/auto/formula.ml b/src/auto/formula.ml
index 7128ba4..097114e 100644
--- 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
--- 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
-- 
2.17.1