1
2
3
4 package net.sf.bddbddb;
5
6 import java.util.Collection;
7 import java.util.HashMap;
8 import java.util.HashSet;
9 import java.util.Iterator;
10 import java.util.LinkedList;
11 import java.util.Map;
12 import java.util.Set;
13 import java.io.BufferedWriter;
14 import java.io.FileWriter;
15 import java.io.IOException;
16 import java.io.LineNumberReader;
17 import java.math.BigInteger;
18 import jwutil.collections.HashWorklist;
19 import jwutil.collections.Worklist;
20 import jwutil.graphs.Graph;
21 import jwutil.strings.MyStringTokenizer;
22 import jwutil.util.Assert;
23 import net.sf.bddbddb.RelationGraph.GraphNode;
24
25 /***
26 * Dot
27 *
28 * @author cunkel
29 * @version $Id: Dot.java 522 2005-04-29 02:34:44Z joewhaley $
30 */
31 public class Dot {
32 private Solver solver;
33 private Collection
34 private Collection
35 private Worklist worklist;
36 private Collection
37 private Collection
38 private Collection
39 private String outputFileName;
40
41 Dot() {
42 edgeSources = new LinkedList();
43 nodeModifiers = new LinkedList();
44 worklist = new HashWorklist(true);
45 nodes = new LinkedList();
46 edges = new LinkedList();
47 usedRelations = new HashSet();
48 }
49
50 void outputGraph() throws IOException {
51 Iterator i = edgeSources.iterator();
52 Set allRoots = new HashSet();
53 while (i.hasNext()) {
54 allRoots.addAll(((EdgeSource) i.next()).roots());
55 }
56 i = allRoots.iterator();
57 while (i.hasNext()) {
58 worklist.push(i.next());
59 }
60 while (!worklist.isEmpty()) {
61 GraphNode n = (GraphNode) worklist.pull();
62 visitNode(n);
63 }
64 BufferedWriter dos = null;
65 try {
66 dos = new BufferedWriter(new FileWriter(solver.basedir + outputFileName));
67 dos.write("digraph {\n");
68 dos.write(" size=\"7.5,10\";\n");
69
70 dos.write(" concentrate=true;\n");
71 dos.write(" ratio=fill;\n");
72 dos.write(" rankdir=LR;");
73 dos.write("\n");
74 i = nodes.iterator();
75 while (i.hasNext()) {
76 dos.write(" ");
77 dos.write((String) i.next());
78 }
79 dos.write("\n");
80 i = edges.iterator();
81 while (i.hasNext()) {
82 dos.write(" ");
83 dos.write((String) i.next());
84 }
85 dos.write("}\n");
86 } finally {
87 if (dos != null) {
88 dos.close();
89 }
90 }
91 }
92
93 void parseInput(Solver s, LineNumberReader in) throws IOException {
94 solver = s;
95 String currentLine = in.readLine();
96 while (currentLine != null) {
97 solver.out.println("Parsing " + currentLine);
98 MyStringTokenizer st = new MyStringTokenizer(currentLine, " \t,()");
99 parseLine(st);
100 currentLine = in.readLine();
101 }
102 }
103
104 private void parseLine(MyStringTokenizer st) {
105 if (!st.hasMoreTokens()) {
106 return;
107 }
108 String s = st.nextToken();
109 if (s.startsWith("#")) {
110 return;
111 }
112 if (s.equals("edge")) {
113 String relationName = st.nextToken();
114 String roots = st.nextToken();
115 String rootsName = st.nextToken();
116 if (!roots.equals("roots")) {
117 throw new IllegalArgumentException();
118 }
119 Relation edgeRelation = solver.getRelation(relationName);
120 Relation rootsRelation = solver.getRelation(rootsName);
121 usedRelations.add(edgeRelation);
122 usedRelations.add(rootsRelation);
123 EdgeSource es = new EdgeSource(edgeRelation, rootsRelation);
124 if (st.hasMoreTokens()) {
125 String label = st.nextToken();
126 if (!label.equals("label")) {
127 throw new IllegalArgumentException();
128 }
129 relationName = st.nextToken();
130 String[] e = new String[3];
131 e[0] = st.nextToken();
132 e[1] = st.nextToken();
133 e[2] = st.nextToken();
134 int sourceIndex = -1;
135 int labelIndex = -1;
136 int sinkIndex = -1;
137 for (int i = 0; i < 3; i++) {
138 if (e[i].equals("source")) {
139 sourceIndex = i;
140 } else if (e[i].equals("sink")) {
141 sinkIndex = i;
142 } else if (e[i].equals("label")) {
143 labelIndex = i;
144 }
145 }
146 if (sourceIndex == -1) throw new IllegalArgumentException();
147 if (sinkIndex == -1) throw new IllegalArgumentException();
148 if (labelIndex == -1) throw new IllegalArgumentException();
149 Relation labelRelation = solver.getRelation(relationName);
150 usedRelations.add(labelRelation);
151 es.setLabelSource(new LabelSource(labelRelation, sourceIndex, sinkIndex, labelIndex));
152 }
153 edgeSources.add(es);
154 } else if (s.equals("domain")) {
155 String domainName = st.nextToken();
156 String attribute = st.nextToken();
157 String value = st.nextToken();
158 nodeModifiers.add(new DomainModifier(attribute, value, solver.getDomain(domainName)));
159 } else if (s.equals("default")) {
160 String attribute = st.nextToken();
161 String value = st.nextToken();
162 nodeModifiers.add(new DefaultModifier(attribute, value));
163 } else if (s.equals("relation")) {
164 String relationName = st.nextToken();
165 String attribute = st.nextToken();
166 String value = st.nextToken();
167 BDDRelation relation = (BDDRelation) solver.getRelation(relationName);
168 usedRelations.add(relation);
169 nodeModifiers.add(new InRelationModifier(attribute, value, relation));
170 } else if (s.equals("output")) {
171 outputFileName = st.nextToken();
172 } else {
173 throw new IllegalArgumentException();
174 }
175 }
176 private static class LabelSource {
177 Relation relation;
178 int sourceIndex;
179 int sinkIndex;
180 int labelIndex;
181 Domain labelDomain;
182
183 LabelSource(Relation r, int sourceI, int sinkI, int labelI) {
184 relation = r;
185 sourceIndex = sourceI;
186 sinkIndex = sinkI;
187 labelIndex = labelI;
188 Attribute a = (Attribute) relation.attributes.get(labelIndex);
189 labelDomain = a.attributeDomain;
190 }
191
192 String getLabel(RelationGraph.GraphNode source, RelationGraph.GraphNode sink) {
193 BigInteger[] restriction = new BigInteger[3];
194 restriction[0] = restriction[1] = restriction[2] = BigInteger.valueOf(-1);
195 restriction[sourceIndex] = source.number;
196 restriction[sinkIndex] = sink.number;
197 TupleIterator i = relation.iterator(restriction);
198 String label = null;
199 while (i.hasNext()) {
200 BigInteger[] labelTuple = i.nextTuple();
201 BigInteger labelNumber = labelTuple[labelIndex];
202 String l = labelDomain.toString(labelNumber);
203 if (label == null) {
204 label = l;
205 } else {
206 label = label + ", " + l;
207 }
208 }
209 return label;
210 }
211 }
212 private static class EdgeSource {
213 Relation relation;
214 Relation roots;
215 LabelSource labelSource;
216 Graph g;
217
218 EdgeSource(Relation rel, Relation rts) {
219 relation = rel;
220 roots = rts;
221 labelSource = null;
222 g = null;
223 }
224
225 public void setLabelSource(LabelSource source) {
226 labelSource = source;
227 }
228
229 public Collection roots() {
230 if (g == null) {
231 g = new RelationGraph(roots, relation);
232 }
233 return g.getRoots();
234 }
235
236 public void visitSources(Dot dot, RelationGraph.GraphNode sink, boolean addEdges) {
237 if (g == null) {
238 g = new RelationGraph(roots, relation);
239 }
240 Collection c = g.getNavigator().prev(sink);
241 Iterator i = c.iterator();
242 while (i.hasNext()) {
243 RelationGraph.GraphNode source = (RelationGraph.GraphNode) i.next();
244 dot.enqueue(source);
245 if (addEdges) {
246 String label = null;
247 if (labelSource != null) {
248 label = labelSource.getLabel(source, sink);
249 }
250 if (label != null) {
251 dot.addEdge(dot.nodeName(source) + " -> " + dot.nodeName(sink) + " [label=\"" + label + "\"];\n");
252 } else {
253 dot.addEdge(dot.nodeName(source) + " -> " + dot.nodeName(sink) + ";\n");
254 }
255 }
256 }
257 }
258
259 public void visitSinks(Dot dot, RelationGraph.GraphNode source, boolean addEdges) {
260 if (g == null) {
261 g = new RelationGraph(roots, relation);
262 }
263 Collection c = g.getNavigator().next(source);
264 Iterator i = c.iterator();
265 while (i.hasNext()) {
266 RelationGraph.GraphNode sink = (RelationGraph.GraphNode) i.next();
267 dot.enqueue(sink);
268 if (addEdges) {
269 String label = null;
270 if (labelSource != null) {
271 label = labelSource.getLabel(source, sink);
272 }
273 if (label != null) {
274 dot.addEdge(dot.nodeName(source) + " -> " + dot.nodeName(sink) + " [label=\"" + label + "\"];\n");
275 } else {
276 dot.addEdge(dot.nodeName(source) + " -> " + dot.nodeName(sink) + ";\n");
277 }
278 }
279 }
280 }
281 }
282 private static abstract class NodeAttributeModifier {
283 abstract boolean match(RelationGraph.GraphNode n, Map a);
284 }
285 private class DefaultModifier extends NodeAttributeModifier {
286 String property;
287 String value;
288
289 DefaultModifier(String p, String v) {
290 property = p;
291 value = v;
292 }
293
294 boolean match(GraphNode n, Map a) {
295 a.put(property, value);
296 return true;
297 }
298 }
299 private class DomainModifier extends NodeAttributeModifier {
300 Domain fd;
301 String property;
302 String value;
303
304 DomainModifier(String p, String v, Domain f) {
305 property = p;
306 value = v;
307 fd = f;
308 }
309
310 boolean match(GraphNode n, Map a) {
311 Domain f = n.v.getDomain();
312 if (f.equals(fd)) {
313 a.put(property, value);
314 return true;
315 } else {
316 return false;
317 }
318 }
319 }
320 private class InRelationModifier extends NodeAttributeModifier {
321 BDDRelation relation;
322 String property;
323 String value;
324
325 InRelationModifier(String p, String v, BDDRelation r) {
326 property = p;
327 value = v;
328 relation = r;
329 Assert._assert(r.attributes.size() == 1);
330 }
331
332 boolean match(GraphNode n, Map a) {
333 Attribute attr = (Attribute) relation.attributes.iterator().next();
334 Domain f = attr.attributeDomain;
335 if (n.v.getDomain().equals(f)) {
336 if (relation.contains(0, n.number)) {
337 a.put(property, value);
338 return true;
339 }
340 }
341 return false;
342 }
343 }
344
345 public void enqueue(GraphNode x) {
346 worklist.push(x);
347 }
348
349 public void addEdge(String edge) {
350 edges.add(edge);
351 }
352
353 public String nodeName(GraphNode n) {
354 return "\"" + n.toString() + "\"";
355 }
356
357 private void visitNode(GraphNode x) {
358 Map attributes = new HashMap();
359 String nodeName = (String) x.v.getDomain().map.get(x.number.intValue());
360 if (nodeName != null) {
361 attributes.put("label", nodeName);
362 }
363 Iterator i = nodeModifiers.iterator();
364 while (i.hasNext()) {
365 NodeAttributeModifier m = (NodeAttributeModifier) i.next();
366 m.match(x, attributes);
367 }
368 String node = nodeName(x) + " [";
369 i = attributes.keySet().iterator();
370 boolean firstAttribute = true;
371 while (i.hasNext()) {
372 String attribute = (String) i.next();
373 String value = (String) attributes.get(attribute);
374 if (!firstAttribute) {
375 node += ", ";
376 }
377 node += attribute + "=" + "\"" + value + "\"";
378 firstAttribute = false;
379 }
380 node += "];\n";
381 nodes.add(node);
382 i = edgeSources.iterator();
383 while (i.hasNext()) {
384 EdgeSource es = (EdgeSource) i.next();
385 es.visitSinks(this, x, true);
386
387 }
388 }
389
390 /***
391 * @return the collection of used relations
392 */
393 public Collection getUsedRelations() {
394 return usedRelations;
395 }
396 }