X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fauto%2Fformula.ml;h=097114e1200838e6ebbfa35f1530c2bff4ad77bf;hp=7128ba4194648d6f1779130f43425fcbf67e031c;hb=c711ac43406b5d9bcb4856b0cb68789f48f461e7;hpb=35c32fbd2543a399cc6939f21317bebf37172646

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