(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-04-25 11:20:58 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
- let oldi = config.Ata.round in
- Html.trace (T.preorder tree node) i oldi
+ Html.trace (T.preorder tree node) i
"node: %i<br/>%s<br/>sat: %a<br/>unsat: %a<br/>todo: %around: %i<br/>"
- ((T.preorder tree node):>int)
+ (T.preorder tree node)
msg
StateSet.print config.Ata.sat
StateSet.print config.Ata.unsat
- (Ata.TransList.print ~sep:"<br/>") config.Ata.todo oldi
+ (Ata.TransList.print ~sep:"<br/>") config.Ata.todo i
- let get c t n = Cache.N1.find c (T.preorder t n)
- let set c t n v i =
- v.Ata.Config.node.Ata.round <- i;
- Cache.N1.add c (T.preorder t n) v
-
-
- type run = { config : Ata.Config.t Cache.N1.t;
+ 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 =
- if node == T.nil then false else 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
+ 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;
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 _i;
- let old_unstable_left = Bitvector.unsafe_get unstable (T.preorder tree fc) in
- let unstable_left = old_unstable_left && 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 _i;
- let old_unstable_right = Bitvector.unsafe_get unstable (T.preorder tree ns) in
- let unstable_right = old_unstable_right && loop ns in
- let nss1 = get cache tree ns 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 _i;
+ 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 (T.preorder tree node) unstable_self;
+ 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
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
+ if Ata.(
+ StateSet.intersect
+ cache.(T.preorder tree node).Config.node.sat
+ auto.selection_states) then node::acc1
else acc1
in
loop node []
if not (Bitvector.unsafe_get run.unstable i) then
incr count
done;
- eprintf "@[STATS: %i nodes over %i were skipped in iteration %i (%.2f %%), redo is: %b@]@."
+ 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 run = { config = Cache.N1.create
- Ata.(Config.make { sat = StateSet.empty;
- unsat = StateSet.empty;
- todo = TransList.nil;
- summary = dummy_summary;
- round = ~-1
- });
- unstable = Bitvector.create ~init:true (T.size tree);
+ 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
}
stats run;
run.pass <- run.pass + 1;
done;
- at_exit (fun () -> eprintf "@[STATS: %i iterations@]@." run.pass);
+ 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
projects / tatoo.git / blobdiff