-IFDEF DEBUG
-THEN
- type trace =
- | TNil of Ptset.t*Ptset.t
- | TNode of Ptset.t*Ptset.t*bool* (int*bool*formula) list
-
- let traces = Hashtbl.create 17
- let dump_trace t =
- let out = open_out "debug_trace.dot"
- in
- let outf = Format.formatter_of_out_channel out in
-
- let rec aux t num =
- if Tree.is_node t
- then
- match (try Hashtbl.find traces (Tree.id t) with Not_found -> TNil(Ptset.empty,Ptset.empty)) with
- | TNode(r,s,mark,trs) ->
- let numl = aux (Tree.left t) num in
- let numr = aux (Tree.right t) (numl+1) in
- let mynum = numr + 1 in
- Format.fprintf outf "n%i [ label=\"<%s>\\nr=" mynum (Tag.to_string (Tree.tag t));
- pr_st outf (Ptset.elements r);
- Format.fprintf outf "\\ns=";
- pr_st outf (Ptset.elements s);
- List.iter (fun (q,m,f) ->
- Format.fprintf outf "\\n%i %s" q (if m then "⇨" else "→");
- pr_frm outf f ) trs;
- Format.fprintf outf "\", %s shape=box ];\n"
- (if mark then "color=cyan1, style=filled," else "");
- let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numl in
- let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numr in
- mynum
- | TNil(r,s) -> Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num;
- pr_st outf (Ptset.elements r);
- Format.fprintf outf "\\ns=";
- pr_st outf (Ptset.elements s);
- Format.fprintf outf "\"];\n";num
- else
- match Hashtbl.find traces (-10) with
- | TNil(r,s) ->
- Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num;
- pr_st outf (Ptset.elements r);
- Format.fprintf outf "\\ns=";
- pr_st outf (Ptset.elements s);
- Format.fprintf outf "\"];\n";
- num
- | _ -> assert false
-
- in
- Format.fprintf outf "digraph G {\n";
- ignore(aux t 0);
- Format.fprintf outf "}\n%!";
- close_out out;
- ignore(Sys.command "dot -Tsvg debug_trace.dot > debug_trace.svg")
-END
-
-
-
- module HFEval = Hashtbl.Make(
- struct
- type t = int*Ptset.t*Ptset.t
- let equal (a,b,c) (d,e,f) =
- a==d && (Ptset.equal b e) && (Ptset.equal c f)
- let hash (a,b,c) =
- a+17*(Ptset.hash b) + 31*(Ptset.hash c)
- end)
-
- 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
-
-*)
-