View Javadoc

1   // BDDOperationInterpreter.java, created Jun 29, 2004 12:54:42 PM 2004 by jwhaley
2   // Copyright (C) 2004 John Whaley <jwhaley@alum.mit.edu>
3   // Licensed under the terms of the GNU LGPL; see COPYING for details.
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.List;
10  import java.util.Map;
11  import java.io.IOException;
12  import jwutil.io.SystemProperties;
13  import jwutil.util.Assert;
14  import net.sf.bddbddb.Attribute;
15  import net.sf.bddbddb.BDDRelation;
16  import net.sf.bddbddb.BDDSolver;
17  import net.sf.bddbddb.Domain;
18  import net.sf.bddbddb.ir.dynamic.If;
19  import net.sf.bddbddb.ir.dynamic.Nop;
20  import net.sf.bddbddb.ir.highlevel.Copy;
21  import net.sf.bddbddb.ir.highlevel.Difference;
22  import net.sf.bddbddb.ir.highlevel.Free;
23  import net.sf.bddbddb.ir.highlevel.GenConstant;
24  import net.sf.bddbddb.ir.highlevel.Invert;
25  import net.sf.bddbddb.ir.highlevel.Join;
26  import net.sf.bddbddb.ir.highlevel.JoinConstant;
27  import net.sf.bddbddb.ir.highlevel.Load;
28  import net.sf.bddbddb.ir.highlevel.Project;
29  import net.sf.bddbddb.ir.highlevel.Rename;
30  import net.sf.bddbddb.ir.highlevel.Save;
31  import net.sf.bddbddb.ir.highlevel.Union;
32  import net.sf.bddbddb.ir.highlevel.Universe;
33  import net.sf.bddbddb.ir.highlevel.Zero;
34  import net.sf.bddbddb.ir.lowlevel.ApplyEx;
35  import net.sf.bddbddb.ir.lowlevel.BDDProject;
36  import net.sf.bddbddb.ir.lowlevel.Replace;
37  import net.sf.javabdd.BDD;
38  import net.sf.javabdd.BDDDomain;
39  import net.sf.javabdd.BDDFactory;
40  import net.sf.javabdd.BDDPairing;
41  import net.sf.javabdd.BDDVarSet;
42  import net.sf.javabdd.BDDFactory.BDDOp;
43  
44  /***
45   * BDDOperationInterpreter
46   * 
47   * @author jwhaley
48   * @version $Id: BDDOperationInterpreter.java 650 2006-11-29 08:08:45Z joewhaley $
49   */
50  public class BDDOperationInterpreter implements OperationInterpreter {
51      boolean TRACE = SystemProperties.getProperty("traceinterpreter") != null;
52      BDDFactory factory;
53      String varorder;
54      BDDSolver solver;
55      public boolean needsDomainMatch;
56  
57      /***
58       * @param factory
59       */
60      public BDDOperationInterpreter(BDDSolver solver, BDDFactory factory) {
61          this.solver = solver;
62          this.factory = factory;
63          this.varorder = solver.VARORDER;
64          this.needsDomainMatch = true;
65      }
66      public static boolean CHECK = !SystemProperties.getProperty("checkir", "no").equals("no");
67  
68      protected BDD makeDomainsMatch(BDD b, BDDRelation r1, BDDRelation r2) {
69          if (CHECK) {
70              r1.verify();
71              r2.verify();
72          }
73          if (!needsDomainMatch) return b;
74          boolean any = false;
75   
76          BDDPairing pair = factory.makePair();
77          for (Iterator i = r1.getAttributes().iterator(); i.hasNext();) {
78              Attribute a = (Attribute) i.next();
79              BDDDomain d1 = r1.getBDDDomain(a);
80              BDDDomain d2 = r2.getBDDDomain(a);
81              if (d2 == null || d1 == d2) continue;
82              any = true;
83              pair.set(d1, d2);
84              if (TRACE) solver.out.println("   " + a + " Renaming " + d1 + " to " + d2);
85              if (CHECK && varorder != null) {
86                  int index1 = varorder.indexOf(d1.toString());
87                  int index2 = varorder.indexOf(d2.toString());
88                  for (Iterator j = r2.getAttributes().iterator(); j.hasNext();) {
89                      Attribute a2 = (Attribute) j.next();
90                      if (a2 == a) continue;
91                      BDDDomain d3 = r2.getBDDDomain(a2);
92                      int index3 = varorder.indexOf(d3.toString());
93                      boolean bad;
94                      if (index1 < index2) bad = (index3 >= index1 && index3 <= index2);
95                      else bad = (index3 >= index2 && index3 <= index1);
96                      if (bad) {
97                          if (TRACE) solver.out.println("Expensive rename! " + r1 + "->" + r2 + ": " + d1 + " to " + d2 + " across " + d3);
98                      }
99                  }
100             }
101         }
102         if (any) {
103             if (TRACE) solver.out.println("      Rename to make " + r1 + " match " + r2);
104             b.replaceWith(pair);
105             if (TRACE) solver.out.println("      Domains of result: " + BDDRelation.activeDomains(b));
106         }
107         pair.reset();
108         return b;
109     }
110 
111     BDDDomain getUnusedDomain(Domain d, Collection dontuse) {
112         for (Iterator i = solver.getBDDDomains(d).iterator(); i.hasNext(); ) {
113             BDDDomain dd = (BDDDomain) i.next();
114             if (!dontuse.contains(dd)) return dd;
115         }
116         BDDDomain dd = solver.allocateBDDDomain(d);
117         return dd;
118     }
119     
120     BDDVarSet getProjectSet(Map m, BDDRelation r1, BDDRelation r2, BDDRelation r3) {
121         BDDVarSet b = factory.emptySet();
122         for (Iterator i = r2.getAttributes().iterator(); i.hasNext();) {
123             Attribute a = (Attribute) i.next();
124             if (r1.getAttributes().contains(a)) continue;
125             BDDDomain d = (m != null)?(BDDDomain)m.get(a):r2.getBDDDomain(a);
126             b.unionWith(d.set());
127         }
128         for (Iterator i = r3.getAttributes().iterator(); i.hasNext();) {
129             Attribute a = (Attribute) i.next();
130             if (r1.getAttributes().contains(a)) continue;
131             BDDDomain d = (m != null)?(BDDDomain)m.get(a):r3.getBDDDomain(a);
132             b.unionWith(d.set());
133         }
134         return b;
135     }
136     
137     protected BDDVarSet makeDomainsMatch(BDD b2, BDD b3, BDDRelation r1, BDDRelation r2, BDDRelation r3) {
138         if (CHECK) {
139             r1.verify();
140             r2.verify();
141             r3.verify();
142         }
143         if (!needsDomainMatch) {
144             return getProjectSet(null, r1, r2, r3);
145         }
146         boolean any2 = false, any3 = false;
147         BDDPairing pair2 = factory.makePair();
148         BDDPairing pair3 = factory.makePair();
149         Map renameMap = new HashMap();
150         for (Iterator i = r1.getAttributes().iterator(); i.hasNext();) {
151             Attribute a = (Attribute) i.next();
152             BDDDomain d1 = r1.getBDDDomain(a);
153             renameMap.put(a, d1);
154         }
155         for (Iterator i = r2.getAttributes().iterator(); i.hasNext();) {
156             Attribute a = (Attribute) i.next();
157             BDDDomain d2 = r2.getBDDDomain(a);
158             BDDDomain d1 = (BDDDomain) renameMap.get(a);
159             if (d1 == null) {
160                 if (!renameMap.values().contains(d2)) d1 = d2;
161                 else d1 = getUnusedDomain(a.getDomain(), renameMap.values());
162                 renameMap.put(a, d1);
163             }
164             if (d1 != d2) {
165                 pair2.set(d2, d1);
166                 any2 = true;
167                 if (TRACE) solver.out.println("   "+r2+": " + a + " Renaming " + d2 + " to " + d1);
168             }
169         }
170         for (Iterator i = r3.getAttributes().iterator(); i.hasNext();) {
171             Attribute a = (Attribute) i.next();
172             BDDDomain d3 = r3.getBDDDomain(a);
173             BDDDomain d1 = (BDDDomain) renameMap.get(a);
174             if (d1 == null) {
175                 if (!renameMap.values().contains(d3)) d1 = d3;
176                 else d1 = getUnusedDomain(a.getDomain(), renameMap.values());
177                 renameMap.put(a, d1);
178             }
179             if (d1 != d3) {
180                 pair3.set(d3, d1);
181                 any3 = true;
182                 if (TRACE) solver.out.println("   "+r3+": " + a + " Renaming " + d3 + " to " + d1);
183             }
184         }
185         if (any2) {
186             if (TRACE) solver.out.println("      Rename to make " + r2 + " match " + r1);
187             b2.replaceWith(pair2);
188             if (TRACE) solver.out.println("      Domains of result: " + BDDRelation.activeDomains(b2));
189         }
190         if (any3) {
191             if (TRACE) solver.out.println("      Rename to make " + r3 + " match " + r1);
192             b3.replaceWith(pair3);
193             if (TRACE) solver.out.println("      Domains of result: " + BDDRelation.activeDomains(b3));
194         }
195         pair2.reset();
196         pair3.reset();
197         return getProjectSet(renameMap, r1, r2, r3);
198     }
199     
200     /*
201      * (non-Javadoc)
202      * 
203      * @see net.sf.bddbddb.ir.HighLevelInterpreter#visit(net.sf.bddbddb.ir.Join)
204      */
205     public Object visit(Join op) {
206         BDDRelation r0 = (BDDRelation) op.getRelationDest();
207         BDDRelation r1 = (BDDRelation) op.getSrc1();
208         BDDRelation r2 = (BDDRelation) op.getSrc2();
209         BDD b1 = makeDomainsMatch(r1.getBDD().id(), r1, r0);
210         BDD b2 = makeDomainsMatch(r2.getBDD().id(), r2, r0);
211         if (TRACE) solver.out.println("   And " + r1 + "," + r2);
212         b1.andWith(b2);
213         r0.setBDD(b1);
214         if (TRACE) solver.out.println("   ---> Nodes: " + b1.nodeCount() + " Domains: " + BDDRelation.activeDomains(b1));
215         if (TRACE) solver.out.println("   ---> " + r0 + "+ elements: "+r0.dsize());
216         return null;
217     }
218 
219     /*
220      * (non-Javadoc)
221      * 
222      * @see net.sf.bddbddb.ir.HighLevelInterpreter#visit(net.sf.bddbddb.ir.Project)
223      */
224     public Object visit(Project op) {
225         if(!needsDomainMatch) 
226             Assert.UNREACHABLE(); /* if we ran domain assignment we should only see BDDProjects */
227         
228         BDDRelation r0 = (BDDRelation) op.getRelationDest();
229         BDDRelation r1 = (BDDRelation) op.getSrc();
230         List attributes = op.getAttributes();
231         BDDVarSet b = factory.emptySet();
232         for (Iterator i = attributes.iterator(); i.hasNext();) {
233             Attribute a = (Attribute) i.next();
234             BDDDomain d = r1.getBDDDomain(a);
235             b.unionWith(d.set());
236             if (TRACE) solver.out.println("   Projecting " + d);
237         }
238         if (TRACE) solver.out.println("   Exist " + r1);
239         BDD r = r1.getBDD().exist(b);
240         b.free();
241         BDD b1 = makeDomainsMatch(r, r1, r0);
242         r0.setBDD(b1);
243         if (TRACE) solver.out.println("   ---> Nodes: " + b1.nodeCount() + " Domains: " + BDDRelation.activeDomains(b1));
244         if (TRACE) solver.out.println("   ---> " + r0 + "+ elements: "+r0.dsize());
245         return null;
246     }
247     
248     public Object visit(BDDProject op) {
249         if(needsDomainMatch)
250             Assert.UNREACHABLE(); /* without domain assignment we can't see these */
251             
252         BDDRelation r0 = (BDDRelation) op.getRelationDest();
253         BDDRelation r1 = (BDDRelation) op.getSrc();
254         List domains = op.getDomains();
255         BDDVarSet b = factory.emptySet();
256         for (Iterator i = domains.iterator(); i.hasNext();) {
257             BDDDomain d = (BDDDomain) i.next();
258             b.unionWith(d.set());
259             if (TRACE) solver.out.println("   Projecting " + d);
260         }
261         if (TRACE) solver.out.println("   Exist " + r1);
262         BDD r = r1.getBDD().exist(b);
263         b.free();
264         r0.setBDD(r);
265         if (TRACE) solver.out.println("   ---> Nodes: " + r.nodeCount() + " Domains: " + BDDRelation.activeDomains(r));
266         if (TRACE) solver.out.println("   ---> " + r0 + "+ elements: "+r0.dsize());
267         return null;
268     }
269     
270     /*
271      * (non-Javadoc)
272      * 
273      * @see net.sf.bddbddb.ir.HighLevelInterpreter#visit(net.sf.bddbddb.ir.Rename)
274      */
275     public Object visit(Rename op) {
276         if(!needsDomainMatch)
277             Assert.UNREACHABLE(); /* all renames should be removed after domains assignment */
278         
279         BDDRelation r0 = (BDDRelation) op.getRelationDest();
280         BDDRelation r1 = (BDDRelation) op.getSrc();
281         if (CHECK) {
282             r1.verify();
283         }
284         Map renames = op.getRenameMap();
285         boolean any = false;
286         BDDPairing pair = factory.makePair();
287         for (Iterator i = r1.getAttributes().iterator(); i.hasNext();) {
288             Attribute a1 = (Attribute) i.next();
289             BDDDomain d1 = r1.getBDDDomain(a1);
290             Attribute a0 = (Attribute) renames.get(a1);
291             if (a0 == null) a0 = a1;
292             BDDDomain d0 = r0.getBDDDomain(a0);
293             Assert._assert(d0 != null);
294             if (d1.equals(d0)) continue;
295             any = true;
296             pair.set(d1, d0);
297             if (TRACE) solver.out.println("   Renaming " + d1 + " to " + d0);
298         }
299         BDD b = r1.getBDD().id();
300         if (any) {
301             if (TRACE) solver.out.println("   " + r0 + " = Replace " + r1);
302             b.replaceWith(pair);
303         }
304         pair.reset();
305         r0.setBDD(b);
306         if (TRACE) solver.out.println("   ---> Nodes: " + b.nodeCount() + " Domains: " + BDDRelation.activeDomains(b));
307         if (TRACE) solver.out.println("   ---> " + r0 + "+ elements: "+r0.dsize());
308         if (CHECK) {
309             r0.verify();
310         }
311         return null;
312     }
313 
314     /*
315      * (non-Javadoc)
316      * 
317      * @see net.sf.bddbddb.ir.HighLevelInterpreter#visit(net.sf.bddbddb.ir.Union)
318      */
319     public Object visit(Union op) {
320         BDDRelation r0 = (BDDRelation) op.getRelationDest();
321         BDDRelation r1 = (BDDRelation) op.getSrc1();
322         BDDRelation r2 = (BDDRelation) op.getSrc2();
323         BDD b1 = makeDomainsMatch(r1.getBDD().id(), r1, r0);
324         BDD b2 = makeDomainsMatch(r2.getBDD().id(), r2, r0);
325         if (TRACE) solver.out.println("   Or " + r1 + "," + r2);
326         b1.orWith(b2);
327         r0.setBDD(b1);
328         if (TRACE) solver.out.println("   ---> Nodes: " + b1.nodeCount() + " Domains: " + BDDRelation.activeDomains(b1));
329         if (TRACE) solver.out.println("   ---> " + r0 + "+ elements: "+r0.dsize());
330         return null;
331     }
332 
333     /*
334      * (non-Javadoc)
335      * 
336      * @see net.sf.bddbddb.ir.HighLevelInterpreter#visit(net.sf.bddbddb.ir.Difference)
337      */
338     public Object visit(Difference op) {
339         BDDRelation r0 = (BDDRelation) op.getRelationDest();
340         BDDRelation r1 = (BDDRelation) op.getSrc1();
341         BDDRelation r2 = (BDDRelation) op.getSrc2();
342         BDD b1 = makeDomainsMatch(r1.getBDD().id(), r1, r0);
343         BDD b2 = makeDomainsMatch(r2.getBDD().id(), r2, r0);
344         if (TRACE) solver.out.println("   " + r0 + " = Diff " + r1 + "," + r2);
345         b1.applyWith(b2, BDDFactory.diff);
346         r0.setBDD(b1);
347         if (TRACE) solver.out.println("   ---> Nodes: " + b1.nodeCount() + " Domains: " + BDDRelation.activeDomains(b1));
348         if (TRACE) solver.out.println("   ---> " + r0 + "+ elements: "+r0.dsize());
349         return null;
350     }
351 
352     /*
353      * (non-Javadoc)
354      * 
355      * @see net.sf.bddbddb.ir.HighLevelInterpreter#visit(net.sf.bddbddb.ir.JoinConstant)
356      */
357     public Object visit(JoinConstant op) {
358         BDDRelation r0 = (BDDRelation) op.getRelationDest();
359         BDDRelation r1 = (BDDRelation) op.getSrc();
360         Attribute a = op.getAttribute();
361         if(TRACE) solver.out.println(r0 + ": " + r0.getAttributes() + " " + r0.getBDDDomains());
362         if(TRACE) solver.out.println(r1 + ": " + r1.getAttributes() + " " + r1.getBDDDomains());
363         long value = op.getValue();
364         BDD r = makeDomainsMatch(r1.getBDD().id(), r1, r0);
365         if (TRACE) solver.out.println("   " + r0 + " = And " + r1 + "," + r0.getBDDDomain(a) + ":" + value);
366         r.andWith(r0.getBDDDomain(a).ithVar(value));
367         r0.setBDD(r);
368         if (TRACE) solver.out.println("   ---> Nodes: " + r.nodeCount() + " Domains: " + BDDRelation.activeDomains(r));
369         if (TRACE) solver.out.println("   ---> " + r0 + "+ elements: "+r0.dsize());
370         return null;
371     }
372 
373     /*
374      * (non-Javadoc)
375      * 
376      * @see net.sf.bddbddb.ir.HighLevelInterpreter#visit(net.sf.bddbddb.ir.GenConstant)
377      */
378     public Object visit(GenConstant op) {
379         BDDRelation r0 = (BDDRelation) op.getRelationDest();
380         Attribute a = op.getAttribute();
381         long value = op.getValue();
382         if (TRACE) solver.out.println("   " + r0 + " = Ithvar " + r0.getBDDDomain(a) + ":" + value);
383         BDD r = r0.getBDDDomain(a).ithVar(value);
384         r0.setBDD(r);
385         if (TRACE) solver.out.println("   ---> Nodes: " + r.nodeCount());
386         if (TRACE) solver.out.println("   ---> " + r0 + "+ elements: "+r0.dsize());
387         return null;
388     }
389 
390     /*
391      * (non-Javadoc)
392      * 
393      * @see net.sf.bddbddb.ir.HighLevelInterpreter#visit(net.sf.bddbddb.ir.Free)
394      */
395     public Object visit(Free op) {
396         BDDRelation r = (BDDRelation) op.getSrc();
397         if (TRACE) solver.out.println("   Free " + r);
398         r.free();
399         //BDD b = factory.zero();
400         //r.setBDD(b);
401         return null;
402     }
403 
404     /*
405      * (non-Javadoc)
406      * 
407      * @see net.sf.bddbddb.ir.HighLevelInterpreter#visit(net.sf.bddbddb.ir.Zero)
408      */
409     public Object visit(Zero op) {
410         BDDRelation r = (BDDRelation) op.getRelationDest();
411         BDD b = factory.zero();
412         if (TRACE) solver.out.println("   Zero " + r);
413         r.setBDD(b);
414         if (TRACE) solver.out.println("   ---> Nodes: " + b.nodeCount());
415         return null;
416     }
417 
418     /*
419      * (non-Javadoc)
420      * 
421      * @see net.sf.bddbddb.ir.HighLevelInterpreter#visit(net.sf.bddbddb.ir.Universe)
422      */
423     public Object visit(Universe op) {
424         BDDRelation r = (BDDRelation) op.getRelationDest();
425         BDD b = factory.universe();
426         for (Iterator i = r.getAttributes().iterator(); i.hasNext();) {
427             Attribute a = (Attribute) i.next();
428             BDDDomain d = r.getBDDDomain(a);
429             b.andWith(d.domain());
430         }
431         if (TRACE) solver.out.println("   Domain " + r);
432         r.setBDD(b);
433         if (TRACE) solver.out.println("   ---> Nodes: " + b.nodeCount());
434         return null;
435     }
436 
437     /*
438      * (non-Javadoc)
439      * 
440      * @see net.sf.bddbddb.ir.HighLevelInterpreter#visit(net.sf.bddbddb.ir.Invert)
441      */
442     public Object visit(Invert op) {
443         BDDRelation r0 = (BDDRelation) op.getRelationDest();
444         BDDRelation r1 = (BDDRelation) op.getSrc();
445         if (TRACE) solver.out.println("   " + r0 + " = Not " + r1);
446         BDD r = makeDomainsMatch(r1.getBDD().not(), r1, r0);
447         r0.setBDD(r);
448         if (TRACE) solver.out.println("   ---> Nodes: " + r.nodeCount() + " Domains: " + BDDRelation.activeDomains(r));
449         if (TRACE) solver.out.println("   ---> " + r0 + "+ elements: "+r0.dsize());
450         return null;
451     }
452 
453     /*
454      * (non-Javadoc)
455      * 
456      * @see net.sf.bddbddb.ir.HighLevelInterpreter#visit(net.sf.bddbddb.ir.Copy)
457      */
458     public Object visit(Copy op) {
459         BDDRelation r0 = (BDDRelation) op.getRelationDest();
460         BDDRelation r1 = (BDDRelation) op.getSrc();
461         if (TRACE) solver.out.println("   " + r0 + " = Id " + r1);
462         BDD r = makeDomainsMatch(r1.getBDD().id(), r1, r0);
463         r0.setBDD(r);
464         if (TRACE) solver.out.println("   ---> Nodes: " + r.nodeCount() + " Domains: " + BDDRelation.activeDomains(r));
465         if (TRACE) solver.out.println("   ---> " + r0 + "+ elements: "+r0.dsize());
466         return null;
467     }
468 
469     /*
470      * (non-Javadoc)
471      * 
472      * @see net.sf.bddbddb.ir.HighLevelOperationVisitor#visit(net.sf.bddbddb.ir.Load)
473      */
474     public Object visit(Load op) {
475         BDDRelation r = (BDDRelation) op.getRelationDest();
476         try {
477             if (op.isTuples()) {
478                 r.loadTuples(op.getFileName());
479             } else {
480                 r.load(op.getFileName());
481             }
482         } catch (IOException x) {
483         }
484         solver.startTime = System.currentTimeMillis();
485         return null;
486     }
487 
488     /*
489      * (non-Javadoc)
490      * 
491      * @see net.sf.bddbddb.ir.HighLevelInterpreter#visit(net.sf.bddbddb.ir.Save)
492      */
493     public Object visit(Save op) {
494         long time = System.currentTimeMillis();
495         BDDRelation r = (BDDRelation) op.getSrc();
496         try {
497             if (op.isTuples()) {
498                 r.saveTuples(op.getFileName());
499             } else {
500                 r.save(op.getFileName());
501             }
502         } catch (IOException x) {
503         }
504         solver.startTime += (System.currentTimeMillis() - time);
505         return null;
506     }
507 
508     /*
509      * (non-Javadoc)
510      * 
511      * @see net.sf.bddbddb.ir.lowlevel.LowLevelOperationVisitor#visit(net.sf.bddbddb.ir.lowlevel.ApplyEx)
512      */
513     public Object visit(ApplyEx op) {
514         BDDRelation r0 = (BDDRelation) op.getRelationDest();
515         BDDRelation r1 = (BDDRelation) op.getSrc1();
516         BDDRelation r2 = (BDDRelation) op.getSrc2();
517         BDDOp bddop = op.getOp();
518         //solver.out.println("Dest: " + r0 + " attrs: " + r0.getAttributes() + " domains: " + r0.getBDDDomains());
519         //solver.out.println("Src1: " + r1 + " attrs: " + r1.getAttributes() + " domains: " + r1.getBDDDomains());
520         //solver.out.println("Src2: " + r2 + " attrs: " + r2.getAttributes() + " domains: " + r2.getBDDDomains());
521      
522         BDD b1 = r1.getBDD().id();
523         BDD b2 = r2.getBDD().id();
524         BDDVarSet b3 = needsDomainMatch ? makeDomainsMatch(b1, b2, r0, r1, r2) : op.getProjectSet();
525         //if (TRACE) solver.out.println("   " + op.toString());
526         BDD b = b1.applyEx(b2, bddop, b3);
527         b1.free();
528         b2.free();
529         b3.free();
530         r0.setBDD(b);
531         if (TRACE) solver.out.println("   ---> Nodes: " + b.nodeCount() + " Domains: " + BDDRelation.activeDomains(b));
532         if (TRACE) solver.out.println("   ---> " + r0 + "+ elements: "+r0.dsize());
533         if (CHECK) {
534             r0.verify();
535         }
536         return null;
537     }
538 
539     /*
540      * (non-Javadoc)
541      * 
542      * @see net.sf.bddbddb.ir.dynamic.DynamicOperationVisitor#visit(net.sf.bddbddb.ir.dynamic.If)
543      */
544     public Object visit(If op) {
545         return null;
546     }
547 
548     /*
549      * (non-Javadoc)
550      * 
551      * @see net.sf.bddbddb.ir.dynamic.DynamicOperationVisitor#visit(net.sf.bddbddb.ir.dynamic.Nop)
552      */
553     public Object visit(Nop op) {
554         return null;
555     }
556 
557     /*
558      * (non-Javadoc)
559      * 
560      * @see net.sf.bddbddb.ir.lowlevel.LowLevelOperationVisitor#visit(net.sf.bddbddb.ir.lowlevel.Replace)
561      */
562     public Object visit(Replace op) {
563         BDDRelation r0 = (BDDRelation) op.getRelationDest();
564         BDDRelation r1 = (BDDRelation) op.getSrc();
565         BDDPairing pair = op.getPairing();
566         BDD r = pair != null ? r1.getBDD().replace(pair) : r1.getBDD().id();
567         r0.setBDD(r);
568         if (TRACE) solver.out.println("   ---> Nodes: " + r.nodeCount() + " Domains: " + BDDRelation.activeDomains(r));
569         if (TRACE) solver.out.println("   ---> " + r0 + "+ elements: "+r0.dsize());
570         return null;
571     }
572 }