SE547: BDDs: Bool Code [19/22] Previous pageContentsNext page

file:simplebdd/bool/BoolPred.java [source] [doc-public] [doc-private]
00001: package simplebdd.bool;
00002: 
00003: /**
00004:  * An implementation of Boolean Predicates using BDDs.
00005:  * The functions which take arguments of type BoolPred may throw a
00006:  * ClassCastException if given an object that was not created by
00007:  * BoolPred.factory().
00008:  */
00009: public interface BoolPred {
00010:   public static BoolPred T = new True ();
00011:   public static BoolPred F = new False ();
00012:   public static BoolPredFactory factory = new BPFactory ();
00013:   public static BoolPredFunctions functions = new BPFunctions ();
00014:   
00015:   public BoolPred not  ();
00016:   public BoolPred and  (BoolPred p);
00017:   public BoolPred or   (BoolPred p);
00018:   public BoolPred xor  (BoolPred p);
00019:   public BoolPred impl (BoolPred p);
00020:   public BoolPred iff  (BoolPred p);
00021:   public BoolPred ite  (BoolPred p, BoolPred q);
00022:   
00023:   public String name();
00024: }
00025: 
00026: interface pBoolPred extends BoolPred, Comparable {
00027:   public String id();
00028:   public void initToGraphString();
00029:   public void toGraphString(StringBuffer b);
00030:   public int compareTo (Object that);
00031: }
00032: 
00033: // in the comparison order, T and F are biggest (and they are both bigger than each other!)
00034: class True implements pBoolPred {
00035:   public BoolPred not  ()           { return F; }
00036:   public BoolPred and  (BoolPred p) { return p; }
00037:   public BoolPred or   (BoolPred p) { return this; }
00038:   public BoolPred xor  (BoolPred p) { return p.not (); }
00039:   public BoolPred impl (BoolPred p) { return p; }
00040:   public BoolPred iff  (BoolPred p) { return p; }
00041:   public BoolPred ite  (BoolPred p, BoolPred q) { return p; }
00042:   
00043:   public String name()      { return "0"; }
00044:   public String id()        { return "0"; }
00045:   public String toString () { return "true"; }
00046:   
00047:   public int compareTo (Object that) { return 1; }
00048:   public void initToGraphString() {}
00049:   public void toGraphString(StringBuffer b) {}
00050: }
00051: 
00052: class False implements pBoolPred {
00053:   public BoolPred not  ()           { return T; }
00054:   public BoolPred and  (BoolPred p) { return this; }
00055:   public BoolPred or   (BoolPred p) { return p; }
00056:   public BoolPred xor  (BoolPred p) { return p; }
00057:   public BoolPred impl (BoolPred p) { return T; }
00058:   public BoolPred iff  (BoolPred p) { return p.not (); }
00059:   public BoolPred ite  (BoolPred p, BoolPred q) { return q; }
00060:   
00061:   public String name()      { return "1"; }
00062:   public String id()        { return "1"; }
00063:   public String toString () { return "false"; }
00064:   
00065:   public int compareTo (Object that) { return 1; }
00066:   public void initToGraphString() {}
00067:   public void toGraphString(StringBuffer b) {}
00068: }
00069: 
00070: class Cond implements pBoolPred {
00071:   private final String _id;
00072:   private final String _name;
00073:   final pBoolPred _t;
00074:   final pBoolPred _f; 
00075:   Cond (String id, String name, BoolPred t, BoolPred f) {
00076:     _id = id; _name = name; _t = (pBoolPred)t; _f = (pBoolPred)f;
00077:   }
00078:   
00079:   public final BoolPred not  ()           { return ite (F, T); }
00080:   public final BoolPred and  (BoolPred p) { return ite (p, F); }
00081:   public final BoolPred or   (BoolPred p) { return ite (T, p); }
00082:   public final BoolPred xor  (BoolPred p) { return ite (p.not (), p); }
00083:   public final BoolPred impl (BoolPred p) { return ite (p, T); }
00084:   public final BoolPred iff  (BoolPred p) { return ite (p, p.not ()); }
00085:   public final BoolPred ite  (BoolPred p, BoolPred q) {
00086:     return BPFactory.buildCond (this, (pBoolPred)p, (pBoolPred)q);
00087:   }
00088:   
00089:   public String name() { return _name; }
00090:   public String id() { return _id; }
00091:   public String toString () { 
00092:     if ( _t == T && _f == F) {
00093:       return _name;
00094:     } else if (_t == F && _f == T) {
00095:       return "!" + _name;
00096:     } else {
00097:       return "(" + _name + " ? " + _t + " : " + _f + ")";
00098:     }
00099:   }
00100:   
00101:   public int compareTo (Object that) { return _name.compareTo (((BoolPred)that).name()); }
00102:   
00103:   private boolean _printed = false;
00104:   public void initToGraphString() {
00105:     _printed=false;
00106:     _t.initToGraphString();
00107:     _f.initToGraphString();
00108:   }
00109:   public void toGraphString(StringBuffer b) {
00110:     if (!_printed) { b.append (id() + " ? " + _t.id() + " : " + _f.id() + "\n"); }
00111:     _printed = true; 
00112:     _t.toGraphString(b);
00113:     _f.toGraphString(b);
00114:   }
00115: }
00116: 
00117: 

file:simplebdd/bool/BoolPredFactory.java [source] [doc-public] [doc-private]
00001: package simplebdd.bool;
00002: 
00003: import simplebdd.util.HashMap3;
00004: 
00005: public interface BoolPredFactory {
00006:   public BoolPred buildVar (String name);
00007: }
00008: 
00009: class BPFactory implements BoolPredFactory {
00010:   private static final HashMap3 flyweight = new HashMap3 ();
00011:   private static int _COUNT = 0;
00012:   private static pBoolPred min(pBoolPred p1, pBoolPred p2, pBoolPred p3) {
00013:     pBoolPred result = p1;
00014:     if (p2.compareTo(result) < 0) { result =  p2; }
00015:     if (p3.compareTo(result) < 0) { result =  p3; }
00016:     return result;
00017:   }
00018:   static BoolPred buildCond (Cond b, pBoolPred p, pBoolPred q) {
00019:     BoolPred result = (pBoolPred)(flyweight.get (b, p, q));
00020:     if (result == null) {
00021:       // Since b is a Cond, n cannot be 0 or 1
00022:       // But b have the same name as p or q
00023:       String n = min(b, p, q).name();
00024:       // The following two lines assign t and f properly but are hard to read
00025:       // BoolPred t = (b.name()!=n ? b : b._t).ite((p.name()!=n ? p : ((Cond)p)._t), (q.name()!=n ? q : ((Cond)q)._t));
00026:       // BoolPred f = (b.name()!=n ? b : b._f).ite((p.name()!=n ? p : ((Cond)p)._f), (q.name()!=n ? q : ((Cond)q)._f));
00027:       BoolPred bt = (b.name() != n) ? b : b._t;
00028:       BoolPred bf = (b.name() != n) ? b : b._f;
00029:       BoolPred pt = (p.name() != n) ? p : ((Cond)p)._t;
00030:       BoolPred pf = (p.name() != n) ? p : ((Cond)p)._f;
00031:       BoolPred qt = (q.name() != n) ? q : ((Cond)q)._t;
00032:       BoolPred qf = (q.name() != n) ? q : ((Cond)q)._f;
00033:       BoolPred t = bt.ite(pt, qt);
00034:       BoolPred f = bf.ite(pf, qf);
00035:       if (t == f) {
00036:         result = t;
00037:       } else {
00038:         result = (BoolPred)(flyweight.get (n, t, f));
00039:         if (result == null) { 
00040:           result = new Cond (n + (++_COUNT), n, t, f);
00041:           flyweight.put (n, t, f, result);
00042:         }
00043:       }
00044:       flyweight.put (b, p, q, result);
00045:     }
00046:     return result;
00047:   }
00048:   public BoolPred buildVar (String name) {
00049:     BoolPred result = (BoolPred)(flyweight.get (name, BoolPred.T, BoolPred.F));
00050:     if (result == null) { 
00051:       result = new Cond (name + (++_COUNT), name, BoolPred.T, BoolPred.F);
00052:       flyweight.put (name, BoolPred.T, BoolPred.F, result);
00053:     }
00054:     return result;
00055:   }
00056: }
00057: 

file:simplebdd/bool/BoolPredFunctions.java [source] [doc-public] [doc-private]
00001: package simplebdd.bool;
00002: 
00003: public interface BoolPredFunctions {
00004:   public String toGraphString (BoolPred p);
00005: }
00006: 
00007: class BPFunctions implements BoolPredFunctions {
00008:   /** @throws ClassCastException if p is not created by BoolPred.factory() */
00009:   public String toGraphString (BoolPred p) {
00010:     ((pBoolPred)p).initToGraphString();
00011:     StringBuffer b = new StringBuffer();
00012:     ((pBoolPred)p).toGraphString(b);
00013:     return b.toString();
00014:   }
00015: }
00016: 

file:simplebdd/test/TestBool.java [source] [doc-public] [doc-private]
00001: package simplebdd.test;
00002: 
00003: import simplebdd.bool.BoolPred;
00004: 
00005: public class TestBool {
00006:   public static void main (String[] args) {
00007:     new TestBool().run ();
00008:   }
00009:   
00010:   final BoolPred x;
00011:   final BoolPred y;
00012:   final BoolPred z;
00013:   TestBool () {
00014:     this.x = BoolPred.factory.buildVar ("x");
00015:     this.y = BoolPred.factory.buildVar ("y");
00016:     this.z = BoolPred.factory.buildVar ("z");
00017:   }
00018:   
00019:   void runtest (String s, BoolPred p, boolean expectedValue) {
00020:     String trueString  = (expectedValue? "Good. " : "BAD!! ");
00021:     String falseString = (expectedValue? "BAD!! " : "Good. ");
00022:     if (p == BoolPred.T) {
00023:       System.out.println 
00024:         (trueString + s + " is always true");
00025:     } else {
00026:       System.out.println 
00027:         (falseString + s + " is sometimes false");
00028:     }
00029:   }
00030:   
00031:   public void run () {
00032:     System.out.println (BoolPred.T);
00033:     System.out.println (BoolPred.functions.toGraphString(BoolPred.T));
00034:     System.out.println (x);
00035:     System.out.println (BoolPred.functions.toGraphString(x));
00036:     System.out.println (x.not());
00037:     System.out.println (BoolPred.functions.toGraphString(x.not()));
00038:     System.out.println (x.ite(y,z));
00039:     System.out.println (BoolPred.functions.toGraphString(x.ite(y,z)));
00040:     System.out.println ("(y ? z : x)");
00041:     System.out.println (BoolPred.functions.toGraphString(y.ite(z,x)));
00042:     
00043:     System.out.println ("x xor y xor z");
00044:     System.out.println (BoolPred.functions.toGraphString(x.xor (y).xor (z)));
00045:     System.out.println ("x and x");
00046:     System.out.println (BoolPred.functions.toGraphString(x.and (x)));
00047:     System.out.println ("x or y");
00048:     System.out.println (BoolPred.functions.toGraphString(x.or (y)));
00049:     System.out.println ("y or x");
00050:     System.out.println (BoolPred.functions.toGraphString(y.or (x)));
00051:     
00052:     runtest (x.and (y) + "iff" + y.and (x),
00053:              x.and (y).iff (y.and (x)), true);
00054:     runtest ("", x.and (BoolPred.T).iff (x), true);
00055:     runtest ("", x.xor (y.xor (z)).iff (x.xor (y).xor (z)), true);
00056:   }
00057:   
00058: }
00059: 

Previous pageContentsNext page