Full implem BU Oracle + eval_form in Formula (impossible in Asta) + transitions_lab...

[tatoo.git] / src / formula.ml

diff --git a/src/formula.ml b/src/formula.ml
index f7eae85..03618c2 100644 (file)
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -71,6 +71,17 @@ 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
+    StateSet.mem s set
+(* End *)
 
 let rec print ?(parent=false) ppf f =
   if parent then fprintf ppf "(";