- loop (T.root tree) []
-
-
- let get_full_results run =
- let cache = run.status in
- let auto = run.auto in
- let tree = run.tree in
- let res_mapper = Hashtbl.create MED_H_SIZE in
- let () =
- StateSet.iter
- (fun q -> Hashtbl.add res_mapper q [])
- (Ata.get_selecting_states auto)
- in
- let dummy = [ T.nil ] in
- let res_mapper = Cache.N1.create dummy in
- let () =
- StateSet.iter
- (fun q -> Cache.N1.add res_mapper (q :> int) [])
- (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
- 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.(T.preorder tree node).NodeStatus.node.sat
- in
- loop (T.root tree);
- (StateSet.fold_right
- (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
- (Ata.get_selecting_states auto) [])
-
+ let _ = loop_td_and_bu (T.root tree) T.nil dummy_set in
+ run.pass <- run.pass + 2
+
+
+ let mk_update_result auto =
+ let sel_states = Ata.get_selecting_states auto in
+ let res = L.create () in
+ (fun prepend sat node ->
+ if StateSet.intersect sel_states sat then begin
+ if prepend then L.push_front node res else
+ L.push_back node res
+ end),
+ (fun () -> res)
+
+
+ let mk_update_full_result auto =
+ 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) (L.create()))
+ (Ata.get_selecting_states auto)
+ in
+ (fun prepend sat node ->
+ StateSet.iter
+ (fun q ->
+ let res = Cache.N1.find res_mapper (q :> int) in
+ if res != dummy then begin
+ if prepend then L.push_front node res
+ else L.push_back node res
+ end
+ ) sat),
+ (fun () ->
+ StateSet.fold_right
+ (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
+ (Ata.get_selecting_states auto) [])