(***********************************************************************)
(* *)
(* 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 "utils.ml"
open Format
module Make (T : Tree.S) :
sig
val eval : Ata.t -> T.t -> T.node -> T.node list
end
= struct
IFDEF HTMLTRACE
THEN
DEFINE TRACE(e) = (e)
ELSE
DEFINE TRACE(e) = ()
END
let html tree node i config msg =
let config = config.Ata.Config.node in
Html.trace (T.preorder tree node) i
"node: %i
%s
sat: %a
unsat: %a
todo: %around: %i
"
(T.preorder tree node)
msg
StateSet.print config.Ata.sat
StateSet.print config.Ata.unsat
(Ata.TransList.print ~sep:"
") config.Ata.todo i
type run = { config : Ata.Config.t array;
unstable : Bitvector.t;
mutable redo : bool;
mutable pass : int;
}
let top_down_run auto tree node run =
let module Array =
struct
include Array
let get a i =
if i < 0 then Ata.dummy_config else get a i
let unsafe_get a i =
if i < 0 then Ata.dummy_config else unsafe_get a i
end
in
let cache = run.config in
let unstable = run.unstable in
let _i = run.pass in
let rec loop node =
let node_id = T.preorder tree node in
if node == T.nil || not (Bitvector.get unstable node_id) then false else begin
let parent = T.parent tree node in
let fc = T.first_child tree node in
let fc_id = T.preorder tree fc in
let ns = T.next_sibling tree node in
let ns_id = T.preorder tree ns in
let tag = T.tag tree node in
let config0 =
let c = cache.(node_id) in
if c == Ata.dummy_config then
Ata.Config.make
{ c.Ata.Config.node with
Ata.todo = Ata.get_trans auto tag auto.Ata.states;
summary = Ata.node_summary
(node == T.first_child tree parent) (* is_left *)
(node == T.next_sibling tree parent) (* is_right *)
(fc != T.nil) (* has_left *)
(ns != T.nil) (* has_right *)
(T.kind tree node) (* kind *)
}
else c
in
TRACE(html tree node _i config0 "Entering node");
let ps = cache.(T.preorder tree parent) in
let fcs = cache.(fc_id) in
let nss = cache.(ns_id) in
let config1 = Ata.eval_trans auto fcs nss ps config0 in
TRACE(html tree node _i config1 "Updating transitions");
if config0 != config1 then cache.(node_id) <- config1;
let unstable_left = loop fc in
let fcs1 = cache.(fc_id) in
let config2 = Ata.eval_trans auto fcs1 nss ps config1 in
TRACE(html tree node _i config2 "Updating transitions (after first-child)");
if config1 != config2 then cache.(node_id) <- config2;
let unstable_right = loop ns in
let nss1 = cache.(ns_id) in
let config3 = Ata.eval_trans auto fcs1 nss1 ps config2 in
TRACE(html tree node _i config3 "Updating transitions (after next-sibling)");
if config2 != config3 then cache.(node_id) <- config3;
let unstable_self =
unstable_left
|| unstable_right
|| Ata.(TransList.nil != config3.Config.node.todo)
in
Bitvector.unsafe_set unstable node_id unstable_self;
TRACE((if not unstable_self then
Html.finalize_node
node_id
_i
Ata.(StateSet.intersect config3.Config.node.sat auto.selection_states)));
unstable_self
end
in
loop node
let get_results auto tree node cache =
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 Ata.(
StateSet.intersect
cache.(T.preorder tree node).Config.node.sat
auto.selection_states) then node::acc1
else acc1
in
loop node []
let stats run =
let count = ref 0 in
let len = Bitvector.length run.unstable in
for i = 0 to len - 1 do
if not (Bitvector.unsafe_get run.unstable i) then
incr count
done;
Logger.msg `STATS
"%i nodes over %i were skipped in iteration %i (%.2f %%), redo is: %b"
!count len run.pass (100. *. (float !count /. float len))
run.redo
let eval auto tree node =
let len = T.size tree in
let run = { config = Array.create len Ata.dummy_config;
unstable = Bitvector.create ~init:true len;
redo = true;
pass = 0
}
in
while run.redo do
run.redo <- false;
Ata.reset auto; (* prevents the .cache2 and .cache4 memoization tables from growing too much *)
run.redo <- top_down_run auto tree node run;
stats run;
run.pass <- run.pass + 1;
done;
at_exit (fun () -> Logger.msg `STATS "%i iterations" run.pass);
at_exit (fun () -> stats run);
let r = get_results auto tree node run.config in
TRACE(Html.gen_trace (module T : Tree.S with type t = T.t) (tree));
r
end