X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fformula.mli;h=14e0f80b69accc48a17c59b62adbde4505736bfc;hb=refs%2Fheads%2Flucca-optim;hp=9ecf30a3d1066b5c40db6cbe24df261a127e8466;hpb=0223b78baf156e7b8de86e334a4648fb2c3819e8;p=tatoo.git

diff --git a/src/formula.mli b/src/formula.mli
index 9ecf30a..14e0f80 100644
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -43,8 +43,8 @@ val equal : t -> t -> bool
 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 *)
@@ -52,10 +52,24 @@ val compare : t -> t -> int
 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