X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fformula.ml;h=1e440bc23f9778bd7c4c68bed85a93ea026d1136;hp=ad774ea7f22f3e1fd729c50661ce027c047f9779;hb=41dd1fed04cabad212f10fce3484545f6e9d9444;hpb=d9c0e4863807eaf472e875a4bad35cfefe985c95

diff --git a/src/formula.ml b/src/formula.ml
index ad774ea..1e440bc 100644
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -13,41 +13,31 @@
 (*                                                                     *)
 (***********************************************************************)
 
-(*
-  Time-stamp: <Last modified on 2013-02-06 14:30:27 CET by Kim Nguyen>
-*)
-
 INCLUDE "utils.ml"
 
 open Format
 
-
 (*
 
 (** 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 +51,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 +165,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