--- /dev/null
+(***********************************************************************)
+(* *)
+(* TAToo *)
+(* *)
+(* Kim Nguyen, LRI UMR8623 *)
+(* Université Paris-Sud & CNRS *)
+(* *)
+(* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(* Recherche Scientifique. All rights reserved. This file is *)
+(* distributed under the terms of the GNU Lesser General Public *)
+(* License, with the special exception on linking described in file *)
+(* ../LICENSE. *)
+(* *)
+(***********************************************************************)
+
+module type ATOM =
+sig
+ include Hcons.S
+ include Common_sig.Printable with type t := t
+end
+
+type ('formula,'atom) expr =
+ | False
+ | True
+ | Or of 'formula * 'formula
+ | And of 'formula * 'formula
+ | Atom of 'atom * bool
+
+(** View of the internal representation of a formula,
+ used for pattern matching *)
+
+module Make(A : ATOM) :
+sig
+ type t
+
+ (** Abstract type representing hashconsed formulae *)
+
+ val hash : t -> int
+ (** Hash function for formulae *)
+
+ val uid : t -> Uid.t
+ (** Returns a unique ID for formulae *)
+
+ val equal : t -> t -> bool
+ (** Equality over formulae *)
+
+ val expr : t -> (t,A.t) expr
+ (** Return a view of the formulae *)
+
+ val compare : t -> t -> int
+ (** Comparison of formulae *)
+
+ 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_false : t -> bool
+ (** [is_false f] tests whether the formula is the atom False *)
+
+ val true_ : t
+ (** Atom True *)
+
+ val false_ : t
+ (** Atom False *)
+
+ val atom_ : A.t -> t
+ (** [atom_ a] creates a new formula consisting of the atome a.
+ *)
+
+ 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 fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
+ (** [fold f phi acc] folds [f] over the formula structure *)
+
+end