rrr::NewBdd::Cache Class Reference

#include <rrrBddManager.h>

Public Member Functions
	Cache (int nCacheSizeLog, int nCacheMaxLog, int nVerbose)
	~Cache ()
lit	Lookup (lit x, lit y)
void	Insert (lit x, lit y, lit z)
void	Clear ()
void	Resize ()

Detailed Description

Definition at line 36 of file rrrBddManager.h.

Constructor & Destructor Documentation

Cache()

rrr::NewBdd::Cache::Cache ( int nCacheSizeLog, int nCacheMaxLog, int nVerbose )

inline

Definition at line 49 of file rrrBddManager.h.

                                                            : nVerbose(nVerbose) {
      if(nCacheMaxLog < nCacheSizeLog)
        fatal_error("nCacheMax must not be smaller than nCacheSize");
      nMax = (cac)1 << nCacheMaxLog;
      if(!(nMax << 1))
        fatal_error("Memout (nCacheMax) in init");
      nSize = (cac)1 << nCacheSizeLog;
      if(nVerbose)
        std::cout << "Allocating " << nSize << " cache entries" << std::endl;
      vCache.resize(nSize * 3);
      Mask = nSize - 1;
      nLookups = 0;
      nHits = 0;
      nThold = (nSize == nMax)? SizeMax(): nSize;
      HitRate = 1;
    }

~Cache()

rrr::NewBdd::Cache::~Cache ( )

inline

Definition at line 65 of file rrrBddManager.h.

             {
      if(nVerbose)
        std::cout << "Free " << nSize << " cache entries" << std::endl;
    }

Member Function Documentation

Clear()

void rrr::NewBdd::Cache::Clear ( )

inline

Definition at line 116 of file rrrBddManager.h.

                        {
      std::fill(vCache.begin(), vCache.end(), 0);
    }

Insert()

void rrr::NewBdd::Cache::Insert ( lit x, lit y, lit z )

inline

Definition at line 103 of file rrrBddManager.h.

                                            {
      cac i = (CacHash(x, y) & Mask) * 3;
      vCache[i] = x;
      vCache[i + 1] = y;
      vCache[i + 2] = z;
      if(nVerbose >= 3)
        std::cout << "Cache ent: "
                  << "x = " << std::setw(10) << x << ", "
                  << "y = " << std::setw(10) << y << ", "
                  << "z = " << std::setw(10) << z << ", "
                  << "hash = " << std::hex << (CacHash(x, y) & Mask) << std::dec
                  << std::endl;
    }

Lookup()

lit rrr::NewBdd::Cache::Lookup ( lit x, lit y )

inline

Definition at line 69 of file rrrBddManager.h.

                                    {
      nLookups++;
      if(nLookups > nThold) {
        double NewHitRate = (double)nHits / nLookups;
        if(nVerbose >= 2)
          std::cout << "Cache Hits: " << std::setw(10) << nHits << ", "
                    << "Lookups: " << std::setw(10) << nLookups << ", "
                    << "Rate: " << std::setw(10) << NewHitRate
                    << std::endl;
        if(NewHitRate > HitRate)
          Resize();
        if(nSize == nMax)
          nThold = SizeMax();
        else {
          nThold <<= 1;
          if(!nThold)
            nThold = SizeMax();
        }
        HitRate = NewHitRate;
      }
      cac i = (CacHash(x, y) & Mask) * 3;
      if(vCache[i] == x && vCache[i + 1] == y) {
        if(nVerbose >= 3)
          std::cout << "Cache hit: "
                    << "x = " << std::setw(10) << x << ", "
                    << "y = " << std::setw(10) << y << ", "
                    << "z = " << std::setw(10) << vCache[i + 2] << ", "
                    << "hash = " << std::hex << (CacHash(x, y) & Mask) << std::dec
                    << std::endl;
        nHits++;
        return vCache[i + 2];
      }
      return LitMax();
    }

Here is the call graph for this function:

Resize()

void rrr::NewBdd::Cache::Resize ( )

inline

Definition at line 119 of file rrrBddManager.h.

                  {
      cac nSizeOld = nSize;
      nSize <<= 1;
      if(nVerbose >= 2)
        std::cout << "Reallocating " << nSize << " cache entries" << std::endl;
      vCache.resize(nSize * 3);
      Mask = nSize - 1;
      for(cac j = 0; j < nSizeOld; j++) {
        cac i = j * 3;
        if(vCache[i] || vCache[i + 1]) {
          cac hash = (CacHash(vCache[i], vCache[i + 1]) & Mask) * 3;
          vCache[hash] = vCache[i];
          vCache[hash + 1] = vCache[i + 1];
          vCache[hash + 2] = vCache[i + 2];
          if(nVerbose >= 3)
            std::cout << "Cache mov: "
                      << "x = " << std::setw(10) << vCache[i] << ", "
                      << "y = " << std::setw(10) << vCache[i + 1] << ", "
                      << "z = " << std::setw(10) << vCache[i + 2] << ", "
                      << "hash = " << std::hex << (CacHash(vCache[i], vCache[i + 1]) & Mask) << std::dec
                      << std::endl;
        }
      }
    }

Here is the caller graph for this function:

---

The documentation for this class was generated from the following file:

• src/opt/rrr/rrrBddManager.h