X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=ata.ml;h=fc29e98fc96c916a05a8710a675a6d08a34a0231;hb=d4342e4bb9c853114de295567cd91ec86bb9e68f;hp=c12be8a5df11acc424faf78ecaee7e67c3b819b9;hpb=d04661689691b4587cfc45a35e98604fcdc2b878;p=SXSI%2Fxpathcomp.git diff --git a/ata.ml b/ata.ml index c12be8a..fc29e98 100644 --- a/ata.ml +++ b/ata.ml @@ -2,7 +2,12 @@ INCLUDE "debug.ml" module Tree = Tree.Binary -let gen_id() = Oo.id (object end) + +let gen_id = + let id = ref (-1) in + fun () -> incr id;!id + + module State = struct type t = int @@ -13,47 +18,64 @@ let mk_state = State.mk type state = State.t -type predicate = Ptset.t*Ptset.t -> Tree.t -> [ `True | `False | `Maybe ] +type predicate = [ `Left of (Tree.t -> bool) | `Right of (Tree.t -> bool) | + `True + ] +let eval_pred t = + function `True -> true + | `Left f | `Right f -> f t + type formula_expr = | False | True - | Or of formula * formula - | And of formula * formula - | Atom of ([ `Left | `Right ]*bool*state*predicate option) + | Or of formula * formula + | And of formula * formula + | Atom of ([ `Left | `Right | `LLeft | `RRight ]*bool*state) and formula = { fid: int; - pos : formula_expr; - neg : formula; - st : Ptset.t*Ptset.t; + fkey : int; + pos : formula_expr; + neg : formula; + st : (Ptset.t*Ptset.t)*(Ptset.t*Ptset.t); + size: int; } +external hash_const_variant : [> ] -> int = "%identity" +external int_bool : bool -> int = "%identity" + +let hash_node_form t = match t with + | False -> 0 + | True -> 1 + | And(f1,f2) -> (2+17*f1.fkey + 37*f2.fkey) land max_int + | Or(f1,f2) -> (3+101*f1.fkey + 253*f2.fkey) land max_int + | Atom(v,b,s) -> ((hash_const_variant v) + (3846*(int_bool b) +257) + (s lsl 13 - s)) land max_int + module FormNode = struct type t = formula - let hash = function - | False -> 0 - | True -> 1 - | And(f1,f2) -> 2+17*f1.fid + 37*f2.fid - | Or(f1,f2) -> 3+101*f1.fid + 253*f2.fid - | Atom(d,b,s,_) -> 5+(if d=`Left then 11 else 19)*(if b then 23 else 31)*s - - let hash t = (hash t.pos) land max_int - + + let hash t = t.fkey let equal f1 f2 = + if f1.fid == f2.fid || f1.fkey == f2.fkey || f1.pos == f2.pos then true + else match f1.pos,f2.pos with | False,False | True,True -> true - | Atom(d1,b1,s1,_), Atom(d2,b2,s2,_) when (d1 = d2) && (b1=b2) &&(s1=s2) -> true + | Atom(d1,b1,s1), Atom(d2,b2,s2) when (b1==b2) && (s1==s2) && (d1 = d2) -> true | Or(g1,g2),Or(h1,h2) | And(g1,g2),And(h1,h2) -> g1.fid == h1.fid && g2.fid == h2.fid | _ -> false + end module WH = Weak.Make(FormNode) let f_pool = WH.create 107 +let empty_pair = Ptset.empty,Ptset.empty +let empty_quad = empty_pair,empty_pair + let true_,false_ = - let rec t = { fid = 1; pos = True; neg = f ; st = Ptset.empty,Ptset.empty} - and f = { fid = 0; pos = False; neg = t; st = Ptset.empty,Ptset.empty } + let rec t = { fid = 1; pos = True; fkey=1; neg = f ; st = empty_quad; size =1; } + and f = { fid = 0; pos = False; fkey=0; neg = t; st = empty_quad; size = 1; } in WH.add f_pool f; WH.add f_pool t; @@ -63,79 +85,103 @@ let is_true f = f.fid == 1 let is_false f = f.fid == 0 -let cons pos neg s1 s2 = +let cons pos neg s1 s2 size1 size2 = let rec pnode = { fid = gen_id (); + fkey = hash_node_form pos; pos = pos; neg = nnode; - st = s1; } + st = s1; + size = size1;} and nnode = { fid = gen_id (); pos = neg; + fkey = hash_node_form neg; neg = pnode; st = s2; + size = size2; } in (WH.merge f_pool pnode),(WH.merge f_pool nnode) -let atom_ ?(pred=None) d p s = +let atom_ d p s = let si = Ptset.singleton s in let ss = match d with - | `Left -> si,Ptset.empty - | `Right -> Ptset.empty,si - in fst (cons (Atom(d,p,s,pred)) (Atom(d,not p,s,pred)) ss ss ) + | `Left -> (si,Ptset.empty),empty_pair + | `Right -> empty_pair,(si,Ptset.empty) + | `LLeft -> (Ptset.empty,si),empty_pair + | `RRight -> empty_pair,(Ptset.empty,si) + in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1) + +let union_quad ((l1,ll1),(r1,rr1)) ((l2,ll2),(r2,rr2)) = + (Ptset.union l1 l2 ,Ptset.union ll1 ll2), + (Ptset.union r1 r2 ,Ptset.union rr1 rr2) let merge_states f1 f2 = let sp = - Ptset.union (fst f1.st) (fst f2.st), - Ptset.union (snd f1.st) (snd f2.st) + union_quad f1.st f2.st and sn = - Ptset.union (fst f1.neg.st) (fst f2.neg.st), - Ptset.union (snd f1.neg.st) (snd f2.neg.st) + union_quad f1.neg.st f2.neg.st in sp,sn + +let full_or_ f1 f2 = + let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in + let sp,sn = merge_states f1 f2 in + let psize = f1.size + f2.size in + let nsize = f1.neg.size + f2.neg.size in + fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize ) let or_ f1 f2 = + let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in if is_true f1 || is_true f2 then true_ else if is_false f1 && is_false f2 then false_ else if is_false f1 then f2 else if is_false f2 then f1 else + let psize = f1.size + f2.size in + let nsize = f1.neg.size + f2.neg.size in let sp,sn = merge_states f1 f2 in - fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn) + fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize) let and_ f1 f2 = + let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in if is_true f1 && is_true f2 then true_ else if is_false f1 || is_false f2 then false_ else if is_true f1 then f2 else if is_true f2 then f1 else + let psize = f1.size + f2.size in + let nsize = f1.neg.size + f2.neg.size in let sp,sn = merge_states f1 f2 in - fst (cons (And(f1,f2)) (Or(f1.neg,f2.neg)) sp sn) + fst (cons (And(f1,f2)) (Or(f1.neg,f2.neg)) sp sn psize nsize) let not_ f = f.neg -type property = [ `None | `Existential ] -let get_prop h s = - try - Hashtbl.find h s - with - Not_found -> `None - + +module HTagSetKey = +struct + type t = Ptset.t*Tag.t + let int_hash key = key lsl 31 lor (key lsl 8) + let equal (s1,s2) (t1,t2) = (s2 == t2) && Ptset.equal s1 t1 + let hash (s,t) = int_hash (Ptset.hash s) lxor ( int_hash (Tag.hash t)) +end +module HTagSet = Hashtbl.Make(HTagSetKey) + type t = { id : int; - states : Ptset.t; + mutable states : Ptset.t; init : Ptset.t; - final : Ptset.t; + mutable final : Ptset.t; universal : Ptset.t; (* Transitions of the Alternating automaton *) - (* (tags,q) -> (marking,formula) *) - phi : ((TagSet.t*state),(bool*formula)) Hashtbl.t; - delta : (TagSet.t,(Ptset.t*bool*Ptset.t*Ptset.t)) Hashtbl.t; - properties : (state,property) Hashtbl.t; + phi : (state,(TagSet.t*(bool*formula*predicate)) list) Hashtbl.t; + delta : (state*Tag.t, (bool*formula*predicate)) Hashtbl.t; +(* delta : (state,(bool*formula*predicate) TagMap.t) Hashtbl.t; *) + sigma : (bool*formula*(predicate list*predicate list)*bool) HTagSet.t; } module Pair (X : Set.OrderedType) (Y : Set.OrderedType) = @@ -161,7 +207,7 @@ type t = { Format.fprintf ppf " }" let rec pr_frm ppf f = match f.pos with | True -> Format.fprintf ppf "⊤" - | False -> Format.fprintf ppf "⊤" + | False -> Format.fprintf ppf "⊥" | And(f1,f2) -> Format.fprintf ppf "("; (pr_frm ppf f1); @@ -172,81 +218,59 @@ type t = { (pr_frm ppf f1); Format.fprintf ppf " ∨ "; (pr_frm ppf f2); - | Atom(dir,b,s,p) -> Format.fprintf ppf "%s%s[%i]%s" + | Atom(dir,b,s) -> Format.fprintf ppf "%s%s[%i]" (if b then "" else "¬") - (if dir = `Left then "↓₁" else "↓₂")s - (match p with None -> "" | _ -> " ") + (match dir with + | `Left -> "↓₁" + | `Right -> "↓₂" + | `LLeft -> "⇓₁" + | `RRight -> "⇓₂") s let dnf_hash = Hashtbl.create 17 let rec dnf_aux f = match f.pos with | False -> PL.empty | True -> PL.singleton (Ptset.empty,Ptset.empty) - | Atom(`Left,_,s,_) -> PL.singleton (Ptset.singleton s,Ptset.empty) - | Atom(`Right,_,s,_) -> PL.singleton (Ptset.empty,Ptset.singleton s) + | Atom((`Left|`LLeft),_,s) -> PL.singleton (Ptset.singleton s,Ptset.empty) + | Atom((`Right|`RRight),_,s) -> PL.singleton (Ptset.empty,Ptset.singleton s) | Or(f1,f2) -> PL.union (dnf f1) (dnf f2) | And(f1,f2) -> - let pl1 = dnf f1 - and pl2 = dnf f2 - in - PL.fold (fun (s1,s2) acc -> - PL.fold ( fun (s1', s2') acc' -> - (PL.add - ((Ptset.union s1 s1'), - (Ptset.union s2 s2')) acc') ) - pl2 acc ) - pl1 PL.empty - - - and dnf f = - try + let pl1 = dnf f1 + and pl2 = dnf f2 + in + PL.fold (fun (s1,s2) acc -> + PL.fold ( fun (s1', s2') acc' -> + (PL.add + ((Ptset.union s1 s1'), + (Ptset.union s2 s2')) acc') ) + pl2 acc ) + pl1 PL.empty + + + and dnf f = + try Hashtbl.find dnf_hash f.fid with - Not_found -> - let d = dnf_aux f in - Hashtbl.add dnf_hash f.fid d;d - - + Not_found -> + let d = dnf_aux f in + Hashtbl.add dnf_hash f.fid d;d + + + let can_top_down f = + let nf = dnf f in + if (PL.cardinal nf > 3)then None + else match PL.elements nf with + | [(s1,s2); (t1,t2); (u1,u2)] when + Ptset.is_empty s1 && Ptset.is_empty s2 && Ptset.is_empty t1 && Ptset.is_empty u2 + -> Some(true,t2,u1) + | [(t1,t2); (u1,u2)] when Ptset.is_empty t1 && Ptset.is_empty u2 + -> Some(false,t2,u1) + | _ -> None + + let equal_form f1 f2 = (f1.fid == f2.fid) || (FormNode.equal f1 f2) || (PL.equal (dnf f1) (dnf f2)) - - let alt_trans_to_nfa ?(accu=[]) ts s mark f = - (* todo memoize *) - let f' = dnf f in - PL.fold (fun (s1,s2) acc -> (ts,s,mark,s1,s2)::acc) f' accu - - let possible_trans ?(accu=[]) a q tag = - (* todo change the data structure to avoid creating (,) *) - let ata_trans = - Hashtbl.fold (fun (ts,s) (m,f) acc -> - if (q==s) && (TagSet.mem tag ts) - then (ts,s,m,f)::acc - else acc) a.phi [] - in - if ata_trans != [] - then begin - List.iter (fun (ts,s,m,f) -> - (* The following builds too many transitions in the nfa - let ts' = TagSet.remove tag ts - in - Hashtbl.remove a.phi (ts,s); - if not (TagSet.is_empty ts') - then Hashtbl.add a.phi (ts',s) (m,f) - *) - Hashtbl.remove a.phi (ts,s) - ) ata_trans; - (* let tstag = TagSet.tag tag in *) - let nfa_trs = List.fold_left (fun acc (ts,s,m,f) -> - alt_trans_to_nfa ~accu:acc ts s m f) [] ata_trans - in - List.iter (fun (ts,s,m,s1,s2) -> - Hashtbl.add a.delta ts ((Ptset.singleton s),m,s1,s2)) nfa_trs - end; - Hashtbl.fold (fun ts (s,m,s1,s2) acc -> - if (Ptset.mem q s) && (TagSet.mem tag ts) - then (m,s1,s2)::acc else acc) a.delta accu - let dump ppf a = Format.fprintf ppf "Automaton (%i) :\n" a.id; Format.fprintf ppf "States : "; pr_st ppf (Ptset.elements a.states); @@ -254,43 +278,47 @@ type t = { Format.fprintf ppf "\nFinal states : "; pr_st ppf (Ptset.elements a.final); Format.fprintf ppf "\nUniversal states : "; pr_st ppf (Ptset.elements a.universal); Format.fprintf ppf "\nAlternating transitions :\n------------------------------\n"; - let l = Hashtbl.fold (fun k t acc -> (k,t)::acc) a.phi [] in + let l = Hashtbl.fold (fun k t acc -> + (List.map (fun (t,(m,f,p)) -> (t,k),(m,f,p)) t)@ acc) a.phi [] in let l = List.sort (fun ((tsx,x),_) ((tsy,y),_) -> if x-y == 0 then TagSet.compare tsx tsy else x-y) l in - List.iter (fun ((ts,q),(b,f)) -> + List.iter (fun ((ts,q),(b,f,_)) -> let s = - try - Tag.to_string (TagSet.choose ts) - with - | _ -> "*" + if TagSet.is_finite ts + then "{" ^ (TagSet.fold (fun t a -> a ^ " '" ^ (Tag.to_string t)^"'") ts "") ^" }" + else let cts = TagSet.neg ts in + if TagSet.is_empty cts then "*" else + (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) cts "*\\{" + )^ "}" in Format.fprintf ppf "(%s,%i) %s " s q (if b then "=>" else "->"); pr_frm ppf f; Format.fprintf ppf "\n")l; Format.fprintf ppf "NFA transitions :\n------------------------------\n"; - Hashtbl.iter (fun (ts) (q,b,s1,s2) -> - - let s = - try - Tag.to_string (TagSet.choose ts) - with - | _ -> "*" - in - pr_st ppf (Ptset.elements q); - Format.fprintf ppf ",%s %s " s (if b then "=>" else "->"); - Format.fprintf ppf "("; - pr_st ppf (Ptset.elements s1); - Format.fprintf ppf ","; - pr_st ppf (Ptset.elements s2); - Format.fprintf ppf ")\n" ) a.delta; + HTagSet.iter (fun (qs,t) (b,f,_,_) -> + pr_st ppf (Ptset.elements qs); + Format.fprintf ppf ",%s %s " (Tag.to_string t) (if b then "=>" else "->"); + pr_frm ppf f; + Format.fprintf ppf "(fid=%i) left=" f.fid; + let (l,ll),(r,rr) = f.st in + pr_st ppf (Ptset.elements l); + Format.fprintf ppf ", "; + pr_st ppf (Ptset.elements ll); + Format.fprintf ppf ", right="; + pr_st ppf (Ptset.elements r); + Format.fprintf ppf ", "; + pr_st ppf (Ptset.elements rr); + Format.fprintf ppf "\n"; + ) a.sigma; Format.fprintf ppf "=======================================\n" module Transitions = struct - type t = state*TagSet.t*bool*formula + type t = state*TagSet.t*bool*formula*predicate let ( ?< ) x = x - let ( >< ) state label = state,label - let ( >=> ) (state,(label,mark)) form = (state,label,mark,form) + let ( >< ) state (l,b) = state,(l,b,`True) + let ( ><@ ) state (l,b,p) = state,(l,b,p) + let ( >=> ) (state,(label,mark,pred)) form = (state,label,mark,form,pred) let ( +| ) f1 f2 = or_ f1 f2 let ( *& ) f1 f2 = and_ f1 f2 let ( ** ) d s = atom_ d true s @@ -299,245 +327,457 @@ type t = { end type transition = Transitions.t - let equal_trans (q1,t1,m1,f1) (q2,t2,m2,f2) = + let equal_trans (q1,t1,m1,f1,_) (q2,t2,m2,f2,_) = (q1 == q2) && (TagSet.equal t1 t2) && (m1 == m2) && (equal_form f1 f2) - - module TS : Set.S with type elt = Tree.t = Set.Make(Tree) - let res = ref TS.empty - + + module TS = + struct + type node = Nil | Cons of Tree.t * node | Concat of node*node + and t = { node : node; size : int } + let node n s = { node=n; size = s } - module BottomUpNew = struct - -IFDEF DEBUG -THEN - type trace = - | TNil of Ptset.t*Ptset.t - | TNode of Ptset.t*Ptset.t*bool* (int*bool*formula) list - - let traces = Hashtbl.create 17 - let dump_trace t = - let out = open_out "debug_trace.dot" + let empty = node Nil 0 + + let cons e t = node (Cons(e,t.node)) (t.size+1) + let concat t1 t2 = node (Concat (t1.node,t2.node)) (t1.size+t2.size) + let append = cons +(* let append e t = node (Concat(t.node,Cons(e,Nil))) (t.size+1) *) + + let to_list_rev t = + let rec aux acc l rest = + match l with + | Nil -> begin + match rest with + | Nil -> acc + | Cons(e,t) -> aux (e::acc) t Nil + | Concat(t1,t2) -> aux acc t1 t2 + end + | Cons(e,r) -> aux (e::acc) r rest + | Concat(t1,t2) -> aux acc t1 (Concat(t2,rest)) in - let outf = Format.formatter_of_out_channel out in + aux [] t.node Nil + + let length = function { size = s } -> s + + let iter f { node = n } = + let rec loop = function + | Nil -> () + | Cons(e,n) -> let _ = f e in loop n + | Concat(n1,n2) -> let _ = loop n1 in loop n2 + in loop n + + let rev_iter f { node = n } = + let rec loop = function + | Nil -> () + | Cons(e,n) -> let _ = loop n in f e + | Concat(n1,n2) -> let _ = loop n2 in loop n1 + in loop n + + + let find f { node = n } = + let rec loop = function + | Nil -> raise Not_found + | Cons(e,n) -> if f e then e else loop n + | Concat(n1,n2) -> try + loop n1 + with + | Not_found -> loop n2 + in + loop n + + end +(* + module BottomUpJumpNew = struct + +*) + module HFEval = Hashtbl.Make( + struct + type t = int*Ptset.t*Ptset.t + let equal (a,b,c) (d,e,f) = + a==d && (Ptset.equal b e) && (Ptset.equal c f) + let hash (a,b,c) = + a+17*(Ptset.hash b) + 31*(Ptset.hash c) + end) + + let hfeval = HFEval.create 4097 + + + let eval_form_bool f s1 s2 = + let rec eval f = match f.pos with + | Atom((`Left|`LLeft),b,q) -> if b == (Ptset.mem q s1) then (true,true,false) else false,false,false + | Atom((`Right|`RRight),b,q) -> if b == (Ptset.mem q s2) then (true,false,true) else false,false,false + (* test some inlining *) + | True -> true,true,true + | False -> false,false,false + | _ -> + try + HFEval.find hfeval (f.fid,s1,s2) + with + | Not_found -> let r = + match f.pos with + | Or(f1,f2) -> + let b1,rl1,rr1 = eval f1 + in + if b1 && rl1 && rr1 then (true,true,true) + else + let b2,rl2,rr2 = eval 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) + | And(f1,f2) -> + let b1,rl1,rr1 = eval f1 in + if b1 && rl1 && rr1 then (true,true,true) + else if b1 + then let b2,rl2,rr2 = eval f2 in + if b2 then (true,rl1||rl2,rr1||rr2) + else (false,false,false) + else (false,false,false) + | _ -> assert false + in + HFEval.add hfeval (f.fid,s1,s2) r; + r + in eval f + + + let fstate_pool = Hashtbl.create 11 + + let merge_pred a b = match a,b with + | Some(f1), Some(f2) -> Some(fun x -> f1 x || f2 x) + | None,None -> None + | None,Some(_) -> b + | Some(_),None -> a + + let acc_pred p l1 l2 = match p with + | `Left _ -> p::l1,l2 + | `Right _ -> l1,p::l2 + | _ -> l1,l2 + + + let merge_trans t a tag q acc = + List.fold_left (fun (accf,accm,acchtrue) (ts,(m,f,pred)) -> + if TagSet.mem tag ts + then + let tmpf,hastrue = + if is_true f then + let newfinal = + try Hashtbl.find fstate_pool f.fid with + | Not_found -> let s = mk_state() in + a.states <- Ptset.add s a.states; + a.final <- Ptset.add s a.final; + Hashtbl.add fstate_pool f.fid s;s + in + (atom_ `Left true newfinal),true + else f,false in + (or_ tmpf accf,accm||m,acchtrue||hastrue) + else (accf,accm,acchtrue) + ) acc (try Hashtbl.find a.phi q with Not_found -> []) + + let get_trans t a tag r = + try + let mark,f,predl,has_true = + HTagSet.find a.sigma (r,tag) + in f.st,f,mark,has_true,r + with + Not_found -> + let f,mark,has_true,accq = + Ptset.fold (fun q (accf,accm,acchtrue,accq) -> + let naccf,naccm,nacctrue = + merge_trans t a tag q (accf,accm,acchtrue ) + in + if is_false naccf then (naccf,naccm,nacctrue,accq) + else (naccf,naccm,nacctrue,Ptset.add q accq) + ) + r (false_,false,false,Ptset.empty) + in + HTagSet.add a.sigma (accq,tag) (mark,f,([],[]),has_true); + f.st,f,mark,has_true,accq + + let h_union = Hashtbl.create 4097 + + let pt_cup s1 s2 = + let h = (Ptset.hash s1,Ptset.hash s2) in + try + Hashtbl.find h_union h + with + | Not_found -> let s = Ptset.union s1 s2 + in + Hashtbl.add h_union h s;s + + + + let tags_of_state a q = Hashtbl.fold + (fun p l acc -> + if p == q then + List.fold_left + (fun acc (ts,_) -> + pt_cup (TagSet.positive ts) acc) acc l + else acc) a.phi Ptset.empty + + let h_tags_states = Hashtbl.create 4096 + + + + + let tags a qs = + try + Hashtbl.find h_tags_states (Ptset.hash qs) + with + | Not_found -> + let l = Ptset.fold (fun q acc -> pt_cup acc (tags_of_state a q)) qs Ptset.empty + in + Hashtbl.add h_tags_states (Ptset.hash qs) l;l + + let time cpt acc f x = + let t1 = Unix.gettimeofday () in + let r = f x in + let t2 = Unix.gettimeofday () in + let t = (1000. *.(t2 -. t1)) in + acc:=!acc+.t; + incr cpt; + r + - let rec aux t num = - if Tree.is_node t - then - match (try Hashtbl.find traces (Tree.id t) with Not_found -> TNil(Ptset.empty,Ptset.empty)) with - | TNode(r,s,mark,trs) -> - let numl = aux (Tree.left t) num in - let numr = aux (Tree.right t) (numl+1) in - let mynum = numr + 1 in - Format.fprintf outf "n%i [ label=\"<%s>\\nr=" mynum (Tag.to_string (Tree.tag t)); - pr_st outf (Ptset.elements r); - Format.fprintf outf "\\ns="; - pr_st outf (Ptset.elements s); - List.iter (fun (q,m,f) -> - Format.fprintf outf "\\n%i %s" q (if m then "⇨" else "→"); - pr_frm outf f ) trs; - Format.fprintf outf "\", %s shape=box ];\n" - (if mark then "color=cyan1, style=filled," else ""); - let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numl in - let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numr in - mynum - | TNil(r,s) -> Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num; - pr_st outf (Ptset.elements r); - Format.fprintf outf "\\ns="; - pr_st outf (Ptset.elements s); - Format.fprintf outf "\"];\n";num - else - match Hashtbl.find traces (-10) with - | TNil(r,s) -> - Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num; - pr_st outf (Ptset.elements r); - Format.fprintf outf "\\ns="; - pr_st outf (Ptset.elements s); - Format.fprintf outf "\"];\n"; - num - | _ -> assert false + let h_time = Hashtbl.create 4096 + let calls = ref 0 + let rtime s f x = + + let cpt,atime = + try + Hashtbl.find h_time s + with + | _ -> (ref 0, ref 0.) + in + let r = time cpt atime f x in - Format.fprintf outf "digraph G {\n"; - ignore(aux t 0); - Format.fprintf outf "}\n%!"; - close_out out; - ignore(Sys.command "dot -Tsvg debug_trace.dot > debug_trace.svg") -END - - - - let hfeval = Hashtbl.create 17 - let miss = ref 0 - let call = ref 0 - let rec findlist s1 s2 = function - | [] -> raise Not_found - | ((ss1,ss2),r)::_ when - (not (Ptset.is_empty s1)) && (Ptset.subset s1 ss1) && - (not (Ptset.is_empty s2)) && (Ptset.subset s2 ss2) -> r - | _::r -> findlist s1 s2 r - - let eval_form f s1 s2 res1 res2 = + Hashtbl.replace h_time s (cpt,atime); + r - let rec eval_aux f = match f.pos with - | Atom(`Left,b,q,_) -> if b == (Ptset.mem q s1) then (true,res1) else false,TS.empty - | Atom(`Right,b,q,_) -> if b == (Ptset.mem q s2) then (true,res2) else false,TS.empty - | True -> true,(TS.union res1 res2) - | False -> false,TS.empty - | Or(f1,f2) -> - let b1,r1 = eval_aux f1 - and b2,r2 = eval_aux f2 - in - let r1 = if b1 then r1 else TS.empty - and r2 = if b2 then r2 else TS.empty - in (b1 || b2, TS.union r1 r2) - - | And(f1,f2) -> - let b1,r1 = eval_aux f1 - and b2,r2 = eval_aux f2 - in - if b1 && b2 then (true, TS.union r1 r2) - else (false,TS.empty) + let rec accepting_among_time a t r ctx = + incr calls; + let orig = r in + let rest = Ptset.inter r a.final in + let r = Ptset.diff r rest in + if Ptset.is_empty r then rest,TS.empty else + if Tree.is_node t + then + let among,result,form = + let ((ls,lls),(rs,rrs)),formula,mark,has_true,r' = + let tag = rtime "Tree.tag" Tree.tag t in + rtime "get_trans" (get_trans t a tag) r + in + let tl = rtime "tags" (tags a) ls + and tr = rtime "tags" (tags a) rs + and tll = rtime "tags" (tags a) lls + and trr = rtime "tags" (tags a) rrs + in + let first = + if Ptset.mem Tag.pcdata (pt_cup tl tll) + then + rtime "Tree.text_below" (Tree.text_below) t + else + let etl = Ptset.is_empty tl + and etll = Ptset.is_empty tll + in + if etl && etll + then Tree.mk_nil t + else + if etl then rtime "Tree.tagged_desc_only" (Tree.tagged_desc_only t) tll + else if etll then rtime "Tree.first_child" (Tree.first_child) t + else (* add child only *) + rtime "Tree.tagged_below" (Tree.tagged_below t tl) tll + and next = + if Ptset.mem Tag.pcdata (pt_cup tr trr) + then + rtime "Tree.text_next" (Tree.text_next t) ctx + else + let etr = Ptset.is_empty tr + and etrr = Ptset.is_empty trr + in + if etr && etrr + then Tree.mk_nil t + else + if etr then rtime "Tree.tagged_foll_only" (Tree.tagged_foll_only t trr) ctx + else if etrr then rtime "Tree.next_sibling" (Tree.next_sibling) t + else (* add ns only *) + rtime "Tree.tagged_next" (Tree.tagged_next t tr trr) ctx + + in + let s1,res1 = accepting_among_time a first (pt_cup ls lls) t + and s2,res2 = accepting_among_time a next (pt_cup rs rrs) ctx + in + let rb,rb1,rb2 = rtime "eval_form_bool" (eval_form_bool formula s1) s2 in + if rb + then + let res1 = if rb1 then res1 else TS.empty + and res2 = if rb2 then res2 else TS.empty + in r', rtime "TS.concat" (TS.concat res2) (if mark then rtime "TS.append" (TS.append t) res1 else res1),formula + else Ptset.empty,TS.empty,formula + + in + + among,result + + else orig,TS.empty + + + let run_time a t = + let st,res = accepting_among_time a t a.init t in + let _ = Printf.eprintf "\n Timings\n"; + let total_time = Hashtbl.fold (fun fname ({ contents=cpt }, {contents=atime}) (total_time) -> + Printf.eprintf "%s\t %i calls, %f ms accumulated time, %f ms mean time\n" + fname cpt atime (atime /. (float_of_int cpt)); + total_time +. atime ) h_time 0. + in + Printf.eprintf "total calls %i, total monitored time %f ms\n%!" !calls total_time + in + if Ptset.is_empty (st) then TS.empty else res - in incr call;eval_aux f - - (* If true, then the formule may evaluate to true in the future, - if false it will always return false, i.e. necessary conditions are not - satisfied - *) - - let val3 = function true -> `True - | false -> `False - - let or3 a b = match a,b with - | `True,_ | _,`True -> `True - | `False,`False -> `False - | _ -> `Maybe - - let and3 a b = match a,b with - | `True,`True -> `True - | `False,_ | _,`False -> `False - | _ -> `Maybe - let not3 = function - | `True -> `False - | `False -> `True - | `Maybe -> `Maybe - - let true3 = function true -> `Maybe - | false -> `False - - let may_eval (s1,s2) f t = - let rec aux f = match f.pos with - | True -> `True - | False -> `False - | Or(f1,f2) -> or3 (aux f1) (aux f2) - | And(f1,f2) -> and3 (aux f1) (aux f2) - | Atom(dir,b,q,predo) -> - and3 (true3 ((Ptset.mem q (match dir with - | `Left -> s1 - | `Right -> s2)) == b)) - (match predo with - | Some pred -> (pred (s1,s2) t) - | None -> `True) - - in aux f - let rec accepting_among a t r = - let r = Ptset.diff r a.final in - let rest = Ptset.inter a.final r in - if Ptset.is_empty r then r,TS.empty else - if (not (Tree.is_node t)) + let rec accepting_among a t r ctx = + let orig = r in + let rest = Ptset.inter r a.final in + let r = Ptset.diff r rest in + if Ptset.is_empty r then rest,TS.empty else + if Tree.is_node t then - let _ = D(Hashtbl.add traces (-10) (TNil(r,Ptset.inter a.final r))) - in - Ptset.inter a.final r,TS.empty - else - let tag = Tree.tag t - and t1 = Tree.first_child t - and t2 = Tree.next_sibling t + let among,result,form = + let ((ls,lls),(rs,rrs)),formula,mark,has_true,r' = + let tag = Tree.tag t in + get_trans t a tag r + in + let tl = tags a ls + and tr = tags a rs + and tll = tags a lls + and trr = tags a rrs + in + let first = + if Ptset.mem Tag.pcdata (pt_cup tl tll) + then + Tree.text_below t + else + let etl = Ptset.is_empty tl + and etll = Ptset.is_empty tll + in + if etl && etll + then Tree.mk_nil t + else + if etl then Tree.tagged_desc_only t tll + else if etll then Tree.first_child t + else (* add child only *) + Tree.tagged_below t tl tll + and next = + if Ptset.mem Tag.pcdata (pt_cup tr trr) + then + Tree.text_next t ctx + else + let etr = Ptset.is_empty tr + and etrr = Ptset.is_empty trr + in + if etr && etrr + then Tree.mk_nil t + else + if etr then Tree.tagged_foll_only t trr ctx + else if etrr then Tree.next_sibling t + else (* add ns only *) + Tree.tagged_next t tr trr ctx + + in + let s1,res1 = accepting_among a first (pt_cup ls lls) t + and s2,res2 = accepting_among a next (pt_cup rs rrs) ctx + in + let rb,rb1,rb2 = eval_form_bool formula s1 s2 in + if rb + then + let res1 = if rb1 then res1 else TS.empty + and res2 = if rb2 then res2 else TS.empty + in r', TS.concat res2 (if mark then TS.append t res1 else res1),formula + else Ptset.empty,TS.empty,formula + + in + among,result + + else orig,TS.empty + + + let run a t = + let st,res = accepting_among a t a.init t in + if Ptset.is_empty (st) then TS.empty else res + + let rec accepting_among_count a t r ctx = + let orig = r in + let rest = Ptset.inter r a.final in + let r = Ptset.diff r rest in + if Ptset.is_empty r then rest,0 else + if Tree.is_node t + then + let ((ls,lls),(rs,rrs)),formula,mark,has_true,r' = + let tag = Tree.tag t in + get_trans t a tag r + in + let tl = tags a ls + and tr = tags a rs + and tll = tags a lls + and trr = tags a rrs + in + let first = + if Ptset.mem Tag.pcdata (pt_cup tl tll) + then + Tree.text_below t + else + let etl = Ptset.is_empty tl + and etll = Ptset.is_empty tll + in + if etl && etll + then Tree.mk_nil t + else + if etl then Tree.tagged_desc_only t tll + else if etll then Tree.first_child t + else (* add child only *) + Tree.tagged_below t tl tll + and next = + if Ptset.mem Tag.pcdata (pt_cup tr trr) + then + Tree.text_next t ctx + else + let etr = Ptset.is_empty tr + and etrr = Ptset.is_empty trr + in + if etr && etrr + then Tree.mk_nil t + else + if etr then Tree.tagged_foll_only t trr ctx + else if etrr then Tree.next_sibling t + else (* add ns only *) + Tree.tagged_next t tr trr ctx + in - let r1,r2,trs = - Hashtbl.fold (fun (ts,q) ((m,f)as tr) ((ar1,ar2,lt)as acc) -> - if (TagSet.mem tag ts) && Ptset.mem q r - then begin - (* Format.fprintf Format.err_formatter "Tree with tag %s qualifies for transition : (%s,%i)%s" - (Tag.to_string tag) - (try - Tag.to_string (TagSet.choose ts) - with - | _ -> "*" ) - q - (if m then "=>" else "->"); - pr_frm Format.err_formatter f; - Format.fprintf Format.err_formatter "\n"; *) - let ls,rs = f.st in - Ptset.union ls ar1,Ptset.union rs ar2,(q,tr)::lt - end - else acc - ) a.phi (Ptset.empty,Ptset.empty,[]) + let s1,res1 = accepting_among_count a first (pt_cup ls lls) t + and s2,res2 = accepting_among_count a next (pt_cup rs rrs) ctx in - let rtrue,rfalse,rmay,trs,selnodes = - List.fold_left (fun (at,af,am,atrs,selnodes) (q,(m,f)) -> - let ppf = Format.err_formatter in - match (*may_eval (r1,r2) f t *) `Maybe with - | `True -> - (* Format.fprintf ppf "Will skip (%i) %s " q (if m then "=>" else "->"); - pr_frm ppf f; - Format.fprintf ppf ", always true \n"; *) - (Ptset.add q at),af,am,atrs,TS.add t selnodes - | `False -> - (*Format.fprintf ppf "Will skip (%i) %s " q (if m then "=>" else "->"); - pr_frm ppf f; - Format.fprintf ppf ", always false \n"; *) - at,(Ptset.add q af),am,atrs,selnodes - - | `Maybe -> -(* Format.fprintf ppf "Must take (%i) %s " q (if m then "=>" else "->"); - pr_frm ppf f; - Format.fprintf ppf "\n"; *) - at,af,(Ptset.add q am),(q,(m,f))::atrs,selnodes) - (Ptset.empty,Ptset.empty,Ptset.empty,[],TS.empty) trs - in - let rr1,rr2,trs = - List.fold_left (fun ((ar1,ar2,trs)as acc) ((q,(_,f)as tr)) -> - if Ptset.mem q rmay - then let ls,rs = f.st in - Ptset.union ls ar1,Ptset.union rs ar2,tr::trs - else acc) (Ptset.empty,Ptset.empty,[]) trs - in - let s1,res1 = accepting_among a t1 rr1 - and s2,res2 = accepting_among a t2 rr2 - in - let res,set,mark,trs = List.fold_left (fun ((sel_nodes,res,amark,acctr) as acc) (q,(mark,f)) -> - let b,resnodes = eval_form f s1 s2 res1 res2 in - (* if b then begin - pr_st Format.err_formatter (Ptset.elements s1); - Format.fprintf Format.err_formatter ","; - pr_st Format.err_formatter (Ptset.elements s2); - Format.fprintf Format.err_formatter " satisfies "; - pr_frm Format.err_formatter f; - Format.fprintf Format.err_formatter " for input tree %s\n" (Tag.to_string tag); - end; *) - if b - then - (TS.union - (if mark then TS.add t resnodes else resnodes) - sel_nodes) - ,Ptset.add q res,amark||mark,(q,mark,f)::acctr - else acc - ) (TS.empty,rtrue,false,[]) trs - in - - let set = Ptset.union a.final set in - let _ = D(Hashtbl.add traces (Tree.id t) (TNode(r,set,mark,trs))) in - set,res - + let rb,rb1,rb2 = eval_form_bool formula s1 s2 in + if rb + then + let res1 = if rb1 then res1 else 0 + and res2 = if rb2 then res2 else 0 + in r', res2 + (if mark then 1 + res1 else res1) + else Ptset.empty,0 + + + + else orig,0 + - let run a t = - let st,res = accepting_among a t a.init in - let b = Ptset.is_empty (st) in - let _ = D(dump_trace t) in - if b then [] - else (TS.elements res) - + let run_count a t = + let st,res = accepting_among_count a t a.init t in + if Ptset.is_empty (st) then 0 else res + + + + + +(* end +*)