(* Todo refactor and remove this alias *)
INCLUDE "debug.ml"
module Tree = Tree.Binary


let gen_id =
  let id = ref (-1) in
    fun () -> incr id;!id


module State = struct

  type t = int
  let mk = gen_id

end
let mk_state = State.mk

type state = State.t

type predicate = [ `Left of (Tree.t -> bool) | `Right of (Tree.t -> bool) |
		       `True
		 ]

let eval_pred t = 
  function `True -> true
    | `Left f | `Right f -> f t
	
type formula_expr = 
  | False | True
  | Or of formula * formula 
  | And of formula * formula 
  | Atom of ([ `Left | `Right ]*bool*state)
and formula = { fid: int;
		pos : formula_expr;
		neg : formula;
		st : Ptset.t*Ptset.t;
		size: int;
	      }
    

module FormNode = 
struct
  type t = formula
  let hash = function
    | False -> 0
    | True -> 1
    | And(f1,f2) -> 2+17*f1.fid + 37*f2.fid
    | Or(f1,f2) -> 3+101*f1.fid + 253*f2.fid
    | Atom(d,b,s) -> 5+(if d=`Left then 11 else 19)*(if b then 23 else 31)*s

  let hash t = (hash t.pos) land max_int

  let equal f1 f2 = 
    match f1.pos,f2.pos with
      | False,False | True,True -> true
      | Atom(d1,b1,s1), Atom(d2,b2,s2) when (d1 = d2) && (b1=b2) &&(s1=s2) -> true
      | Or(g1,g2),Or(h1,h2) 
      | And(g1,g2),And(h1,h2)  -> g1.fid == h1.fid && g2.fid == h2.fid
      | _ -> false
end
module WH = Weak.Make(FormNode)

let f_pool = WH.create 107

let true_,false_ = 
  let rec t = { fid = 1; pos = True; neg = f ; st = Ptset.empty,Ptset.empty; size =1; }
  and f = { fid = 0; pos = False; neg = t; st = Ptset.empty,Ptset.empty; size = 1; }
  in 
    WH.add f_pool f;
    WH.add f_pool t;
    t,f

let is_true f = f.fid == 1
let is_false f = f.fid == 0


let cons pos neg s1 s2 size1 size2 = 
  let rec pnode = 
    { fid = gen_id ();
      pos = pos;
      neg = nnode;
      st = s1; 
      size = size1;}
  and nnode = { 
    fid = gen_id ();
    pos = neg;
    neg = pnode;
    st = s2;
    size = size2;
  }
  in
    (WH.merge f_pool pnode),(WH.merge f_pool nnode)

let atom_  d p s = 
  let si = Ptset.singleton s in
  let ss = match d with
    | `Left -> si,Ptset.empty
    | `Right -> Ptset.empty,si
  in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)

let merge_states f1 f2 =
  let sp = 
    Ptset.union (fst f1.st) (fst f2.st),
    Ptset.union (snd f1.st) (snd f2.st)
  and sn = 
    Ptset.union (fst f1.neg.st) (fst f2.neg.st),
    Ptset.union (snd f1.neg.st) (snd f2.neg.st)
  in
    sp,sn

let full_or_ f1 f2 = 
  let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
  let sp,sn = merge_states f1 f2 in
  let psize = f1.size + f2.size in
  let nsize = f1.neg.size + f2.neg.size in
    fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize )

let or_ f1 f2 = 
  let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
  if is_true f1 || is_true f2 then true_
  else if is_false f1 && is_false f2 then false_
  else if is_false f1 then f2
  else if is_false f2 then f1
  else 
    let psize = f1.size + f2.size in
    let nsize = f1.neg.size + f2.neg.size in
    let sp,sn = merge_states f1 f2 in
      fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize)



let and_ f1 f2 = 
  let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
  if is_true f1 && is_true f2 then true_
  else if is_false f1 || is_false f2 then false_
  else if is_true f1 then f2 
  else if is_true f2 then f1
  else
    let psize = f1.size + f2.size in
    let nsize = f1.neg.size + f2.neg.size in
    let sp,sn = merge_states f1 f2 in
      fst (cons (And(f1,f2)) (Or(f1.neg,f2.neg)) sp sn psize nsize)
	

let not_ f = f.neg


module HTagSetKey = 
struct 
  type t = Ptset.t*Tag.t 
  let int_hash key = key lsl 31 lor (key lsl 8)
  let equal (s1,s2) (t1,t2) = Tag.equal s2 t2 &&  Ptset.equal s1 t1
  let hash (s,t) = int_hash (Ptset.hash s) lxor ( int_hash (Tag.hash t))
end
module HTagSet = Hashtbl.Make(HTagSetKey)

type t = { 
    id : int;
    mutable states : Ptset.t;
    init : Ptset.t;
    mutable final : Ptset.t;
    universal : Ptset.t;
    (* Transitions of the Alternating automaton *)
    phi : (state,(TagSet.t*(bool*formula*predicate)) list) Hashtbl.t;
    delta : (state*Tag.t, (bool*formula*predicate)) Hashtbl.t;
(*    delta : (state,(bool*formula*predicate) TagMap.t) Hashtbl.t; *)
    sigma : (bool*formula*(predicate list*predicate list)*bool) HTagSet.t;
  }
	   
  module Pair (X : Set.OrderedType) (Y : Set.OrderedType) =
  struct
    type t = X.t*Y.t
    let compare (x1,y1) (x2,y2) =
      let r = X.compare x1 x2 in
	if r == 0 then Y.compare y1 y2
	else r
  end

  module PL = Set.Make (Pair (Ptset) (Ptset))


      let pr_st ppf l = Format.fprintf ppf "{";
    begin
      match l with
	|	[] -> ()
	| [s] -> Format.fprintf ppf " %i" s
	| p::r -> Format.fprintf ppf " %i" p;
	    List.iter (fun i -> Format.fprintf ppf "; %i" i) r
    end;
    Format.fprintf ppf " }"
  let rec pr_frm ppf f = match f.pos with
    | True -> Format.fprintf ppf "⊤"
    | False -> Format.fprintf ppf "⊥"
    | And(f1,f2) -> 
	Format.fprintf ppf "(";
	(pr_frm ppf f1);
	Format.fprintf ppf ") ∧ (";
	(pr_frm ppf f2);
	Format.fprintf ppf ")"
    | Or(f1,f2) -> 
	(pr_frm ppf f1);
	Format.fprintf ppf " ∨ ";
	(pr_frm ppf f2);
    | Atom(dir,b,s) -> Format.fprintf ppf "%s%s[%i]"
	(if b then "" else "¬")
	(if dir = `Left then "↓₁" else "↓₂") s 	  

  let dnf_hash = Hashtbl.create 17

  let rec dnf_aux f = match f.pos with
    | False -> PL.empty
    | True -> PL.singleton (Ptset.empty,Ptset.empty)
    | Atom(`Left,_,s) -> PL.singleton (Ptset.singleton s,Ptset.empty) 
    | Atom(`Right,_,s) -> PL.singleton (Ptset.empty,Ptset.singleton s)
    | Or(f1,f2) -> PL.union (dnf f1) (dnf f2)
    | And(f1,f2) ->
	  let pl1 = dnf f1
	  and pl2 = dnf f2
	  in
	    PL.fold (fun (s1,s2) acc ->
		       PL.fold ( fun (s1', s2') acc' ->
				   (PL.add 
				      ((Ptset.union s1 s1'),
				       (Ptset.union s2 s2')) acc') )
			  pl2 acc ) 
	      pl1 PL.empty


  and dnf f = 
    try 
      Hashtbl.find dnf_hash f.fid
    with
	Not_found -> 
	  let d = dnf_aux f in
	    Hashtbl.add dnf_hash f.fid d;d


  let can_top_down f = 
    let nf = dnf f in
      if (PL.cardinal nf > 3)then None
      else match PL.elements nf with
	| [(s1,s2); (t1,t2); (u1,u2)] when
	    Ptset.is_empty s1 && Ptset.is_empty s2 && Ptset.is_empty t1 && Ptset.is_empty u2
	      -> Some(true,t2,u1)
	| [(t1,t2); (u1,u2)] when Ptset.is_empty t1 && Ptset.is_empty u2
	    -> Some(false,t2,u1)
	| _ -> None

     
  let equal_form f1 f2 = 
    (f1.fid == f2.fid) || (FormNode.equal f1 f2) || (PL.equal (dnf f1) (dnf f2))
      
  let dump ppf a = 
    Format.fprintf ppf "Automaton (%i) :\n" a.id;
    Format.fprintf ppf "States : "; pr_st ppf (Ptset.elements a.states);
    Format.fprintf ppf "\nInitial states : "; pr_st ppf (Ptset.elements a.init);
    Format.fprintf ppf "\nFinal states : "; pr_st ppf (Ptset.elements a.final);
    Format.fprintf ppf "\nUniversal states : "; pr_st ppf (Ptset.elements a.universal);
    Format.fprintf ppf "\nAlternating transitions :\n------------------------------\n";
    let l = Hashtbl.fold (fun k t acc -> 
			    (List.map (fun (t,(m,f,p)) -> (t,k),(m,f,p)) t)@ acc) a.phi [] in
    let l = List.sort (fun ((tsx,x),_) ((tsy,y),_) -> if x-y == 0 then TagSet.compare tsx tsy else x-y) l in
    List.iter (fun ((ts,q),(b,f,_)) ->
		    
		    let s = 
		      if TagSet.is_finite ts 
		      then "{" ^ (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) ts "") ^"}"
		      else let cts = TagSet.neg ts in
			if TagSet.is_empty cts then "*" else
			  (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) cts "*\\{"
			  )^ "}"
		    in
		      Format.fprintf ppf "(%s,%i) %s " s q (if b then "=>" else "->");
		      pr_frm ppf f;
		      Format.fprintf ppf "\n")l;
    
    Format.fprintf ppf "NFA transitions :\n------------------------------\n";
    HTagSet.iter (fun (qs,t) (b,f,_,_) ->
		    pr_st ppf (Ptset.elements qs);
		    Format.fprintf ppf ",%s  %s " (Tag.to_string t) (if b then "=>" else "->");
		    pr_frm ppf f;
		    Format.fprintf ppf "(fid=%i) left=" f.fid;
		    let l,r = f.st in pr_st ppf (Ptset.elements l);
		      Format.fprintf ppf ", right=";
		      pr_st ppf (Ptset.elements r);
		      Format.fprintf ppf "\n";
		 ) a.sigma;    
    Format.fprintf ppf "=======================================\n"
    
  module Transitions = struct
    type t = state*TagSet.t*bool*formula*predicate
    let ( ?< ) x = x
    let ( >< ) state (l,b) = state,(l,b,`True)
    let ( ><@ ) state (l,b,p) = state,(l,b,p)
    let ( >=> ) (state,(label,mark,pred)) form = (state,label,mark,form,pred)
    let ( +| ) f1 f2 = or_ f1 f2
    let ( *& ) f1 f2 = and_ f1 f2
    let ( ** ) d s = atom_ d true s


  end
  type transition = Transitions.t

  let equal_trans (q1,t1,m1,f1,_) (q2,t2,m2,f2,_) =
    (q1 == q2) && (TagSet.equal t1 t2) && (m1 == m2) && (equal_form f1 f2)
    
  module TS = 
  struct
    type node = Nil | Cons of Tree.t * node | Concat of node*node
    and t = { node : node; size : int }
    let node n s = { node=n; size = s }

    let empty = node Nil 0 
      
    let cons e t = node (Cons(e,t.node)) (t.size+1)
    let concat t1 t2 = node (Concat (t1.node,t2.node)) (t1.size+t2.size)
    let append e t = concat t (cons e empty)
      
    let to_list_rev t = 
      let rec aux acc l rest =     
	match l with
	  | Nil -> begin
	      match rest with 
		| Nil -> acc
		| Cons(e,t) -> aux (e::acc) t Nil
		| Concat(t1,t2) -> aux acc t1 t2
	    end
	  | Cons(e,r) -> aux (e::acc) r rest
	  | Concat(t1,t2) -> aux acc t1 (Concat(t2,rest))
      in
    aux [] t.node Nil

    let length = function { size = s } -> s

    let iter f { node = n } =
      let rec loop = function
	| Nil -> ()
	| Cons(e,n) -> let _ = f e in loop n
	| Concat(n1,n2) -> let _ = loop n1 in loop n2
      in loop n

  end
  module TS2 = 
  struct
    type t = string
    let empty = String.make  10_000_000 '0'
    let cons e t = t.[Tree.id e] <- '1';t
    let append = cons
    let concat s1 s2 = failwith "not implemented"

    let length t = 
      let res = ref 0 in
	for i = 0 to 9_999_999 do
	  if t.[i] == '1' then
	    incr res
	done; !res
      
    let iter f t =  failwith "not implemented"
    let to_list_rev t = failwith "not implemented"
  end

  module BottomUpNew = struct
    
IFDEF DEBUG
THEN
    type trace = 
      | TNil of Ptset.t*Ptset.t
      | TNode of Ptset.t*Ptset.t*bool* (int*bool*formula) list
		    
    let traces = Hashtbl.create 17
    let dump_trace t = 
      let out = open_out "debug_trace.dot"
      in
      let outf = Format.formatter_of_out_channel out in      
	
      let rec aux t num =
	if Tree.is_node t 
	then
	  match (try Hashtbl.find traces (Tree.id t) with Not_found -> TNil(Ptset.empty,Ptset.empty)) with
	    | TNode(r,s,mark,trs) ->
		let numl = aux (Tree.left t) num in
		let numr = aux (Tree.right t) (numl+1) in
		let mynum = numr + 1 in
		  Format.fprintf outf "n%i [ label=\"<%s>\\nr=" mynum (Tag.to_string (Tree.tag t));
		  pr_st outf (Ptset.elements r);
		  Format.fprintf outf "\\ns=";
		  pr_st outf (Ptset.elements s);
		  List.iter (fun (q,m,f) ->
			       Format.fprintf outf "\\n%i %s" q (if m then "⇨" else "→");
			       pr_frm outf f ) trs;
		  Format.fprintf outf "\", %s shape=box ];\n"
		    (if mark then "color=cyan1, style=filled," else "");		
		  let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numl in
		  let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numr in
		  mynum
	    | TNil(r,s) -> Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num;
		pr_st outf (Ptset.elements r);
		Format.fprintf outf "\\ns=";
		pr_st outf (Ptset.elements s);
		Format.fprintf outf "\"];\n";num
	else
	  match Hashtbl.find traces (-10) with
	    | TNil(r,s) -> 
		Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num;
		pr_st outf (Ptset.elements r);
		Format.fprintf outf "\\ns=";
		pr_st outf (Ptset.elements s);
		Format.fprintf outf "\"];\n";
		num
	    | _ -> assert false

      in
	Format.fprintf outf "digraph G {\n";
	ignore(aux t 0);
	Format.fprintf outf "}\n%!";
	close_out out;
	ignore(Sys.command "dot -Tsvg debug_trace.dot > debug_trace.svg")
END



    module HFEval = Hashtbl.Make(
      struct
	type t = int*Ptset.t*Ptset.t
	let equal (a,b,c) (d,e,f) =
	  a==d && (Ptset.equal b e) && (Ptset.equal c f)
	let hash (a,b,c) = 
	  a+17*(Ptset.hash b) + 31*(Ptset.hash c)
      end)
	
    let hfeval = HFEval.create 4097
     

(*    let miss = ref 0 
    let call = ref 0
    let timeref = ref 0.0
    let timerefall = ref 0.0
    let time f x = 
      incr call;
      let t1 =  Unix.gettimeofday ()
      in let r = f x
      in 
	timeref := !timeref +. ((Unix.gettimeofday()) -. t1);
	r

    let timeall f x = 
      let t1 =  Unix.gettimeofday ()
      in let r = f x
      in 
	timerefall := !timerefall +. ((Unix.gettimeofday()) -. t1);
	r

*)


    let eval_form_bool f s1 s2 =      
      let rec eval f = match f.pos with
	| Atom(`Left,b,q) -> if b == (Ptset.mem q s1) then (true,true,false) else false,false,false
	| Atom(`Right,b,q) -> if b == (Ptset.mem q s2) then (true,false,true) else false,false,false
	    (* test some inlining *)
	| True -> true,true,true
	| False -> false,false,false
	| _ ->
	    try	  
	       HFEval.find hfeval (f.fid,s1,s2) 
	    with
	      |	Not_found -> let r = 
		  match f.pos with
		    | Or(f1,f2) ->	    
			let b1,rl1,rr1 = eval f1 
			in
			  if b1 && rl1 && rr1 then (true,true,true)
			  else
			    let b2,rl2,rr2 = eval f2
			    in
			    let rl1,rr1 = if b1 then rl1,rr1 else false,false
			    and rl2,rr2 = if b2 then rl2,rr2 else false,false
			    in (b1 || b2, rl1||rl2,rr1||rr2)				 
		    | And(f1,f2) -> 
			let b1,rl1,rr1 = eval f1 in
			  if b1 && rl1 && rr1 then (true,true,true)
			  else if b1 
			  then let b2,rl2,rr2 = eval f2 in
			    if b2 then (true,rl1||rl2,rr1||rr2)
			    else (false,false,false)
			  else (false,false,false) 
		    | _ -> assert false
		in
		  HFEval.add hfeval (f.fid,s1,s2) r;
		  r
      in eval f


    module HFEvalDir = Hashtbl.Make(
      struct
	type t = int*Ptset.t*[`Left | `Right ]
	let equal (a,b,c) (d,e,f) =
	  a==d && (Ptset.equal b e) && (c = f)
	let hash_dir = function `Left -> 7919 
	  | `Right -> 3517

	let hash (a,b,c) = 
	  a+17*(Ptset.hash b) + 31*(hash_dir c)
      end)
	
    let hfeval_dir = HFEvalDir.create 4097


    let eval_dir dir f s = 
      let rec eval f = match f.pos with
	| Atom(d,b,q) when d = dir -> if b == (Ptset.mem q s) then true_ else false_
	| Atom(_,b,q) -> f
	    (* test some inlining *)
	| True -> true_
	| False -> false_
	| _ ->
 	    try	  
	      HFEvalDir.find hfeval_dir (f.fid,s,dir) 
	    with
	      | Not_found -> 
		  let r = 
		    match f.pos with
		      | Or(f1,f2) ->	    
			  let f1 = eval f1 
			  in
			    if is_true f1 then true_
			    else if is_false f1 then eval f2
			    else or_ f1 f2				 
		      | And(f1,f2) -> 
			  let f1 = eval f1 in
			    if is_false f1 then false_
			    else if is_true f1 then eval f2
			    else and_ f1 f2
		      | _ -> assert false
		  in
		    HFEvalDir.add hfeval_dir (f.fid,s,dir) r;
		    r
	  
      in eval f



    let fstate_pool = Hashtbl.create 11

    let merge_pred a b = match a,b with
      | Some(f1), Some(f2) -> Some(fun x -> f1 x || f2 x)
      | None,None -> None
      | None,Some(_) -> b
      | Some(_),None -> a

    let acc_pred p l1 l2 = match p with
      | `Left _ -> p::l1,l2
      | `Right _ -> l1,p::l2
      | _ -> l1,l2


    let merge_trans t a tag q acc = 
      List.fold_left (fun (accf,accm,acchtrue) (ts,(m,f,pred)) ->
			if TagSet.mem tag ts 
			then
			  let tmpf,hastrue = 
			    if is_true f then
			      let newfinal =
				try Hashtbl.find fstate_pool f.fid with
				  | Not_found -> let s = mk_state() in 
				      a.states <- Ptset.add s a.states;
				      a.final <- Ptset.add s a.final;
				      Hashtbl.add fstate_pool f.fid s;s
			      in
				(atom_ `Left true newfinal),true
			    else f,false in
			    (or_ tmpf accf,accm||m,acchtrue||hastrue)
			else (accf,accm,acchtrue)
		     ) acc (Hashtbl.find a.phi q)


    let get_trans t a tag r = 
      try
	let mark,f,predl,has_true = 
	  HTagSet.find a.sigma (r,tag)
	in f.st,f,mark,has_true,r
      with
	  Not_found -> 
	    let f,mark,has_true,accq = 
	      Ptset.fold (fun q (accf,accm,acchtrue,accq) ->
			    let naccf,naccm,nacctrue =
			      merge_trans t a tag q (accf,accm,acchtrue )
			    in
			      if is_false naccf then (naccf,naccm,nacctrue,accq)
			      else (naccf,naccm,nacctrue,Ptset.add q accq)
			 )
		r (false_,false,false,Ptset.empty)
	    in 
	      HTagSet.add a.sigma (accq,tag) (mark,f,([],[]),has_true);
	      f.st,f,mark,has_true,accq
		

    let check_pred l t = true (*l = [] ||
      List.exists (function p ->
		     match p with 
			 `Left f | `Right f -> f t
		       | _ -> assert false) l
			      *)
	

    let rec accepting_among2  a t r acc =
      let orig = r in
      let rest = Ptset.inter r a.final in
      let r = Ptset.diff r rest in
	if Ptset.is_empty r then rest,acc else 
	  if (not (Tree.is_node t))
	  then 
	      orig,acc
	  else 
	    let t1 = Tree.first_child t 
	    and t2 = Tree.next_sibling t in
	    let (r1,r2),formula,mark,has_true,r = get_trans t a (Tree.tag t) r
 	    in 
	    let s1,res1 = accepting_among2 a t1 r1 acc
	    in
	    let formula = eval_dir `Left formula s1 in
	      if is_false formula then rest,acc
	      else
		if is_true formula then (* tail call equivalent to a top down *)
		  accepting_among2 a t2 orig (if mark then TS.append t res1 else res1)		  
		else
		  let s2,res2 = accepting_among2 a t2 r2 res1
		  in
		  let formula = eval_dir `Right formula s2
		  in
		    if is_false formula then rest,res1
		    else
		      orig,(if mark then TS.append t (res2)
			    else res2)


    let rec accepting_among a t r =
      let orig = r in
      let rest = Ptset.inter r a.final in
      let r = Ptset.diff r rest in
	if Ptset.is_empty r then rest,TS.empty else 
	  if Tree.is_node t
	  then 
	    let (r1,r2),formula,mark,has_true,r = get_trans t a (Tree.tag t) r
 	    in 
	    let s1,res1 = accepting_among a (Tree.first_child t) r1 
	    and s2,res2 = accepting_among a (Tree.next_sibling t) r2 
	    in
	    let rb,rb1,rb2 = eval_form_bool formula s1 s2 in
	      if rb
	      then 
		let res1 = if rb1 then res1 else TS.empty
		and res2 = if rb2 then res2 else TS.empty
		in r, TS.concat res2 (if mark then TS.cons t res1 else res1)
	      else orig,TS.empty
	  else orig,TS.empty



		
    let rec accepting_count a t r =
      let orig = r in
      let rest = Ptset.inter r a.final in
      let r = Ptset.diff r rest in
	if Ptset.is_empty r then rest,0 else 
	  if Tree.is_node t
	  then 
	    let (r1,r2),formula,mark,has_true,r = get_trans t a (Tree.tag t) r
 	    in 
	    let s1,res1 = accepting_count a (Tree.first_child t) r1 
	    and s2,res2 = accepting_count a (Tree.next_sibling t) r2 
	    in
	    let rb,rb1,rb2 = eval_form_bool formula s1 s2 in
	      if rb
	      then 
		let res1 = if rb1 then res1 else 0 
		and res2 = if rb2 then res2 else 0
		in r, res1+res2+(if mark then 1 else 0)
	      else orig,0
	  else orig,0


    let run a t = 
(*      let _ = 
	call := 0; miss:=0;
	timeref := 0.0; 
	HFEval.clear hfeval;
	Hashtbl.clear dnf_hash;
	Hashtbl.clear fstate_pool; 
      in *)
      let st,res = accepting_among a t a.init  in
      let b = Ptset.is_empty (st) in
	if b then TS.empty
	else
	  res	  

    let run_count a t = 
(*      let _ = 
	call := 0; miss:=0;
	timeref := 0.0;
	timerefall := 0.0; 
	HFEval.clear hfeval;
	Hashtbl.clear dnf_hash;
	Hashtbl.clear fstate_pool; 
	in *)
      let st,res = accepting_count a t a.init  in
      let b = Ptset.is_empty (st) in
      if b then 0
      else
	res	  
  end
	
  module Jump = struct
    let eval_dir = BottomUpNew.eval_dir
    let xi1 = HTagSet.create 10
    let xi2 = HTagSet.create 10 
    

    let rec accept_from orig a t r acc =
      if (Tree.is_root t) || 
	(Ptset.subset orig r)
      then
	acc
      else
	let is_left = Tree.is_left t in
	let tag = Tree.tag t in
	let nr,f, mark = 
	  try
	    HTagSet.find (if is_left then xi1 else xi2)
	      (r,tag)
	  with
	    | Not_found ->
		let trans = 
		  Hashtbl.fold 
		    (fun q l acc ->
		       List.fold_left (fun ((racc,facc,macc) as acc) (ts,(m,f,_)) ->
					 let rl,rr = f.st in
					 if (TagSet.mem tag ts) && 
					   (Ptset.intersect (if is_left then rl else rr) r)
					 then (Ptset.add q racc,or_ f facc, macc||m)
					 else acc) acc l)
		    a.phi (Ptset.empty,false_,false)

		in
		  HTagSet.add (if is_left then xi1 else xi2) (r,tag) trans;
		  trans
	in
	let form = eval_dir (if is_left then `Left else `Right) f r
	in
	  if is_true form then accept_from orig a (Tree.parent t) nr 
	    (if mark then TS.cons t acc else acc)
	  else if is_false form then TS.empty
	  else assert false

    let run a t r = 
      HTagSet.clear xi1;
      HTagSet.clear xi2;
      let orig = 
	List.fold_left (fun s (_,(_,f,_)) ->
			  Ptset.union s (fst f.st))
	  Ptset.empty (Hashtbl.find a.phi (Ptset.choose a.init))
      in
	accept_from orig a t r TS.empty
	    

  end