Transduction::Transduction< Man, Param, lit, LitMax > Class Template Reference

#include <giaTransduction.h>

Inheritance diagram for Transduction::Transduction< Man, Param, lit, LitMax >:

Collaboration diagram for Transduction::Transduction< Man, Param, lit, LitMax >:

Public Member Functions
int	CountGates () const
int	CountWires () const
int	CountNodes () const
int	CountLevels () const
void	Print (std::string str, bool nl) const
void	PrintStats (std::string prefix, bool nl, int prefix_size=0) const
void	PrintPfHeader (std::string prefix, int block, int block_i0)
int	TrivialMerge ()
int	TrivialDecompose ()
int	Decompose ()
int	Resub (bool fMspf)
int	ResubMono (bool fMspf)
int	ResubShared (bool fMspf)
int	RepeatResub (bool fMono, bool fMspf)
int	RepeatInner (bool fMspf, bool fInner)
int	RepeatOuter (bool fMspf, bool fInner, bool fOuter)
int	RepeatAll (bool fFirstMerge, bool fMspfMerge, bool fMspfResub, bool fInner, bool fOuter)
int	Cspf ()
int	Mspf ()
	Transduction (Gia_Man_t *pGia, int nVerbose, bool fNewLine, int nSortType, int nPiShuffle, bool fLevel, Gia_Man_t *pExdc, Param &p)
	~Transduction ()
Gia_Man_t *	GenerateAig () const
PfState	State () const
bool	BuildDebug ()
bool	CspfDebug ()
bool	MspfDebug ()
bool	Verify () const
void	PrintObjs () const

Detailed Description

template<class Man, class Param, class lit, lit LitMax>
class Transduction::Transduction< Man, Param, lit, LitMax >

Definition at line 141 of file giaTransduction.h.

Constructor & Destructor Documentation

Transduction()

template<class Man, class Param, class lit, lit LitMax>

Transduction::Transduction< Man, Param, lit, LitMax >::Transduction ( Gia_Man_t * pGia, int nVerbose, bool fNewLine, int nSortType, int nPiShuffle, bool fLevel, Gia_Man_t * pExdc, Param & p )

inline

Definition at line 1611 of file giaTransduction.h.

                                                                                                                                    : nVerbose(nVerbose), nSortType(nSortType), fLevel(fLevel), fNewLine(fNewLine) {
    startclk = Abc_Clock();
    p.nGbc = 1;
    p.nReo = 4000;
    if(nSortType && nSortType < 4)
      p.fCountOnes = true;
    this->man = new Man(Gia_ManCiNum(pGia), p);
    ImportAig(pGia);
    this->Update(vFs[0], this->man->Const0());
    for(unsigned i = 0; i < vPis.size(); i++)
      this->Update(vFs[i + 1], this->man->IthVar(i));
    nMaxLevels = -1;
    Build(false);
    this->man->Reorder();
    this->man->TurnOffReo();
    if(pExdc) {
      std::vector<lit> vExdc;
      Aig2Bdd(pExdc, vExdc);
      for(unsigned i = 0; i < vPos.size(); i++)
        vvCs[vPos[i]][0] = vExdc.size() == 1? vExdc[0]: vExdc[i];
    } else
      for(unsigned i = 0; i < vPos.size(); i++)
        this->Update(vvCs[vPos[i]][0], this->man->Const0());
    RemoveConstOutputs();
    vPoFs.resize(vPos.size(), LitMax);
    for(unsigned i = 0; i < vPos.size(); i++)
      this->Update(vPoFs[i], LitFi(vPos[i], 0));
    state = none;
    if(nPiShuffle)
      ShufflePis(nPiShuffle);
    if(fLevel)
      ComputeLevel();
    if(nVerbose)
      PrintStats("Init", true, 11);
  }

Here is the call graph for this function:

~Transduction()

template<class Man, class Param, class lit, lit LitMax>

Transduction::Transduction< Man, Param, lit, LitMax >::~Transduction ( )

inline

Definition at line 1646 of file giaTransduction.h.

                  {
    if(nVerbose)
      PrintStats("End", true, 11);
    this->DelVec(vFs);
    this->DelVec(vGs);
    this->DelVec(vvCs);
    this->DelVec(vPoFs);
    //assert(this->man->CountNodes() == (int)vPis.size() + 1);
    //assert(!this->man->Ref(this->man->Const0()));
    delete this->man;
  }

Here is the call graph for this function:

Member Function Documentation

BuildDebug()

template<class Man, class Param, class lit, lit LitMax>

bool Transduction::Transduction< Man, Param, lit, LitMax >::BuildDebug ( )

inline

Definition at line 1695 of file giaTransduction.h.

                    {
    for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
      vUpdates[*it] = true;
    std::vector<lit> vFsOld;
    CopyVec(vFsOld, vFs);
    Build(false);
    bool r = LitVecIsEq(vFsOld, vFs);
    DelVec(vFsOld);
    return r;
  }

Here is the call graph for this function:

CountGates()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::CountGates ( ) const

inline

Definition at line 177 of file giaTransduction.h.

                                {
    return vObjs.size();
  }

Here is the caller graph for this function:

CountLevels()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::CountLevels ( ) const

inline

Definition at line 189 of file giaTransduction.h.

                                 {
    int count = 0;
    for(unsigned i = 0; i < vPos.size(); i++)
      count = std::max(count, vLevels[vvFis[vPos[i]][0] >> 1]);
    return count;
  }

Here is the caller graph for this function:

CountNodes()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::CountNodes ( ) const

inline

Definition at line 186 of file giaTransduction.h.

                                {
    return CountWires() - CountGates();
  }

Here is the call graph for this function:

Here is the caller graph for this function:

CountWires()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::CountWires ( ) const

inline

Definition at line 180 of file giaTransduction.h.

                                {
    int count = 0;
    for(std::list<int>::const_iterator it = vObjs.begin(); it != vObjs.end(); it++)
      count += vvFis[*it].size();
    return count;
  }

Here is the caller graph for this function:

Cspf()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::Cspf ( )

inline

Definition at line 1456 of file giaTransduction.h.

             {
    return Cspf(true);
  }

CspfDebug()

template<class Man, class Param, class lit, lit LitMax>

bool Transduction::Transduction< Man, Param, lit, LitMax >::CspfDebug ( )

inline

Definition at line 1705 of file giaTransduction.h.

                   {
    std::vector<lit> vGsOld;
    this->CopyVec(vGsOld, vGs);
    std::vector<std::vector<lit> > vvCsOld;
    this->CopyVec(vvCsOld, vvCs);
    state = none;
    Cspf(false);
    bool r = this->LitVecIsEq(vGsOld, vGs) && this->LitVecIsEq(vvCsOld, vvCs);
    this->DelVec(vGsOld);
    this->DelVec(vvCsOld);
    return r;
  }

Here is the call graph for this function:

Decompose()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::Decompose ( )

inline

Definition at line 1025 of file giaTransduction.h.

                  {
    int count = 0;
    int pos = vPis.size() + 1;
    for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++) {
      std::set<int> s1(vvFis[*it].begin(), vvFis[*it].end());
      assert(s1.size() == vvFis[*it].size());
      std::list<int>::iterator it2 = it;
      for(it2++; it2 != vObjs.end(); it2++) {
        std::set<int> s2(vvFis[*it2].begin(), vvFis[*it2].end());
        std::set<int> s;
        std::set_intersection(s1.begin(), s1.end(), s2.begin(), s2.end(), std::inserter(s, s.begin()));
        if(s.size() > 1) {
          if(s == s1) {
            if(s == s2) {
              if(nVerbose > 2) {
                std::stringstream ss;
                ss << "\treplace Gate " << std::setw(5) << *it2
                   << " by Gate " << std::setw(5) << *it;
                Print(ss.str() , nVerbose > 3);
              }
              count += Replace(*it2, *it << 1, false);
              it2 = vObjs.erase(it2);
              it2--;
            } else {
              if(nVerbose > 2) {
                std::stringstream ss;
                ss << "\tdecompose Gate " << std::setw(5) << *it2
                   << " by Gate " << std::setw(5) << *it;
                Print(ss.str() , nVerbose > 3);
              }
              for(std::set<int>::iterator it3 = s.begin(); it3 != s.end(); it3++) {
                unsigned j = find(vvFis[*it2].begin(), vvFis[*it2].end(), *it3) - vvFis[*it2].begin();
                Disconnect(*it2, *it3 >> 1, j, false);
              }
              count += s.size();
              if(std::find(vvFis[*it2].begin(), vvFis[*it2].end(), *it << 1) == vvFis[*it2].end()) {
                Connect(*it2, *it << 1, false, false);
                count--;
              }
              vPfUpdates[*it2] = true;
            }
            continue;
          }
          if(s == s2) {
            it = vObjs.insert(it, *it2);
            vObjs.erase(it2);
          } else {
            NewGate(pos);
            if(nVerbose > 2) {
              std::stringstream ss;
              ss << "\tdecompose Gate " << std::setw(5) << *it
                 << " and " << std::setw(5) << *it2
                 << " by a new Gate " << std::setw(5) <<  pos;
              Print(ss.str() , nVerbose > 3);
            }
            if(nVerbose > 4) {
              std::stringstream ss;
              ss << "\t\tIntersection:";
              for(std::set<int>::iterator it3 = s.begin(); it3 != s.end(); it3++)
                ss << " " << (*it3 >> 1) << "(" << (*it3 & 1) << ")";
              Print(ss.str(), true);
            }
            for(std::set<int>::iterator it3 = s.begin(); it3 != s.end(); it3++)
              Connect(pos, *it3, false, false);
            count -= s.size();
            it = vObjs.insert(it, pos);
            Build(pos, vFs);
            vPfUpdates[*it] = true;
          }
          s1 = s;
          it2 = it;
        }
      }
      if(vvFis[*it].size() > 2)
        count += TrivialDecomposeOne(it, pos);
    }
    return count;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

GenerateAig()

template<class Man, class Param, class lit, lit LitMax>

Gia_Man_t * Transduction::Transduction< Man, Param, lit, LitMax >::GenerateAig ( ) const

inline

Definition at line 1659 of file giaTransduction.h.

                                 {
    Gia_Man_t * pGia, *pTemp;
    pGia = Gia_ManStart(1 + vPis.size() + CountNodes() + vPos.size());
    Gia_ManHashAlloc(pGia);
    std::vector<int> values(nObjsAlloc);
    values[0] = Gia_ManConst0Lit();
    for(unsigned i = 0; i < vPis.size(); i++)
      values[i + 1] = Gia_ManAppendCi(pGia);
    for(std::list<int>::const_iterator it = vObjs.begin(); it != vObjs.end(); it++) {
      assert(vvFis[*it].size() > 1);
      int i0 = vvFis[*it][0] >> 1;
      int i1 = vvFis[*it][1] >> 1;
      int c0 = vvFis[*it][0] & 1;
      int c1 = vvFis[*it][1] & 1;
      int r = Gia_ManHashAnd(pGia, Abc_LitNotCond(values[i0], c0), Abc_LitNotCond(values[i1], c1));
      for(unsigned i = 2; i < vvFis[*it].size(); i++) {
        int ii = vvFis[*it][i] >> 1;
        int ci = vvFis[*it][i] & 1;
        r = Gia_ManHashAnd(pGia, r, Abc_LitNotCond(values[ii], ci));
      }
      values[*it] = r;
    }
    for(unsigned i = 0; i < vPos.size(); i++) {
      int i0 = vvFis[vPos[i]][0] >> 1;
      int c0 = vvFis[vPos[i]][0] & 1;
      Gia_ManAppendCo(pGia, Abc_LitNotCond(values[i0], c0));
    }
    pGia = Gia_ManCleanup(pTemp = pGia);
    Gia_ManStop(pTemp);
    return pGia;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

Mspf()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::Mspf ( )

inline

Definition at line 1459 of file giaTransduction.h.

             {
    return Mspf(true);
  }

MspfDebug()

template<class Man, class Param, class lit, lit LitMax>

bool Transduction::Transduction< Man, Param, lit, LitMax >::MspfDebug ( )

inline

Definition at line 1717 of file giaTransduction.h.

                   {
    std::vector<lit> vGsOld;
    this->CopyVec(vGsOld, vGs);
    std::vector<std::vector<lit> > vvCsOld;
    this->CopyVec(vvCsOld, vvCs);
    state = none;
    Mspf(false);
    bool r = this->LitVecIsEq(vGsOld, vGs) && this->LitVecIsEq(vvCsOld, vvCs);
    this->DelVec(vGsOld);
    this->DelVec(vvCsOld);
    return r;
  }

Here is the call graph for this function:

Print()

template<class Man, class Param, class lit, lit LitMax>

void Transduction::Transduction< Man, Param, lit, LitMax >::Print ( std::string str, bool nl ) const

inline

Definition at line 195 of file giaTransduction.h.

                                                  {
    if(!fNewLine)
      std::cout << "\33[2K\r";
    std::cout << str;
    if(fNewLine || nl)
      std::cout << std::endl;
    else
      std::cout << std::flush;
  }

Here is the caller graph for this function:

PrintObjs()

template<class Man, class Param, class lit, lit LitMax>

void Transduction::Transduction< Man, Param, lit, LitMax >::PrintObjs ( ) const

inline

Definition at line 1740 of file giaTransduction.h.

                         {
    for(std::list<int>::const_iterator it = vObjs.begin(); it != vObjs.end(); it++) {
      std::cout << "Gate " << *it << ":";
      if(fLevel)
        std::cout << " Level = " << vLevels[*it] << ", Slack = " << vSlacks[*it];
      std::cout << std::endl;
      std::string delim = "";
      std::cout << "\tFis: ";
      for(unsigned j = 0; j < vvFis[*it].size(); j++) {
        std::cout << delim << (vvFis[*it][j] >> 1) << "(" << (vvFis[*it][j] & 1) << ")";
        delim = ", ";
      }
      std::cout << std::endl;
      delim = "";
      std::cout << "\tFos: ";
      for(unsigned j = 0; j < vvFos[*it].size(); j++) {
        std::cout << delim << vvFos[*it][j];
        delim = ", ";
      }
      std::cout << std::endl;
    }
  }

PrintPfHeader()

template<class Man, class Param, class lit, lit LitMax>

void Transduction::Transduction< Man, Param, lit, LitMax >::PrintPfHeader ( std::string prefix, int block, int block_i0 )

inline

Definition at line 215 of file giaTransduction.h.

                                                                       {
    std::stringstream ss;
    ss << "\t\t" << prefix;
    if(block_i0 != -1)
      ss << " (blocking Wire " << block_i0 << " -> " << block << ")";
    else if(block != -1)
      ss << " (blocking Gate " << block << ")";
    Print(ss.str(), true);
  }

Here is the call graph for this function:

PrintStats()

template<class Man, class Param, class lit, lit LitMax>

void Transduction::Transduction< Man, Param, lit, LitMax >::PrintStats ( std::string prefix, bool nl, int prefix_size = 0 ) const

inline

Definition at line 204 of file giaTransduction.h.

                                                                               {
    if(!prefix_size)
      prefix_size = prefix.size();
    std::stringstream ss;
    ss << std::left << std::setw(prefix_size) << prefix << ": " << std::right;
    ss << "#nodes = " << std::setw(5) << CountNodes();
    if(fLevel)
      ss << ", #level = " << std::setw(5) << CountLevels();
    ss << ", elapsed = " << std::setprecision(2) << std::fixed << std::setw(8) << 1.0 * (Abc_Clock() - startclk) / CLOCKS_PER_SEC << "s";
    Print(ss.str(), nl);
  }

Here is the call graph for this function:

Here is the caller graph for this function:

RepeatAll()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::RepeatAll ( bool fFirstMerge, bool fMspfMerge, bool fMspfResub, bool fInner, bool fOuter )

inline

Definition at line 1428 of file giaTransduction.h.

                                                                                              {
    TransductionBackup<Man, lit, LitMax> b;
    Save(b);
    int count = 0;
    int diff = 0;
    if(fFirstMerge)
      diff = ResubShared(fMspfMerge);
    diff += RepeatOuter(fMspfResub, fInner, fOuter);
    if(diff > 0) {
      count = diff;
      Save(b);
      diff = 0;
    }
    while(true) {
      diff += ResubShared(fMspfMerge) + RepeatOuter(fMspfResub, fInner, fOuter);
      if(diff > 0) {
        count += diff;
        Save(b);
        diff = 0;
      } else {
        Load(b);
        break;
      }
    }
    return count;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

RepeatInner()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::RepeatInner ( bool fMspf, bool fInner )

inline

Definition at line 1410 of file giaTransduction.h.

                                           {
    int count = 0;
    while(int diff = RepeatResub(true, fMspf) + RepeatResub(false, fMspf)) {
      count += diff;
      if(!fInner)
        break;
    }
    return count;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

RepeatOuter()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::RepeatOuter ( bool fMspf, bool fInner, bool fOuter )

inline

Definition at line 1419 of file giaTransduction.h.

                                                        {
    int count = 0;
    while(int diff = fMspf? RepeatInner(false, fInner) + RepeatInner(true, fInner): RepeatInner(false, fInner)) {
      count += diff;
      if(!fOuter)
        break;
    }
    return count;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

RepeatResub()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::RepeatResub ( bool fMono, bool fMspf )

inline

Definition at line 1404 of file giaTransduction.h.

                                          {
    int count = 0;
    while(int diff = fMono? ResubMono(fMspf): Resub(fMspf))
      count += diff;
    return count;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

Resub()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::Resub ( bool fMspf )

inline

Definition at line 1162 of file giaTransduction.h.

                        {
    int count = fMspf? Mspf(true): Cspf(true);
    int nodes = CountNodes();
    TransductionBackup<Man, lit, LitMax> b;
    Save(b);
    int count_ = count;
    std::list<int> targets = vObjs;
    for(std::list<int>::reverse_iterator it = targets.rbegin(); it != targets.rend(); it++) {
      if(nVerbose > 1) {
        std::stringstream ss;
        ss << "[Resub] processing Gate " << std::setw(5) << *it
           << " (" << std::setw(5) << std::distance(targets.rbegin(), it) + 1
           << "/" << std::setw(5) << targets.size() << ")";
        PrintStats(ss.str(), nVerbose > 2);
      }
      if(vvFos[*it].empty())
        continue;
      count += TrivialMergeOne(*it);
      std::vector<bool> lev;
      if(fLevel) {
        for(unsigned j = 0; j < vvFis[*it].size(); j++)
          add(lev, vLevels[vvFis[*it][j] >> 1]);
        if((int)lev.size() > vLevels[*it] + vSlacks[*it]) {
          Load(b);
          count = count_;
          continue;
        }
        lev.resize(vLevels[*it] + vSlacks[*it]);
      }
      bool fConnect = false;
      std::vector<bool> vMarks(nObjsAlloc);
      MarkFoCone_rec(vMarks, *it);
      std::list<int> targets2 = vObjs;
      for(std::list<int>::iterator it2 = targets2.begin(); it2 != targets2.end(); it2++) {
        if(fLevel && (int)lev.size() > vLevels[*it] + vSlacks[*it])
          break;
        if(!vMarks[*it2] && !vvFos[*it2].empty())
          if(!fLevel || noexcess(lev, vLevels[*it2]))
            if(TryConnect(*it, *it2, false) || TryConnect(*it, *it2, true)) {
              fConnect = true;
              count--;
              if(fLevel)
                add(lev, vLevels[*it2]);
            }
      }
      if(fConnect) {
        if(fMspf) {
          Build();
          count += Mspf(true, *it);
        } else {
          vPfUpdates[*it] = true;
          count += Cspf(true, *it);
        }
        if(!vvFos[*it].empty()) {
          vPfUpdates[*it] = true;
          count += fMspf? Mspf(true): Cspf(true);
        }
      }
      if(nodes < CountNodes()) {
        Load(b);
        count = count_;
        continue;
      }
      if(!vvFos[*it].empty() && vvFis[*it].size() > 2) {
        std::list<int>::iterator it2 = find(vObjs.begin(), vObjs.end(), *it);
        int pos = nObjsAlloc;
        if(fLevel)
          count += BalancedDecomposeOne(it2, pos) + (fMspf? Mspf(true): Cspf(true));
        else
          count += TrivialDecomposeOne(it2, pos);
      }
      nodes = CountNodes();
      Save(b);
      count_ = count;
    }
    if(nVerbose)
      PrintStats("Resub", true, 11);
    return count;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

ResubMono()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::ResubMono ( bool fMspf )

inline

Definition at line 1241 of file giaTransduction.h.

                            {
    int count = fMspf? Mspf(true): Cspf(true);
    std::list<int> targets = vObjs;
    for(std::list<int>::reverse_iterator it = targets.rbegin(); it != targets.rend(); it++) {
      if(nVerbose > 1) {
        std::stringstream ss;
        ss << "[ResubMono] processing Gate " << std::setw(5) << *it
           << " (" << std::setw(5) << std::distance(targets.rbegin(), it) + 1
           << "/" << std::setw(5) << targets.size() << ")";
        PrintStats(ss.str(), nVerbose > 2);
      }
      if(vvFos[*it].empty())
        continue;
      count += TrivialMergeOne(*it);
      TransductionBackup<Man, lit, LitMax> b;
      Save(b);
      int count_ = count;
      for(unsigned i = 0; i < vPis.size(); i++) {
        if(vvFos[*it].empty())
          break;
        if(nVerbose > 2) {
          std::stringstream ss;
          ss << "\ttrying a new fanin PI " << std::setw(2) << i;
          PrintStats(ss.str(), nVerbose > 3);
        }
        if(TryConnect(*it, vPis[i], false) || TryConnect(*it, vPis[i], true)) {
          count--;
          int diff;
          if(fMspf) {
            Build();
            diff = Mspf(true, *it, vPis[i]);
          } else {
            vPfUpdates[*it] = true;
            diff = Cspf(true, *it, vPis[i]);
          }
          if(diff) {
            count += diff;
            if(!vvFos[*it].empty()) {
              vPfUpdates[*it] = true;
              count += fMspf? Mspf(true): Cspf(true);
            }
            if(fLevel && CountLevels() > nMaxLevels) {
              Load(b);
              count = count_;
            } else {
              Save(b);
              count_ = count;
            }
          } else {
            Load(b);
            count = count_;
          }
        }
      }
      if(vvFos[*it].empty())
        continue;
      std::vector<bool> vMarks(nObjsAlloc);
      MarkFoCone_rec(vMarks, *it);
      std::list<int> targets2 = vObjs;
      for(std::list<int>::iterator it2 = targets2.begin(); it2 != targets2.end(); it2++) {
        if(vvFos[*it].empty())
          break;
        if(nVerbose > 2) {
          std::stringstream ss;
          ss << "\ttrying a new fanin Gate " << std::setw(5) << *it2
             << " (" << std::setw(5) << std::distance(targets2.begin(), it2) + 1
             << "/" << std::setw(5) << targets2.size() << ")";
          PrintStats(ss.str(), nVerbose > 3);
        }
        if(!vMarks[*it2] && !vvFos[*it2].empty())
          if(TryConnect(*it, *it2, false) || TryConnect(*it, *it2, true)) {
            count--;
            int diff;
            if(fMspf) {
              Build();
              diff = Mspf(true, *it, *it2);
            } else {
              vPfUpdates[*it] = true;
              diff = Cspf(true, *it, *it2);
            }
            if(diff) {
              count += diff;
              if(!vvFos[*it].empty()) {
                vPfUpdates[*it] = true;
                count += fMspf? Mspf(true): Cspf(true);
              }
              if(fLevel && CountLevels() > nMaxLevels) {
                Load(b);
                count = count_;
              } else {
                Save(b);
                count_ = count;
              }
            } else {
              Load(b);
              count = count_;
            }
          }
      }
      if(vvFos[*it].empty())
        continue;
      if(vvFis[*it].size() > 2) {
        std::list<int>::iterator it2 = find(vObjs.begin(), vObjs.end(), *it);
        int pos = nObjsAlloc;
        if(fLevel)
          count += BalancedDecomposeOne(it2, pos) + (fMspf? Mspf(true): Cspf(true));
        else
          count += TrivialDecomposeOne(it2, pos);
      }
    }
    if(nVerbose)
      PrintStats("ResubMono", true, 11);
    return count;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

ResubShared()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::ResubShared ( bool fMspf )

inline

Definition at line 1355 of file giaTransduction.h.

                              {
    int count = fMspf? Mspf(true): Cspf(true);
    std::list<int> targets = vObjs;
    for(std::list<int>::reverse_iterator it = targets.rbegin(); it != targets.rend(); it++) {
      if(nVerbose > 1) {
        std::stringstream ss;
        ss << "[ResubShared] processing Gate " << std::setw(5) << *it
           << " (" << std::setw(5) << std::distance(targets.rbegin(), it) + 1
           << "/" << std::setw(5) << targets.size() << ")";
        PrintStats(ss.str(), nVerbose > 2);
      }
      if(vvFos[*it].empty())
        continue;
      count += TrivialMergeOne(*it);
      bool fConnect = false;
      for(unsigned i = 0; i < vPis.size(); i++)
        if(TryConnect(*it, vPis[i], false) || TryConnect(*it, vPis[i], true)) {
          fConnect |= true;
          count--;
        }
      std::vector<bool> vMarks(nObjsAlloc);
      MarkFoCone_rec(vMarks, *it);
      for(std::list<int>::iterator it2 = targets.begin(); it2 != targets.end(); it2++)
        if(!vMarks[*it2] && !vvFos[*it2].empty())
          if(TryConnect(*it, *it2, false) || TryConnect(*it, *it2, true)) {
            fConnect |= true;
            count--;
          }
      if(fConnect) {
        if(fMspf) {
          Build();
          count += Mspf(true, *it);
        } else {
          vPfUpdates[*it] = true;
          count += Cspf(true, *it);
        }
        if(!vvFos[*it].empty()) {
          vPfUpdates[*it] = true;
          count += fMspf? Mspf(true): Cspf(true);
        }
      }
    }
    count += Decompose();
    if(nVerbose)
      PrintStats("ResubShared", true, 11);
    return count;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

State()

template<class Man, class Param, class lit, lit LitMax>

PfState Transduction::Transduction< Man, Param, lit, LitMax >::State ( ) const

inline

Definition at line 1692 of file giaTransduction.h.

                        {
    return state;
  }

TrivialDecompose()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::TrivialDecompose ( )

inline

Definition at line 1017 of file giaTransduction.h.

                         {
    int count = 0;
    int pos = vPis.size() + 1;
    for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
      if(vvFis[*it].size() > 2)
        count += TrivialDecomposeOne(it, pos);
    return count;
  }

TrivialMerge()

template<class Man, class Param, class lit, lit LitMax>

int Transduction::Transduction< Man, Param, lit, LitMax >::TrivialMerge ( )

inline

Definition at line 1009 of file giaTransduction.h.

                     {
    int count = 0;
    for(std::list<int>::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend();) {
      count += TrivialMergeOne(*it);
      it++;
    }
    return count;
  }

Verify()

template<class Man, class Param, class lit, lit LitMax>

bool Transduction::Transduction< Man, Param, lit, LitMax >::Verify ( ) const

inline

Definition at line 1729 of file giaTransduction.h.

                      {
    for(unsigned j = 0; j < vPos.size(); j++) {
      lit x = this->Xor(LitFi(vPos[j], 0), vPoFs[j]);
      this->IncRef(x);
      this->Update(x, this->man->And(x, this->man->LitNot(vvCs[vPos[j]][0])));
      this->DecRef(x);
      if(!this->man->IsConst0(x))
        return false;
    }
    return true;
  }

Here is the call graph for this function:

Here is the caller graph for this function:

---

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

• src/aig/gia/giaTransduction.h