X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=ata.ml;h=bb38863bad0285e25b696f1dfe85528557bf2854;hb=497ac3f74338faede9a844f5940857f55c0e9b64;hp=bba32034008d9318e3a110cbb1834f17e5cd3464;hpb=f98a8d98d86941a885f492d5cc134e34989c198a;p=SXSI%2Fxpathcomp.git

diff --git a/ata.ml b/ata.ml
index bba3203..bb38863 100644
--- a/ata.ml
+++ b/ata.ml
@@ -1,6 +1,7 @@
 INCLUDE "debug.ml"
 INCLUDE "utils.ml"
 
+type jump_kind = [ `TAG of Tag.t | `CONTAINS of string | `NOTHING ]
 let cpt_trans = ref 0
 let miss_trans = ref 0
 let cpt_eval = ref 0
@@ -398,8 +399,8 @@ type 'a t = {
 	    let b,b1,b2 = eval_form_bool f s1 s2 in
 	    let r = if b then (Ptset.add q s, b, b1'||b1,b2'||b2,mark||amark)
 	    else s,b',b1',b2',amark
-	    in
-(*	      Format.fprintf Format.err_formatter "\nEvaluating formula (%i) %i %s" h q (if mark then "=>" else "->");
+	    in(*
+	      Format.fprintf Format.err_formatter "\nEvaluating formula (%i) %i %s" h q (if mark then "=>" else "->");
 	      pr_frm (Format.err_formatter) f;
 	      Format.fprintf Format.err_formatter " in context ";
 	      pr_st Format.err_formatter (Ptset.elements s1);
@@ -438,467 +439,7 @@ type 'a t = {
     let r_ignore _ x = x
       
     let set_get_tag r t = r := (fun _ -> t)
-      (*
-
-	let merge_trans t a tag q acc = 
-	List.fold_left (fun (accf,acchash,idx) (ts,(m,f,pred)) ->
-	if TagSet.mem tag ts 
-	then
-	let acchash = HASHINT3(acchash,f.fid,q) in
-	(Cons(q,f,acchash,idx,m,accf),acchash,idx+1)
-	else (accf,acchash,idx)
-	) acc (try Hashtbl.find a.phi q with Not_found -> [])
-
-	
-
-    let cast_cont :'b -> ('a t -> Tree.t -> Tree.t -> Ptset.t*'a) = 
-      Obj.magic 
-
-    let get_trans conti t a tag r = 
-      try	
-	  Hashtbl.find a.sigma (HASHINT2(Ptset.hash r,Tag.hash tag))
-      with
-	  Not_found -> 
-	    let fl,_,accq,_ = 
-	      Ptset.fold (fun q (accf,acchash,accq,aidx) ->
-			    let naccf,acchash,naidx =
-			      merge_trans t a tag q (accf,acchash,aidx )
-			    in
-			      (naccf,acchash,Ptset.add q accq,naidx)
-			 )
-		r (Nil,17,Ptset.empty,0)
-	    in 
-	    let (ls,lls,llls),(rs,rrs,rrrs) = 
-	     form_list_fold_left (fun ((a1,b1,c1),(a2,b2,c2)) _ f _ _ _ ->
-				    let (x1,y1,z1),(x2,y2,z2) = f.st in
-				      ((Ptset.union x1 a1),(Ptset.union y1 b1),(Ptset.union c1 z1)),
-				    ((Ptset.union x2 a2),(Ptset.union y2 b2),(Ptset.union c2 z2)))
-	       ((Ptset.empty,Ptset.empty,Ptset.empty),
-		(Ptset.empty,Ptset.empty,Ptset.empty))
-		fl 
-	    in
-	    let tb,ta = 
-	      Tree.tags t tag 
-	    in 
-	    let tl,htlt,lfin = inter_text tb (tags a ls)
-	    and tll,htllt,llfin = inter_text tb (tags a lls)
-	    and tr,htrt,rfin = inter_text ta (tags a rs)
-	    and trr,htrrt,rrfin = inter_text ta  (tags a rrs)
-	    in
-	    let get_tag = ref Tree.tag in
-	    let first,flabel =
-	      if (llfin && lfin) then (* no stars *)
-		(if htlt || htllt then (Tree.text_below, "#text_below")
-		 else
-		   let etl = Ptset.is_empty tl
-		   and etll = Ptset.is_empty tll
-		   in
-		     if (etl && etll)
-			 then (Tree.mk_nil, "#mk_nil")
-			 else
-			   if etl then 
-			     if Ptset.is_singleton tll 
-			     then begin
-			       set_get_tag get_tag (Ptset.choose tll);
-			       (Tree.tagged_desc (Ptset.choose tll), "#tagged_desc")
-			     end
-			     else (Tree.select_desc_only tll, "#select_desc_only")
-			   else if etll then (Tree.node_child,"#node_child")
-			   else (Tree.select_below tl tll,"#select_below"))
-		  else (* stars or node() *)
-		    if htlt||htllt then (Tree.first_child,"#first_child")
-		    else (Tree.node_child,"#node_child")
-	    and next,nlabel =
-	      if (rrfin && rfin) then (* no stars *)
-		( if htrt || htrrt
-		  then (Tree.text_next, "#text_next")
-		    else
-		      let etr = Ptset.is_empty tr
-		      and etrr = Ptset.is_empty trr
-		      in
-			if etr && etrr 
-			then (mk_nil_ctx, "#mk_nil_ctx")
-			else
-			  if etr then
-			    if Ptset.is_singleton trr 
-			    then begin
-			      set_get_tag get_tag (Ptset.choose trr);
-			      (Tree.tagged_foll_below (Ptset.choose trr),"#tagged_foll_below")
-			    end
-			    else (Tree.select_foll_only trr,"#select_foll_only")
-			  else if etrr then (Tree.node_sibling_ctx,"#node_sibling_ctx")
-			  else 	
-			    (Tree.select_next tr trr,"#select_next") )
-
-		  else if htrt || htrrt then (Tree.next_sibling_ctx,"#next_sibling_ctx")
-		  else (Tree.node_sibling_ctx,"#node_sibling_ctx")
-	    in
-	    let cont = let flist = fl in
-	      fun a t res ctx -> 
-		let s1,res1 = conti a (first t) llls res t
-		and s2,res2 = conti a (next t ctx) rrrs res ctx in
-		let r',rb,rb1,rb2,mark,idxl = eval_formlist s1 s2 flist
-		in	
-		  r',(vb rb)*((vb mark)  + (vb rb1)*res1 + (vb rb2)*res2)	  
-	    in
-	      Hashtbl.add a.sigma (HASHINT2(Ptset.hash r,Tag.hash tag)) (cast_cont cont);
-	      (cast_cont cont)
-		
-	
-(*
-    let rec accepting_among a t r ctx =           
-      if Tree.is_nil t || Ptset.is_empty r then Ptset.empty,0,TS.Nil else 
-	let dispatch,mark,flist,llls,rrrs =
-	  get_trans (fun _ _ _ _ -> failwith "toto") t a (Tree.tag t) r
-	in
-	let s1,n1,res1 = accepting_among a (dispatch.first t) llls t in
-	let s2,n2,res2 = accepting_among a (dispatch.next t ctx) rrrs ctx in
-	let r',rb,rb1,rb2 = eval_formlist s1 s2 flist in
-	  r',(vb rb)*((vb mark) + (vb rb1)* n1 + (vb rb2)*n2),if rb then 
-	    dispatch.consres t res1 res2 rb1 rb2
-	  else TS.Nil *)
-
-    let run a t = assert false (*
-      let st,n,res = accepting_among a t a.init t in
-        if Ptset.is_empty (st) then TS.empty,0 else res,n *)
- 
-    let rec accepting_among_count_no_star  a t r ctx  =
-      if Tree.is_nil t then Ptset.empty,0 else 
-	(get_trans (accepting_among_count_no_star) t a (Tree.tag t) r)
-	  a t ctx
-	    
-(*
-    let rec accepting_among_count_star a t n =     
-	if Tree.is_nil t then n else 
-	  if (Tree.tag t == Tag.attribute) 
-	  then accepting_among_count_star a (Tree.node_sibling t) n
-	  else accepting_among_count_star a (Tree.node_sibling t) 
-	    (accepting_among_count_star a (Tree.node_child t) (1+n))
-
-    let rec accepting_among_count_may_star starstate a t r ctx =
-      if r == starstate then starstate,(accepting_among_count_star a t 0)
-      else
-	if Tree.is_nil t||Ptset.is_empty r then Ptset.empty,0 else 
-	  let dispatch,mark,flist,llls,rrrs =
-	    get_trans (fun _ _ _ _ -> failwith "toto") t a (Tree.tag t) r
-	  in    
-	  let s1,res1 = accepting_among_count_may_star starstate a (dispatch.first t) llls t
-	  and s2,res2 = accepting_among_count_may_star starstate a (dispatch.next t ctx) rrrs ctx
-	  in
-	  let r',rb,rb1,rb2 = eval_formlist s1 s2 flist
-	  in	
-	    r',(vb rb)*((vb mark) + (vb rb1)*res1 + (vb rb2)*res2)      
-	
-*)
-    let run_count a t = 
-      
-      let st,res = match a.starstate with 
-	| None -> accepting_among_count_no_star  a t a.init t 
-	| Some s -> assert false (*accepting_among_count_may_star s a t a.init t  *)
-      in
-        if Ptset.is_empty (st) then 0 else  res
-
-	  
-    let run_time _ _ = failwith "blah"
-	  
-
-    module RealBottomUp = struct
-
-      (* decrease number of arguments *) 
-      let ton t = if Tree.is_nil t then "##"
-      else Tag.to_string (Tree.tag t)
-      ;;
-      let ion t = Tree.dump_node t
-      let memo = Hashtbl.create 4097
-      let rlist = ref []
-
-	let cpt = ref 0;;
-      let rec run a t res r root rinit next targettag r0 first tomark =
-	incr cpt;
-	let res = (vb tomark) + res in
-	let newr,newres = if first then
-	  accepting_among_count_no_star  a t r t 
-	else r, res
-	in      
-	let r,res = if Ptset.is_empty newr then r,0 else newr,newres in	  
-	  if Tree.equal t root then 
-	    if Ptset.intersect r rinit then (r,res,next) 
-	    else (Ptset.empty,0,next)
-	  else
-	  let tag = Tree.tag t in
-	  let parent = Tree.binary_parent t in
-	  let parent_tag = Tree.tag parent in
-	  let left = Tree.is_left t in
-	  let r',mark =
-	      try Hashtbl.find memo (r,parent_tag,left) with
-		| Not_found ->
-		    let pair = 
-		      Hashtbl.fold 
-			(fun q l acc -> 
-			   List.fold_left 
-			     (fun (aq,am) (ts,(mark,form,_)) ->
-				if TagSet.mem parent_tag ts then
-				  let (value,_,_) = if left then
- 				    eval_form_bool form r Ptset.empty
-				  else
-				    eval_form_bool form Ptset.empty r
-				  in
-(*				  let _ = if value then begin
-				    Format.fprintf Format.err_formatter "Can take transition (%i,%s)%s%!"
-				      q (Tag.to_string parent_tag) 
-				      (if mark then "=>" else "->");
-				    pr_frm Format.err_formatter form;
-				    Format.fprintf Format.err_formatter "%! %s(" (if left then "left" else "right");
-				    pr_st Format.err_formatter (Ptset.elements r);
-				    Format.fprintf Format.err_formatter ")\n%!" end;
-			      in *)
-				    if value then (Ptset.add q aq, mark||am) 
-				    else (aq,am)
-				else (aq,am))
-			     acc l				
-			) a.phi (Ptset.empty,false)
-		    in Hashtbl.add memo (r,parent_tag,left) pair;pair
-	  in
-	    if Ptset.is_empty r' then Ptset.empty,0,next
-	    else
-	    if Tree.is_below_right t next then
-	      let rn,resn,nextofnext = run a next 0 r0 t r (Tree.tagged_next next targettag) targettag r0 true false
-	      in
-	      let rn,resn = if Ptset.is_empty rn then Ptset.empty,0 else rn,resn in
-		run a (parent) (resn+res) r' root rinit nextofnext targettag r0 false false
-	    else
-	      run a (parent) (res) r' root rinit next targettag r0 false (mark&&left)
-			    
-		
-		
-      let accept_count a t tag initset =
-	let tree1 = Tree.tagged_lowest t tag in
-	let tree2 = Tree.tagged_next tree1 tag in
-	  let c,b,_ =run a tree1 0 initset t a.init tree2 tag initset true false
-	  in Printf.eprintf "%i\n%!" !cpt;
-	    if Ptset.is_empty c then 0 else b
-			    
-    end *)
-(*
-    module RealBottomUp2 = struct
-      module Formlist = 
-      struct
-	type t = formlist
-	let nil : t = Nil
-	let cons q f i m l = Cons(q,f,i,m,l)
-	let hash = function Nil -> 0 | Cons(_,_,i,_,_) -> max_int land i
-	let pr fmt l = 
-	  let rec loop = function
-	    | Nil -> ()
-	    | Cons(q,f,_,m,l) ->
-		Format.fprintf fmt "%i %s" q (if m then "=>" else "->");
-		pr_frm fmt f;
-		Format.fprintf fmt "\n%!";
-		loop l
-	  in
-	    loop l
-      end
-
-      type ptset_list = Nil | Cons of Ptset.t*int*ptset_list
-      let hpl l = match l with
-	| Nil -> 0
-	| Cons (_,i,_) -> i 
 
-      let cons s l = Cons (s,(Ptset.hash s) + 65599 * (hpl l), l)
-	  
-      let rec empty_size n = 
-	if n == 0 then Nil
-	else cons Ptset.empty (empty_size (n-1))
-	
-      let fold_pl f l acc = 
-	let rec loop l acc = match l with
-	    Nil -> acc
-	  | Cons(s,h,pl) -> loop pl (f s h acc)
-	in
-	  loop l acc
-      let map_pl f l = 
-	let rec loop =
-	  function Nil -> Nil 
-	    | Cons(s,h,ll) -> cons (f s) (loop ll) 
-	in loop l
-
-      let rev_pl l = 
-	let rec loop acc l = match l with 
-	  | Nil -> acc
-	  | Cons(s,_,ll) -> loop (cons s acc) ll
-	in
-	  loop Nil l
-
-      let rev_map_pl f l  = 
-	let rec loop acc l = 
-	  match l with 
-	    | Nil -> acc
-	    | Cons(s,_,ll) -> loop (cons (f s) acc) ll
-	in
-	  loop Nil l
-
-      let merge_int _ rb rb1 rb2 mark _ res1 res2 =
-	if rb then (vb mark) + ((vb rb1)*res1) + ((vb rb2)*res2)
-	else 0
-
-      let td_trans = Hashtbl.create 4096 
-	
-      let choose_jump tagset qtags1 qtagsn a f_nil f_text f_t1 f_s1 f_tn f_sn f_notext =
-	let tags1,hastext1,fin1 = inter_text tagset (tags a qtags1) in
-	let tagsn,hastextn,finn = inter_text tagset (tags a qtagsn) in
-(*	  Format.fprintf Format.err_formatter "Tags below states ";
-	  pr_st Format.err_formatter (Ptset.elements qtags1);
-	  Format.fprintf Format.err_formatter " are { ";
-	  Ptset.iter (fun t -> Format.fprintf Format.err_formatter "%s " (Tag.to_string t)) tags1;
-	  Format.fprintf Format.err_formatter "}, %b,%b\n%!" hastext1 fin1;
-
-	  Format.fprintf Format.err_formatter "Tags below states ";
-	  pr_st Format.err_formatter (Ptset.elements qtagsn);
-	  Format.fprintf Format.err_formatter " are { ";
-	  Ptset.iter (fun t -> Format.fprintf Format.err_formatter "%s " (Tag.to_string t)) tagsn;
-	  Format.fprintf Format.err_formatter "}, %b,%b\n%!" hastextn finn;
-*)
-	  if (hastext1||hastextn) then f_text  (* jumping to text nodes doesn't work really well *)
-	  else if (Ptset.is_empty tags1) && (Ptset.is_empty tagsn) then f_nil
-	  else if (Ptset.is_empty tagsn) then 
-	    if (Ptset.is_singleton tags1) then f_t1 (Ptset.choose tags1)  (* TaggedChild/Sibling *)
-	    else f_s1 tags1 (* SelectChild/Sibling *)
-	  else if (Ptset.is_empty tags1) then 
-	    if (Ptset.is_singleton tagsn) then f_tn (Ptset.choose tagsn) (* TaggedDesc/Following *)
-	    else f_sn tagsn (* SelectDesc/Following *)
-	  else f_notext
-	  
-      let choose_jump_down a b c d =
-	choose_jump a b c d
-	  (Tree.mk_nil)
-	  (Tree.text_below ) 
-	  (fun _ -> Tree.node_child ) (* !! no tagged_child in Tree.ml *)
-	  (fun _ -> Tree.node_child ) (* !! no select_child in Tree.ml *)
-	  (Tree.tagged_desc)
-	  (fun _ -> Tree.node_child ) (* !! no select_desc *)
-	  (Tree.node_child)
-
-      let choose_jump_next a b c d = 
-	choose_jump a b c d
-	  (fun t _ -> Tree.mk_nil t)
-	  (Tree.text_next)
-	  (fun _ -> Tree.node_sibling_ctx) (* !! no tagged_sibling in Tree.ml *)
-	  (fun _ -> Tree.node_sibling_ctx) (* !! no select_child in Tree.ml *)
-	  (Tree.tagged_foll_below)
-	  (fun _ -> Tree.node_sibling_ctx) (* !! no select_foll *)
-	  (Tree.node_sibling_ctx)
-	  
-      module type RS = sig
-	type t
-	type elt
-	val empty : t
-	val cons : elt -> t -> t
-	val concat : t -> t -> t
-      end
-	
-				    
-      let get_trans slist tag a t = 
-	try 
-	  Hashtbl.find td_trans (tag,hpl slist)
-	with
-	  | Not_found -> 
-	      let fl_list,llist,rlist,ca,da,sa,fa = 
-		fold_pl 
-		  (fun set _ (fll_acc,lllacc,rllacc,ca,da,sa,fa) -> (* For each set *)
-		     let fl,ll,rr,ca,da,sa,fa = 
-		       Ptset.fold
-	 		 (fun q acc ->
-			    fst (
-	 		      List.fold_left 
-				(fun (((fl_acc,ll_acc,rl_acc,c_acc,d_acc,s_acc,f_acc),h_acc) as acc) 
-				   (ts,(m,f,_))  ->
-				     if (TagSet.mem tag ts)
-				     then 
-				       let (child,desc,below),(sibl,foll,after) = f.st in
-					 ((Formlist.cons q f h_acc m fl_acc,
-					   Ptset.union ll_acc below,
-					   Ptset.union rl_acc after,
-					   Ptset.union child c_acc,
-					   Ptset.union desc d_acc,
-					   Ptset.union sibl s_acc,
-					   Ptset.union foll f_acc),
-					  HASHINT3(h_acc,f.fid,HASHINT2(q,vb m)))
-				   else acc ) (acc,0) (
-				  try Hashtbl.find a.phi q 
-				  with
-				      Not_found -> Printf.eprintf "Looking for state %i, doesn't exist!!!\n%!"
-					q;[]
-				))
-			      
-			 ) set (Formlist.nil,Ptset.empty,Ptset.empty,ca,da,sa,fa)
-		     in fl::fll_acc, cons ll lllacc, cons rr rllacc,ca,da,sa,fa)
-		  slist ([],Nil,Nil,Ptset.empty,Ptset.empty,Ptset.empty,Ptset.empty)
-	      in
-		(* Logic to chose the first and next function *)
-	      let tags_below,tags_after = Tree.tags t tag in
-	      let first = choose_jump_down tags_below ca da a
-	      and next = choose_jump_next tags_after sa fa a in	
-	      let v = (fl_list,llist,rlist,first,next) in
-		Hashtbl.add td_trans (tag, hpl slist) v; v
-		  
-
-      let top_down ?(noright=false) a merge null t slist ctx slot_size =	
-	let pempty = empty_size slot_size in	
-
-	let eval_fold2_slist fll sl1 sl2 res1 res2 t =
-	  let res = Array.copy res1 in
-	  let rec fold l1 l2 fll i aq = match l1,l2,fll with
-	    | Cons(s1,_,ll1), Cons(s2, _ ,ll2),fl::fll -> 
-		let r',rb,rb1,rb2,mark = eval_formlist s1 s2 fl in
-		let _ = res.(i) <- merge null rb rb1 rb2 mark t res1.(i) res2.(i) 
-		in
-(*		let _ = Format.fprintf Format.err_formatter "(%b,%b,%b,%b) Result was %i %i, now %i\n%!"
-		  rb rb1 rb2 mark (Obj.magic res1.(i))  (Obj.magic res2.(i)) (Obj.magic res.(i));
-		in *)
-		  
-		  fold ll1 ll2 fll (i+1) (cons r' aq)
-	    | Nil, Nil,[] -> aq,res
-	    | _ -> assert false
-	  in
-	    fold sl1 sl2 fll 0 Nil
-	in
-	let rec loop  t slist ctx = 
-	  if Tree.is_nil t then (pempty,Array.make slot_size null)
-	  else	    
-	    let tag = Tree.tag t in
-	    let fl_list,llist,rlist,first,next = get_trans slist tag a t in
-	    let sl1,res1 = loop (first t) llist t in
-	    let sl2,res2 = if noright then (pempty,Array.make slot_size null) 
-	    else loop (next t ctx) rlist ctx in
-	    eval_fold2_slist fl_list sl1 sl2 res1 res2 t	    
-	in
-	  loop t slist ctx
-
-	let run_top_down_count a t =
-	  let init = cons a.init Nil in
-	  let _,res = top_down a (fun _ rb rb1 rb2 mark t res1 res2 ->
-				    (vb rb)*( (vb mark) + (vb rb1)*res1 + (vb rb2)*res2))
-	    0 t init t 1
-	  in res.(0)
-	;;
-
-	let run_top_down a t =
-	  let init = cons a.init Nil in
-	  let _,res = 
-	    top_down a (fun null rb rb1 rb2 mark t res1 res2 ->
-			 if rb then
-			   TS.concat 
-			     (TS.concat	(if mark then TS.Sing(t) else null)
-				(if rb1 then res1 else null))
-			       (if rb2 then res2 else null)
-			 else null)
-	      TS.Nil t init t 1
-	  in res.(0)
-	;;
-
-
-    end
-*)
     module type ResultSet = 
     sig
       type t
@@ -938,7 +479,6 @@ type 'a t = {
       let concat t1 t2 = { node = Concat(t1.node,t2.node); length = t1.length+t2.length }
       let append e t = { node = Concat(t.node,Cons(e,Nil)); length = t.length+1 } 
 	
-	
       let fold f l acc = 
 	let rec loop acc t = match t with
 	  | Nil -> acc
@@ -970,6 +510,8 @@ type 'a t = {
 
     module Run (RS : ResultSet) =
     struct
+      let fmt = Format.err_formatter
+      let pr x = Format.fprintf fmt x
       module Formlist = 
       struct
 	type t = formlist
@@ -1010,6 +552,11 @@ type 'a t = {
 	  function Nil -> Nil 
 	    | Cons(s,h,ll) -> cons (f s) (loop ll) 
 	in loop l
+      let iter_pl f l = 
+	let rec loop =
+	  function Nil -> ()
+	    | Cons(s,h,ll) ->  (f s);(loop ll) 
+	in loop l
 
       let rev_pl l = 
 	let rec loop acc l = match l with 
@@ -1104,6 +651,7 @@ type 'a t = {
 				     if (TagSet.mem tag ts)
 				     then 
 				       let (child,desc,below),(sibl,foll,after) = f.st in
+				       let h_acc = HASHINT3(h_acc,f.fid,HASHINT2(q,vb m)) in
 					 ((Formlist.cons q f h_acc m fl_acc,
 					   Ptset.union ll_acc below,
 					   Ptset.union rl_acc after,
@@ -1111,7 +659,7 @@ type 'a t = {
 					   Ptset.union desc d_acc,
 					   Ptset.union sibl s_acc,
 					   Ptset.union foll f_acc),
-					  HASHINT3(h_acc,f.fid,HASHINT2(q,vb m)))
+					  h_acc)				 
 				   else acc ) (acc,0) (
 				  try Hashtbl.find a.phi q 
 				  with
@@ -1147,6 +695,13 @@ type 'a t = {
 	  let rec fold l1 l2 fll i aq = match l1,l2,fll with
 	    | Cons(s1,_,ll1), Cons(s2, _ ,ll2),fl::fll -> 
 		let r',rb,rb1,rb2,mark = eval_formlist s1 s2 fl in
+(*		let _ = pr "Evaluation context : "; pr_st fmt (Ptset.elements s1);
+		  pr_st fmt (Ptset.elements s2);
+		  pr "Formlist (%i) : " (Formlist.hash fl);
+		  Formlist.pr fmt fl;
+		  pr "Results : "; pr_st fmt (Ptset.elements r');
+		  pr ", %b %b %b %b\n%!" rb rb1 rb2 mark
+		in *)
 		let _ = res.(i) <- merge rb rb1 rb2 mark t res1.(i) res2.(i) 
 		in		  
 		  fold ll1 ll2 fll (i+1) (cons r' aq)
@@ -1157,14 +712,25 @@ type 'a t = {
 	in
 	let null_result() = (pempty,Array.make slot_size RS.empty) in
 	let rec loop t slist ctx = 
+	  let (a,b) = 
 	  if Tree.is_nil t then null_result()
 	  else	    
 	    let tag = Tree.tag t in
 	    let fl_list,llist,rlist,first,next = get_trans slist tag a t in
+(*	    let _ = pr "For tag %s,node %s, returning formulae list: \n%!"
+	      (Tag.to_string tag) (Tree.dump_node t);
+	      List.iter (fun f -> Formlist.pr fmt f;pr "\n%!") fl_list
+	    in*)
 	    let sl1,res1 = loop (first t) llist t in
-	    let sl2,res2 = if noright then null_result()
-	    else loop (next t ctx) rlist ctx in
+	    let sl2,res2 = loop (next t ctx) rlist ctx in
 	      eval_fold2_slist fl_list sl1 sl2 res1 res2 t	    
+	  in 
+(*	  let _ = pr "Inside topdown call: tree was %s, tag = %s" (Tree.dump_node t) (if Tree.is_nil t then "###" 
+										      else Tag.to_string (Tree.tag t));
+	    iter_pl (fun s -> (pr_st fmt (Ptset.elements s))) a;
+	    Array.iter (fun i -> pr "%i" (RS.length i)) b;
+	    pr "\n%!"; in*) (a,b)
+	    
 	in
 	let loop_no_right t slist ctx =
 	  if Tree.is_nil t then null_result()
@@ -1240,8 +806,7 @@ type 'a t = {
 		results = imap }
 
 	end
-	let fmt = Format.err_formatter
-	let pr x = Format.fprintf fmt x
+
 	let h_fold = Hashtbl.create 511 
 
 	let fold_f_conf  t slist fl_list conf dir= 
@@ -1296,8 +861,10 @@ type 'a t = {
 	    Hashtbl.fold (fun q l acc ->
 			    List.fold_left (fun  (fl_acc,h_acc) (ts,(m,f,_))  ->
 					      if TagSet.mem ptag ts				       
-					      then (Formlist.cons q f h_acc m fl_acc,
-						    HASHINT3(h_acc,f.fid,q))
+					      then
+						let h_acc = HASHINT3(h_acc,f.fid,HASHINT2(q,vb m)) in
+						  (Formlist.cons q f h_acc m fl_acc,
+						   h_acc)
 					      else (fl_acc,h_acc))
 	    		      acc l)
 	      a.phi (Formlist.nil,0)
@@ -1306,37 +873,38 @@ type 'a t = {
 	  in
 	    (Hashtbl.add h_trans key res;res) 
 		      
-
+	      
+	let h_tdconf = Hashtbl.create 511 
 	let rec bottom_up a tree conf next jump_fun root dotd init accu = 
 	  if (not dotd) && (Configuration.is_empty conf ) then
-	 (*   let _ = pr "Returning early from %s, with accu %i, next is %s\n%!" 
-	      (Tree.dump_node tree) (Obj.magic accu) (Tree.dump_node next)
-	      in *)
-	    accu,conf,next
+(*	    	    let _ = pr "Returning early from %s, with accu %i, next is %s\n%!" 
+		    (Tree.dump_node tree) (Obj.magic accu) (Tree.dump_node next)
+		    in *)
+	    accu,conf,next 
 	  else
-(*	  let _ =   
+(*	    let _ =   
 	    pr "Going bottom up for tree with tag %s configuration is" 
-	      (if Tree.is_nil tree then "###" else Tag.to_string (Tree.tag tree));
+	    (if Tree.is_nil tree then "###" else Tag.to_string (Tree.tag tree));
 	    Configuration.pr fmt conf 
-	  in *)
-	  let below_right = Tree.is_below_right tree next in 
-(*	  let _ = Format.fprintf Format.err_formatter "below_right %s %s = %b\n%!"
-	    (Tree.dump_node tree) (Tree.dump_node next)  below_right
-	  in *)
-	  let accu,rightconf,next_of_next = 	    
+	    in *)
+	    let below_right = Tree.is_below_right tree next in 
+	      (*	  let _ = Format.fprintf Format.err_formatter "below_right %s %s = %b\n%!"
+			  (Tree.dump_node tree) (Tree.dump_node next)  below_right
+			  in *)
+	    let accu,rightconf,next_of_next = 	    
 	    if below_right then (* jump to the next *)
-(*	      let _ = pr "Jumping to %s\n%!" (Tree.dump_node next) in  *)
+(*	      let _ = pr "Jumping to %s tag %s\n%!" (Tree.dump_node next) (Tag.to_string (Tree.tag next)) in   *)
 	      bottom_up a next conf (jump_fun next) jump_fun (Tree.next_sibling tree) true init accu
 	    else accu,Configuration.empty,next
 	  in 
-(*	  let _ = if below_right then pr "Returning from jump to next\n" in  *)
+(*	  let _ = if below_right then pr "Returning from jump to next = %s\n" (Tree.dump_node next)in   *)
 	  let sub =
 	    if dotd then
 	      if below_right then (* only recurse on the left subtree *)
-	(*	let _ = pr "Topdown on subtree\n%!" in     *)
+(*		let _ = pr "Topdown on left subtree\n%!" in      *)
 		prepare_topdown a tree true
 	      else 
-(*		let _ = pr "Topdown on whole tree\n%!" in   *)
+(*		let _ = pr "Topdown on whole tree\n%!" in *)
 		prepare_topdown a tree false
 	    else conf
 	  in
@@ -1344,10 +912,10 @@ type 'a t = {
 	    (Configuration.merge rightconf sub, next_of_next)
 	  in
 	    if Tree.equal tree root then 
-(*	      let _ = pr "Stopping at root, configuration after topdown is:" ;
+(*	        let _ = pr "Stopping at root, configuration after topdown is:" ;
 		Configuration.pr fmt conf;
 		pr "\n%!" 		
-	      in  *) accu,conf,next 
+	      in *)  accu,conf,next 
 	    else	      
 	  let parent = Tree.binary_parent tree in
 	  let ptag = Tree.tag parent in
@@ -1355,7 +923,7 @@ type 'a t = {
 	  let slist = Configuration.Ptss.fold (fun e a -> cons e a) conf.Configuration.sets Nil in
 	  let fl_list = get_up_trans slist ptag a parent in
 	  let slist = rev_pl (slist) in 
-(*	  let _ = pr "Current conf is : %i " (Tree.id tree);
+(*	  let _ = pr "Current conf is : %s " (Tree.dump_node tree); 
 	    Configuration.pr fmt conf;
 	    pr "\n" 
 	  in *)
@@ -1377,9 +945,25 @@ type 'a t = {
 	    bottom_up a parent newconf next jump_fun root false init accu
 
 	and prepare_topdown a t noright =
-(*	  pr "Going top down on tree with tag %s\n%!" 
-	    (if Tree.is_nil t then "###" else (Tag.to_string(Tree.tag t))); *)
- 	  let r = cons a.states Nil in
+	  let tag = Tree.tag t in
+(*	  pr "Going top down on tree with tag %s = %s "  
+	    (if Tree.is_nil t then "###" else (Tag.to_string(Tree.tag t))) (Tree.dump_node t); *)
+ 	  let r = 
+	    try
+	      Hashtbl.find h_tdconf tag
+	    with
+	      | Not_found -> 
+		  let res = Hashtbl.fold (fun q l acc -> 
+					    if List.exists (fun (ts,_) -> TagSet.mem tag ts) l
+					    then Ptset.add q acc
+					    else acc) a.phi Ptset.empty
+		  in Hashtbl.add h_tdconf tag res;res
+	  in 
+(*	  let _ = pr ", among ";
+	    pr_st fmt (Ptset.elements r);
+	    pr "\n%!";
+	  in *)
+	  let r = cons r Nil in
 	  let set,res = top_down (~noright:noright) a t r t 1 in
 	  let set = match set with
 	    | Cons(x,_,Nil) ->x
@@ -1392,7 +976,7 @@ type 'a t = {
 
 
 
-	let run_bottom_up_contains a t =
+	let run_bottom_up a t k =
 	  let trlist = Hashtbl.find a.phi (Ptset.choose a.init)
 	  in
 	  let init = List.fold_left 
@@ -1400,12 +984,18 @@ type 'a t = {
 	       Ptset.union acc (let (_,_,l) = fst (f.st) in l))
 	    Ptset.empty trlist
 	  in
-	  let tree1 = Tree.text_below t in
-	  let jump_fun = fun tree -> Tree.text_next tree t  in
+	  let tree1,jump_fun =
+	    match k with
+	      | `TAG (tag) -> 
+		  (*Tree.tagged_lowest t tag, fun tree -> Tree.tagged_next tree tag*)
+		  (Tree.tagged_desc tag t, fun tree -> Tree.tagged_foll_below tag tree t)
+	      | `CONTAINS(_) -> (Tree.text_below t,fun tree -> Tree.text_next tree t)
+	      | _ -> assert false
+	  in
 	  let tree2 = jump_fun tree1 in
 	  let rec loop tree next acc = 
-(*	    let _ = pr "\n_________________________\nNew iteration\n" in *)
-(*	    let _ = pr "Jumping to %s\n%!" (Tree.dump_node tree) in  *)
+(*	    let _ = pr "\n_________________________\nNew iteration\n" in 
+	    let _ = pr "Jumping to %s\n%!" (Tree.dump_node tree) in  *)
 	    let acc,conf,next_of_next = bottom_up a tree 
 	      Configuration.empty next jump_fun (Tree.root tree) true init acc
 	    in 
@@ -1423,21 +1013,10 @@ type 'a t = {
 	  loop tree1 tree2 RS.empty
 
 
-
-
-
-
-
-
-
-
-
-
-
     end
           
     let top_down_count a t = let module RI = Run(Integer) in Integer.length (RI.run_top_down a t)
     let top_down a t = let module RI = Run(IdSet) in (RI.run_top_down a t)
-    let bottom_up_count_contains a t = let module RI = Run(Integer) in Integer.length (RI.run_bottom_up_contains a t)
-    let bottom_up_count a t = failwith "not implemented"
+    let bottom_up_count a t k = let module RI = Run(Integer) in Integer.length (RI.run_bottom_up a t k)
+