+ let eval_form phi tree node fcs nss ps ss =
+ let rec loop phi =
+ match Ata.SFormula.expr phi with
+ Formula.True -> true
+ | Formula.False -> false
+ | Formula.Atom a ->
+ let p, b, q = Ata.Atom.node a in
+ let pos =
+ let open Ata in
+ match p with
+ | First_child -> StateSet.mem q fcs
+ | Next_sibling -> StateSet.mem q nss
+ | Parent | Previous_sibling -> StateSet.mem q ps
+ | Stay -> StateSet.mem q ss
+ | Is_first_child ->
+ node == (T.first_child tree (T.parent tree node))
+ | Is_next_sibling ->
+ node == (T.next_sibling tree (T.parent tree node))
+ | Is k -> k == (T.kind tree node)
+ | Has_first_child ->
+ T.nil != T.first_child tree node
+ | Has_next_sibling ->
+ T.nil != T.next_sibling tree node
+ in
+ if Ata.is_move p && (not b) then
+ eprintf "Warning: Invalid negative atom %a" Ata.Atom.print a;
+ b == pos
+ | Formula.And(phi1, phi2) -> loop phi1 && loop phi2
+ | Formula.Or (phi1, phi2) -> loop phi1 || loop phi2
+ in
+ loop phi