1
2(*****************************************************************************)
3(* PrintBdd.sml                                                              *)
4(* ------------                                                              *)
5(*                                                                           *)
6(* Some BDD utilities for printing using dot                                 *)
7(*  http://www.research.att.com/sw/tools/graphviz/                           *)
8(*                                                                           *)
9(*****************************************************************************)
10(*                                                                           *)
11(* Revision history:                                                         *)
12(*                                                                           *)
13(*   Tue Oct  9 08:53:21 BST 2001 -- created file                            *)
14(*   Thu Nov  1 21:04:27 GMT 2001 -- updated for judgement assumptions       *)
15(*   Thu Mar 28 09:40:05 GMT 2002 -- added signature file                    *)
16(*                                                                           *)
17(*****************************************************************************)
18
19structure PrintBdd :> PrintBdd = struct
20
21(*
22load "muddyLib";
23load "PrimitiveBddRules";
24
25val _ = if not(bdd.isRunning()) then bdd.init 1000000 10000 else ();
26*)
27
28local
29
30open bdd;
31open Varmap;
32open PrimitiveBddRules;
33
34open Globals HolKernel Parse boolLib bdd;
35infixr 3 -->;
36infix ## |-> THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL;
37
38in
39
40(*****************************************************************************)
41(* Print a BDD to <file>.dot and convert it to <file>.ps; return the bdd     *)
42(*****************************************************************************)
43
44fun dotBdd file label bdd =
45 let val glab  = ("label=\""^label^"\"");
46     val gsize = "size=\"7.5,8\""
47 in
48 (bdd.fnprintdot (file^".dot") bdd;
49  Process.system("dot -G"^glab^" -G"^gsize^" -Tps "^file^".dot -o "^file^".ps");
50  bdd)
51 end;
52
53(*****************************************************************************)
54(* Print a term_bdd using a supplied label into <file>.dot;                  *)
55(* make a sed script to replace node numbers with variable names;            *)
56(* execute the sed script to create edited_<file>.dot;                       *)
57(* run:                                                                      *)
58(*  dot -Glabel="label" -Gsize="7.5,10" -Tps edited_<file>.dot -o <file>.ps  *)
59(* delete dot, sed edits and and edited dot files                            *)
60(* return the bdd and the variable name-to-number mapping                    *)
61(*****************************************************************************)
62
63
64(*****************************************************************************)
65(* Create a sed script for editing a dot file so that BBD nodes              *)
66(* are labelled with variable names rather than numbers                      *)
67(*****************************************************************************)
68
69local
70
71fun varmap_to_sed_script file varmap_pairs =
72 let val out = BasicIO.open_out file
73 in
74 (List.map
75  (fn (s,n) =>
76    BasicIO.output
77     (out,
78      "s/\\\""^(makestring n)^"\\\"/\\\""^s^"\\\"/g\n"
79     ))
80  varmap_pairs;
81 BasicIO.close_out out)
82 end
83
84in
85
86fun dotLabelledTermBdd file label tb =
87 let val (_,ass,vm,tm,bdd) = dest_term_bdd tb;
88     val pairs           = Binarymap.listItems vm;
89     val glab            = ("label=\""^label^"\"");
90     val gsize           = "size=\"7.5,8\""
91     val _               = if not(HOLset.isEmpty ass)
92                            then print "printing a term_bdd with assumptions"
93                            else ()
94 in
95 (bdd.fnprintdot (file^".dot") bdd;
96  varmap_to_sed_script(file^"_sed_edits")pairs;
97  Process.system("sed -f "^file^"_sed_edits "^file^".dot > edited_"^file^".dot");
98  Process.system("dot -G"^glab^" -G"^gsize^" -Tps edited_"^file^".dot -o "^file^".ps");
99  Process.system("rm "^file^".dot");
100  Process.system("rm "^file^"_sed_edits");
101  Process.system("rm edited_"^file^".dot");
102  ())
103 end
104
105end;
106
107(*****************************************************************************)
108(* Print dot-drawn BDD to scratchBdd.ps, with the term as label if           *)
109(* !dotTermBddFlag is true and an empty label if it's false.                 *)
110(*****************************************************************************)
111
112val dotTermBddFlag = ref true;
113
114(* Old version -- gets printing of "/\" and "\/" wrong
115fun dotTermBdd tb =
116 (print "writing scratchBdd.ps\n";
117  dotLabelledTermBdd
118   "scratchBdd"
119   (if !dotTermBddFlag then Parse.term_to_string(getTerm tb) else "")
120   tb);
121*)
122
123fun dotTermBdd tb =
124 let val _ = add_rule {term_name = "/\\",
125                       fixity = Infixr  400,
126                       pp_elements = [HardSpace 1, TOK "AND", BreakSpace(1,0)],
127                       paren_style = OnlyIfNecessary,
128                       block_style = (AroundSameName, (PP.INCONSISTENT, 0))}
129     val _ = add_rule {term_name = "\\/",
130                       fixity = Infixr  300,
131                       pp_elements = [HardSpace 1, TOK "OR", BreakSpace(1,0)],
132                       paren_style = OnlyIfNecessary,
133                       block_style = (AroundSameName, (PP.INCONSISTENT, 0))}
134     val _ = print "writing scratchBdd.ps\n";
135     val _ = dotLabelledTermBdd
136              "scratchBdd"
137              (if !dotTermBddFlag then Parse.term_to_string(getTerm tb) else "")
138              tb
139     val _ = remove_termtok {term_name = "/\\", tok = "AND"}
140     val _ = prefer_form_with_tok {term_name = "/\\", tok = "/\\"}
141     val _ = remove_termtok {term_name = "\\/", tok = "OR"}
142     val _ = prefer_form_with_tok {term_name = "\\/", tok = "\\/"}
143 in
144 ()
145 end;
146
147end
148end
149