ata.ml

   1 INCLUDE "debug.ml"
   2 INCLUDE "utils.ml"
   3
   4 let cpt_trans = ref 0
   5 let miss_trans = ref 0
   6 let cpt_eval = ref 0
   7 let miss_eval = ref 0
   8
   9 let gen_id =
  10   let id = ref (-1) in
  11     fun () -> incr id;!id
  12
  13 let h_union = Hashtbl.create 4097
  14
  15 let pt_cup s1 s2 =
  16   (* special case, since this is a union we want hash(s1,s2) = hash(s2,s1) *)
  17   let x = Ptset.hash s1
  18   and y = Ptset.hash s2 in
  19   let h = if x < y then HASHINT2(x,y) else HASHINT2(y,x) in
  20     try
  21       Hashtbl.find h_union h
  22     with
  23       | Not_found -> let s = Ptset.union s1 s2
  24         in
  25           Hashtbl.add h_union h s;s
  26
  27 module State = struct
  28
  29   type t = int
  30   let mk = gen_id
  31
  32 end
  33 let mk_state = State.mk
  34
  35 type state = State.t
  36
  37
  38
  39 type formula_expr =
  40   | False | True
  41   | Or of formula * formula
  42   | And of formula * formula
  43   | Atom of ([ `Left | `Right  | `LLeft | `RRight  ]*bool*state)
  44 and formula = { fid: int;
  45                 fkey : int;
  46                 pos : formula_expr;
  47                 neg : formula;
  48                 st : (Ptset.t*Ptset.t*Ptset.t)*(Ptset.t*Ptset.t*Ptset.t);
  49                 size: int;
  50               }
  51
  52 external hash_const_variant : [> ] -> int = "%identity"
  53 external vb : bool -> int = "%identity"
  54
  55 let hash_node_form t = match t with
  56   | False -> 0
  57   | True -> 1
  58   | And(f1,f2) -> (2+17*f1.fkey + 37*f2.fkey) (*land max_int *)
  59   | Or(f1,f2) -> (3+101*f1.fkey + 253*f2.fkey) (*land max_int *)
  60   | Atom(v,b,s) -> HASHINT3(hash_const_variant v,(3846*(vb b) +257),s)
  61
  62
  63
  64 module FormNode =
  65 struct
  66   type t = formula
  67
  68   let hash t = t.fkey
  69   let equal f1 f2 =
  70     if f1.fid == f2.fid || f1.fkey == f2.fkey || f1.pos == f2.pos then true
  71     else
  72     match f1.pos,f2.pos with
  73       | False,False | True,True -> true
  74       | Atom(d1,b1,s1), Atom(d2,b2,s2) when (b1==b2) &&  (s1==s2) && (d1 = d2) -> true
  75       | Or(g1,g2),Or(h1,h2)
  76       | And(g1,g2),And(h1,h2)  -> g1.fid == h1.fid && g2.fid == h2.fid
  77       | _ -> false
  78
  79 end
  80 module WH = Weak.Make(FormNode)
  81
  82 let f_pool = WH.create 107
  83
  84 let empty_triple = Ptset.empty,Ptset.empty,Ptset.empty
  85 let empty_hex = empty_triple,empty_triple
  86
  87 let true_,false_ =
  88   let rec t = { fid = 1; pos = True; fkey=1; neg = f ; st = empty_hex; size =1; }
  89   and f = { fid = 0; pos = False; fkey=0; neg = t; st = empty_hex; size = 1; }
  90   in
  91     WH.add f_pool f;
  92     WH.add f_pool t;
  93     t,f
  94
  95 let is_true f = f.fid == 1
  96 let is_false f = f.fid == 0
  97
  98
  99 let cons pos neg s1 s2 size1 size2 =
 100   let rec pnode =
 101     { fid = gen_id ();
 102       fkey = hash_node_form pos;
 103       pos = pos;
 104       neg = nnode;
 105       st = s1;
 106       size = size1;}
 107   and nnode = {
 108     fid = gen_id ();
 109     pos = neg;
 110     fkey = hash_node_form neg;
 111     neg = pnode;
 112     st = s2;
 113     size = size2;
 114   }
 115   in
 116     (WH.merge f_pool pnode),(WH.merge f_pool nnode)
 117
 118 let atom_  d p s =
 119   let si = Ptset.singleton s in
 120   let ss = match d with
 121     | `Left -> (si,Ptset.empty,si),empty_triple
 122     | `Right -> empty_triple,(si,Ptset.empty,si)
 123     | `LLeft -> (Ptset.empty,si,si),empty_triple
 124     | `RRight -> empty_triple,(Ptset.empty,si,si)
 125   in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
 126
 127 let union_hex  ((l1,ll1,lll1),(r1,rr1,rrr1))  ((l2,ll2,lll2),(r2,rr2,rrr2)) =
 128   (pt_cup l1 l2 ,pt_cup ll1 ll2,pt_cup lll1 lll2),
 129   (pt_cup r1 r2 ,pt_cup rr1 rr2,pt_cup rrr1 rrr2)
 130
 131 let merge_states f1 f2 =
 132   let sp =
 133     union_hex f1.st f2.st
 134   and sn =
 135     union_hex f1.neg.st f2.neg.st
 136   in
 137     sp,sn
 138
 139 let full_or_ f1 f2 =
 140   let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
 141   let sp,sn = merge_states f1 f2 in
 142   let psize = f1.size + f2.size in
 143   let nsize = f1.neg.size + f2.neg.size in
 144     fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize )
 145
 146 let or_ f1 f2 =
 147   let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
 148   if is_true f1 || is_true f2 then true_
 149   else if is_false f1 && is_false f2 then false_
 150   else if is_false f1 then f2
 151   else if is_false f2 then f1
 152   else
 153     let psize = f1.size + f2.size in
 154     let nsize = f1.neg.size + f2.neg.size in
 155     let sp,sn = merge_states f1 f2 in
 156       fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize)
 157
 158
 159
 160 let and_ f1 f2 =
 161   let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
 162   if is_true f1 && is_true f2 then true_
 163   else if is_false f1 || is_false f2 then false_
 164   else if is_true f1 then f2
 165   else if is_true f2 then f1
 166   else
 167     let psize = f1.size + f2.size in
 168     let nsize = f1.neg.size + f2.neg.size in
 169     let sp,sn = merge_states f1 f2 in
 170       fst (cons (And(f1,f2)) (Or(f1.neg,f2.neg)) sp sn psize nsize)
 171
 172
 173 let not_ f = f.neg
 174
 175 let k_hash (s,t) = HASHINT2(Ptset.hash s,Tag.hash t)
 176
 177 module HTagSetKey =
 178 struct
 179   type t = Ptset.t*Tag.t
 180   let equal (s1,s2) (t1,t2) =  (s2 == t2) &&  Ptset.equal s1 t1
 181   let hash = k_hash
 182 end
 183
 184 module HTagSet = Hashtbl.Make(HTagSetKey)
 185
 186 type skiplist = Nothing | All
 187                 | Zero of skiplist
 188                 | One of skiplist | Two of skiplist | Three of skiplist
 189                 | Four of skiplist | Five of skiplist | Six of skiplist
 190                 | Seven of skiplist | Eight of skiplist | Nine of skiplist
 191
 192
 193 type formlist = Nil | Cons of state*formula*int*bool*formlist
 194
 195 type 'a t = {
 196     id : int;
 197     mutable states : Ptset.t;
 198     init : Ptset.t;
 199     mutable final : Ptset.t;
 200     universal : Ptset.t;
 201     starstate : Ptset.t option;
 202     (* Transitions of the Alternating automaton *)
 203     phi : (state,(TagSet.t*(bool*formula*bool)) list) Hashtbl.t;
 204     sigma : (int,('a t -> Tree.t -> Tree.t -> Ptset.t*'a)) Hashtbl.t;
 205 }
 206
 207   module Pair (X : Set.OrderedType) (Y : Set.OrderedType) =
 208   struct
 209     type t = X.t*Y.t
 210     let compare (x1,y1) (x2,y2) =
 211       let r = X.compare x1 x2 in
 212         if r == 0 then Y.compare y1 y2
 213         else r
 214   end
 215
 216   module PL = Set.Make (Pair (Ptset) (Ptset))
 217
 218
 219   let pr_st ppf l = Format.fprintf ppf "{";
 220     begin
 221       match l with
 222         |       [] -> ()
 223         | [s] -> Format.fprintf ppf " %i" s
 224         | p::r -> Format.fprintf ppf " %i" p;
 225             List.iter (fun i -> Format.fprintf ppf "; %i" i) r
 226     end;
 227     Format.fprintf ppf " }"
 228   let rec pr_frm ppf f = match f.pos with
 229     | True -> Format.fprintf ppf "⊤"
 230     | False -> Format.fprintf ppf "⊥"
 231     | And(f1,f2) ->
 232         Format.fprintf ppf "(";
 233         (pr_frm ppf f1);
 234         Format.fprintf ppf ") ∧ (";
 235         (pr_frm ppf f2);
 236         Format.fprintf ppf ")"
 237     | Or(f1,f2) ->
 238         (pr_frm ppf f1);
 239         Format.fprintf ppf " ∨ ";
 240         (pr_frm ppf f2);
 241     | Atom(dir,b,s) -> Format.fprintf ppf "%s%s[%i]"
 242         (if b then "" else "¬")
 243         (match  dir with
 244            | `Left ->  "↓₁"
 245            | `Right -> "↓₂"
 246            | `LLeft ->  "⇓₁"
 247            | `RRight -> "⇓₂") s
 248
 249   let dump ppf a =
 250     Format.fprintf ppf "Automaton (%i) :\n" a.id;
 251     Format.fprintf ppf "States : "; pr_st ppf (Ptset.elements a.states);
 252     Format.fprintf ppf "\nInitial states : "; pr_st ppf (Ptset.elements a.init);
 253     Format.fprintf ppf "\nFinal states : "; pr_st ppf (Ptset.elements a.final);
 254     Format.fprintf ppf "\nUniversal states : "; pr_st ppf (Ptset.elements a.universal);
 255     Format.fprintf ppf "\nAlternating transitions :\n------------------------------\n";
 256     let l = Hashtbl.fold (fun k t acc ->
 257                             (List.map (fun (t,(m,f,p)) -> (t,k),(m,f,p)) t)@ acc) a.phi [] in
 258     let l = List.sort (fun ((tsx,x),_) ((tsy,y),_) -> if x-y == 0 then TagSet.compare tsx tsy else x-y) l in
 259     List.iter (fun ((ts,q),(b,f,_)) ->
 260
 261                     let s =
 262                       if TagSet.is_finite ts
 263                       then "{" ^ (TagSet.fold (fun t a -> a ^ " '" ^ (Tag.to_string t)^"'") ts "") ^" }"
 264                       else let cts = TagSet.neg ts in
 265                         if TagSet.is_empty cts then "*" else
 266                           (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) cts "*\\{"
 267                           )^ "}"
 268                     in
 269                       Format.fprintf ppf "(%s,%i) %s " s q (if b then "=>" else "->");
 270                       pr_frm ppf f;
 271                       Format.fprintf ppf "\n")l;
 272
 273     Format.fprintf ppf "NFA transitions :\n------------------------------\n";
 274 (*    HTagSet.iter (fun (qs,t) (disp,b,_,flist,_,_) ->
 275                     let (ls,lls,_),(rs,rrs,_) =
 276                       List.fold_left (fun ((a1,b1,c1),(a2,b2,c2)) (_,f) ->
 277                                         let (x1,y1,z1),(x2,y2,z2) = f.st in
 278                                           ((Ptset.union x1 a1),(Ptset.union y1 b1),(Ptset.union c1 z1)),
 279                                         ((Ptset.union x2 a2),(Ptset.union y2 b2),(Ptset.union c2 z2)))
 280                         ((Ptset.empty,Ptset.empty,Ptset.empty),
 281                          (Ptset.empty,Ptset.empty,Ptset.empty))
 282                         flist
 283                     in
 284                       pr_st ppf (Ptset.elements qs);
 285                       Format.fprintf ppf ",%s  %s " (Tag.to_string t) (if b then "=>" else "->");
 286                       List.iter (fun (q,f) ->
 287                                    Format.fprintf ppf "\n%i," q;
 288                                    pr_frm ppf f)           flist;
 289                       Format.fprintf ppf "\nleft=";
 290                       pr_st ppf (Ptset.elements ls);
 291                       Format.fprintf ppf " , ";
 292                       pr_st ppf (Ptset.elements lls);
 293                       Format.fprintf ppf ", right=";
 294                       pr_st ppf (Ptset.elements rs);
 295                       Format.fprintf ppf ", ";
 296                       pr_st ppf (Ptset.elements rrs);
 297                       Format.fprintf ppf ", first=%s, next=%s\n\n" disp.flabel disp.nlabel;
 298       ) a.sigma;    *)
 299     Format.fprintf ppf "=======================================\n%!"
 300
 301   module Transitions = struct
 302     type t = state*TagSet.t*bool*formula*bool
 303     let ( ?< ) x = x
 304     let ( >< ) state (l,b) = state,(l,b,false)
 305     let ( ><@ ) state (l,b) = state,(l,b,true)
 306     let ( >=> ) (state,(label,mark,pred)) form = (state,label,mark,form,pred)
 307     let ( +| ) f1 f2 = or_ f1 f2
 308     let ( *& ) f1 f2 = and_ f1 f2
 309     let ( ** ) d s = atom_ d true s
 310
 311
 312   end
 313   type transition = Transitions.t
 314
 315   let equal_trans (q1,t1,m1,f1,_) (q2,t2,m2,f2,_) =
 316     (q1 == q2) && (TagSet.equal t1 t2) && (m1 == m2) (*&& (equal_form f1 f2) *)
 317
 318
 319   module HFEval = Hashtbl.Make(
 320     struct
 321       type t = int*Ptset.t*Ptset.t
 322       let equal (a,b,c) (d,e,f) =
 323         a==d && (Ptset.equal b e) && (Ptset.equal c f)
 324       let hash (a,b,c) =
 325         HASHINT3(a,Ptset.hash b,Ptset.hash c)
 326     end)
 327
 328
 329
 330
 331   let hfeval = HFEval.create 4097
 332     let eval_form_bool f s1 s2 =
 333       let rec eval f = match f.pos with
 334           (* test some inlining *)
 335         | True -> true,true,true
 336         | False -> false,false,false
 337         | _ ->
 338             try
 339               HFEval.find hfeval (f.fid,s1,s2)
 340             with
 341               | Not_found -> let r =
 342                   match f.pos with
 343                     | Atom((`Left|`LLeft),b,q) ->
 344                         if b == (Ptset.mem q s1)
 345                         then (true,true,false)
 346                         else false,false,false
 347                     | Atom(_,b,q) ->
 348                         if b == (Ptset.mem q s2)
 349                         then (true,false,true)
 350                         else false,false,false
 351                     | Or(f1,f2) ->
 352                         let b1,rl1,rr1 = eval f1
 353                         in
 354                           if b1 && rl1 && rr1 then (true,true,true)
 355                           else
 356                             let b2,rl2,rr2 = eval f2
 357                             in
 358                             let rl1,rr1 = if b1 then rl1,rr1 else false,false
 359                             and rl2,rr2 = if b2 then rl2,rr2 else false,false
 360                             in (b1 || b2, rl1||rl2,rr1||rr2)
 361                     | And(f1,f2) ->
 362                         let b1,rl1,rr1 = eval f1 in
 363                           if b1 && rl1 && rr1 then (true,true,true)
 364                           else if b1
 365                           then let b2,rl2,rr2 = eval f2 in
 366                             if b2 then (true,rl1||rl2,rr1||rr2)
 367                             else (false,false,false)
 368                           else (false,false,false)
 369                     | _ -> assert false
 370                 in
 371                   HFEval.add hfeval (f.fid,s1,s2) r;
 372                   r
 373       in eval f
 374
 375
 376     let form_list_fold_left f acc fl =
 377       let rec loop acc fl =
 378         match fl with
 379           | Nil -> acc
 380           | Cons(s,frm,h,m,fll) -> loop (f acc s frm h m) fll
 381       in
 382         loop acc fl
 383
 384     let h_formlist = Hashtbl.create 4096
 385     let rec eval_formlist ?(memo=true) s1 s2 fl =
 386       match fl with
 387       | Nil -> Ptset.empty,false,false,false,false
 388       | Cons(q,f,h,mark,fll) ->
 389           let k = (h,Ptset.hash s1,Ptset.hash s2,mark)
 390           in
 391
 392             try
 393               if memo then Hashtbl.find h_formlist k
 394               else (raise Not_found)
 395             with
 396                 Not_found ->
 397             let s,b',b1',b2',amark = eval_formlist (~memo:memo) s1 s2 fll in
 398             let b,b1,b2 = eval_form_bool f s1 s2 in
 399             let r = if b then (Ptset.add q s, b, b1'||b1,b2'||b2,mark||amark)
 400             else s,b',b1',b2',amark
 401             in
 402 (*            Format.fprintf Format.err_formatter "\nEvaluating formula (%i) %i %s" h q (if mark then "=>" else "->");
 403               pr_frm (Format.err_formatter) f;
 404               Format.fprintf Format.err_formatter " in context ";
 405               pr_st Format.err_formatter (Ptset.elements s1);
 406               Format.fprintf Format.err_formatter ", ";
 407               pr_st Format.err_formatter (Ptset.elements s2);
 408               Format.fprintf Format.err_formatter " result is %b\n%!" b; *)
 409               (Hashtbl.add h_formlist k r;r)
 410
 411
 412
 413     let tags_of_state a q = Hashtbl.fold
 414       (fun p l acc ->
 415          if p == q then
 416            List.fold_left
 417              (fun acc (ts,(_,_,aux)) ->
 418                 if aux then acc else
 419                   TagSet.cup ts acc) acc l
 420          else acc) a.phi TagSet.empty
 421
 422
 423
 424     let tags a qs =
 425       let ts = Ptset.fold (fun q acc -> TagSet.cup acc (tags_of_state a q)) qs TagSet.empty
 426       in
 427         if TagSet.is_finite ts
 428         then `Positive(TagSet.positive ts)
 429         else `Negative(TagSet.negative ts)
 430
 431     let inter_text a b =
 432       match b with
 433         | `Positive s -> let r = Ptset.inter a s in (r,Ptset.mem Tag.pcdata r, true)
 434         | `Negative s -> let r = Ptset.diff a s in (r, Ptset.mem Tag.pcdata r, false)
 435
 436     let mk_nil_ctx x _ = Tree.mk_nil x
 437     let next_sibling_ctx x _ = Tree.next_sibling x
 438     let r_ignore _ x = x
 439
 440     let set_get_tag r t = r := (fun _ -> t)
 441       (*
 442
 443         let merge_trans t a tag q acc =
 444         List.fold_left (fun (accf,acchash,idx) (ts,(m,f,pred)) ->
 445         if TagSet.mem tag ts
 446         then
 447         let acchash = HASHINT3(acchash,f.fid,q) in
 448         (Cons(q,f,acchash,idx,m,accf),acchash,idx+1)
 449         else (accf,acchash,idx)
 450         ) acc (try Hashtbl.find a.phi q with Not_found -> [])
 451
 452
 453
 454     let cast_cont :'b -> ('a t -> Tree.t -> Tree.t -> Ptset.t*'a) =
 455       Obj.magic
 456
 457     let get_trans conti t a tag r =
 458       try
 459           Hashtbl.find a.sigma (HASHINT2(Ptset.hash r,Tag.hash tag))
 460       with
 461           Not_found ->
 462             let fl,_,accq,_ =
 463               Ptset.fold (fun q (accf,acchash,accq,aidx) ->
 464                             let naccf,acchash,naidx =
 465                               merge_trans t a tag q (accf,acchash,aidx )
 466                             in
 467                               (naccf,acchash,Ptset.add q accq,naidx)
 468                          )
 469                 r (Nil,17,Ptset.empty,0)
 470             in
 471             let (ls,lls,llls),(rs,rrs,rrrs) =
 472              form_list_fold_left (fun ((a1,b1,c1),(a2,b2,c2)) _ f _ _ _ ->
 473                                     let (x1,y1,z1),(x2,y2,z2) = f.st in
 474                                       ((Ptset.union x1 a1),(Ptset.union y1 b1),(Ptset.union c1 z1)),
 475                                     ((Ptset.union x2 a2),(Ptset.union y2 b2),(Ptset.union c2 z2)))
 476                ((Ptset.empty,Ptset.empty,Ptset.empty),
 477                 (Ptset.empty,Ptset.empty,Ptset.empty))
 478                 fl
 479             in
 480             let tb,ta =
 481               Tree.tags t tag
 482             in
 483             let tl,htlt,lfin = inter_text tb (tags a ls)
 484             and tll,htllt,llfin = inter_text tb (tags a lls)
 485             and tr,htrt,rfin = inter_text ta (tags a rs)
 486             and trr,htrrt,rrfin = inter_text ta  (tags a rrs)
 487             in
 488             let get_tag = ref Tree.tag in
 489             let first,flabel =
 490               if (llfin && lfin) then (* no stars *)
 491                 (if htlt || htllt then (Tree.text_below, "#text_below")
 492                  else
 493                    let etl = Ptset.is_empty tl
 494                    and etll = Ptset.is_empty tll
 495                    in
 496                      if (etl && etll)
 497                          then (Tree.mk_nil, "#mk_nil")
 498                          else
 499                            if etl then
 500                              if Ptset.is_singleton tll
 501                              then begin
 502                                set_get_tag get_tag (Ptset.choose tll);
 503                                (Tree.tagged_desc (Ptset.choose tll), "#tagged_desc")
 504                              end
 505                              else (Tree.select_desc_only tll, "#select_desc_only")
 506                            else if etll then (Tree.node_child,"#node_child")
 507                            else (Tree.select_below tl tll,"#select_below"))
 508                   else (* stars or node() *)
 509                     if htlt||htllt then (Tree.first_child,"#first_child")
 510                     else (Tree.node_child,"#node_child")
 511             and next,nlabel =
 512               if (rrfin && rfin) then (* no stars *)
 513                 ( if htrt || htrrt
 514                   then (Tree.text_next, "#text_next")
 515                     else
 516                       let etr = Ptset.is_empty tr
 517                       and etrr = Ptset.is_empty trr
 518                       in
 519                         if etr && etrr
 520                         then (mk_nil_ctx, "#mk_nil_ctx")
 521                         else
 522                           if etr then
 523                             if Ptset.is_singleton trr
 524                             then begin
 525                               set_get_tag get_tag (Ptset.choose trr);
 526                               (Tree.tagged_foll_below (Ptset.choose trr),"#tagged_foll_below")
 527                             end
 528                             else (Tree.select_foll_only trr,"#select_foll_only")
 529                           else if etrr then (Tree.node_sibling_ctx,"#node_sibling_ctx")
 530                           else
 531                             (Tree.select_next tr trr,"#select_next") )
 532
 533                   else if htrt || htrrt then (Tree.next_sibling_ctx,"#next_sibling_ctx")
 534                   else (Tree.node_sibling_ctx,"#node_sibling_ctx")
 535             in
 536             let cont = let flist = fl in
 537               fun a t res ctx ->
 538                 let s1,res1 = conti a (first t) llls res t
 539                 and s2,res2 = conti a (next t ctx) rrrs res ctx in
 540                 let r',rb,rb1,rb2,mark,idxl = eval_formlist s1 s2 flist
 541                 in
 542                   r',(vb rb)*((vb mark)  + (vb rb1)*res1 + (vb rb2)*res2)
 543             in
 544               Hashtbl.add a.sigma (HASHINT2(Ptset.hash r,Tag.hash tag)) (cast_cont cont);
 545               (cast_cont cont)
 546
 547
 548 (*
 549     let rec accepting_among a t r ctx =
 550       if Tree.is_nil t || Ptset.is_empty r then Ptset.empty,0,TS.Nil else
 551         let dispatch,mark,flist,llls,rrrs =
 552           get_trans (fun _ _ _ _ -> failwith "toto") t a (Tree.tag t) r
 553         in
 554         let s1,n1,res1 = accepting_among a (dispatch.first t) llls t in
 555         let s2,n2,res2 = accepting_among a (dispatch.next t ctx) rrrs ctx in
 556         let r',rb,rb1,rb2 = eval_formlist s1 s2 flist in
 557           r',(vb rb)*((vb mark) + (vb rb1)* n1 + (vb rb2)*n2),if rb then
 558             dispatch.consres t res1 res2 rb1 rb2
 559           else TS.Nil *)
 560
 561     let run a t = assert false (*
 562       let st,n,res = accepting_among a t a.init t in
 563         if Ptset.is_empty (st) then TS.empty,0 else res,n *)
 564
 565     let rec accepting_among_count_no_star  a t r ctx  =
 566       if Tree.is_nil t then Ptset.empty,0 else
 567         (get_trans (accepting_among_count_no_star) t a (Tree.tag t) r)
 568           a t ctx
 569
 570 (*
 571     let rec accepting_among_count_star a t n =
 572         if Tree.is_nil t then n else
 573           if (Tree.tag t == Tag.attribute)
 574           then accepting_among_count_star a (Tree.node_sibling t) n
 575           else accepting_among_count_star a (Tree.node_sibling t)
 576             (accepting_among_count_star a (Tree.node_child t) (1+n))
 577
 578     let rec accepting_among_count_may_star starstate a t r ctx =
 579       if r == starstate then starstate,(accepting_among_count_star a t 0)
 580       else
 581         if Tree.is_nil t||Ptset.is_empty r then Ptset.empty,0 else
 582           let dispatch,mark,flist,llls,rrrs =
 583             get_trans (fun _ _ _ _ -> failwith "toto") t a (Tree.tag t) r
 584           in
 585           let s1,res1 = accepting_among_count_may_star starstate a (dispatch.first t) llls t
 586           and s2,res2 = accepting_among_count_may_star starstate a (dispatch.next t ctx) rrrs ctx
 587           in
 588           let r',rb,rb1,rb2 = eval_formlist s1 s2 flist
 589           in
 590             r',(vb rb)*((vb mark) + (vb rb1)*res1 + (vb rb2)*res2)
 591
 592 *)
 593     let run_count a t =
 594
 595       let st,res = match a.starstate with
 596         | None -> accepting_among_count_no_star  a t a.init t
 597         | Some s -> assert false (*accepting_among_count_may_star s a t a.init t  *)
 598       in
 599         if Ptset.is_empty (st) then 0 else  res
 600
 601
 602     let run_time _ _ = failwith "blah"
 603
 604
 605     module RealBottomUp = struct
 606
 607       (* decrease number of arguments *)
 608       let ton t = if Tree.is_nil t then "##"
 609       else Tag.to_string (Tree.tag t)
 610       ;;
 611       let ion t = Tree.dump_node t
 612       let memo = Hashtbl.create 4097
 613       let rlist = ref []
 614
 615         let cpt = ref 0;;
 616       let rec run a t res r root rinit next targettag r0 first tomark =
 617         incr cpt;
 618         let res = (vb tomark) + res in
 619         let newr,newres = if first then
 620           accepting_among_count_no_star  a t r t
 621         else r, res
 622         in
 623         let r,res = if Ptset.is_empty newr then r,0 else newr,newres in
 624           if Tree.equal t root then
 625             if Ptset.intersect r rinit then (r,res,next)
 626             else (Ptset.empty,0,next)
 627           else
 628           let tag = Tree.tag t in
 629           let parent = Tree.binary_parent t in
 630           let parent_tag = Tree.tag parent in
 631           let left = Tree.is_left t in
 632           let r',mark =
 633               try Hashtbl.find memo (r,parent_tag,left) with
 634                 | Not_found ->
 635                     let pair =
 636                       Hashtbl.fold
 637                         (fun q l acc ->
 638                            List.fold_left
 639                              (fun (aq,am) (ts,(mark,form,_)) ->
 640                                 if TagSet.mem parent_tag ts then
 641                                   let (value,_,_) = if left then
 642                                     eval_form_bool form r Ptset.empty
 643                                   else
 644                                     eval_form_bool form Ptset.empty r
 645                                   in
 646 (*                                let _ = if value then begin
 647                                     Format.fprintf Format.err_formatter "Can take transition (%i,%s)%s%!"
 648                                       q (Tag.to_string parent_tag)
 649                                       (if mark then "=>" else "->");
 650                                     pr_frm Format.err_formatter form;
 651                                     Format.fprintf Format.err_formatter "%! %s(" (if left then "left" else "right");
 652                                     pr_st Format.err_formatter (Ptset.elements r);
 653                                     Format.fprintf Format.err_formatter ")\n%!" end;
 654                               in *)
 655                                     if value then (Ptset.add q aq, mark||am)
 656                                     else (aq,am)
 657                                 else (aq,am))
 658                              acc l
 659                         ) a.phi (Ptset.empty,false)
 660                     in Hashtbl.add memo (r,parent_tag,left) pair;pair
 661           in
 662             if Ptset.is_empty r' then Ptset.empty,0,next
 663             else
 664             if Tree.is_below_right t next then
 665               let rn,resn,nextofnext = run a next 0 r0 t r (Tree.tagged_next next targettag) targettag r0 true false
 666               in
 667               let rn,resn = if Ptset.is_empty rn then Ptset.empty,0 else rn,resn in
 668                 run a (parent) (resn+res) r' root rinit nextofnext targettag r0 false false
 669             else
 670               run a (parent) (res) r' root rinit next targettag r0 false (mark&&left)
 671
 672
 673
 674       let accept_count a t tag initset =
 675         let tree1 = Tree.tagged_lowest t tag in
 676         let tree2 = Tree.tagged_next tree1 tag in
 677           let c,b,_ =run a tree1 0 initset t a.init tree2 tag initset true false
 678           in Printf.eprintf "%i\n%!" !cpt;
 679             if Ptset.is_empty c then 0 else b
 680
 681     end *)
 682 (*
 683     module RealBottomUp2 = struct
 684       module Formlist =
 685       struct
 686         type t = formlist
 687         let nil : t = Nil
 688         let cons q f i m l = Cons(q,f,i,m,l)
 689         let hash = function Nil -> 0 | Cons(_,_,i,_,_) -> max_int land i
 690         let pr fmt l =
 691           let rec loop = function
 692             | Nil -> ()
 693             | Cons(q,f,_,m,l) ->
 694                 Format.fprintf fmt "%i %s" q (if m then "=>" else "->");
 695                 pr_frm fmt f;
 696                 Format.fprintf fmt "\n%!";
 697                 loop l
 698           in
 699             loop l
 700       end
 701
 702       type ptset_list = Nil | Cons of Ptset.t*int*ptset_list
 703       let hpl l = match l with
 704         | Nil -> 0
 705         | Cons (_,i,_) -> i
 706
 707       let cons s l = Cons (s,(Ptset.hash s) + 65599 * (hpl l), l)
 708
 709       let rec empty_size n =
 710         if n == 0 then Nil
 711         else cons Ptset.empty (empty_size (n-1))
 712
 713       let fold_pl f l acc =
 714         let rec loop l acc = match l with
 715             Nil -> acc
 716           | Cons(s,h,pl) -> loop pl (f s h acc)
 717         in
 718           loop l acc
 719       let map_pl f l =
 720         let rec loop =
 721           function Nil -> Nil
 722             | Cons(s,h,ll) -> cons (f s) (loop ll)
 723         in loop l
 724
 725       let rev_pl l =
 726         let rec loop acc l = match l with
 727           | Nil -> acc
 728           | Cons(s,_,ll) -> loop (cons s acc) ll
 729         in
 730           loop Nil l
 731
 732       let rev_map_pl f l  =
 733         let rec loop acc l =
 734           match l with
 735             | Nil -> acc
 736             | Cons(s,_,ll) -> loop (cons (f s) acc) ll
 737         in
 738           loop Nil l
 739
 740       let merge_int _ rb rb1 rb2 mark _ res1 res2 =
 741         if rb then (vb mark) + ((vb rb1)*res1) + ((vb rb2)*res2)
 742         else 0
 743
 744       let td_trans = Hashtbl.create 4096
 745
 746       let choose_jump tagset qtags1 qtagsn a f_nil f_text f_t1 f_s1 f_tn f_sn f_notext =
 747         let tags1,hastext1,fin1 = inter_text tagset (tags a qtags1) in
 748         let tagsn,hastextn,finn = inter_text tagset (tags a qtagsn) in
 749 (*        Format.fprintf Format.err_formatter "Tags below states ";
 750           pr_st Format.err_formatter (Ptset.elements qtags1);
 751           Format.fprintf Format.err_formatter " are { ";
 752           Ptset.iter (fun t -> Format.fprintf Format.err_formatter "%s " (Tag.to_string t)) tags1;
 753           Format.fprintf Format.err_formatter "}, %b,%b\n%!" hastext1 fin1;
 754
 755           Format.fprintf Format.err_formatter "Tags below states ";
 756           pr_st Format.err_formatter (Ptset.elements qtagsn);
 757           Format.fprintf Format.err_formatter " are { ";
 758           Ptset.iter (fun t -> Format.fprintf Format.err_formatter "%s " (Tag.to_string t)) tagsn;
 759           Format.fprintf Format.err_formatter "}, %b,%b\n%!" hastextn finn;
 760 *)
 761           if (hastext1||hastextn) then f_text  (* jumping to text nodes doesn't work really well *)
 762           else if (Ptset.is_empty tags1) && (Ptset.is_empty tagsn) then f_nil
 763           else if (Ptset.is_empty tagsn) then
 764             if (Ptset.is_singleton tags1) then f_t1 (Ptset.choose tags1)  (* TaggedChild/Sibling *)
 765             else f_s1 tags1 (* SelectChild/Sibling *)
 766           else if (Ptset.is_empty tags1) then
 767             if (Ptset.is_singleton tagsn) then f_tn (Ptset.choose tagsn) (* TaggedDesc/Following *)
 768             else f_sn tagsn (* SelectDesc/Following *)
 769           else f_notext
 770
 771       let choose_jump_down a b c d =
 772         choose_jump a b c d
 773           (Tree.mk_nil)
 774           (Tree.text_below )
 775           (fun _ -> Tree.node_child ) (* !! no tagged_child in Tree.ml *)
 776           (fun _ -> Tree.node_child ) (* !! no select_child in Tree.ml *)
 777           (Tree.tagged_desc)
 778           (fun _ -> Tree.node_child ) (* !! no select_desc *)
 779           (Tree.node_child)
 780
 781       let choose_jump_next a b c d =
 782         choose_jump a b c d
 783           (fun t _ -> Tree.mk_nil t)
 784           (Tree.text_next)
 785           (fun _ -> Tree.node_sibling_ctx) (* !! no tagged_sibling in Tree.ml *)
 786           (fun _ -> Tree.node_sibling_ctx) (* !! no select_child in Tree.ml *)
 787           (Tree.tagged_foll_below)
 788           (fun _ -> Tree.node_sibling_ctx) (* !! no select_foll *)
 789           (Tree.node_sibling_ctx)
 790
 791       module type RS = sig
 792         type t
 793         type elt
 794         val empty : t
 795         val cons : elt -> t -> t
 796         val concat : t -> t -> t
 797       end
 798
 799
 800       let get_trans slist tag a t =
 801         try
 802           Hashtbl.find td_trans (tag,hpl slist)
 803         with
 804           | Not_found ->
 805               let fl_list,llist,rlist,ca,da,sa,fa =
 806                 fold_pl
 807                   (fun set _ (fll_acc,lllacc,rllacc,ca,da,sa,fa) -> (* For each set *)
 808                      let fl,ll,rr,ca,da,sa,fa =
 809                        Ptset.fold
 810                          (fun q acc ->
 811                             fst (
 812                               List.fold_left
 813                                 (fun (((fl_acc,ll_acc,rl_acc,c_acc,d_acc,s_acc,f_acc),h_acc) as acc)
 814                                    (ts,(m,f,_))  ->
 815                                      if (TagSet.mem tag ts)
 816                                      then
 817                                        let (child,desc,below),(sibl,foll,after) = f.st in
 818                                          ((Formlist.cons q f h_acc m fl_acc,
 819                                            Ptset.union ll_acc below,
 820                                            Ptset.union rl_acc after,
 821                                            Ptset.union child c_acc,
 822                                            Ptset.union desc d_acc,
 823                                            Ptset.union sibl s_acc,
 824                                            Ptset.union foll f_acc),
 825                                           HASHINT3(h_acc,f.fid,HASHINT2(q,vb m)))
 826                                    else acc ) (acc,0) (
 827                                   try Hashtbl.find a.phi q
 828                                   with
 829                                       Not_found -> Printf.eprintf "Looking for state %i, doesn't exist!!!\n%!"
 830                                         q;[]
 831                                 ))
 832
 833                          ) set (Formlist.nil,Ptset.empty,Ptset.empty,ca,da,sa,fa)
 834                      in fl::fll_acc, cons ll lllacc, cons rr rllacc,ca,da,sa,fa)
 835                   slist ([],Nil,Nil,Ptset.empty,Ptset.empty,Ptset.empty,Ptset.empty)
 836               in
 837                 (* Logic to chose the first and next function *)
 838               let tags_below,tags_after = Tree.tags t tag in
 839               let first = choose_jump_down tags_below ca da a
 840               and next = choose_jump_next tags_after sa fa a in
 841               let v = (fl_list,llist,rlist,first,next) in
 842                 Hashtbl.add td_trans (tag, hpl slist) v; v
 843
 844
 845       let top_down ?(noright=false) a merge null t slist ctx slot_size =
 846         let pempty = empty_size slot_size in
 847
 848         let eval_fold2_slist fll sl1 sl2 res1 res2 t =
 849           let res = Array.copy res1 in
 850           let rec fold l1 l2 fll i aq = match l1,l2,fll with
 851             | Cons(s1,_,ll1), Cons(s2, _ ,ll2),fl::fll ->
 852                 let r',rb,rb1,rb2,mark = eval_formlist s1 s2 fl in
 853                 let _ = res.(i) <- merge null rb rb1 rb2 mark t res1.(i) res2.(i)
 854                 in
 855 (*              let _ = Format.fprintf Format.err_formatter "(%b,%b,%b,%b) Result was %i %i, now %i\n%!"
 856                   rb rb1 rb2 mark (Obj.magic res1.(i))  (Obj.magic res2.(i)) (Obj.magic res.(i));
 857                 in *)
 858
 859                   fold ll1 ll2 fll (i+1) (cons r' aq)
 860             | Nil, Nil,[] -> aq,res
 861             | _ -> assert false
 862           in
 863             fold sl1 sl2 fll 0 Nil
 864         in
 865         let rec loop  t slist ctx =
 866           if Tree.is_nil t then (pempty,Array.make slot_size null)
 867           else
 868             let tag = Tree.tag t in
 869             let fl_list,llist,rlist,first,next = get_trans slist tag a t in
 870             let sl1,res1 = loop (first t) llist t in
 871             let sl2,res2 = if noright then (pempty,Array.make slot_size null)
 872             else loop (next t ctx) rlist ctx in
 873             eval_fold2_slist fl_list sl1 sl2 res1 res2 t
 874         in
 875           loop t slist ctx
 876
 877         let run_top_down_count a t =
 878           let init = cons a.init Nil in
 879           let _,res = top_down a (fun _ rb rb1 rb2 mark t res1 res2 ->
 880                                     (vb rb)*( (vb mark) + (vb rb1)*res1 + (vb rb2)*res2))
 881             0 t init t 1
 882           in res.(0)
 883         ;;
 884
 885         let run_top_down a t =
 886           let init = cons a.init Nil in
 887           let _,res =
 888             top_down a (fun null rb rb1 rb2 mark t res1 res2 ->
 889                          if rb then
 890                            TS.concat
 891                              (TS.concat (if mark then TS.Sing(t) else null)
 892                                 (if rb1 then res1 else null))
 893                                (if rb2 then res2 else null)
 894                          else null)
 895               TS.Nil t init t 1
 896           in res.(0)
 897         ;;
 898
 899
 900     end
 901 *)
 902     module type ResultSet =
 903     sig
 904       type t
 905       val empty : t
 906       val cons : Tree.t -> t -> t
 907       val concat : t -> t -> t
 908       val iter : (Tree.t -> unit) -> t -> unit
 909       val fold : (Tree.t -> 'a -> 'a) -> t -> 'a -> 'a
 910       val map : (Tree.t -> Tree.t) -> t -> t
 911       val length : t -> int
 912     end
 913
 914     module Integer : ResultSet =
 915     struct
 916       type t = int
 917       let empty = 0
 918       let cons _ x = x+1
 919       let concat x y = x + y
 920       let iter _ _ = failwith "iter not implemented"
 921       let fold _ _ _ = failwith "fold not implemented"
 922       let map _ _ = failwith "map not implemented"
 923       let length x = x
 924     end
 925
 926     module IdSet : ResultSet =
 927     struct
 928       type node = Nil
 929                   | Cons of Tree.t * node
 930                   | Concat of node*node
 931
 932       and t = { node : node;
 933                 length :  int }
 934
 935       let empty = { node = Nil; length = 0 }
 936
 937       let cons e t = { node = Cons(e,t.node); length = t.length+1 }
 938       let concat t1 t2 = { node = Concat(t1.node,t2.node); length = t1.length+t2.length }
 939       let append e t = { node = Concat(t.node,Cons(e,Nil)); length = t.length+1 }
 940
 941
 942       let fold f l acc =
 943         let rec loop acc t = match t with
 944           | Nil -> acc
 945           | Cons (e,t) -> loop (f e acc) t
 946           | Concat (t1,t2) -> loop (loop acc t1) t2
 947         in
 948           loop acc l.node
 949
 950       let length l = l.length
 951
 952
 953       let iter f l =
 954         let rec loop = function
 955           | Nil -> ()
 956           | Cons (e,t) -> f e; loop t
 957           | Concat(t1,t2) -> loop t1;loop t2
 958         in loop l.node
 959
 960       let map f l =
 961         let rec loop = function
 962           | Nil -> Nil
 963           | Cons(e,t) -> Cons(f e, loop t)
 964           | Concat(t1,t2) -> Concat(loop t1,loop t2)
 965         in
 966           { l with node = loop l.node }
 967
 968
 969     end
 970
 971     module Run (RS : ResultSet) =
 972     struct
 973       module Formlist =
 974       struct
 975         type t = formlist
 976         let nil : t = Nil
 977         let cons q f i m l = Cons(q,f,i,m,l)
 978         let hash = function Nil -> 0 | Cons(_,_,i,_,_) -> max_int land i
 979         let pr fmt l =
 980           let rec loop = function
 981             | Nil -> ()
 982             | Cons(q,f,_,m,l) ->
 983                 Format.fprintf fmt "%i %s" q (if m then "=>" else "->");
 984                 pr_frm fmt f;
 985                 Format.fprintf fmt "\n%!";
 986                 loop l
 987           in
 988             loop l
 989       end
 990
 991       type ptset_list = Nil | Cons of Ptset.t*int*ptset_list
 992       let hpl l = match l with
 993         | Nil -> 0
 994         | Cons (_,i,_) -> i
 995
 996       let cons s l = Cons (s,(Ptset.hash s) + 65599 * (hpl l), l)
 997
 998       let rec empty_size n =
 999         if n == 0 then Nil
1000         else cons Ptset.empty (empty_size (n-1))
1001
1002       let fold_pl f l acc =
1003         let rec loop l acc = match l with
1004             Nil -> acc
1005           | Cons(s,h,pl) -> loop pl (f s h acc)
1006         in
1007           loop l acc
1008       let map_pl f l =
1009         let rec loop =
1010           function Nil -> Nil
1011             | Cons(s,h,ll) -> cons (f s) (loop ll)
1012         in loop l
1013
1014       let rev_pl l =
1015         let rec loop acc l = match l with
1016           | Nil -> acc
1017           | Cons(s,_,ll) -> loop (cons s acc) ll
1018         in
1019           loop Nil l
1020
1021       let rev_map_pl f l  =
1022         let rec loop acc l =
1023           match l with
1024             | Nil -> acc
1025             | Cons(s,_,ll) -> loop (cons (f s) acc) ll
1026         in
1027           loop Nil l
1028
1029       let td_trans = Hashtbl.create 4096
1030
1031
1032       let choose_jump tagset qtags1 qtagsn a f_nil f_text f_t1 f_s1 f_tn f_sn f_notext =
1033         let tags1,hastext1,fin1 = inter_text tagset (tags a qtags1) in
1034         let tagsn,hastextn,finn = inter_text tagset (tags a qtagsn) in
1035 (*        Format.fprintf Format.err_formatter "Tags below states ";
1036           pr_st Format.err_formatter (Ptset.elements qtags1);
1037           Format.fprintf Format.err_formatter " are { ";
1038           Ptset.iter (fun t -> Format.fprintf Format.err_formatter "%s " (Tag.to_string t)) tags1;
1039           Format.fprintf Format.err_formatter "}, %b,%b\n%!" hastext1 fin1;
1040
1041           Format.fprintf Format.err_formatter "Tags below states ";
1042           pr_st Format.err_formatter (Ptset.elements qtagsn);
1043           Format.fprintf Format.err_formatter " are { ";
1044           Ptset.iter (fun t -> Format.fprintf Format.err_formatter "%s " (Tag.to_string t)) tagsn;
1045           Format.fprintf Format.err_formatter "}, %b,%b\n%!" hastextn finn;
1046 *)
1047           if (hastext1||hastextn) then f_text  (* jumping to text nodes doesn't work really well *)
1048           else if (Ptset.is_empty tags1) && (Ptset.is_empty tagsn) then f_nil
1049           else if (Ptset.is_empty tagsn) then
1050             if (Ptset.is_singleton tags1) then f_t1 (Ptset.choose tags1)  (* TaggedChild/Sibling *)
1051             else f_s1 tags1 (* SelectChild/Sibling *)
1052           else if (Ptset.is_empty tags1) then
1053             if (Ptset.is_singleton tagsn) then f_tn (Ptset.choose tagsn) (* TaggedDesc/Following *)
1054             else f_sn tagsn (* SelectDesc/Following *)
1055           else f_notext
1056
1057       let choose_jump_down a b c d =
1058         choose_jump a b c d
1059           (Tree.mk_nil)
1060           (Tree.text_below)
1061           (*fun x -> let i,j = Tree.doc_ids x in
1062            let res = Tree.text_below x in
1063              Printf.printf "Calling text_below %s (tag=%s), docids= (%i,%i), res=%s\n"
1064                (Tree.dump_node x) (Tag.to_string (Tree.tag x)) i j (Tree.dump_node res);
1065              res*)
1066           (fun _ -> Tree.node_child ) (* !! no tagged_child in Tree.ml *)
1067           (fun _ -> Tree.node_child ) (* !! no select_child in Tree.ml *)
1068           (Tree.tagged_desc)
1069           (fun _ -> Tree.node_child ) (* !! no select_desc *)
1070           (Tree.node_child)
1071
1072       let choose_jump_next a b c d =
1073         choose_jump a b c d
1074           (fun t _ -> Tree.mk_nil t)
1075           (Tree.text_next)
1076           (*fun x y -> let i,j = Tree.doc_ids x in
1077            let res = Tree.text_next x y in
1078              Printf.printf "Calling text_next %s (tag=%s) ctx=%s, docids= (%i,%i), res=%s\n"
1079                (Tree.dump_node x) (Tag.to_string (Tree.tag x)) (Tree.dump_node y) i j (Tree.dump_node res);
1080              res*)
1081
1082           (fun _ -> Tree.node_sibling_ctx) (* !! no tagged_sibling in Tree.ml *)
1083           (fun _ -> Tree.node_sibling_ctx) (* !! no select_child in Tree.ml *)
1084           (Tree.tagged_foll_below)
1085           (fun _ -> Tree.node_sibling_ctx) (* !! no select_foll *)
1086           (Tree.node_sibling_ctx)
1087
1088
1089       let get_trans slist tag a t =
1090         try
1091           Hashtbl.find td_trans (tag,hpl slist)
1092         with
1093           | Not_found ->
1094               let fl_list,llist,rlist,ca,da,sa,fa =
1095                 fold_pl
1096                   (fun set _ (fll_acc,lllacc,rllacc,ca,da,sa,fa) -> (* For each set *)
1097                      let fl,ll,rr,ca,da,sa,fa =
1098                        Ptset.fold
1099                          (fun q acc ->
1100                             fst (
1101                               List.fold_left
1102                                 (fun (((fl_acc,ll_acc,rl_acc,c_acc,d_acc,s_acc,f_acc),h_acc) as acc)
1103                                    (ts,(m,f,_))  ->
1104                                      if (TagSet.mem tag ts)
1105                                      then
1106                                        let (child,desc,below),(sibl,foll,after) = f.st in
1107                                          ((Formlist.cons q f h_acc m fl_acc,
1108                                            Ptset.union ll_acc below,
1109                                            Ptset.union rl_acc after,
1110                                            Ptset.union child c_acc,
1111                                            Ptset.union desc d_acc,
1112                                            Ptset.union sibl s_acc,
1113                                            Ptset.union foll f_acc),
1114                                           HASHINT3(h_acc,f.fid,HASHINT2(q,vb m)))
1115                                    else acc ) (acc,0) (
1116                                   try Hashtbl.find a.phi q
1117                                   with
1118                                       Not_found -> Printf.eprintf "Looking for state %i, doesn't exist!!!\n%!"
1119                                         q;[]
1120                                 ))
1121
1122                          ) set (Formlist.nil,Ptset.empty,Ptset.empty,ca,da,sa,fa)
1123                      in fl::fll_acc, cons ll lllacc, cons rr rllacc,ca,da,sa,fa)
1124                   slist ([],Nil,Nil,Ptset.empty,Ptset.empty,Ptset.empty,Ptset.empty)
1125               in
1126                 (* Logic to chose the first and next function *)
1127               let tags_below,tags_after = Tree.tags t tag in
1128               let first = choose_jump_down tags_below ca da a
1129               and next = choose_jump_next tags_after sa fa a in
1130               let v = (fl_list,llist,rlist,first,next) in
1131                 Hashtbl.add td_trans (tag, hpl slist) v; v
1132
1133       let merge rb rb1 rb2 mark t res1 res2 =
1134         if rb
1135         then
1136           let res1 = if rb1 then res1 else RS.empty
1137           and res2 = if rb2 then res2 else RS.empty
1138           in
1139             if mark then RS.cons t (RS.concat res1 res2)
1140             else RS.concat res1 res2
1141         else RS.empty
1142
1143       let top_down ?(noright=false) a t slist ctx slot_size =
1144         let pempty = empty_size slot_size in
1145         let eval_fold2_slist fll sl1 sl2 res1 res2 t =
1146           let res = Array.copy res1 in
1147           let rec fold l1 l2 fll i aq = match l1,l2,fll with
1148             | Cons(s1,_,ll1), Cons(s2, _ ,ll2),fl::fll ->
1149                 let r',rb,rb1,rb2,mark = eval_formlist s1 s2 fl in
1150                 let _ = res.(i) <- merge rb rb1 rb2 mark t res1.(i) res2.(i)
1151                 in
1152                   fold ll1 ll2 fll (i+1) (cons r' aq)
1153             | Nil, Nil,[] -> aq,res
1154             | _ -> assert false
1155           in
1156             fold sl1 sl2 fll 0 Nil
1157         in
1158         let null_result() = (pempty,Array.make slot_size RS.empty) in
1159         let rec loop t slist ctx =
1160           if Tree.is_nil t then null_result()
1161           else
1162             let tag = Tree.tag t in
1163             let fl_list,llist,rlist,first,next = get_trans slist tag a t in
1164             let sl1,res1 = loop (first t) llist t in
1165             let sl2,res2 = if noright then null_result()
1166             else loop (next t ctx) rlist ctx in
1167               eval_fold2_slist fl_list sl1 sl2 res1 res2 t
1168         in
1169         let loop_no_right t slist ctx =
1170           if Tree.is_nil t then null_result()
1171           else
1172             let tag = Tree.tag t in
1173             let fl_list,llist,rlist,first,next = get_trans slist tag a t in
1174             let sl1,res1 = loop (first t) llist t in
1175             let sl2,res2 = null_result() in
1176               eval_fold2_slist fl_list sl1 sl2 res1 res2 t
1177         in
1178           (if noright then loop_no_right else loop) t slist ctx
1179
1180         let run_top_down a t =
1181           let init = cons a.init Nil in
1182           let _,res = top_down a t init t 1
1183           in res.(0)
1184         ;;
1185
1186         module Configuration =
1187         struct
1188           module Ptss = Set.Make(Ptset)
1189           module IMap = Map.Make(Ptset)
1190           type t = { hash : int;
1191                         sets : Ptss.t;
1192                         results : RS.t IMap.t }
1193           let empty = { hash = 0;
1194                         sets = Ptss.empty;
1195                         results = IMap.empty;
1196                       }
1197           let is_empty c = Ptss.is_empty c.sets
1198           let add c s r =
1199             if Ptss.mem s c.sets then
1200               { c with results = IMap.add s (RS.concat r (IMap.find s c.results)) c.results}
1201             else
1202               { hash = HASHINT2(c.hash,Ptset.hash s);
1203                 sets = Ptss.add s c.sets;
1204                 results = IMap.add s r c.results
1205               }
1206
1207           let pr fmt c = Format.fprintf fmt "{";
1208             Ptss.iter (fun s -> pr_st fmt (Ptset.elements s);
1209                         Format.fprintf fmt "  ") c.sets;
1210             Format.fprintf fmt "}\n%!";
1211             IMap.iter (fun k d ->
1212                          pr_st fmt (Ptset.elements k);
1213                          Format.fprintf fmt "-> %i\n" (RS.length d)) c.results;
1214             Format.fprintf fmt "\n%!"
1215
1216           let merge c1 c2  =
1217             let acc1 = IMap.fold (fun s r acc ->
1218                                     IMap.add s
1219                                       (try
1220                                          RS.concat r (IMap.find s acc)
1221                                        with
1222                                          | Not_found -> r) acc) c1.results IMap.empty
1223             in
1224             let imap =
1225               IMap.fold (fun s r acc ->
1226                            IMap.add s
1227                              (try
1228                                 RS.concat r (IMap.find s acc)
1229                               with
1230                                 | Not_found -> r) acc)  c2.results acc1
1231             in
1232             let h,s =
1233               Ptss.fold
1234                 (fun s (ah,ass) -> (HASHINT2(ah,Ptset.hash s),
1235                                     Ptss.add s ass))
1236                 (Ptss.union c1.sets c2.sets) (0,Ptss.empty)
1237             in
1238               { hash = h;
1239                 sets =s;
1240                 results = imap }
1241
1242         end
1243         let fmt = Format.err_formatter
1244         let pr x = Format.fprintf fmt x
1245         let h_fold = Hashtbl.create 511
1246
1247         let fold_f_conf  t slist fl_list conf dir=
1248           let rec loop sl fl acc =
1249             match sl,fl with
1250               |Nil,[] -> acc
1251               | Cons(s,hs,sll), formlist::fll ->
1252                   let r',rb,rb1,rb2,mark =
1253                     try
1254                       Hashtbl.find h_fold (hs,Formlist.hash formlist,dir)
1255                     with
1256                         Not_found -> let res =
1257                           if dir then eval_formlist ~memo:false s Ptset.empty formlist
1258                           else eval_formlist ~memo:false Ptset.empty s formlist
1259                         in (Hashtbl.add h_fold (hs,Formlist.hash formlist,dir) res;res)
1260                   in(*
1261                   let _ = pr "Evaluating on set (%s) with tree %s=%s"
1262                     (if dir then "left" else "right")
1263                     (Tag.to_string (Tree.tag t))
1264                     (Tree.dump_node t) ;
1265                     pr_st fmt (Ptset.elements s);
1266                     pr ", formualae (with hash %i): \n" (Formlist.hash formlist);
1267                     Formlist.pr fmt formlist;
1268                     pr "result is ";
1269                     pr_st fmt (Ptset.elements r');
1270                     pr " %b %b %b %b \n%!" rb rb1 rb2 mark ;
1271                   in *)
1272                     if rb && ((dir&&rb1)|| ((not dir) && rb2))
1273                     then
1274                       let acc =
1275                         let old_r =
1276                           try Configuration.IMap.find s conf.Configuration.results
1277                           with Not_found -> RS.empty
1278                         in
1279                           Configuration.add acc r' (if mark then RS.cons t old_r else old_r)
1280                       in
1281                         loop sll fll acc
1282                     else loop sll fll acc
1283               | _ -> assert false
1284           in
1285             loop slist fl_list Configuration.empty
1286
1287         let h_trans = Hashtbl.create 4096
1288
1289         let get_up_trans slist ptag a tree =
1290           let key = (HASHINT2(hpl slist,Tag.hash ptag)) in
1291             try
1292           Hashtbl.find h_trans key
1293           with
1294           | Not_found ->
1295           let f_list,_ =
1296             Hashtbl.fold (fun q l acc ->
1297                             List.fold_left (fun  (fl_acc,h_acc) (ts,(m,f,_))  ->
1298                                               if TagSet.mem ptag ts
1299                                               then (Formlist.cons q f h_acc m fl_acc,
1300                                                     HASHINT3(h_acc,f.fid,q))
1301                                               else (fl_acc,h_acc))
1302                               acc l)
1303               a.phi (Formlist.nil,0)
1304           in
1305           let res = fold_pl (fun _ _ acc -> f_list::acc) slist []
1306           in
1307             (Hashtbl.add h_trans key res;res)
1308
1309
1310         let rec bottom_up a tree conf next jump_fun root dotd init accu =
1311           if (not dotd) && (Configuration.is_empty conf ) then
1312          (*   let _ = pr "Returning early from %s, with accu %i, next is %s\n%!"
1313               (Tree.dump_node tree) (Obj.magic accu) (Tree.dump_node next)
1314               in *)
1315             accu,conf,next
1316           else
1317 (*        let _ =
1318             pr "Going bottom up for tree with tag %s configuration is"
1319               (if Tree.is_nil tree then "###" else Tag.to_string (Tree.tag tree));
1320             Configuration.pr fmt conf
1321           in *)
1322           let below_right = Tree.is_below_right tree next in
1323 (*        let _ = Format.fprintf Format.err_formatter "below_right %s %s = %b\n%!"
1324             (Tree.dump_node tree) (Tree.dump_node next)  below_right
1325           in *)
1326           let accu,rightconf,next_of_next =
1327             if below_right then (* jump to the next *)
1328 (*            let _ = pr "Jumping to %s\n%!" (Tree.dump_node next) in  *)
1329               bottom_up a next conf (jump_fun next) jump_fun (Tree.next_sibling tree) true init accu
1330             else accu,Configuration.empty,next
1331           in
1332 (*        let _ = if below_right then pr "Returning from jump to next\n" in  *)
1333           let sub =
1334             if dotd then
1335               if below_right then (* only recurse on the left subtree *)
1336         (*      let _ = pr "Topdown on subtree\n%!" in     *)
1337                 prepare_topdown a tree true
1338               else
1339 (*              let _ = pr "Topdown on whole tree\n%!" in   *)
1340                 prepare_topdown a tree false
1341             else conf
1342           in
1343           let conf,next =
1344             (Configuration.merge rightconf sub, next_of_next)
1345           in
1346             if Tree.equal tree root then
1347 (*            let _ = pr "Stopping at root, configuration after topdown is:" ;
1348                 Configuration.pr fmt conf;
1349                 pr "\n%!"
1350               in  *) accu,conf,next
1351             else
1352           let parent = Tree.binary_parent tree in
1353           let ptag = Tree.tag parent in
1354           let dir = Tree.is_left tree in
1355           let slist = Configuration.Ptss.fold (fun e a -> cons e a) conf.Configuration.sets Nil in
1356           let fl_list = get_up_trans slist ptag a parent in
1357           let slist = rev_pl (slist) in
1358 (*        let _ = pr "Current conf is : %i " (Tree.id tree);
1359             Configuration.pr fmt conf;
1360             pr "\n"
1361           in *)
1362           let newconf = fold_f_conf parent slist fl_list conf dir in
1363 (*        let _ = pr "New conf before pruning is (dir=%b):" dir;
1364             Configuration.pr fmt newconf ;
1365             pr "accu is %i\n" (RS.length accu);
1366           in        *)
1367           let accu,newconf = Configuration.IMap.fold (fun s res (ar,nc) ->
1368                                                         if Ptset.intersect s init then
1369                                                           ( RS.concat res ar ,nc)
1370                                                         else (ar,Configuration.add nc s res))
1371             (newconf.Configuration.results) (accu,Configuration.empty)
1372           in
1373 (*        let _ = pr "New conf after pruning is (dir=%b):" dir;
1374             Configuration.pr fmt newconf ;
1375             pr "accu is %i\n" (RS.length accu);
1376           in        *)
1377             bottom_up a parent newconf next jump_fun root false init accu
1378
1379         and prepare_topdown a t noright =
1380 (*        pr "Going top down on tree with tag %s\n%!"
1381             (if Tree.is_nil t then "###" else (Tag.to_string(Tree.tag t))); *)
1382           let r = cons a.states Nil in
1383           let set,res = top_down (~noright:noright) a t r t 1 in
1384           let set = match set with
1385             | Cons(x,_,Nil) ->x
1386             | _ -> assert false
1387           in
1388 (*          pr "Result of topdown run is %!";
1389             pr_st fmt (Ptset.elements set);
1390             pr ", number is %i\n%!" (RS.length res.(0));  *)
1391             Configuration.add Configuration.empty set res.(0)
1392
1393
1394
1395         let run_bottom_up_contains a t =
1396           let trlist = Hashtbl.find a.phi (Ptset.choose a.init)
1397           in
1398           let init = List.fold_left
1399             (fun acc (_,(_,f,_)) ->
1400                Ptset.union acc (let (_,_,l) = fst (f.st) in l))
1401             Ptset.empty trlist
1402           in
1403           let tree1 = Tree.text_below t in
1404           let jump_fun = fun tree -> Tree.text_next tree t  in
1405           let tree2 = jump_fun tree1 in
1406           let rec loop tree next acc =
1407 (*          let _ = pr "\n_________________________\nNew iteration\n" in *)
1408 (*          let _ = pr "Jumping to %s\n%!" (Tree.dump_node tree) in  *)
1409             let acc,conf,next_of_next = bottom_up a tree
1410               Configuration.empty next jump_fun (Tree.root tree) true init acc
1411             in
1412               (*            let _ = pr "End of first iteration, conf is:\n%!";
1413                             Configuration.pr fmt conf
1414                             in *)
1415             let acc = Configuration.IMap.fold
1416               ( fun s res acc -> if Ptset.intersect init s
1417                 then RS.concat res acc else acc) conf.Configuration.results acc
1418             in
1419               if Tree.is_nil next_of_next  (*|| Tree.equal next next_of_next *)then
1420                 acc
1421               else loop next_of_next (jump_fun next_of_next) acc
1422           in
1423           loop tree1 tree2 RS.empty
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437     end
1438
1439     let top_down_count a t = let module RI = Run(Integer) in Integer.length (RI.run_top_down a t)
1440     let top_down a t = let module RI = Run(IdSet) in (RI.run_top_down a t)
1441     let bottom_up_count_contains a t = let module RI = Run(Integer) in Integer.length (RI.run_bottom_up_contains a t)
1442     let bottom_up_count a t = failwith "not implemented"
1443