001package simplebdd.bool;
002
003/**
004 * An implementation of Boolean Predicates using BDDs.
005 * The functions which take arguments of type BoolPred may throw a
006 * ClassCastException if given an object that was not created by
007 * BoolPred.factory().
008 */
009public interface BoolPred {
010        public static BoolPred T = new True ();
011        public static BoolPred F = new False ();
012        public static BoolPredFactory factory = new BPFactory ();
013        public static BoolPredFunctions functions = new BPFunctions ();
014
015        public BoolPred not  ();
016        public BoolPred and  (BoolPred p);
017        public BoolPred or   (BoolPred p);
018        public BoolPred xor  (BoolPred p);
019        public BoolPred impl (BoolPred p);
020        public BoolPred iff  (BoolPred p);
021        public BoolPred ite  (BoolPred p, BoolPred q);
022
023        public String name();
024}
025
026interface pBoolPred extends BoolPred, Comparable<BoolPred> {
027        public String id();
028        public void initToGraphString();
029        public void toGraphString(StringBuilder b);
030        public int compareTo (BoolPred that);
031}
032
033// in the comparison order, T and F are biggest (and they are both bigger than each other!)
034class True implements pBoolPred {
035        public BoolPred not  ()           { return F; }
036        public BoolPred and  (BoolPred p) { return p; }
037        public BoolPred or   (BoolPred p) { return this; }
038        public BoolPred xor  (BoolPred p) { return p.not (); }
039        public BoolPred impl (BoolPred p) { return p; }
040        public BoolPred iff  (BoolPred p) { return p; }
041        public BoolPred ite  (BoolPred p, BoolPred q) { return p; }
042
043        public String name()      { return "0"; }
044        public String id()        { return "0"; }
045        public String toString () { return "true"; }
046
047        public int compareTo (BoolPred that) { return 1; }
048        public void initToGraphString() {}
049        public void toGraphString(StringBuilder b) {}
050}
051
052class False implements pBoolPred {
053        public BoolPred not  ()           { return T; }
054        public BoolPred and  (BoolPred p) { return this; }
055        public BoolPred or   (BoolPred p) { return p; }
056        public BoolPred xor  (BoolPred p) { return p; }
057        public BoolPred impl (BoolPred p) { return T; }
058        public BoolPred iff  (BoolPred p) { return p.not (); }
059        public BoolPred ite  (BoolPred p, BoolPred q) { return q; }
060
061        public String name()      { return "1"; }
062        public String id()        { return "1"; }
063        public String toString () { return "false"; }
064
065        public int compareTo (BoolPred that) { return 1; }
066        public void initToGraphString() {}
067        public void toGraphString(StringBuilder b) {}
068}
069
070class Cond implements pBoolPred {
071        private final String id;
072        private final String name;
073        final pBoolPred t;
074        final pBoolPred f;
075        Cond (String id, String name, BoolPred t, BoolPred f) {
076                this.id = id; this.name = name; this.t = (pBoolPred)t; this.f = (pBoolPred)f;
077        }
078
079        public final BoolPred not  ()           { return ite (F, T); }
080        public final BoolPred and  (BoolPred p) { return ite (p, F); }
081        public final BoolPred or   (BoolPred p) { return ite (T, p); }
082        public final BoolPred xor  (BoolPred p) { return ite (p.not (), p); }
083        public final BoolPred impl (BoolPred p) { return ite (p, T); }
084        public final BoolPred iff  (BoolPred p) { return ite (p, p.not ()); }
085        public final BoolPred ite  (BoolPred p, BoolPred q) {
086                return BPFactory.buildCond (this, (pBoolPred)p, (pBoolPred)q);
087        }
088
089        public String name() { return name; }
090        public String id() { return id; }
091        public String toString () {
092                if ( t == T && f == F) {
093                        return name;
094                } else if (t == F && f == T) {
095                        return "!" + name;
096                } else {
097                        return "(" + name + " ? " + t + " : " + f + ")";
098                }
099        }
100
101        public int compareTo (BoolPred that) { return name.compareTo (that.name()); }
102
103        private boolean printed = false;
104        public void initToGraphString() {
105                printed=false;
106                t.initToGraphString();
107                f.initToGraphString();
108        }
109        public void toGraphString(StringBuilder b) {
110                if (!printed) { b.append (id() + " ? " + t.id() + " : " + f.id() + "\n"); }
111                printed = true;
112                t.toGraphString(b);
113                f.toGraphString(b);
114        }
115}
116