X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=ata.ml;fp=ata.ml;h=9eb531188d21ce58d57ab4e5df74fb2ac5069679;hb=6a7025fee3c050eff58baa536a14d80baf5c1b87;hp=7949921d2f54d98e13850b842e0a2e75e1b90d56;hpb=3445f7f08f15fe41e0d1bfaaabaacf60cdc10b61;p=SXSI%2Fxpathcomp.git diff --git a/ata.ml b/ata.ml index 7949921..9eb5311 100644 --- a/ata.ml +++ b/ata.ml @@ -194,16 +194,18 @@ end module Transition = struct - type node = State.t*bool*Formula.t*bool + type node = State.t*TagSet.t*bool*Formula.t*bool include Hcons.Make(struct type t = node - let hash (s,m,f,b) = HASHINT4(s,Formula.uid f,vb m,vb b) - let equal (s,b,f,m) (s',b',f',m') = - s == s' && b==b' && m==m' && Formula.equal f f' + let hash (s,ts,m,f,b) = HASHINT5(s,TagSet.uid ts,Formula.uid f,vb m,vb b) + let equal (s,ts,b,f,m) (s',ts',b',f',m') = + s == s' && ts == ts' && b==b' && m==m' && f == f' end) - let print ppf f = let (st,mark,form,b) = node f in - Format.fprintf ppf "%i %s" st (if mark then "⇒" else "→"); + let print ppf f = let (st,ts,mark,form,b) = node f in + Format.fprintf ppf "(%i, " st; + TagSet.print ppf ts; + Format.fprintf ppf ") %s" (if mark then "⇒" else "→"); Formula.print ppf form; Format.fprintf ppf "%s%!" (if b then " (b)" else "") @@ -212,7 +214,7 @@ module Transition = struct let ( ?< ) x = x let ( >< ) state (l,mark) = state,(l,mark,false) let ( ><@ ) state (l,mark) = state,(l,mark,true) - let ( >=> ) (state,(label,mark,bur)) form = (state,label,(make (state,mark,form,bur))) + let ( >=> ) (state,(label,mark,bur)) form = (state,label,(make (state,label,mark,form,bur))) end end @@ -254,7 +256,7 @@ let dump ppf a = if y-x == 0 then TagSet.compare tsy tsx else y-x) l in let maxh,maxt,l_print = List.fold_left ( - fun (maxh,maxt,l) ((ts,q),(_,b,f,_)) -> + fun (maxh,maxt,l) ((ts,q),(_,_,b,f,_)) -> let s = if TagSet.is_finite ts then "{" ^ (TagSet.fold (fun t a -> a ^ " '" ^ (Tag.to_string t)^"'") ts "") ^" }" @@ -327,29 +329,31 @@ let eval_form_bool = module FTable = Hashtbl.Make( struct - type t = Formlist.t*StateSet.t*StateSet.t - let equal (f1,s1,t1) (f2,s2,t2) = - f1 == f2 && s1 == s2 && t1 == t2;; - let hash (f,s,t) = HASHINT3(Formlist.uid f ,StateSet.uid s,StateSet.uid t);; + type t = Tag.t*Formlist.t*StateSet.t*StateSet.t + let equal (tg1,f1,s1,t1) (tg2,f2,s2,t2) = + tg1 == tg2 && f1 == f2 && s1 == s2 && t1 == t2;; + let hash (tg,f,s,t) = HASHINT4(tg,Formlist.uid f ,StateSet.uid s,StateSet.uid t);; end) let h_f = FTable.create BIG_H_SIZE -let eval_formlist s1 s2 fl = +let eval_formlist tag s1 s2 fl = let rec loop fl = try - FTable.find h_f (fl,s1,s2) + FTable.find h_f (tag,fl,s1,s2) with | Not_found -> match Formlist.node fl with | Formlist.Cons(f,fll) -> - let q,mark,f,_ = Transition.node f in - let b,b1,b2 = eval_form_bool f s1 s2 in + let q,ts,mark,f,_ = Transition.node f in + let b,b1,b2 = + if TagSet.mem tag ts then eval_form_bool f s1 s2 else (false,false,false) + in let (s,(b',b1',b2',amark)) as res = loop fll in let r = if b then (StateSet.add q s, (b, b1'||b1,b2'||b2,mark||amark)) else res - in FTable.add h_f (fl,s1,s2) r;r + in FTable.add h_f (tag,fl,s1,s2) r;r | Formlist.Nil -> StateSet.empty,(false,false,false,false) in loop fl @@ -358,7 +362,7 @@ let tags_of_state a q = (fun p l acc -> if p == q then List.fold_left (fun acc (ts,t) -> - let _,_,_,aux = Transition.node t in + let _,_,_,_,aux = Transition.node t in if aux then acc else TagSet.cup ts acc) acc l @@ -559,7 +563,7 @@ END (List.fold_left (fun acc (ts,f) -> - let _,_,_,bur = Transition.node f in + let _,_,_,_,bur = Transition.node f in if bur then acc else TagSet.cup acc ts) acc l) else acc ) a.trans TagSet.empty @@ -567,7 +571,7 @@ END let is_rec a s access = List.exists - (fun (_,t) -> let _,_,f,_ = Transition.node t in + (fun (_,t) -> let _,_,_,f,_ = Transition.node t in StateSet.mem s ((fun (_,_,x) -> x) (access (Formula.st f)))) (Hashtbl.find a.trans s) @@ -617,13 +621,13 @@ END let tag = Ptset.Int.choose ll in (`TAG(tag),mk_app_fun f_tn tag (Tag.to_string tag)) else - (`ANY,mk_app_fun f_sn ll (string_of_ts ll)) + (`MANY(ll),mk_app_fun f_sn ll (string_of_ts ll)) else if Ptset.Int.is_empty ll then if Ptset.Int.is_singleton cl then let tag = Ptset.Int.choose cl in (`TAG(tag),mk_app_fun f_t1 tag (Tag.to_string tag)) else - (`ANY,mk_app_fun f_s1 cl (string_of_ts cl)) + (`MANY(cl),mk_app_fun f_s1 cl (string_of_ts cl)) else (`ANY,mk_app_fun2 f_s1n cl ll ((string_of_ts cl) ^ " " ^ (string_of_ts ll))) @@ -713,15 +717,16 @@ END module Fold2Res = struct type 'a t = 'a SListTable.t SListTable.t FllTable.t + let create n = Array.init 10000 (fun _ -> FllTable.create n) - let create n = FllTable.create n - - let find hf fl s1 s2 = + let find h tag fl s1 s2 = + let hf = h.(tag) in let hs1 = FllTable.find hf fl in let hs2 = SListTable.find hs1 s1 in SListTable.find hs2 s2 - let add hf fl s1 s2 data = + let add h tag fl s1 s2 data = + let hf = h.(tag) in let hs1 = try FllTable.find hf fl with | Not_found -> @@ -738,22 +743,22 @@ END SListTable.add hs2 s2 data end - let h_fold2 = Fold2Res.create BIG_H_SIZE + let h_fold2 = Fold2Res.create SMALL_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 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 fll sl1 sl2 in + 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 -> + 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, @@ -763,14 +768,14 @@ END | Formlistlist.Cons(fl,fll), SList.Cons(s1,ll1), SList.Cons(s2,ll2) -> - let r',((b,_,_,_) as flags) = eval_formlist s1 s2 fl in + let r',((b,_,_,_) as flags) = eval_formlist tag 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); + 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; @@ -801,7 +806,7 @@ END (ts,t) -> if (TagSet.mem tag ts) then - let _,_,f,_ = Transition.node t in + 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, @@ -825,10 +830,6 @@ END 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 _ = 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 d_f and n_kind,next = if noright then (`NIL, fun _ _ -> Tree.nil ) else choose_jump_next tree d_n in @@ -836,57 +837,71 @@ END let cont = match f_kind,n_kind with | `NIL,`NIL -> - (fun t _ -> eval_fold2_slist fl_list t empty_res empty_res) + (fun t _ -> eval_fold2_slist fl_list t (Tree.tag tree 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 )) + |`TAG(tag') -> + (fun t _ -> eval_fold2_slist fl_list t (Tree.tag tree t) empty_res + (loop_tag tag' (first t) llist t )) | `ANY -> - (fun t _ -> eval_fold2_slist fl_list t empty_res + (fun t _ -> eval_fold2_slist fl_list t (Tree.tag tree t) empty_res (loop (first t) llist t )) | _ -> assert false) | `NIL,_ -> ( match n_kind with - |`TAG(tag) -> - if SList.equal rlist slist then + |`TAG(tag') -> + if SList.equal rlist slist && tag == tag' then let rec loop t ctx = - if t == Tree.nil then empty_res - else + if t == Tree.nil then empty_res else let res2 = loop (next t ctx) ctx in - eval_fold2_slist fl_list t res2 empty_res + eval_fold2_slist fl_list t tag res2 empty_res in loop else - (fun t ctx -> eval_fold2_slist fl_list 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_tag tag' (next t ctx) rlist ctx ) empty_res) | `ANY -> - (fun t ctx -> eval_fold2_slist fl_list t + (fun t ctx -> eval_fold2_slist fl_list t (Tree.tag tree t) (loop (next t ctx) rlist ctx ) empty_res) | _ -> assert false) | `TAG(tag1),`TAG(tag2) -> (fun t ctx -> - eval_fold2_slist fl_list t + 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 -> + + | `TAG(tag'),`ANY -> (fun t ctx -> - eval_fold2_slist fl_list t + eval_fold2_slist fl_list t (Tree.tag tree t) (loop (next t ctx) rlist ctx ) - (loop_tag tag (first t) llist t )) + (loop_tag tag' (first t) llist t )) - | `ANY,`TAG(tag) -> + | `ANY,`TAG(tag') -> (fun t ctx -> - eval_fold2_slist fl_list t - (loop_tag tag (next t ctx) rlist 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 + 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 )) | _ -> assert false @@ -975,7 +990,8 @@ END let h_fold = Hashtbl.create 511 - let fold_f_conf t slist fl_list conf dir= + 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 @@ -986,8 +1002,8 @@ END Hashtbl.find h_fold key with Not_found -> let res = - if dir then eval_formlist s Ptset.Int.empty formlist - else eval_formlist Ptset.Int.empty s formlist + 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 if rb && ((dir&&rb1)|| ((not dir) && rb2)) @@ -1057,7 +1073,7 @@ END let slist = Configuration.Ptss.fold (fun e a -> SList.cons e a) conf.Configuration.sets SList.nil in let fl_list = get_up_trans slist ptag a parent in let slist = SList.rev (slist) in - let newconf = fold_f_conf parent slist fl_list conf dir in + let newconf = fold_f_conf tree parent slist fl_list conf dir in let accu,newconf = Configuration.IMap.fold (fun s res (ar,nc) -> if Ptset.Int.intersect s init then ( RS.concat res ar ,nc) @@ -1100,7 +1116,7 @@ END in let init = List.fold_left (fun acc (_,t) -> - let _,_,f,_ = Transition.node t in + let _,_,_,f,_ = Transition.node t in let _,_,l = fst ( Formula.st f ) in StateSet.union acc l) StateSet.empty trlist