(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-01-30 19:08:52 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-04-04 18:41:24 CEST by Kim Nguyen>
*)
-(** Implementation of hashconsed Boolean formulae *)
+module type ATOM =
+sig
+ type t
+ val neg : t -> t
+ include Hcons.Abstract with type t := t
+ include Common_sig.Printable with type t := t
+end
-type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ]
-
-(** Direction for automata predicates *)
-
-type 'formula expr =
+type ('formula,'atom) expr =
| False
| True
| Or of 'formula * 'formula
| And of 'formula * 'formula
- | Move of move * bool * State.t
+ | Atom of 'atom
(** View of the internal representation of a formula,
used for pattern matching *)
-type t
+module Make(P : ATOM) :
+sig
+ type t
-(** Abstract type representing hashconsed formulae *)
+ (** Abstract type representing hashconsed formulae *)
-val hash : t -> int
-(** Hash function for formulae *)
+ val hash : t -> int
+ (** Hash function for formulae *)
-val uid : t -> Uid.t
-(** Returns a unique ID for formulae *)
+ val uid : t -> Uid.t
+ (** Returns a unique ID for formulae *)
-val equal : t -> t -> bool
-(** Equality over formulae *)
+ val equal : t -> t -> bool
+ (** Equality over formulae *)
-val expr : t -> t expr
-(** Equality over formulae *)
+ val expr : t -> (t,P.t) expr
+ (** Return a view of the 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 compare : t -> t -> int
-(** Comparison of formulae *)
+ val print : Format.formatter -> t -> unit
+ (** Pretty printer *)
-val print : Format.formatter -> t -> unit
-(** Pretty printer *)
+ val is_true : t -> bool
+ (** [is_true f] tests whether the formula is the atom True *)
-val is_true : t -> bool
-(** [is_true f] tests whether the formula is the atom True *)
+ val is_false : t -> bool
+ (** [is_false f] tests whether the formula is the atom False *)
-val is_false : t -> bool
-(** [is_false f] tests whether the formula is the atom False *)
+ val true_ : t
+ (** Atom True *)
-val true_ : t
-(** Atom True *)
+ val false_ : t
+ (** Atom False *)
-val false_ : t
-(** Atom False *)
+ 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 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 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 not_ : t -> t
-val or_ : t -> t -> t
-val and_ : t -> t -> t
-(** Boolean connective *)
+ val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
+ (** [fold f phi acc] folds [f] over the formula structure *)
-val of_bool : bool -> t
-(** Convert an ocaml Boolean value to a formula *)
+end