in loop f
-module FTable = Hashtbl.Make( struct
- type t = Tag.t*Formlist.t*StateSet.t*StateSet.t
- let equal (tg1,f1,s1,t1) (tg2,f2,s2,t2) =
- tg1 == tg2 && f1 == f2 && s1 == s2 && t1 == t2;;
- let hash (tg,f,s,t) = HASHINT4(tg,Formlist.uid f ,StateSet.uid s,StateSet.uid t);;
- end)
+module FTable = Hashtbl.Make(struct
+ type t = Tag.t*Formlist.t*StateSet.t*StateSet.t
+ let equal (tg1,f1,s1,t1) (tg2,f2,s2,t2) =
+ tg1 == tg2 && f1 == f2 && s1 == s2 && t1 == t2;;
+ let hash (tg,f,s,t) = HASHINT4(tg,Formlist.uid f ,StateSet.uid s,StateSet.uid t);;
+ end)
let h_f = FTable.create BIG_H_SIZE
val map : ( elt -> elt) -> t -> t
val length : t -> int
val merge : (bool*bool*bool*bool) -> elt -> t -> t -> t
+ val mk_quick_tag_loop : (elt -> elt -> 'a*t array) -> 'a -> int -> Tree.t -> Tag.t -> (elt -> elt -> 'a*t array)
+ val mk_quick_star_loop : (elt -> elt -> 'a*t array) -> 'a -> int -> Tree.t -> (elt -> elt -> 'a*t array)
end
module Integer : ResultSet =
if mark then 1+res1+res2
else res1+res2
else 0
+ let mk_quick_tag_loop _ sl ss tree tag = ();
+ fun t ctx ->
+ (sl, Array.make ss (Tree.subtree_tags tree tag t))
+ let mk_quick_star_loop _ sl ss tree = ();
+ fun t ctx ->
+ (sl, Array.make ss (Tree.subtree_elements tree t))
+
end
module IdSet : ResultSet =
else
{ node = (Concat(res1.node,res2.node));
length = res1.length + res2.length ;}
- else empty
-
-
+ else empty
+ let mk_quick_tag_loop f _ _ _ _ = f
+ let mk_quick_star_loop f _ _ _ = f
end
- module GResult = struct
- type t
+ module GResult(Doc : sig val doc : Tree.t end) = struct
+ type bits
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
+ external create_empty : int -> bits = "caml_result_set_create"
+ external set : bits -> int -> unit = "caml_result_set_set"
+ external next : bits -> int -> int = "caml_result_set_next"
+ external clear : bits -> elt -> elt -> unit = "caml_result_set_clear"
+
+ type t =
+ { segments : elt list;
+ bits : bits;
+ }
+
+ let ebits =
+ let size = (Tree.subtree_size Doc.doc Tree.root) in
+ create_empty (size*2+1)
+
+ let empty = { segments = [];
+ bits = ebits }
- let cons e t = set t (Obj.magic e)
- let concat _ t = t
+ let cons e t =
+ let rec loop l = match l with
+ | [] -> { bits = (set t.bits (Obj.magic e);t.bits);
+ segments = [ e ] }
+ | p::r ->
+ if Tree.is_binary_ancestor Doc.doc e p then
+ loop r
+ else
+ { bits = (set t.bits (Obj.magic e);t.bits);
+ segments = e::l }
+ in
+ loop t.segments
+
+ let concat t1 t2 =
+ if t2.segments == [] then t1
+ else
+ if t1.segments == [] then t2
+ else
+ let h2 = List.hd t2.segments in
+ let rec loop l = match l with
+ | [] -> t2.segments
+ | p::r ->
+ if Tree.is_binary_ancestor Doc.doc p h2 then
+ l
+ else
+ p::(loop r)
+ in
+ { bits = t1.bits;
+ segments = loop t1.segments
+ }
+
let iter f t =
let rec loop i =
if i == -1 then ()
- else (f (Obj.magic i);loop (next t i))
- in loop 0
+ else (f ((Obj.magic i):elt);loop (next t.bits i))
+ in loop (next t.bits 0)
let fold _ _ _ = failwith "noop"
let map _ _ = failwith "noop"
- let length t = let cpt = ref ~-1 in
+ let length t = let cpt = ref 0 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
-
+ if rb then
+(* let _ = Printf.eprintf "Lenght before merging is %i %i\n"
+ (List.length t1.segments) (List.length t2.segments)
+ in *)
+ match t1.segments,t2.segments with
+ [],[] -> if mark then cons elt empty else empty
+ | [p],[] when rb1 -> if mark then cons elt t1 else t1
+ | [], [p] when rb2 -> if mark then cons elt t2 else t2
+ | [x],[y] when rb1 && rb2 -> if mark then cons elt empty else
+ concat t1 t2
+ | _,_ ->
+ let t1 = if rb1 then t1 else
+ (List.iter (fun idx -> clear t1.bits idx (Tree.closing Doc.doc idx)) t1.segments;empty)
+ and t2 = if rb2 then t2 else
+ (List.iter (fun idx -> clear t2.bits idx (Tree.closing Doc.doc idx)) t2.segments;empty)
+ in
+ (if mark then cons elt (concat t1 t2)
+ else concat t1 t2)
+ else
+ let _ =
+ List.iter (fun idx -> clear t1.bits idx (Tree.closing Doc.doc idx)) t1.segments;
+ List.iter (fun idx -> clear t2.bits idx (Tree.closing Doc.doc idx)) t2.segments
+ in
+ empty
+ let mk_quick_tag_loop f _ _ _ _ = f
+ let mk_quick_star_loop f _ _ _ = f
end
module Run (RS : ResultSet) =
struct
(fun (_,t) -> let _,_,_,f,_ = Transition.node t in
StateSet.mem s ((fun (_,_,x) -> x) (access (Formula.st f)))) (Hashtbl.find a.trans s)
-
+ let is_final_marking a s =
+ List.exists (fun (_,t) -> let _,_,m,f,_ = Transition.node t in m&& (Formula.is_true f))
+ (Hashtbl.find a.trans s)
+
+
let decide a c_label l_label dir_states dir =
let l = StateSet.fold
| _,`NIL -> (
match f_kind with
|`TAG(tag') ->
- (fun t _ -> eval_fold2_slist fl_list t (Tree.tag tree t) empty_res
- (loop_tag tag' (first t) llist t ))
- | `ANY ->
+ let default = fun t _ -> eval_fold2_slist fl_list t (Tree.tag tree t) empty_res
+ (loop_tag tag' (first t) llist t )
+ in
+ let cf = SList.hd llist in
+ if (slot_size == 1) && StateSet.is_singleton cf
+ then
+ let s = StateSet.choose cf in
+ if (Algebra.is_rec a s fst) && (Algebra.is_rec a s snd)
+ && (Algebra.is_final_marking a s)
+ then RS.mk_quick_subtree default llist 1 tree tag'
+ else default
+ else default
+ | _ ->
(fun t _ -> eval_fold2_slist fl_list t (Tree.tag tree t) empty_res
(loop (first t) llist t ))
- | _ -> assert false)
+ )
| `NIL,_ -> (
match n_kind with
|`TAG(tag') ->
(fun t ctx -> eval_fold2_slist fl_list t (Tree.tag tree t)
(loop_tag tag' (next t ctx) rlist ctx ) empty_res)
- | `ANY ->
+ | _ ->
(fun t ctx -> eval_fold2_slist fl_list t (Tree.tag tree t)
(loop (next t ctx) rlist ctx ) empty_res)
-
- | _ -> assert false)
+ )
| `TAG(tag1),`TAG(tag2) ->
(fun t ctx ->
eval_fold2_slist fl_list t (Tree.tag tree t)
(loop (next t ctx) rlist ctx )
(loop (first t) llist t ))
- | _ -> assert false
+
in
let cont = D_IF_( (fun t ctx ->
let a,b = cont t ctx in
let bottom_up_count a t k = let module RI = Run(Integer) in Integer.length (RI.run_bottom_up a t k)
+ module Test (Doc : sig val doc : Tree.t end) =
+ struct
+ module Results = GResult(Doc)
+ let top_down a t = let module R = Run(Results) in (R.run_top_down a t)
+ end
+