- | 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 -> is_left
- | Is_next_sibling -> is_right
- | Is k -> k == kind
- | Has_first_child -> has_left
- | Has_next_sibling -> has_right
- in
- if is_move p && (not b) then
- eprintf "Warning: Invalid negative atom %a" Atom.print a;
- b == pos
- | Formula.And(phi1, phi2) -> loop phi1 && loop phi2
- | Formula.Or (phi1, phi2) -> loop phi1 || loop phi2
+ | First_child ->
+ if b == StateSet.mem q fcs then SFormula.true_ else phi
+ | Next_sibling ->
+ if b == StateSet.mem q nss then SFormula.true_ else phi
+ | Parent | Previous_sibling ->
+ if b == StateSet.mem q ps then SFormula.true_ else phi
+ | Stay ->
+ if b == StateSet.mem q ss then SFormula.true_ else phi
+ | Is_first_child -> SFormula.of_bool (b == is_left)
+ | Is_next_sibling -> SFormula.of_bool (b == is_right)
+ | Is k -> SFormula.of_bool (b == (k == kind))
+ | Has_first_child -> SFormula.of_bool (b == has_left)
+ | Has_next_sibling -> SFormula.of_bool (b == has_right)
+ end
+ | Formula.And(phi1, phi2) -> SFormula.and_ (loop phi1) (loop phi2)
+ | Formula.Or (phi1, phi2) -> SFormula.or_ (loop phi1) (loop phi2)