#include <rrrBddManager.h>

Public Member Functions
lit	Bvar2Lit (bvar a) const

lit	Bvar2Lit (bvar a, bool c) const

bvar	Lit2Bvar (lit x) const

var	VarOfBvar (bvar a) const

lit	ThenOfBvar (bvar a) const

lit	ElseOfBvar (bvar a) const

ref	RefOfBvar (bvar a) const

lit	Const0 () const

lit	Const1 () const

bool	IsConst0 (lit x) const

bool	IsConst1 (lit x) const

lit	IthVar (var v) const

lit	LitRegular (lit x) const

lit	LitIrregular (lit x) const

lit	LitNot (lit x) const

lit	LitNotCond (lit x, bool c) const

bool	LitIsCompl (lit x) const

bool	LitIsEq (lit x, lit y) const

var	Var (lit x) const

var	Level (lit x) const

lit	Then (lit x) const

lit	Else (lit x) const

ref	Ref (lit x) const

double	OneCount (lit x) const

void	IncRef (lit x)

void	DecRef (lit x)

bool	Resize ()

void	ResizeUnique (var v)

bool	Gbc ()

	Man (int nVars_, Param p)

	~Man ()

void	Reorder ()

lit	And (lit x, lit y)

lit	Or (lit x, lit y)

void	SetRef (std::vector< lit > const &vLits)

void	RemoveRefIfUnused ()

void	TurnOnReo (int nReo_=0, std::vector< lit > const *vLits=NULL)

void	TurnOffReo ()

var	GetNumVars () const

void	GetOrdering (std::vector< int > &Var2Level_)

bvar	CountNodes ()

bvar	CountNodes (std::vector< lit > const &vLits)

void	PrintStats ()

unsigned long long	GetNumTotalCreatedNodes ()

Detailed Description

Definition at line 178 of file rrrBddManager.h.

Constructor & Destructor Documentation

◆ Man()

rrr::NewBdd::Man::Man	(	int	nVars_,
		Param	p )

inline

Definition at line 646 of file rrrBddManager.h.

                             {
      nCreatedTotal = 0;
      nVerbose = p.nVerbose;
      // parameter sanity check
      if(p.nObjsMaxLog < p.nObjsAllocLog)
        fatal_error("nObjsMax must not be smaller than nObjsAlloc");
      if(nVars_ >= (int)VarMax())
        fatal_error("Memout (nVars) in init");
      nVars = nVars_;
      lit nObjsMaxLit = (lit)1 << p.nObjsMaxLog;
      if(!nObjsMaxLit)
        fatal_error("Memout (nObjsMax) in init");
      if(nObjsMaxLit > (lit)BvarMax())
        nObjsMax = BvarMax();
      else
        nObjsMax = (bvar)nObjsMaxLit;
      lit nObjsAllocLit = (lit)1 << p.nObjsAllocLog;
      if(!nObjsAllocLit)
        fatal_error("Memout (nObjsAlloc) in init");
      if(nObjsAllocLit > (lit)BvarMax())
        nObjsAlloc = BvarMax();
      else
        nObjsAlloc = (bvar)nObjsAllocLit;
      if(nObjsAlloc <= (bvar)nVars)
        fatal_error("nObjsAlloc must be larger than nVars");
      uniq nUniqueSize = (uniq)1 << p.nUniqueSizeLog;
      if(!nUniqueSize)
        fatal_error("Memout (nUniqueSize) in init");
      // allocation
      if(nVerbose)
        std::cout << "Allocating " << nObjsAlloc << " nodes and " << nVars << " x " << nUniqueSize << " unique table entries" << std::endl;
      vVars.resize(nObjsAlloc);
      vObjs.resize((lit)nObjsAlloc * 2);
      vNexts.resize(nObjsAlloc);
      vMarks.resize(nObjsAlloc);
      vvUnique.resize(nVars);
      vUniqueMasks.resize(nVars);
      vUniqueCounts.resize(nVars);
      vUniqueTholds.resize(nVars);
      for(var v = 0; v < nVars; v++) {
        vvUnique[v].resize(nUniqueSize);
        vUniqueMasks[v] = nUniqueSize - 1;
        if((lit)(nUniqueSize * p.UniqueDensity) > (lit)BvarMax())
          vUniqueTholds[v] = BvarMax();
        else
          vUniqueTholds[v] = (bvar)(nUniqueSize * p.UniqueDensity);
      }
      if(p.fCountOnes) {
        if(nVars > 1023)
          fatal_error("nVars must be less than 1024 to count ones");
        vOneCounts.resize(nObjsAlloc);
      }
      // set up cache
      cache = new Cache(p.nCacheSizeLog, p.nCacheMaxLog, p.nCacheVerbose);
      // create nodes for variables
      nObjs = 1;
      vVars[0] = VarMax();
      for(var v = 0; v < nVars; v++)
        UniqueCreateInt(v, 1, 0);
      // set up variable order
      Var2Level.resize(nVars);
      Level2Var.resize(nVars);
      for(var v = 0; v < nVars; v++) {
        if(p.pVar2Level)
          Var2Level[v] = (*p.pVar2Level)[v];
        else
          Var2Level[v] = v;
        Level2Var[Var2Level[v]] = v;
      }
      // set other parameters
      RemovedHead = 0;
      nGbc = p.nGbc;
      nReo = p.nReo;
      MaxGrowth = p.MaxGrowth;
      fReoVerbose = p.fReoVerbose;
      if(nGbc || nReo != BvarMax())
        vRefs.resize(nObjsAlloc);
    }

◆ ~Man()

rrr::NewBdd::Man::~Man ( )

inline

Definition at line 724 of file rrrBddManager.h.

           {
      if(nVerbose) {
        std::cout << "Free " << nObjsAlloc << " nodes (" << nObjs << " live nodes)" << std::endl;
        std::cout << "Free {";
        std::string delim;
        for(var v = 0; v < nVars; v++) {
          std::cout << delim << vvUnique[v].size();
          delim = ", ";
        }
        std::cout << "} unique table entries" << std::endl;
        if(!vRefs.empty())
          std::cout << "Free " << vRefs.size() << " refs" << std::endl;
      }
      delete cache;
    }

Member Function Documentation

◆ And()

lit rrr::NewBdd::Man::And	(	lit	x,
		lit	y )

inline

Definition at line 750 of file rrrBddManager.h.

                                 {
      if(nObjs > nReo) {
        Reorder();
        while(nReo < nObjs) {
          nReo <<= 1;
          if((lit)nReo > (lit)BvarMax())
            nReo = BvarMax();
        }
      }
      return And_rec(x, y);
    }

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Bvar2Lit() [1/2]

lit rrr::NewBdd::Man::Bvar2Lit ( bvar a ) const

inline

Definition at line 207 of file rrrBddManager.h.

207{ return (lit)a << 1; }

Here is the caller graph for this function:

◆ Bvar2Lit() [2/2]

lit rrr::NewBdd::Man::Bvar2Lit	(	bvar	a,
		bool	c ) const

inline

Definition at line 208 of file rrrBddManager.h.

208{ return ((lit)a << 1) ^ (lit)c; }

◆ Const0()

lit rrr::NewBdd::Man::Const0 ( ) const

inline

Definition at line 214 of file rrrBddManager.h.

214{ return (lit)0; }

Here is the caller graph for this function:

◆ Const1()

lit rrr::NewBdd::Man::Const1 ( ) const

inline

Definition at line 215 of file rrrBddManager.h.

215{ return (lit)1; }

Here is the caller graph for this function:

◆ CountNodes() [1/2]

bvar rrr::NewBdd::Man::CountNodes ( )

inline

Definition at line 801 of file rrrBddManager.h.

                      {
      bvar count = 1;
      if(!vEdges.empty()) {
        for(bvar a = 1; a < nObjs; a++)
          if(EdgeOfBvar(a))
            count++;
        return count;
      }
      for(bvar a = 1; a <= (bvar)nVars; a++) {
        count++;
        SetMarkOfBvar(a);
      }
      for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
        if(RefOfBvar(a))
          count += CountNodes_rec(Bvar2Lit(a));
      for(bvar a = 1; a <= (bvar)nVars; a++)
        ResetMarkOfBvar(a);
      for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
        if(RefOfBvar(a))
          ResetMark_rec(Bvar2Lit(a));
      return count;
    }

Here is the call graph for this function:

Here is the caller graph for this function:

◆ CountNodes() [2/2]

bvar rrr::NewBdd::Man::CountNodes ( std::vector< lit > const & vLits )

inline

Definition at line 823 of file rrrBddManager.h.

                                                 {
      bvar count = 1;
      for(size_t i = 0; i < vLits.size(); i++)
        count += CountNodes_rec(vLits[i]);
      for(size_t i = 0; i < vLits.size(); i++)
        ResetMark_rec(vLits[i]);
      return count;
    }

◆ DecRef()

void rrr::NewBdd::Man::DecRef ( lit x )

inline

Definition at line 240 of file rrrBddManager.h.

240{ if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]--; }

rrr::NewBdd::Man::Lit2Bvar

bvar Lit2Bvar(lit x) const

Definition rrrBddManager.h:209

rrr::NewBdd::Man::Ref

ref Ref(lit x) const

Definition rrrBddManager.h:229

Here is the call graph for this function:

◆ Else()

lit rrr::NewBdd::Man::Else ( lit x ) const

inline

Definition at line 228 of file rrrBddManager.h.

228{ return LitNotCond(vObjs[LitIrregular(x)], LitIsCompl(x)); }

rrr::NewBdd::Man::LitNotCond

lit LitNotCond(lit x, bool c) const

Definition rrrBddManager.h:222

rrr::NewBdd::Man::LitIsCompl

bool LitIsCompl(lit x) const

Definition rrrBddManager.h:223

rrr::NewBdd::Man::LitIrregular

lit LitIrregular(lit x) const

Definition rrrBddManager.h:220

Here is the call graph for this function:

◆ ElseOfBvar()

lit rrr::NewBdd::Man::ElseOfBvar ( bvar a ) const

inline

Definition at line 212 of file rrrBddManager.h.

212{ return vObjs[Bvar2Lit(a, true)]; }

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gbc()

bool rrr::NewBdd::Man::Gbc ( )

inline

Definition at line 371 of file rrrBddManager.h.

               {
      if(nVerbose >= 2)
        std::cout << "Garbage collect" << std::endl;
      if(!vEdges.empty()) {
        for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
          if(!EdgeOfBvar(a) && VarOfBvar(a) != VarMax())
            RemoveBvar(a);
      } else {
        for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
          if(RefOfBvar(a))
            SetMark_rec(Bvar2Lit(a));
        for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
          if(!MarkOfBvar(a) && VarOfBvar(a) != VarMax())
            RemoveBvar(a);
        for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
          if(RefOfBvar(a))
            ResetMark_rec(Bvar2Lit(a));
      }
      cache->Clear();
      return RemovedHead;
    }

Here is the call graph for this function:

◆ GetNumTotalCreatedNodes()

unsigned long long rrr::NewBdd::Man::GetNumTotalCreatedNodes ( )

inline

Definition at line 846 of file rrrBddManager.h.

                                                 {
      return nCreatedTotal;
    }

◆ GetNumVars()

var rrr::NewBdd::Man::GetNumVars ( ) const

inline

Definition at line 793 of file rrrBddManager.h.

                           {
      return nVars;
    }

◆ GetOrdering()

void rrr::NewBdd::Man::GetOrdering ( std::vector< int > & Var2Level_ )

inline

Definition at line 796 of file rrrBddManager.h.

                                                 {
      Var2Level_.resize(nVars);
      for(var v = 0; v < nVars; v++)
        Var2Level_[v] = Var2Level[v];
    }

◆ IncRef()

void rrr::NewBdd::Man::IncRef ( lit x )

inline

Definition at line 239 of file rrrBddManager.h.

239{ if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]++; }

Here is the call graph for this function:

Here is the caller graph for this function:

◆ IsConst0()

bool rrr::NewBdd::Man::IsConst0 ( lit x ) const

inline

Definition at line 216 of file rrrBddManager.h.

216{ return x == Const0(); }

rrr::NewBdd::Man::Const0

lit Const0() const

Definition rrrBddManager.h:214

Here is the call graph for this function:

◆ IsConst1()

bool rrr::NewBdd::Man::IsConst1 ( lit x ) const

inline

Definition at line 217 of file rrrBddManager.h.

217{ return x == Const1(); }

rrr::NewBdd::Man::Const1

lit Const1() const

Definition rrrBddManager.h:215

Here is the call graph for this function:

◆ IthVar()

lit rrr::NewBdd::Man::IthVar ( var v ) const

inline

Definition at line 218 of file rrrBddManager.h.

218{ return Bvar2Lit((bvar)v + 1); }

Here is the call graph for this function:

◆ Level()

var rrr::NewBdd::Man::Level ( lit x ) const

inline

Definition at line 226 of file rrrBddManager.h.

226{ return Var2Level[Var(x)]; }

Var

int Var

Definition exorList.c:228

◆ Lit2Bvar()

bvar rrr::NewBdd::Man::Lit2Bvar ( lit x ) const

inline

Definition at line 209 of file rrrBddManager.h.

209{ return (bvar)(x >> 1); }

Here is the caller graph for this function:

◆ LitIrregular()

lit rrr::NewBdd::Man::LitIrregular ( lit x ) const

inline

Definition at line 220 of file rrrBddManager.h.

220{ return x | (lit)1; }

Here is the caller graph for this function:

◆ LitIsCompl()

bool rrr::NewBdd::Man::LitIsCompl ( lit x ) const

inline

Definition at line 223 of file rrrBddManager.h.

223{ return x & (lit)1; }

Here is the caller graph for this function:

◆ LitIsEq()

bool rrr::NewBdd::Man::LitIsEq	(	lit	x,
		lit	y ) const

inline

Definition at line 224 of file rrrBddManager.h.

224{ return x == y; }

◆ LitNot()

lit rrr::NewBdd::Man::LitNot ( lit x ) const

inline

Definition at line 221 of file rrrBddManager.h.

221{ return x ^ (lit)1; }

Here is the caller graph for this function:

◆ LitNotCond()

lit rrr::NewBdd::Man::LitNotCond	(	lit	x,
		bool	c ) const

inline

Definition at line 222 of file rrrBddManager.h.

222{ return x ^ (lit)c; }

Here is the caller graph for this function:

◆ LitRegular()

lit rrr::NewBdd::Man::LitRegular ( lit x ) const

inline

Definition at line 219 of file rrrBddManager.h.

219{ return x & ~(lit)1; }

Here is the caller graph for this function:

◆ OneCount()

double rrr::NewBdd::Man::OneCount ( lit x ) const

inline

Definition at line 230 of file rrrBddManager.h.

                                                {
      if(vOneCounts.empty())
        fatal_error("fCountOnes was not set");
      if(LitIsCompl(x))
        return std::pow(2.0, nVars) - vOneCounts[Lit2Bvar(x)];
      return vOneCounts[Lit2Bvar(x)];
    }

Here is the call graph for this function:

◆ Or()

lit rrr::NewBdd::Man::Or	(	lit	x,
		lit	y )

inline

Definition at line 761 of file rrrBddManager.h.

                                {
      return LitNot(And(LitNot(x), LitNot(y)));
    }

Here is the call graph for this function:

◆ PrintStats()

void rrr::NewBdd::Man::PrintStats ( )

inline

Definition at line 831 of file rrrBddManager.h.

                      {
      bvar nRemoved = 0;
      bvar a = RemovedHead;
      while(a)
        a = vNexts[a], nRemoved++;
      bvar nLive = 1;
      for(var v = 0; v < nVars; v++)
        nLive += vUniqueCounts[v];
      std::cout << "ref: " << std::setw(10) << (vRefs.empty()? 0: CountNodes()) << ", "
                << "used: " << std::setw(10) << nObjs << ", "
                << "live: " << std::setw(10) << nLive << ", "
                << "dead: " << std::setw(10) << nRemoved << ", "
                << "alloc: " << std::setw(10) << nObjsAlloc
                << std::endl;
    }

Here is the call graph for this function:

◆ Ref()

ref rrr::NewBdd::Man::Ref ( lit x ) const

inline

Definition at line 229 of file rrrBddManager.h.

229{ return vRefs[Lit2Bvar(x)]; }

Here is the call graph for this function:

Here is the caller graph for this function:

◆ RefOfBvar()

ref rrr::NewBdd::Man::RefOfBvar ( bvar a ) const

inline

Definition at line 213 of file rrrBddManager.h.

213{ return vRefs[a]; }

Here is the caller graph for this function:

◆ RemoveRefIfUnused()

void rrr::NewBdd::Man::RemoveRefIfUnused ( )

inline

Definition at line 772 of file rrrBddManager.h.

                             {
      if(!nGbc && nReo == BvarMax())
        vRefs.clear();
    }

◆ Reorder()

void rrr::NewBdd::Man::Reorder ( )

inline

Definition at line 739 of file rrrBddManager.h.

                   {
      if(nVerbose >= 2)
        std::cout << "Reorder" << std::endl;
      int nGbc_ = nGbc;
      nGbc = 0;
      CountEdges();
      Sift();
      vEdges.clear();
      cache->Clear();
      nGbc = nGbc_;
    }

Here is the caller graph for this function:

◆ Resize()

bool rrr::NewBdd::Man::Resize ( )

inline

Definition at line 314 of file rrrBddManager.h.

                  {
      if(nObjsAlloc == nObjsMax)
        return false;
      lit nObjsAllocLit = (lit)nObjsAlloc << 1;
      if(nObjsAllocLit > (lit)BvarMax())
        nObjsAlloc = BvarMax();
      else
        nObjsAlloc = (bvar)nObjsAllocLit;
      if(nVerbose >= 2)
        std::cout << "Reallocating " << nObjsAlloc << " nodes" << std::endl;
      vVars.resize(nObjsAlloc);
      vObjs.resize((lit)nObjsAlloc * 2);
      vNexts.resize(nObjsAlloc);
      vMarks.resize(nObjsAlloc);
      if(!vRefs.empty())
        vRefs.resize(nObjsAlloc);
      if(!vEdges.empty())
        vEdges.resize(nObjsAlloc);
      if(!vOneCounts.empty())
        vOneCounts.resize(nObjsAlloc);
      return true;
    }

◆ ResizeUnique()

void rrr::NewBdd::Man::ResizeUnique ( var v )

inline

Definition at line 336 of file rrrBddManager.h.

                             {
      uniq nUniqueSize, nUniqueSizeOld;
      nUniqueSize = nUniqueSizeOld = vvUnique[v].size();
      nUniqueSize <<= 1;
      if(!nUniqueSize) {
        vUniqueTholds[v] = BvarMax();
        return;
      }
      if(nVerbose >= 2)
        std::cout << "Reallocating " << nUniqueSize << " unique table entries for Var " << v << std::endl;
      vvUnique[v].resize(nUniqueSize);
      vUniqueMasks[v] = nUniqueSize - 1;
      for(uniq i = 0; i < nUniqueSizeOld; i++) {
        std::vector<bvar>::iterator q, tail, tail1, tail2;
        q = tail1 = vvUnique[v].begin() + i;
        tail2 = q + nUniqueSizeOld;
        while(*q) {
          uniq hash = UniqHash(ThenOfBvar(*q), ElseOfBvar(*q)) & vUniqueMasks[v];
          if(hash == i)
            tail = tail1;
          else
            tail = tail2;
          if(tail != q)
            *tail = *q, *q = 0;
          q = vNexts.begin() + *tail;
          if(tail == tail1)
            tail1 = q;
          else
            tail2 = q;
        }
      }
      vUniqueTholds[v] <<= 1;
      if((lit)vUniqueTholds[v] > (lit)BvarMax())
        vUniqueTholds[v] = BvarMax();
    }

Here is the call graph for this function:

◆ SetRef()

void rrr::NewBdd::Man::SetRef ( std::vector< lit > const & vLits )

inline

Definition at line 766 of file rrrBddManager.h.

                                             {
      vRefs.clear();
      vRefs.resize(nObjsAlloc);
      for(size_t i = 0; i < vLits.size(); i++)
        IncRef(vLits[i]);
    }

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Then()

lit rrr::NewBdd::Man::Then ( lit x ) const

inline

Definition at line 227 of file rrrBddManager.h.

227{ return LitNotCond(vObjs[LitRegular(x)], LitIsCompl(x)); }

rrr::NewBdd::Man::LitRegular

lit LitRegular(lit x) const

Definition rrrBddManager.h:219

Here is the call graph for this function:

◆ ThenOfBvar()

lit rrr::NewBdd::Man::ThenOfBvar ( bvar a ) const

inline

Definition at line 211 of file rrrBddManager.h.

211{ return vObjs[Bvar2Lit(a)]; }

Here is the call graph for this function:

Here is the caller graph for this function:

◆ TurnOffReo()

void rrr::NewBdd::Man::TurnOffReo ( )

inline

Definition at line 790 of file rrrBddManager.h.

                      {
      nReo = BvarMax();
    }

◆ TurnOnReo()

void rrr::NewBdd::Man::TurnOnReo	(	int	nReo_ = 0,
		std::vector< lit > const *	vLits = NULL )

inline

Definition at line 776 of file rrrBddManager.h.

                                                                      {
      if(nReo_)
        nReo = nReo_;
      else
        nReo = nObjs << 1;
      if((lit)nReo > (lit)BvarMax())
        nReo = BvarMax();
      if(vRefs.empty()) {
        if(vLits)
          SetRef(*vLits);
        else
          vRefs.resize(nObjsAlloc);
      }
    }

Here is the call graph for this function:

◆ Var()

var rrr::NewBdd::Man::Var ( lit x ) const

inline

Definition at line 225 of file rrrBddManager.h.

225{ return vVars[Lit2Bvar(x)]; }

Here is the call graph for this function:

◆ VarOfBvar()

var rrr::NewBdd::Man::VarOfBvar ( bvar a ) const

inline

Definition at line 210 of file rrrBddManager.h.

210{ return vVars[a]; }

Here is the caller graph for this function:

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

src/opt/rrr/rrrBddManager.h

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ Man()

◆ ~Man()

Member Function Documentation

◆ And()

◆ Bvar2Lit() [1/2]

◆ Bvar2Lit() [2/2]

◆ Const0()

◆ Const1()

◆ CountNodes() [1/2]

◆ CountNodes() [2/2]

◆ DecRef()

◆ Else()

◆ ElseOfBvar()

◆ Gbc()

◆ GetNumTotalCreatedNodes()

◆ GetNumVars()

◆ GetOrdering()

◆ IncRef()

◆ IsConst0()

◆ IsConst1()

◆ IthVar()

◆ Level()

◆ Lit2Bvar()

◆ LitIrregular()

◆ LitIsCompl()

◆ LitIsEq()

◆ LitNot()

◆ LitNotCond()

◆ LitRegular()

◆ OneCount()

◆ Or()

◆ PrintStats()

◆ Ref()

◆ RefOfBvar()

◆ RemoveRefIfUnused()

◆ Reorder()

◆ Resize()

◆ ResizeUnique()

◆ SetRef()

◆ Then()

◆ ThenOfBvar()

◆ TurnOffReo()

◆ TurnOnReo()

◆ Var()

◆ VarOfBvar()