001package simplebdd.bool;
002
003import stdlib.HashMap3;
004
005public interface BoolPredFactory {
006        public BoolPred buildVar (String name);
007}
008
009class BPFactory implements BoolPredFactory {
010        private static final HashMap3 flyweight = new HashMap3 ();
011        private static int COUNT = 0;
012        private static pBoolPred min(pBoolPred p1, pBoolPred p2, pBoolPred p3) {
013                pBoolPred result = p1;
014                if (p2.compareTo(result) < 0) { result =  p2; }
015                if (p3.compareTo(result) < 0) { result =  p3; }
016                return result;
017        }
018        static BoolPred buildCond (Cond b, pBoolPred p, pBoolPred q) {
019                BoolPred result = (pBoolPred)(flyweight.get (b, p, q));
020                if (result == null) {
021                        // Since b is a Cond, n cannot be 0 or 1
022                        // But b have the same name as p or q
023                        String n = min(b, p, q).name();
024                        // The following two lines assign t and f properly but are hard to read
025                        // BoolPred t = (b.name()!=n ? b : b.t).ite((p.name()!=n ? p : ((Cond)p).t), (q.name()!=n ? q : ((Cond)q).t));
026                        // BoolPred f = (b.name()!=n ? b : b.f).ite((p.name()!=n ? p : ((Cond)p).f), (q.name()!=n ? q : ((Cond)q).f));
027                        BoolPred bt = (b.name() != n) ? b : b.t;
028                        BoolPred bf = (b.name() != n) ? b : b.f;
029                        BoolPred pt = (p.name() != n) ? p : ((Cond)p).t;
030                        BoolPred pf = (p.name() != n) ? p : ((Cond)p).f;
031                        BoolPred qt = (q.name() != n) ? q : ((Cond)q).t;
032                        BoolPred qf = (q.name() != n) ? q : ((Cond)q).f;
033                        BoolPred t = bt.ite(pt, qt);
034                        BoolPred f = bf.ite(pf, qf);
035                        if (t == f) {
036                                result = t;
037                        } else {
038                                result = (BoolPred)(flyweight.get (n, t, f));
039                                if (result == null) {
040                                        result = new Cond (n + (++COUNT), n, t, f);
041                                        flyweight.put (n, t, f, result);
042                                }
043                        }
044                        flyweight.put (b, p, q, result);
045                }
046                return result;
047        }
048        public BoolPred buildVar (String name) {
049                BoolPred result = (BoolPred)(flyweight.get (name, BoolPred.T, BoolPred.F));
050                if (result == null) {
051                        result = new Cond (name + (++COUNT), name, BoolPred.T, BoolPred.F);
052                        flyweight.put (name, BoolPred.T, BoolPred.F, result);
053                }
054                return result;
055        }
056}