From c3002932ccf2287a2a3d399dfa140cc216bc2b69 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Sat, 11 Jan 2014 14:38:27 +0100 Subject: [PATCH] Perform selection of nodes during the last run instead of performing an extra traversal. --- src/run.ml | 131 ++++++++++++++++++++++++----------------------------- 1 file changed, 58 insertions(+), 73 deletions(-) diff --git a/src/run.ml b/src/run.ml index f125346..f9222f1 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 @@ -222,7 +223,7 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = } - 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,6 +234,7 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = 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 @@ -269,12 +271,22 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = (* 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 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 @@ -283,6 +295,7 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = status1 bu_todo in unsafe_set run.sat node_id status2 status0; + if last_run then update_res true status2 node; status2 end in @@ -290,59 +303,38 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = 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 res = L.create () in - let rec loop node = - if node != T.nil then begin - if StateSet.intersect sel_states cache.(T.preorder tree node) then - L.push_back node res; - loop (T.first_child tree node); - loop (T.next_sibling tree node) - end - in - loop (T.root tree); - res - - - 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 = 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 - let rec loop node = - if node != T.nil then begin - StateSet.iter - (fun q -> - let res = Cache.N1.find res_mapper (q :> int) in - if res != dummy then L.add node res - ) - cache.(T.preorder tree node); - loop (T.first_child tree node); - loop (T.next_sibling tree node) - end - 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 @@ -356,24 +348,14 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = let tree_size = ref 0 let pass = ref 0 -let time f arg msg = - let t1 = Unix.gettimeofday () in - let r = f arg in - let t2 = Unix.gettimeofday () in - let time = (t2 -. t1) *. 1000. in - Printf.eprintf "%s: %fms%!" msg time; - r - - - - 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 - time top_down run ("Timing run number " ^ string_of_int run.pass ^ "/" ^ string_of_int (Ata.get_max_rank auto + 1)); + 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; @@ -383,14 +365,17 @@ let time f arg msg = 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 - let nl = get_results r in - nl + 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; -- 2.17.1