Extend the interface with a fold function (over the structure

[tatoo.git] / src / auto / formula.ml

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