(* Todo refactor and remove this alias *) INCLUDE "debug.ml" module Tree = Tree.Binary let gen_id = let id = ref (-1) in fun () -> incr id;!id module State = struct type t = int let mk = gen_id end let mk_state = State.mk type state = State.t 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 | `LLeft | `RRight ]*bool*state) and formula = { fid: int; 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 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 (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; 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; t,f let is_true f = f.fid == 1 let is_false f = f.fid == 0 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; 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_ d p s = let si = Ptset.singleton s in let ss = match d with | `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 = union_quad f1.st f2.st and sn = 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 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 psize nsize) let not_ f = f.neg 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; mutable states : Ptset.t; init : Ptset.t; mutable final : Ptset.t; universal : Ptset.t; (* Transitions of the Alternating automaton *) 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) = struct type t = X.t*Y.t let compare (x1,y1) (x2,y2) = let r = X.compare x1 x2 in if r == 0 then Y.compare y1 y2 else r end module PL = Set.Make (Pair (Ptset) (Ptset)) let pr_st ppf l = Format.fprintf ppf "{"; begin match l with | [] -> () | [s] -> Format.fprintf ppf " %i" s | p::r -> Format.fprintf ppf " %i" p; List.iter (fun i -> Format.fprintf ppf "; %i" i) r end; Format.fprintf ppf " }" let rec pr_frm ppf f = match f.pos with | True -> Format.fprintf ppf "⊤" | False -> Format.fprintf ppf "⊥" | And(f1,f2) -> Format.fprintf ppf "("; (pr_frm ppf f1); Format.fprintf ppf ") ∧ ("; (pr_frm ppf f2); Format.fprintf ppf ")" | Or(f1,f2) -> (pr_frm ppf f1); Format.fprintf ppf " ∨ "; (pr_frm ppf f2); | Atom(dir,b,s) -> Format.fprintf ppf "%s%s[%i]" (if b then "" else "¬") (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|`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 Hashtbl.find dnf_hash f.fid with 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 dump ppf a = Format.fprintf ppf "Automaton (%i) :\n" a.id; Format.fprintf ppf "States : "; pr_st ppf (Ptset.elements a.states); Format.fprintf ppf "\nInitial states : "; pr_st ppf (Ptset.elements a.init); 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 -> (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,_)) -> let s = 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"; 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*predicate let ( ?< ) x = x 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 end type transition = Transitions.t 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 = 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 } 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 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 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 Hashtbl.replace h_time s (cpt,atime); r 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 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 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 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 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_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 *)