(Ata.TransList.print ~sep:"<br/>") config.todo i
+ let debug msg tree node i config =
+ let config = config.NodeStatus.node in
+ eprintf
+ "DEBUG:%s node: %i\nsat: %a\nunsat: %a\ntodo: %around: %i\n"
+ msg
+ (T.preorder tree node)
+ StateSet.print config.sat
+ StateSet.print config.unsat
+ (Ata.TransList.print ~sep:"\n") config.todo i
+
let get_trans cache2 auto tag states =
let trs =
- let top_down node run =
+ let top_down run =
let tree = run.tree in
let auto = run.auto in
let status = run.status in
if c == dummy_status then
(* first time we visit the node *)
NodeStatus.make
- { c.NodeStatus.node with
+ { sat = StateSet.empty;
+ unsat = Ata.get_starting_states auto;
todo = get_trans cache2 auto tag (Ata.get_states auto);
summary = NodeSummary.make
(node == T.first_child tree parent) (* is_left *)
unstable_self
end
in
- run.redo <- loop node;
+ run.redo <- loop (T.root tree);
run.pass <- run.pass + 1
(*
in
loop (T.root tree) []
+ let prepare_run run list =
+ let tree = run.tree in
+ let auto = run.auto in
+ let status = run.status in
+ let cache2 = run.cache2 in
+ List.iter (fun node ->
+ let parent = T.parent tree node in
+ let fc = T.first_child tree node in
+ let ns = T.next_sibling tree node in
+ let tag = T.tag tree node in
+
+ let status0 =
+ NodeStatus.make
+ { sat = Ata.get_starting_states auto;
+ unsat = StateSet.empty;
+ todo = get_trans cache2 auto tag (Ata.get_states auto);
+ summary = NodeSummary.make
+ (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 *)
+ }
+ in
+ let node_id = T.preorder tree node in
+ status.(node_id) <- status0) list
+
- let eval auto tree node =
+
+ let eval auto tree nodes =
let run = make auto tree in
- while run.redo do top_down node run done;
+ prepare_run run nodes;
+ while run.redo do
+ top_down run;
+ done;
get_results run
end