#include <giaNewTt.h>

Public Member Functions
lit	Bvar2Lit (bvar a) const

bvar	Lit2Bvar (lit x) const

lit	IthVar (int v) const

lit	LitNot (lit x) const

lit	LitNotCond (lit x, bool c) const

bool	LitIsCompl (lit x) const

ref	Ref (lit x) const

lit	Const0 () const

lit	Const1 () const

bool	IsConst0 (lit x) const

bool	IsConst1 (lit x) const

bool	LitIsEq (lit x, lit y) const

size	OneCount (lit x) const

void	IncRef (lit x)

void	DecRef (lit x)

bool	Resize ()

bool	Gbc ()

	Man (int nVars, Param p)

lit	And (lit x, lit y)

lit	Or (lit x, lit y)

void	Reorder ()

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

void	RemoveRefIfUnused ()

void	TurnOffReo ()

int	GetNumVars () const

void	PrintNode (lit x) const

Detailed Description

Definition at line 68 of file giaNewTt.h.

Constructor & Destructor Documentation

◆ Man()

NewTt::Man::Man	(	int	nVars,
		Param	p )

inline

Definition at line 189 of file giaNewTt.h.

                           : nVars(nVars) {
      if(p.nObjsMaxLog < p.nObjsAllocLog)
        fatal_error("nObjsMax must not be smaller than nObjsAlloc");
      if(nVars >= lww())
        nSize = 1ull << (nVars - lww());
      else
        nSize = 1;
      if(!nSize)
        fatal_error("Memout (nVars) in init");
      if(!(nSize << p.nObjsMaxLog))
        fatal_error("Memout (nObjsMax) in init");
      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");
      nTotalSize = nSize << p.nObjsAllocLog;
      vVals.resize(nTotalSize);
      if(p.fCountOnes && nVars > 63)
        fatal_error("nVars must be less than 64 to count ones");
      nObjs = 1;
      for(int i = 0; i < 6 && i < nVars; i++) {
        for(size j = 0; j < nSize; j++)
          vVals[nSize * nObjs + j] = vars(i);
        nObjs++;
      }
      for(int i = 0; i < nVars - 6; i++) {
        for(size j = 0; j < nSize; j += (2ull << i))
          for(size k = 0; k < (1ull << i); k++)
            vVals[nSize * nObjs + j + k] = one();
        nObjs++;
      }
      nVerbose = p.nVerbose;
      nGbc = p.nGbc;
      if(nGbc || p.nReo != BvarMax())
        vRefs.resize(nObjsAlloc);
    }

Member Function Documentation

◆ And()

lit NewTt::Man::And	(	lit	x,
		lit	y )

inline

Definition at line 237 of file giaNewTt.h.

                                 {
      bvar xvar = Lit2Bvar(x);
      bvar yvar = Lit2Bvar(y);
      word xcompl = LitIsCompl(x)? one(): 0;
      word ycompl = LitIsCompl(y)? one(): 0;
      unsigned j;
      if(nObjs >= nObjsAlloc && vDeads.empty()) {
        bool fRemoved = false;
        if(nGbc > 1)
          fRemoved = Gbc();
        if(!Resize() && !fRemoved && (nGbc != 1 || !Gbc()))
          fatal_error("Memout (node)");
      }
      bvar zvar;
      if(nObjs < nObjsAlloc)
        zvar = nObjs++;
      else
        zvar = vDeads.back(), vDeads.resize(vDeads.size() - 1);
      for(j = 0; j < nSize; j++)
        vVals[nSize * zvar + j] = (vVals[nSize * xvar + j] ^ xcompl) & (vVals[nSize * yvar + j] ^ ycompl);
      return zvar << 1;
    }

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Bvar2Lit()

lit NewTt::Man::Bvar2Lit ( bvar a ) const

inline

Definition at line 109 of file giaNewTt.h.

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

◆ Const0()

lit NewTt::Man::Const0 ( ) const

inline

Definition at line 116 of file giaNewTt.h.

116{ return (lit)0; }

◆ Const1()

lit NewTt::Man::Const1 ( ) const

inline

Definition at line 117 of file giaNewTt.h.

117{ return (lit)1; }

◆ DecRef()

void NewTt::Man::DecRef ( lit x )

inline

Definition at line 160 of file giaNewTt.h.

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

NewTt::Man::Ref

ref Ref(lit x) const

Definition giaNewTt.h:115

Here is the call graph for this function:

◆ Gbc()

bool NewTt::Man::Gbc ( )

inline

Definition at line 179 of file giaNewTt.h.

               {
      if(nVerbose >= 2)
        std::cout << "Garbage collect" << std::endl;
      for(bvar a = nVars + 1; a < nObjs; a++)
        if(!vRefs[a])
          vDeads.push_back(a);
      return vDeads.size();
    }

Here is the caller graph for this function:

◆ GetNumVars()

int NewTt::Man::GetNumVars ( ) const

inline

Definition at line 276 of file giaNewTt.h.

                           {
      return nVars;
    }

◆ IncRef()

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

inline

Definition at line 159 of file giaNewTt.h.

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

inline

Definition at line 118 of file giaNewTt.h.

                                                {
      bvar a = Lit2Bvar(x);
      word c = LitIsCompl(x)? one(): 0;
      for(size j = 0; j < nSize; j++)
        if(vVals[nSize * a + j] ^ c)
          return false;
      return true;
    }

Here is the call graph for this function:

◆ IsConst1()

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

inline

Definition at line 126 of file giaNewTt.h.

                                                {
      bvar a = Lit2Bvar(x);
      word c = LitIsCompl(x)? one(): 0;
      for(size j = 0; j < nSize; j++)
        if(~(vVals[nSize * a + j] ^ c))
          return false;
      return true;
    }

Here is the call graph for this function:

◆ IthVar()

lit NewTt::Man::IthVar ( int v ) const

inline

Definition at line 111 of file giaNewTt.h.

111{ return ((lit)v + 1) << 1; }

◆ Lit2Bvar()

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

inline

Definition at line 110 of file giaNewTt.h.

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

Here is the caller graph for this function:

◆ LitIsCompl()

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

inline

Definition at line 114 of file giaNewTt.h.

114{ return x & (lit)1; }

Here is the caller graph for this function:

◆ LitIsEq()

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

inline

Definition at line 134 of file giaNewTt.h.

                                                {
      if(x == y)
        return true;
      if(x == LitMax() || y == LitMax())
        return false;
      bvar xvar = Lit2Bvar(x);
      bvar yvar = Lit2Bvar(y);
      word c = LitIsCompl(x) ^ LitIsCompl(y)? one(): 0;
      for(size j = 0; j < nSize; j++)
        if(vVals[nSize * xvar + j] ^ vVals[nSize * yvar + j] ^ c)
          return false;
      return true;
    }

Here is the call graph for this function:

◆ LitNot()

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

inline

Definition at line 112 of file giaNewTt.h.

112{ return x ^ (lit)1; }

Here is the caller graph for this function:

◆ LitNotCond()

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

inline

Definition at line 113 of file giaNewTt.h.

113{ return x ^ (lit)c; }

◆ OneCount()

size NewTt::Man::OneCount ( lit x ) const

inline

Definition at line 147 of file giaNewTt.h.

                                                {
      bvar a = Lit2Bvar(x);
      size count = 0;
      if(nVars > 6) {
        for(size j = 0; j < nSize; j++)
          count += bsw(vVals[nSize * a + j]).count();
      } else
        count = bsw(vVals[nSize * a] & ones(nVars)).count();
      return LitIsCompl(x)? ((size)1 << nVars) - count: count;
    }

Here is the call graph for this function:

◆ Or()

lit NewTt::Man::Or	(	lit	x,
		lit	y )

inline

Definition at line 259 of file giaNewTt.h.

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

Here is the call graph for this function:

◆ PrintNode()

void NewTt::Man::PrintNode ( lit x ) const

inline

Definition at line 279 of file giaNewTt.h.

                                {
      bvar a = Lit2Bvar(x);
      word c = LitIsCompl(x)? one(): 0;
      for(size j = 0; j < nSize; j++)
        std::cout << bsw(vVals[nSize * a + j] ^ c);
      std::cout << std::endl;
    }

Here is the call graph for this function:

◆ Ref()

ref NewTt::Man::Ref ( lit x ) const

inline

Definition at line 115 of file giaNewTt.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ RemoveRefIfUnused()

void NewTt::Man::RemoveRefIfUnused ( )

inline

Definition at line 271 of file giaNewTt.h.

                             {
      if(!nGbc)
        vRefs.clear();
    }

◆ Reorder()

void NewTt::Man::Reorder ( )

inline

Definition at line 262 of file giaNewTt.h.

262{} // dummy

◆ Resize()

bool NewTt::Man::Resize ( )

inline

Definition at line 163 of file giaNewTt.h.

                  {
      if(nObjsAlloc == nObjsMax)
        return false;
      lit nObjsAllocLit = (lit)nObjsAlloc << 1;
      if(nObjsAllocLit > (lit)BvarMax())
        nObjsAlloc = BvarMax();
      else
        nObjsAlloc = (bvar)nObjsAllocLit;
      nTotalSize = nTotalSize << 1;
      if(nVerbose >= 2)
        std::cout << "Reallocating " << nObjsAlloc << " nodes" << std::endl;
      vVals.resize(nTotalSize);
      if(!vRefs.empty())
        vRefs.resize(nObjsAlloc);
      return true;
    }

Here is the caller graph for this function:

◆ SetRef()

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

inline

Definition at line 265 of file giaNewTt.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:

◆ TurnOffReo()

void NewTt::Man::TurnOffReo ( )

inline

Definition at line 275 of file giaNewTt.h.

275{}

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

src/aig/gia/giaNewTt.h

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ Man()

Member Function Documentation

◆ And()

◆ Bvar2Lit()

◆ Const0()

◆ Const1()

◆ DecRef()

◆ Gbc()

◆ GetNumVars()

◆ IncRef()

◆ IsConst0()

◆ IsConst1()

◆ IthVar()

◆ Lit2Bvar()

◆ LitIsCompl()

◆ LitIsEq()

◆ LitNot()

◆ LitNotCond()

◆ OneCount()

◆ Or()

◆ PrintNode()

◆ Ref()

◆ RemoveRefIfUnused()

◆ Reorder()

◆ Resize()

◆ SetRef()

◆ TurnOffReo()