mutable nodes_per_run : int list;
}
-module NodeSummary =
-struct
- (* Pack into an integer the result of the is_* and has_ predicates
- for a given node *)
- type t = int
- let dummy = -1
- (*
- ...44443210
- ...4444 -> kind
- 3 -> has_right
- 2 -> has_left
- 1 -> is_right
- 0 -> is_left
- *)
- let is_left (s : t) : bool =
- s land 1 != 0
-
- let is_right (s : t) : bool =
- s land 0b10 != 0
-
- let has_left (s : t) : bool =
- s land 0b100 != 0
-
- let has_right (s : t) : bool =
- s land 0b1000 != 0
-
- let kind (s : t) : Tree.NodeKind.t =
- Obj.magic (s lsr 4)
-
- let make is_left is_right has_left has_right kind =
- (int_of_bool is_left) lor
- ((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
let dummy_set = StateSet.singleton State.dummy_state
(* 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: Bytes.t;
stats : stats;
}
| Boolean.True -> true
| Boolean.Atom (a, b) ->
begin
- let open NodeSummary in
+ let open Tree.NodeSummary in
match a.Atom.node with
| Move (m, q) ->
b && StateSet.mem q (
Cache.N6.add trans_cache tagid summary ssid fcsid nssid psid new_action;
new_action
-
+module NodeSummary = Tree.NodeSummary
module Make (T : Tree.S) =
struct
module Tree : Tree.S with type node = T.node = T
let make auto tree =
let len = Tree.size tree in
- let ba = Bytes.make len '\000' in
{
tree = tree;
auto = auto;
fetch_trans_cache = Cache.N2.create dummy_form;
td_cache = Cache.N6.create dummy_action;
bu_cache = Cache.N6.create dummy_action;
- node_summaries = ba;
stats = {
pass = 0;
tree_size = len;
let last_run = i >= Array.length states_by_rank - 2 in
let rec common node parent parent_sat action_builder =
- if node == Tree.nil then StateSet.empty
- else begin
+ begin
incr num_visited;
let tag = Tree.tag tree node in
let node_id = Tree.preorder tree node in
+ let summary = Tree.summary tree node in
let fc = Tree.first_child tree node in
let ns = Tree.next_sibling tree node in
(* We enter the node from its parent *)
- let summary =
- let s = Char.code (Bytes.unsafe_get run.node_summaries node_id) in
- if s != 0 then s else
- let s =
- NodeSummary.make
- (node == (Tree.first_child tree parent)) (*is_left *)
- (node == (Tree.next_sibling tree parent)) (*is_right *)
- (fc != Tree.nil) (* has_left *)
- (ns != Tree.nil) (* has_right *)
- (Tree.kind tree node) (* kind *)
- in
- Bytes.unsafe_set run.node_summaries node_id (Char.chr s); s
- in
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 *)
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
- action node node_id
+ )
+ and td_and_bu_action_builder parent_sat summary tag status1 =
+ match NodeSummary.(has_left summary, has_right summary) with
+ false, false ->
+ (fun node node_id fc ns ->
+ let action =
+ eval_trans run run.bu_cache tag summary StateSet.empty StateSet.empty
+ parent_sat status1 bu_todo bu_action_builder
+ in
+ action node node_id)
+ | true, false ->
+ (fun node node_id fc ns ->
+ let fcs1 = loop_td_and_bu fc node status1 in
+ let action =
+ eval_trans run run.bu_cache tag summary fcs1 StateSet.empty
+ parent_sat status1 bu_todo bu_action_builder
+ in
+ action node node_id
+ )
+ | false, true ->
+ (fun node node_id fc ns ->
+ let nss1 = loop_td_and_bu ns node status1 in
+ let action =
+ eval_trans run run.bu_cache tag summary StateSet.empty nss1
+ parent_sat status1 bu_todo bu_action_builder
+ in
+ action node node_id
+ )
+ | _ ->
+ (fun 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
+ 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 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
- action node node_id
+ and td_and_bu_last_action_builder parent_sat summary tag status1 =
+ match NodeSummary.(has_left summary, has_right summary) with
+ false, false ->
+ (fun node node_id fc ns ->
+ let action =
+ eval_trans run run.bu_cache tag summary StateSet.empty StateSet.empty
+ parent_sat status1 bu_todo bu_last_action_builder
+ in
+ action node node_id)
+ | true, false ->
+ (fun node node_id fc ns ->
+ let fcs1 = loop_td_and_bu_last fc node status1 in
+ let action =
+ eval_trans run run.bu_cache tag summary fcs1 StateSet.empty
+ parent_sat status1 bu_todo bu_last_action_builder
+ in
+ action node node_id
+ )
+ | false, true ->
+ (fun node node_id fc ns ->
+ let nss1 = loop_td_and_bu_last ns node status1 in
+ let action =
+ eval_trans run run.bu_cache tag summary StateSet.empty nss1
+ parent_sat status1 bu_todo bu_last_action_builder
+ in
+ action node node_id
+ )
+ | _ ->
+ (fun 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
+ 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 ->
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 (fun n -> ResultSet.push_back n res; f_acc n)
else f_acc) sat (fun _ -> ())),
(fun () -> res_mapper)