X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fauto%2Fformula.mli;h=d708c2d16835a63d69f96b1f247c9dc18faf14c0;hp=3cf240d2899bb5d8cadba296f9eaf08de5f68bf0;hb=03b6a364e7240ca827585e7baff225a0aaa33bc6;hpb=30bc0bb1291426e5e26eb2dee1ffc41e4c246349

diff --git a/src/auto/formula.mli b/src/auto/formula.mli
index 3cf240d..d708c2d 100644
--- a/src/auto/formula.mli
+++ b/src/auto/formula.mli
@@ -14,30 +14,28 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-02-07 10:03:26 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-09 11:16:45 CET by Kim Nguyen>
 *)
 
-module type PREDICATE =
+module type ATOM =
 sig
   type t
-  type ctx
-  val eval : ctx -> t -> bool
   val neg : t -> t
   include Utils.Hcons.Abstract with type t := t
-  include Utils.Sigs.AUX.Printable with type t := t
+  include Utils.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
 
 (** View of the internal representation of a formula,
     used for pattern matching *)
 
-module Make(P : PREDICATE) :
+module Make(P : ATOM) :
 sig
   type t
 
@@ -53,7 +51,7 @@ sig
   (** Equality over formulae *)
 
   val expr : t -> (t,P.t) expr
-  (** Equality over formulae *)
+  (** Return a view of the formulae *)
 
   val compare : t -> t -> int
   (** Comparison of formulae *)
@@ -86,6 +84,7 @@ sig
   val of_bool : bool -> t
   (** Convert an ocaml Boolean value to a formula *)
 
-  val eval : P.ctx -> t -> bool
-    (** Evaluate a formula given a context for atomic predicates *)
+  val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
+  (** [fold f phi acc] folds [f] over the formula structure *)
+
 end