- let rtrue,rfalse,rmay,trs,selnodes =
- List.fold_left (fun (at,af,am,atrs,selnodes) (q,(m,f)) ->
- let ppf = Format.err_formatter in
- match (*may_eval (r1,r2) f t *) `Maybe with
- | `True ->
- (* Format.fprintf ppf "Will skip (%i) %s " q (if m then "=>" else "->");
- pr_frm ppf f;
- Format.fprintf ppf ", always true \n"; *)
- (Ptset.add q at),af,am,atrs,TS.add t selnodes
- | `False ->
- (*Format.fprintf ppf "Will skip (%i) %s " q (if m then "=>" else "->");
- pr_frm ppf f;
- Format.fprintf ppf ", always false \n"; *)
- at,(Ptset.add q af),am,atrs,selnodes
-
- | `Maybe ->
-(* Format.fprintf ppf "Must take (%i) %s " q (if m then "=>" else "->");
- pr_frm ppf f;
- Format.fprintf ppf "\n"; *)
- at,af,(Ptset.add q am),(q,(m,f))::atrs,selnodes)
- (Ptset.empty,Ptset.empty,Ptset.empty,[],TS.empty) trs
- in
- let rr1,rr2,trs =
- List.fold_left (fun ((ar1,ar2,trs)as acc) ((q,(_,f)as tr)) ->
- if Ptset.mem q rmay
- then let ls,rs = f.st in
- Ptset.union ls ar1,Ptset.union rs ar2,tr::trs
- else acc) (Ptset.empty,Ptset.empty,[]) trs
- in
- let s1,res1 = accepting_among a t1 rr1
- and s2,res2 = accepting_among a t2 rr2
- in
- let res,set,mark,trs = List.fold_left (fun ((sel_nodes,res,amark,acctr) as acc) (q,(mark,f)) ->
- let b,resnodes = eval_form f s1 s2 res1 res2 in
- (* if b then begin
- pr_st Format.err_formatter (Ptset.elements s1);
- Format.fprintf Format.err_formatter ",";
- pr_st Format.err_formatter (Ptset.elements s2);
- Format.fprintf Format.err_formatter " satisfies ";
- pr_frm Format.err_formatter f;
- Format.fprintf Format.err_formatter " for input tree %s\n" (Tag.to_string tag);
- end; *)
- if b
- then
- (TS.union
- (if mark then TS.add t resnodes else resnodes)
- sel_nodes)
- ,Ptset.add q res,amark||mark,(q,mark,f)::acctr
- else acc
- ) (TS.empty,rtrue,false,[]) trs
- in
-
- let set = Ptset.union a.final set in
- let _ = D(Hashtbl.add traces (Tree.id t) (TNode(r,set,mark,trs))) in
- set,res
-
-
- let run a t =
- let st,res = accepting_among a t a.init in
- let b = Ptset.is_empty (st) in
- let _ = D(dump_trace t) in
- if b then []
- else (TS.elements res)
-
- end
+ { hash = h;
+ sets =s;
+ results = imap }
+
+ end
+
+ let h_fold = Hashtbl.create 511
+
+ let fold_f_conf t slist fl_list conf dir=
+ let rec loop sl fl acc =
+ match SList.node sl,fl with
+ |SList.Nil,[] -> acc
+ |SList.Cons(s,sll), formlist::fll ->
+ let r',rb,rb1,rb2,mark =
+ let key = SList.hash sl,Formlist.hash formlist,dir in
+ try
+ Hashtbl.find h_fold key
+ with
+ Not_found -> let res =
+ if dir then eval_formlist s Ptset.Int.empty formlist
+ else eval_formlist Ptset.Int.empty s formlist
+ in (Hashtbl.add h_fold key res;res)
+ in
+ if rb && ((dir&&rb1)|| ((not dir) && rb2))
+ then
+ let acc =
+ let old_r =
+ try Configuration.IMap.find s conf.Configuration.results
+ with Not_found -> RS.empty
+ in
+ Configuration.add acc r' (if mark then RS.cons t old_r else old_r)
+ in
+ loop sll fll acc
+ else loop sll fll acc
+ | _ -> assert false
+ in
+ loop slist fl_list Configuration.empty
+
+ let h_trans = Hashtbl.create 4096
+
+ let get_up_trans slist ptag a tree =
+ let key = (HASHINT2(SList.uid slist,ptag)) in
+ try
+ Hashtbl.find h_trans key
+ with
+ | Not_found ->
+ let f_list =
+ Hashtbl.fold (fun q l acc ->
+ List.fold_left (fun fl_acc (ts,t) ->
+ if TagSet.mem ptag ts then Formlist.cons t fl_acc
+ else fl_acc)
+
+ acc l)
+ a.trans Formlist.nil
+ in
+ let res = SList.fold (fun _ acc -> f_list::acc) slist []
+ 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
+
+ accu,conf,next
+ else
+
+ let below_right = Tree.is_below_right tree next in
+
+ let accu,rightconf,next_of_next =
+ if below_right then (* jump to the next *)
+ bottom_up a next conf (jump_fun next) jump_fun (Tree.next_sibling tree) true init accu
+ else accu,Configuration.empty,next
+ in
+ let sub =
+ if dotd then
+ if below_right then prepare_topdown a tree true
+ else prepare_topdown a tree false
+ else conf
+ in
+ let conf,next =
+ (Configuration.merge rightconf sub, next_of_next)
+ in
+ if Tree.equal tree root then accu,conf,next
+ else
+ let parent = Tree.binary_parent tree in
+ let ptag = Tree.tag parent in
+ let dir = Tree.is_left tree in
+ let slist = Configuration.Ptss.fold (fun e a -> SList.cons e a) conf.Configuration.sets SList.nil in
+ let fl_list = get_up_trans slist ptag a parent in
+ let slist = SList.rev (slist) in
+ let newconf = fold_f_conf parent slist fl_list conf dir in
+ let accu,newconf = Configuration.IMap.fold (fun s res (ar,nc) ->
+ if Ptset.Int.intersect s init then
+ ( RS.concat res ar ,nc)
+ else (ar,Configuration.add nc s res))
+ (newconf.Configuration.results) (accu,Configuration.empty)
+ in
+
+ bottom_up a parent newconf next jump_fun root false init accu
+
+ and prepare_topdown a t noright =
+ 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.Int.add q acc
+ else acc) a.trans Ptset.Int.empty
+ in Hashtbl.add h_tdconf tag res;res
+ in
+(* let _ = pr ", among ";
+ StateSet.print fmt (Ptset.Int.elements r);
+ pr "\n%!";
+ in *)
+ let r = SList.cons r SList.nil in
+ let set,res = top_down (~noright:noright) a t r t 1 in
+ let set = match SList.node set with
+ | SList.Cons(x,_) ->x
+ | _ -> assert false
+ in
+(* pr "Result of topdown run is %!";
+ StateSet.print fmt (Ptset.Int.elements set);
+ pr ", number is %i\n%!" (RS.length res.(0)); *)
+ Configuration.add Configuration.empty set res.(0)
+
+
+
+ let run_bottom_up a t k =
+ let trlist = Hashtbl.find a.trans (Ptset.Int.choose a.init)
+ in
+ let init = List.fold_left
+ (fun acc (_,t) ->
+ let _,_,f,_ = Transition.node t in
+ let _,_,l = fst ( Formula.st f ) in
+ Ptset.Int.union acc l)
+ Ptset.Int.empty trlist
+ 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_ctx tag tree t)
+ | `CONTAINS(_) -> (Tree.first_child t,fun tree -> Tree.next_sibling_ctx 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 acc,conf,next_of_next = bottom_up a tree
+ Configuration.empty next jump_fun (Tree.root tree) true init acc
+ in
+ (* let _ = pr "End of first iteration, conf is:\n%!";
+ Configuration.pr fmt conf
+ in *)
+ let acc = Configuration.IMap.fold
+ ( fun s res acc -> if Ptset.Int.intersect init s
+ then RS.concat res acc else acc) conf.Configuration.results acc
+ in
+ if Tree.is_nil next_of_next (*|| Tree.equal next next_of_next *)then
+ acc
+ else loop next_of_next (jump_fun next_of_next) acc
+ in
+ 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 a t k = let module RI = Run(Integer) in Integer.length (RI.run_bottom_up a t k)
+
+