X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fformula.mli;fp=src%2Fformula.mli;h=9ecf30a3d1066b5c40db6cbe24df261a127e8466;hb=0223b78baf156e7b8de86e334a4648fb2c3819e8;hp=69bdb78645a9f63df4bafbad7d581756f04daa34;hpb=09cd270a1d9d1405795aa3d220267bc3141dd0bd;p=tatoo.git

diff --git a/src/formula.mli b/src/formula.mli
index 69bdb78..9ecf30a 100644
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -15,7 +15,7 @@
 
 (** Implementation of hashconsed Boolean formulae *)
 
-type move = [ `Left |`Right ]
+type move = [ `Left |`Right | `Self ]
 (** Direction for automata predicates *)
 
 type 'hcons expr =
@@ -52,11 +52,11 @@ val compare : t -> t -> int
 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 *)