+ let pr fmt c = Format.fprintf fmt "{";
+ Ptss.iter (fun s -> StateSet.print fmt s;
+ Format.fprintf fmt " ") c.sets;
+ Format.fprintf fmt "}\n%!";
+ IMap.iter (fun k d ->
+ StateSet.print fmt k;
+ Format.fprintf fmt "-> %i\n" (RS.length d)) c.results;
+ Format.fprintf fmt "\n%!"
+
+ let merge c1 c2 =
+ let acc1 = IMap.fold (fun s r acc ->
+ IMap.add s
+ (try
+ RS.concat r (IMap.find s acc)
+ with
+ | Not_found -> r) acc) c1.results IMap.empty
+ in
+ let imap =
+ IMap.fold (fun s r acc ->
+ IMap.add s
+ (try
+ RS.concat r (IMap.find s acc)
+ with
+ | Not_found -> r) acc) c2.results acc1
+ in
+ let h,s =
+ Ptss.fold
+ (fun s (ah,ass) -> (HASHINT2(ah,Ptset.Int.hash s),
+ Ptss.add s ass))
+ (Ptss.union c1.sets c2.sets) (0,Ptss.empty)
+ in
+ { 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 sl,fl with
+ |Nil,[] -> acc
+ | Cons(s,hs,sll), formlist::fll ->
+ let r',rb,rb1,rb2,mark =
+ try
+ Hashtbl.find h_fold (hs,Formlist.hash formlist,dir)
+ with
+ Not_found -> let res =
+ if dir then eval_formlist ~memo:false s Ptset.Int.empty formlist
+ else eval_formlist ~memo:false Ptset.Int.empty s formlist
+ in (Hashtbl.add h_fold (hs,Formlist.hash formlist,dir) res;res)
+ in(*
+ let _ = pr "Evaluating on set (%s) with tree %s=%s"
+ (if dir then "left" else "right")
+ (Tag.to_string (Tree.tag t))
+ (Tree.dump_node t) ;
+ StateSet.print fmt (Ptset.Int.elements s);
+ pr ", formualae (with hash %i): \n" (Formlist.hash formlist);
+ Formlist.pr fmt formlist;
+ pr "result is ";
+ StateSet.print fmt (Ptset.Int.elements r');
+ pr " %b %b %b %b \n%!" rb rb1 rb2 mark ;
+ 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(hpl slist,Tag.hash 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.add t fl_acc
+ else fl_acc)
+
+ acc l)
+ a.trans Formlist.empty
+ in
+ let res = fold_pl (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
+(* 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 _ =
+ pr "Going bottom up for tree with tag %s configuration is"
+ (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 =
+ if below_right then (* jump to the next *)
+(* 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 = %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 left subtree\n%!" in *)
+ prepare_topdown a tree true
+ else
+(* let _ = pr "Topdown on whole tree\n%!" in *)
+ 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
+(* let _ = pr "Stopping at root, configuration after topdown is:" ;
+ Configuration.pr fmt conf;
+ pr "\n%!"
+ in *) 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 -> 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 : %s " (Tree.dump_node tree);
+ Configuration.pr fmt conf;
+ pr "\n"
+ in *)
+ let newconf = fold_f_conf parent slist fl_list conf dir in
+(* let _ = pr "New conf before pruning is (dir=%b):" dir;
+ Configuration.pr fmt newconf ;
+ pr "accu is %i\n" (RS.length accu);
+ 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
+(* let _ = pr "New conf after pruning is (dir=%b):" dir;
+ Configuration.pr fmt newconf ;
+ pr "accu is %i\n" (RS.length accu);
+ 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 = 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
+ | _ -> 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_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 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