let psize = (size f1) + (size f2) in
let nsize = (size (not_ f1)) + (size (not_ f2)) in
let sp,sn = merge_states f1 f2 in
- fst (cons (Or(f1,f2)) (And(not_ f1,not_ f2)) sp sn psize nsize)
+ fst (cons (Or(f1,f2)) (And(not_ f1,not_ f2)) sp sn psize nsize)
let and_ f1 f2 =
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 "*\\{"
- )^ "}"
+ if TagSet.is_empty cts then "*" else
+ (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) cts "*\\{"
+ )^ "}"
in
let s = Printf.sprintf "(%s,%i)" s q in
let s_frm =
let merge (rb,rb1,rb2,mark) t res1 res2 =
if rb then
let res1 = if rb1 then res1 else empty
- and res2 = if rb2 then res2 else empty
+ and res2 = if rb2 then res2 else empty
in
if mark then { node = Cons(t,(Concat(res1.node,res2.node)));
length = res1.length + res2.length + 1;}
end
-
+ module GResult = struct
+ type t
+ type elt = [` Tree] Tree.node
+ external create_empty : int -> t = "caml_result_set_create"
+ external set : t -> int -> t = "caml_result_set_set"
+ external next : t -> int -> int = "caml_result_set_next"
+ external clear : t -> int -> int -> unit = "caml_result_set_clear"
+ let empty = create_empty 100000000
+
+ let cons e t = set t (Obj.magic e)
+ let concat _ t = t
+ let iter f t =
+ let rec loop i =
+ if i == -1 then ()
+ else (f (Obj.magic i);loop (next t i))
+ in loop 0
+
+ let fold _ _ _ = failwith "noop"
+ let map _ _ = failwith "noop"
+ let length t = let cpt = ref ~-1 in
+ iter (fun _ -> incr cpt) t; !cpt
+
+ let merge (rb,rb1,rb2,mark) elt t1 t2 =
+ if mark then (set t1 (Obj.magic elt) ; t1) else t1
+
+ end
module Run (RS : ResultSet) =
struct
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
+ 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
+ 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
|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)
+ 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
- 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
+ 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
in
(Hashtbl.add h_trans key res;res)
+
let h_tdconf = Hashtbl.create 511
let rec bottom_up a tree t conf next jump_fun root dotd init accu =
if (not dotd) && (Configuration.is_empty conf ) then
-
- accu,conf,next
+ accu,conf,next
else
- let below_right = Tree.is_below_right tree t next in
-
- let accu,rightconf,next_of_next =
- if below_right then (* jump to the next *)
- bottom_up a tree next conf (jump_fun next) jump_fun (Tree.next_sibling tree t) true init accu
- else accu,Configuration.empty,next
- in
+ let below_right = Tree.is_below_right tree t next in
+
+ let accu,rightconf,next_of_next =
+ if below_right then (* jump to the next *)
+ bottom_up a tree next conf (jump_fun next) jump_fun (Tree.next_sibling tree t) true init accu
+ else accu,Configuration.empty,next
+ in
let sub =
if dotd then
- if below_right then prepare_topdown a tree t true
- else prepare_topdown a tree t false
+ if below_right then prepare_topdown a tree t true
+ else prepare_topdown a tree t false
else conf
in
let conf,next =
(Configuration.merge rightconf sub, next_of_next)
in
- if t == root then accu,conf,next
- else
+ if t == root then accu,conf,next else
let parent = Tree.binary_parent tree t in
let ptag = Tree.tag tree parent in
let dir = Tree.is_left tree t in
in
bottom_up a tree parent newconf next jump_fun root false init accu
-
+
and prepare_topdown a tree t noright =
let tag = Tree.tag tree 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
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)
+ in
+ Configuration.add Configuration.empty set res.(0)
let run_bottom_up a tree k =
let t = Tree.root in
- let trlist = Hashtbl.find a.trans (Ptset.Int.choose a.init)
+ let trlist = Hashtbl.find a.trans (StateSet.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
+ StateSet.union acc l)
+ StateSet.empty trlist
in
let tree1,jump_fun =
match k with
(*Tree.tagged_lowest t tag, fun tree -> Tree.tagged_next tree tag*)
(Tree.tagged_desc tree tag t, let jump = Tree.tagged_foll_ctx tree tag
in fun n -> jump n t )
- | `CONTAINS(_) -> (Tree.first_child tree t,let jump = Tree.next_sibling_ctx tree
+ | `CONTAINS(_) -> (Tree.text_below tree t,let jump = Tree.text_next tree
in fun n -> jump n t)
| _ -> assert false
in
let tree2 = jump_fun tree1 in
let rec loop t 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 t
Configuration.empty next jump_fun (Tree.root) 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
+ ( fun s res acc -> if StateSet.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
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 top_down a t = let module RI = Run(GResult) 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)