X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fformula.mli;h=e83bca138884c37917f40b528cfca3efdf7106b6;hp=9a0b0665e7d8e30b76fcfa773b84dbcc95122243;hb=d9c0e4863807eaf472e875a4bad35cfefe985c95;hpb=9c0b145d050a5981010435f54848dc862782709c

diff --git a/src/formula.mli b/src/formula.mli
index 9a0b066..e83bca1 100644
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -14,72 +14,78 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-02-04 16:04:03 CET by Kim Nguyễn>
+  Time-stamp: <Last modified on 2013-02-05 16:11:43 CET by Kim Nguyen>
 *)
 
-(** Implementation of hashconsed Boolean formulae *)
-
-type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ]
-
-(** Direction for automata predicates *)
-
-type 'formula expr =
+module type PREDICATE =
+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
+end
+
+type ('formula,'pred) expr =
   | False
   | True
   | Or of 'formula * 'formula
   | And of 'formula * 'formula
-  | Atom of move * bool * State.t
+  | Atom of 'pred
 
 (** View of the internal representation of a formula,
     used for pattern matching *)
 
-type t
-
-(** Abstract type representing hashconsed formulae *)
+module Make(P : PREDICATE) :
+sig
+  type t
 
-val hash : t -> int
-(** Hash function for formulae *)
+  (** Abstract type representing hashconsed formulae *)
 
-val uid : t -> Uid.t
-(** Returns a unique ID for formulae *)
+  val hash : t -> int
+  (** Hash function for formulae *)
 
-val equal : t -> t -> bool
-(** Equality over formulae *)
+  val uid : t -> Uid.t
+  (** Returns a unique ID for formulae *)
 
-val expr : t -> t expr
-(** Equality over formulae *)
+  val equal : t -> t -> bool
+  (** Equality over formulae *)
 
-(*val st : t -> StateSet.t * StateSet.t
-(** states occuring left and right, positively or negatively *)
-*)
-
-val compare : t -> t -> int
-(** Comparison of formulae *)
+  val expr : t -> (t,P.t) expr
+  (** Equality over formulae *)
 
-val print : Format.formatter -> t -> unit
-(** Pretty printer *)
+  val compare : t -> t -> int
+  (** Comparison of formulae *)
 
-val is_true : t -> bool
-(** [is_true f] tests whether the formula is the atom True *)
+  val print : Format.formatter -> t -> unit
+  (** Pretty printer *)
 
-val is_false : t -> bool
-(** [is_false f] tests whether the formula is the atom False *)
+  val is_true : t -> bool
+  (** [is_true f] tests whether the formula is the atom True *)
 
-val true_ : t
-(** Atom True *)
+  val is_false : t -> bool
+  (** [is_false f] tests whether the formula is the atom False *)
 
-val false_ : t
-(** Atom False *)
-
-val atom_ : move -> bool -> StateSet.elt -> t
-(** [atom_ dir b q] creates a down_left or down_right atom for state
-    [q]. The atom is positive if [b == true].
-*)
+  val true_ : t
+  (** Atom True *)
 
-val not_ : t -> t
-val or_ : t -> t -> t
-val and_ : t -> t -> t
-(** Boolean connective *)
+  val false_ : t
+  (** Atom False *)
 
-val of_bool : bool -> t
-(** Convert an ocaml Boolean value to a formula *)
+  val atom_ : P.t -> t
+  (** [atom_ dir b q] creates a down_left or down_right atom for state
+      [q]. The atom is positive if [b == true].
+  *)
+    
+  val not_ : t -> t
+  val or_ : t -> t -> t
+  val and_ : t -> t -> t
+  (** Boolean connective *)
+    
+  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 *)
+end