include/AD/symbolic/bdd.h

   1 //////////////////////////////////////////////////////////////////////////////
   2 // NOTICE:
   3 //
   4 // ADLib, Prop and their related set of tools and documentation are in the
   5 // public domain.   The author(s) of this software reserve no copyrights on
   6 // the source code and any code generated using the tools.  You are encouraged
   7 // to use ADLib and Prop to develop software, in both academic and commercial
   8 // settings, and are free to incorporate any part of ADLib and Prop into
   9 // your programs.
  10 //
  11 // Although you are under no obligation to do so, we strongly recommend that
  12 // you give away all software developed using our tools.
  13 //
  14 // We also ask that credit be given to us when ADLib and/or Prop are used in
  15 // your programs, and that this notice be preserved intact in all the source
  16 // code.
  17 //
  18 // This software is still under development and we welcome any suggestions
  19 // and help from the users.
  20 //
  21 // Allen Leung
  22 // 1994
  23 //////////////////////////////////////////////////////////////////////////////
  24
  25 #ifndef binary_decision_diagrams_h
  26 #define binary_decision_diagrams_h
  27
  28 //////////////////////////////////////////////////////////////////////////////
  29 // Binary Decision Diagrams (BDD)\cite{bool-diag}
  30 // for computing boolean functions.   BDDs are maximally reduced
  31 // binary dag structure used to represent boolean functions.  A
  32 // BDD is characterized as follows:
  33 //   (a) A finite linear ordered set of boolean variable names $x_i$ are
  34 //       used to label each non-leaf node such that given two nodes
  35 //       $a$ and $b$, if $a$ is a descendent of $b$ then, $var(a) > var(b)$.
  36 //   (b) A leaf node is labeled either 0 or 1.
  37 //   (c) No node points to the same dag on both its branches.
  38 //   (d) No two subdags are isomorphic.  That is, all isomorphic
  39 //       subdags are merged.
  40 //
  41 // Class |BDDSet| represents a set of boolean functions, each one
  42 // is of type |BDDSet::BDD|.
  43 //////////////////////////////////////////////////////////////////////////////
  44
  45 #include <new.h>
  46 #include <AD/generic/generic.h>  // Generic definitions
  47
  48 //////////////////////////////////////////////////////////////////////////////
  49 //  Class BDDSet actually implements a collection of BDD's.  All BDD's
  50 //  must be allocated from the same system and operations are assumed to
  51 //  be performed on BDD's in the same system.
  52 //
  53 //  An BDDSet object manages the storage used during the BDDs computation.
  54 //  It performs internal garbage collection and compaction transparently
  55 //  from the client program.
  56 //////////////////////////////////////////////////////////////////////////////
  57
  58 class BDDSet {
  59
  60    BDDSet(const BDDSet&);            // no copy constructor
  61    void operator = (const BDDSet&);  // no assignment
  62
  63 public:
  64
  65    ///////////////////////////////////////////////////////////////////////////
  66    //  Type definitions.
  67    ///////////////////////////////////////////////////////////////////////////
  68    enum Op {                           // Binary boolean operations
  69       Not,                             // negation
  70       And,                             // conjunction
  71       Or,                              // disjunction
  72       Nor,                             //
  73       Nand,                            //
  74       Xor,                             // exclusive or
  75       Xnor,                            // exclusive nor
  76       Restrict
  77    };
  78    typedef int  Var;   // Function variable names
  79    typedef long BDD;   // a BDD
  80
  81    //  A BDD node.
  82    struct BDDNode
  83    {  Var var;                  // name of variable
  84       BDD branches[2];          // the two branches
  85       inline BDDNode() {}
  86       inline BDDNode(Var v, BDD l, BDD r)
  87          : var(v) { branches[0] = l; branches[1] = r; }
  88    };
  89
  90
  91 protected:
  92
  93    ///////////////////////////////////////////////////////////////////////////
  94    //  Given an BDD, we'll use 0 to denote the fixed encoding for the zero
  95    //  function and 1 to denote the one function.  This means that
  96    //  it is not possible to negate a function in constant time (but in
  97    //  linear time).  However,  with less sharing it is easier to
  98    //  perform garbage collection.
  99    //
 100    //  Allen.
 101    ///////////////////////////////////////////////////////////////////////////
 102
 103    ///////////////////////////////////////////////////////////////////////////
 104    //  Internal definitions.
 105    ///////////////////////////////////////////////////////////////////////////
 106    BDDNode  * bdds;            // array of bdds
 107    BDDNode  * bdd_next;        // next available node
 108    BDDNode  * bdd_limit;       // limit
 109    BDDNode  * bdd_highwater;   // highwater
 110    BDDNode  * bdd_last;        //
 111    BDD *      bdd_roots;       // roots
 112    int        bdd_count;       // number of bdds used
 113    int        bdd_capacity;    // capacity of the bdds array.
 114    class BDDTable * table;     // internal hash table.
 115    class BDDMemo  * memo;      // for memorization during computation.
 116
 117 public:
 118
 119    ////////////////////////////////////////////////////////////////////////
 120    //  Constructors and destructor.
 121    ////////////////////////////////////////////////////////////////////////
 122             BDDSet(size_t default_nodes = 1024);
 123    virtual ~BDDSet();
 124
 125    ////////////////////////////////////////////////////////////////////////
 126    //  Initialization
 127    ////////////////////////////////////////////////////////////////////////
 128    virtual void clear();
 129
 130    ////////////////////////////////////////////////////////////////////////
 131    //  Selectors
 132    ////////////////////////////////////////////////////////////////////////
 133    inline int size     () const      { return bdd_count; }
 134    inline int capacity () const      { return bdd_capacity; }
 135    inline Var var_of   (BDD f) const { return bdds[f].var; }
 136    inline const BDD * operator () (BDD f) const { return bdds[f].branches; }
 137
 138    ////////////////////////////////////////////////////////////////////////
 139    //  Roots in the set
 140    ////////////////////////////////////////////////////////////////////////
 141    inline BDD operator [] (int i) const { return bdd_roots[i]; }
 142    void kill (BDD f);  // delete f from the set
 143
 144    ////////////////////////////////////////////////////////////////////////
 145    //  Operations
 146    ////////////////////////////////////////////////////////////////////////
 147    virtual BDD apply    (Op op, BDD f, BDD g);
 148    virtual BDD restrict (BDD f, Var var, BDD value);
 149    virtual BDD negate   (BDD f);
 150
 151    ///////////////////////////////////////////////////////////////////////////
 152    //  Garbage collection
 153    ///////////////////////////////////////////////////////////////////////////
 154    virtual void collect(); // invoke garbage collection
 155
 156 private:
 157    ///////////////////////////////////////////////////////////////////////////
 158    //  Internals methods
 159    ///////////////////////////////////////////////////////////////////////////
 160    BDD  hash_cons   (Var v, BDD f, BDD g); // create a node
 161    BDD  do_apply    (Op op, BDD f, BDD g);
 162    BDD  do_restrict (BDD f, Var var, BDD value);
 163    BDD  do_negate   (BDD f);
 164    virtual void do_collect (); // garbage collection
 165    void add_root    (BDD f);
 166 };
 167
 168 #endif