- let rtrue,rfalse,rmay,trs,selnodes =
- List.fold_left (fun (at,af,am,atrs,selnodes) (q,(m,f)) ->
- let ppf = Format.err_formatter in
- match (*may_eval (r1,r2) f t *) `Maybe with
- | `True ->
- (* Format.fprintf ppf "Will skip (%i) %s " q (if m then "=>" else "->");
- pr_frm ppf f;
- Format.fprintf ppf ", always true \n"; *)
- (Ptset.add q at),af,am,atrs,TS.add t selnodes
- | `False ->
- (*Format.fprintf ppf "Will skip (%i) %s " q (if m then "=>" else "->");
- pr_frm ppf f;
- Format.fprintf ppf ", always false \n"; *)
- at,(Ptset.add q af),am,atrs,selnodes
-
- | `Maybe ->
-(* Format.fprintf ppf "Must take (%i) %s " q (if m then "=>" else "->");
- pr_frm ppf f;
- Format.fprintf ppf "\n"; *)
- at,af,(Ptset.add q am),(q,(m,f))::atrs,selnodes)
- (Ptset.empty,Ptset.empty,Ptset.empty,[],TS.empty) trs
- in
- let rr1,rr2,trs =
- List.fold_left (fun ((ar1,ar2,trs)as acc) ((q,(_,f)as tr)) ->
- if Ptset.mem q rmay
- then let ls,rs = f.st in
- Ptset.union ls ar1,Ptset.union rs ar2,tr::trs
- else acc) (Ptset.empty,Ptset.empty,[]) trs
- in
- let s1,res1 = accepting_among a t1 rr1
- and s2,res2 = accepting_among a t2 rr2
- in
- let res,set,mark,trs = List.fold_left (fun ((sel_nodes,res,amark,acctr) as acc) (q,(mark,f)) ->
- let b,resnodes = eval_form f s1 s2 res1 res2 in
- (* if b then begin
- pr_st Format.err_formatter (Ptset.elements s1);
- Format.fprintf Format.err_formatter ",";
- pr_st Format.err_formatter (Ptset.elements s2);
- Format.fprintf Format.err_formatter " satisfies ";
- pr_frm Format.err_formatter f;
- Format.fprintf Format.err_formatter " for input tree %s\n" (Tag.to_string tag);
- end; *)
- if b
- then
- (TS.union
- (if mark then TS.add t resnodes else resnodes)
- sel_nodes)
- ,Ptset.add q res,amark||mark,(q,mark,f)::acctr
- else acc
- ) (TS.empty,rtrue,false,[]) trs
- in
-
- let set = Ptset.union a.final set in
- let _ = D(Hashtbl.add traces (Tree.id t) (TNode(r,set,mark,trs))) in
- set,res