#include <giaNewBdd.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 ()

Detailed Description

Definition at line 198 of file giaNewBdd.h.

Constructor & Destructor Documentation

◆ Man()

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

inline

Definition at line 664 of file giaNewBdd.h.

                             {
      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()

NewBdd::Man::~Man ( )

inline

Definition at line 741 of file giaNewBdd.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 NewBdd::Man::And	(	lit	x,
		lit	y )

inline

Definition at line 767 of file giaNewBdd.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 NewBdd::Man::Bvar2Lit ( bvar a ) const

inline

Definition at line 226 of file giaNewBdd.h.

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

Here is the caller graph for this function:

◆ Bvar2Lit() [2/2]

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

inline

Definition at line 227 of file giaNewBdd.h.

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

◆ Const0()

lit NewBdd::Man::Const0 ( ) const

inline

Definition at line 233 of file giaNewBdd.h.

233{ return (lit)0; }

Here is the caller graph for this function:

◆ Const1()

lit NewBdd::Man::Const1 ( ) const

inline

Definition at line 234 of file giaNewBdd.h.

234{ return (lit)1; }

Here is the caller graph for this function:

◆ CountNodes() [1/2]

bvar NewBdd::Man::CountNodes ( )

inline

Definition at line 818 of file giaNewBdd.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 NewBdd::Man::CountNodes ( std::vector< lit > const & vLits )

inline

Definition at line 840 of file giaNewBdd.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 NewBdd::Man::DecRef ( lit x )

inline

Definition at line 259 of file giaNewBdd.h.

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

NewBdd::Man::Lit2Bvar

bvar Lit2Bvar(lit x) const

Definition giaNewBdd.h:228

NewBdd::Man::Ref

ref Ref(lit x) const

Definition giaNewBdd.h:248

Here is the call graph for this function:

◆ Else()

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

inline

Definition at line 247 of file giaNewBdd.h.

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

NewBdd::Man::LitIsCompl

bool LitIsCompl(lit x) const

Definition giaNewBdd.h:242

NewBdd::Man::LitIrregular

lit LitIrregular(lit x) const

Definition giaNewBdd.h:239

NewBdd::Man::LitNotCond

lit LitNotCond(lit x, bool c) const

Definition giaNewBdd.h:241

Here is the call graph for this function:

◆ ElseOfBvar()

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

inline

Definition at line 231 of file giaNewBdd.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Gbc()

bool NewBdd::Man::Gbc ( )

inline

Definition at line 390 of file giaNewBdd.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:

◆ GetNumVars()

var NewBdd::Man::GetNumVars ( ) const

inline

Definition at line 810 of file giaNewBdd.h.

                           {
      return nVars;
    }

◆ GetOrdering()

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

inline

Definition at line 813 of file giaNewBdd.h.

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

◆ IncRef()

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

inline

Definition at line 258 of file giaNewBdd.h.

258{ 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 NewBdd::Man::IsConst0 ( lit x ) const

inline

Definition at line 235 of file giaNewBdd.h.

235{ return x == Const0(); }

NewBdd::Man::Const0

lit Const0() const

Definition giaNewBdd.h:233

Here is the call graph for this function:

◆ IsConst1()

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

inline

Definition at line 236 of file giaNewBdd.h.

236{ return x == Const1(); }

NewBdd::Man::Const1

lit Const1() const

Definition giaNewBdd.h:234

Here is the call graph for this function:

◆ IthVar()

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

inline

Definition at line 237 of file giaNewBdd.h.

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

Here is the call graph for this function:

◆ Level()

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

inline

Definition at line 245 of file giaNewBdd.h.

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

Var

int Var

Definition exorList.c:228

◆ Lit2Bvar()

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

inline

Definition at line 228 of file giaNewBdd.h.

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

Here is the caller graph for this function:

◆ LitIrregular()

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

inline

Definition at line 239 of file giaNewBdd.h.

239{ return x | (lit)1; }

Here is the caller graph for this function:

◆ LitIsCompl()

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

inline

Definition at line 242 of file giaNewBdd.h.

242{ return x & (lit)1; }

Here is the caller graph for this function:

◆ LitIsEq()

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

inline

Definition at line 243 of file giaNewBdd.h.

243{ return x == y; }

◆ LitNot()

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

inline

Definition at line 240 of file giaNewBdd.h.

240{ return x ^ (lit)1; }

Here is the caller graph for this function:

◆ LitNotCond()

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

inline

Definition at line 241 of file giaNewBdd.h.

241{ return x ^ (lit)c; }

Here is the caller graph for this function:

◆ LitRegular()

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

inline

Definition at line 238 of file giaNewBdd.h.

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

Here is the caller graph for this function:

◆ OneCount()

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

inline

Definition at line 249 of file giaNewBdd.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 NewBdd::Man::Or	(	lit	x,
		lit	y )

inline

Definition at line 778 of file giaNewBdd.h.

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

Here is the call graph for this function:

◆ PrintStats()

void NewBdd::Man::PrintStats ( )

inline

Definition at line 848 of file giaNewBdd.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 NewBdd::Man::Ref ( lit x ) const

inline

Definition at line 248 of file giaNewBdd.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ RefOfBvar()

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

inline

Definition at line 232 of file giaNewBdd.h.

232{ return vRefs[a]; }

Here is the caller graph for this function:

◆ RemoveRefIfUnused()

void NewBdd::Man::RemoveRefIfUnused ( )

inline

Definition at line 789 of file giaNewBdd.h.

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

◆ Reorder()

void NewBdd::Man::Reorder ( )

inline

Definition at line 756 of file giaNewBdd.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 NewBdd::Man::Resize ( )

inline

Definition at line 333 of file giaNewBdd.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 NewBdd::Man::ResizeUnique ( var v )

inline

Definition at line 355 of file giaNewBdd.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 NewBdd::Man::SetRef ( std::vector< lit > const & vLits )

inline

Definition at line 783 of file giaNewBdd.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 NewBdd::Man::Then ( lit x ) const

inline

Definition at line 246 of file giaNewBdd.h.

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

NewBdd::Man::LitRegular

lit LitRegular(lit x) const

Definition giaNewBdd.h:238

Here is the call graph for this function:

◆ ThenOfBvar()

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

inline

Definition at line 230 of file giaNewBdd.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ TurnOffReo()

void NewBdd::Man::TurnOffReo ( )

inline

Definition at line 807 of file giaNewBdd.h.

                      {
      nReo = BvarMax();
    }

◆ TurnOnReo()

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

inline

Definition at line 793 of file giaNewBdd.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 NewBdd::Man::Var ( lit x ) const

inline

Definition at line 244 of file giaNewBdd.h.

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

Here is the call graph for this function:

◆ VarOfBvar()

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

inline

Definition at line 229 of file giaNewBdd.h.

229{ return vVars[a]; }

Here is the caller graph for this function:

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

src/aig/gia/giaNewBdd.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()

◆ 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()