1
2
3
4 package net.sf.bddbddb.ir;
5
6 import java.util.Collection;
7 import java.util.HashMap;
8 import java.util.Iterator;
9 import java.util.LinkedList;
10 import java.util.List;
11 import java.util.ListIterator;
12 import java.util.Map;
13 import java.util.StringTokenizer;
14 import java.io.BufferedReader;
15 import java.io.BufferedWriter;
16 import java.io.FileReader;
17 import java.io.IOException;
18 import jwutil.collections.GenericMultiMap;
19 import jwutil.collections.MultiMap;
20 import jwutil.collections.Pair;
21 import jwutil.io.SystemProperties;
22 import jwutil.util.Assert;
23 import net.sf.bddbddb.Attribute;
24 import net.sf.bddbddb.BDDRelation;
25 import net.sf.bddbddb.BDDSolver;
26 import net.sf.bddbddb.Domain;
27 import net.sf.bddbddb.IterationList;
28 import net.sf.bddbddb.Relation;
29 import net.sf.bddbddb.Solver;
30 import net.sf.bddbddb.dataflow.PartialOrder.Constraint;
31 import net.sf.bddbddb.dataflow.PartialOrder.Constraints;
32 import net.sf.bddbddb.ir.dynamic.If;
33 import net.sf.bddbddb.ir.dynamic.Nop;
34 import net.sf.bddbddb.ir.highlevel.BooleanOperation;
35 import net.sf.bddbddb.ir.highlevel.Copy;
36 import net.sf.bddbddb.ir.highlevel.Difference;
37 import net.sf.bddbddb.ir.highlevel.Free;
38 import net.sf.bddbddb.ir.highlevel.GenConstant;
39 import net.sf.bddbddb.ir.highlevel.Invert;
40 import net.sf.bddbddb.ir.highlevel.Join;
41 import net.sf.bddbddb.ir.highlevel.JoinConstant;
42 import net.sf.bddbddb.ir.highlevel.Load;
43 import net.sf.bddbddb.ir.highlevel.Project;
44 import net.sf.bddbddb.ir.highlevel.Rename;
45 import net.sf.bddbddb.ir.highlevel.Save;
46 import net.sf.bddbddb.ir.highlevel.Union;
47 import net.sf.bddbddb.ir.highlevel.Universe;
48 import net.sf.bddbddb.ir.highlevel.Zero;
49 import net.sf.bddbddb.ir.lowlevel.ApplyEx;
50 import net.sf.bddbddb.ir.lowlevel.BDDProject;
51 import net.sf.bddbddb.ir.lowlevel.Replace;
52 import net.sf.javabdd.BDDDomain;
53
54 /***
55 * DomainAssignment
56 *
57 * @author John Whaley
58 * @version $Id: DomainAssignment.java 522 2005-04-29 02:34:44Z joewhaley $
59 */
60 public abstract class DomainAssignment implements OperationVisitor {
61 int SIZE = 16;
62 Solver solver;
63 MultiMap
64 List inserted;
65 static boolean TRACE = false;
66 ListIterator currentBlock;
67 Map
68
69 public abstract void doAssignment();
70
71 private void addConstraints(List loops, int loopDepth, IterationList list) {
72 if (TRACE) solver.out.println("Entering: " + list);
73 List s;
74 if (loopDepth >= loops.size()) {
75 loops.add(s = new LinkedList());
76 } else {
77 s = (List) loops.get(loopDepth);
78 }
79 s.add(list);
80 for (Iterator i = list.iterator(); i.hasNext();) {
81 Object o = i.next();
82 if (o instanceof IterationList) {
83 IterationList that = (IterationList) o;
84 addConstraints(loops, loopDepth + (that.isLoop() ? 1 : 0), that);
85 }
86 }
87 }
88
89 public void addConstraints(IterationList list) {
90
91 List loops = new LinkedList();
92 addConstraints(loops, 0, list);
93 while (!loops.isEmpty()) {
94 int index = loops.size() - 1;
95 List s = (List) loops.remove(index);
96 if (TRACE) solver.out.println("Doing loop depth " + index);
97 for (Iterator j = s.iterator(); j.hasNext();) {
98 list = (IterationList) j.next();
99 if (TRACE) solver.out.println("Doing " + list);
100
101 for (ListIterator i = list.iterator(); i.hasNext();) {
102 Object o = i.next();
103 if (o instanceof ApplyEx) {
104 Operation op = (Operation) o;
105 currentBlock = i;
106 op.visit(this);
107 }
108 }
109
110 for (ListIterator i = list.iterator(); i.hasNext();) {
111 Object o = i.next();
112 if (o instanceof Operation) {
113 if (o instanceof ApplyEx) continue;
114 Operation op = (Operation) o;
115 currentBlock = i;
116 op.visit(this);
117 }
118 }
119 }
120 }
121 }
122
123 /***
124 *
125 */
126 public DomainAssignment(Solver s) {
127 this.solver = s;
128 domainToAttributes = new GenericMultiMap();
129 this.inserted = new LinkedList();
130 int totalNumber = 0;
131 for (int i = 0; i < s.getNumberOfRelations(); ++i) {
132 Relation r = s.getRelation(i);
133 totalNumber += r.getAttributes().size();
134 }
135 for (int i = 0; i < s.getNumberOfRelations(); ++i) {
136 Relation r = s.getRelation(i);
137 int numAttribs = r.getAttributes().size();
138 for (int j = 0; j < numAttribs; ++j) {
139 Attribute a = r.getAttribute(j);
140 domainToAttributes.add(a.getDomain(), a);
141 }
142 }
143 constraintMap = new HashMap();
144 }
145
146 /***
147 *
148 */
149 public DomainAssignment(Solver s, Constraints[] constraints) {
150 this(s);
151 for (int i = 0; i < constraints.length; i++) {
152 constraintMap.put(s.getRelation(i), constraints[i]);
153 }
154 }
155
156 void initialize() {
157 BDDSolver s = (BDDSolver) solver;
158
159
160 for (int i = 0; i < solver.getNumberOfRelations(); ++i) {
161 Relation r = solver.getRelation(i);
162 forceDifferent(r);
163 }
164
165
166 for (Iterator i = s.getComparisonRelations().iterator(); i.hasNext();) {
167 BDDRelation r = (BDDRelation) i.next();
168 forceEqual(new Pair(r, r.getAttribute(0)), r.getBDDDomain(0));
169 forceEqual(new Pair(r, r.getAttribute(1)), r.getBDDDomain(1));
170 if (r.getNegated() != null) {
171 forceEqual(new Pair(r.getNegated(), r.getAttribute(0)), r.getBDDDomain(0));
172 forceEqual(new Pair(r.getNegated(), r.getAttribute(1)), r.getBDDDomain(1));
173 }
174 }
175
176 String domainFile = SystemProperties.getProperty("domainfile", "domainfile");
177 BufferedReader in = null;
178 try {
179 in = new BufferedReader(new FileReader(domainFile));
180 loadDomainAssignment(in);
181 } catch (IOException x) {
182 } finally {
183 if (in != null) try {
184 in.close();
185 } catch (IOException _) {
186 }
187 }
188 }
189
190 abstract void forceDifferent(Relation r);
191
192 abstract boolean forceEqual(Object o1, Object o2);
193
194 abstract boolean forceNotEqual(Object o1, Object o2);
195
196 abstract boolean forceBefore(Object o1, Object o2);
197
198 abstract boolean forceBefore(Relation r1, Attribute a1, Relation r2, Attribute a2);
199
200 abstract boolean forceInterleaved(Object o1, Object o2);
201
202 abstract boolean forceInterleaved(Relation r1, Attribute a1, Relation r2, Attribute a2);
203
204 public void forceConstraints(Relation r) {
205 Constraints cons = (Constraints) constraintMap.get(r);
206
207 if (cons != null) {
208 Collection bcons = cons.getBeforeConstraints();
209 if (TRACE && bcons.size() == 0) solver.out.println("No before constraints for " + r);
210 for (Iterator it = bcons.iterator(); it.hasNext();) {
211 Constraint c = (Constraint) it.next();
212 forceBefore(c.getLeftRelation(), c.getLeftAttribute(),
213 c.getRightRelation(), c.getRightAttribute());
214 }
215 Collection icons = cons.getInterleavedConstraints();
216 for (Iterator it = icons.iterator(); it.hasNext();) {
217 Constraint c = (Constraint) it.next();
218 forceInterleaved(c.getLeftRelation(), c.getLeftAttribute(),
219 c.getRightRelation(), c.getRightAttribute());
220 }
221 }
222 }
223
224
225
226
227
228
229
230 boolean forceEqual(Relation r1, Attribute a1, int k) {
231 Domain dom = a1.getDomain();
232 BDDDomain d = ((BDDSolver) solver).getBDDDomain(dom, k);
233 return forceEqual(new Pair(r1, a1), d);
234 }
235
236
237
238
239
240
241
242
243 boolean forceEqual(Relation r1, Attribute a1, Relation r2, Attribute a2, boolean equal) {
244 Pair p1 = new Pair(r1, a1);
245 Pair p2 = new Pair(r2, a2);
246 if (equal) {
247 return forceEqual(p1, p2);
248 } else {
249 return forceNotEqual(p1, p2);
250 }
251 }
252
253 void insertBefore(Operation op) {
254 if (TRACE) solver.out.println("Inserting before current operation: " + op);
255 inserted.add(op);
256 currentBlock.previous();
257 currentBlock.add(op);
258 currentBlock.next();
259 }
260
261 void insertAfter(Operation op) {
262 if (TRACE) solver.out.println("Inserting after current operation: " + op);
263 inserted.add(op);
264 currentBlock.add(op);
265 }
266
267 abstract Relation allocNewRelation(Relation old_r);
268
269 Relation insertReplaceBefore(Operation op, Relation r1) {
270 Relation r1_new = allocNewRelation(r1);
271 Operation move = new Replace((BDDRelation) r1_new, (BDDRelation) r1);
272 insertBefore(move);
273 op.replaceSrc(r1, r1_new);
274 r1 = r1_new;
275 return r1;
276 }
277
278 Relation insertReplaceAfter(Operation op, Relation r0) {
279 Relation r0_new = allocNewRelation(r0);
280 Operation move = new Replace((BDDRelation) r0, (BDDRelation) r0_new);
281 insertAfter(move);
282 op.setRelationDest(r0_new);
283 r0 = r0_new;
284 return r0;
285 }
286
287 Object visitUnaryOp(Operation op, Relation r0, Relation r1) {
288 if (TRACE) solver.out.println("Unary op: " + op);
289 for (Iterator i = r1.getAttributes().iterator(); i.hasNext();) {
290 Attribute a1 = (Attribute) i.next();
291 if (r0.getAttributes().contains(a1)) {
292 if (!forceEqual(r1, a1, r0, a1, true)) {
293
294
295 r1 = insertReplaceBefore(op, r1);
296 return visitUnaryOp(op, r0, r1);
297 }
298 }
299 }
300 forceConstraints(r0);
301 return null;
302 }
303
304 Object visitBooleanOp(BooleanOperation op) {
305 Relation r0 = op.getRelationDest();
306 Relation r1 = op.getSrc1();
307 Relation r2 = op.getSrc2();
308 return visitBooleanOp(op, r0, r1, r2);
309 }
310
311 Object visitBooleanOp(Operation op, Relation r0, Relation r1, Relation r2) {
312 if (TRACE) solver.out.println("Boolean op: " + op);
313 for (Iterator i = r1.getAttributes().iterator(); i.hasNext();) {
314 Attribute a1 = (Attribute) i.next();
315 for (Iterator j = r2.getAttributes().iterator(); j.hasNext();) {
316 Attribute a2 = (Attribute) j.next();
317 if (a1 == a2) {
318 if (!forceEqual(r1, a1, r2, a2, true)) {
319
320
321 if (false) {
322 r1 = insertReplaceBefore(op, r1);
323 } else {
324 r2 = insertReplaceBefore(op, r2);
325 }
326 return visitBooleanOp(op, r0, r1, r2);
327 }
328 } else if (a1.getDomain() == a2.getDomain()) {
329 if (!forceEqual(r1, a1, r2, a2, false)) {
330
331
332 if (false) {
333 r1 = insertReplaceBefore(op, r1);
334 } else {
335 r2 = insertReplaceBefore(op, r2);
336 }
337 return visitBooleanOp(op, r0, r1, r2);
338 }
339 }
340 }
341 }
342 for (Iterator i = r0.getAttributes().iterator(); i.hasNext();) {
343 Attribute a0 = (Attribute) i.next();
344 for (Iterator j = r1.getAttributes().iterator(); j.hasNext();) {
345 Attribute a1 = (Attribute) j.next();
346 if (a0 == a1) {
347 if (!forceEqual(r0, a0, r1, a1, true)) {
348
349 r0 = insertReplaceAfter(op, r0);
350 return visitBooleanOp(op, r0, r1, r2);
351 }
352 }
353 }
354 for (Iterator j = r2.getAttributes().iterator(); j.hasNext();) {
355 Attribute a2 = (Attribute) j.next();
356 if (a0 == a2) {
357 if (!forceEqual(r0, a0, r2, a2, true)) {
358
359 r0 = insertReplaceAfter(op, r0);
360 return visitBooleanOp(op, r0, r1, r2);
361 }
362 }
363 }
364 }
365 forceConstraints(r0);
366 return null;
367 }
368
369
370
371
372
373
374 public Object visit(Join op) {
375 return visitBooleanOp(op);
376 }
377
378
379
380
381
382
383 public Object visit(Project op) {
384 Relation r0 = op.getRelationDest();
385 Relation r1 = op.getSrc();
386 return visitUnaryOp(op, r0, r1);
387 }
388 public Object visit(BDDProject op) {
389 Assert.UNREACHABLE();
390 return null;
391 }
392
393
394
395
396
397
398 public Object visit(Rename op) {
399 if (TRACE) solver.out.println("Rename op: " + op);
400 Relation r0 = op.getRelationDest();
401 Relation r1 = op.getSrc();
402 for (Iterator i = r1.getAttributes().iterator(); i.hasNext();) {
403 Attribute a1 = (Attribute) i.next();
404 Attribute a0 = (Attribute) op.getRenameMap().get(a1);
405 if (a0 == null){
406 a0 = a1;
407 }
408 if (!forceEqual(r1, a1, r0, a0, true)) {
409
410
411 r1 = insertReplaceBefore(op, r1);
412 return visit(op);
413 }
414 }
415 forceConstraints(r0);
416 return null;
417 }
418
419
420
421
422
423
424 public Object visit(Union op) {
425 return visitBooleanOp(op);
426 }
427
428
429
430
431
432
433 public Object visit(Difference op) {
434 return visitBooleanOp(op);
435 }
436
437
438
439
440
441
442 public Object visit(JoinConstant op) {
443 Relation r0 = op.getRelationDest();
444 Relation r1 = op.getSrc();
445 return visitUnaryOp(op, r0, r1);
446 }
447
448
449
450
451
452
453 public Object visit(GenConstant op) {
454 return null;
455 }
456
457
458
459
460
461
462 public Object visit(Free op) {
463 return null;
464 }
465
466
467
468
469
470
471 public Object visit(Universe op) {
472 return null;
473 }
474
475
476
477
478
479
480 public Object visit(Zero op) {
481 return null;
482 }
483
484
485
486
487
488
489 public Object visit(Invert op) {
490 Relation r0 = op.getRelationDest();
491 Relation r1 = op.getSrc();
492 return visitUnaryOp(op, r0, r1);
493 }
494
495
496
497
498
499
500 public Object visit(Copy op) {
501 Relation r0 = op.getRelationDest();
502 Relation r1 = op.getSrc();
503 return visitUnaryOp(op, r0, r1);
504 }
505
506
507
508
509
510
511 public Object visit(Replace op) {
512 Relation r0 = op.getRelationDest();
513 Relation r1 = op.getSrc();
514 return visitUnaryOp(op, r0, r1);
515 }
516
517
518
519
520
521
522 public Object visit(Load op) {
523 if (TRACE) solver.out.println("Load op: " + op);
524 Relation r0 = op.getRelationDest();
525 for (Iterator i = r0.getAttributes().iterator(); i.hasNext();) {
526 Attribute a = (Attribute) i.next();
527 String option = a.getOptions();
528 if (option == null || option.length() == 0) continue;
529 Domain d = a.getDomain();
530 int number = Integer.parseInt(option.substring(d.toString().length()));
531 if (!forceEqual(r0, a, number)) {
532
533 r0 = insertReplaceAfter(op, r0);
534 return visit(op);
535 }
536 }
537 forceConstraints(r0);
538 return null;
539 }
540
541
542
543
544
545
546 public Object visit(Save op) {
547 if (TRACE) solver.out.println("Save op: " + op);
548 Relation r1 = op.getSrc();
549 for (Iterator i = r1.getAttributes().iterator(); i.hasNext();) {
550 Attribute a = (Attribute) i.next();
551 String option = a.getOptions();
552 if (option == null || option.length() == 0) continue;
553 Domain d = a.getDomain();
554 int number = Integer.parseInt(option.substring(d.toString().length()));
555 if (!forceEqual(r1, a, number)) {
556
557 r1 = insertReplaceBefore(op, r1);
558 return visit(op);
559 }
560 }
561 forceConstraints(r1);
562 return null;
563 }
564
565
566
567
568
569
570 public Object visit(ApplyEx op) {
571 Relation r0 = op.getRelationDest();
572 Relation r1 = op.getSrc1();
573 Relation r2 = op.getSrc2();
574 return visitBooleanOp(op, r0, r1, r2);
575 }
576
577
578
579
580
581
582 public Object visit(If op) {
583 return null;
584 }
585
586
587
588
589
590
591 public Object visit(Nop op) {
592 return null;
593 }
594
595 public abstract void saveDomainAssignment(BufferedWriter out) throws IOException;
596
597 public void loadDomainAssignment(BufferedReader in) throws IOException {
598 BDDSolver bs = (BDDSolver) solver;
599 int count = 0;
600 solver.out.println("Loading domain assignment from file...");
601 for (;;) {
602 String s = in.readLine();
603 if (s == null) break;
604 s = s.trim();
605 if (s.length() == 0) continue;
606 if (s.startsWith("#")) continue;
607 StringTokenizer st = new StringTokenizer(s);
608 {
609 Object o1 = null, o2 = null;
610 String constraint;
611 String s1 = st.nextToken();
612 String s2 = st.nextToken();
613 String s3 = st.nextToken();
614 if (s2.equals("=") || s2.equals("!=") || s2.equals("<") || s2.equals("~")) {
615 o1 = bs.getBDDDomain(s1);
616 constraint = s2;
617 if (!st.hasMoreTokens()) {
618 o2 = bs.getBDDDomain(s3);
619 } else {
620 String s4 = st.nextToken();
621 Relation r = bs.getRelation(s3);
622 Attribute a = r != null ? r.getAttribute(s4) : null;
623 if (r != null && a != null) o2 = new Pair(r, a);
624 }
625 } else {
626 Relation r1 = bs.getRelation(s1);
627 Attribute a1 = r1 != null ? r1.getAttribute(s2) : null;
628 if (r1 != null && a1 != null) o1 = new Pair(r1, a1);
629 constraint = s3;
630 String s4 = st.nextToken();
631 if (!st.hasMoreTokens()) {
632 o2 = bs.getBDDDomain(s4);
633 } else {
634 String s5 = st.nextToken();
635 Relation r2 = bs.getRelation(s4);
636 Attribute a2 = r2 != null ? r1.getAttribute(s5) : null;
637 if (r2 != null && a2 != null) o2 = new Pair(r2, a2);
638 }
639 }
640 boolean success = false;
641 if (o1 != null && o2 != null) {
642 if (constraint.equals("=")) {
643 success = forceEqual(o1, o2);
644 } else if (constraint.equals("!=")) {
645 success = forceNotEqual(o1, o2);
646 } else if (constraint.equals("<")) {
647 success = forceBefore(o1, o2);
648 } else if (constraint.equals("~")) {
649 success = forceInterleaved(o1, o2);
650 }
651 }
652 if (!success) {
653 if(TRACE) solver.out.println("Cannot add constraint: " + s);
654 } else {
655 ++count;
656 }
657 }
658 }
659 solver.out.println("Incorporated " + count + " constraints from file.");
660 }
661
662 public abstract void setVariableOrdering();
663 }