X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fformula.mli;h=bea2ff5f8ea434a0ebe633072d7cfa66dc8b66ba;hb=1efafef0e88ad043612ed631eaee31b38b79dfc6;hp=46cbe6508c5219513329ebc404be212edaa77d98;hpb=cba2938d929fd5119b1491686ddc224d5af618c6;p=tatoo.git

diff --git a/src/formula.mli b/src/formula.mli
index 46cbe65..bea2ff5 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 =
@@ -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,6 +52,12 @@ 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
+(** [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
+(** [eval_form S Sf Sn F] infers S; (S1,S2) |- F *)
+
 val print : Format.formatter -> t -> unit
 (** Pretty printer *)