+
+module FORMULA =
+struct
+ module type ATOM =
+ sig
+ type t
+ type ctx
+ val eval : ctx -> t -> bool
+ val neg : t -> t
+ include HCONS.S with type t := t
+ include AUX.Printable with type t := t
+ end
+ module type S =
+ sig
+ module Atom : ATOM
+ include HCONS.S
+ include AUX.Printable with type t := t
+ val of_bool : bool -> t
+ val true_ : t
+ val false_ : t
+ val or_ : t -> t -> t
+ val and_ : t -> t -> t
+ val not_ : t -> t
+ val diff_ : t -> t -> t
+ val eval : Atom.ctx -> t -> bool
+ end
+
+end