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 =
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_id == T.preorder tree (T.first_child tree parent)) (*is_left *)
+ (node_id == T.preorder tree (T.next_sibling tree parent))(*is_right *)
(fc != T.nil) (* has_left *)
(ns != T.nil) (* has_right *)
(T.kind tree node) (* kind *)
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
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
+ 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) []
+ loop (T.root tree);
+ res
let get_full_results run =
(fun q -> Hashtbl.add res_mapper q [])
(Ata.get_selecting_states auto)
in
- let dummy = [ T.nil ] 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) [])
+ (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
- let () = loop (T.next_sibling tree node) in
- let () = loop (T.first_child tree node) in
+ if node != T.nil then begin
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)
+ if res != dummy then L.add node res
)
- cache.(T.preorder tree node)
+ 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
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 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 =
pass := 0;
tree_size := T.size tree;
prepare_run run nodes;
let rank = Ata.get_max_rank auto in
while run.pass <= rank do
- top_down run;
+ time top_down run ("Timing run number " ^ string_of_int run.pass ^ "/" ^ string_of_int (Ata.get_max_rank auto + 1));
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;
let eval auto tree nodes =
let r = compute_run auto tree nodes in
- get_results r
+ let nl = get_results r in
+ nl
let stats () = {
tree_size = !tree_size;