X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fauto%2Fformula.ml;h=097114e1200838e6ebbfa35f1530c2bff4ad77bf;hp=70407cf7fd1cd38b1c2f857e0d4de299870d8433;hb=03b6a364e7240ca827585e7baff225a0aaa33bc6;hpb=30bc0bb1291426e5e26eb2dee1ffc41e4c246349

diff --git a/src/auto/formula.ml b/src/auto/formula.ml
index 70407cf..097114e 100644
--- a/src/auto/formula.ml
+++ b/src/auto/formula.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-02-07 10:00:33 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-09 11:16:29 CET by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -26,28 +26,23 @@ open Utils
 
 (** Implementation of hashconsed Boolean formulae *)
 
-type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ]
-
-(** Direction for automata predicates *)
 *)
-module type PREDICATE =
+module type ATOM =
 sig
   type t
-  type ctx
-  val eval : ctx -> t -> bool
   val neg : t -> t
   include Hcons.Abstract with type t := t
-  include Sigs.AUX.Printable with type t := t
+  include Common_sig.Printable with type t := t
 end
 
-type ('formula,'pred) expr =
+type ('formula,'atom) expr =
   | False
   | True
   | Or of 'formula * 'formula
   | And of 'formula * 'formula
-  | Atom of 'pred
+  | Atom of 'atom
 
-module Make (P: PREDICATE) =
+module Make (P: ATOM) =
 struct
 
 
@@ -61,7 +56,7 @@ struct
 
   module rec Node : Hcons.S
     with type data = Data.t = Hcons.Make (Data)
-    and Data : Hashtbl.HashedType  with type t = Node.t node =
+    and Data : Common_sig.HashedType  with type t = Node.t node =
   struct
     type t =  Node.t node
     let equal x y =
@@ -175,12 +170,13 @@ let and_ f1 f2 =
 
 let of_bool = function true -> true_ | false -> false_
 
-let rec eval ctx f =
-  match f.Node.node.pos with
-    True -> true
-  | False -> false
-  | Atom p -> P.eval ctx p
-  | And(f1, f2) -> eval ctx f1 && eval ctx f2
-  | Or(f1, f2) -> eval ctx f1 || eval ctx f2
+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