open Format
open Misc
-open Bigarray
type stats = { mutable pass : int;
tree_size : int;
if i < 0 then StateSet.empty else
Array.unsafe_get (IFHTML(List.hd a, a)) i
-let unsafe_set a i v old_v =
- if v != old_v then
+let unsafe_set a i v =
+ (* if v != old_v then *)
Array.unsafe_set (IFHTML(List.hd a, a)) i v
-type 'a run = {
- tree : 'a ;
+type 'node td_action = 'node -> int -> 'node -> 'node -> StateSet.t
+type 'node bu_action = 'node -> int -> StateSet.t
+let dummy_action = fun _ _ -> assert false
+
+type ('tree, 'node) run = {
+ tree : 'tree ;
(* The argument of the run *)
auto : Ata.t;
(* The automaton to be run *)
(* 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 : StateSet.t Cache.N6.t;
- mutable bu_cache : StateSet.t Cache.N6.t;
+ mutable td_cache : 'node td_action Cache.N6.t;
+ mutable bu_cache : 'node bu_action 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; *)
node_summaries: Bytes.t;
stats : stats;
}
eval_trans_fix run tag summary fcs nss ps new_sat todo
-let eval_trans run trans_cache tag summary fcs nss ps ss todo =
+let eval_trans run trans_cache tag summary fcs nss ps ss todo action_builder =
let stats = run.stats in
let fcsid = (fcs.StateSet.id :> int) in
let nssid = (nss.StateSet.id :> int) in
let res = Cache.N6.find trans_cache tagid summary ssid fcsid nssid psid in
stats.eval_trans_cache_access <- 1 + stats.eval_trans_cache_access;
- if res != dummy_set then
+ if res != dummy_action then
res
- else let new_sat = if todo == StateSet.empty then ss else
- eval_trans_fix run tag summary fcs nss ps ss todo
+ else
+ let new_sat =
+ eval_trans_fix run tag summary fcs nss ps ss todo
in
stats.eval_trans_cache_miss <- 1 + stats.eval_trans_cache_miss;
- Cache.N6.add trans_cache tagid summary ssid fcsid nssid psid new_sat;
- new_sat
+ let new_action = action_builder ps summary tag new_sat in
+ Cache.N6.add trans_cache tagid summary ssid fcsid nssid psid new_action;
+ new_action
module Make (T : Tree.S) =
let make auto tree =
let len = Tree.size tree in
- (* let ba = Array1.create int16_unsigned c_layout len in
- Array1.fill ba 0; *)
let ba = Bytes.make len '\000' in
{
tree = tree;
IFHTML([a], a));
pass = 0;
fetch_trans_cache = Cache.N2.create dummy_form;
- td_cache = Cache.N6.create dummy_set;
- bu_cache = Cache.N6.create dummy_set;
+ td_cache = Cache.N6.create dummy_action;
+ bu_cache = Cache.N6.create dummy_action;
node_summaries = ba;
stats = {
pass = 0;
}
- let top_down2 run update_res =
+ let top_down run mk_update_res =
let num_visited = ref 0 in
let i = run.pass in
let tree = run.tree in
in
let run_sat = run.sat in
let last_run = i >= Array.length states_by_rank - 2 in
- let rec common node parent parent_sat kont =
+
+ let rec common node parent parent_sat action_builder =
if node == Tree.nil then StateSet.empty
else begin
incr num_visited;
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 status1 =
+ let action =
eval_trans run
run.td_cache tag
summary
(unsafe_get run_sat (Tree.preorder tree fc))
(unsafe_get run_sat (Tree.preorder tree ns))
parent_sat
- status0 td_todo
+ status0 td_todo action_builder
in
- kont summary tag parent_sat status0 status1 fc ns node node_id
+ action node node_id fc ns
end
- and kont_pure_td summary tag parent_sat status0 status1 fc ns node node_id =
- unsafe_set run_sat node_id status1 status0; (* write the td_states *)
- update_res false status1 node;
- if fc != Tree.nil then ignore (loop_td fc node status1);
- if ns == Tree.nil then StateSet.empty else loop_td ns node status1 (* tail call *)
- and kont_td_and_bu summary tag parent_sat status0 status1 fc ns node node_id =
- let fcs1 = if fc == Tree.nil then StateSet.empty else loop_td_and_bu fc node status1 in
- let nss1 = if ns == Tree.nil then StateSet.empty else loop_td_and_bu ns node status1 in
- let status2 =
- eval_trans run run.bu_cache tag
- summary fcs1
- nss1
- parent_sat
- status1 bu_todo
+ and td_action_builder parent_sat summary tag status1 =
+ let update_res = mk_update_res false status1 in
+ match NodeSummary.(has_left summary, has_right summary) with
+ false, false ->
+ (fun node node_id fc ns ->
+ unsafe_set run_sat node_id status1;
+ update_res node;
+ StateSet.empty)
+ | true, false ->
+ (fun node node_id fc ns ->
+ unsafe_set run_sat node_id status1;
+ update_res node;
+ loop_td fc node status1)
+ | false, true ->
+ (fun node node_id fc ns ->
+ unsafe_set run_sat node_id status1;
+ update_res node;
+ loop_td ns node status1)
+ | _ ->
+ (fun node node_id fc ns ->
+ unsafe_set run_sat node_id status1; (* write the td_states *)
+ update_res node;
+ ignore (loop_td fc node status1);
+ loop_td ns node status1 (* tail call *)
+ )
+ and td_and_bu_action_builder parent_sat summary tag status1 node node_id fc ns =
+ let fcs1 = loop_td_and_bu fc node status1 in
+ let nss1 = loop_td_and_bu ns node status1 in
+ let action =
+ eval_trans run run.bu_cache tag summary fcs1 nss1 parent_sat status1 bu_todo bu_action_builder
in
- unsafe_set run_sat node_id status2 status0;
+ action node node_id
+ and bu_action_builder parent_sat summary tag status2 node node_id =
+ unsafe_set run_sat node_id status2;
status2
- and kont_td_and_bu_last summary tag parent_sat status0 status1 fc ns node node_id =
- let nss1 = if ns == Tree.nil then StateSet.empty else loop_td_and_bu_last ns node status1 in
- let fcs1 = if fc == Tree.nil then StateSet.empty else loop_td_and_bu_last fc node status1 in
- let status2 =
- eval_trans run run.bu_cache tag
- summary fcs1
- nss1
- parent_sat
- status1 bu_todo
+ and td_and_bu_last_action_builder parent_sat summary tag status1 node node_id fc ns =
+ let nss1 = loop_td_and_bu_last ns node status1 in
+ let fcs1 = loop_td_and_bu_last fc node status1 in
+ let action =
+ eval_trans run run.bu_cache tag summary fcs1 nss1 parent_sat status1 bu_todo bu_last_action_builder
in
- unsafe_set run_sat node_id status2 status0;
- if status2 != StateSet.empty then update_res true status2 node;
- status2
+ action node node_id
+ and bu_last_action_builder parent_sat summary tag status2 =
+ let update_res = mk_update_res true status2 in
+ (fun node node_id ->
+ unsafe_set run_sat node_id status2;
+ update_res node;
+ status2)
and loop_td node parent parent_sat =
- common node parent parent_sat kont_pure_td
+ common node parent parent_sat td_action_builder
and loop_td_and_bu node parent parent_sat =
- common node parent parent_sat kont_td_and_bu
+ common node parent parent_sat td_and_bu_action_builder
and loop_td_and_bu_last node parent parent_sat =
- common node parent parent_sat kont_td_and_bu_last
+ common node parent parent_sat td_and_bu_last_action_builder
in
-
let _ =
if bu_todo == StateSet.empty then
loop_td (Tree.root tree) Tree.nil dummy_set
run.stats.nodes_per_run <- !num_visited :: run.stats.nodes_per_run
- type res_op = Dummy | Prepend | Append | Nothing
let mk_update_result auto =
let sel_states = Ata.get_selecting_states auto in
let res = ResultSet.create () in
- let cache = Cache.N2.create Dummy in
- (fun prepend sat node ->
- let sat_id = (sat.StateSet.id :> int) in
- let prep_id : int = Obj.magic prepend in
- let op = Cache.N2.find cache prep_id sat_id in
- let op =
- if op == Dummy then
- let op =
- if StateSet.intersect sel_states sat then
- if prepend then
- Prepend
- else Append
- else Nothing
- in
- let () = Cache.N2.add cache prep_id sat_id op in
- op
- else op
- in
- match op with
- Dummy | Nothing -> ()
- | Prepend -> ResultSet.push_front node res
- | Append -> ResultSet.push_back node res
- (*
- if StateSet.intersect sel_states sat then begin
- if prepend then L.push_front node res else
- L.push_back node res
- end*)),
+ (fun prepend sat ->
+ if StateSet.intersect sat sel_states then
+ if prepend then (fun n -> ResultSet.push_front n res)
+ else (fun n -> ResultSet.push_back n res)
+ else (fun _ -> ())),
(fun () -> res)
let mk_update_full_result auto =
- let dummy = ResultSet.create () in
- let res_mapper = Cache.N1.create dummy in
- let () =
- StateSet.iter
- (fun q -> Cache.N1.add res_mapper (q :> int) (ResultSet.create()))
- (Ata.get_selecting_states auto)
+ let sel_states = Ata.get_selecting_states auto in
+ let res_mapper =
+ StateSet.fold_right (fun q acc -> (q, ResultSet.create())::acc) sel_states []
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 ResultSet.push_front node res
- else ResultSet.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) [])
+ (fun prepend sat ->
+ StateSet.fold (fun q f_acc ->
+ if StateSet.mem q sel_states then
+ let res = List.assoc q res_mapper in
+ if prepend then (fun n -> ResultSet.push_front n res; f_acc n)
+ else (fun n -> ResultSet.push_front n res; f_acc n)
+ else f_acc) sat (fun _ -> ())),
+ (fun () -> res_mapper)
let prepare_run run list =
let tree = run.tree in
sat.(node_id) <- sat0) list
- let compute_run auto tree nodes update_res =
+ let compute_run auto tree nodes mk_update_res =
let run = make auto tree in
prepare_run run nodes;
let rank = Ata.get_max_rank auto in
while run.pass <= rank do
- top_down2 run update_res;
+ top_down run mk_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;
+ run.td_cache <- Cache.N6.create dummy_action;
+ run.bu_cache <- Cache.N6.create dummy_action;
done;
IFHTML((run.sat <- List.tl run.sat), ());
IFHTML(Html_trace.gen_trace auto run.sat (module T : Tree.S with type t = Tree.t) tree ,());
let last_stats = ref None
let full_eval auto tree nodes =
- let update_full,get_full = mk_update_full_result auto in
- let run = compute_run auto tree nodes update_full in
+ let mk_update_full,get_full = mk_update_full_result auto in
+ let run = compute_run auto tree nodes mk_update_full in
last_stats := Some run.stats;
get_full ()
let eval auto tree nodes =
- let update_res,get_res = mk_update_result auto in
- let run = compute_run auto tree nodes update_res in
+ let mk_update_res,get_res = mk_update_result auto in
+ let run = compute_run auto tree nodes mk_update_res in
last_stats := Some run.stats;
get_res ()
projects / tatoo.git / commitdiff