SE547: BDDs: Bool Code [19/22]

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: