+ let neg a =
+ let p, b, q = a.node in
+ make (p, not b, q)
+
+
+end
+
+module SFormula =
+struct
+ include Formula.Make(Atom)
+ open Tree.Common.NodeKind
+ let mk_atom a b c = atom_ (Atom.make (a,b,c))
+ let mk_kind k = mk_atom (Is k) true State.dummy
+ let has_first_child =
+ (mk_atom Has_first_child true State.dummy)
+
+ let has_next_sibling =
+ (mk_atom Has_next_sibling true State.dummy)
+
+ let is_first_child =
+ (mk_atom Is_first_child true State.dummy)
+
+ let is_next_sibling =
+ (mk_atom Is_next_sibling true State.dummy)
+
+ let is_attribute =
+ (mk_atom (Is Attribute) true State.dummy)
+
+ let is_element =
+ (mk_atom (Is Element) true State.dummy)
+
+ let is_processing_instruction =
+ (mk_atom (Is ProcessingInstruction) true State.dummy)
+
+ let is_comment =
+ (mk_atom (Is Comment) true State.dummy)
+
+ let first_child q =
+ and_
+ (mk_atom First_child true q)
+ has_first_child
+
+ let next_sibling q =
+ and_
+ (mk_atom Next_sibling true q)
+ has_next_sibling
+
+ let parent q =
+ and_
+ (mk_atom Parent true q)
+ is_first_child
+
+ let previous_sibling q =
+ and_
+ (mk_atom Previous_sibling true q)
+ is_next_sibling
+
+ let stay q =
+ (mk_atom Stay true q)
+
+ let get_states phi =
+ fold (fun phi acc ->
+ match expr phi with
+ | Formula.Atom a -> let _, _, q = Atom.node a in
+ if q != State.dummy then StateSet.add q acc else acc
+ | _ -> acc
+ ) phi StateSet.empty