(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 ->
- try
- let acc = Hashtbl.find res_mapper q in
- Hashtbl.replace res_mapper q (node::acc)
- with
- Not_found -> ())
+ 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);
List.rev (StateSet.fold
- (fun q acc -> (q, Hashtbl.find res_mapper q)::acc)
+ (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
(Ata.get_selecting_states auto) [])
let prepare_run run list =
if full then `Full (get_full_results run)
else `Normal (get_results run)
-
let full_eval auto tree nodes =
match eval true auto tree nodes with
`Full l -> l