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