X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=ata.ml;h=0132b36cb04b534f5b0d378c1187385c868ffc54;hb=479afaf5e67e28ef73c0126e95ca8badec3392aa;hp=ebc74a53d8df0b2801502bc723cfe3f7fe89d409;hpb=b8aa8e7f1036cf00d0fadc75ccbe0264bae6c1b2;p=SXSI%2Fxpathcomp.git diff --git a/ata.ml b/ata.ml index ebc74a5..0132b36 100644 --- a/ata.ml +++ b/ata.ml @@ -1,8 +1,6 @@ INCLUDE "debug.ml" INCLUDE "utils.ml" - - type jump_kind = [ `TAG of Tag.t | `CONTAINS of string | `NOTHING ] (* Todo : move elsewhere *) @@ -67,8 +65,8 @@ struct match f.pos with | False -> 0 | True -> 1 - | Or (f1,f2) -> HASHINT3(PRIME2,HNode.hash f1,HNode.hash f2) - | And (f1,f2) -> HASHINT3(PRIME3,HNode.hash f1,HNode.hash f2) + | Or (f1,f2) -> HASHINT3(PRIME2,HNode.uid f1,HNode.uid f2) + | And (f1,f2) -> HASHINT3(PRIME3,HNode.uid f1,HNode.uid f2) | Atom(d,p,s) -> HASHINT4(PRIME4,hash_const_variant d,vb p,s) end @@ -230,7 +228,7 @@ module SetTagKey = struct type t = Ptset.Int.t*Tag.t let equal (s1,t1) (s2,t2) = (t1 == t2) && Ptset.Int.equal s1 s2 - let hash (s,t) = HASHINT2(Ptset.Int.hash s,Tag.hash t) + let hash (s,t) = HASHINT2(Ptset.Int.uid s, t) end module TransTable = Hashtbl @@ -288,17 +286,18 @@ let dump ppf a = Format.fprintf ppf "%s\n%!" (String.make (maxt+maxh+3) '_') +module FormTable = Hashtbl.Make(struct + type t = Formula.t*StateSet.t*StateSet.t + let equal (f1,s1,t1) (f2,s2,t2) = + Formula.equal f1 f2 && StateSet.equal s1 s2 && StateSet.equal t1 t2 + let hash (f,s,t) = + HASHINT3(Formula.uid f ,StateSet.uid s,StateSet.uid t) + end) +(* Too slow module MemoForm = Memoizer.Make( - Hashtbl.Make(struct - type t = Formula.t*(StateSet.t*StateSet.t) - let equal (f1,(s1,t1)) (f2,(s2,t2)) = - Formula.equal f1 f2 && StateSet.equal s1 s2 && StateSet.equal t1 t2 - let hash (f,(s,t)) = - HASHINT3(Formula.uid f ,StateSet.uid s,StateSet.uid t) - end)) - -module F = Formula +module F = Formula +(* let eval_form_bool = MemoForm.make_rec( fun eval (f, ((s1,s2) as sets)) -> @@ -331,20 +330,60 @@ let eval_form_bool = else (false,false,false) ) -let eval_form_bool f s1 s2 = eval_form_bool (f,(s1,s2)) - +*) *) +module F = Formula -module MemoFormlist = Memoizer.Make( - Hashtbl.Make(struct - type t = Formlist.t*(StateSet.t*StateSet.t) - let equal (f1,(s1,t1)) (f2,(s2,t2)) = - Formlist.equal f1 f2 && StateSet.equal s1 s2 && StateSet.equal t1 t2 - let hash (f,(s,t)) = - HASHINT3(Formlist.uid f ,StateSet.uid s,StateSet.uid t) - end)) +let eval_form_bool = + let h_f = FormTable.create BIG_H_SIZE in + fun f s1 s2 -> + let rec loop f = + match F.expr f with + | F.True -> true,true,true + | F.False -> false,false,false + | F.Atom((`Left|`LLeft),b,q) -> + if b == (StateSet.mem q s1) + then (true,true,false) + else false,false,false + | F.Atom(_,b,q) -> + if b == (StateSet.mem q s2) + then (true,false,true) + else false,false,false + | f' -> + try FormTable.find h_f (f,s1,s2) + with Not_found -> let r = + match f' with + | F.Or(f1,f2) -> + let b1,rl1,rr1 = loop f1 + in + if b1 && rl1 && rr1 then (true,true,true) else + let b2,rl2,rr2 = loop f2 in + let rl1,rr1 = if b1 then rl1,rr1 else false,false + and rl2,rr2 = if b2 then rl2,rr2 else false,false + in (b1 || b2, rl1||rl2,rr1||rr2) + + | F.And(f1,f2) -> + let b1,rl1,rr1 = loop f1 in + if b1 && rl1 && rr1 then (true,true,true) else + if b1 then + let b2,rl2,rr2 = loop f2 in + if b2 then (true,rl1||rl2,rr1||rr2) else (false,false,false) + else (false,false,false) + | _ -> assert false + in FormTable.add h_f (f,s1,s2) r;r + in loop f + +module FTable = Hashtbl.Make( + struct + type t = Formlist.t*StateSet.t*StateSet.t + let equal (f1,s1,t1) (f2,s2,t2) = + Formlist.equal f1 f2 && StateSet.equal s1 s2 && StateSet.equal t1 t2;; + let hash (f,s,t) = HASHINT3(Formlist.uid f ,StateSet.uid s,StateSet.uid t);; + end) + +(* +module MemoFormlist = Memoizer.Make(FTable) - - + Too slow let eval_formlist = MemoFormlist.make_rec ( fun eval (fl,((s1,s2)as sets)) -> match Formlist.node fl with @@ -355,10 +394,29 @@ module MemoFormlist = Memoizer.Make( let s,b',b1',b2',amark = eval (fll,sets) in if b then (StateSet.add q s, b, b1'||b1,b2'||b2,mark||amark) else s,b',b1',b2',amark ) - - let eval_formlist ?(memo=true) s1 s2 fl = - eval_formlist (fl,(s1,s2)) - +*) + + + + let eval_formlist = + let h_f = FTable.create BIG_H_SIZE in + fun s1 s2 fl -> + let rec loop fl = + let key = (fl,s1,s2) in + try + FTable.find h_f key + with + | Not_found -> + match Formlist.node fl with + | Formlist.Nil -> StateSet.empty,false,false,false,false + | Formlist.Cons(f,fll) -> + let q,mark,f,_ = Transition.node f in + let b,b1,b2 = eval_form_bool f s1 s2 in + let s,b',b1',b2',amark = loop fll in + let r = if b then (StateSet.add q s, b, b1'||b1,b2'||b2,mark||amark) + else s,b',b1',b2',amark + in FTable.add h_f key r;r + in loop fl let tags_of_state a q = Hashtbl.fold @@ -612,7 +670,7 @@ END if Tree.is_nil t then null_result() else let tag = Tree.tag t in - let fl_list,llist,rlist,first,next = get_trans slist tag a t in + let fl_list,llist,_,first,next = get_trans slist tag a t in let sl1,res1 = loop (first t) llist t in let sl2,res2 = null_result() in let res = eval_fold2_slist fl_list sl1 sl2 res1 res2 t @@ -650,7 +708,7 @@ END 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.hash s); + { hash = HASHINT2(c.hash,Ptset.Int.uid s); sets = Ptss.add s c.sets; results = IMap.add s r c.results } @@ -682,7 +740,7 @@ END in let h,s = Ptss.fold - (fun s (ah,ass) -> (HASHINT2(ah,Ptset.Int.hash s), + (fun s (ah,ass) -> (HASHINT2(ah,Ptset.Int.uid s), Ptss.add s ass)) (Ptss.union c1.sets c2.sets) (0,Ptss.empty) in @@ -727,7 +785,7 @@ END let h_trans = Hashtbl.create 4096 let get_up_trans slist ptag a tree = - let key = (HASHINT2(SList.hash slist,Tag.hash ptag)) in + let key = (HASHINT2(SList.uid slist,ptag)) in try Hashtbl.find h_trans key with