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

diff --git a/src/auto/formula.ml b/src/auto/formula.ml
index a27ffc6..097114e 100644
--- a/src/auto/formula.ml
+++ b/src/auto/formula.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-04 22:52:17 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-09 11:16:29 CET by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -27,24 +27,22 @@ open Utils
 (** Implementation of hashconsed Boolean formulae *)
 
 *)
-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 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
 
 
@@ -172,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