--- /dev/null
+(***********************************************************************)
+(* *)
+(* 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 }
--- /dev/null
+(***********************************************************************)
+(* *)
+(* 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
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 = 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 =
(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
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;
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 ->
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;
projects / tatoo.git / commitdiff