module Make (T : Tree.S) =
struct
- let eval_form phi tree node fcs nss pars selfs =
+ let int (x : bool) : int = Obj.magic x
+ let kint (x : Tree.NodeKind.t) : int = Obj.magic x
+ let summary tree node parent fc ns =
+ (int (ns != T.nil)) lor
+ ((int (fc != T.nil)) lsl 1) lor
+ ((int (node == T.next_sibling tree parent)) lsl 2) lor
+ ((int (node == T.first_child tree parent)) lsl 3) lor
+ ((kint (T.kind tree node)) lsl 4)
+
+ let has_next_sibling summary : bool = Obj.magic (summary land 1)
+ let has_first_child summary : bool = Obj.magic ((summary lsr 1) land 1)
+ let is_next_sibling summary : bool = Obj.magic ((summary lsr 2) land 1)
+ let is_first_child summary : bool = Obj.magic ((summary lsr 3) land 1)
+ let kind summary : Tree.NodeKind.t = Obj.magic (summary lsr 4)
+
+
+ let eval_form phi node_summary f_set n_set p_set s_set =
let rec loop phi =
let open Boolean in
match Ata.Formula.expr phi with
| And (phi1, phi2) -> loop phi1 && loop phi2
| Atom (a, b) -> b == Ata.(
match Atom.node a with
- Is_first_child -> let par = T.parent tree node in
- (T.first_child tree par) == node
- | Is_next_sibling -> let par = T.parent tree node in
- (T.next_sibling tree par) == 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
+ Is_first_child -> is_first_child node_summary
+ | Is_next_sibling -> is_next_sibling node_summary
+ | Is k -> k == kind node_summary
+ | Has_first_child -> has_first_child node_summary
+ | Has_next_sibling -> has_next_sibling node_summary
| Move (m, q) ->
let set =
match m with
- `First_child -> fcs
- | `Next_sibling -> nss
+ `First_child -> f_set
+ | `Next_sibling -> n_set
| `Parent
- | `Previous_sibling -> pars
- | `Stay -> selfs
+ | `Previous_sibling -> p_set
+ | `Stay -> s_set
in
StateSet.mem q set
)
loop phi
- let eval_trans_aux trans tree node fcs nss pars selfs =
+ let eval_trans_aux trans_list node_summary f_set n_set p_set s_set =
let open Ata in
TransList.fold (fun trs acc ->
let q, _ , phi = Transition.node trs in
- let res = eval_form phi tree node fcs nss pars selfs in
- if false then begin
- Format.eprintf "Formula %a evaluates to %b with context: (fcs=%a, nss=%a, pars=%a, olds=%a) @\n@."
- Formula.print phi res
- StateSet.print fcs
- StateSet.print nss
- StateSet.print pars
- StateSet.print selfs
- end;
- if res then
+ if eval_form phi node_summary f_set n_set p_set s_set then
StateSet.add q acc
else
- acc) trans selfs
+ acc) trans_list s_set
- let eval_trans trans tree node fcs nss pars sstates =
- let rec loop olds =
+ let eval_trans trans_list node_summary f_set n_set p_set s_set =
+ let rec loop old_s =
- let news = eval_trans_aux trans tree node fcs nss pars olds in
- if false then begin
- Format.eprintf "Saturating formula: olds=%a, news=%a@\n@."
- StateSet.print olds
- StateSet.print news
- end;
- if news == olds then olds else
- loop news
+ let new_s =
+ eval_trans_aux trans_list node_summary f_set n_set p_set old_s
+ in
+ if new_s == old_s then old_s else loop new_s
in
- let r = loop sstates in
- if false then begin
- Format.eprintf "Evaluating transitions (fcs=%a, nss=%a, pars=%a, olds=%a):@\n\t%a@."
- StateSet.print fcs
- StateSet.print nss
- StateSet.print pars
- StateSet.print sstates
- (Ata.TransList.print ~sep:"\n\t") trans;
- Format.eprintf "Got %a@\n@." StateSet.print r;
- end;
- r
+ loop s_set
+
+ let dummy_set = StateSet.singleton State.dummy
+ let count = ref 0
+ let total = ref 0
+ let () = at_exit (fun () -> Format.eprintf "Cache miss: %i/%i\n%!" !count !total)
+
+ let eval_trans auto cache set tag node_summary f_set n_set p_set s_set =
+ incr total;
+ let i = (tag.QName.id :> int) in
+ let j = node_summary in
+ let k = (f_set.StateSet.id :> int) in
+ let l = (n_set.StateSet.id :> int) in
+ let m = (p_set.StateSet.id :> int) in
+ let n = (s_set.StateSet.id :> int) in
+ let res = Cache.N6.find cache i j k l m n in
+ if res == dummy_set then begin
+ incr count;
+ let trans_list = Ata.get_trans auto tag set in
+ let res = eval_trans trans_list node_summary f_set n_set p_set s_set in
+ Cache.N6.add cache i j k l m n res;
+ res
+ end
+ else res
let auto_run auto tree prev_nodes td_states bu_states exit_states _i =
StateSet.print td_states
StateSet.print bu_states
StateSet.print exit_states;
- let rec loop res node parset =
+ let td_cache = Cache.N6.create dummy_set in
+ let bu_cache = Cache.N6.create dummy_set in
+ let rec loop res node parent parent_set =
if node == T.nil then StateSet.empty else begin
let set,lset,rset =
if Sequence.is_empty prev_nodes then
StateSet.(empty,empty,empty)
in
let tag = T.tag tree node in
- let td_trans = Ata.get_trans auto tag td_states in
- let status1 = eval_trans td_trans tree node lset rset parset set in
- let fcs = loop res (T.first_child tree node) status1 in
+ let first_child = T.first_child tree node in
+ let next_sibling = T.next_sibling tree node in
+ let node_summary = summary tree node parent first_child next_sibling in
+
+ let status1 =
+ eval_trans auto td_cache td_states tag node_summary lset rset parent_set set
+ in
+ let fcs = loop res first_child node status1 in
let rres = Sequence.create () in
- let nss = loop rres (T.next_sibling tree node) status1 in
- let bu_trans = Ata.get_trans auto tag bu_states in
- let status2 = eval_trans bu_trans tree node fcs nss parset status1 in
+ let nss = loop rres next_sibling node status1 in
+
+ let status2 =
+ eval_trans auto bu_cache bu_states tag node_summary fcs nss parent_set status1
+ in
let mstates = StateSet.inter status2 exit_states in
if false then begin
Format.eprintf "On node %i (tag : %a) status0 = %a, status1 = %a, fcs = %a, nss = %a, par = %a, status2 = %a, mstates = %a@\n@."
StateSet.print status1
StateSet.print fcs
StateSet.print nss
- StateSet.print parset
+ StateSet.print parent_set
StateSet.print status2
StateSet.print mstates;
end;
end
in
let res = Sequence.create () in
- ignore (loop res (T.root tree) StateSet.empty);
+ ignore (loop res (T.root tree) T.nil StateSet.empty);
if false then Format.eprintf "Finished pass: %i @\n-----------------------@\n@." _i;
res