lib-src/symbolic/bdd.cc

   1 #include <AD/symbolic/bdd.h>
   2 #include <AD/hash/lhash.h>
   3
   4 ///////////////////////////////////////////////////////////////////////////////
   5 //  Import some type definitions.
   6 ///////////////////////////////////////////////////////////////////////////////
   7 typedef BDDSet::Var     Var;
   8 typedef BDDSet::BDDNode BDDNode;
   9 typedef BDDSet::BDD     BDD;
  10 typedef BDDSet::Op      Op;
  11
  12 ///////////////////////////////////////////////////////////////////////////////
  13 //  Hashing and equality functions on a BDDNode
  14 ///////////////////////////////////////////////////////////////////////////////
  15 inline unsigned int hash(const BDDNode& n)
  16 {  return n.var + n.branches[0] * 4 + n.branches[1] * 32; }
  17
  18 inline Bool equal (const BDDNode& a, const BDDNode& b)
  19 {  return a.var == b.var && a.branches[0] == b.branches[0]
  20                          && a.branches[1] == b.branches[1];
  21 }
  22
  23 ///////////////////////////////////////////////////////////////////////////////
  24 //  The BDD table.
  25 ///////////////////////////////////////////////////////////////////////////////
  26 struct BDDTable : public LHashTable<BDDNode, BDD>
  27 {
  28 };
  29
  30 ///////////////////////////////////////////////////////////////////////////////
  31 //  The memo table.
  32 ///////////////////////////////////////////////////////////////////////////////
  33 struct BDDMemo : public LHashTable<BDDNode,BDD>
  34 {
  35 };
  36
  37 ///////////////////////////////////////////////////////////////////////////////
  38 //  Constructors
  39 ///////////////////////////////////////////////////////////////////////////////
  40 BDDSet:: BDDSet(size_t default_nodes)
  41    : bdd_roots(0),
  42      bdd_count(0),
  43      bdd_capacity(0),
  44      table(new BDDTable), memo(new BDDMemo)
  45    { bdds          = new BDDNode [default_nodes];
  46      bdd_next      = bdds + 2;
  47      int n         = default_nodes - 2;
  48      bdd_highwater = bdd_next + default_nodes;
  49      bdd_limit     = bdds + n / 2;
  50    }
  51
  52 ///////////////////////////////////////////////////////////////////////////////
  53 //  Destructor
  54 ///////////////////////////////////////////////////////////////////////////////
  55 BDDSet::~BDDSet()
  56 {  delete [] bdds;
  57    delete [] bdd_roots;
  58    delete table;
  59    delete memo;
  60 }
  61
  62 ///////////////////////////////////////////////////////////////////////////////
  63 //  Initialization
  64 ///////////////////////////////////////////////////////////////////////////////
  65 void BDDSet::clear()
  66 {  bdd_count = 0;
  67    bdd_next  = bdds + 2;
  68    memo->clear();
  69    table->clear();
  70 }
  71
  72 ///////////////////////////////////////////////////////////////////////////////
  73 //  Hash cons.
  74 ///////////////////////////////////////////////////////////////////////////////
  75 inline BDD BDDSet::hash_cons(Var v, BDD f, BDD g)
  76 {  if (bdd_next == bdd_limit) do_collect();  // garbage collect if full
  77    BDDNode n(v,f,g);
  78    Ix i = table->lookup(n);
  79    if (i) return table->value(i);
  80    BDDNode * next = bdd_next++;
  81    next->var = v;
  82    next->branches[0] = f;
  83    next->branches[1] = g;
  84    BDD h = next - bdds;
  85    table->insert(n,h);
  86    return h;
  87 }
  88
  89 ///////////////////////////////////////////////////////////////////////////////
  90 //  Application
  91 ///////////////////////////////////////////////////////////////////////////////
  92 BDD BDDSet::do_apply(Op op, BDD f, BDD g)
  93 {
  94    switch (op)
  95    {  case Or:   if (f == 1 || g == 1) return 1;
  96                  if (f == 0) return g;   // 0 + g = g
  97                  if (g == 0) return f;   // f + 0 = f
  98                  break;
  99       case And:  if (f == 0 || g == 0) return 0;
 100                  if (f == 1)  return g;   // 1 * g = g
 101                  if (g == 1)  return f;   // f * 1 = f
 102                  break;
 103       case Not:  return do_negate(f);
 104       case Nor:  if (f == 1 || g == 1) return 0;
 105                  if (f == 0) return do_negate(g);
 106                  if (g == 0) return do_negate(g);
 107                  break;
 108       case Nand: if (f == 0 || g == 0) return 1;
 109                  if (f == 1) return do_negate(g);
 110                  if (g == 1) return do_negate(g);
 111                  break;
 112       case Xor:  if (f == 0) return g;   // 0 xor g = g
 113                  if (g == 0) return f;   // f xor 0 = f
 114                  if (f == 1) return do_negate(g);
 115                  if (g == 1) return do_negate(f);
 116                  break;
 117       case Xnor: if (f == 0) return g;    // 1 xnor g = g
 118                  if (g == 0) return f;    // f xnor 1 = f
 119                  if (f == 1) return do_negate(g);
 120                  if (g == 1) return do_negate(f);
 121                  break;
 122       default: break;
 123    }
 124    // Check if result is already in place.
 125    BDDNode n(op, f, g);
 126    Ix i = memo->lookup(n);
 127    if (i) return memo->value(i);
 128
 129    register Var fv = var_of(f);
 130    register Var gv = var_of(g);
 131    BDD r;
 132    if (fv == gv)
 133       r = hash_cons(fv, do_apply(op,bdds[f].branches[0],bdds[g].branches[0]),
 134                         do_apply(op,bdds[f].branches[1],bdds[g].branches[1]));
 135    else if (fv < gv)
 136       r = hash_cons(fv, do_apply(op,bdds[f].branches[0],g),
 137                         do_apply(op,bdds[f].branches[1],g));
 138    else
 139       r = hash_cons(gv, do_apply(op,f,bdds[g].branches[0]),
 140                         do_apply(op,f,bdds[g].branches[1]));
 141
 142    memo->insert(n, r);  // update the memo map.
 143    return r;
 144 }
 145
 146 ///////////////////////////////////////////////////////////////////////////////
 147 //  Restriction
 148 ///////////////////////////////////////////////////////////////////////////////
 149 BDD BDDSet::do_restrict(BDD f, Var var, BDD value)
 150 {  if (f == 0) return 0;
 151    if (f == 1) return 1;
 152    Var fv = var_of(f);
 153    if (fv == var) return bdds[f].branches[value];
 154    BDDNode n(Restrict, f, var);
 155    Ix i = memo->lookup(n);
 156    if (i) return memo->value(i);
 157    BDD r = hash_cons(fv,do_restrict(bdds[f].branches[0], var, value),
 158                         do_restrict(bdds[f].branches[1], var, value));
 159    memo->insert(n,r);
 160    return r;
 161 }
 162
 163 ///////////////////////////////////////////////////////////////////////////////
 164 //  Negate
 165 ///////////////////////////////////////////////////////////////////////////////
 166 BDD BDDSet::do_negate (BDD f)
 167 {  if (f == 0) return 1;
 168    if (f == 1) return 0;
 169    BDDNode n(Not, f, 0);
 170    Ix i = memo->lookup(n);
 171    if (i) return memo->value(i);
 172    BDD r = hash_cons (var_of(f),
 173                       do_negate(bdds[f].branches[0]),
 174                       do_negate(bdds[f].branches[1]));
 175    memo->insert(n,r);
 176    return r;
 177 }
 178
 179 ///////////////////////////////////////////////////////////////////////////////
 180 //  Apply
 181 ///////////////////////////////////////////////////////////////////////////////
 182 BDD BDDSet::apply (Op op, BDD f, BDD g)
 183 {  memo->clear();
 184    bdd_last = bdd_next;
 185    return do_apply(op, f, g);
 186 }
 187
 188 ///////////////////////////////////////////////////////////////////////////////
 189 //  Restrict
 190 ///////////////////////////////////////////////////////////////////////////////
 191 BDD BDDSet::restrict (BDD f, Var var, BDD value)
 192 {  memo->clear();
 193    bdd_last = bdd_next;
 194    return do_restrict(f, var, value);
 195 }
 196
 197 ///////////////////////////////////////////////////////////////////////////////
 198 //  Negate
 199 ///////////////////////////////////////////////////////////////////////////////
 200 BDD BDDSet::negate (BDD f)
 201 {  memo->clear();
 202    bdd_last = bdd_next;
 203    return do_negate(f);
 204 }
 205
 206 ///////////////////////////////////////////////////////////////////////////////
 207 //  Top level method to involve garbage collection.
 208 ///////////////////////////////////////////////////////////////////////////////
 209 void BDDSet::collect()
 210 {  bdd_last = bdd_next;
 211    collect();
 212 }
 213
 214 ///////////////////////////////////////////////////////////////////////////////
 215 //  Garbage collection.
 216 ///////////////////////////////////////////////////////////////////////////////
 217 void BDDSet::do_collect()
 218 {
 219    // Mark all user roots
 220    for (int i = 0; i < size(); i++)
 221       ;
 222
 223    // Everything from [bdd_last ... bdd_limit) must be non-garbage.
 224    // Mark them.
 225    {  for (register BDDNode * p = bdd_last, * q = bdd_limit; p < q; p++);
 226    }
 227
 228    //
 229    // Copy phase, use the to space as a queue.
 230    //
 231
 232    //
 233    // Exchange from/to space.
 234    //
 235
 236 }