X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fformula.ml;h=c75748fb6ef9ebe56b13aa8438930d872ea27561;hb=83c90cb5eeebfffa05d0383430eb80e7905b46a0;hp=f7eae8516083c264f88bad92af477ede121173ba;hpb=cba2938d929fd5119b1491686ddc224d5af618c6;p=tatoo.git

diff --git a/src/formula.ml b/src/formula.ml
index f7eae85..c75748f 100644
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -71,6 +71,31 @@ let prio f =
     | Atom _ -> 8
     | And _ -> 6
     | Or _ -> 1
+      
+(* Begin Lucca Hirschi *)
+let rec eval_form ss f = match expr f with
+  | False -> false
+  | True -> true
+  | And(f1,f2) -> eval_form ss f1 && eval_form ss f2
+  | Or(f1,f2) -> eval_form ss f1 || eval_form ss f2
+  | Atom(dir, b, s) -> 
+    let set = match dir with |`Left -> fst ss | `Right -> snd ss in
+    if b then StateSet.mem s set
+    else not (StateSet.mem s set)
+
+let rec infer_form ssq ssr f = match expr f with
+  | False -> false
+  | True -> true
+  | And(f1,f2) -> infer_form ssq ssr f1 && infer_form ssq ssr f2
+  | Or(f1,f2) -> infer_form ssq ssr f1 || infer_form ssq ssr f2
+  | Atom(dir, b, s) -> 
+    let setq, setr = match dir with
+      |`Left -> fst ssq, fst ssr
+      | `Right -> snd ssq, fst ssr in
+    (* WG: WE SUPPOSE THAT Q^r and Q^q are disjoint ! *)
+    let mem =  StateSet.mem s setq || StateSet.mem s setr in
+    if b then mem else not mem
+(* End *)
 
 let rec print ?(parent=false) ppf f =
   if parent then fprintf ppf "(";