INCLUDE "debug.ml"
INCLUDE "utils.ml"
+INCLUDE "trace.ml"
open Format
| [ (_, (l, r, _) ) ] when l == StateSet.empty -> JUMP_ONE(rel_labels)
| _ ->
- if Ptset.Int.mem Tag.pcdata rel_labels then
- let () =
- D_TRACE_(Format.eprintf ">>> Computed rel_labels: %a\n%!"
- TagSet.print (TagSet.inj_positive rel_labels))
- in NODE
- else STAR
+ if Ptset.Int.mem Tag.pcdata rel_labels then begin
+ TRACE("top-down-approx", 3, __ "Computed rel_labels: %a\n"
+ TagSet.print
+ (TagSet.inj_positive rel_labels));
+ NODE
+ end else STAR
module Cache = Hashtbl.Make(StateSet)
let cache = Cache.create 1023
merge_trans by_states merge_labels
(List.sort by_states uniq_states_trs)
in
- D_TRACE_(
- let is_pairwise_disjoint l =
- List.for_all (fun ((ts, _) as tr) ->
- List.for_all (fun ((ts', _) as tr') ->
- (ts == ts' && (by_states tr tr' == 0)) ||
- TagSet.is_empty (TagSet.cap ts ts')) l) l
- in
- let is_complete l = TagSet.positive
- (List.fold_left (fun acc (ts, _) -> TagSet.cup acc ts)
- TagSet.empty l)
- ==
- (Tree.node_tags tree)
- in
- eprintf "Top-down approximation (%b, %b):\n%!"
- (is_pairwise_disjoint td_approx)
- (is_complete td_approx);
- List.iter (fun (ts,(l,r, m)) ->
- let ts = if TagSet.cardinal ts >10
- then TagSet.diff TagSet.any
- (TagSet.diff
- (TagSet.inj_positive (Tree.node_tags tree))
- ts)
- else ts
- in
- eprintf "%a, %a, %b -> %a, %a\n%!"
- StateSet.print states
- TagSet.print ts
- m
- StateSet.print l
- StateSet.print r
- ) td_approx;
- eprintf "\n%!"
-
+ TRACE(
+ "top-down-approx", 2,
+ let is_pairwise_disjoint l =
+ List.for_all (fun ((ts, _) as tr) ->
+ List.for_all (fun ((ts', _) as tr') ->
+ (ts == ts' && (by_states tr tr' == 0)) ||
+ TagSet.is_empty (TagSet.cap ts ts')) l) l
+ in
+ let is_complete l = TagSet.positive
+ (List.fold_left (fun acc (ts, _) -> TagSet.cup acc ts)
+ TagSet.empty l)
+ ==
+ (Tree.node_tags tree)
+ in
+ let pr_td_approx fmt td_approx =
+ List.iter (fun (ts,(l,r, m)) ->
+ let ts = if TagSet.cardinal ts >10
+ then TagSet.diff TagSet.any
+ (TagSet.diff
+ (TagSet.inj_positive (Tree.node_tags tree))
+ ts)
+ else ts
+ in
+ fprintf fmt "\t%a, %a, %b -> %a, %a\n%!"
+ StateSet.print states
+ TagSet.print ts
+ m
+ StateSet.print l
+ StateSet.print r
+ ) td_approx;
+ fprintf fmt "\n%!"
+ in
+ __ " pairwise-disjoint:%b, complete:%b:\n%a"
+ (is_pairwise_disjoint td_approx)
+ (is_complete td_approx)
+ pr_td_approx td_approx
);
let jump =
compute_jump
(List.exists (fun (_,(_,_,b)) -> b) td_approx)
in
Cache.add cache states jump; jump
-