-let rec eval ctx f =
- match f.Node.node.pos with
- True -> true
- | False -> false
- | Atom p -> P.eval ctx p
- | And(f1, f2) -> eval ctx f1 && eval ctx f2
- | Or(f1, f2) -> eval ctx f1 || eval ctx f2
+let fold f phi acc =
+ let rec loop phi acc =
+ match expr phi with
+ | And (phi1, phi2) | Or(phi1, phi2) ->
+ loop phi2 (loop phi1 (f phi acc))
+ | _ -> f phi acc
+ in
+ loop phi acc