+ module NodeInfo = Hcons.Make(Info)
+
+ let eval_form phi node_info fcs nss ps ss =
+ let open NodeInfo in
+ let open Info in
+ let rec loop phi =
+ begin 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_info.node.is_left
+ | Is_next_sibling -> node_info.node.is_right
+ | Is k -> k == node_info.node.kind
+ | Has_first_child -> node_info.node.has_left
+ | Has_next_sibling -> node_info.node.has_right
+ 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
+ end
+ in
+ loop phi
+
+ let eval_trans cache ltrs node_info fcs nss ps ss =
+ let j = (node_info.NodeInfo.id :> int)
+ and k = (fcs.StateSet.id :> int)
+ and l = (nss.StateSet.id :> int)
+ and m = (ps.StateSet.id :> int) in
+ let rec loop ltrs ss =
+ let i = (ltrs.Ata.TransList.id :> int)
+ and n = (ss.StateSet.id :> int) in
+ let (new_ltrs, new_ss) as res =
+ let res = Cache.N6.find cache i j k l m n in
+ if res == Cache.N6.dummy cache then
+ let res =
+ Ata.TransList.fold (fun trs (acct, accs) ->
+ let q, _, phi = Ata.Transition.node trs in
+ if StateSet.mem q accs then (acct, accs) else
+ if eval_form phi node_info fcs nss ps accs then
+ (acct, StateSet.add q accs)
+ else
+ (Ata.TransList.cons trs acct, accs)
+ ) ltrs (Ata.TransList.nil, ss)
+ in
+ Cache.N6.add cache i j k l m n res; res