(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-02-05 16:11:43 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-04-04 18:41:24 CEST by Kim Nguyen>
*)
-module type PREDICATE =
+module type ATOM =
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
+ include Common_sig.Printable with type t := t
end
-type ('formula,'pred) expr =
+type ('formula,'atom) expr =
| False
| True
| Or of 'formula * 'formula
| And of 'formula * 'formula
- | Atom of 'pred
+ | Atom of 'atom
(** View of the internal representation of a formula,
used for pattern matching *)
-module Make(P : PREDICATE) :
+module Make(P : ATOM) :
sig
type t
(** Equality over formulae *)
val expr : t -> (t,P.t) expr
- (** Equality over formulae *)
+ (** Return a view of the formulae *)
val compare : t -> t -> int
(** Comparison of formulae *)
(** [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 *)
+
+ val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
+ (** [fold f phi acc] folds [f] over the formula structure *)
+
end