+type predicate =
+ Move of move * State.t (** In the [move] direction, the automaton must be in the given state *)
+ | Is_first_child (** True iff the node is the first child of its parent *)
+ | Is_next_sibling (** True iff the node is the next sibling of its parent *)
+ | Is of Tree.NodeKind.t (** True iff the node is of the given kind *)
+ | Has_first_child (** True iff the node has a first child *)
+ | Has_next_sibling (** True iff the node has a next sibling *)
+(** Type of the predicates that can occur in the Boolean formulae that are in the transitions of the automaton *)
+
+module Atom : sig
+ include Hcons.S with type data = predicate
+ include Common_sig.Printable with type t:= t
+end
+(** Module representing atoms of Boolean formulae, which are simply hashconsed [predicate]s *)