val expr : t -> t expr
(** Equality over formulae *)
-val st : t -> StateSet.t * StateSet.t
-(** states occuring left and right, positively or negatively *)
+val st : t -> StateSet.t * StateSet.t * StateSet.t
+(** States occuring self, left and right, positively or negatively *)
val compare : t -> t -> int
(** Comparison of formulae *)
val size : t -> int
(** Syntactic size of the formula *)
-val eval_form : (StateSet.t * StateSet.t * StateSet.t) -> t -> bool
+
+module HcEval : sig
+ include Sigs.HashedType
+end
+module HcInfer : sig
+ include Sigs.HashedType
+end
+module HashEval : Hashtbl.S
+module HashInfer : Hashtbl.S
+type hcEval = bool HashEval.t
+type hcInfer = bool HashInfer.t
+(** Optimization: hconsigned eval and infer *)
+
+val eval_form : (StateSet.t * StateSet.t * StateSet.t) -> t -> hcEval -> 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) -> (StateSet.t * StateSet.t) -> t -> bool
+val infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) ->
+ (StateSet.t * StateSet.t) -> t -> hcInfer -> bool
(** [eval_form S Sf Sn F] infers S; (S1,S2) |- F *)
val print : Format.formatter -> t -> unit