ata.ml

   1 (* Todo refactor and remove this alias *)
   2 INCLUDE "debug.ml"
   3 module Tree = Tree.Binary
   4
   5
   6 let gen_id =
   7   let id = ref (-1) in
   8     fun () -> incr id;!id
   9
  10
  11 module State = struct
  12
  13   type t = int
  14   let mk = gen_id
  15
  16 end
  17 let mk_state = State.mk
  18
  19 type state = State.t
  20
  21 type predicate = [ `Left of (Tree.t -> bool) | `Right of (Tree.t -> bool) |
  22                        `True
  23                  ]
  24
  25 let eval_pred t =
  26   function `True -> true
  27     | `Left f | `Right f -> f t
  28
  29 type formula_expr =
  30   | False | True
  31   | Or of formula * formula
  32   | And of formula * formula
  33   | Atom of ([ `Left | `Right ]*bool*state)
  34 and formula = { fid: int;
  35                 pos : formula_expr;
  36                 neg : formula;
  37                 st : Ptset.t*Ptset.t;
  38                 size: int;
  39               }
  40
  41
  42 module FormNode =
  43 struct
  44   type t = formula
  45   let hash = function
  46     | False -> 0
  47     | True -> 1
  48     | And(f1,f2) -> 2+17*f1.fid + 37*f2.fid
  49     | Or(f1,f2) -> 3+101*f1.fid + 253*f2.fid
  50     | Atom(d,b,s) -> 5+(if d=`Left then 11 else 19)*(if b then 23 else 31)*s
  51
  52   let hash t = (hash t.pos) land max_int
  53
  54   let equal f1 f2 =
  55     match f1.pos,f2.pos with
  56       | False,False | True,True -> true
  57       | Atom(d1,b1,s1), Atom(d2,b2,s2) when (d1 = d2) && (b1=b2) &&(s1=s2) -> true
  58       | Or(g1,g2),Or(h1,h2)
  59       | And(g1,g2),And(h1,h2)  -> g1.fid == h1.fid && g2.fid == h2.fid
  60       | _ -> false
  61 end
  62 module WH = Weak.Make(FormNode)
  63
  64 let f_pool = WH.create 107
  65
  66 let true_,false_ =
  67   let rec t = { fid = 1; pos = True; neg = f ; st = Ptset.empty,Ptset.empty; size =1; }
  68   and f = { fid = 0; pos = False; neg = t; st = Ptset.empty,Ptset.empty; size = 1; }
  69   in
  70     WH.add f_pool f;
  71     WH.add f_pool t;
  72     t,f
  73
  74 let is_true f = f.fid == 1
  75 let is_false f = f.fid == 0
  76
  77
  78 let cons pos neg s1 s2 size1 size2 =
  79   let rec pnode =
  80     { fid = gen_id ();
  81       pos = pos;
  82       neg = nnode;
  83       st = s1;
  84       size = size1;}
  85   and nnode = {
  86     fid = gen_id ();
  87     pos = neg;
  88     neg = pnode;
  89     st = s2;
  90     size = size2;
  91   }
  92   in
  93     (WH.merge f_pool pnode),(WH.merge f_pool nnode)
  94
  95 let atom_  d p s =
  96   let si = Ptset.singleton s in
  97   let ss = match d with
  98     | `Left -> si,Ptset.empty
  99     | `Right -> Ptset.empty,si
 100   in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
 101
 102 let merge_states f1 f2 =
 103   let sp =
 104     Ptset.union (fst f1.st) (fst f2.st),
 105     Ptset.union (snd f1.st) (snd f2.st)
 106   and sn =
 107     Ptset.union (fst f1.neg.st) (fst f2.neg.st),
 108     Ptset.union (snd f1.neg.st) (snd f2.neg.st)
 109   in
 110     sp,sn
 111
 112 let full_or_ f1 f2 =
 113   let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
 114   let sp,sn = merge_states f1 f2 in
 115   let psize = f1.size + f2.size in
 116   let nsize = f1.neg.size + f2.neg.size in
 117     fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize )
 118
 119 let or_ f1 f2 =
 120   let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
 121   if is_true f1 || is_true f2 then true_
 122   else if is_false f1 && is_false f2 then false_
 123   else if is_false f1 then f2
 124   else if is_false f2 then f1
 125   else
 126     let psize = f1.size + f2.size in
 127     let nsize = f1.neg.size + f2.neg.size in
 128     let sp,sn = merge_states f1 f2 in
 129       fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize)
 130
 131
 132
 133 let and_ f1 f2 =
 134   let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
 135   if is_true f1 && is_true f2 then true_
 136   else if is_false f1 || is_false f2 then false_
 137   else if is_true f1 then f2
 138   else if is_true f2 then f1
 139   else
 140     let psize = f1.size + f2.size in
 141     let nsize = f1.neg.size + f2.neg.size in
 142     let sp,sn = merge_states f1 f2 in
 143       fst (cons (And(f1,f2)) (Or(f1.neg,f2.neg)) sp sn psize nsize)
 144
 145
 146 let not_ f = f.neg
 147
 148
 149 module HTagSetKey =
 150 struct
 151   type t = Ptset.t*Tag.t
 152   let int_hash key = key lsl 31 lor (key lsl 8)
 153   let equal (s1,s2) (t1,t2) = Tag.equal s2 t2 &&  Ptset.equal s1 t1
 154   let hash (s,t) = int_hash (Ptset.hash s) lxor ( int_hash (Tag.hash t))
 155 end
 156 module HTagSet = Hashtbl.Make(HTagSetKey)
 157
 158 type t = {
 159     id : int;
 160     mutable states : Ptset.t;
 161     init : Ptset.t;
 162     mutable final : Ptset.t;
 163     universal : Ptset.t;
 164     (* Transitions of the Alternating automaton *)
 165     phi : (state,(TagSet.t*(bool*formula*predicate)) list) Hashtbl.t;
 166     delta : (state*Tag.t, (bool*formula*predicate)) Hashtbl.t;
 167 (*    delta : (state,(bool*formula*predicate) TagMap.t) Hashtbl.t; *)
 168     sigma : (bool*formula*(predicate list*predicate list)*bool) HTagSet.t;
 169   }
 170
 171   module Pair (X : Set.OrderedType) (Y : Set.OrderedType) =
 172   struct
 173     type t = X.t*Y.t
 174     let compare (x1,y1) (x2,y2) =
 175       let r = X.compare x1 x2 in
 176         if r == 0 then Y.compare y1 y2
 177         else r
 178   end
 179
 180   module PL = Set.Make (Pair (Ptset) (Ptset))
 181
 182
 183       let pr_st ppf l = Format.fprintf ppf "{";
 184     begin
 185       match l with
 186         |       [] -> ()
 187         | [s] -> Format.fprintf ppf " %i" s
 188         | p::r -> Format.fprintf ppf " %i" p;
 189             List.iter (fun i -> Format.fprintf ppf "; %i" i) r
 190     end;
 191     Format.fprintf ppf " }"
 192   let rec pr_frm ppf f = match f.pos with
 193     | True -> Format.fprintf ppf "⊤"
 194     | False -> Format.fprintf ppf "⊥"
 195     | And(f1,f2) ->
 196         Format.fprintf ppf "(";
 197         (pr_frm ppf f1);
 198         Format.fprintf ppf ") ∧ (";
 199         (pr_frm ppf f2);
 200         Format.fprintf ppf ")"
 201     | Or(f1,f2) ->
 202         (pr_frm ppf f1);
 203         Format.fprintf ppf " ∨ ";
 204         (pr_frm ppf f2);
 205     | Atom(dir,b,s) -> Format.fprintf ppf "%s%s[%i]"
 206         (if b then "" else "¬")
 207         (if dir = `Left then "↓₁" else "↓₂") s
 208
 209   let dnf_hash = Hashtbl.create 17
 210
 211   let rec dnf_aux f = match f.pos with
 212     | False -> PL.empty
 213     | True -> PL.singleton (Ptset.empty,Ptset.empty)
 214     | Atom(`Left,_,s) -> PL.singleton (Ptset.singleton s,Ptset.empty)
 215     | Atom(`Right,_,s) -> PL.singleton (Ptset.empty,Ptset.singleton s)
 216     | Or(f1,f2) -> PL.union (dnf f1) (dnf f2)
 217     | And(f1,f2) ->
 218           let pl1 = dnf f1
 219           and pl2 = dnf f2
 220           in
 221             PL.fold (fun (s1,s2) acc ->
 222                        PL.fold ( fun (s1', s2') acc' ->
 223                                    (PL.add
 224                                       ((Ptset.union s1 s1'),
 225                                        (Ptset.union s2 s2')) acc') )
 226                           pl2 acc )
 227               pl1 PL.empty
 228
 229
 230   and dnf f =
 231     try
 232       Hashtbl.find dnf_hash f.fid
 233     with
 234         Not_found ->
 235           let d = dnf_aux f in
 236             Hashtbl.add dnf_hash f.fid d;d
 237
 238
 239   let can_top_down f =
 240     let nf = dnf f in
 241       if (PL.cardinal nf > 3)then None
 242       else match PL.elements nf with
 243         | [(s1,s2); (t1,t2); (u1,u2)] when
 244             Ptset.is_empty s1 && Ptset.is_empty s2 && Ptset.is_empty t1 && Ptset.is_empty u2
 245               -> Some(true,t2,u1)
 246         | [(t1,t2); (u1,u2)] when Ptset.is_empty t1 && Ptset.is_empty u2
 247             -> Some(false,t2,u1)
 248         | _ -> None
 249
 250
 251   let equal_form f1 f2 =
 252     (f1.fid == f2.fid) || (FormNode.equal f1 f2) || (PL.equal (dnf f1) (dnf f2))
 253
 254   let dump ppf a =
 255     Format.fprintf ppf "Automaton (%i) :\n" a.id;
 256     Format.fprintf ppf "States : "; pr_st ppf (Ptset.elements a.states);
 257     Format.fprintf ppf "\nInitial states : "; pr_st ppf (Ptset.elements a.init);
 258     Format.fprintf ppf "\nFinal states : "; pr_st ppf (Ptset.elements a.final);
 259     Format.fprintf ppf "\nUniversal states : "; pr_st ppf (Ptset.elements a.universal);
 260     Format.fprintf ppf "\nAlternating transitions :\n------------------------------\n";
 261     let l = Hashtbl.fold (fun k t acc ->
 262                             (List.map (fun (t,(m,f,p)) -> (t,k),(m,f,p)) t)@ acc) a.phi [] in
 263     let l = List.sort (fun ((tsx,x),_) ((tsy,y),_) -> if x-y == 0 then TagSet.compare tsx tsy else x-y) l in
 264     List.iter (fun ((ts,q),(b,f,_)) ->
 265
 266                     let s =
 267                       if TagSet.is_finite ts
 268                       then "{" ^ (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) ts "") ^"}"
 269                       else let cts = TagSet.neg ts in
 270                         if TagSet.is_empty cts then "*" else
 271                           (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) cts "*\\{"
 272                           )^ "}"
 273                     in
 274                       Format.fprintf ppf "(%s,%i) %s " s q (if b then "=>" else "->");
 275                       pr_frm ppf f;
 276                       Format.fprintf ppf "\n")l;
 277
 278     Format.fprintf ppf "NFA transitions :\n------------------------------\n";
 279     HTagSet.iter (fun (qs,t) (b,f,_,_) ->
 280                     pr_st ppf (Ptset.elements qs);
 281                     Format.fprintf ppf ",%s  %s " (Tag.to_string t) (if b then "=>" else "->");
 282                     pr_frm ppf f;
 283                     Format.fprintf ppf "(fid=%i) left=" f.fid;
 284                     let l,r = f.st in pr_st ppf (Ptset.elements l);
 285                       Format.fprintf ppf ", right=";
 286                       pr_st ppf (Ptset.elements r);
 287                       Format.fprintf ppf "\n";
 288                  ) a.sigma;
 289     Format.fprintf ppf "=======================================\n"
 290
 291   module Transitions = struct
 292     type t = state*TagSet.t*bool*formula*predicate
 293     let ( ?< ) x = x
 294     let ( >< ) state (l,b) = state,(l,b,`True)
 295     let ( ><@ ) state (l,b,p) = state,(l,b,p)
 296     let ( >=> ) (state,(label,mark,pred)) form = (state,label,mark,form,pred)
 297     let ( +| ) f1 f2 = or_ f1 f2
 298     let ( *& ) f1 f2 = and_ f1 f2
 299     let ( ** ) d s = atom_ d true s
 300
 301
 302   end
 303   type transition = Transitions.t
 304
 305   let equal_trans (q1,t1,m1,f1,_) (q2,t2,m2,f2,_) =
 306     (q1 == q2) && (TagSet.equal t1 t2) && (m1 == m2) && (equal_form f1 f2)
 307
 308   module TS =
 309   struct
 310     type node = Nil | Cons of Tree.t * node | Concat of node*node
 311     and t = { node : node; size : int }
 312     let node n s = { node=n; size = s }
 313
 314     let empty = node Nil 0
 315
 316     let cons e t = node (Cons(e,t.node)) (t.size+1)
 317     let concat t1 t2 = node (Concat (t1.node,t2.node)) (t1.size+t2.size)
 318     let append e t = concat t (cons e empty)
 319
 320     let to_list_rev t =
 321       let rec aux acc l rest =
 322         match l with
 323           | Nil -> begin
 324               match rest with
 325                 | Nil -> acc
 326                 | Cons(e,t) -> aux (e::acc) t Nil
 327                 | Concat(t1,t2) -> aux acc t1 t2
 328             end
 329           | Cons(e,r) -> aux (e::acc) r rest
 330           | Concat(t1,t2) -> aux acc t1 (Concat(t2,rest))
 331       in
 332     aux [] t.node Nil
 333
 334     let length = function { size = s } -> s
 335
 336     let iter f { node = n } =
 337       let rec loop = function
 338         | Nil -> ()
 339         | Cons(e,n) -> let _ = f e in loop n
 340         | Concat(n1,n2) -> let _ = loop n1 in loop n2
 341       in loop n
 342
 343   end
 344   module TS2 =
 345   struct
 346     type t = string
 347     let empty = String.make  10_000_000 '0'
 348     let cons e t = t.[Tree.id e] <- '1';t
 349     let append = cons
 350     let concat s1 s2 = failwith "not implemented"
 351
 352     let length t =
 353       let res = ref 0 in
 354         for i = 0 to 9_999_999 do
 355           if t.[i] == '1' then
 356             incr res
 357         done; !res
 358
 359     let iter f t =  failwith "not implemented"
 360     let to_list_rev t = failwith "not implemented"
 361   end
 362
 363   module BottomUpNew = struct
 364
 365 IFDEF DEBUG
 366 THEN
 367     type trace =
 368       | TNil of Ptset.t*Ptset.t
 369       | TNode of Ptset.t*Ptset.t*bool* (int*bool*formula) list
 370
 371     let traces = Hashtbl.create 17
 372     let dump_trace t =
 373       let out = open_out "debug_trace.dot"
 374       in
 375       let outf = Format.formatter_of_out_channel out in
 376
 377       let rec aux t num =
 378         if Tree.is_node t
 379         then
 380           match (try Hashtbl.find traces (Tree.id t) with Not_found -> TNil(Ptset.empty,Ptset.empty)) with
 381             | TNode(r,s,mark,trs) ->
 382                 let numl = aux (Tree.left t) num in
 383                 let numr = aux (Tree.right t) (numl+1) in
 384                 let mynum = numr + 1 in
 385                   Format.fprintf outf "n%i [ label=\"<%s>\\nr=" mynum (Tag.to_string (Tree.tag t));
 386                   pr_st outf (Ptset.elements r);
 387                   Format.fprintf outf "\\ns=";
 388                   pr_st outf (Ptset.elements s);
 389                   List.iter (fun (q,m,f) ->
 390                                Format.fprintf outf "\\n%i %s" q (if m then "⇨" else "→");
 391                                pr_frm outf f ) trs;
 392                   Format.fprintf outf "\", %s shape=box ];\n"
 393                     (if mark then "color=cyan1, style=filled," else "");
 394                   let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numl in
 395                   let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numr in
 396                   mynum
 397             | TNil(r,s) -> Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num;
 398                 pr_st outf (Ptset.elements r);
 399                 Format.fprintf outf "\\ns=";
 400                 pr_st outf (Ptset.elements s);
 401                 Format.fprintf outf "\"];\n";num
 402         else
 403           match Hashtbl.find traces (-10) with
 404             | TNil(r,s) ->
 405                 Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num;
 406                 pr_st outf (Ptset.elements r);
 407                 Format.fprintf outf "\\ns=";
 408                 pr_st outf (Ptset.elements s);
 409                 Format.fprintf outf "\"];\n";
 410                 num
 411             | _ -> assert false
 412
 413       in
 414         Format.fprintf outf "digraph G {\n";
 415         ignore(aux t 0);
 416         Format.fprintf outf "}\n%!";
 417         close_out out;
 418         ignore(Sys.command "dot -Tsvg debug_trace.dot > debug_trace.svg")
 419 END
 420
 421
 422
 423     module HFEval = Hashtbl.Make(
 424       struct
 425         type t = int*Ptset.t*Ptset.t
 426         let equal (a,b,c) (d,e,f) =
 427           a==d && (Ptset.equal b e) && (Ptset.equal c f)
 428         let hash (a,b,c) =
 429           a+17*(Ptset.hash b) + 31*(Ptset.hash c)
 430       end)
 431
 432     let hfeval = HFEval.create 4097
 433
 434
 435 (*    let miss = ref 0
 436     let call = ref 0
 437     let timeref = ref 0.0
 438     let timerefall = ref 0.0
 439     let time f x =
 440       incr call;
 441       let t1 =  Unix.gettimeofday ()
 442       in let r = f x
 443       in
 444         timeref := !timeref +. ((Unix.gettimeofday()) -. t1);
 445         r
 446
 447     let timeall f x =
 448       let t1 =  Unix.gettimeofday ()
 449       in let r = f x
 450       in
 451         timerefall := !timerefall +. ((Unix.gettimeofday()) -. t1);
 452         r
 453
 454 *)
 455
 456
 457     let eval_form_bool f s1 s2 =
 458       let rec eval f = match f.pos with
 459         | Atom(`Left,b,q) -> if b == (Ptset.mem q s1) then (true,true,false) else false,false,false
 460         | Atom(`Right,b,q) -> if b == (Ptset.mem q s2) then (true,false,true) else false,false,false
 461             (* test some inlining *)
 462         | True -> true,true,true
 463         | False -> false,false,false
 464         | _ ->
 465             try
 466                HFEval.find hfeval (f.fid,s1,s2)
 467             with
 468               | Not_found -> let r =
 469                   match f.pos with
 470                     | Or(f1,f2) ->
 471                         let b1,rl1,rr1 = eval f1
 472                         in
 473                           if b1 && rl1 && rr1 then (true,true,true)
 474                           else
 475                             let b2,rl2,rr2 = eval f2
 476                             in
 477                             let rl1,rr1 = if b1 then rl1,rr1 else false,false
 478                             and rl2,rr2 = if b2 then rl2,rr2 else false,false
 479                             in (b1 || b2, rl1||rl2,rr1||rr2)
 480                     | And(f1,f2) ->
 481                         let b1,rl1,rr1 = eval f1 in
 482                           if b1 && rl1 && rr1 then (true,true,true)
 483                           else if b1
 484                           then let b2,rl2,rr2 = eval f2 in
 485                             if b2 then (true,rl1||rl2,rr1||rr2)
 486                             else (false,false,false)
 487                           else (false,false,false)
 488                     | _ -> assert false
 489                 in
 490                   HFEval.add hfeval (f.fid,s1,s2) r;
 491                   r
 492       in eval f
 493
 494
 495     module HFEvalDir = Hashtbl.Make(
 496       struct
 497         type t = int*Ptset.t*[`Left | `Right ]
 498         let equal (a,b,c) (d,e,f) =
 499           a==d && (Ptset.equal b e) && (c = f)
 500         let hash_dir = function `Left -> 7919
 501           | `Right -> 3517
 502
 503         let hash (a,b,c) =
 504           a+17*(Ptset.hash b) + 31*(hash_dir c)
 505       end)
 506
 507     let hfeval_dir = HFEvalDir.create 4097
 508
 509
 510     let eval_dir dir f s =
 511       let rec eval f = match f.pos with
 512         | Atom(d,b,q) when d = dir -> if b == (Ptset.mem q s) then true_ else false_
 513         | Atom(_,b,q) -> f
 514             (* test some inlining *)
 515         | True -> true_
 516         | False -> false_
 517         | _ ->
 518             try
 519               HFEvalDir.find hfeval_dir (f.fid,s,dir)
 520             with
 521               | Not_found ->
 522                   let r =
 523                     match f.pos with
 524                       | Or(f1,f2) ->
 525                           let f1 = eval f1
 526                           in
 527                             if is_true f1 then true_
 528                             else if is_false f1 then eval f2
 529                             else or_ f1 f2
 530                       | And(f1,f2) ->
 531                           let f1 = eval f1 in
 532                             if is_false f1 then false_
 533                             else if is_true f1 then eval f2
 534                             else and_ f1 f2
 535                       | _ -> assert false
 536                   in
 537                     HFEvalDir.add hfeval_dir (f.fid,s,dir) r;
 538                     r
 539
 540       in eval f
 541
 542
 543
 544     let fstate_pool = Hashtbl.create 11
 545
 546     let merge_pred a b = match a,b with
 547       | Some(f1), Some(f2) -> Some(fun x -> f1 x || f2 x)
 548       | None,None -> None
 549       | None,Some(_) -> b
 550       | Some(_),None -> a
 551
 552     let acc_pred p l1 l2 = match p with
 553       | `Left _ -> p::l1,l2
 554       | `Right _ -> l1,p::l2
 555       | _ -> l1,l2
 556
 557
 558     let merge_trans t a tag q acc =
 559       List.fold_left (fun (accf,accm,acchtrue) (ts,(m,f,pred)) ->
 560                         if TagSet.mem tag ts
 561                         then
 562                           let tmpf,hastrue =
 563                             if is_true f then
 564                               let newfinal =
 565                                 try Hashtbl.find fstate_pool f.fid with
 566                                   | Not_found -> let s = mk_state() in
 567                                       a.states <- Ptset.add s a.states;
 568                                       a.final <- Ptset.add s a.final;
 569                                       Hashtbl.add fstate_pool f.fid s;s
 570                               in
 571                                 (atom_ `Left true newfinal),true
 572                             else f,false in
 573                             (or_ tmpf accf,accm||m,acchtrue||hastrue)
 574                         else (accf,accm,acchtrue)
 575                      ) acc (Hashtbl.find a.phi q)
 576
 577
 578     let get_trans t a tag r =
 579       try
 580         let mark,f,predl,has_true =
 581           HTagSet.find a.sigma (r,tag)
 582         in f.st,f,mark,has_true,r
 583       with
 584           Not_found ->
 585             let f,mark,has_true,accq =
 586               Ptset.fold (fun q (accf,accm,acchtrue,accq) ->
 587                             let naccf,naccm,nacctrue =
 588                               merge_trans t a tag q (accf,accm,acchtrue )
 589                             in
 590                               if is_false naccf then (naccf,naccm,nacctrue,accq)
 591                               else (naccf,naccm,nacctrue,Ptset.add q accq)
 592                          )
 593                 r (false_,false,false,Ptset.empty)
 594             in
 595               HTagSet.add a.sigma (accq,tag) (mark,f,([],[]),has_true);
 596               f.st,f,mark,has_true,accq
 597
 598
 599     let check_pred l t = true (*l = [] ||
 600       List.exists (function p ->
 601                      match p with
 602                          `Left f | `Right f -> f t
 603                        | _ -> assert false) l
 604                               *)
 605
 606
 607     let rec accepting_among2  a t r acc =
 608       let orig = r in
 609       let rest = Ptset.inter r a.final in
 610       let r = Ptset.diff r rest in
 611         if Ptset.is_empty r then rest,acc else
 612           if (not (Tree.is_node t))
 613           then
 614               orig,acc
 615           else
 616             let t1 = Tree.first_child t
 617             and t2 = Tree.next_sibling t in
 618             let (r1,r2),formula,mark,has_true,r = get_trans t a (Tree.tag t) r
 619             in
 620             let s1,res1 = accepting_among2 a t1 r1 acc
 621             in
 622             let formula = eval_dir `Left formula s1 in
 623               if is_false formula then rest,acc
 624               else
 625                 if is_true formula then (* tail call equivalent to a top down *)
 626                   accepting_among2 a t2 orig (if mark then TS.append t res1 else res1)
 627                 else
 628                   let s2,res2 = accepting_among2 a t2 r2 res1
 629                   in
 630                   let formula = eval_dir `Right formula s2
 631                   in
 632                     if is_false formula then rest,res1
 633                     else
 634                       orig,(if mark then TS.append t (res2)
 635                             else res2)
 636
 637
 638     let rec accepting_among a t r =
 639       let orig = r in
 640       let rest = Ptset.inter r a.final in
 641       let r = Ptset.diff r rest in
 642         if Ptset.is_empty r then rest,TS.empty else
 643           if Tree.is_node t
 644           then
 645             let (r1,r2),formula,mark,has_true,r = get_trans t a (Tree.tag t) r
 646             in
 647             let s1,res1 = accepting_among a (Tree.first_child t) r1
 648             and s2,res2 = accepting_among a (Tree.next_sibling t) r2
 649             in
 650             let rb,rb1,rb2 = eval_form_bool formula s1 s2 in
 651               if rb
 652               then
 653                 let res1 = if rb1 then res1 else TS.empty
 654                 and res2 = if rb2 then res2 else TS.empty
 655                 in r, TS.concat res2 (if mark then TS.cons t res1 else res1)
 656               else orig,TS.empty
 657           else orig,TS.empty
 658
 659
 660
 661
 662     let rec accepting_count a t r =
 663       let orig = r in
 664       let rest = Ptset.inter r a.final in
 665       let r = Ptset.diff r rest in
 666         if Ptset.is_empty r then rest,0 else
 667           if Tree.is_node t
 668           then
 669             let (r1,r2),formula,mark,has_true,r = get_trans t a (Tree.tag t) r
 670             in
 671             let s1,res1 = accepting_count a (Tree.first_child t) r1
 672             and s2,res2 = accepting_count a (Tree.next_sibling t) r2
 673             in
 674             let rb,rb1,rb2 = eval_form_bool formula s1 s2 in
 675               if rb
 676               then
 677                 let res1 = if rb1 then res1 else 0
 678                 and res2 = if rb2 then res2 else 0
 679                 in r, res1+res2+(if mark then 1 else 0)
 680               else orig,0
 681           else orig,0
 682
 683
 684     let run a t =
 685 (*      let _ =
 686         call := 0; miss:=0;
 687         timeref := 0.0;
 688         HFEval.clear hfeval;
 689         Hashtbl.clear dnf_hash;
 690         Hashtbl.clear fstate_pool;
 691       in *)
 692       let st,res = accepting_among a t a.init  in
 693       let b = Ptset.is_empty (st) in
 694         if b then TS.empty
 695         else
 696           res
 697
 698     let run_count a t =
 699 (*      let _ =
 700         call := 0; miss:=0;
 701         timeref := 0.0;
 702         timerefall := 0.0;
 703         HFEval.clear hfeval;
 704         Hashtbl.clear dnf_hash;
 705         Hashtbl.clear fstate_pool;
 706         in *)
 707       let st,res = accepting_count a t a.init  in
 708       let b = Ptset.is_empty (st) in
 709       if b then 0
 710       else
 711         res
 712   end
 713
 714   module Jump = struct
 715     let eval_dir = BottomUpNew.eval_dir
 716     let xi1 = HTagSet.create 10
 717     let xi2 = HTagSet.create 10
 718
 719
 720     let rec accept_from orig a t r acc =
 721       if (Tree.is_root t) ||
 722         (Ptset.subset orig r)
 723       then
 724         acc
 725       else
 726         let is_left = Tree.is_left t in
 727         let tag = Tree.tag t in
 728         let nr,f, mark =
 729           try
 730             HTagSet.find (if is_left then xi1 else xi2)
 731               (r,tag)
 732           with
 733             | Not_found ->
 734                 let trans =
 735                   Hashtbl.fold
 736                     (fun q l acc ->
 737                        List.fold_left (fun ((racc,facc,macc) as acc) (ts,(m,f,_)) ->
 738                                          let rl,rr = f.st in
 739                                          if (TagSet.mem tag ts) &&
 740                                            (Ptset.intersect (if is_left then rl else rr) r)
 741                                          then (Ptset.add q racc,or_ f facc, macc||m)
 742                                          else acc) acc l)
 743                     a.phi (Ptset.empty,false_,false)
 744
 745                 in
 746                   HTagSet.add (if is_left then xi1 else xi2) (r,tag) trans;
 747                   trans
 748         in
 749         let form = eval_dir (if is_left then `Left else `Right) f r
 750         in
 751           if is_true form then accept_from orig a (Tree.parent t) nr
 752             (if mark then TS.cons t acc else acc)
 753           else if is_false form then TS.empty
 754           else assert false
 755
 756     let run a t r =
 757       HTagSet.clear xi1;
 758       HTagSet.clear xi2;
 759       let orig =
 760         List.fold_left (fun s (_,(_,f,_)) ->
 761                           Ptset.union s (fst f.st))
 762           Ptset.empty (Hashtbl.find a.phi (Ptset.choose a.init))
 763       in
 764         accept_from orig a t r TS.empty
 765
 766
 767   end