1 (* Todo refactor and remove this alias *)
3 module Tree = Tree.Binary
16 let mk_state = State.mk
20 type predicate = [ `Left of (Tree.t -> bool) | `Right of (Tree.t -> bool) |
25 function `True -> true
26 | `Left f | `Right f -> f t
30 | Or of formula * formula
31 | And of formula * formula
32 | Atom of ([ `Left | `Right ]*bool*state)
33 and formula = { fid: int;
47 | And(f1,f2) -> 2+17*f1.fid + 37*f2.fid
48 | Or(f1,f2) -> 3+101*f1.fid + 253*f2.fid
49 | Atom(d,b,s) -> 5+(if d=`Left then 11 else 19)*(if b then 23 else 31)*s
51 let hash t = (hash t.pos) land max_int
54 match f1.pos,f2.pos with
55 | False,False | True,True -> true
56 | Atom(d1,b1,s1), Atom(d2,b2,s2) when (d1 = d2) && (b1=b2) &&(s1=s2) -> true
58 | And(g1,g2),And(h1,h2) -> g1.fid == h1.fid && g2.fid == h2.fid
61 module WH = Weak.Make(FormNode)
63 let f_pool = WH.create 107
66 let rec t = { fid = 1; pos = True; neg = f ; st = Ptset.empty,Ptset.empty; size =1; }
67 and f = { fid = 0; pos = False; neg = t; st = Ptset.empty,Ptset.empty; size = 1; }
73 let is_true f = f.fid == 1
74 let is_false f = f.fid == 0
77 let cons pos neg s1 s2 size1 size2 =
92 (WH.merge f_pool pnode),(WH.merge f_pool nnode)
95 let si = Ptset.singleton s in
97 | `Left -> si,Ptset.empty
98 | `Right -> Ptset.empty,si
99 in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
101 let merge_states f1 f2 =
103 Ptset.union (fst f1.st) (fst f2.st),
104 Ptset.union (snd f1.st) (snd f2.st)
106 Ptset.union (fst f1.neg.st) (fst f2.neg.st),
107 Ptset.union (snd f1.neg.st) (snd f2.neg.st)
112 let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
113 let sp,sn = merge_states f1 f2 in
114 let psize = f1.size + f2.size in
115 let nsize = f1.neg.size + f2.neg.size in
116 fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize )
119 let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
120 if is_true f1 || is_true f2 then true_
121 else if is_false f1 && is_false f2 then false_
122 else if is_false f1 then f2
123 else if is_false f2 then f1
125 let psize = f1.size + f2.size in
126 let nsize = f1.neg.size + f2.neg.size in
127 let sp,sn = merge_states f1 f2 in
128 fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize)
133 let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
134 if is_true f1 && is_true f2 then true_
135 else if is_false f1 || is_false f2 then false_
136 else if is_true f1 then f2
137 else if is_true f2 then f1
139 let psize = f1.size + f2.size in
140 let nsize = f1.neg.size + f2.neg.size in
141 let sp,sn = merge_states f1 f2 in
142 fst (cons (And(f1,f2)) (Or(f1.neg,f2.neg)) sp sn psize nsize)
150 type t = Ptset.t*Tag.t
151 let int_hash key = key lsl 31 lor (key lsl 8)
152 let equal (s1,s2) (t1,t2) = Tag.equal s2 t2 && Ptset.equal s1 t1
153 let hash (s,t) = int_hash (Ptset.hash s) lxor ( int_hash (Tag.hash t))
155 module HTagSet = Hashtbl.Make(HTagSetKey)
159 mutable states : Ptset.t;
161 mutable final : Ptset.t;
163 (* Transitions of the Alternating automaton *)
164 phi : (state,(TagSet.t*(bool*formula*predicate)) list) Hashtbl.t;
165 delta : (state*Tag.t, (bool*formula*predicate)) Hashtbl.t;
166 (* delta : (state,(bool*formula*predicate) TagMap.t) Hashtbl.t; *)
167 sigma : (bool*formula*(predicate list*predicate list)*bool) HTagSet.t;
170 module Pair (X : Set.OrderedType) (Y : Set.OrderedType) =
173 let compare (x1,y1) (x2,y2) =
174 let r = X.compare x1 x2 in
175 if r == 0 then Y.compare y1 y2
179 module PL = Set.Make (Pair (Ptset) (Ptset))
182 let pr_st ppf l = Format.fprintf ppf "{";
186 | [s] -> Format.fprintf ppf " %i" s
187 | p::r -> Format.fprintf ppf " %i" p;
188 List.iter (fun i -> Format.fprintf ppf "; %i" i) r
190 Format.fprintf ppf " }"
191 let rec pr_frm ppf f = match f.pos with
192 | True -> Format.fprintf ppf "⊤"
193 | False -> Format.fprintf ppf "⊥"
195 Format.fprintf ppf "(";
197 Format.fprintf ppf ") ∧ (";
199 Format.fprintf ppf ")"
202 Format.fprintf ppf " ∨ ";
204 | Atom(dir,b,s) -> Format.fprintf ppf "%s%s[%i]"
205 (if b then "" else "¬")
206 (if dir = `Left then "↓₁" else "↓₂") s
208 let dnf_hash = Hashtbl.create 17
210 let rec dnf_aux f = match f.pos with
212 | True -> PL.singleton (Ptset.empty,Ptset.empty)
213 | Atom(`Left,_,s) -> PL.singleton (Ptset.singleton s,Ptset.empty)
214 | Atom(`Right,_,s) -> PL.singleton (Ptset.empty,Ptset.singleton s)
215 | Or(f1,f2) -> PL.union (dnf f1) (dnf f2)
220 PL.fold (fun (s1,s2) acc ->
221 PL.fold ( fun (s1', s2') acc' ->
223 ((Ptset.union s1 s1'),
224 (Ptset.union s2 s2')) acc') )
231 Hashtbl.find dnf_hash f.fid
235 Hashtbl.add dnf_hash f.fid d;d
240 if (PL.cardinal nf > 3)then None
241 else match PL.elements nf with
242 | [(s1,s2); (t1,t2); (u1,u2)] when
243 Ptset.is_empty s1 && Ptset.is_empty s2 && Ptset.is_empty t1 && Ptset.is_empty u2
245 | [(t1,t2); (u1,u2)] when Ptset.is_empty t1 && Ptset.is_empty u2
250 let equal_form f1 f2 =
251 (f1.fid == f2.fid) || (FormNode.equal f1 f2) || (PL.equal (dnf f1) (dnf f2))
254 Format.fprintf ppf "Automaton (%i) :\n" a.id;
255 Format.fprintf ppf "States : "; pr_st ppf (Ptset.elements a.states);
256 Format.fprintf ppf "\nInitial states : "; pr_st ppf (Ptset.elements a.init);
257 Format.fprintf ppf "\nFinal states : "; pr_st ppf (Ptset.elements a.final);
258 Format.fprintf ppf "\nUniversal states : "; pr_st ppf (Ptset.elements a.universal);
259 Format.fprintf ppf "\nAlternating transitions :\n------------------------------\n";
260 let l = Hashtbl.fold (fun k t acc ->
261 (List.map (fun (t,(m,f,p)) -> (t,k),(m,f,p)) t)@ acc) a.phi [] in
262 let l = List.sort (fun ((tsx,x),_) ((tsy,y),_) -> if x-y == 0 then TagSet.compare tsx tsy else x-y) l in
263 List.iter (fun ((ts,q),(b,f,_)) ->
266 if TagSet.is_finite ts
267 then "{" ^ (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) ts "") ^"}"
268 else let cts = TagSet.neg ts in
269 if TagSet.is_empty cts then "*" else
270 (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) cts "*\\{"
273 Format.fprintf ppf "(%s,%i) %s " s q (if b then "=>" else "->");
275 Format.fprintf ppf "\n")l;
277 Format.fprintf ppf "NFA transitions :\n------------------------------\n";
278 HTagSet.iter (fun (qs,t) (b,f,_,_) ->
279 pr_st ppf (Ptset.elements qs);
280 Format.fprintf ppf ",%s %s " (Tag.to_string t) (if b then "=>" else "->");
282 Format.fprintf ppf "(fid=%i) left=" f.fid;
283 let l,r = f.st in pr_st ppf (Ptset.elements l);
284 Format.fprintf ppf ", right=";
285 pr_st ppf (Ptset.elements r);
286 Format.fprintf ppf "\n";
288 Format.fprintf ppf "=======================================\n"
290 module Transitions = struct
291 type t = state*TagSet.t*bool*formula*predicate
293 let ( >< ) state (l,b) = state,(l,b,`True)
294 let ( ><@ ) state (l,b,p) = state,(l,b,p)
295 let ( >=> ) (state,(label,mark,pred)) form = (state,label,mark,form,pred)
296 let ( +| ) f1 f2 = or_ f1 f2
297 let ( *& ) f1 f2 = and_ f1 f2
298 let ( ** ) d s = atom_ d true s
302 type transition = Transitions.t
304 let equal_trans (q1,t1,m1,f1,_) (q2,t2,m2,f2,_) =
305 (q1 == q2) && (TagSet.equal t1 t2) && (m1 == m2) && (equal_form f1 f2)
309 type node = Nil | Cons of Tree.t * node | Concat of node*node
310 and t = { node : node; size : int }
311 let node n s = { node=n; size = s }
313 let empty = node Nil 0
315 let cons e t = node (Cons(e,t.node)) (t.size+1)
316 let concat t1 t2 = node (Concat (t1.node,t2.node)) (t1.size+t2.size)
317 let append e t = concat t (cons e empty)
320 let rec aux acc l rest =
325 | Cons(e,t) -> aux (e::acc) t Nil
326 | Concat(t1,t2) -> aux acc t1 t2
328 | Cons(e,r) -> aux (e::acc) r rest
329 | Concat(t1,t2) -> aux acc t1 (Concat(t2,rest))
332 let length = function { size = s } -> s
334 let iter f { node = n } =
335 let rec loop = function
337 | Cons(e,n) -> let _ = f e in loop n
338 | Concat(n1,n2) -> let _ = loop n1 in loop n2
344 module BottomUpNew = struct
349 | TNil of Ptset.t*Ptset.t
350 | TNode of Ptset.t*Ptset.t*bool* (int*bool*formula) list
352 let traces = Hashtbl.create 17
354 let out = open_out "debug_trace.dot"
356 let outf = Format.formatter_of_out_channel out in
361 match (try Hashtbl.find traces (Tree.id t) with Not_found -> TNil(Ptset.empty,Ptset.empty)) with
362 | TNode(r,s,mark,trs) ->
363 let numl = aux (Tree.left t) num in
364 let numr = aux (Tree.right t) (numl+1) in
365 let mynum = numr + 1 in
366 Format.fprintf outf "n%i [ label=\"<%s>\\nr=" mynum (Tag.to_string (Tree.tag t));
367 pr_st outf (Ptset.elements r);
368 Format.fprintf outf "\\ns=";
369 pr_st outf (Ptset.elements s);
370 List.iter (fun (q,m,f) ->
371 Format.fprintf outf "\\n%i %s" q (if m then "⇨" else "→");
373 Format.fprintf outf "\", %s shape=box ];\n"
374 (if mark then "color=cyan1, style=filled," else "");
375 let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numl in
376 let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numr in
378 | TNil(r,s) -> Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num;
379 pr_st outf (Ptset.elements r);
380 Format.fprintf outf "\\ns=";
381 pr_st outf (Ptset.elements s);
382 Format.fprintf outf "\"];\n";num
384 match Hashtbl.find traces (-10) with
386 Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num;
387 pr_st outf (Ptset.elements r);
388 Format.fprintf outf "\\ns=";
389 pr_st outf (Ptset.elements s);
390 Format.fprintf outf "\"];\n";
395 Format.fprintf outf "digraph G {\n";
397 Format.fprintf outf "}\n%!";
399 ignore(Sys.command "dot -Tsvg debug_trace.dot > debug_trace.svg")
404 module HFEval = Hashtbl.Make(
406 type t = int*Ptset.t*Ptset.t
407 let equal (a,b,c) (d,e,f) =
408 a==d && (Ptset.equal b e) && (Ptset.equal c f)
410 a+17*(Ptset.hash b) + 31*(Ptset.hash c)
413 let hfeval = HFEval.create 4097
416 let eval_form_bool f s1 s2 =
417 let rec eval f = match f.pos with
418 | Atom(`Left,b,q) -> if b == (Ptset.mem q s1) then (true,true,false) else false,false,false
419 | Atom(`Right,b,q) -> if b == (Ptset.mem q s2) then (true,false,true) else false,false,false
420 (* test some inlining *)
421 | True -> true,true,true
422 | False -> false,false,false
425 HFEval.find hfeval (f.fid,s1,s2)
427 | Not_found -> let r =
430 let b1,rl1,rr1 = eval f1
432 if b1 && rl1 && rr1 then (true,true,true)
434 let b2,rl2,rr2 = eval f2
436 let rl1,rr1 = if b1 then rl1,rr1 else false,false
437 and rl2,rr2 = if b2 then rl2,rr2 else false,false
438 in (b1 || b2, rl1||rl2,rr1||rr2)
440 let b1,rl1,rr1 = eval f1 in
441 if b1 && rl1 && rr1 then (true,true,true)
443 then let b2,rl2,rr2 = eval f2 in
444 if b2 then (true,rl1||rl2,rr1||rr2)
445 else (false,false,false)
446 else (false,false,false)
449 HFEval.add hfeval (f.fid,s1,s2) r;
454 module HFEvalDir = Hashtbl.Make(
456 type t = int*Ptset.t*[`Left | `Right ]
457 let equal (a,b,c) (d,e,f) =
458 a==d && (Ptset.equal b e) && (c = f)
459 let hash_dir = function `Left -> 7919
463 a+17*(Ptset.hash b) + 31*(hash_dir c)
466 let hfeval_dir = HFEvalDir.create 4097
469 let eval_dir dir f s =
470 let rec eval f = match f.pos with
471 | Atom(d,b,q) when d = dir -> if b == (Ptset.mem q s) then true_ else false_
473 (* test some inlining *)
478 HFEvalDir.find hfeval_dir (f.fid,s,dir)
486 if is_true f1 then true_
487 else if is_false f1 then eval f2
491 if is_false f1 then false_
492 else if is_true f1 then eval f2
496 HFEvalDir.add hfeval_dir (f.fid,s,dir) r;
503 let fstate_pool = Hashtbl.create 11
505 let merge_pred a b = match a,b with
506 | Some(f1), Some(f2) -> Some(fun x -> f1 x || f2 x)
511 let acc_pred p l1 l2 = match p with
512 | `Left _ -> p::l1,l2
513 | `Right _ -> l1,p::l2
517 let merge_trans t a tag q acc =
518 List.fold_left (fun (accf,accm,acchtrue) (ts,(m,f,pred)) ->
524 try Hashtbl.find fstate_pool f.fid with
525 | Not_found -> let s = mk_state() in
526 a.states <- Ptset.add s a.states;
527 a.final <- Ptset.add s a.final;
528 Hashtbl.add fstate_pool f.fid s;s
530 (atom_ `Left true newfinal),true
532 (or_ tmpf accf,accm||m,acchtrue||hastrue)
533 else (accf,accm,acchtrue)
534 ) acc (Hashtbl.find a.phi q)
538 let get_trans t a tag r =
540 let mark,f,predl,has_true =
541 HTagSet.find a.sigma (r,tag)
542 in f.st,f,mark,has_true,r,predl
545 let f,mark,has_true,accq =
546 Ptset.fold (fun q (accf,accm,acchtrue,accq) ->
547 let naccf,naccm,nacctrue =
548 merge_trans t a tag q (accf,accm,acchtrue )
550 if is_false naccf then (naccf,naccm,nacctrue,accq)
551 else (naccf,naccm,nacctrue,Ptset.add q accq)
553 r (false_,false,false,Ptset.empty)
555 HTagSet.add a.sigma (accq,tag) (mark,f,([],[]),has_true);
556 f.st,f,mark,has_true,accq,([],[])
559 let check_pred l t = true (*l = [] ||
560 List.exists (function p ->
562 `Left f | `Right f -> f t
563 | _ -> assert false) l
567 let rec accepting_among2 a t r acc =
569 let rest = Ptset.inter r a.final in
570 let r = Ptset.diff r rest in
571 if Ptset.is_empty r then rest,acc else
572 if (not (Tree.is_node t))
576 let tag = Tree.tag t in
577 let t1 = Tree.first_child t
578 and t2 = Tree.next_sibling t in
579 let (r1,r2),formula,mark,has_true,r,_ = get_trans t a tag r
581 let s1,res1 = accepting_among2 a t1 r1 acc
583 let formula = eval_dir `Left formula s1 in
584 if is_false formula then rest,acc
586 if is_true formula then (* tail call equivalent to a top down *)
587 accepting_among2 a t2 orig (if mark then TS.append t res1 else res1)
589 let s2,res2 = accepting_among2 a t2 r2 res1
591 let formula = eval_dir `Right formula s2
593 if is_false formula then rest,res1
595 orig,(if mark then TS.append t (res2)
600 let st,res = accepting_among2 a t a.init TS.empty in
601 let b = Ptset.is_empty (st) in