From: Kim Nguyễn Date: Tue, 3 Dec 2013 22:57:12 +0000 (+0100) Subject: Speed-up the run function by keeping only the set of node to be satified for each... X-Git-Tag: v0.1~16 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=f9b9f1ce524acda75c7f3583cd3751901ecd17a5 Speed-up the run function by keeping only the set of node to be satified for each node. --- diff --git a/src/run.ml b/src/run.ml index 0e4e0b3..1824aeb 100644 --- a/src/run.ml +++ b/src/run.ml @@ -48,95 +48,58 @@ module Make (T : Tree.S) = type t = int let dummy = -1 (* - 333333333333333210 - 3333 -> kind - 2 -> has_right - 1 -> has_left - 0 -> is_left/is_right + ...44443210 + ...4444 -> kind + 3 -> has_right + 2 -> has_left + 1 -> is_right + 0 -> is_left *) let is_left (s : t) : bool = - s land 1 == 1 + s land 1 != 0 let is_right (s : t) : bool = - s land 1 == 0 + s land 0b10 != 0 let has_left (s : t) : bool = - (s lsr 1) land 1 == 1 + s land 0b100 != 0 let has_right (s : t) : bool = - (s lsr 2) land 1 == 1 + s land 0b1000 != 0 let kind (s : t) : Tree.NodeKind.t = - Obj.magic (s lsr 3) + Obj.magic (s lsr 4) - let make is_left has_left has_right kind = + let make is_left is_right has_left has_right kind = (int_of_bool is_left) lor - ((int_of_bool has_left) lsl 1) lor - ((int_of_bool has_right) lsl 2) lor - ((Obj.magic kind) lsl 3) + ((int_of_bool is_right) lsl 1) lor + ((int_of_bool has_left) lsl 2) lor + ((int_of_bool has_right) lsl 3) lor + ((Obj.magic kind) lsl 4) end - type node_status = { - rank : int; - sat : StateSet.t; (* States that are satisfied at the current node *) - todo : StateSet.t; (* States that remain to be proven *) - (* For every node_status and automaton a, - a.states - (sat U todo) = unsat *) - summary : NodeSummary.t; (* Summary of the shape of the node *) - } -(* Describe what is kept at each node for a run *) - - module NodeStatus = - struct - include Hcons.Make(struct - type t = node_status - let equal c d = - c == d || - c.rank == d.rank && - c.sat == d.sat && - c.todo == d.todo && - c.summary == d.summary - - let hash c = - HASHINT4(c.rank, - (c.sat.StateSet.id :> int), - (c.todo.StateSet.id :> int), - c.summary) - end - ) - let print ppf s = - fprintf ppf - "{ rank: %i; sat: %a; todo: %a; summary: _ }" - s.node.rank - StateSet.print s.node.sat - StateSet.print s.node.todo - end - - let dummy_status = - NodeStatus.make { - rank = -1; - sat = StateSet.empty; - todo = StateSet.empty; - summary = NodeSummary.dummy; - } - - + let dummy_set = StateSet.singleton State.dummy + open Bigarray type run = { tree : T.t ; (* The argument of the run *) auto : Ata.t; (* The automaton to be run *) - status : NodeStatus.t array; - (* A mapping from node preorders to NodeStatus *) + sat: StateSet.t array; + (* A mapping from node preorders to states satisfied at that node *) mutable pass : int; + (* Number of run we have performed *) mutable fetch_trans_cache : Ata.Formula.t Cache.N2.t; (* A cache from states * label to list of transitions *) - mutable td_cache : NodeStatus.t Cache.N5.t; - mutable bu_cache : NodeStatus.t Cache.N5.t; + mutable td_cache : StateSet.t Cache.N6.t; + mutable bu_cache : StateSet.t Cache.N6.t; + (* Two 6-way caches used during the top-down and bottom-up phase + 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 let make auto tree = @@ -144,45 +107,15 @@ module Make (T : Tree.S) = { tree = tree; auto = auto; - status = Array.create len dummy_status; + sat = Array.create len StateSet.empty; pass = 0; fetch_trans_cache = Cache.N2.create dummy_form; - td_cache = Cache.N5.create dummy_status; - bu_cache = Cache.N5.create dummy_status; + td_cache = Cache.N6.create dummy_set; + bu_cache = Cache.N6.create dummy_set; + node_summaries = let ba = Array1.create int16_unsigned c_layout len in + Array1.fill ba 0; ba } - let get_status a i = - if i < 0 then dummy_status else Array.get a i - - let unsafe_get_status a i = - if i < 0 then dummy_status else Array.unsafe_get a i - -IFDEF HTMLTRACE - THEN -DEFINE IFTRACE(e) = (e) - ELSE -DEFINE IFTRACE(e) = () -END - - let html tree node i config msg = - let config = config.NodeStatus.node in - Html.trace ~msg:msg - (T.preorder tree node) i - config.todo - config.sat - - - - let debug msg tree node i config = - let config = config.NodeStatus.node in - eprintf - "DEBUG:%s node: %i\nsat: %a\ntodo: %a\nround: %i\n" - msg - (T.preorder tree node) - StateSet.print config.sat - StateSet.print config.todo - i - let get_form fetch_trans_cache auto tag q = let phi = incr fetch_trans_cache_access; @@ -201,276 +134,137 @@ END phi end - type trivalent = False | True | Unknown - let of_bool = function false -> False | true -> True - let or_ t1 t2 = - match t1 with - False -> t2 - | True -> True - | Unknown -> if t2 == True then True else Unknown - - let and_ t1 t2 = - match t1 with - False -> False - | True -> t2 - | Unknown -> if t2 == False then False else Unknown - - (* Define as macros to get lazyness *) -DEFINE OR_(t1,t2) = - match t1 with - False -> (t2) - | True -> True - | Unknown -> if (t2) == True then True else Unknown - -DEFINE AND_(t1,t2) = - match t1 with - False -> False - | True -> (t2) - | Unknown -> if (t2) == False then False else Unknown - let eval_form phi fcs nss ps ss summary = let open Ata in let rec loop phi = begin match Formula.expr phi with - | Boolean.False -> False - | Boolean.True -> True + | Boolean.False -> false + | Boolean.True -> true | Boolean.Atom (a, b) -> begin let open NodeSummary in match a.Atom.node with | Move (m, q) -> - let down, ({ NodeStatus.node = n_sum; _ } as sum) = + b && StateSet.mem q ( match m with - `First_child -> true, fcs - | `Next_sibling -> true, nss - | `Parent | `Previous_sibling -> false, ps - | `Stay -> false, ss - in - if sum == dummy_status - (*|| (down && n_sum.rank < ss.NodeStatus.node.rank) *) - || StateSet.mem q n_sum.todo then - Unknown - else - of_bool (b == StateSet.mem q n_sum.sat) - | Is_first_child -> of_bool (b == is_left summary) - | Is_next_sibling -> of_bool (b == is_right summary) - | Is k -> of_bool (b == (k == kind summary)) - | Has_first_child -> of_bool (b == has_left summary) - | Has_next_sibling -> of_bool (b == has_right summary) + `First_child -> fcs + | `Next_sibling -> nss + | `Parent | `Previous_sibling -> ps + | `Stay -> ss + ) + | Is_first_child -> b == is_left summary + | Is_next_sibling -> b == is_right summary + | Is k -> b == (k == kind summary) + | Has_first_child -> b == has_left summary + | Has_next_sibling -> b == has_right summary end - | Boolean.And(phi1, phi2) -> AND_ (loop phi1, loop phi2) - | Boolean.Or (phi1, phi2) -> OR_ (loop phi1, loop phi2) + | Boolean.And(phi1, phi2) -> loop phi1 && loop phi2 + | Boolean.Or (phi1, phi2) -> loop phi1 || loop phi2 end in loop phi - let eval_trans_aux auto fetch_trans_cache tag fcs nss ps old_status = - let { sat = old_sat; - todo = old_todo; - summary = old_summary } as os_node = old_status.NodeStatus.node - in - let sat, todo = - StateSet.fold (fun q ((a_sat, a_todo) as acc) -> - let phi = - get_form fetch_trans_cache auto tag q - in - - let v = eval_form phi fcs nss ps old_status old_summary in - match v with - True -> StateSet.add q a_sat, a_todo - | False -> acc - | Unknown -> a_sat, StateSet.add q a_todo - ) old_todo (old_sat, StateSet.empty) - in - if old_sat != sat || old_todo != todo then - NodeStatus.make { os_node with sat; todo } - else old_status + let eval_trans_aux auto fetch_trans_cache tag fcs nss ps sat todo summary = + StateSet.fold (fun q (a_sat) -> + let phi = + get_form fetch_trans_cache auto tag q + in + if eval_form phi fcs nss ps a_sat summary then + StateSet.add q a_sat + else a_sat + ) todo sat - let rec eval_trans_fix auto fetch_trans_cache tag fcs nss ps old_status = - let new_status = - eval_trans_aux auto fetch_trans_cache tag fcs nss ps old_status + let rec eval_trans_fix auto fetch_trans_cache tag fcs nss ps sat todo summary = + let new_sat = + eval_trans_aux auto fetch_trans_cache tag fcs nss ps sat todo summary in - if new_status == old_status then old_status else - eval_trans_fix auto fetch_trans_cache tag fcs nss ps new_status + if new_sat == sat then sat else + eval_trans_fix auto fetch_trans_cache tag fcs nss ps new_sat todo summary - let eval_trans auto fetch_trans_cache td_cache tag fcs nss ps ss = - let fcsid = (fcs.NodeStatus.id :> int) in - let nssid = (nss.NodeStatus.id :> int) in - let psid = (ps.NodeStatus.id :> int) in - let ssid = (ss.NodeStatus.id :> int) in + let eval_trans auto fetch_trans_cache eval_cache tag fcs nss ps ss todo summary = + let fcsid = (fcs.StateSet.id :> int) in + let nssid = (nss.StateSet.id :> int) in + let psid = (ps.StateSet.id :> int) in + let ssid = (ss.StateSet.id :> int) in let tagid = (tag.QName.id :> int) in - let res = Cache.N5.find td_cache tagid ssid fcsid nssid psid in + let res = Cache.N6.find eval_cache tagid summary ssid fcsid nssid psid in incr eval_trans_cache_access; - if res != dummy_status then begin incr eval_trans_cache_hit; res end - else let new_status = eval_trans_fix auto fetch_trans_cache tag fcs nss ps ss in - Cache.N5.add td_cache tagid ssid fcsid nssid psid new_status; - new_status + if res != dummy_set then begin incr eval_trans_cache_hit; res end + else let new_sat = + eval_trans_fix auto fetch_trans_cache tag fcs nss ps ss todo summary + in + Cache.N6.add eval_cache tagid summary ssid fcsid nssid psid new_sat; + new_sat + - let top_down run = + let unsafe_get a i = if i < 0 then StateSet.empty else Array.unsafe_get a i + + let top_down run = let i = run.pass in let tree = run.tree in let auto = run.auto in - let status = run.status in - let fetch_trans_cache = run.fetch_trans_cache in - let td_cache = run.td_cache in - let bu_cache = run.bu_cache in let states_by_rank = Ata.get_states_by_rank auto in let td_todo = states_by_rank.(i) in let bu_todo = if i + 1 = Array.length states_by_rank then StateSet.empty else states_by_rank.(i+1) in - let rec loop_td_and_bu node = - if node == T.nil then () else begin + let rec loop_td_and_bu node parent parent_sat = + if node == T.nil then StateSet.empty else begin let node_id = T.preorder tree node in - let parent = T.parent tree node in let fc = T.first_child tree node in - let fc_id = T.preorder tree fc in let ns = T.next_sibling tree node in - let ns_id = T.preorder tree ns in let tag = T.tag tree node in (* We enter the node from its parent *) - let status0 = - let c = unsafe_get_status status node_id in - if c.NodeStatus.node.rank < i then - (* first time we visit the node during this run *) - NodeStatus.make - { rank = i; - sat = c.NodeStatus.node.sat; - todo = td_todo; - summary = - let summary = c.NodeStatus.node.summary in - if summary != NodeSummary.dummy then summary - else - NodeSummary.make - (node != T.next_sibling tree parent) - (fc != T.nil) (* has_left *) - (ns != T.nil) (* has_right *) - (T.kind tree node) (* kind *) - } - else c - in - let () = Logger.msg `STATS "Run %i, Node %a, %a@\n" - i QName.print tag NodeStatus.print status0 + let summary = + let s = Array1.unsafe_get run.node_summaries node_id in + 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 *) + (fc != T.nil) (* has_left *) + (ns != T.nil) (* has_right *) + (T.kind tree node) (* kind *) + in + run.node_summaries.{node_id} <- s; s in + let status0 = unsafe_get run.sat node_id in (* get the node_statuses for the first child, next sibling and parent *) - let ps = unsafe_get_status status (T.preorder tree parent) in - let fcs = unsafe_get_status status fc_id in - let nss = unsafe_get_status status ns_id in + let fcs = unsafe_get run.sat (T.preorder tree fc) in + let nss = unsafe_get run.sat (T.preorder tree ns) in (* evaluate the transitions with all this statuses *) let status1 = - if status0.NodeStatus.node.todo == StateSet.empty then status0 - else begin - let status1 = eval_trans auto fetch_trans_cache td_cache tag fcs nss ps status0 in - (* update the cache if the status of the node changed *) - if status1 != status0 then status.(node_id) <- status1; - status1 - end - in - let () = Logger.msg `STATS "Run %i, Node %a, %a@\n" - i QName.print tag NodeStatus.print status1 - in - (* recursively traverse the first child *) - let () = loop_td_and_bu fc in - (* here we re-enter the node from its first child, - get the new status of the first child *) - let fcs1 = unsafe_get_status status fc_id in - (* update the status *) - let status1 = if status1.NodeStatus.node.rank < i+1 then - NodeStatus.make { status1.NodeStatus.node with - rank = i+1; - todo = bu_todo } - else - status1 - in - let status2 = - if status1.NodeStatus.node.todo == StateSet.empty then status1 - else begin - let status2 = eval_trans auto fetch_trans_cache bu_cache tag fcs1 nss ps status1 in - if status2 != status1 then status.(node_id) <- status2; - status2 - end - in - let () = Logger.msg `STATS "Run %i, Node %a, %a@\n" - (i+1) QName.print tag NodeStatus.print status2 - in - let () = loop_td_and_bu ns in - let nss1 = unsafe_get_status status ns_id in - if status2.NodeStatus.node.todo != StateSet.empty then - let status3 = eval_trans auto fetch_trans_cache bu_cache tag fcs1 nss1 ps status2 in - let () = Logger.msg `STATS "Run %i, Node %a, %a@\n" - (i+1) QName.print tag NodeStatus.print status3 - in - - if status3 != status2 then status.(node_id) <- status3 - end - and loop_td_only node = - if node == T.nil then () else begin - let node_id = T.preorder tree node in - let parent = T.parent tree node in - let fc = T.first_child tree node in - let fc_id = T.preorder tree fc in - let ns = T.next_sibling tree node in - let ns_id = T.preorder tree ns in - let tag = T.tag tree node in - (* We enter the node from its parent *) - let status0 = - let c = unsafe_get_status status node_id in - if c.NodeStatus.node.rank < i then - (* first time we visit the node during this run *) - NodeStatus.make - { rank = i; - sat = c.NodeStatus.node.sat; - todo = td_todo; - summary = - let summary = c.NodeStatus.node.summary in - if summary != NodeSummary.dummy then summary - else - NodeSummary.make - (node != T.next_sibling tree parent) - (fc != T.nil) (* has_left *) - (ns != T.nil) (* has_right *) - (T.kind tree node) (* kind *) - } - else c + eval_trans auto run.fetch_trans_cache run.td_cache tag fcs nss + parent_sat + status0 td_todo summary in - let () = Logger.msg `STATS "Run %i, Node %a, %a@\n" - (i) QName.print tag NodeStatus.print status0 - in - - (* get the node_statuses for the first child, next sibling and parent *) - let ps = unsafe_get_status status (T.preorder tree parent) in - let fcs = unsafe_get_status status fc_id in - let nss = unsafe_get_status status ns_id in - (* evaluate the transitions with all this statuses *) - if status0.NodeStatus.node.todo != StateSet.empty then begin - let status1 = eval_trans auto fetch_trans_cache td_cache tag fcs nss ps status0 in - (* update the cache if the status of the node changed *) - let () = Logger.msg `STATS "Run %i, Node %a, %a@\n" - (i) QName.print tag NodeStatus.print status1 + (* update the cache if the status of the node changed *) + if status1 != status0 then run.sat.(node_id) <- status1; + let fcs1 = loop_td_and_bu fc node status1 in + if bu_todo == StateSet.empty then + loop_td_and_bu ns node status1 (* tail call *) + else + let nss1 = loop_td_and_bu ns node status1 in + let status2 = + eval_trans auto run.fetch_trans_cache run.bu_cache tag fcs1 nss1 + parent_sat + status1 bu_todo summary in - - if status1 != status0 then status.(node_id) <- status1; - end; - (* recursively traverse the first child *) - loop_td_only fc; - loop_td_only ns + if status2 != status1 then run.sat.(node_id) <- status2; + status2 end in - if bu_todo == StateSet.empty then - let () = loop_td_only (T.root tree) in - run.pass <- run.pass + 1 - else - let () = loop_td_and_bu (T.root tree) in - run.pass <- run.pass + 2 + let _ = loop_td_and_bu (T.root tree) T.nil StateSet.empty in + run.pass <- run.pass + 2 let get_results run = - let cache = run.status in + let cache = run.sat in let auto = run.auto in let tree = run.tree in let sel_states = Ata.get_selecting_states auto in @@ -481,7 +275,7 @@ DEFINE AND_(t1,t2) = let acc1 = loop (T.first_child tree node) acc0 in if StateSet.intersect - cache.(T.preorder tree node).NodeStatus.node.sat + cache.(T.preorder tree node)(* NodeStatus.node.sat *) sel_states then node::acc1 else acc1 in @@ -489,7 +283,7 @@ DEFINE AND_(t1,t2) = let get_full_results run = - let cache = run.status in + let cache = run.sat(*tatus*) in let auto = run.auto in let tree = run.tree in let res_mapper = Hashtbl.create MED_H_SIZE in @@ -515,7 +309,7 @@ DEFINE AND_(t1,t2) = if res != dummy then Cache.N1.add res_mapper (q :> int) (node::res) ) - cache.(T.preorder tree node).NodeStatus.node.sat + cache.(T.preorder tree node)(* NodeStatus.node.sat *) in loop (T.root tree); (StateSet.fold_right @@ -526,26 +320,10 @@ DEFINE AND_(t1,t2) = let prepare_run run list = let tree = run.tree in let auto = run.auto in - let status = run.status in + let sat0 = Ata.get_starting_states auto in List.iter (fun node -> - let parent = T.parent tree node in - let fc = T.first_child tree node in - let ns = T.next_sibling tree node in - let status0 = - NodeStatus.make - { rank = 0; - sat = Ata.get_starting_states auto; - todo = - StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto); - summary = NodeSummary.make - (node != T.next_sibling tree parent) (* is_left *) - (fc != T.nil) (* has_left *) - (ns != T.nil) (* has_right *) - (T.kind tree node) (* kind *) - } - in let node_id = T.preorder tree node in - status.(node_id) <- status0) list + run.sat.(node_id) <- sat0) list let tree_size = ref 0 let pass = ref 0 @@ -557,11 +335,10 @@ DEFINE AND_(t1,t2) = let rank = Ata.get_max_rank auto in while run.pass <= rank do top_down run; - run.td_cache <- Cache.N5.create dummy_status; - run.bu_cache <- Cache.N5.create dummy_status; + run.td_cache <- Cache.N6.create dummy_set; + run.bu_cache <- Cache.N6.create dummy_set; done; pass := Ata.get_max_rank auto + 1; - IFTRACE(Html.gen_trace auto (module T : Tree.S with type t = T.t) tree); run