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

diff --git a/src/formula.mli b/src/formula.mli
index 46cbe65..69bdb78 100644
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -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) -> t -> bool
+(** [eval_form (sf,sn) F] evaluates the formula [F] on [(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 print : Format.formatter -> t -> unit
 (** Pretty printer *)