- let inter_text a b =
- match b with
- | `Positive s -> let r = Ptset.inter a s in (r,Ptset.mem Tag.pcdata r, true)
- | `Negative s -> (Ptset.empty, not (Ptset.mem Tag.pcdata s), false)
-
- let mk_nil_ctx x _ = Tree.mk_nil x
- let next_sibling_ctx x _ = Tree.next_sibling x
- let r_ignore _ x = x
-
- let get_trans t a tag r =
- try
- HTagSet.find a.sigma (r,tag)
- with
- Not_found ->
- let fl,mark,_,_,accq =
- Ptset.fold (fun q (accf,accm,acchtrue,acchash,accq) ->
- let naccf,naccm,nacctrue,acchash =
- merge_trans t a tag q (accf,accm,acchtrue,acchash )
- in
- (* if is_false naccf then (naccf,naccm,nacctrue,accq)
- else *) (naccf,naccm,nacctrue,acchash,Ptset.add q accq)
- )
- r (Nil,false,false,17,Ptset.empty)
- in
- let (ls,lls,llls),(rs,rrs,rrrs) =
- form_list_fold_left (fun ((a1,b1,c1),(a2,b2,c2)) _ f _ ->
- let (x1,y1,z1),(x2,y2,z2) = f.st in
- ((Ptset.union x1 a1),(Ptset.union y1 b1),(Ptset.union c1 z1)),
- ((Ptset.union x2 a2),(Ptset.union y2 b2),(Ptset.union c2 z2)))
- ((Ptset.empty,Ptset.empty,Ptset.empty),
- (Ptset.empty,Ptset.empty,Ptset.empty))
- fl
- in
- let tb,ta =
- Tree.tags t tag
- in
- let tl,htlt,lfin = inter_text tb (tags a ls)
- and tll,htllt,llfin = inter_text tb (tags a lls)
- and tr,htrt,rfin = inter_text ta (tags a rs)
- and trr,htrrt,rrfin = inter_text ta (tags a rrs)
- in(*
- let _ =
- Format.fprintf Format.err_formatter "Tag %s, right_states " (Tag.to_string tag);
- pr_st Format.err_formatter (Ptset.elements rs);
- Format.fprintf Format.err_formatter " tags = ";
- Ptset.iter (fun t -> Format.fprintf Format.err_formatter "%s "
- (Tag.to_string t)) tr;
- Format.fprintf Format.err_formatter ", next_states ";
- pr_st Format.err_formatter (Ptset.elements rrs);
- Format.fprintf Format.err_formatter " tags = ";
- Ptset.iter (fun t -> Format.fprintf Format.err_formatter "%s "
- (Tag.to_string t)) trr;
- Format.fprintf Format.err_formatter "\n%!";
+ let empty_size n =
+ let rec loop acc = function 0 -> acc
+ | n -> loop (SList.cons StateSet.empty acc) (n-1)
+ in loop SList.nil n
+
+
+ module Fold2Res = Hashtbl.Make(struct
+ type t = Formlistlist.t*SList.t*SList.t
+ let hash (f,s,t) = HASHINT3(f.Formlistlist.Node.id,
+ s.SList.Node.id,
+ t.SList.Node.id)
+ let equal (a,b,c) (d,e,f) = a==d && b == e && c == f
+ end)
+
+ let h_fold2 = Fold2Res.create BIG_H_SIZE
+
+ 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 (sl2,res2) (sl1,res1) =
+ let res = Array.copy rempty in
+ try
+ let r,b,btab = Fold2Res.find h_fold2 (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 ->
+ let btab = Array.make slot_size (false,false,false,false) 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',((b,_,_,_) as flags) = eval_formlist s1 s2 fl in
+ let _ = btab.(i) <- flags
+ in
+ fold ll1 ll2 fll (i+1) (SList.cons r' aq) (b||ab)
+ | _ -> aq,ab
+ in
+ let r,b = fold sl1 sl2 fll 0 SList.nil false in
+ Fold2Res.add h_fold2 (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
+ 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
+ CachedTransTable.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,_ = Transition.node t 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_below,_,tags_after = Tree.tags tree tag in
+(* let _ = Printf.eprintf "Tags below %s are : \n" (Tag.to_string tag) in
+ let _ = Ptset.Int.iter (fun i -> Printf.eprintf "%s " (Tag.to_string i)) tags_below in
+ let _ = Printf.eprintf "\n%!" in *)
+ let tags_below = Ptset.Int.remove tag tags_below in
+ let f_kind,first = choose_jump_down tree tags_below ca da a
+ and n_kind,next = if noright then (`NIL, fun _ _ -> Tree.nil )
+ else choose_jump_next tree tags_after sa fa a 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 empty_res empty_res )
+ | _,`NIL -> (
+ match f_kind with
+ |`TAG(tag) ->
+ (fun t _ -> eval_fold2_slist fl_list t empty_res
+ (loop_tag tag (first t) llist t))
+ | `ANY ->
+ (fun t _ -> eval_fold2_slist fl_list t empty_res
+ (loop (first t) llist t))
+ | _ -> assert false)
+
+ | `NIL,_ -> (
+ match n_kind with
+ |`TAG(tag) ->
+ (fun t ctx -> eval_fold2_slist fl_list t
+ (loop_tag tag (next t ctx) rlist ctx) empty_res)
+
+ | `ANY ->
+ (fun t ctx -> eval_fold2_slist fl_list t
+ (loop (next t ctx) rlist ctx) empty_res)
+
+ | _ -> assert false)
+
+ | `TAG(tag1),`TAG(tag2) ->
+ (fun t ctx -> eval_fold2_slist fl_list 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
+ (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
+ (loop_tag tag (next t ctx) rlist ctx)
+ (loop (first t) llist t) )
+ | `ANY,`ANY ->
+ (fun t ctx ->
+ eval_fold2_slist fl_list t
+ (loop (next t ctx) rlist ctx)
+ (loop (first t) llist t) )
+ | _ -> assert false
+ 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
+ (CachedTransTable.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,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%!"