(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-04-22 18:25:49 CEST by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-04-25 17:22:15 CEST by Kim Nguyen>
*)
INCLUDE "utils.ml"
let html tree node i config msg =
let config = config.Ata.Config.node in
Html.trace (T.preorder tree node) i
- "%s<br/>sat: %a<br/>unsat: %a<br/>todo: %a<br/>"
+ "node: %i<br/>%s<br/>sat: %a<br/>unsat: %a<br/>todo: %around: %i<br/>"
+ (T.preorder tree node)
msg
StateSet.print config.Ata.sat
StateSet.print config.Ata.unsat
- (Ata.TransList.print ~sep:"<br/>") config.Ata.todo
+ (Ata.TransList.print ~sep:"<br/>") config.Ata.todo i
- type cache = StateSet.t Cache.N1.t
- let get c t n = Cache.N1.find c (T.preorder t n)
- let set c t n v = Cache.N1.add c (T.preorder t n) v
+ type run = { config : Ata.Config.t array;
+ unstable : Bitvector.t;
+ mutable redo : bool;
+ mutable pass : int;
+ }
+
- let top_down_run auto tree node cache _i =
- let redo = ref false in
+ 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 =
- if node != T.nil then begin
+ 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 = get cache tree node in
- if c == Cache.N1.dummy cache 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 *)
- }
+ 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 = get cache tree parent in
- let fcs = get cache tree fc in
- let nss = get cache tree ns in
+ 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 set cache tree node config1;
- let () = loop fc in
- let fcs1 = get cache tree fc in
+ 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 set cache tree node config2;
- let () = loop ns in
- let config3 = Ata.eval_trans auto fcs1 (get cache tree ns) ps config2 in
+ 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 set cache tree node config3;
- (* We do set the redo flat if : *)
- if not (
- config0 == config3 (* did not gain any new information *)
- || !redo (* already set *)
- || Ata.TransList.nil == config3.Ata.Config.node.Ata.todo ) (* no more transition to check *)
- then redo := true
+ 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;
- !redo
+ loop node
let get_results auto tree node cache =
let rec loop node acc =
let acc0 = loop (T.next_sibling tree node) acc in
let acc1 = loop (T.first_child tree node) acc0 in
- if StateSet.intersect (get cache tree node).Ata.Config.node.Ata.sat auto.Ata.selection_states then
- node::acc1
- else
- acc1
+ 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 cache = Cache.N1.create
- (Ata.Config.make { Ata.sat = StateSet.empty;
- Ata.unsat = StateSet.empty;
- Ata.todo = Ata.TransList.nil;
- Ata.summary = Ata.dummy_summary;
- })
+ 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
- let redo = ref true in
- let iter = ref 0 in
- Ata.reset auto;
- while !redo do
- redo := false;
+ while run.redo do
+ run.redo <- false;
Ata.reset auto; (* prevents the .cache2 and .cache4 memoization tables from growing too much *)
- redo := top_down_run auto tree node cache !iter;
- incr iter;
+ run.redo <- top_down_run auto tree node run;
+ stats run;
+ run.pass <- run.pass + 1;
done;
- at_exit (fun () -> eprintf "@[STATS: %i iterations@]@." !iter);
- let r = get_results auto tree node cache in
+ 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
projects / tatoo.git / blobdiff