bddBdd.h

Go to the documentation of this file.

/*
 * CrocoPat is a tool for relational programming.
 * This file is part of CrocoPat. 
 *
 * Copyright (C) 2002-2008  Dirk Beyer
 *
 * CrocoPat is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public License
 * as published by the Free Software Foundation; either
 * version 2.1 of the License, or (at your option) any later version.
 *
 * CrocoPat is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public License
 * along with CrocoPat; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 *
 * Please find the GNU Lesser General Public License in file
 * License_LGPL.txt or at http://www.gnu.org/licenses/lgpl.txt
 *
 * Author:
 * Dirk Beyer (firstname.lastname@sfu.ca)
 * Simon Fraser University
 *
 * With contributions of: Andreas Noack, Michael Vogel
 */

#ifndef _bddBdd_h
#define _bddBdd_h

#include "relObject.h"

#include <vector>
#include <set>
#include <map>
#include <cassert>

struct bddNode 
{
  unsigned mark:1;
  unsigned var:31; 
  unsigned low;    
  unsigned high;
  unsigned next;
};

struct bddBinEntry 
{  
  unsigned op;     
  unsigned root1;
  unsigned root2;
  unsigned result;
};

struct bddStatEntry 
{
  unsigned root;
  double result;  
};

struct bddGraphNode
{
  unsigned id;
  unsigned var;
  unsigned low;
  unsigned high;
};

class bddBdd : private relObject
{
private: // Constants.

  enum { mComplement = 1, mRenameVars, mExists,
         mUnite, mIntersect, mSetContains };

private: // Static attributes.

  static bddNode* mNodes;
  static unsigned mMaxNodeNr;
  static unsigned mFree;

  static multiset<unsigned> mExtRefs;

  static unsigned* mUniqueHash;
  static unsigned mUniqueHBitNr;
  static bddBinEntry* mBinCache;
  static unsigned mBinCBitNr;
  static bddStatEntry* mStatCache;
  static unsigned mStatCBitNr;

  static unsigned mRenameCnt; // = 0;

private: // Private static methods.

  static inline unsigned 
  hash(unsigned p1, unsigned pHashBitNr);
  static inline unsigned 
  hash(unsigned p1, unsigned p2, unsigned p3, unsigned pHashBitNr);
  static inline void 
  normalize(unsigned& p1, unsigned& p2);

  static void 
  mark(unsigned pRoot);
  static void 
  unMark(unsigned pRoot);

  static void 
  gc();

  static unsigned 
  insert(unsigned pVar, unsigned pLow, unsigned pHigh);

  bool
  testVars_(unsigned pRoot, 
            unsigned pVarIdFirst, 
            unsigned pVarIdLast);
  static double 
  getTupleNr_(unsigned pRoot, unsigned pVar, unsigned pMaxVar);
  static unsigned 
  getTuple_(unsigned pRoot, unsigned pVar, unsigned pMaxVar);
  static unsigned 
  getNodeNr_(unsigned pRoot);
  static void
  getNodesPerVarId_(unsigned pRoot, 
                    map<unsigned, unsigned>& pBddNodesPerVar);
  static void
  getGraph_(unsigned pRoot, 
            multimap<unsigned,bddGraphNode>& pGraph);
  static void 
  print_(ostream& pS, unsigned pRoot);
  
  static bool 
  setContains_(unsigned pRoot1, unsigned pRoot2);

  static unsigned 
  complement_(unsigned pRoot);
  static unsigned 
  unite_(unsigned pRoot1, unsigned pRoot2);
  static unsigned 
  intersect_(unsigned pRoot1, unsigned pRoot2);
  static unsigned 
  exists_(unsigned pRoot, unsigned pVar);
  static unsigned 
  renameVars_(unsigned pRoot, 
              unsigned pFirst, 
              unsigned pLast, 
              int      pOffset);

public: // Public static methods.

  static void
  init(unsigned pMaxNodeNr, 
    unsigned pUniqueHBitNr, unsigned pBinCBitNr, unsigned pStatCBitNr);
  static void done ();

  static unsigned 
  getReachNodeNr();
  static unsigned 
  getExtRefNr();

  static void 
  analyseUniqueHash ();

private: // Attributes.

  unsigned mRoot;

private: // Private methods.

  inline void decRef() 
  {
    if(mRoot != 0 && mRoot != 1)
    {
      multiset<unsigned>::iterator lDelete = mExtRefs.find(mRoot);
      // Otherwise error in external BDD references.
      assert(lDelete != mExtRefs.end());
      mExtRefs.erase(lDelete);
    }
  }

  inline void incRef() 
  {
    if(mRoot != 0 && mRoot != 1)
    {
      mExtRefs.insert(mRoot);
    }
  }

public: // Constructors and destructor.

  bddBdd(unsigned pRoot = 0) 
  {
    mRoot = pRoot;
    incRef();
  }

  bddBdd(const bddBdd& pBdd) 
  {
    mRoot = pBdd.mRoot;
    incRef();
  }

  bddBdd (unsigned pVarId, bool pValue);
  static unsigned 
  bddBdd_(unsigned pVarId, bool pValue);

  bddBdd (unsigned pVarId, unsigned pBitNr, unsigned pValue);
  static unsigned 
  bddBdd_(unsigned pVarId, unsigned pBitNr, unsigned pValue);

  bddBdd (unsigned pVarId1, unsigned pVarId2);
  static unsigned 
  bddBdd_(unsigned pVarId1, unsigned pVarId2);
  
  ~bddBdd() 
  {
    decRef();
  }

  bddBdd& 
  operator=(const bddBdd& aBdd);

  static bddBdd
  mkLessEqual (unsigned pVarId, unsigned pBitNr, unsigned pValue);
  static unsigned 
  mkLessEqual_(unsigned pVarId, unsigned pBitNr, unsigned pValue);

public: // Accessors.

  bool
  testVars(unsigned pVarIdFirst, unsigned pVarIdLast)
  {
    bool lResult = testVars_(mRoot, pVarIdFirst, pVarIdLast);
    unMark(mRoot);
    return lResult;
  }

  double
  getTupleNr(unsigned pMinVar, unsigned pMaxVar) const
  { return getTupleNr_(mRoot, pMinVar, pMaxVar); }

  unsigned
  getTuple(unsigned pMinVar, unsigned pMaxVar) const
  {
    assert(!isEmpty());
    return getTuple_(mRoot, pMinVar, pMaxVar); 
  }

  unsigned 
  getNodeNr() const;

  unsigned
  getFreeNodeNr() const;

  unsigned
  getMaxNodeNr() const
  { return mMaxNodeNr; }

  map<unsigned, unsigned>
  getNodesPerVarId() const
  { map<unsigned, unsigned> lBddNodesPerVar;
    getNodesPerVarId_(mRoot, lBddNodesPerVar);
    unMark(mRoot);
    return lBddNodesPerVar;  }

  void
  getGraph(multimap<unsigned,bddGraphNode>& pGraph) const 
  { getGraph_(mRoot, pGraph);
    unMark(mRoot);  }

  void 
  print(ostream& pS) const
  { print_(pS, mRoot);
    cout << endl;  }
  
public: // Service methods.

  bool 
  setEqual(const bddBdd& pBdd) const
  { return mRoot == pBdd.mRoot; }
  
  bool 
  setContains(const bddBdd& pBdd) const
  { return setContains_(mRoot, pBdd.mRoot); }

  bool 
  isEmpty() const
  { return mRoot == 0; }



  void 
  complement();

  void 
  unite(const bddBdd& pBdd);

  void 
  intersect(const bddBdd& pBdd);

  void 
  exists(unsigned pVar);

  void 
  renameVars(unsigned pFirst, unsigned pLast, int pOffset);
};

#endif

---