INCLUDE "debug.ml"
module Tree = Tree.Binary
+
let gen_id =
let id = ref (-1) in
fun () -> incr id;!id
| 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 } =
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
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
| False -> false,false,false
| _ ->
try
- HFEval.find hfeval (f.fid,s1,s2)
+ HFEval.find hfeval (f.fid,s1,s2)
with
| Not_found -> let r =
match f.pos with
else (accf,accm,acchtrue)
) acc (Hashtbl.find a.phi q)
- let miss = ref 0
- let call = ref 0
- let get_trans t a tag r =
+
+ 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,predl
+ in f.st,f,mark,has_true,r
with
- Not_found ->
+ Not_found ->
let f,mark,has_true,accq =
Ptset.fold (fun q (accf,accm,acchtrue,accq) ->
let naccf,naccm,nacctrue =
r (false_,false,false,Ptset.empty)
in
HTagSet.add a.sigma (accq,tag) (mark,f,([],[]),has_true);
- f.st,f,mark,has_true,accq,([],[])
+ f.st,f,mark,has_true,accq
let check_pred l t = true (*l = [] ||
*)
- let rec accepting_among2 a t r acc =
+ 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
then
orig,acc
else
- let tag = Tree.tag t in
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 tag r
+ 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
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 st,res = accepting_among2 a t a.init TS.empty in
+(* 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