+ let add t k1 k2 k3 k4 v =
+ let key = hash k1 k2 k3 k4 in
+ let i = find_slot t key in
+ t.(i)<- { key = key; obj = (Obj.repr v) }
+
+ end
+
+ let h_fold2 = Fold2Res.create 10000
+
+ let top_down ?(noright=false) a tree t slist ctx slot_size =
+ let pempty = empty_size slot_size in
+ let rempty = Array.make slot_size RS.empty in
+ (* evaluation starts from the right so we put sl1,res1 at the end *)
+ let eval_fold2_slist fll t tag (sl2,res2) (sl1,res1) =
+ let res = Array.copy rempty in
+ try
+ let r,b,btab = Fold2Res.find h_fold2 tag fll sl1 sl2 in
+ if b then for i=0 to slot_size - 1 do
+ res.(i) <- RS.merge btab.(i) t res1.(i) res2.(i);
+ done;
+ r,res
+ with
+ Not_found ->
+ begin
+ let btab = Array.make slot_size NO in
+ let rec fold l1 l2 fll i aq ab =
+ match fll.Formlistlist.Node.node,
+ l1.SList.Node.node,
+ l2.SList.Node.node
+ with
+ | Formlistlist.Cons(fl,fll),
+ SList.Cons(s1,ll1),
+ SList.Cons(s2,ll2) ->
+ let r',conf = eval_formlist tag s1 s2 fl in
+ let _ = btab.(i) <- conf
+ in
+ fold ll1 ll2 fll (i+1) (SList.cons r' aq) ((conf!=NO)||ab)
+ | _ -> aq,ab
+ in
+ let r,b = fold sl1 sl2 fll 0 SList.nil false in
+ Fold2Res.add h_fold2 tag fll sl1 sl2 (r,b,btab);
+ if b then for i=0 to slot_size - 1 do
+ res.(i) <- RS.merge btab.(i) t res1.(i) res2.(i);
+ done;
+ r,res;
+ end
+ in
+
+ let null_result = (pempty,Array.copy rempty) in
+ let rec loop t slist ctx =
+ if t == Tree.nil then null_result else get_trans t slist (Tree.tag tree t) ctx
+ and loop_tag tag t slist ctx =
+ if t == Tree.nil then null_result else get_trans t slist tag ctx
+ and loop_no_right t slist ctx =
+ if t == Tree.nil then null_result else get_trans ~noright:true t slist (Tree.tag tree t) ctx
+ and get_trans ?(noright=false) t slist tag ctx =
+ let cont =
+ try
+ TransCache.find td_trans tag slist
+ with
+ | Not_found ->
+ let fl_list,llist,rlist,ca,da,sa,fa =
+ SList.fold
+ (fun set (fll_acc,lllacc,rllacc,ca,da,sa,fa) -> (* For each set *)
+ let fl,ll,rr,ca,da,sa,fa =
+ StateSet.fold
+ (fun q acc ->
+ List.fold_left
+ (fun ((fl_acc,ll_acc,rl_acc,c_acc,d_acc,s_acc,f_acc) as acc)
+ (ts,t) ->
+ if (TagSet.mem tag ts)
+ then
+ let _,_,_,f,_ = t.Transition.node in
+ let (child,desc,below),(sibl,foll,after) = Formula.st f in
+ (Formlist.cons t fl_acc,
+ StateSet.union ll_acc below,
+ StateSet.union rl_acc after,
+ StateSet.union child c_acc,
+ StateSet.union desc d_acc,
+ StateSet.union sibl s_acc,
+ StateSet.union foll f_acc)
+ else acc ) acc (
+ try Hashtbl.find a.trans q
+ with
+ Not_found -> Printf.eprintf "Looking for state %i, doesn't exist!!!\n%!"
+ q;[]
+ )
+
+ ) set (Formlist.nil,StateSet.empty,StateSet.empty,ca,da,sa,fa)
+ in (Formlistlist.cons fl fll_acc), (SList.cons ll lllacc), (SList.cons rr rllacc),ca,da,sa,fa)
+ slist (Formlistlist.nil,SList.nil,SList.nil,StateSet.empty,StateSet.empty,StateSet.empty,StateSet.empty)
+ in
+ (* Logic to chose the first and next function *)
+ let tags_child,tags_below,tags_siblings,tags_after = Tree.tags tree tag in
+ let d_f = Algebra.decide a tags_child tags_below (StateSet.union ca da) true in
+ let d_n = Algebra.decide a tags_siblings tags_after (StateSet.union sa fa) false in
+ let f_kind,first = choose_jump_down tree d_f
+ and n_kind,next = if noright then (`NIL, fun _ _ -> Tree.nil )
+ else choose_jump_next tree d_n in
+ (*let f_kind,first = `ANY, Tree.first_child tree
+ and n_kind,next = `ANY, Tree.next_sibling_below tree
+ in *)
+ let empty_res = null_result in
+ let cont =
+ match f_kind,n_kind with
+ | `NIL,`NIL ->
+ (fun t _ -> eval_fold2_slist fl_list t (Tree.tag tree t) empty_res empty_res)
+ | _,`NIL -> (
+ match f_kind with
+ (*|`TAG(tag') ->
+ let default = fun t _ -> eval_fold2_slist fl_list t (Tree.tag tree t) empty_res
+ (loop_tag tag' (first t) llist t )
+ in default (*
+ let cf = SList.hd llist in
+ if (slot_size == 1) && StateSet.is_singleton cf
+ then
+ let s = StateSet.choose cf in
+ if (Algebra.is_rec a s fst) && (Algebra.is_rec a s snd)
+ && (Algebra.is_final_marking a s)
+ then
+ RS.mk_quick_tag_loop default llist 1 tree tag'
+ else default
+ else default *) *)
+ | _ ->
+ (fun t _ -> eval_fold2_slist fl_list t (Tree.tag tree t) empty_res
+ (loop (first t) llist t ))
+ )
+ | `NIL,_ -> (
+ match n_kind with
+ |`TAG(tag') ->
+ if SList.equal rlist slist && tag == tag' then
+ let rec loop t ctx =
+ if t == Tree.nil then empty_res else
+ let res2 = loop (next t ctx) ctx in
+ eval_fold2_slist fl_list t tag res2 empty_res
+ in loop
+ else
+ (fun t ctx -> eval_fold2_slist fl_list t (Tree.tag tree t)
+ (loop_tag tag' (next t ctx) rlist ctx ) empty_res)
+
+ | _ ->
+ (fun t ctx -> eval_fold2_slist fl_list t (Tree.tag tree t)
+ (loop (next t ctx) rlist ctx ) empty_res)
+ )
+
+ | `TAG(tag1),`TAG(tag2) ->
+ (fun t ctx ->
+ eval_fold2_slist fl_list t (Tree.tag tree t)
+ (loop_tag tag2 (next t ctx) rlist ctx )
+ (loop_tag tag1 (first t) llist t ))
+
+ | `TAG(tag'),`ANY ->
+ (fun t ctx ->
+ eval_fold2_slist fl_list t (Tree.tag tree t)
+ (loop (next t ctx) rlist ctx )
+ (loop_tag tag' (first t) llist t ))
+
+ | `ANY,`TAG(tag') ->
+ (fun t ctx ->
+ eval_fold2_slist fl_list t (Tree.tag tree t)
+ (loop_tag tag' (next t ctx) rlist ctx )
+ (loop (first t) llist t ))
+
+ | `ANY,`ANY ->
+ (*if SList.equal slist rlist && SList.equal slist llist
+ then
+ let rec loop t ctx =
+ if t == Tree.nil then empty_res else
+ let r1 = loop (first t) t
+ and r2 = loop (next t ctx) ctx
+ in
+ eval_fold2_slist fl_list t (Tree.tag tree t) r2 r1
+ in loop
+ else *)
+ (fun t ctx ->
+ eval_fold2_slist fl_list t (Tree.tag tree t)
+ (loop (next t ctx) rlist ctx )
+ (loop (first t) llist t ))
+ | _,_ ->
+ (fun t ctx ->
+ eval_fold2_slist fl_list t (Tree.tag tree t)
+ (loop (next t ctx) rlist ctx )
+ (loop (first t) llist t ))
+
+ in
+ let cont = D_IF_( (fun t ctx ->
+ let a,b = cont t ctx in
+ register_trace tree t (slist,a,fl_list,first,next,ctx);
+ (a,b)
+ ) ,cont)
+ in
+ ( TransCache.add td_trans tag slist cont ; cont)
+ in cont t ctx
+
+ in
+ (if noright then loop_no_right else loop) t slist ctx
+
+ let run_top_down a tree =
+ let init = SList.cons a.init SList.nil in
+ let _,res = top_down a tree Tree.root init Tree.root 1
+ in
+ D_IGNORE_(
+ output_trace a tree "trace.html"
+ (RS.fold (fun t a -> IntSet.add (Tree.id tree t) a) res.(0) IntSet.empty),
+ res.(0))
+ ;;
+
+ module Configuration =
+ struct
+ module Ptss = Set.Make(StateSet)
+ module IMap = Map.Make(StateSet)
+ type t = { hash : int;
+ sets : Ptss.t;
+ results : RS.t IMap.t }
+ let empty = { hash = 0;
+ sets = Ptss.empty;
+ results = IMap.empty;
+ }
+ let is_empty c = Ptss.is_empty c.sets
+ let add c s r =
+ if Ptss.mem s c.sets then
+ { c with results = IMap.add s (RS.concat r (IMap.find s c.results)) c.results}
+ else
+ { hash = HASHINT2(c.hash,Uid.to_int (Ptset.Int.uid s));
+ sets = Ptss.add s c.sets;
+ results = IMap.add s r c.results
+ }
+
+ let pr fmt c = Format.fprintf fmt "{";
+ Ptss.iter (fun s -> StateSet.print fmt s;
+ Format.fprintf fmt " ") c.sets;
+ Format.fprintf fmt "}\n%!";
+ IMap.iter (fun k d ->
+ StateSet.print fmt k;
+ Format.fprintf fmt "-> %i\n" (RS.length d)) c.results;
+ Format.fprintf fmt "\n%!"
+
+ let merge c1 c2 =
+ let acc1 =
+ IMap.fold
+ ( fun s r acc ->
+ IMap.add s
+ (try
+ RS.concat r (IMap.find s acc)
+ with
+ | Not_found -> r) acc) c1.results IMap.empty
+ in
+ let imap =
+ IMap.fold (fun s r acc ->
+ IMap.add s
+ (try
+ RS.concat r (IMap.find s acc)
+ with
+ | Not_found -> r) acc) c2.results acc1
+ in
+ let h,s =
+ Ptss.fold
+ (fun s (ah,ass) -> (HASHINT2(ah, Uid.to_int (Ptset.Int.uid s)),
+ Ptss.add s ass))
+ (Ptss.union c1.sets c2.sets) (0,Ptss.empty)
+ in
+ { hash = h;
+ sets =s;
+ results = imap }
+
+ end
+
+ let h_fold = Hashtbl.create 511
+
+ let fold_f_conf tree t slist fl_list conf dir=
+ let tag = Tree.tag tree t in
+ let rec loop sl fl acc =
+ match SList.node sl,fl with
+ |SList.Nil,[] -> acc
+ |SList.Cons(s,sll), formlist::fll ->
+ let r',mcnf =
+ let key = SList.hash sl,Formlist.hash formlist,dir in
+ try
+ Hashtbl.find h_fold key
+ with
+ Not_found -> let res =
+ if dir then eval_formlist tag s Ptset.Int.empty formlist
+ else eval_formlist tag Ptset.Int.empty s formlist
+ in (Hashtbl.add h_fold key res;res)
+ in
+ let (rb,rb1,rb2,mark) = bool_of_merge mcnf in
+ if rb && ((dir&&rb1)|| ((not dir) && rb2))
+ then
+ let acc =
+ let old_r =
+ try Configuration.IMap.find s conf.Configuration.results
+ with Not_found -> RS.empty
+ in
+ Configuration.add acc r' (if mark then RS.cons t old_r else old_r)
+ in
+ loop sll fll acc
+ else loop sll fll acc
+ | _ -> assert false
+ in
+ loop slist fl_list Configuration.empty
+
+ let h_trans = Hashtbl.create 4096
+
+ let get_up_trans slist ptag a tree =
+ let key = (HASHINT2(Uid.to_int slist.SList.Node.id ,ptag)) in
+ try
+ Hashtbl.find h_trans key
+ with
+ | Not_found ->
+ let f_list =
+ Hashtbl.fold (fun q l acc ->
+ List.fold_left (fun fl_acc (ts,t) ->
+ if TagSet.mem ptag ts then Formlist.cons t fl_acc
+ else fl_acc)
+
+ acc l)
+ a.trans Formlist.nil
+ in
+ let res = SList.fold (fun _ acc -> f_list::acc) slist []
+ in
+ (Hashtbl.add h_trans key res;res)
+
+
+
+ let h_tdconf = Hashtbl.create 511
+ let rec bottom_up a tree t conf next jump_fun root dotd init accu =
+ if (not dotd) && (Configuration.is_empty conf ) then
+ accu,conf,next
+ else
+
+ let below_right = Tree.is_below_right tree t next in