From 3406b26f1ea26a997d7f194c547439891c108ce6 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Sat, 11 Jan 2014 00:34:11 +0100 Subject: [PATCH] Abstract result sets beind a Node_list interface. --- src/naive_node_list.ml | 58 +++++++++++++++++++++++++++++++++++++++ src/naive_node_list.mli | 17 ++++++++++++ src/node_list.ml | 25 +++++++++++++++++ src/run.ml | 60 ++++++++++++++++++++++++++--------------- src/run.mli | 6 ++--- src/tatoo.ml | 9 ++++--- 6 files changed, 146 insertions(+), 29 deletions(-) create mode 100644 src/naive_node_list.ml create mode 100644 src/naive_node_list.mli create mode 100644 src/node_list.ml diff --git a/src/naive_node_list.ml b/src/naive_node_list.ml new file mode 100644 index 0000000..c148732 --- /dev/null +++ b/src/naive_node_list.ml @@ -0,0 +1,58 @@ +(***********************************************************************) +(* *) +(* TAToo *) +(* *) +(* Kim Nguyen, LRI UMR8623 *) +(* Université Paris-Sud & CNRS *) +(* *) +(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *) +(* Recherche Scientifique. All rights reserved. This file is *) +(* distributed under the terms of the GNU Lesser General Public *) +(* License, with the special exception on linking described in file *) +(* ../LICENSE. *) +(* *) +(***********************************************************************) + + +type node = Naive_tree.node +type cell = { node : node; + mutable next : cell } + + +type t = { mutable length : int; + mutable head : cell; + mutable last : cell; } + +let rec nil = { node = Naive_tree.nil; + next = nil } + +let create () = { length = 0; + head = nil; + last = nil } + +let iter f l = + let rec loop c = + if c != nil then begin + f c.node; + loop c.next + end + in + loop l.head + + +let length l = l.length + + +let add n l = + let ncell = { node = n; + next = nil } + in + if l.last == nil then + { length = 1; + head = ncell; + last = ncell } + else + let () = l.last.next <- ncell in + { length = l.length + 1; + head = l.head; + last = ncell } diff --git a/src/naive_node_list.mli b/src/naive_node_list.mli new file mode 100644 index 0000000..e1fde9c --- /dev/null +++ b/src/naive_node_list.mli @@ -0,0 +1,17 @@ +(***********************************************************************) +(* *) +(* TAToo *) +(* *) +(* Kim Nguyen, LRI UMR8623 *) +(* Université Paris-Sud & CNRS *) +(* *) +(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *) +(* Recherche Scientifique. All rights reserved. This file is *) +(* distributed under the terms of the GNU Lesser General Public *) +(* License, with the special exception on linking described in file *) +(* ../LICENSE. *) +(* *) +(***********************************************************************) + + +include Node_list.S with type node = Naive_tree.node diff --git a/src/node_list.ml b/src/node_list.ml new file mode 100644 index 0000000..2219d5b --- /dev/null +++ b/src/node_list.ml @@ -0,0 +1,25 @@ +(***********************************************************************) +(* *) +(* TAToo *) +(* *) +(* Kim Nguyen, LRI UMR8623 *) +(* Université Paris-Sud & CNRS *) +(* *) +(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *) +(* Recherche Scientifique. All rights reserved. This file is *) +(* distributed under the terms of the GNU Lesser General Public *) +(* License, with the special exception on linking described in file *) +(* ../LICENSE. *) +(* *) +(***********************************************************************) + +module type S = + sig + type node + type t + + val create : unit -> t + val add : node -> t -> t + val iter : (node -> unit) -> t -> unit + val length : t -> int + end diff --git a/src/run.ml b/src/run.ml index fb9f81d..8eb58f9 100644 --- a/src/run.ml +++ b/src/run.ml @@ -203,7 +203,7 @@ END 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 = @@ -245,8 +245,8 @@ module Make (T : Tree.S) = 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 *) @@ -266,6 +266,7 @@ module Make (T : Tree.S) = 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 @@ -294,16 +295,17 @@ module Make (T : Tree.S) = 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 = ref (L.create ()) in + let rec loop node = + if node != T.nil then begin + if StateSet.intersect sel_states cache.(T.preorder tree node) then + res := L.add 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 = @@ -316,24 +318,26 @@ module Make (T : Tree.S) = (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) + Cache.N1.add res_mapper (q :> int) (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 @@ -346,12 +350,23 @@ module Make (T : Tree.S) = 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; @@ -359,7 +374,7 @@ module Make (T : Tree.S) = 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; @@ -375,7 +390,8 @@ module Make (T : Tree.S) = 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; diff --git a/src/run.mli b/src/run.mli index 725192e..e124e8a 100644 --- a/src/run.mli +++ b/src/run.mli @@ -19,9 +19,9 @@ type stats = { run : int; eval_trans_cache_access : int; eval_trans_cache_hit : int; } -module Make (T : Tree.S) : +module Make (T : Tree.S) (L : Node_list.S with type node = T.node) : sig - val eval : Ata.t -> T.t -> T.node list -> T.node list - val full_eval : Ata.t -> T.t -> T.node list -> (State.t * T.node list) list + val eval : Ata.t -> T.t -> L.t -> L.t + val full_eval : Ata.t -> T.t -> L.t -> (State.t * L.t) list val stats : unit -> stats end diff --git a/src/tatoo.ml b/src/tatoo.ml index 9fb7045..24e212f 100644 --- a/src/tatoo.ml +++ b/src/tatoo.ml @@ -104,9 +104,10 @@ let main () = Logger.msg `STATS "@[Automaton: @\n%a@]" Ata.print auto) auto_list; end; - let module Naive = Run.Make(Naive_tree) in + let module Naive = Run.Make(Naive_tree)(Naive_node_list) in let result_list = - let root = [ Naive_tree.root doc] in + + let root = Naive_node_list.(add (Naive_tree.root doc) (create())) in let f, msg = match !Options.parallel, !Options.compose with true, true -> @@ -134,10 +135,10 @@ let main () = output_string output (string_of_int !count); output_string output "\" >\n"; if !Options.count then begin - output_string output (string_of_int (List.length results)); + output_string output (string_of_int (Naive_node_list.length results)); output_char output '\n'; end else - List.iter (fun n -> + Naive_node_list.iter (fun n -> Naive_tree.print_xml output doc n; output_char output '\n' ) results; -- 2.17.1