+
+(* 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, snd 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 *)