1 (* Todo refactor and remove this alias *)
3 module Tree = Tree.Binary
17 let mk_state = State.mk
21 type predicate = [ `Left of (Tree.t -> bool) | `Right of (Tree.t -> bool) |
26 function `True -> true
27 | `Left f | `Right f -> f t
31 | Or of formula * formula
32 | And of formula * formula
33 | Atom of ([ `Left | `Right | `LLeft | `RRight ]*bool*state)
34 and formula = { fid: int;
38 st : (Ptset.t*Ptset.t)*(Ptset.t*Ptset.t);
42 external hash_const_variant : [> ] -> int = "%identity"
43 external int_bool : bool -> int = "%identity"
45 let hash_node_form t = match t with
48 | And(f1,f2) -> (2+17*f1.fkey + 37*f2.fkey) land max_int
49 | Or(f1,f2) -> (3+101*f1.fkey + 253*f2.fkey) land max_int
50 | Atom(v,b,s) -> ((hash_const_variant v) + (3846*(int_bool b) +257) + (s lsl 13 - s)) land max_int
59 if f1.fid == f2.fid || f1.fkey == f2.fkey || f1.pos == f2.pos then true
61 match f1.pos,f2.pos with
62 | False,False | True,True -> true
63 | Atom(d1,b1,s1), Atom(d2,b2,s2) when (b1==b2) && (s1==s2) && (d1 = d2) -> true
65 | And(g1,g2),And(h1,h2) -> g1.fid == h1.fid && g2.fid == h2.fid
69 module WH = Weak.Make(FormNode)
71 let f_pool = WH.create 107
73 let empty_pair = Ptset.empty,Ptset.empty
74 let empty_quad = empty_pair,empty_pair
77 let rec t = { fid = 1; pos = True; fkey=1; neg = f ; st = empty_quad; size =1; }
78 and f = { fid = 0; pos = False; fkey=0; neg = t; st = empty_quad; size = 1; }
84 let is_true f = f.fid == 1
85 let is_false f = f.fid == 0
88 let cons pos neg s1 s2 size1 size2 =
91 fkey = hash_node_form pos;
99 fkey = hash_node_form neg;
105 (WH.merge f_pool pnode),(WH.merge f_pool nnode)
108 let si = Ptset.singleton s in
109 let ss = match d with
110 | `Left -> (si,Ptset.empty),empty_pair
111 | `Right -> empty_pair,(si,Ptset.empty)
112 | `LLeft -> (Ptset.empty,si),empty_pair
113 | `RRight -> empty_pair,(Ptset.empty,si)
114 in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
116 let union_quad ((l1,ll1),(r1,rr1)) ((l2,ll2),(r2,rr2)) =
117 (Ptset.union l1 l2 ,Ptset.union ll1 ll2),
118 (Ptset.union r1 r2 ,Ptset.union rr1 rr2)
120 let merge_states f1 f2 =
122 union_quad f1.st f2.st
124 union_quad f1.neg.st f2.neg.st
129 let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
130 let sp,sn = merge_states f1 f2 in
131 let psize = f1.size + f2.size in
132 let nsize = f1.neg.size + f2.neg.size in
133 fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize )
136 let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
137 if is_true f1 || is_true f2 then true_
138 else if is_false f1 && is_false f2 then false_
139 else if is_false f1 then f2
140 else if is_false f2 then f1
142 let psize = f1.size + f2.size in
143 let nsize = f1.neg.size + f2.neg.size in
144 let sp,sn = merge_states f1 f2 in
145 fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize)
150 let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
151 if is_true f1 && is_true f2 then true_
152 else if is_false f1 || is_false f2 then false_
153 else if is_true f1 then f2
154 else if is_true f2 then f1
156 let psize = f1.size + f2.size in
157 let nsize = f1.neg.size + f2.neg.size in
158 let sp,sn = merge_states f1 f2 in
159 fst (cons (And(f1,f2)) (Or(f1.neg,f2.neg)) sp sn psize nsize)
167 type t = Ptset.t*Tag.t
168 let int_hash key = key lsl 31 lor (key lsl 8)
169 let equal (s1,s2) (t1,t2) = (s2 == t2) && Ptset.equal s1 t1
170 let hash (s,t) = int_hash (Ptset.hash s) lxor ( int_hash (Tag.hash t))
172 module HTagSet = Hashtbl.Make(HTagSetKey)
176 mutable states : Ptset.t;
178 mutable final : Ptset.t;
180 (* Transitions of the Alternating automaton *)
181 phi : (state,(TagSet.t*(bool*formula*predicate)) list) Hashtbl.t;
182 delta : (state*Tag.t, (bool*formula*predicate)) Hashtbl.t;
183 (* delta : (state,(bool*formula*predicate) TagMap.t) Hashtbl.t; *)
184 sigma : (bool*formula*(predicate list*predicate list)*bool) HTagSet.t;
187 module Pair (X : Set.OrderedType) (Y : Set.OrderedType) =
190 let compare (x1,y1) (x2,y2) =
191 let r = X.compare x1 x2 in
192 if r == 0 then Y.compare y1 y2
196 module PL = Set.Make (Pair (Ptset) (Ptset))
199 let pr_st ppf l = Format.fprintf ppf "{";
203 | [s] -> Format.fprintf ppf " %i" s
204 | p::r -> Format.fprintf ppf " %i" p;
205 List.iter (fun i -> Format.fprintf ppf "; %i" i) r
207 Format.fprintf ppf " }"
208 let rec pr_frm ppf f = match f.pos with
209 | True -> Format.fprintf ppf "⊤"
210 | False -> Format.fprintf ppf "⊥"
212 Format.fprintf ppf "(";
214 Format.fprintf ppf ") ∧ (";
216 Format.fprintf ppf ")"
219 Format.fprintf ppf " ∨ ";
221 | Atom(dir,b,s) -> Format.fprintf ppf "%s%s[%i]"
222 (if b then "" else "¬")
229 let dnf_hash = Hashtbl.create 17
231 let rec dnf_aux f = match f.pos with
233 | True -> PL.singleton (Ptset.empty,Ptset.empty)
234 | Atom((`Left|`LLeft),_,s) -> PL.singleton (Ptset.singleton s,Ptset.empty)
235 | Atom((`Right|`RRight),_,s) -> PL.singleton (Ptset.empty,Ptset.singleton s)
236 | Or(f1,f2) -> PL.union (dnf f1) (dnf f2)
241 PL.fold (fun (s1,s2) acc ->
242 PL.fold ( fun (s1', s2') acc' ->
244 ((Ptset.union s1 s1'),
245 (Ptset.union s2 s2')) acc') )
252 Hashtbl.find dnf_hash f.fid
256 Hashtbl.add dnf_hash f.fid d;d
261 if (PL.cardinal nf > 3)then None
262 else match PL.elements nf with
263 | [(s1,s2); (t1,t2); (u1,u2)] when
264 Ptset.is_empty s1 && Ptset.is_empty s2 && Ptset.is_empty t1 && Ptset.is_empty u2
266 | [(t1,t2); (u1,u2)] when Ptset.is_empty t1 && Ptset.is_empty u2
271 let equal_form f1 f2 =
272 (f1.fid == f2.fid) || (FormNode.equal f1 f2) || (PL.equal (dnf f1) (dnf f2))
275 Format.fprintf ppf "Automaton (%i) :\n" a.id;
276 Format.fprintf ppf "States : "; pr_st ppf (Ptset.elements a.states);
277 Format.fprintf ppf "\nInitial states : "; pr_st ppf (Ptset.elements a.init);
278 Format.fprintf ppf "\nFinal states : "; pr_st ppf (Ptset.elements a.final);
279 Format.fprintf ppf "\nUniversal states : "; pr_st ppf (Ptset.elements a.universal);
280 Format.fprintf ppf "\nAlternating transitions :\n------------------------------\n";
281 let l = Hashtbl.fold (fun k t acc ->
282 (List.map (fun (t,(m,f,p)) -> (t,k),(m,f,p)) t)@ acc) a.phi [] in
283 let l = List.sort (fun ((tsx,x),_) ((tsy,y),_) -> if x-y == 0 then TagSet.compare tsx tsy else x-y) l in
284 List.iter (fun ((ts,q),(b,f,_)) ->
287 if TagSet.is_finite ts
288 then "{" ^ (TagSet.fold (fun t a -> a ^ " '" ^ (Tag.to_string t)^"'") ts "") ^" }"
289 else let cts = TagSet.neg ts in
290 if TagSet.is_empty cts then "*" else
291 (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) cts "*\\{"
294 Format.fprintf ppf "(%s,%i) %s " s q (if b then "=>" else "->");
296 Format.fprintf ppf "\n")l;
298 Format.fprintf ppf "NFA transitions :\n------------------------------\n";
299 HTagSet.iter (fun (qs,t) (b,f,_,_) ->
300 pr_st ppf (Ptset.elements qs);
301 Format.fprintf ppf ",%s %s " (Tag.to_string t) (if b then "=>" else "->");
303 Format.fprintf ppf "(fid=%i) left=" f.fid;
304 let (l,ll),(r,rr) = f.st in
305 pr_st ppf (Ptset.elements l);
306 Format.fprintf ppf ", ";
307 pr_st ppf (Ptset.elements ll);
308 Format.fprintf ppf ", right=";
309 pr_st ppf (Ptset.elements r);
310 Format.fprintf ppf ", ";
311 pr_st ppf (Ptset.elements rr);
312 Format.fprintf ppf "\n";
314 Format.fprintf ppf "=======================================\n"
316 module Transitions = struct
317 type t = state*TagSet.t*bool*formula*predicate
319 let ( >< ) state (l,b) = state,(l,b,`True)
320 let ( ><@ ) state (l,b,p) = state,(l,b,p)
321 let ( >=> ) (state,(label,mark,pred)) form = (state,label,mark,form,pred)
322 let ( +| ) f1 f2 = or_ f1 f2
323 let ( *& ) f1 f2 = and_ f1 f2
324 let ( ** ) d s = atom_ d true s
328 type transition = Transitions.t
330 let equal_trans (q1,t1,m1,f1,_) (q2,t2,m2,f2,_) =
331 (q1 == q2) && (TagSet.equal t1 t2) && (m1 == m2) && (equal_form f1 f2)
335 type node = Nil | Cons of Tree.t * node | Concat of node*node
336 and t = { node : node; size : int }
337 let node n s = { node=n; size = s }
339 let empty = node Nil 0
341 let cons e t = node (Cons(e,t.node)) (t.size+1)
342 let concat t1 t2 = node (Concat (t1.node,t2.node)) (t1.size+t2.size)
344 (* let append e t = node (Concat(t.node,Cons(e,Nil))) (t.size+1) *)
347 let rec aux acc l rest =
352 | Cons(e,t) -> aux (e::acc) t Nil
353 | Concat(t1,t2) -> aux acc t1 t2
355 | Cons(e,r) -> aux (e::acc) r rest
356 | Concat(t1,t2) -> aux acc t1 (Concat(t2,rest))
360 let length = function { size = s } -> s
362 let iter f { node = n } =
363 let rec loop = function
365 | Cons(e,n) -> let _ = f e in loop n
366 | Concat(n1,n2) -> let _ = loop n1 in loop n2
369 let rev_iter f { node = n } =
370 let rec loop = function
372 | Cons(e,n) -> let _ = loop n in f e
373 | Concat(n1,n2) -> let _ = loop n2 in loop n1
377 let find f { node = n } =
378 let rec loop = function
379 | Nil -> raise Not_found
380 | Cons(e,n) -> if f e then e else loop n
381 | Concat(n1,n2) -> try
384 | Not_found -> loop n2
390 module BottomUpJumpNew = struct
393 module HFEval = Hashtbl.Make(
395 type t = int*Ptset.t*Ptset.t
396 let equal (a,b,c) (d,e,f) =
397 a==d && (Ptset.equal b e) && (Ptset.equal c f)
399 a+17*(Ptset.hash b) + 31*(Ptset.hash c)
402 let hfeval = HFEval.create 4097
405 let eval_form_bool f s1 s2 =
406 let rec eval f = match f.pos with
407 | Atom((`Left|`LLeft),b,q) -> if b == (Ptset.mem q s1) then (true,true,false) else false,false,false
408 | Atom((`Right|`RRight),b,q) -> if b == (Ptset.mem q s2) then (true,false,true) else false,false,false
409 (* test some inlining *)
410 | True -> true,true,true
411 | False -> false,false,false
414 HFEval.find hfeval (f.fid,s1,s2)
416 | Not_found -> let r =
419 let b1,rl1,rr1 = eval f1
421 if b1 && rl1 && rr1 then (true,true,true)
423 let b2,rl2,rr2 = eval f2
425 let rl1,rr1 = if b1 then rl1,rr1 else false,false
426 and rl2,rr2 = if b2 then rl2,rr2 else false,false
427 in (b1 || b2, rl1||rl2,rr1||rr2)
429 let b1,rl1,rr1 = eval f1 in
430 if b1 && rl1 && rr1 then (true,true,true)
432 then let b2,rl2,rr2 = eval f2 in
433 if b2 then (true,rl1||rl2,rr1||rr2)
434 else (false,false,false)
435 else (false,false,false)
438 HFEval.add hfeval (f.fid,s1,s2) r;
443 let fstate_pool = Hashtbl.create 11
445 let merge_pred a b = match a,b with
446 | Some(f1), Some(f2) -> Some(fun x -> f1 x || f2 x)
451 let acc_pred p l1 l2 = match p with
452 | `Left _ -> p::l1,l2
453 | `Right _ -> l1,p::l2
457 let merge_trans t a tag q acc =
458 List.fold_left (fun (accf,accm,acchtrue) (ts,(m,f,pred)) ->
464 try Hashtbl.find fstate_pool f.fid with
465 | Not_found -> let s = mk_state() in
466 a.states <- Ptset.add s a.states;
467 a.final <- Ptset.add s a.final;
468 Hashtbl.add fstate_pool f.fid s;s
470 (atom_ `Left true newfinal),true
472 (or_ tmpf accf,accm||m,acchtrue||hastrue)
473 else (accf,accm,acchtrue)
474 ) acc (try Hashtbl.find a.phi q with Not_found -> [])
476 let get_trans t a tag r =
478 let mark,f,predl,has_true =
479 HTagSet.find a.sigma (r,tag)
480 in f.st,f,mark,has_true,r
483 let f,mark,has_true,accq =
484 Ptset.fold (fun q (accf,accm,acchtrue,accq) ->
485 let naccf,naccm,nacctrue =
486 merge_trans t a tag q (accf,accm,acchtrue )
488 if is_false naccf then (naccf,naccm,nacctrue,accq)
489 else (naccf,naccm,nacctrue,Ptset.add q accq)
491 r (false_,false,false,Ptset.empty)
493 HTagSet.add a.sigma (accq,tag) (mark,f,([],[]),has_true);
494 f.st,f,mark,has_true,accq
496 let h_union = Hashtbl.create 4097
499 let h = (Ptset.hash s1,Ptset.hash s2) in
501 Hashtbl.find h_union h
503 | Not_found -> let s = Ptset.union s1 s2
505 Hashtbl.add h_union h s;s
509 let tags_of_state a q = Hashtbl.fold
514 pt_cup (TagSet.positive ts) acc) acc l
515 else acc) a.phi Ptset.empty
517 let h_tags_states = Hashtbl.create 4096
524 Hashtbl.find h_tags_states (Ptset.hash qs)
527 let l = Ptset.fold (fun q acc -> pt_cup acc (tags_of_state a q)) qs Ptset.empty
529 Hashtbl.add h_tags_states (Ptset.hash qs) l;l
531 let time cpt acc f x =
532 let t1 = Unix.gettimeofday () in
534 let t2 = Unix.gettimeofday () in
535 let t = (1000. *.(t2 -. t1)) in
541 let h_time = Hashtbl.create 4096
548 Hashtbl.find h_time s
550 | _ -> (ref 0, ref 0.)
552 let r = time cpt atime f x
554 Hashtbl.replace h_time s (cpt,atime);
557 let rec accepting_among_time a t r ctx =
560 let rest = Ptset.inter r a.final in
561 let r = Ptset.diff r rest in
562 if Ptset.is_empty r then rest,TS.empty else
565 let among,result,form =
566 let ((ls,lls),(rs,rrs)),formula,mark,has_true,r' =
567 let tag = rtime "Tree.tag" Tree.tag t in
568 rtime "get_trans" (get_trans t a tag) r
570 let tl = rtime "tags" (tags a) ls
571 and tr = rtime "tags" (tags a) rs
572 and tll = rtime "tags" (tags a) lls
573 and trr = rtime "tags" (tags a) rrs
576 if Ptset.mem Tag.pcdata (pt_cup tl tll)
578 rtime "Tree.text_below" (Tree.text_below) t
580 let etl = Ptset.is_empty tl
581 and etll = Ptset.is_empty tll
586 if etl then rtime "Tree.tagged_desc_only" (Tree.tagged_desc_only t) tll
587 else if etll then rtime "Tree.first_child" (Tree.first_child) t
588 else (* add child only *)
589 rtime "Tree.tagged_below" (Tree.tagged_below t tl) tll
591 if Ptset.mem Tag.pcdata (pt_cup tr trr)
593 rtime "Tree.text_next" (Tree.text_next t) ctx
595 let etr = Ptset.is_empty tr
596 and etrr = Ptset.is_empty trr
601 if etr then rtime "Tree.tagged_foll_only" (Tree.tagged_foll_only t trr) ctx
602 else if etrr then rtime "Tree.next_sibling" (Tree.next_sibling) t
603 else (* add ns only *)
604 rtime "Tree.tagged_next" (Tree.tagged_next t tr trr) ctx
607 let s1,res1 = accepting_among_time a first (pt_cup ls lls) t
608 and s2,res2 = accepting_among_time a next (pt_cup rs rrs) ctx
610 let rb,rb1,rb2 = rtime "eval_form_bool" (eval_form_bool formula s1) s2 in
613 let res1 = if rb1 then res1 else TS.empty
614 and res2 = if rb2 then res2 else TS.empty
615 in r', rtime "TS.concat" (TS.concat res2) (if mark then rtime "TS.append" (TS.append t) res1 else res1),formula
616 else Ptset.empty,TS.empty,formula
626 let st,res = accepting_among_time a t a.init t in
627 let _ = Printf.eprintf "\n Timings\n";
628 let total_time = Hashtbl.fold (fun fname ({ contents=cpt }, {contents=atime}) (total_time) ->
629 Printf.eprintf "%s\t %i calls, %f ms accumulated time, %f ms mean time\n"
630 fname cpt atime (atime /. (float_of_int cpt));
631 total_time +. atime ) h_time 0.
633 Printf.eprintf "total calls %i, total monitored time %f ms\n%!" !calls total_time
635 if Ptset.is_empty (st) then TS.empty else res
639 let rec accepting_among a t r ctx =
641 let rest = Ptset.inter r a.final in
642 let r = Ptset.diff r rest in
643 if Ptset.is_empty r then rest,TS.empty else
646 let among,result,form =
647 let ((ls,lls),(rs,rrs)),formula,mark,has_true,r' =
648 let tag = Tree.tag t in
657 if Ptset.mem Tag.pcdata (pt_cup tl tll)
661 let etl = Ptset.is_empty tl
662 and etll = Ptset.is_empty tll
667 if etl then Tree.tagged_desc_only t tll
668 else if etll then Tree.first_child t
669 else (* add child only *)
670 Tree.tagged_below t tl tll
672 if Ptset.mem Tag.pcdata (pt_cup tr trr)
676 let etr = Ptset.is_empty tr
677 and etrr = Ptset.is_empty trr
682 if etr then Tree.tagged_foll_only t trr ctx
683 else if etrr then Tree.next_sibling t
684 else (* add ns only *)
685 Tree.tagged_next t tr trr ctx
688 let s1,res1 = accepting_among a first (pt_cup ls lls) t
689 and s2,res2 = accepting_among a next (pt_cup rs rrs) ctx
691 let rb,rb1,rb2 = eval_form_bool formula s1 s2 in
694 let res1 = if rb1 then res1 else TS.empty
695 and res2 = if rb2 then res2 else TS.empty
696 in r', TS.concat res2 (if mark then TS.append t res1 else res1),formula
697 else Ptset.empty,TS.empty,formula
706 let st,res = accepting_among a t a.init t in
707 if Ptset.is_empty (st) then TS.empty else res