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 hash (f,s,t) =
HASHINT3(Formula.uid f ,StateSet.uid s,StateSet.uid t)
end)
-(* Too slow
-module MemoForm = Memoizer.Make(
-
-module F = Formula
-(*
-let eval_form_bool =
- MemoForm.make_rec(
- fun eval (f, ((s1,s2) as sets)) ->
- match F.expr f with
- | F.True -> true,true,true
- | F.False -> false,false,false
- | F.Atom((`Left|`LLeft),b,q) ->
- if b == (StateSet.mem q s1)
- then (true,true,false)
- else false,false,false
- | F.Atom(_,b,q) ->
- if b == (StateSet.mem q s2)
- then (true,false,true)
- else false,false,false
- | F.Or(f1,f2) ->
- let b1,rl1,rr1 = eval (f1,sets)
- in
- if b1 && rl1 && rr1 then (true,true,true) else
- let b2,rl2,rr2 = eval (f2,sets) in
- let rl1,rr1 = if b1 then rl1,rr1 else false,false
- and rl2,rr2 = if b2 then rl2,rr2 else false,false
- in (b1 || b2, rl1||rl2,rr1||rr2)
-
- | F.And(f1,f2) ->
- let b1,rl1,rr1 = eval (f1,sets) in
- if b1 && rl1 && rr1 then (true,true,true) else
- if b1 then
- let b2,rl2,rr2 = eval (f2,sets) in
- if b2 then (true,rl1||rl2,rr1||rr2) else (false,false,false)
- else (false,false,false)
- )
-
-*) *)
module F = Formula
let eval_form_bool =
let string_of_ts tags = (Ptset.Int.fold (fun t a -> a ^ " " ^ (Tag.to_string t) ) tags "{")^ " }"
+
+ module Algebra =
+ struct
+ type jump = [ `LONG | `CLOSE | `NIL ]
+ type t = jump*Ptset.Int.t
+
+ let merge_jump (j1,l1) (j2,l2) =
+ match j1,j2 with
+ | _ when j1 = j2 -> (j1,Ptset.Int.union l1 l2)
+ | _,`NIL -> j1,l1
+ | `NIL,_ -> j2,l2
+ | _,_ -> (`CLOSE, Ptset.Int.union l1 l2)
+
+ let merge_jump_list = function
+ | [] -> `NIL,Ptset.Int.empty
+ | p::r -> List.fold_left (merge_jump) p r
+
+ let labels a s =
+ Hashtbl.fold
+ (
+ fun q l acc ->
+ if (q == s)
+ then
+
+ (List.fold_left
+ (fun acc (ts,f) ->
+ let _,_,_,bur = Transition.node f in
+ if bur then acc else TagSet.cup acc ts)
+ acc l)
+ else acc ) a.trans TagSet.empty
+ exception Found
+
+ let is_rec a s access =
+ List.exists
+ (fun (_,t) -> let _,_,f,_ = Transition.node t in
+ StateSet.mem s (access f)) (Hashtbl.find a.trans s)
+
+
+ let decide a c_label l_label dir_states access =
+
+ let l = StateSet.fold
+ (fun s l ->
+ let s_rec= is_rec a s access in
+ let tlabels,jmp =
+ if s_rec then l_label,`LONG
+ else c_label,`CLOSE in
+ let slabels = TagSet.positive ((TagSet.cap (labels a s) tlabels))
+ in
+ (if Ptset.Int.is_empty slabels
+ then `NIL,Ptset.Int.empty
+ else jmp,slabels)::l) dir_states []
+ in merge_jump_list l
+
+
+
+
+
+ end
+
+
+
let choose_jump tagset qtags1 qtagsn a f_nil f_t1 f_s1 f_tn f_sn f_notext f_maytext =
let tags1,hastext1,fin1 = inter_text tagset (tags a qtags1) in
let tagsn,hastextn,finn = inter_text tagset (tags a qtagsn) in
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
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 "