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