(** Implementation of hashconsed Boolean formulae *)
-type move = [ `Left |`Right ]
+type move = [ `Left |`Right | `Self ]
(** Direction for automata predicates *)
type 'hcons expr =
val size : t -> int
(** Syntactic size of the formula *)
-val eval_form : (StateSet.t * StateSet.t) -> t -> bool
-(** [eval_form (sf,sn) F] evaluates the formula [F] on [(sf,sn)] *)
+val eval_form : (StateSet.t * StateSet.t * StateSet.t) -> t -> bool
+(** [eval_form (s,sf,sn) F] evaluates the formula [F] on [(s,sf,sn)] *)
-val infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> t -> bool
-(** [eval_form S1 S2 F] infers S1; S2 |- F *)
+val infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> t -> bool
+(** [eval_form S Sf Sn F] infers S; (S1,S2) |- F *)
val print : Format.formatter -> t -> unit
(** Pretty printer *)