(* *)
(***********************************************************************)
+(*
+ Time-stamp: <Last modified on 2013-02-05 15:58:13 CET by Kim Nguyen>
+*)
+
(** This module contains all the signatures of the project, to avoid
code duplication. Each toplevel module (HCONS, PTSET, ...)
corresponds to an existing module in the project. The AUX modules
(** Initializes the internal storage. Any previously hashconsed
element is discarded. *)
val init : unit -> unit
+
+ (** Create a dummy (non-hashconsed) node with a boggus identifer
+ and hash *)
+ val dummy : data -> t
end
val inj_negative : set -> t
end
end
+
+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