X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=53f48c3666418f0ef703097700736334e36e66b9;hp=fb9f81d751099ed5ed496464ba9d6c91ced8f553;hb=aae9118fbf9d29df5d7fc36efe2afd6eadab11d1;hpb=a089738aa464521c0ae79944eb00fc147cc37ac9 diff --git a/src/run.ml b/src/run.ml index fb9f81d..53f48c3 100644 --- a/src/run.ml +++ b/src/run.ml @@ -114,6 +114,7 @@ END label * self-set * fc-set * ns-set * parent-set * node-shape -> self-set *) node_summaries: (int, int16_unsigned_elt, c_layout) Array1.t; + } let dummy_form = Ata.Formula.stay State.dummy @@ -152,8 +153,8 @@ END match m with `First_child -> fcs | `Next_sibling -> nss - | `Parent | `Previous_sibling -> ps - | `Stay -> ss + | `Parent | `Previous_sibling -> ps + | `Stay -> ss ) | Is_first_child -> b == is_left summary | Is_next_sibling -> b == is_right summary @@ -203,7 +204,7 @@ END new_sat -module Make (T : Tree.S) = +module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = struct let make auto tree = @@ -222,7 +223,7 @@ module Make (T : Tree.S) = } - let top_down run = + let top_down run update_res = let i = run.pass in let tree = run.tree in let auto = run.auto in @@ -233,9 +234,11 @@ module Make (T : Tree.S) = else states_by_rank.(i+1) in + let last_run = i >= Array.length states_by_rank - 2 in let rec loop_td_and_bu node parent parent_sat = if node == T.nil then StateSet.empty else begin + let tag = T.tag tree node in let node_id = T.preorder tree node in let fc = T.first_child tree node in let ns = T.next_sibling tree node in @@ -245,8 +248,8 @@ module Make (T : Tree.S) = if s != 0 then s else let s = NodeSummary.make - (node == T.first_child tree parent) (*is_left *) - (node == T.next_sibling tree parent)(*is_right *) + (node == (T.first_child tree parent)) (*is_left *) + (node == (T.next_sibling tree parent))(*is_right *) (fc != T.nil) (* has_left *) (ns != T.nil) (* has_right *) (T.kind tree node) (* kind *) @@ -256,7 +259,6 @@ module Make (T : Tree.S) = let status0 = unsafe_get run.sat node_id in (* get the node_statuses for the first child, next sibling and parent *) (* evaluate the transitions with all this statuses *) - let tag = T.tag tree node in let status1 = eval_trans auto run.fetch_trans_cache run.td_cache tag @@ -266,14 +268,26 @@ module Make (T : Tree.S) = parent_sat status0 td_todo in - (* update the cache if the status of the node changed - unsafe_set run.sat node_id status1 status0;*) - let fcs1 = loop_td_and_bu fc node status1 in + if status1 == StateSet.empty && status0 != StateSet.empty + then StateSet.empty else + (* update the cache if the status of the node changed + unsafe_set run.sat node_id status1 status0;*) if bu_todo == StateSet.empty then begin unsafe_set run.sat node_id status1 status0; (* write the td_states *) + update_res false status1 node; + let _ = loop_td_and_bu fc node status1 in loop_td_and_bu ns node status1 (* tail call *) end else - let nss1 = loop_td_and_bu ns node status1 in + let fcs1, nss1 = + if last_run then + let nss1 = loop_td_and_bu ns node status1 in + let fcs1 = loop_td_and_bu fc node status1 in + fcs1, nss1 + else + let fcs1 = loop_td_and_bu fc node status1 in + let nss1 = loop_td_and_bu ns node status1 in + fcs1, nss1 + in let status2 = eval_trans auto run.fetch_trans_cache run.bu_cache tag summary fcs1 @@ -282,6 +296,7 @@ module Make (T : Tree.S) = status1 bu_todo in unsafe_set run.sat node_id status2 status0; + if last_run && status2 != StateSet.empty then update_res true status2 node; status2 end in @@ -289,77 +304,59 @@ module Make (T : Tree.S) = run.pass <- run.pass + 2 - let get_results run = - let cache = IFHTML((List.hd run.sat), run.sat) in - let auto = run.auto in - let tree = run.tree in - let sel_states = Ata.get_selecting_states auto in - let rec loop node acc = - if node == T.nil then acc - else - let acc0 = loop (T.next_sibling tree node) acc in - let acc1 = loop (T.first_child tree node) acc0 in - if StateSet.intersect cache.(T.preorder tree node) - sel_states then node::acc1 - else acc1 - in - loop (T.root tree) [] - - - let get_full_results run = - let cache = IFHTML((List.hd run.sat), run.sat) in - let auto = run.auto in - let tree = run.tree in - let res_mapper = Hashtbl.create MED_H_SIZE in - let () = - StateSet.iter - (fun q -> Hashtbl.add res_mapper q []) - (Ata.get_selecting_states auto) - in - let dummy = [ T.nil ] in - let res_mapper = Cache.N1.create dummy in - let () = - StateSet.iter - (fun q -> Cache.N1.add res_mapper (q :> int) []) - (Ata.get_selecting_states auto) - in - let rec loop node = - if node != T.nil then - let () = loop (T.next_sibling tree node) in - let () = loop (T.first_child tree node) in - StateSet.iter - (fun q -> - let res = Cache.N1.find res_mapper (q :> int) in - if res != dummy then - Cache.N1.add res_mapper (q :> int) (node::res) - ) - cache.(T.preorder tree node) - in - loop (T.root tree); - (StateSet.fold_right - (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc) - (Ata.get_selecting_states auto) []) - + let mk_update_result auto = + let sel_states = Ata.get_selecting_states auto in + let res = L.create () in + (fun prepend sat node -> + if StateSet.intersect sel_states sat then begin + if prepend then L.push_front node res else + L.push_back node res + end), + (fun () -> res) + + + let mk_update_full_result auto = + let dummy = L.create () in + let res_mapper = Cache.N1.create dummy in + let () = + StateSet.iter + (fun q -> Cache.N1.add res_mapper (q :> int) (L.create())) + (Ata.get_selecting_states auto) + in + (fun prepend sat node -> + StateSet.iter + (fun q -> + let res = Cache.N1.find res_mapper (q :> int) in + if res != dummy then begin + if prepend then L.push_front node res + else L.push_back node res + end + ) sat), + (fun () -> + StateSet.fold_right + (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc) + (Ata.get_selecting_states auto) []) let prepare_run run list = let tree = run.tree in let auto = run.auto in let sat = IFHTML((List.hd run.sat), run.sat) in let sat0 = Ata.get_starting_states auto in - List.iter (fun node -> + L.iter (fun node -> let node_id = T.preorder tree node in sat.(node_id) <- sat0) list let tree_size = ref 0 let pass = ref 0 - let compute_run auto tree nodes = + + let compute_run auto tree nodes update_res = pass := 0; tree_size := T.size tree; let run = make auto tree in prepare_run run nodes; let rank = Ata.get_max_rank auto in while run.pass <= rank do - top_down run; + top_down run update_res; IFHTML((run.sat <- (Array.copy (List.hd run.sat)) :: run.sat), ()); run.td_cache <- Cache.N6.create dummy_set; run.bu_cache <- Cache.N6.create dummy_set; @@ -369,13 +366,17 @@ module Make (T : Tree.S) = IFHTML(Html_trace.gen_trace auto run.sat (module T : Tree.S with type t = T.t) tree ,()); run + + let full_eval auto tree nodes = - let r = compute_run auto tree nodes in - get_full_results r + let update_full,get_full = mk_update_full_result auto in + let _ = compute_run auto tree nodes update_full in + get_full () let eval auto tree nodes = - let r = compute_run auto tree nodes in - get_results r + let update_res,get_res = mk_update_result auto in + let _ = compute_run auto tree nodes update_res in + get_res () let stats () = { tree_size = !tree_size;