Merge pull request #178 from MyskYko/ttopt

Import ttopt

src/aig/gia/giaTtopt.cpp

+// Author : Yukio Miyasaka
+#include <iostream>
+#include <fstream>
+#include <string>
+#include <vector>
+#include <list>
+#include <algorithm>
+#include <numeric>
+#include <random>
+#include <cassert>
+#include <map>
+#include <bitset>
+#include <unordered_map>
+
+#include "gia.h"
+
+ABC_NAMESPACE_IMPL_START
+
+namespace Ttopt {
+
+struct PairHasher {
+  std::size_t operator()(const std::pair<int, int> & k) const {
+    std::hash<int> hasher;
+    std::size_t seed = hasher(k.first) + 0x9e3779b9;
+    seed = hasher(k.second) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
+    return seed;
+  }
+};
+
+class TruthTable {
+public:
+  const int ww = 64; // word width
+  const int lww = 6; // log word width
+  typedef std::bitset<64> bsw;
+
+  int nInputs;
+  int nSize;
+  int nTotalSize;
+  int nOutputs;
+  std::vector<word> t;
+
+  std::vector<std::vector<int> > vvIndices;
+  std::vector<std::vector<int> > vvRedundantIndices;
+  std::vector<int> vLevels;
+
+  std::vector<std::vector<word> > savedt;
+  std::vector<std::vector<std::vector<int> > > vvIndicesSaved;
+  std::vector<std::vector<std::vector<int> > > vvRedundantIndicesSaved;
+  std::vector<std::vector<int> > vLevelsSaved;
+
+  std::mt19937 rng;
+  static const word ones[];
+  static const word swapmask[];
+
+  TruthTable(int nInputs, int nOutputs): nInputs(nInputs), nOutputs(nOutputs) {
+    if(nInputs >= lww) {
+      nSize = 1 << (nInputs - lww);
+      nTotalSize = nSize * nOutputs;
+      t.resize(nTotalSize);
+    } else {
+      nSize = 0;
+      nTotalSize = ((1 << nInputs) * nOutputs + ww - 1) / ww;
+      t.resize(nTotalSize);
+    }
+    vLevels.resize(nInputs);
+    std::iota(vLevels.begin(), vLevels.end(), 0);
+  }
+
+  std::string BinaryToString(int bin, int size) {
+    std::string str;
+    for(int i = 0; i < size; i++) {
+      str += (bin & 1) + '0';
+      bin = bin >> 1;
+    }
+    return str;
+  }
+  void GeneratePla(std::string filename) {
+    std::ofstream f(filename);
+    f << ".i " << nInputs << std::endl;
+    f << ".o " << nOutputs << std::endl;
+    if(nSize) {
+      for(int index = 0; index < nSize; index++) {
+        for(int pos = 0; pos < ww; pos++) {
+          int pat = (index << lww) + pos;
+          f << BinaryToString(pat, nInputs) << " ";
+          for(int i = 0; i < nOutputs; i++) {
+            f << ((t[nSize * i + index] >> pos) & 1);
+          }
+          f << std::endl;
+        }
+      }
+    } else {
+      for(int pos = 0; pos < (1 << nInputs); pos++) {
+        f << BinaryToString(pos, nInputs) << " ";
+        for(int i = 0; i < nOutputs; i++) {
+          int padding = i * (1 << nInputs);
+          f << ((t[padding / ww] >> (pos + padding % ww)) & 1);
+        }
+        f << std::endl;
+      }
+    }
+  }
+
+  virtual void Save(uint i) {
+    if(savedt.size() < i + 1) {
+      savedt.resize(i + 1);
+      vLevelsSaved.resize(i + 1);
+    }
+    savedt[i] = t;
+    vLevelsSaved[i] = vLevels;
+  }
+
+  virtual void Load(uint i) {
+    assert(i < savedt.size());
+    t = savedt[i];
+    vLevels = vLevelsSaved[i];
+  }
+
+  virtual void SaveIndices(uint i) {
+    if(vvIndicesSaved.size() < i + 1) {
+      vvIndicesSaved.resize(i + 1);
+      vvRedundantIndicesSaved.resize(i + 1);
+    }
+    vvIndicesSaved[i] = vvIndices;
+    vvRedundantIndicesSaved[i] = vvRedundantIndices;
+  }
+
+  virtual void LoadIndices(uint i) {
+    vvIndices = vvIndicesSaved[i];
+    vvRedundantIndices = vvRedundantIndicesSaved[i];
+  }
+
+  word GetValue(int index_lev, int lev) {
+    assert(index_lev >= 0);
+    assert(nInputs - lev <= lww);
+    int logwidth = nInputs - lev;
+    int index = index_lev >> (lww - logwidth);
+    int pos = (index_lev % (1 << (lww - logwidth))) << logwidth;
+    return (t[index] >> pos) & ones[logwidth];
+  }
+
+  int IsEq(int index1, int index2, int lev, bool fCompl = false) {
+    assert(index1 >= 0);
+    assert(index2 >= 0);
+    int logwidth = nInputs - lev;
+    bool fEq = true;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) {
+        fEq &= t[nScopeSize * index1 + i] == t[nScopeSize * index2 + i];
+        fCompl &= t[nScopeSize * index1 + i] == ~t[nScopeSize * index2 + i];
+      }
+    } else {
+      word value = GetValue(index1, lev) ^ GetValue(index2, lev);
+      fEq &= !value;
+      fCompl &= !(value ^ ones[logwidth]);
+    }
+    return 2 * fCompl + fEq;
+  }
+
+  bool Imply(int index1, int index2, int lev) {
+    assert(index1 >= 0);
+    assert(index2 >= 0);
+    int logwidth = nInputs - lev;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      for(int i = 0; i < nScopeSize; i++) {
+        if(t[nScopeSize * index1 + i] & ~t[nScopeSize * index2 + i]) {
+          return false;
+        }
+      }
+      return true;
+    }
+    return !(GetValue(index1, lev) & (GetValue(index2, lev) ^ ones[logwidth]));
+  }
+
+  int BDDNodeCountLevel(int lev) {
+    return vvIndices[lev].size() - vvRedundantIndices[lev].size();
+  }
+
+  int BDDNodeCount() {
+    int count = 1; // const node
+    for(int i = 0; i < nInputs; i++) {
+      count += BDDNodeCountLevel(i);
+    }
+    return count;
+  }
+
+  int BDDFind(int index, int lev) {
+    int logwidth = nInputs - lev;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      bool fZero = true;
+      bool fOne = true;
+      for(int i = 0; i < nScopeSize && (fZero || fOne); i++) {
+        word value = t[nScopeSize * index + i];
+        fZero &= !value;
+        fOne &= !(~value);
+      }
+      if(fZero || fOne) {
+        return -2 ^ fOne;
+      }
+      for(uint j = 0; j < vvIndices[lev].size(); j++) {
+        int index2 = vvIndices[lev][j];
+        bool fEq = true;
+        bool fCompl = true;
+        for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) {
+          fEq &= t[nScopeSize * index + i] == t[nScopeSize * index2 + i];
+          fCompl &= t[nScopeSize * index + i] == ~t[nScopeSize * index2 + i];
+        }
+        if(fEq || fCompl) {
+          return (j << 1) ^ fCompl;
+        }
+      }
+    } else {
+      word value = GetValue(index, lev);
+      if(!value) {
+        return -2;
+      }
+      if(!(value ^ ones[logwidth])) {
+        return -1;
+      }
+      for(uint j = 0; j < vvIndices[lev].size(); j++) {
+        int index2 = vvIndices[lev][j];
+        word value2 = value ^ GetValue(index2, lev);
+        if(!(value2)) {
+          return j << 1;
+        }
+        if(!(value2 ^ ones[logwidth])) {
+          return (j << 1) ^ 1;
+        }
+      }
+    }
+    return -3;
+  }
+
+  virtual int BDDBuildOne(int index, int lev) {
+    int r = BDDFind(index, lev);
+    if(r >= -2) {
+      return r;
+    }
+    vvIndices[lev].push_back(index);
+    return (vvIndices[lev].size() - 1) << 1;
+  }
+
+  virtual void BDDBuildStartup() {
+    vvIndices.clear();
+    vvIndices.resize(nInputs);
+    vvRedundantIndices.clear();
+    vvRedundantIndices.resize(nInputs);
+    for(int i = 0; i < nOutputs; i++) {
+      BDDBuildOne(i, 0);
+    }
+  }
+
+  virtual void BDDBuildLevel(int lev) {
+    for(int index: vvIndices[lev-1]) {
+      int cof0 = BDDBuildOne(index << 1, lev);
+      int cof1 = BDDBuildOne((index << 1) ^ 1, lev);
+      if(cof0 == cof1) {
+        vvRedundantIndices[lev-1].push_back(index);
+      }
+    }
+  }
+
+  virtual int BDDBuild() {
+    BDDBuildStartup();
+    for(int i = 1; i < nInputs; i++) {
+      BDDBuildLevel(i);
+    }
+    return BDDNodeCount();
+  }
+
+  virtual int BDDRebuild(int lev) {
+    vvIndices[lev].clear();
+    vvIndices[lev+1].clear();
+    for(int i = lev; i < lev + 2; i++) {
+      if(!i) {
+        for(int j = 0; j < nOutputs; j++) {
+          BDDBuildOne(j, 0);
+        }
+      } else {
+        vvRedundantIndices[i-1].clear();
+        BDDBuildLevel(i);
+      }
+    }
+    if(lev < nInputs - 2) {
+      vvRedundantIndices[lev+1].clear();
+      for(int index: vvIndices[lev+1]) {
+        if(IsEq(index << 1, (index << 1) ^ 1, lev + 2)) {
+          vvRedundantIndices[lev+1].push_back(index);
+        }
+      }
+    }
+    return BDDNodeCount();
+  }
+
+  virtual void Swap(int lev) {
+    assert(lev < nInputs - 1);
+    auto it0 = std::find(vLevels.begin(), vLevels.end(), lev);
+    auto it1 = std::find(vLevels.begin(), vLevels.end(), lev + 1);
+    std::swap(*it0, *it1);
+    if(nInputs - lev - 1 > lww) {
+      int nScopeSize = 1 << (nInputs - lev - 2 - lww);
+      for(int i = nScopeSize; i < nTotalSize; i += (nScopeSize << 2)) {
+        for(int j = 0; j < nScopeSize; j++) {
+          std::swap(t[i + j], t[i + nScopeSize + j]);
+        }
+      }
+    } else if(nInputs - lev - 1 == lww) {
+      for(int i = 0; i < nTotalSize; i += 2) {
+        t[i+1] ^= t[i] >> (ww / 2);
+        t[i] ^= t[i+1] << (ww / 2);
+        t[i+1] ^= t[i] >> (ww / 2);
+      }
+    } else {
+      for(int i = 0; i < nTotalSize; i++) {
+        int d = nInputs - lev - 2;
+        int shamt = 1 << d;
+        t[i] ^= (t[i] >> shamt) & swapmask[d];
+        t[i] ^= (t[i] & swapmask[d]) << shamt;
+        t[i] ^= (t[i] >> shamt) & swapmask[d];
+      }
+    }
+  }
+
+  void SwapIndex(int &index, int d) {
+    if((index >> d) % 4 == 1) {
+      index += 1 << d;
+    } else if((index >> d) % 4 == 2) {
+      index -= 1 << d;
+    }
+  }
+
+  virtual int BDDSwap(int lev) {
+    Swap(lev);
+    for(int i = lev + 2; i < nInputs; i++) {
+      for(uint j = 0; j < vvIndices[i].size(); j++) {
+        SwapIndex(vvIndices[i][j], i - (lev + 2));
+      }
+    }
+    // swapping vvRedundantIndices is unnecessary for node counting
+    return BDDRebuild(lev);
+  }
+
+  int SiftReo() {
+    int best = BDDBuild();
+    Save(0);
+    SaveIndices(0);
+    std::vector<int> vars(nInputs);
+    std::iota(vars.begin(), vars.end(), 0);
+    std::sort(vars.begin(), vars.end(), [&](int i1, int i2) {return BDDNodeCountLevel(vLevels[i1]) > BDDNodeCountLevel(vLevels[i2]);});
+    bool turn = true;
+    for(int var: vars) {
+      bool updated = false;
+      int lev = vLevels[var];
+      for(int i = lev; i < nInputs - 1; i++) {
+        int count = BDDSwap(i);
+        if(best > count) {
+          best = count;
+          updated = true;
+          Save(turn);
+          SaveIndices(turn);
+        }
+      }
+      if(lev) {
+        Load(!turn);
+        LoadIndices(!turn);
+        for(int i = lev - 1; i >= 0; i--) {
+          int count = BDDSwap(i);
+          if(best > count) {
+            best = count;
+            updated = true;
+            Save(turn);
+            SaveIndices(turn);
+          }
+        }
+      }
+      turn ^= updated;
+      Load(!turn);
+      LoadIndices(!turn);
+    }
+    return best;
+  }
+
+  void Reo(std::vector<int> vLevelsNew) {
+    for(int i = 0; i < nInputs; i++) {
+      int var = std::find(vLevelsNew.begin(), vLevelsNew.end(), i) - vLevelsNew.begin();
+      int lev = vLevels[var];
+      if(lev < i) {
+        for(int j = lev; j < i; j++) {
+          Swap(j);
+        }
+      } else if(lev > i) {
+        for(int j = lev - 1; j >= i; j--) {
+          Swap(j);
+        }
+      }
+    }
+    assert(vLevels == vLevelsNew);
+  }
+
+  int RandomSiftReo(int nRound) {
+    int best = SiftReo();
+    Save(2);
+    for(int i = 0; i < nRound; i++) {
+      std::vector<int> vLevelsNew(nInputs);
+      std::iota(vLevelsNew.begin(), vLevelsNew.end(), 0);
+      std::shuffle(vLevelsNew.begin(), vLevelsNew.end(), rng);
+      Reo(vLevelsNew);
+      int r = SiftReo();
+      if(best > r) {
+        best = r;
+        Save(2);
+      }
+    }
+    Load(2);
+    return best;
+  }
+
+  int BDDGenerateAigRec(Gia_Man_t *pNew, std::vector<int> const &vInputs, std::vector<std::vector<int> > &vvNodes, int index, int lev) {
+    int r = BDDFind(index, lev);
+    if(r >= 0) {
+      return vvNodes[lev][r >> 1] ^ (r & 1);
+    }
+    if(r >= -2) {
+      return r + 2;
+    }
+    int cof0 = BDDGenerateAigRec(pNew, vInputs, vvNodes, index << 1, lev + 1);
+    int cof1 = BDDGenerateAigRec(pNew, vInputs, vvNodes, (index << 1) ^ 1, lev + 1);
+    if(cof0 == cof1) {
+      return cof0;
+    }
+    int node;
+    if(Imply(index << 1, (index << 1) ^ 1, lev + 1)) {
+      node = Gia_ManHashOr(pNew, Gia_ManHashAnd(pNew, vInputs[lev], cof1), cof0);
+    } else if(Imply((index << 1) ^ 1, index << 1, lev + 1)) {
+      node = Gia_ManHashOr(pNew, Gia_ManHashAnd(pNew, vInputs[lev] ^ 1, cof0), cof1);
+    } else {
+      node = Gia_ManHashMux(pNew, vInputs[lev], cof1, cof0);
+    }
+    vvIndices[lev].push_back(index);
+    vvNodes[lev].push_back(node);
+    return node;
+  }
+
+  virtual void BDDGenerateAig(Gia_Man_t *pNew, Vec_Int_t *vSupp) {
+    vvIndices.clear();
+    vvIndices.resize(nInputs);
+    std::vector<std::vector<int> > vvNodes(nInputs);
+    std::vector<int> vInputs(nInputs);
+    for(int i = 0; i < nInputs; i++) {
+      vInputs[vLevels[i]] = Vec_IntEntry(vSupp, nInputs - i - 1) << 1;
+    }
+    for(int i = 0; i < nOutputs; i++) {
+      int node = BDDGenerateAigRec(pNew, vInputs, vvNodes, i, 0);
+      Gia_ManAppendCo(pNew, node);
+    }
+  }
+};
+
+const word TruthTable::ones[7] = {ABC_CONST(0x0000000000000001),
+                                  ABC_CONST(0x0000000000000003),
+                                  ABC_CONST(0x000000000000000f),
+                                  ABC_CONST(0x00000000000000ff),
+                                  ABC_CONST(0x000000000000ffff),
+                                  ABC_CONST(0x00000000ffffffff),
+                                  ABC_CONST(0xffffffffffffffff)};
+  
+const word TruthTable::swapmask[5] = {ABC_CONST(0x2222222222222222),
+                                      ABC_CONST(0x0c0c0c0c0c0c0c0c),
+                                      ABC_CONST(0x00f000f000f000f0),
+                                      ABC_CONST(0x0000ff000000ff00),
+                                      ABC_CONST(0x00000000ffff0000)};
+  
+class TruthTableReo : public TruthTable {
+public:
+  bool fBuilt = false;
+  std::vector<std::vector<int> > vvChildren;
+  std::vector<std::vector<std::vector<int> > > vvChildrenSaved;
+
+  TruthTableReo(int nInputs, int nOutputs): TruthTable(nInputs, nOutputs) {}
+
+  void Save(uint i) override {
+    if(vLevelsSaved.size() < i + 1) {
+      vLevelsSaved.resize(i + 1);
+    }
+    vLevelsSaved[i] = vLevels;
+  }
+
+  void Load(uint i) override {
+    assert(i < vLevelsSaved.size());
+    vLevels = vLevelsSaved[i];
+  }
+
+  void SaveIndices(uint i) override {
+    TruthTable::SaveIndices(i);
+    if(vvChildrenSaved.size() < i + 1) {
+      vvChildrenSaved.resize(i + 1);
+    }
+    vvChildrenSaved[i] = vvChildren;
+  }
+
+  void LoadIndices(uint i) override {
+    TruthTable::LoadIndices(i);
+    vvChildren = vvChildrenSaved[i];
+  }
+
+  void BDDBuildStartup() override {
+    vvChildren.clear();
+    vvChildren.resize(nInputs);
+    TruthTable::BDDBuildStartup();
+  }
+
+  void BDDBuildLevel(int lev) override {
+    for(int index: vvIndices[lev-1]) {
+      int cof0 = BDDBuildOne(index << 1, lev);
+      int cof1 = BDDBuildOne((index << 1) ^ 1, lev);
+      vvChildren[lev-1].push_back(cof0);
+      vvChildren[lev-1].push_back(cof1);
+      if(cof0 == cof1) {
+        vvRedundantIndices[lev-1].push_back(index);
+      }
+    }
+  }
+
+  int BDDBuild() override {
+    if(fBuilt) {
+      return BDDNodeCount();
+    }
+    fBuilt = true;
+    BDDBuildStartup();
+    for(int i = 1; i < nInputs + 1; i++) {
+      BDDBuildLevel(i);
+    }
+    return BDDNodeCount();
+  }
+
+  int BDDRebuildOne(int index, int cof0, int cof1, int lev, std::unordered_map<std::pair<int, int>, int, PairHasher> &unique, std::vector<int> &vChildrenLow) {
+    if(cof0 < 0 && cof0 == cof1) {
+      return cof0;
+    }
+    bool fCompl = cof0 & 1;
+    if(fCompl) {
+      cof0 ^= 1;
+      cof1 ^= 1;
+    }
+    if(unique.count({cof0, cof1})) {
+      return (unique[{cof0, cof1}] << 1) ^ fCompl;
+    }
+    vvIndices[lev].push_back(index);
+    unique[{cof0, cof1}] = vvIndices[lev].size() - 1;
+    vChildrenLow.push_back(cof0);
+    vChildrenLow.push_back(cof1);
+    if(cof0 == cof1) {
+      vvRedundantIndices[lev].push_back(index);
+    }
+    return ((vvIndices[lev].size() - 1) << 1) ^ fCompl;
+  }
+
+  int BDDRebuild(int lev) override {
+    vvRedundantIndices[lev].clear();
+    vvRedundantIndices[lev+1].clear();
+    std::vector<int> vChildrenHigh;
+    std::vector<int> vChildrenLow;
+    std::unordered_map<std::pair<int, int>, int, PairHasher> unique;
+    unique.reserve(2 * vvIndices[lev+1].size());
+    vvIndices[lev+1].clear();
+    for(uint i = 0; i < vvIndices[lev].size(); i++) {
+      int index = vvIndices[lev][i];
+      int cof0index = vvChildren[lev][i+i] >> 1;
+      int cof1index = vvChildren[lev][i+i+1] >> 1;
+      bool cof0c = vvChildren[lev][i+i] & 1;
+      bool cof1c = vvChildren[lev][i+i+1] & 1;
+      int cof00, cof01, cof10, cof11;
+      if(cof0index < 0) {
+        cof00 = -2 ^ cof0c;
+        cof01 = -2 ^ cof0c;
+      } else {
+        cof00 = vvChildren[lev+1][cof0index+cof0index] ^ cof0c;
+        cof01 = vvChildren[lev+1][cof0index+cof0index+1] ^ cof0c;
+      }
+      if(cof1index < 0) {
+        cof10 = -2 ^ cof1c;
+        cof11 = -2 ^ cof1c;
+      } else {
+        cof10 = vvChildren[lev+1][cof1index+cof1index] ^ cof1c;
+        cof11 = vvChildren[lev+1][cof1index+cof1index+1] ^ cof1c;
+      }
+      int newcof0 = BDDRebuildOne(index << 1, cof00, cof10, lev + 1, unique, vChildrenLow);
+      int newcof1 = BDDRebuildOne((index << 1) ^ 1, cof01, cof11, lev + 1, unique, vChildrenLow);
+      vChildrenHigh.push_back(newcof0);
+      vChildrenHigh.push_back(newcof1);
+      if(newcof0 == newcof1) {
+        vvRedundantIndices[lev].push_back(index);
+      }
+    }
+    vvChildren[lev] = vChildrenHigh;
+    vvChildren[lev+1] = vChildrenLow;
+    return BDDNodeCount();
+  }
+
+  void Swap(int lev) override {
+    assert(lev < nInputs - 1);
+    auto it0 = std::find(vLevels.begin(), vLevels.end(), lev);
+    auto it1 = std::find(vLevels.begin(), vLevels.end(), lev + 1);
+    std::swap(*it0, *it1);
+    BDDRebuild(lev);
+  }
+
+  int BDDSwap(int lev) override {
+    Swap(lev);
+    return BDDNodeCount();
+  }
+
+  virtual void BDDGenerateAig(Gia_Man_t *pNew, Vec_Int_t *vSupp) override {
+    abort();
+  }
+};
+
+class TruthTableRewrite : public TruthTable {
+public:
+  TruthTableRewrite(int nInputs, int nOutputs): TruthTable(nInputs, nOutputs) {}
+
+  void SetValue(int index_lev, int lev, word value) {
+    assert(index_lev >= 0);
+    assert(nInputs - lev <= lww);
+    int logwidth = nInputs - lev;
+    int index = index_lev >> (lww - logwidth);
+    int pos = (index_lev % (1 << (lww - logwidth))) << logwidth;
+    t[index] &= ~(ones[logwidth] << pos);
+    t[index] ^= value << pos;
+  }
+
+  void CopyFunc(int index1, int index2, int lev, bool fCompl) {
+    assert(index1 >= 0);
+    int logwidth = nInputs - lev;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      if(!fCompl) {
+        if(index2 < 0) {
+          for(int i = 0; i < nScopeSize; i++) {
+            t[nScopeSize * index1 + i] = 0;
+          }
+        } else {
+          for(int i = 0; i < nScopeSize; i++) {
+            t[nScopeSize * index1 + i] = t[nScopeSize * index2 + i];
+          }
+        }
+      } else {
+        if(index2 < 0) {
+          for(int i = 0; i < nScopeSize; i++) {
+            t[nScopeSize * index1 + i] = ones[lww];
+          }
+        } else {
+          for(int i = 0; i < nScopeSize; i++) {
+            t[nScopeSize * index1 + i] = ~t[nScopeSize * index2 + i];
+          }
+        }
+      }
+    } else {
+      word value = 0;
+      if(index2 >= 0) {
+        value = GetValue(index2, lev);
+      }
+      if(fCompl) {
+        value ^= ones[logwidth];
+      }
+      SetValue(index1, lev, value);
+    }
+  }
+
+  void ShiftToMajority(int index, int lev) {
+    assert(index >= 0);
+    int logwidth = nInputs - lev;
+    int count = 0;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      for(int i = 0; i < nScopeSize; i++) {
+        count += bsw(t[nScopeSize * index + i]).count();
+      }
+    } else {
+      count = bsw(GetValue(index, lev)).count();
+    }
+    bool majority = count > (1 << (logwidth - 1));
+    CopyFunc(index, -1, lev, majority);
+  }
+};
+
+class TruthTableCare : public TruthTableRewrite {
+public:
+  std::vector<word> originalt;
+  std::vector<word> caret;
+  std::vector<word> care;
+
+  std::vector<std::vector<std::pair<int, int> > > vvMergedIndices;
+
+  std::vector<std::vector<word> > savedcare;
+  std::vector<std::vector<std::vector<std::pair<int, int> > > > vvMergedIndicesSaved;
+
+  TruthTableCare(int nInputs, int nOutputs): TruthTableRewrite(nInputs, nOutputs) {
+    if(nSize) {
+      care.resize(nSize);
+    } else {
+      care.resize(1);
+    }
+  }
+
+  void Save(uint i) override {
+    TruthTable::Save(i);
+    if(savedcare.size() < i + 1) {
+      savedcare.resize(i + 1);
+    }
+    savedcare[i] = care;
+  }
+
+  void Load(uint i) override {
+    TruthTable::Load(i);
+    care = savedcare[i];
+  }
+
+  void SaveIndices(uint i) override {
+    TruthTable::SaveIndices(i);
+    if(vvMergedIndicesSaved.size() < i + 1) {
+      vvMergedIndicesSaved.resize(i + 1);
+    }
+    vvMergedIndicesSaved[i] = vvMergedIndices;
+  }
+
+  void LoadIndices(uint i) override {
+    TruthTable::LoadIndices(i);
+    vvMergedIndices = vvMergedIndicesSaved[i];
+  }
+
+  void Swap(int lev) override {
+    TruthTable::Swap(lev);
+    if(nInputs - lev - 1 > lww) {
+      int nScopeSize = 1 << (nInputs - lev - 2 - lww);
+      for(int i = nScopeSize; i < nSize; i += (nScopeSize << 2)) {
+        for(int j = 0; j < nScopeSize; j++) {
+          std::swap(care[i + j], care[i + nScopeSize + j]);
+        }
+      }
+    } else if(nInputs - lev - 1 == lww) {
+      for(int i = 0; i < nSize; i += 2) {
+        care[i+1] ^= care[i] >> (ww / 2);
+        care[i] ^= care[i+1] << (ww / 2);
+        care[i+1] ^= care[i] >> (ww / 2);
+      }
+    } else {
+      for(int i = 0; i < nSize || (i == 0 && !nSize); i++) {
+        int d = nInputs - lev - 2;
+        int shamt = 1 << d;
+        care[i] ^= (care[i] >> shamt) & swapmask[d];
+        care[i] ^= (care[i] & swapmask[d]) << shamt;
+        care[i] ^= (care[i] >> shamt) & swapmask[d];
+      }
+    }
+  }
+
+  void RestoreCare() {
+    caret.clear();
+    if(nSize) {
+      for(int i = 0; i < nOutputs; i++) {
+        caret.insert(caret.end(), care.begin(), care.end());
+      }
+    } else {
+      caret.resize(nTotalSize);
+      for(int i = 0; i < nOutputs; i++) {
+        int padding = i * (1 << nInputs);
+        caret[padding / ww] |= care[0] << (padding % ww);
+      }
+    }
+  }
+
+  word GetCare(int index_lev, int lev) {
+    assert(index_lev >= 0);
+    assert(nInputs - lev <= lww);
+    int logwidth = nInputs - lev;
+    int index = index_lev >> (lww - logwidth);
+    int pos = (index_lev % (1 << (lww - logwidth))) << logwidth;
+    return (caret[index] >> pos) & ones[logwidth];
+  }
+
+  void CopyFuncMasked(int index1, int index2, int lev, bool fCompl) {
+    assert(index1 >= 0);
+    assert(index2 >= 0);
+    int logwidth = nInputs - lev;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      for(int i = 0; i < nScopeSize; i++) {
+        word value = t[nScopeSize * index2 + i];
+        if(fCompl) {
+          value = ~value;
+        }
+        word cvalue = caret[nScopeSize * index2 + i];
+        t[nScopeSize * index1 + i] &= ~cvalue;
+        t[nScopeSize * index1 + i] |= cvalue & value;
+      }
+    } else {
+      word one = ones[logwidth];
+      word value1 = GetValue(index1, lev);
+      word value2 = GetValue(index2, lev);
+      if(fCompl) {
+        value2 ^= one;
+      }
+      word cvalue = GetCare(index2, lev);
+      value1 &= cvalue ^ one;
+      value1 |= cvalue & value2;
+      SetValue(index1, lev, value1);
+    }
+  }
+
+  bool IsDC(int index, int lev) {
+    if(nInputs - lev > lww) {
+      int nScopeSize = 1 << (nInputs - lev - lww);
+      for(int i = 0; i < nScopeSize; i++) {
+        if(caret[nScopeSize * index + i]) {
+          return false;
+        }
+      }
+    } else if(GetCare(index, lev)) {
+      return false;
+    }
+    return true;
+  }
+
+  int Include(int index1, int index2, int lev, bool fCompl) {
+    assert(index1 >= 0);
+    assert(index2 >= 0);
+    int logwidth = nInputs - lev;
+    bool fEq = true;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) {
+        word cvalue = caret[nScopeSize * index2 + i];
+        if(~caret[nScopeSize * index1 + i] & cvalue) {
+          return 0;
+        }
+        word value = t[nScopeSize * index1 + i] ^ t[nScopeSize * index2 + i];
+        fEq &= !(value & cvalue);
+        fCompl &= !(~value & cvalue);
+      }
+    } else {
+      word cvalue = GetCare(index2, lev);
+      if((GetCare(index1, lev) ^ ones[logwidth]) & cvalue) {
+        return 0;
+      }
+      word value = GetValue(index1, lev) ^ GetValue(index2, lev);
+      fEq &= !(value & cvalue);
+      fCompl &= !((value ^ ones[logwidth]) & cvalue);
+    }
+    return 2 * fCompl + fEq;
+  }
+
+  int Intersect(int index1, int index2, int lev, bool fCompl, bool fEq = true) {
+    assert(index1 >= 0);
+    assert(index2 >= 0);
+    int logwidth = nInputs - lev;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) {
+        word value = t[nScopeSize * index1 + i] ^ t[nScopeSize * index2 + i];
+        word cvalue = caret[nScopeSize * index1 + i] & caret[nScopeSize * index2 + i];
+        fEq &= !(value & cvalue);
+        fCompl &= !(~value & cvalue);
+      }
+    } else {
+      word value = GetValue(index1, lev) ^ GetValue(index2, lev);
+      word cvalue = GetCare(index1, lev) & GetCare(index2, lev);
+      fEq &= !(value & cvalue);
+      fCompl &= !((value ^ ones[logwidth]) & cvalue);
+    }
+    return 2 * fCompl + fEq;
+  }
+
+  void MergeCare(int index1, int index2, int lev) {
+    assert(index1 >= 0);
+    assert(index2 >= 0);
+    int logwidth = nInputs - lev;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      for(int i = 0; i < nScopeSize; i++) {
+        caret[nScopeSize * index1 + i] |= caret[nScopeSize * index2 + i];
+      }
+    } else {
+      word value = GetCare(index2, lev);
+      int index = index1 >> (lww - logwidth);
+      int pos = (index1 % (1 << (lww - logwidth))) << logwidth;
+      caret[index] |= value << pos;
+    }
+  }
+
+  void Merge(int index1, int index2, int lev, bool fCompl) {
+    MergeCare(index1, index2, lev);
+    vvMergedIndices[lev].push_back({(index1 << 1) ^ fCompl, index2});
+  }
+
+  int BDDBuildOne(int index, int lev) override {
+    int r = BDDFind(index, lev);
+    if(r >= -2) {
+      if(r >= 0) {
+        Merge(vvIndices[lev][r >> 1], index, lev, r & 1);
+      }
+      return r;
+    }
+    vvIndices[lev].push_back(index);
+    return (vvIndices[lev].size() - 1) << 1;
+  }
+
+  void CompleteMerge() {
+    for(int i = nInputs - 1; i >= 0; i--) {
+      for(auto it = vvMergedIndices[i].rbegin(); it != vvMergedIndices[i].rend(); it++) {
+        CopyFunc((*it).second, (*it).first >> 1, i, (*it).first & 1);
+      }
+    }
+  }
+
+  void BDDBuildStartup() override {
+    RestoreCare();
+    vvIndices.clear();
+    vvIndices.resize(nInputs);
+    vvRedundantIndices.clear();
+    vvRedundantIndices.resize(nInputs);
+    vvMergedIndices.clear();
+    vvMergedIndices.resize(nInputs);
+    for(int i = 0; i < nOutputs; i++) {
+      if(!IsDC(i, 0)) {
+        BDDBuildOne(i, 0);
+      }
+    }
+  }
+
+  virtual void BDDRebuildByMerge(int lev) {
+    for(auto &p: vvMergedIndices[lev]) {
+      MergeCare(p.first >> 1, p.second, lev);
+    }
+  }
+
+  int BDDRebuild(int lev) override {
+    RestoreCare();
+    for(int i = lev; i < nInputs; i++) {
+      vvIndices[i].clear();
+      vvMergedIndices[i].clear();
+      if(i) {
+        vvRedundantIndices[i-1].clear();
+      }
+    }
+    for(int i = 0; i < lev; i++) {
+      BDDRebuildByMerge(i);
+    }
+    for(int i = lev; i < nInputs; i++) {
+      if(!i) {
+        for(int j = 0; j < nOutputs; j++) {
+          if(!IsDC(j, 0)) {
+            BDDBuildOne(j, 0);
+          }
+        }
+      } else {
+        BDDBuildLevel(i);
+      }
+    }
+    return BDDNodeCount();
+  }
+
+  int BDDSwap(int lev) override {
+    Swap(lev);
+    return BDDRebuild(lev);
+  }
+
+  void OptimizationStartup() {
+    originalt = t;
+    RestoreCare();
+    vvIndices.clear();
+    vvIndices.resize(nInputs);
+    vvMergedIndices.clear();
+    vvMergedIndices.resize(nInputs);
+    for(int i = 0; i < nOutputs; i++) {
+      if(!IsDC(i, 0)) {
+        BDDBuildOne(i, 0);
+      } else {
+        ShiftToMajority(i, 0);
+      }
+    }
+  }
+
+  virtual void Optimize() {
+    OptimizationStartup();
+    for(int i = 1; i < nInputs; i++) {
+      for(int index: vvIndices[i-1]) {
+        BDDBuildOne(index << 1, i);
+        BDDBuildOne((index << 1) ^ 1, i);
+      }
+    }
+    CompleteMerge();
+  }
+};
+
+class TruthTableLevelTSM : public TruthTableCare {
+public:
+  TruthTableLevelTSM(int nInputs, int nOutputs): TruthTableCare(nInputs, nOutputs) {}
+
+  int BDDFindTSM(int index, int lev) {
+    int logwidth = nInputs - lev;
+    if(logwidth > lww) {
+      int nScopeSize = 1 << (logwidth - lww);
+      bool fZero = true;
+      bool fOne = true;
+      for(int i = 0; i < nScopeSize && (fZero || fOne); i++) {
+        word value = t[nScopeSize * index + i];
+        word cvalue = caret[nScopeSize * index + i];
+        fZero &= !(value & cvalue);
+        fOne &= !(~value & cvalue);
+      }
+      if(fZero || fOne) {
+        return -2 ^ fOne;
+      }
+      for(int index2: vvIndices[lev]) {
+        bool fEq = true;
+        bool fCompl = true;
+        for(int i = 0; i < nScopeSize && (fEq || fCompl); i++) {
+          word value = t[nScopeSize * index + i] ^ t[nScopeSize * index2 + i];
+          word cvalue = caret[nScopeSize * index + i] & caret[nScopeSize * index2 + i];
+          fEq &= !(value & cvalue);
+          fCompl &= !(~value & cvalue);
+        }
+        if(fEq || fCompl) {
+          return (index2 << 1) ^ !fEq;
+        }
+      }
+    } else {
+      word one = ones[logwidth];
+      word value = GetValue(index, lev);
+      word cvalue = GetCare(index, lev);
+      if(!(value & cvalue)) {
+        return -2;
+      }
+      if(!((value ^ one) & cvalue)) {
+        return -1;
+      }
+      for(int index2: vvIndices[lev]) {
+        word value2 = value ^ GetValue(index2, lev);
+        word cvalue2 = cvalue & GetCare(index2, lev);
+        if(!(value2 & cvalue2)) {
+          return index2 << 1;
+        }
+        if(!((value2 ^ one) & cvalue2)) {
+          return (index2 << 1) ^ 1;
+        }
+      }
+    }
+    return -3;
+  }
+
+  int BDDBuildOne(int index, int lev) override {
+    int r = BDDFindTSM(index, lev);
+    if(r >= -2) {
+      if(r >= 0) {
+        CopyFuncMasked(r >> 1, index, lev, r & 1);
+        Merge(r >> 1, index, lev, r & 1);
+      } else {
+        vvMergedIndices[lev].push_back({r, index});
+      }
+      return r;
+    }
+    vvIndices[lev].push_back(index);
+    return index << 1;
+  }
+
+  int BDDBuild() override {
+    TruthTable::Save(3);
+    int r = TruthTable::BDDBuild();
+    TruthTable::Load(3);
+    return r;
+  }
+
+  void BDDRebuildByMerge(int lev) override {
+    for(auto &p: vvMergedIndices[lev]) {
+      if(p.first >= 0) {
+        CopyFuncMasked(p.first >> 1, p.second, lev, p.first & 1);
+        MergeCare(p.first >> 1, p.second, lev);
+      }
+    }
+  }
+
+  int BDDRebuild(int lev) override {
+    TruthTable::Save(3);
+    int r = TruthTableCare::BDDRebuild(lev);
+    TruthTable::Load(3);
+    return r;
+  }
+};
+
+}
+
+extern "C"
+Vec_Int_t * Gia_ManCollectSuppNew( Gia_Man_t * p, int iOut, int nOuts );
+
+extern "C"
+Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vSupp;
+    word v;
+    word * pTruth;
+    int i, g, k, nInputs;
+    Gia_ManLevelNum( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManForEachCi( p, pObj, k )
+        Gia_ManAppendCi( pNew );
+    Gia_ObjComputeTruthTableStart( p, nIns );
+    Gia_ManHashStart( pNew );
+    for ( g = 0; g < Gia_ManCoNum(p); g += nOuts )
+    {
+        vSupp = Gia_ManCollectSuppNew( p, g, nOuts );
+        nInputs = Vec_IntSize( vSupp );
+        Ttopt::TruthTableReo tt( nInputs, nOuts );
+        for ( k = 0; k < nOuts; k++ )
+        {
+            pObj = Gia_ManCo( p, g+k );
+            pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ObjFanin0(pObj), vSupp );
+            if ( nInputs >= 6 )
+                for ( i = 0; i < tt.nSize; i++ )
+                    tt.t[i + tt.nSize * k] = Gia_ObjFaninC0(pObj)? ~pTruth[i]: pTruth[i];
+            else
+            {
+                i = k * (1 << nInputs);
+                v = (Gia_ObjFaninC0(pObj)? ~pTruth[0]: pTruth[0]) & tt.ones[nInputs];
+                tt.t[i / tt.ww] |= v << (i % tt.ww);
+            }
+        }
+        tt.RandomSiftReo( nRounds );
+        Ttopt::TruthTable tt2( nInputs, nOuts );
+        tt2.t = tt.t;
+        tt2.Reo( tt.vLevels );
+        tt2.BDDGenerateAig( pNew, vSupp );
+        Vec_IntFree( vSupp );
+    }
+    Gia_ObjComputeTruthTableStop( p );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+extern "C"
+word * Gia_ManCountFraction( Gia_Man_t * p, Vec_Wrd_t * vSimI, Vec_Int_t * vSupp, int Thresh, int fVerbose, int * pCare );
+
+extern "C"
+Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity )
+{
+    int fVerbose = 0;
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vSupp;
+    word v;
+    word * pTruth, * pCare;
+    int i, g, k, nInputs;
+    Vec_Wrd_t * vSimI = Vec_WrdReadBin( pFileName, fVerbose );
+    Gia_ManLevelNum( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManForEachCi( p, pObj, k )
+        Gia_ManAppendCi( pNew );
+    Gia_ObjComputeTruthTableStart( p, nIns );
+    Gia_ManHashStart( pNew );
+    for ( g = 0; g < Gia_ManCoNum(p); g += nOuts )
+    {
+        vSupp = Gia_ManCollectSuppNew( p, g, nOuts );
+        nInputs = Vec_IntSize( vSupp );
+        Ttopt::TruthTableLevelTSM tt( nInputs, nOuts );
+        for ( k = 0; k < nOuts; k++ )
+        {
+            pObj = Gia_ManCo( p, g+k );
+            pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ObjFanin0(pObj), vSupp );
+            if ( nInputs >= 6 )
+                for ( i = 0; i < tt.nSize; i++ )
+                    tt.t[i + tt.nSize * k] = Gia_ObjFaninC0(pObj)? ~pTruth[i]: pTruth[i];
+            else
+            {
+                i = k * (1 << nInputs);
+                v = (Gia_ObjFaninC0(pObj)? ~pTruth[0]: pTruth[0]) & tt.ones[nInputs];
+                tt.t[i / tt.ww] |= v << (i % tt.ww);
+            }
+        }
+        i = 1 << Vec_IntSize( vSupp );
+        pCare = Gia_ManCountFraction( p, vSimI, vSupp, nRarity, fVerbose, &i );
+        tt.care[0] = pCare[0];
+        for ( i = 1; i < tt.nSize; i++ )
+            tt.care[i] = pCare[i];
+        ABC_FREE( pCare );
+        tt.RandomSiftReo( nRounds );
+        tt.Optimize();
+        tt.BDDGenerateAig( pNew, vSupp );
+        Vec_IntFree( vSupp );
+    }
+    Gia_ObjComputeTruthTableStop( p );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    Vec_WrdFreeP( &vSimI );
+    return pNew;
+}
+
+ABC_NAMESPACE_IMPL_END

src/aig/gia/module.make

@@ -105,5 +105,6 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaTis.c \
     src/aig/gia/giaTruth.c \
     src/aig/gia/giaTsim.c \
+    src/aig/gia/giaTtopt.cpp \
     src/aig/gia/giaUnate.c \
     src/aig/gia/giaUtil.c

src/base/abci/abc.c

@@ -499,6 +499,7 @@ static int Abc_CommandAbc9LNetRead           ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9LNetSim            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9LNetEval           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9LNetOpt            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Ttopt              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9LNetMap            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Unmap              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Struct             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1249,6 +1250,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&lnetsim",      Abc_CommandAbc9LNetSim,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&lneteval",     Abc_CommandAbc9LNetEval,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&lnetopt",      Abc_CommandAbc9LNetOpt,      0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&ttopt",        Abc_CommandAbc9Ttopt,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&lnetmap",      Abc_CommandAbc9LNetMap,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&unmap",        Abc_CommandAbc9Unmap,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&struct",       Abc_CommandAbc9Struct,       0 );
@@ -42202,6 +42204,113 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Ttopt( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds );
+    extern Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity );
+    Gia_Man_t * pTemp;
+    char * pFileName = NULL;
+    int c, nIns = 6, nOuts = 2, Limit = 0, nRounds = 20, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "IORXvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nIns = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'O':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-O\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nOuts = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-R\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            Limit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'X':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-X\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nRounds = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+        default:
+            goto usage;
+        }
+    }
+    if ( argc > globalUtilOptind + 1 )
+    {
+        return 0;
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Empty GIA network.\n" );
+        return 1;
+    }
+    if ( argc == globalUtilOptind + 1 )
+    {
+        FILE * pFile = fopen( argv[globalUtilOptind], "rb" );
+        if ( pFile == NULL )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9BCore(): Cannot open file \"%s\" for reading the simulation information.\n", argv[globalUtilOptind] );
+            return 0;
+        }
+        fclose( pFile );
+        pFileName = argv[globalUtilOptind];
+    }
+    if ( pFileName )
+        pTemp = Gia_ManTtoptCare( pAbc->pGia, nIns, nOuts, nRounds, pFileName, Limit );
+    else
+        pTemp = Gia_ManTtopt( pAbc->pGia, nIns, nOuts, nRounds );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &ttopt [-IORX num] [-vh] <file>\n" );
+    Abc_Print( -2, "\t           performs specialized AIG optimization\n" );
+    Abc_Print( -2, "\t-I num   : the input support size [default = %d]\n",                 nIns );
+    Abc_Print( -2, "\t-O num   : the output group size [default = %d]\n",                  nOuts );
+    Abc_Print( -2, "\t-R num   : patterns are cares starting this value [default = %d]\n", Limit );
+    Abc_Print( -2, "\t-X num   : the number of optimization rounds [default = %d]\n",      nRounds );
+    Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n",                 fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : prints the command usage\n");
+    Abc_Print( -2, "\t<file>   : file name with simulation information\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9LNetMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Abc_Ntk_t * Gia_ManPerformLNetMap( Gia_Man_t * p, int GroupSize, int fUseFixed, int fTryNew, int fVerbose );