- run.pass <- run.pass + 2
-
-
- let get_results run =
- let cache = IFHTML((List.hd run.sat), run.sat) in
- let auto = run.auto in
- let tree = run.tree in
- let sel_states = Ata.get_selecting_states auto in
- let res = ref (L.create ()) in
- let rec loop node =
- if node != T.nil then begin
- if StateSet.intersect sel_states cache.(T.preorder tree node) then
- res := L.add node !res;
- loop (T.first_child tree node);
- loop (T.next_sibling tree node)
- end
- in
- loop (T.root tree);
- !res
-
-
- let get_full_results run =
- let cache = IFHTML((List.hd run.sat), run.sat) 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 = 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
- let rec loop node =
- if node != T.nil then begin
- 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) (L.add node res)
- )
- cache.(T.preorder tree node);
- loop (T.first_child tree node);
- loop (T.next_sibling tree node)
- end
- 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) [])
-
+ run.pass <- run.pass + 2;
+ run.stats.pass <- run.stats.pass + 1;
+ run.stats.nodes_per_run <- !num_visited :: run.stats.nodes_per_run
+
+
+
+ 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) [])