transduction

src/aig/gia/gia.h

@@ -1769,10 +1769,14 @@ extern int                 Gia_ManCountPosWithNonZeroDrivers( Gia_Man_t * p );
 extern void                Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManComputeDistance( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, int fVerbose );
 
-/*=== giaTtopt.c ===========================================================*/
+/*=== giaTtopt.cpp ===========================================================*/
 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 );
 
+/*=== giaTransduction.cpp ===========================================================*/
+extern Gia_Man_t *         Gia_ManTransductionBdd( Gia_Man_t * pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t * pExdc, int nVerbose );
+extern Gia_Man_t *         Gia_ManTransductionTt( Gia_Man_t * pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t * pExdc, int nVerbose );
+
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
 extern Tas_Man_t *         Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );

src/aig/gia/giaNewBdd.h

+#ifndef ABC__aig__gia__giaNewBdd_h
+#define ABC__aig__gia__giaNewBdd_h
+
+#include <limits>
+#include <vector>
+#include <iostream>
+#include <iomanip>
+#include <cmath>
+
+namespace NewBdd {
+
+  typedef unsigned short     var;
+  typedef int                bvar;
+  typedef unsigned           lit;
+  typedef unsigned short     ref;
+  typedef unsigned long long size;
+  typedef unsigned           edge;
+  typedef unsigned           uniq;
+  typedef unsigned           cac;
+  static inline var  VarMax()                     { return std::numeric_limits<var>::max();  }
+  static inline bvar BvarMax()                    { return std::numeric_limits<bvar>::max(); }
+  static inline lit  LitMax()                     { return std::numeric_limits<lit>::max();  }
+  static inline ref  RefMax()                     { return std::numeric_limits<ref>::max();  }
+  static inline size SizeMax()                    { return std::numeric_limits<size>::max(); }
+  static inline uniq UniqHash(lit Arg0, lit Arg1) { return Arg0 + 4256249 * Arg1;            }
+  static inline cac  CacHash(lit Arg0, lit Arg1)  { return Arg0 + 4256249 * Arg1;            }
+
+  class Cache {
+  private:
+    cac    nSize;
+    cac    nMax;
+    cac    Mask;
+    size   nLookups;
+    size   nHits;
+    size   nThold;
+    double HitRate;
+    int    nVerbose;
+    std::vector<lit> vCache;
+
+  public:
+    Cache(int nCacheSizeLog, int nCacheMaxLog, int nVerbose): nVerbose(nVerbose) {
+      if(nCacheMaxLog < nCacheSizeLog)
+        throw std::invalid_argument("nCacheMax must not be smaller than nCacheSize");
+      nMax = (cac)1 << nCacheMaxLog;
+      if(!(nMax << 1))
+        throw std::length_error("Memout (nCacheMax) in init");
+      nSize = (cac)1 << nCacheSizeLog;
+      if(nVerbose)
+        std::cout << "Allocating " << nSize << " cache entries" << std::endl;
+      vCache.resize(nSize * 3);
+      Mask = nSize - 1;
+      nLookups = 0;
+      nHits = 0;
+      nThold = (nSize == nMax)? SizeMax(): nSize;
+      HitRate = 1;
+    }
+    ~Cache() {
+      if(nVerbose)
+        std::cout << "Free " << nSize << " cache entries" << std::endl;
+    }
+    inline lit Lookup(lit x, lit y) {
+      nLookups++;
+      if(nLookups > nThold) {
+        double NewHitRate = (double)nHits / nLookups;
+        if(nVerbose >= 2)
+          std::cout << "Cache Hits: " << std::setw(10) << nHits << ", "
+                    << "Lookups: " << std::setw(10) << nLookups << ", "
+                    << "Rate: " << std::setw(10) << NewHitRate
+                    << std::endl;
+        if(NewHitRate > HitRate)
+          Resize();
+        if(nSize == nMax)
+          nThold = SizeMax();
+        else {
+          nThold <<= 1;
+          if(!nThold)
+            nThold = SizeMax();
+        }
+        HitRate = NewHitRate;
+      }
+      cac i = (CacHash(x, y) & Mask) * 3;
+      if(vCache[i] == x && vCache[i + 1] == y) {
+        if(nVerbose >= 3)
+          std::cout << "Cache hit: "
+                    << "x = " << std::setw(10) << x << ", "
+                    << "y = " << std::setw(10) << y << ", "
+                    << "z = " << std::setw(10) << vCache[i + 2] << ", "
+                    << "hash = " << std::hex << (CacHash(x, y) & Mask) << std::dec
+                    << std::endl;
+        nHits++;
+        return vCache[i + 2];
+      }
+      return LitMax();
+    }
+    inline void Insert(lit x, lit y, lit z) {
+      cac i = (CacHash(x, y) & Mask) * 3;
+      vCache[i] = x;
+      vCache[i + 1] = y;
+      vCache[i + 2] = z;
+      if(nVerbose >= 3)
+        std::cout << "Cache ent: "
+                  << "x = " << std::setw(10) << x << ", "
+                  << "y = " << std::setw(10) << y << ", "
+                  << "z = " << std::setw(10) << z << ", "
+                  << "hash = " << std::hex << (CacHash(x, y) & Mask) << std::dec
+                  << std::endl;
+    }
+    inline void Clear() {
+      std::fill(vCache.begin(), vCache.end(), 0);
+    }
+    void Resize() {
+      cac nSizeOld = nSize;
+      nSize <<= 1;
+      if(nVerbose >= 2)
+        std::cout << "Reallocating " << nSize << " cache entries" << std::endl;
+      vCache.resize(nSize * 3);
+      Mask = nSize - 1;
+      for(cac j = 0; j < nSizeOld; j++) {
+        cac i = j * 3;
+        if(vCache[i] || vCache[i + 1]) {
+          cac hash = (CacHash(vCache[i], vCache[i + 1]) & Mask) * 3;
+          vCache[hash] = vCache[i];
+          vCache[hash + 1] = vCache[i + 1];
+          vCache[hash + 2] = vCache[i + 2];
+          if(nVerbose >= 3)
+            std::cout << "Cache mov: "
+                      << "x = " << std::setw(10) << vCache[i] << ", "
+                      << "y = " << std::setw(10) << vCache[i + 1] << ", "
+                      << "z = " << std::setw(10) << vCache[i + 2] << ", "
+                      << "hash = " << std::hex << (CacHash(vCache[i], vCache[i + 1]) & Mask) << std::dec
+                      << std::endl;
+        }
+      }
+    }
+  };
+
+  struct Param {
+    int    nObjsAllocLog  = 20;
+    int    nObjsMaxLog    = 25;
+    int    nUniqueSizeLog = 10;
+    double UniqueDensity  = 4;
+    int    nCacheSizeLog  = 15;
+    int    nCacheMaxLog   = 20;
+    int    nCacheVerbose  = 0;
+    bool   fCountOnes     = false;
+    int    nGbc           = 0;
+    bvar   nReo           = BvarMax();
+    double MaxGrowth      = 1.2;
+    bool   fReoVerbose    = false;
+    int    nVerbose       = 0;
+    std::vector<var> *pVar2Level = NULL;
+  };
+
+  class Man {
+  private:
+    var    nVars;
+    bvar   nObjs;
+    bvar   nObjsAlloc;
+    bvar   nObjsMax;
+    bvar   RemovedHead;
+    int    nGbc;
+    bvar   nReo;
+    double MaxGrowth;
+    bool   fReoVerbose;
+    int    nVerbose;
+    std::vector<var>    vVars;
+    std::vector<var>    Var2Level;
+    std::vector<var>    Level2Var;
+    std::vector<lit>    vObjs;
+    std::vector<bvar>   vNexts;
+    std::vector<bool>   vMarks;
+    std::vector<ref>    vRefs;
+    std::vector<edge>   vEdges;
+    std::vector<double> vOneCounts;
+    std::vector<uniq>   vUniqueMasks;
+    std::vector<bvar>   vUniqueCounts;
+    std::vector<bvar>   vUniqueTholds;
+    std::vector<std::vector<bvar> > vvUnique;
+    Cache *cache;
+
+  public:
+    inline lit  Bvar2Lit(bvar a)          const { return (lit)a << 1;                                       }
+    inline lit  Bvar2Lit(bvar a, bool c)  const { return ((lit)a << 1) ^ (lit)c;                            }
+    inline bvar Lit2Bvar(lit x)           const { return (bvar)(x >> 1);                                    }
+    inline var  VarOfBvar(bvar a)         const { return vVars[a];                                          }
+    inline lit  ThenOfBvar(bvar a)        const { return vObjs[Bvar2Lit(a)];                                }
+    inline lit  ElseOfBvar(bvar a)        const { return vObjs[Bvar2Lit(a, true)];                          }
+    inline ref  RefOfBvar(bvar a)         const { return vRefs[a];                                          }
+    inline lit  Const0()                  const { return (lit)0;                                            }
+    inline lit  Const1()                  const { return (lit)1;                                            }
+    inline bool IsConst0(lit x)           const { return x == Const0();                                     }
+    inline bool IsConst1(lit x)           const { return x == Const1();                                     }
+    inline lit  IthVar(var v)             const { return Bvar2Lit((bvar)v + 1);                             }
+    inline lit  LitRegular(lit x)         const { return x & ~(lit)1;                                       }
+    inline lit  LitIrregular(lit x)       const { return x | (lit)1;                                        }
+    inline lit  LitNot(lit x)             const { return x ^ (lit)1;                                        }
+    inline lit  LitNotCond(lit x, bool c) const { return x ^ (lit)c;                                        }
+    inline bool LitIsCompl(lit x)         const { return x & (lit)1;                                        }
+    inline bool LitIsEq(lit x, lit y)     const { return x == y;                                            }
+    inline var  Var(lit x)                const { return vVars[Lit2Bvar(x)];                                }
+    inline var  Level(lit x)              const { return Var2Level[Var(x)];                                 }
+    inline lit  Then(lit x)               const { return LitNotCond(vObjs[LitRegular(x)], LitIsCompl(x));   }
+    inline lit  Else(lit x)               const { return LitNotCond(vObjs[LitIrregular(x)], LitIsCompl(x)); }
+    inline ref  Ref(lit x)                const { return vRefs[Lit2Bvar(x)];                                }
+    inline double OneCount(lit x)         const {
+      if(vOneCounts.empty())
+        throw std::logic_error("fCountOnes was not set");
+      if(LitIsCompl(x))
+        return std::pow(2.0, nVars) - vOneCounts[Lit2Bvar(x)];
+      return vOneCounts[Lit2Bvar(x)];
+    }
+
+  public:
+    inline void IncRef(lit x)              { if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]++; }
+    inline void DecRef(lit x)              { if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]--; }
+
+  private:
+    inline bool Mark(lit x)               const { return vMarks[Lit2Bvar(x)];                               }
+    inline edge Edge(lit x)               const { return vEdges[Lit2Bvar(x)];                               }
+    inline void SetMark(lit x)                  { vMarks[Lit2Bvar(x)] = true;                               }
+    inline void ResetMark(lit x)                { vMarks[Lit2Bvar(x)] = false;                              }
+    inline void IncEdge(lit x)                  { vEdges[Lit2Bvar(x)]++;                                    }
+    inline void DecEdge(lit x)                  { vEdges[Lit2Bvar(x)]--;                                    }
+    inline bool MarkOfBvar(bvar a)        const { return vMarks[a];                                         }
+    inline edge EdgeOfBvar(bvar a)        const { return vEdges[a];                                         }
+    inline void SetVarOfBvar(bvar a, var v)     { vVars[a] = v;                                             }
+    inline void SetThenOfBvar(bvar a, lit x)    { vObjs[Bvar2Lit(a)] = x;                                   }
+    inline void SetElseOfBvar(bvar a, lit x)    { vObjs[Bvar2Lit(a, true)] = x;                             }
+    inline void SetMarkOfBvar(bvar a)           { vMarks[a] = true;                                         }
+    inline void ResetMarkOfBvar(bvar a)         { vMarks[a] = false;                                        }
+    inline void RemoveBvar(bvar a)              {
+      var v = VarOfBvar(a);
+      SetVarOfBvar(a, VarMax());
+      std::vector<bvar>::iterator q = vvUnique[v].begin() + (UniqHash(ThenOfBvar(a), ElseOfBvar(a)) & vUniqueMasks[v]);
+      for(; *q; q = vNexts.begin() + *q)
+        if(*q == a)
+          break;
+      bvar next = vNexts[*q];
+      vNexts[*q] = RemovedHead;
+      RemovedHead = *q;
+      *q = next;
+      vUniqueCounts[v]--;
+    }
+
+  private:
+    void SetMark_rec(lit x) {
+      if(x < 2 || Mark(x))
+        return;
+      SetMark(x);
+      SetMark_rec(Then(x));
+      SetMark_rec(Else(x));
+    }
+    void ResetMark_rec(lit x) {
+      if(x < 2 || !Mark(x))
+        return;
+      ResetMark(x);
+      ResetMark_rec(Then(x));
+      ResetMark_rec(Else(x));
+    }
+    bvar CountNodes_rec(lit x) {
+      if(x < 2 || Mark(x))
+        return 0;
+      SetMark(x);
+      return 1 + CountNodes_rec(Then(x)) + CountNodes_rec(Else(x));
+    }
+    void CountEdges_rec(lit x) {
+      if(x < 2)
+        return;
+      IncEdge(x);
+      if(Mark(x))
+        return;
+      SetMark(x);
+      CountEdges_rec(Then(x));
+      CountEdges_rec(Else(x));
+    }
+    void CountEdges() {
+      vEdges.resize(nObjsAlloc);
+      for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
+        if(RefOfBvar(a))
+          CountEdges_rec(Bvar2Lit(a));
+      for(bvar a = 1; a <= (bvar)nVars; a++)
+        vEdges[a]++;
+      for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
+        if(RefOfBvar(a))
+          ResetMark_rec(Bvar2Lit(a));
+    }
+
+  public:
+    bool Resize() {
+      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;
+    }
+    void ResizeUnique(var v) {
+      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();
+    }
+    bool Gbc() {
+      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;
+    }
+
+  private:
+    inline lit UniqueCreateInt(var v, lit x1, lit x0) {
+      std::vector<bvar>::iterator p, q;
+      p = q = vvUnique[v].begin() + (UniqHash(x1, x0) & vUniqueMasks[v]);
+      for(; *q; q = vNexts.begin() + *q)
+        if(VarOfBvar(*q) == v && ThenOfBvar(*q) == x1 && ElseOfBvar(*q) == x0)
+          return Bvar2Lit(*q);
+      bvar next = *p;
+      if(nObjs < nObjsAlloc)
+        *p = nObjs++;
+      else if(RemovedHead)
+        *p = RemovedHead, RemovedHead = vNexts[*p];
+      else
+        return LitMax();
+      SetVarOfBvar(*p, v);
+      SetThenOfBvar(*p, x1);
+      SetElseOfBvar(*p, x0);
+      vNexts[*p] = next;
+      if(!vOneCounts.empty())
+        vOneCounts[*p] = OneCount(x1) / 2 + OneCount(x0) / 2;
+      if(nVerbose >= 3) {
+        std::cout << "Create node " << std::setw(10) << *p << ": "
+                  << "Var = " << std::setw(6) << v << ", "
+                  << "Then = " << std::setw(10) << x1 << ", "
+                  << "Else = " << std::setw(10) << x0;
+        if(!vOneCounts.empty())
+          std::cout << ", Ones = " << std::setw(10) << vOneCounts[*q];
+        std::cout << std::endl;
+      }
+      vUniqueCounts[v]++;
+      if(vUniqueCounts[v] > vUniqueTholds[v]) {
+        bvar a = *p;
+        ResizeUnique(v);
+        return Bvar2Lit(a);
+      }
+      return Bvar2Lit(*p);
+    }
+    inline lit UniqueCreate(var v, lit x1, lit x0) {
+      if(x1 == x0)
+        return x1;
+      lit x;
+      while(true) {
+        if(!LitIsCompl(x0))
+          x = UniqueCreateInt(v, x1, x0);
+        else
+          x = UniqueCreateInt(v, LitNot(x1), LitNot(x0));
+        if(x == LitMax()) {
+          bool fRemoved = false;
+          if(nGbc > 1)
+            fRemoved = Gbc();
+          if(!Resize() && !fRemoved && (nGbc != 1 || !Gbc()))
+            throw std::length_error("Memout (node)");
+        } else
+          break;
+      }
+      return LitIsCompl(x0)? LitNot(x): x;
+    }
+    lit And_rec(lit x, lit y) {
+      if(x == 0 || y == 1)
+        return x;
+      if(x == 1 || y == 0)
+        return y;
+      if(Lit2Bvar(x) == Lit2Bvar(y))
+        return (x == y)? x: 0;
+      if(x > y)
+        std::swap(x, y);
+      lit z = cache->Lookup(x, y);
+      if(z != LitMax())
+        return z;
+      var v;
+      lit x0, x1, y0, y1;
+      if(Level(x) < Level(y))
+        v = Var(x), x1 = Then(x), x0 = Else(x), y0 = y1 = y;
+      else if(Level(x) > Level(y))
+        v = Var(y), x0 = x1 = x, y1 = Then(y), y0 = Else(y);
+      else
+        v = Var(x), x1 = Then(x), x0 = Else(x), y1 = Then(y), y0 = Else(y);
+      lit z1 = And_rec(x1, y1);
+      IncRef(z1);
+      lit z0 = And_rec(x0, y0);
+      IncRef(z0);
+      z = UniqueCreate(v, z1, z0);
+      DecRef(z1);
+      DecRef(z0);
+      cache->Insert(x, y, z);
+      return z;
+    }
+
+  private:
+    bvar Swap(var i) {
+      var v1 = Level2Var[i];
+      var v2 = Level2Var[i + 1];
+      bvar f = 0;
+      bvar diff = 0;
+      for(std::vector<bvar>::iterator p = vvUnique[v1].begin(); p != vvUnique[v1].end(); p++) {
+        std::vector<bvar>::iterator q = p;
+        while(*q) {
+          if(!EdgeOfBvar(*q)) {
+            SetVarOfBvar(*q, VarMax());
+            bvar next = vNexts[*q];
+            vNexts[*q] = RemovedHead;
+            RemovedHead = *q;
+            *q = next;
+            vUniqueCounts[v1]--;
+            continue;
+          }
+          lit f1 = ThenOfBvar(*q);
+          lit f0 = ElseOfBvar(*q);
+          if(Var(f1) == v2 || Var(f0) == v2) {
+            DecEdge(f1);
+            if(Var(f1) == v2 && !Edge(f1))
+              DecEdge(Then(f1)), DecEdge(Else(f1)), diff--;
+            DecEdge(f0);
+            if(Var(f0) == v2 && !Edge(f0))
+              DecEdge(Then(f0)), DecEdge(Else(f0)), diff--;
+            bvar next = vNexts[*q];
+            vNexts[*q] = f;
+            f = *q;
+            *q = next;
+            vUniqueCounts[v1]--;
+            continue;
+          }
+          q = vNexts.begin() + *q;
+        }
+      }
+      while(f) {
+        lit f1 = ThenOfBvar(f);
+        lit f0 = ElseOfBvar(f);
+        lit f00, f01, f10, f11;
+        if(Var(f1) == v2)
+          f11 = Then(f1), f10 = Else(f1);
+        else
+          f10 = f11 = f1;
+        if(Var(f0) == v2)
+          f01 = Then(f0), f00 = Else(f0);
+        else
+          f00 = f01 = f0;
+        if(f11 == f01)
+          f1 = f11;
+        else {
+          f1 = UniqueCreate(v1, f11, f01);
+          if(!Edge(f1))
+            IncEdge(f11), IncEdge(f01), diff++;
+        }
+        IncEdge(f1);
+        IncRef(f1);
+        if(f10 == f00)
+          f0 = f10;
+        else {
+          f0 = UniqueCreate(v1, f10, f00);
+          if(!Edge(f0))
+            IncEdge(f10), IncEdge(f00), diff++;
+        }
+        IncEdge(f0);
+        DecRef(f1);
+        SetVarOfBvar(f, v2);
+        SetThenOfBvar(f, f1);
+        SetElseOfBvar(f, f0);
+        std::vector<bvar>::iterator q = vvUnique[v2].begin() + (UniqHash(f1, f0) & vUniqueMasks[v2]);
+        lit next = vNexts[f];
+        vNexts[f] = *q;
+        *q = f;
+        vUniqueCounts[v2]++;
+        f = next;
+      }
+      Var2Level[v1] = i + 1;
+      Var2Level[v2] = i;
+      Level2Var[i] = v2;
+      Level2Var[i + 1] = v1;
+      return diff;
+    }
+    void Sift() {
+      bvar count = CountNodes();
+      std::vector<var> sift_order(nVars);
+      for(var v = 0; v < nVars; v++)
+        sift_order[v] = v;
+      for(var i = 0; i < nVars; i++) {
+        var max_j = i;
+        for(var j = i + 1; j < nVars; j++)
+          if(vUniqueCounts[sift_order[j]] > vUniqueCounts[sift_order[max_j]])
+            max_j = j;
+        if(max_j != i)
+          std::swap(sift_order[max_j], sift_order[i]);
+      }
+      for(var v = 0; v < nVars; v++) {
+        bvar lev = Var2Level[sift_order[v]];
+        bool UpFirst = lev < (bvar)(nVars / 2);
+        bvar min_lev = lev;
+        bvar min_diff = 0;
+        bvar diff = 0;
+        bvar thold = count * (MaxGrowth - 1);
+        if(fReoVerbose)
+          std::cout << "Sift " << sift_order[v] << " : Level = " << lev << " Count = " << count << " Thold = " << thold << std::endl;
+        if(UpFirst) {
+          lev--;
+          for(; lev >= 0; lev--) {
+            diff += Swap(lev);
+            if(fReoVerbose)
+              std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
+            if(diff < min_diff)
+              min_lev = lev, min_diff = diff, thold = (count + diff) * (MaxGrowth - 1);
+            else if(diff > thold) {
+              lev--;
+              break;
+            }
+          }
+          lev++;
+        }
+        for(; lev < (bvar)nVars - 1; lev++) {
+          diff += Swap(lev);
+          if(fReoVerbose)
+            std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
+          if(diff <= min_diff)
+            min_lev = lev + 1, min_diff = diff, thold = (count + diff) * (MaxGrowth - 1);
+          else if(diff > thold) {
+            lev++;
+            break;
+          }
+        }
+        lev--;
+        if(UpFirst) {
+          for(; lev >= min_lev; lev--) {
+            diff += Swap(lev);
+            if(fReoVerbose)
+              std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
+          }
+        } else {
+          for(; lev >= 0; lev--) {
+            diff += Swap(lev);
+            if(fReoVerbose)
+              std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
+            if(diff <= min_diff)
+              min_lev = lev, min_diff = diff, thold = (count + diff) * (MaxGrowth - 1);
+            else if(diff > thold) {
+              lev--;
+              break;
+            }
+          }
+          lev++;
+          for(; lev < min_lev; lev++) {
+            diff += Swap(lev);
+            if(fReoVerbose)
+              std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
+          }
+        }
+        count += min_diff;
+        if(fReoVerbose)
+          std::cout << "Sifted " << sift_order[v] << " : Level = " << min_lev << " Count = " << count << " Thold = " << thold << std::endl;
+      }
+    }
+
+  public:
+    Man(int nVars_, Param p) {
+      nVerbose = p.nVerbose;
+      // parameter sanity check
+      if(p.nObjsMaxLog < p.nObjsAllocLog)
+        throw std::invalid_argument("nObjsMax must not be smaller than nObjsAlloc");
+      if(nVars_ >= (int)VarMax())
+        throw std::length_error("Memout (nVars) in init");
+      nVars = nVars_;
+      lit nObjsMaxLit = (lit)1 << p.nObjsMaxLog;
+      if(!nObjsMaxLit)
+        throw std::length_error("Memout (nObjsMax) in init");
+      if(nObjsMaxLit > (lit)BvarMax())
+        nObjsMax = BvarMax();
+      else
+        nObjsMax = (bvar)nObjsMaxLit;
+      lit nObjsAllocLit = (lit)1 << p.nObjsAllocLog;
+      if(!nObjsAllocLit)
+        throw std::length_error("Memout (nObjsAlloc) in init");
+      if(nObjsAllocLit > (lit)BvarMax())
+        nObjsAlloc = BvarMax();
+      else
+        nObjsAlloc = (bvar)nObjsAllocLit;
+      if(nObjsAlloc <= (bvar)nVars)
+        throw std::invalid_argument("nObjsAlloc must be larger than nVars");
+      uniq nUniqueSize = (uniq)1 << p.nUniqueSizeLog;
+      if(!nUniqueSize)
+        throw std::length_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)
+          throw std::length_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() {
+      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;
+    }
+    void Reorder() {
+      if(nVerbose >= 2)
+        std::cout << "Reorder" << std::endl;
+      int nGbc_ = nGbc;
+      nGbc = 0;
+      CountEdges();
+      Sift();
+      vEdges.clear();
+      cache->Clear();
+      nGbc = nGbc_;
+    }
+    inline lit And(lit x, lit y) {
+      if(nObjs > nReo) {
+        Reorder();
+        while(nReo < nObjs) {
+          nReo <<= 1;
+          if((lit)nReo > (lit)BvarMax())
+            nReo = BvarMax();
+        }
+      }
+      return And_rec(x, y);
+    }
+    inline lit Or(lit x, lit y) {
+      return LitNot(And(LitNot(x), LitNot(y)));
+    }
+
+  public:
+    void SetRef(std::vector<lit> const &vLits) {
+      vRefs.clear();
+      vRefs.resize(nObjsAlloc);
+      for(size_t i = 0; i < vLits.size(); i++)
+        IncRef(vLits[i]);
+    }
+    void TurnOffReo() {
+      nReo = BvarMax();
+      if(!nGbc)
+        vRefs.clear();
+    }
+    bvar CountNodes() {
+      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;
+    }
+    bvar CountNodes(std::vector<lit> const &vLits) {
+      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;
+    }
+    void PrintStats() {
+      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;
+    }
+  };
+
+}
+
+#endif

src/aig/gia/giaNewTt.h

+#ifndef ABC__aig__gia__giaNewTt_h
+#define ABC__aig__gia__giaNewTt_h
+
+#include <limits>
+#include <iomanip>
+#include <iostream>
+#include <vector>
+#include <bitset>
+
+namespace NewTt {
+
+  typedef int                bvar;
+  typedef unsigned           lit;
+  typedef unsigned short     ref;
+  typedef unsigned long long size;
+  
+  static inline bvar BvarMax() { return std::numeric_limits<bvar>::max(); }
+  static inline lit  LitMax()  { return std::numeric_limits<lit>::max();  }
+  static inline ref  RefMax()  { return std::numeric_limits<ref>::max();  }
+  static inline size SizeMax() { return std::numeric_limits<size>::max(); }
+
+  struct Param {
+    int  nObjsAllocLog      = 15;
+    int  nObjsMaxLog        = 20;
+    int  nVerbose           = 0;
+    bool fCountOnes         = false;
+    int  nGbc               = 0;
+    int  nReo               = BvarMax(); // dummy
+  };
+
+  class Man {
+  private:
+    typedef unsigned long long word;
+    typedef std::bitset<64> bsw;
+    static inline int ww() { return 64; } // word width
+    static inline int lww() { return 6; } // log word width
+    static inline word one() {return 0xffffffffffffffffull; }
+    static inline word vars(int i) {
+      static const word vars[] = {0xaaaaaaaaaaaaaaaaull,
+                                  0xccccccccccccccccull,
+                                  0xf0f0f0f0f0f0f0f0ull,
+                                  0xff00ff00ff00ff00ull,
+                                  0xffff0000ffff0000ull,
+                                  0xffffffff00000000ull};
+      return vars[i];
+    }
+    static inline word ones(int i) {
+      static const word ones[] = {0x0000000000000001ull,
+                                  0x0000000000000003ull,
+                                  0x000000000000000full,
+                                  0x00000000000000ffull,
+                                  0x000000000000ffffull,
+                                  0x00000000ffffffffull,
+                                  0xffffffffffffffffull};
+      return ones[i];
+    }
+
+  private:
+    int  nVars;
+    bvar nObjs;
+    bvar nObjsAlloc;
+    bvar nObjsMax;
+    size nSize;
+    size nTotalSize;
+    std::vector<word> vVals;
+    std::vector<bvar> vDeads;
+    std::vector<ref>  vRefs;
+    int nGbc;
+    int nVerbose;
+
+  public:
+    inline lit  Bvar2Lit(bvar a)          const { return (lit)a << 1;        }
+    inline bvar Lit2Bvar(lit x)           const { return (bvar)(x >> 1);     }
+    inline lit  IthVar(int v)             const { return ((lit)v + 1) << 1;  }
+    inline lit  LitNot(lit x)             const { return x ^ (lit)1;         }
+    inline lit  LitNotCond(lit x, bool c) const { return x ^ (lit)c;         }
+    inline bool LitIsCompl(lit x)         const { return x & (lit)1;         }
+    inline ref  Ref(lit x)                const { return vRefs[Lit2Bvar(x)]; }
+    inline lit  Const0()                  const { return (lit)0;             }
+    inline lit  Const1()                  const { return (lit)1;             }
+    inline bool IsConst0(lit x)           const {
+      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;
+    }
+    inline bool IsConst1(lit x)           const {
+      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;
+    }
+    inline bool LitIsEq(lit x, lit y)     const {
+      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;
+    }
+    inline size OneCount(lit x)           const {
+      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;
+    }
+
+  public:
+    inline void IncRef(lit x) { if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]++; }
+    inline void DecRef(lit x) { if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]--; }
+
+  public:
+    bool Resize() {
+      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;
+    }
+    bool Gbc() {
+      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();
+    }
+
+  public:
+    Man(int nVars, Param p): nVars(nVars) {
+      if(p.nObjsMaxLog < p.nObjsAllocLog)
+        throw std::invalid_argument("nObjsMax must not be smaller than nObjsAlloc");
+      if(nVars >= lww())
+        nSize = 1 << (nVars - lww());
+      else
+        nSize = 1;
+      if(!nSize)
+        throw std::length_error("Memout (nVars) in init");
+      if(!(nSize << p.nObjsMaxLog))
+        throw std::length_error("Memout (nObjsMax) in init");
+      lit nObjsMaxLit = (lit)1 << p.nObjsMaxLog;
+      if(!nObjsMaxLit)
+        throw std::length_error("Memout (nObjsMax) in init");
+      if(nObjsMaxLit > (lit)BvarMax())
+        nObjsMax = BvarMax();
+      else
+        nObjsMax = (bvar)nObjsMaxLit;
+      lit nObjsAllocLit = (lit)1 << p.nObjsAllocLog;
+      if(!nObjsAllocLit)
+        throw std::length_error("Memout (nObjsAlloc) in init");
+      if(nObjsAllocLit > (lit)BvarMax())
+        nObjsAlloc = BvarMax();
+      else
+        nObjsAlloc = (bvar)nObjsAllocLit;
+      if(nObjsAlloc <= (bvar)nVars)
+        throw std::invalid_argument("nObjsAlloc must be larger than nVars");
+      nTotalSize = nSize << p.nObjsAllocLog;
+      vVals.resize(nTotalSize);
+      if(p.fCountOnes && nVars > 63)
+        throw std::length_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);
+    }
+    inline lit And(lit x, lit y) {
+      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()))
+          throw std::length_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;
+    }
+    inline lit Or(lit x, lit y) {
+      return LitNot(And(LitNot(x), LitNot(y)));
+    }
+    void Reorder() {} // dummy
+
+  public:
+    void SetRef(std::vector<lit> const &vLits) {
+      vRefs.clear();
+      vRefs.resize(nObjsAlloc);
+      for(size_t i = 0; i < vLits.size(); i++)
+        IncRef(vLits[i]);
+    }
+    void TurnOffReo() {
+      if(!nGbc)
+        vRefs.clear();
+    }
+    void PrintNode(lit x) const {
+      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;
+    }
+  };
+
+}
+
+#endif

src/aig/gia/giaTransduction.cpp

+#ifdef _WIN32
+#ifndef __MINGW32__
+#pragma warning(disable : 4786) // warning C4786: identifier was truncated to '255' characters in the browser information
+#endif
+#endif
+
+#include "giaTransduction.h"
+#include "giaNewBdd.h"
+#include "giaNewTt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+Gia_Man_t *Gia_ManTransductionBdd(Gia_Man_t *pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t *pExdc, int nVerbose) {
+  if(nRandom) {
+    srand(nRandom);
+    nSortType = rand() % 4;
+    nPiShuffle = rand();
+    nParameter = rand() % 16;
+  }
+  NewBdd::Param p;
+  Transduction::Transduction<NewBdd::Man, NewBdd::Param, NewBdd::lit, 0xffffffff> t(pGia, nVerbose, nSortType, nPiShuffle, fLevel, pExdc, p);
+  int count = t.CountWires();
+  switch(nType) {
+  case 0:
+    count -= fMspf? t.Mspf(): t.Cspf();
+    break;
+  case 1:
+    count -= t.Resub(fMspf);
+    break;
+  case 2:
+    count -= t.ResubMono(fMspf);
+    break;
+  case 3:
+    count -= t.ResubShared(fMspf);
+    break;
+  case 4:
+    count -= t.RepeatResub(false, fMspf);
+    break;
+  case 5:
+    count -= t.RepeatResub(true, fMspf);
+    break;
+  case 6: {
+    bool fInner = (nParameter / 4) % 2;
+    count -= t.RepeatResubInner(fMspf, fInner);
+    break;
+  }
+  case 7: {
+    bool fInner = (nParameter / 4) % 2;
+    bool fOuter = (nParameter / 8) % 2;
+    count -= t.RepeatResubOuter(fMspf, fInner, fOuter);
+    break;
+  }
+  case 8: {
+    bool fFirstMerge = nParameter % 2;
+    bool fMspfMerge = fMspf? (nParameter / 2) % 2: false;
+    bool fInner = (nParameter / 4) % 2;
+    bool fOuter = (nParameter / 8) % 2;
+    count -= t.Optimize(fFirstMerge, fMspfMerge, fMspf, fInner, fOuter);
+    break;
+  }
+  default:
+    std::cout << "Invalid transduction type" << std::endl;
+    assert(0);
+  }
+  assert(t.Verify());
+  assert(count == t.CountWires());
+  return t.GenerateAig();
+}
+
+Gia_Man_t *Gia_ManTransductionTt(Gia_Man_t *pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t *pExdc, int nVerbose) {
+  if(nRandom) {
+    srand(nRandom);
+    nSortType = rand() % 4;
+    nPiShuffle = rand();
+    nParameter = rand() % 16;
+  }
+  NewTt::Param p;
+  Transduction::Transduction<NewTt::Man, NewTt::Param, NewTt::lit, 0xffffffff> t(pGia, nVerbose, nSortType, nPiShuffle, fLevel, pExdc, p);
+  int count = t.CountWires();
+  switch(nType) {
+  case 0:
+    count -= fMspf? t.Mspf(): t.Cspf();
+    break;
+  case 1:
+    count -= t.Resub(fMspf);
+    break;
+  case 2:
+    count -= t.ResubMono(fMspf);
+    break;
+  case 3:
+    count -= t.ResubShared(fMspf);
+    break;
+  case 4:
+    count -= t.RepeatResub(false, fMspf);
+    break;
+  case 5:
+    count -= t.RepeatResub(true, fMspf);
+    break;
+  case 6: {
+    bool fInner = (nParameter / 4) % 2;
+    count -= t.RepeatResubInner(fMspf, fInner);
+    break;
+  }
+  case 7: {
+    bool fInner = (nParameter / 4) % 2;
+    bool fOuter = (nParameter / 8) % 2;
+    count -= t.RepeatResubOuter(fMspf, fInner, fOuter);
+    break;
+  }
+  case 8: {
+    bool fFirstMerge = nParameter % 2;
+    bool fMspfMerge = fMspf? (nParameter / 2) % 2: false;
+    bool fInner = (nParameter / 4) % 2;
+    bool fOuter = (nParameter / 8) % 2;
+    count -= t.Optimize(fFirstMerge, fMspfMerge, fMspf, fInner, fOuter);
+    break;
+  }
+  default:
+    std::cout << "Invalid transduction type" << std::endl;
+    assert(0);
+  }
+  assert(t.Verify());
+  assert(count == t.CountWires());
+  return t.GenerateAig();
+}
+
+ABC_NAMESPACE_IMPL_END

src/aig/gia/giaTransduction.h

+#ifndef ABC__aig__gia__giaTransduction_h
+#define ABC__aig__gia__giaTransduction_h
+
+#include <iostream>
+#include <iomanip>
+#include <vector>
+#include <list>
+#include <set>
+#include <algorithm>
+#include <cassert>
+
+#include "gia.h"
+
+namespace Transduction {
+  
+enum PfState {none, cspf, mspf};
+
+template <class Man, class lit, lit LitMax>
+class ManUtil {
+protected:
+  Man *man;
+  inline void IncRef(lit x) const {
+    if(x != LitMax)
+      man->IncRef(x);
+  }
+  inline void DecRef(lit x) const {
+    if(x != LitMax)
+      man->DecRef(x);
+  }
+  inline void Update(lit &x, lit y) const {
+    DecRef(x);
+    x = y;
+    IncRef(x);
+  }
+  inline void DelVec(std::vector<lit> &v) const {
+    for(unsigned i = 0; i < v.size(); i++)
+      DecRef(v[i]);
+    v.clear();
+  }
+  inline void DelVec(std::vector<std::vector<lit> > &v) const {
+    for(unsigned i = 0; i < v.size(); i++)
+      DelVec(v[i]);
+    v.clear();
+  }
+  inline void CopyVec(std::vector<lit> &v, std::vector<lit> const &u) const {
+    DelVec(v);
+    v = u;
+    for(unsigned i = 0; i < v.size(); i++)
+      IncRef(v[i]);
+  }
+  inline void CopyVec(std::vector<std::vector<lit> > &v, std::vector<std::vector<lit> > const &u) const {
+    for(unsigned i = u.size(); i < v.size(); i++)
+      DelVec(v[i]);
+    v.resize(u.size());
+    for(unsigned i = 0; i < v.size(); i++)
+      CopyVec(v[i], u[i]);
+  }
+  inline bool LitVecIsEq(std::vector<lit> const &v, std::vector<lit> const &u) const {
+    if(v.size() != u.size())
+      return false;
+    for(unsigned i = 0; i < v.size(); i++)
+      if(!man->LitIsEq(v[i], u[i]))
+        return false;
+    return true;
+  }
+  inline bool LitVecIsEq(std::vector<std::vector<lit> > const &v, std::vector<std::vector<lit> > const &u) const {
+    if(v.size() != u.size())
+      return false;
+    for(unsigned i = 0; i < v.size(); i++)
+      if(!LitVecIsEq(v[i], u[i]))
+        return false;
+    return true;
+  }
+  inline lit Xor(lit x, lit y) const {
+    lit f = man->And(x, man->LitNot(y));
+    man->IncRef(f);
+    lit g = man->And(man->LitNot(x), y);
+    man->IncRef(g);
+    lit r = man->Or(f, g);
+    man->DecRef(f);
+    man->DecRef(g);
+    return r;
+  }
+};
+
+template <class Man, class lit, lit LitMax>
+class TransductionBackup: ManUtil<Man, lit, LitMax> {
+private:
+  int nObjsAlloc;
+  PfState state;
+  std::list<int> vObjs;
+  std::vector<std::vector<int> > vvFis;
+  std::vector<std::vector<int> > vvFos;
+  std::vector<int> vLevels;
+  std::vector<int> vSlacks;
+  std::vector<std::vector<int> > vvFiSlacks;
+  std::vector<lit> vFs;
+  std::vector<lit> vGs;
+  std::vector<std::vector<lit> > vvCs;
+  std::vector<bool> vUpdates;
+  std::vector<bool> vPfUpdates;
+  std::vector<bool> vFoConeShared;
+  template <class Man_, class Param, class lit_, lit_ LitMax_>
+  friend class Transduction;
+
+public:
+  ~TransductionBackup() {
+    if(this->man) {
+      this->DelVec(vFs);
+      this->DelVec(vGs);
+      this->DelVec(vvCs);
+    }
+  }
+};
+
+template <class Man, class Param, class lit, lit LitMax>
+class Transduction: ManUtil<Man, lit, LitMax> {
+private:
+  int  nVerbose;
+  int  nSortType;
+  bool fLevel;
+  int  nObjsAlloc;
+  int  nMaxLevels;
+  PfState state;
+  std::vector<int> vPis;
+  std::vector<int> vPos;
+  std::list<int> vObjs;
+  std::vector<std::vector<int> > vvFis;
+  std::vector<std::vector<int> > vvFos;
+  std::vector<int> vLevels;
+  std::vector<int> vSlacks;
+  std::vector<std::vector<int> > vvFiSlacks;
+  std::vector<lit> vFs;
+  std::vector<lit> vGs;
+  std::vector<std::vector<lit> > vvCs;
+  std::vector<bool> vUpdates;
+  std::vector<bool> vPfUpdates;
+  std::vector<bool> vFoConeShared;
+  std::vector<lit> vPoFs;
+
+private: // Helper functions
+  inline bool AllFalse(std::vector<bool> const &v) const {
+    for(std::list<int>::const_iterator it = vObjs.begin(); it != vObjs.end(); it++)
+      if(v[*it])
+        return false;
+    return true;
+  }
+
+public: // Counting
+  inline int CountGates() const {
+    return vObjs.size();
+  }
+  inline int CountWires() const {
+    int count = 0;
+    for(std::list<int>::const_iterator it = vObjs.begin(); it != vObjs.end(); it++)
+      count += vvFis[*it].size();
+    return count;
+  }
+  inline int CountNodes() const {
+    return CountWires() - CountGates();
+  }
+  inline int CountLevels() const {
+    int count = 0;
+    for(unsigned i = 0; i < vPos.size(); i++)
+      count = std::max(count, vLevels[vvFis[vPos[i]][0] >> 1]);
+    return count;
+  }
+
+private: // MIAIG
+  void SortObjs_rec(std::list<int>::iterator const &it) {
+    for(unsigned j = 0; j < vvFis[*it].size(); j++) {
+      int i0 = vvFis[*it][j] >> 1;
+      if(!vvFis[i0].empty()) {
+        std::list<int>::iterator it_i0 = std::find(it, vObjs.end(), i0);
+        if(it_i0 != vObjs.end()) {
+          if(nVerbose > 6)
+            std::cout << "\t\t\t\t\t\tMove " << i0 << " before " << *it << std::endl;
+          vObjs.erase(it_i0);
+          it_i0 = vObjs.insert(it, i0);
+          SortObjs_rec(it_i0);
+        }
+      }
+    }
+  }
+  inline void Connect(int i, int f, bool fSort = false, bool fUpdate = true, lit c = LitMax) {
+    int i0 = f >> 1;
+    if(nVerbose > 5)
+      std::cout << "\t\t\t\t\tConnect " << i0 << "(" << (f & 1) << ")" << " to " << i << std::endl;
+    assert(std::find(vvFis[i].begin(), vvFis[i].end(), f) == vvFis[i].end());
+    vvFis[i].push_back(f);
+    vvFos[i0].push_back(i);
+    if(fUpdate)
+      vUpdates[i] = true;
+    this->IncRef(c);
+    vvCs[i].push_back(c);
+    if(fSort && !vvFos[i].empty() && !vvFis[i0].empty()) {
+      std::list<int>::iterator it = find(vObjs.begin(), vObjs.end(), i);
+      std::list<int>::iterator it_i0 = find(it, vObjs.end(), i0);
+      if(it_i0 != vObjs.end()) {
+        if(nVerbose > 6)
+          std::cout << "\t\t\t\t\t\tMove " << i0 << " before " << *it << std::endl;
+        vObjs.erase(it_i0);
+        it_i0 = vObjs.insert(it, i0);
+        SortObjs_rec(it_i0);
+      }
+    }
+  }
+  inline void Disconnect(int i, int i0, unsigned j, bool fUpdate = true, bool fPfUpdate = true) {
+    if(nVerbose > 5)
+      std::cout << "\t\t\t\t\tDisconnect " << i0 << "(" << (vvFis[i][j] & 1) << ")" << " from " << i << std::endl;
+    vvFos[i0].erase(std::find(vvFos[i0].begin(), vvFos[i0].end(), i));
+    vvFis[i].erase(vvFis[i].begin() + j);
+    this->DecRef(vvCs[i][j]);
+    vvCs[i].erase(vvCs[i].begin() + j);
+    if(fUpdate)
+      vUpdates[i] = true;
+    if(fPfUpdate)
+      vPfUpdates[i0] = true;
+  }
+  inline int Remove(int i, bool fPfUpdate = true) {
+    if(nVerbose > 4)
+      std::cout << "\t\t\t\tRemove " << i << std::endl;
+    assert(vvFos[i].empty());
+    for(unsigned j = 0; j < vvFis[i].size(); j++) {
+      int i0 = vvFis[i][j] >> 1;
+      vvFos[i0].erase(std::find(vvFos[i0].begin(), vvFos[i0].end(), i));
+      if(fPfUpdate)
+        vPfUpdates[i0] = true;
+    }
+    int count = vvFis[i].size();
+    vvFis[i].clear();
+    this->DecRef(vFs[i]);
+    this->DecRef(vGs[i]);
+    vFs[i] = vGs[i] = LitMax;
+    this->DelVec(vvCs[i]);
+    vUpdates[i] = vPfUpdates[i] = false;
+    return count;
+  }
+  inline int FindFi(int i, int i0) const {
+    for(unsigned j = 0; j < vvFis[i].size(); j++)
+      if((vvFis[i][j] >> 1) == i0)
+        return j;
+    return -1;
+  }
+  inline int Replace(int i, int f, bool fUpdate = true) {
+    if(nVerbose > 4)
+      std::cout << "\t\t\t\tReplace " << i << " by " << (f >> 1) << "(" << (f & 1) << ")" << std::endl;
+    assert(i != (f >> 1));
+    int count = 0;
+    for(unsigned j = 0; j < vvFos[i].size(); j++) {
+      int k = vvFos[i][j];
+      int l = FindFi(k, i);
+      assert(l >= 0);
+      int fc = f ^ (vvFis[k][l] & 1);
+      if(find(vvFis[k].begin(), vvFis[k].end(), fc) != vvFis[k].end()) {
+        this->DecRef(vvCs[k][l]);
+        vvCs[k].erase(vvCs[k].begin() + l);
+        vvFis[k].erase(vvFis[k].begin() + l);
+        count++;
+      } else {
+        vvFis[k][l] = f ^ (vvFis[k][l] & 1);
+        vvFos[f >> 1].push_back(k);
+      }
+      if(fUpdate)
+        vUpdates[k] = true;
+    }
+    vvFos[i].clear();
+    vPfUpdates[f >> 1] = true;
+    return count + Remove(i);
+  }
+  int ReplaceByConst(int i, bool c) {
+    if(nVerbose > 4)
+      std::cout << "\t\t\t\tReplace " << i << " by " << c << std::endl;
+    int count = 0;
+    for(unsigned j = 0; j < vvFos[i].size(); j++) {
+      int k = vvFos[i][j];
+      int l = FindFi(k, i);
+      assert(l >= 0);
+      bool fc = c ^ (vvFis[k][l] & 1);
+      this->DecRef(vvCs[k][l]);
+      vvCs[k].erase(vvCs[k].begin() + l);
+      vvFis[k].erase(vvFis[k].begin() + l);
+      if(fc) {
+        if(vvFis[k].size() == 1)
+          count += Replace(k, vvFis[k][0]);
+        else
+          vUpdates[k] = true;
+      } else
+        count += ReplaceByConst(k, 0);
+    }
+    count += vvFos[i].size();
+    vvFos[i].clear();
+    return count + Remove(i);
+  }
+  inline void NewGate(int &pos) {
+    while(pos != nObjsAlloc && (!vvFis[pos].empty() || !vvFos[pos].empty()))
+      pos++;
+    if(nVerbose > 4)
+      std::cout << "\t\t\t\tCreate " << pos << std::endl;
+    if(pos == nObjsAlloc) {
+      nObjsAlloc++;
+      vvFis.resize(nObjsAlloc);
+      vvFos.resize(nObjsAlloc);
+      if(fLevel) {
+        vLevels.resize(nObjsAlloc);
+        vSlacks.resize(nObjsAlloc);
+        vvFiSlacks.resize(nObjsAlloc);
+      }
+      vFs.resize(nObjsAlloc, LitMax);
+      vGs.resize(nObjsAlloc, LitMax);
+      vvCs.resize(nObjsAlloc);
+      vUpdates.resize(nObjsAlloc);
+      vPfUpdates.resize(nObjsAlloc);
+    }
+  }
+  void MarkFiCone_rec(std::vector<bool> &vMarks, int i) const {
+    if(vMarks[i])
+      return;
+    vMarks[i] = true;
+    for(unsigned j = 0; j < vvFis[i].size(); j++)
+      MarkFiCone_rec(vMarks, vvFis[i][j] >> 1);
+  }
+  void MarkFoCone_rec(std::vector<bool> &vMarks, int i) const {
+    if(vMarks[i])
+      return;
+    vMarks[i] = true;
+    for(unsigned j = 0; j < vvFos[i].size(); j++)
+      MarkFoCone_rec(vMarks, vvFos[i][j]);
+  }
+  bool IsFoConeShared_rec(std::vector<int> &vVisits, int i, int visitor) const {
+    if(vVisits[i] == visitor)
+      return false;
+    if(vVisits[i])
+      return true;
+    vVisits[i] = visitor;
+    for(unsigned j = 0; j < vvFos[i].size(); j++)
+      if(IsFoConeShared_rec(vVisits, vvFos[i][j], visitor))
+        return true;
+    return false;
+  }
+  inline bool IsFoConeShared(int i) const {
+    std::vector<int> vVisits(nObjsAlloc);
+    for(unsigned j = 0; j < vvFos[i].size(); j++)
+      if(IsFoConeShared_rec(vVisits, vvFos[i][j], j + 1))
+        return true;
+    return false;
+  }
+
+private: // Level calculation
+  inline void add(std::vector<bool> &a, unsigned i) {
+    if(a.size() <= i) {
+      a.resize(i + 1);
+      a[i] = true;
+      return;
+    }
+    for(; i < a.size() && a[i]; i++)
+      a[i] = false;
+    if(i == a.size())
+      a.resize(i + 1);
+    a[i] = true;
+  }
+  inline bool balanced(std::vector<bool> const &a) {
+    for(unsigned i = 0; i < a.size() - 1; i++)
+      if(a[i])
+        return false;
+    return true;
+  }
+  inline bool noexcess(std::vector<bool> const &a, unsigned i) {
+    if(a.size() <= i)
+      return false;
+    for(unsigned j = i; j < a.size(); j++)
+      if(!a[j])
+        return true;
+    for(unsigned j = 0; j < i; j++)
+      if(a[j])
+        return false;
+    return true;
+  }
+  inline void ComputeLevel() {
+    for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++) {
+      if(vvFis[*it].size() == 2)
+        vLevels[*it] = std::max(vLevels[vvFis[*it][0] >> 1], vLevels[vvFis[*it][1] >> 1]) + 1;
+      else {
+        std::vector<bool> lev;
+        for(unsigned j = 0; j < vvFis[*it].size(); j++)
+          add(lev, vLevels[vvFis[*it][j] >> 1]);
+        if(balanced(lev))
+          vLevels[*it] = (int)lev.size() - 1;
+        else
+          vLevels[*it] = (int)lev.size();
+      }
+    }
+    if(nMaxLevels == -1)
+      nMaxLevels = CountLevels();
+    for(unsigned i = 0; i < vPos.size(); i++) {
+      vvFiSlacks[vPos[i]].resize(1);
+      vvFiSlacks[vPos[i]][0] = nMaxLevels - vLevels[vvFis[vPos[i]][0] >> 1];
+    }
+    for(std::list<int>::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend(); it++) {
+      vSlacks[*it] = nMaxLevels;
+      for(unsigned j = 0; j < vvFos[*it].size(); j++) {
+        int k = vvFos[*it][j];
+        int l = FindFi(k, *it);
+        assert(l >= 0);
+        vSlacks[*it] = std::min(vSlacks[*it], vvFiSlacks[k][l]);
+      }
+      vvFiSlacks[*it].resize(vvFis[*it].size());
+      for(unsigned j = 0; j < vvFis[*it].size(); j++)
+        vvFiSlacks[*it][j] = vSlacks[*it] + vLevels[*it] - 1 - vLevels[vvFis[*it][j] >> 1];
+    }
+  }
+
+private: // Cost function
+  inline void ShufflePis(int seed) {
+    srand(seed);
+    for(int i = (int)vPis.size() - 1; i > 0; i--)
+      std::swap(vPis[i], vPis[rand() % (i + 1)]);
+  }
+  inline bool CostCompare(int a, int b) const { // return (cost(a) > cost(b))
+    int a0 = a >> 1;
+    int b0 = b >> 1;
+    if(vvFis[a0].empty() && vvFis[b0].empty())
+      return std::find(find(vPis.begin(), vPis.end(), a0), vPis.end(), b0) != vPis.end();
+    if(vvFis[a0].empty() && !vvFis[b0].empty())
+      return false;
+    if(!vvFis[a0].empty() && vvFis[b0].empty())
+      return true;
+    if(vvFos[a0].size() > vvFos[b0].size())
+      return false;
+    if(vvFos[a0].size() < vvFos[b0].size())
+      return true;
+    bool ac = a & 1;
+    bool bc = b & 1;
+    switch(nSortType) {
+    case 0:
+      return std::find(find(vObjs.begin(), vObjs.end(), a0), vObjs.end(), b0) == vObjs.end();
+    case 1:
+      return this->man->OneCount(this->man->LitNotCond(vFs[a0], ac)) < this->man->OneCount(this->man->LitNotCond(vFs[b0], bc));
+    case 2:
+      return this->man->OneCount(vFs[a0]) < this->man->OneCount(vFs[b0]);
+    case 3:
+      return this->man->OneCount(this->man->LitNot(vFs[a0])) < this->man->OneCount(vFs[b0]); // pseudo random
+    default:
+      return false; // no sorting
+    }
+  }
+  inline bool SortFis(int i) {
+    if(nVerbose > 4)
+      std::cout << "\t\t\t\tSort fanins " << i << std::endl;
+    bool fSort = false;
+    for(int p = 1; p < (int)vvFis[i].size(); p++) {
+      int f = vvFis[i][p];
+      lit c = vvCs[i][p];
+      int q = p - 1;
+      for(; q >= 0 && CostCompare(f, vvFis[i][q]); q--) {
+        vvFis[i][q + 1] = vvFis[i][q];
+        vvCs[i][q + 1] = vvCs[i][q];
+      }
+      if(q + 1 != p) {
+        fSort = true;
+        vvFis[i][q + 1] = f;
+        vvCs[i][q + 1] = c;
+      }
+    }
+    if(nVerbose > 5)
+      for(unsigned j = 0; j < vvFis[i].size(); j++)
+        std::cout << "\t\t\t\t\tFanin " << j << " : " << (vvFis[i][j] >> 1) << "(" << (vvFis[i][j] & 1) << ")" << std::endl;
+    return fSort;
+  }
+
+private: // Symbolic simulation
+  inline lit LitFi(int i, int j) const {
+    int i0 = vvFis[i][j] >> 1;
+    bool c0 = vvFis[i][j] & 1;
+    return this->man->LitNotCond(vFs[i0], c0);
+  }
+  inline lit LitFi(int i, int j, std::vector<lit> const &vFs_) const {
+    int i0 = vvFis[i][j] >> 1;
+    bool c0 = vvFis[i][j] & 1;
+    return this->man->LitNotCond(vFs_[i0], c0);
+  }
+  inline void Build(int i, std::vector<lit> &vFs_) const {
+    if(nVerbose > 4)
+      std::cout << "\t\t\t\tBuild " << i << std::endl;
+    this->Update(vFs_[i], this->man->Const1());
+    for(unsigned j = 0; j < vvFis[i].size(); j++)
+      this->Update(vFs_[i], this->man->And(vFs_[i], LitFi(i, j, vFs_)));
+  }
+  inline void Build(bool fPfUpdate = true) {
+    if(nVerbose > 3)
+      std::cout << "\t\t\tBuild" << std::endl;
+    for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
+      if(vUpdates[*it]) {
+        lit x = vFs[*it];
+        this->IncRef(x);
+        Build(*it, vFs);
+        this->DecRef(x);
+        if(!this->man->LitIsEq(x, vFs[*it]))
+          for(unsigned j = 0; j < vvFos[*it].size(); j++)
+            vUpdates[vvFos[*it][j]] = true;
+      }
+    if(fPfUpdate)
+      for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
+        vPfUpdates[*it] = vPfUpdates[*it] || vUpdates[*it];
+    for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
+      vUpdates[*it] = false;
+    assert(AllFalse(vUpdates));
+  }
+  void BuildFoConeCompl(int i, std::vector<lit> &vPoFsCompl) const {
+    if(nVerbose > 3)
+      std::cout << "\t\t\tBuild with complemented " << i << std::endl;
+    std::vector<lit> vFsCompl;
+    this->CopyVec(vFsCompl, vFs);
+    vFsCompl[i] = this->man->LitNot(vFs[i]);
+    std::vector<bool> vUpdatesCompl(nObjsAlloc);
+    for(unsigned j = 0; j < vvFos[i].size(); j++)
+      vUpdatesCompl[vvFos[i][j]] = true;
+    for(std::list<int>::const_iterator it = vObjs.begin(); it != vObjs.end(); it++)
+      if(vUpdatesCompl[*it]) {
+        Build(*it, vFsCompl);
+        if(!this->man->LitIsEq(vFsCompl[*it], vFs[*it]))
+          for(unsigned j = 0; j < vvFos[*it].size(); j++)
+            vUpdatesCompl[vvFos[*it][j]] = true;
+      }
+    for(unsigned j = 0; j < vPos.size(); j++)
+      this->Update(vPoFsCompl[j], LitFi(vPos[j], 0, vFsCompl));
+    this->DelVec(vFsCompl);
+  }
+
+private: // CSPF
+  inline int RemoveRedundantFis(int i, int block_i0 = -1, unsigned j = 0) {
+    int count = 0;
+    for(; j < vvFis[i].size(); j++) {
+      if(block_i0 == (vvFis[i][j] >> 1))
+        continue;
+      lit x = this->man->Const1();
+      this->IncRef(x);
+      for(unsigned jj = 0; jj < vvFis[i].size(); jj++)
+        if(j != jj)
+          this->Update(x, this->man->And(x, LitFi(i, jj)));
+      this->Update(x, this->man->Or(this->man->LitNot(x), vGs[i]));
+      this->Update(x, this->man->Or(x, LitFi(i, j)));
+      this->DecRef(x);
+      if(this->man->IsConst1(x)) {
+        int i0 = vvFis[i][j] >> 1;
+        if(nVerbose > 4)
+          std::cout << "\t\t\t\tRRF remove wire " << i0 << "(" << (vvFis[i][j] & 1) << ")" << " -> " << i << std::endl;
+        Disconnect(i, i0, j--);
+        count++;
+      }
+    }
+    return count;
+  }
+  inline void CalcG(int i) {
+    this->Update(vGs[i], this->man->Const1());
+    for(unsigned j = 0; j < vvFos[i].size(); j++) {
+      int k = vvFos[i][j];
+      int l = FindFi(k, i);
+      assert(l >= 0);
+      this->Update(vGs[i], this->man->And(vGs[i], vvCs[k][l]));
+    }
+  }
+  inline int CalcC(int i) {
+    int count = 0;
+    for(unsigned j = 0; j < vvFis[i].size(); j++) {
+      lit x = this->man->Const1();
+      this->IncRef(x);
+      for(unsigned jj = j + 1; jj < vvFis[i].size(); jj++)
+        this->Update(x, this->man->And(x, LitFi(i, jj)));
+      this->Update(x, this->man->Or(this->man->LitNot(x), vGs[i]));
+      int i0 = vvFis[i][j] >> 1;
+      if(this->man->IsConst1(this->man->Or(x, LitFi(i, j)))) {
+        if(nVerbose > 4)
+          std::cout << "\t\t\t\tCspf remove wire " << i0 << "(" << (vvFis[i][j] & 1) << ")" << " -> " << i << std::endl;
+        Disconnect(i, i0, j--);
+        count++;
+      } else if(!this->man->LitIsEq(vvCs[i][j], x)) {
+        this->Update(vvCs[i][j], x);
+        vPfUpdates[i0] = true;
+      }
+      this->DecRef(x);
+    }
+    return count;
+  }
+  int Cspf(bool fSortRemove, int block = -1, int block_i0 = -1) {
+    if(nVerbose > 2) {
+      std::cout << "\t\tCspf";
+      if(block_i0 != -1)
+        std::cout << " (block " << block_i0 << " -> " << block << ")";
+      else if(block != -1)
+        std::cout << " (block " << block << ")";
+      std::cout << std::endl;
+    }
+    if(state != PfState::cspf)
+      for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
+        vPfUpdates[*it] = true;
+    state = PfState::cspf;
+    int count = 0;
+    for(std::list<int>::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend();) {
+      if(vvFos[*it].empty()) {
+        if(nVerbose > 3)
+          std::cout << "\t\t\tRemove unused " << *it << std::endl;
+        count += Remove(*it);
+        it = std::list<int>::reverse_iterator(vObjs.erase(--(it.base())));
+        continue;
+      }
+      if(!vPfUpdates[*it]) {
+        it++;
+        continue;
+      }
+      if(nVerbose > 3)
+        std::cout << "\t\t\tCspf " << *it << std::endl;
+      CalcG(*it);
+      if(fSortRemove) {
+        if(*it != block)
+          SortFis(*it), count += RemoveRedundantFis(*it);
+        else if(block_i0 != -1)
+          count += RemoveRedundantFis(*it, block_i0);
+      }
+      count += CalcC(*it);
+      vPfUpdates[*it] = false;
+      assert(!vvFis[*it].empty());
+      if(vvFis[*it].size() == 1) {
+        count += Replace(*it, vvFis[*it][0]);
+        it = std::list<int>::reverse_iterator(vObjs.erase(--(it.base())));
+        continue;
+      }
+      it++;
+    }
+    Build(false);
+    assert(AllFalse(vPfUpdates));
+    if(fLevel)
+      ComputeLevel();
+    return count;
+  }
+
+private: // MSPF
+  inline bool MspfCalcG(int i) {
+    lit g = vGs[i];
+    this->IncRef(g);
+    std::vector<lit> vPoFsCompl(vPos.size(), LitMax);
+    BuildFoConeCompl(i, vPoFsCompl);
+    this->Update(vGs[i], this->man->Const1());
+    for(unsigned j = 0; j < vPos.size(); j++) {
+      lit x = this->man->LitNot(this->Xor(vPoFs[j], vPoFsCompl[j]));
+      this->IncRef(x);
+      this->Update(x, this->man->Or(x, vvCs[vPos[j]][0]));
+      this->Update(vGs[i], this->man->And(vGs[i], x));
+      this->DecRef(x);
+    }
+    this->DelVec(vPoFsCompl);
+    this->DecRef(g);
+    return !this->man->LitIsEq(vGs[i], g);
+  }
+  inline int MspfCalcC(int i, int block_i0 = -1) {
+    for(unsigned j = 0; j < vvFis[i].size(); j++) {
+      lit x = this->man->Const1();
+      this->IncRef(x);
+      for(unsigned jj = 0; jj < vvFis[i].size(); jj++)
+        if(j != jj)
+          this->Update(x, this->man->And(x, LitFi(i, jj)));
+      this->Update(x, this->man->Or(this->man->LitNot(x), vGs[i]));
+      int i0 = vvFis[i][j] >> 1;
+      if(i0 != block_i0 && this->man->IsConst1(this->man->Or(x, LitFi(i, j)))) {
+        if(nVerbose > 4)
+          std::cout << "\t\t\t\tMspf remove wire " << i0 << "(" << (vvFis[i][j] & 1) << ")" << " -> " << i << std::endl;
+        Disconnect(i, i0, j);
+        this->DecRef(x);
+        return RemoveRedundantFis(i, block_i0, j) + 1;
+      } else if(!this->man->LitIsEq(vvCs[i][j], x)) {
+        this->Update(vvCs[i][j], x);
+        vPfUpdates[i0] = true;
+      }
+      this->DecRef(x);
+    }
+    return 0;
+  }
+  int Mspf(bool fSort, int block = -1, int block_i0 = -1) {
+    if(nVerbose > 2) {
+      std::cout << "\t\tMspf";
+      if(block_i0 != -1)
+        std::cout << " (block " << block_i0 << " -> " << block << ")";
+      else if(block != -1)
+        std::cout << " (block " << block << ")";
+      std::cout << std::endl;
+    }
+    assert(AllFalse(vUpdates));
+    vFoConeShared.resize(nObjsAlloc);
+    if(state != PfState::mspf)
+      for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
+        vPfUpdates[*it] = true;
+    state = PfState::mspf;
+    int count = 0;
+    for(std::list<int>::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend();) {
+      if(vvFos[*it].empty()) {
+        if(nVerbose > 3)
+          std::cout << "\t\t\tRemove unused " << *it << std::endl;
+        count += Remove(*it);
+        it = std::list<int>::reverse_iterator(vObjs.erase(--(it.base())));
+        continue;
+      }
+      if(!vFoConeShared[*it] && !vPfUpdates[*it] && (vvFos[*it].size() == 1 || !IsFoConeShared(*it))) {
+        it++;
+        continue;
+      }
+      if(nVerbose > 3)
+        std::cout << "\t\t\tMspf " << *it << std::endl;
+      if(vvFos[*it].size() == 1 || !IsFoConeShared(*it)) {
+        if(vFoConeShared[*it]) {
+          vFoConeShared[*it] = false;
+          lit g = vGs[*it];
+          this->IncRef(g);
+          CalcG(*it);
+          this->DecRef(g);
+          if(g == vGs[*it] && !vPfUpdates[*it]) {
+            it++;
+            continue;
+          }
+        } else
+          CalcG(*it);
+      } else {
+        vFoConeShared[*it] = true;
+        if(!MspfCalcG(*it) && !vPfUpdates[*it]) {
+          it++;
+          continue;
+        }
+        bool IsConst1 = this->man->IsConst1(this->man->Or(vGs[*it], vFs[*it]));
+        bool IsConst0 = IsConst1? false: this->man->IsConst1(this->man->Or(vGs[*it], this->man->LitNot(vFs[*it])));
+        if(IsConst1 || IsConst0) {
+          count += ReplaceByConst(*it, (int)IsConst1);
+          vObjs.erase(--(it.base()));
+          Build();
+          it = vObjs.rbegin();
+          continue;
+        }
+      }
+      if(fSort && block != *it)
+        SortFis(*it);
+      if(int diff = (block == *it)? MspfCalcC(*it, block_i0): MspfCalcC(*it)) {
+        count += diff;
+        assert(!vvFis[*it].empty());
+        if(vvFis[*it].size() == 1) {
+          count += Replace(*it, vvFis[*it][0]);
+          vObjs.erase(--(it.base()));
+        }
+        Build();
+        it = vObjs.rbegin();
+        continue;
+      }
+      vPfUpdates[*it] = false;
+      it++;
+    }
+    assert(AllFalse(vUpdates));
+    assert(AllFalse(vPfUpdates));
+    if(fLevel)
+      ComputeLevel();
+    return count;
+  }
+
+private: // Merge/decompose one
+  inline int TrivialMergeOne(int i) {
+    if(nVerbose > 3)
+      std::cout << "\t\t\tTrivial merge " << i << std::endl;
+    int count = 0;
+    std::vector<int> vFisOld = vvFis[i];
+    std::vector<lit> vCsOld = vvCs[i];
+    vvFis[i].clear();
+    vvCs[i].clear();
+    for(unsigned j = 0; j < vFisOld.size(); j++) {
+      int i0 = vFisOld[j] >> 1;
+      int c0 = vFisOld[j] & 1;
+      if(vvFis[i0].empty() || vvFos[i0].size() > 1 || c0) {
+        if(nVerbose > 5)
+          std::cout << "\t\t\t\t\tFanin " << j << " : " << i0 << "(" << c0 << ")" << std::endl;
+        vvFis[i].push_back(vFisOld[j]);
+        vvCs[i].push_back(vCsOld[j]);
+        continue;
+      }
+      vPfUpdates[i] = vPfUpdates[i] | vPfUpdates[i0];
+      vvFos[i0].erase(find(vvFos[i0].begin(), vvFos[i0].end(), i));
+      count++;
+      typename std::vector<int>::iterator itfi = vFisOld.begin() + j;
+      typename std::vector<lit>::iterator itc = vCsOld.begin() + j;
+      for(unsigned jj = 0; jj < vvFis[i0].size(); jj++) {
+        int f = vvFis[i0][jj];
+        std::vector<int>::iterator it = find(vvFis[i].begin(), vvFis[i].end(), f);
+        if(it == vvFis[i].end()) {
+          vvFos[f >> 1].push_back(i);
+          itfi = vFisOld.insert(itfi, f);
+          itc = vCsOld.insert(itc, vvCs[i0][jj]);
+          this->IncRef(*itc);
+          itfi++;
+          itc++;
+          count--;
+        } else {
+          assert(state == PfState::none);
+        }
+      }
+      count += Remove(i0, false);
+      vObjs.erase(find(vObjs.begin(), vObjs.end(), i0));
+      vFisOld.erase(itfi);
+      this->DecRef(*itc);
+      vCsOld.erase(itc);
+      j--;
+    }
+    return count;
+  }
+  inline int TrivialDecomposeOne(std::list<int>::iterator const &it, int &pos) {
+    if(nVerbose > 3)
+      std::cout << "\t\t\tTrivial decompose " << *it << std::endl;
+    assert(vvFis[*it].size() > 2);
+    int count = 2 - vvFis[*it].size();
+    while(vvFis[*it].size() > 2) {
+      int f0 = vvFis[*it].back();
+      lit c0 = vvCs[*it].back();
+      Disconnect(*it, f0 >> 1, vvFis[*it].size() - 1, false, false);
+      int f1 = vvFis[*it].back();
+      lit c1 = vvCs[*it].back();
+      Disconnect(*it, f1 >> 1, vvFis[*it].size() - 1, false, false);
+      NewGate(pos);
+      Connect(pos, f1, false, false, c1);
+      Connect(pos, f0, false, false, c0);
+      if(!vPfUpdates[*it]) {
+        if(state == PfState::cspf)
+          this->Update(vGs[pos], vGs[*it]);
+        else if(state == PfState::mspf) {
+          lit x = this->man->Const1();
+          this->IncRef(x);
+          for(unsigned j = 0; j < vvFis[*it].size(); j++)
+            this->Update(x, this->man->And(x, LitFi(*it, j)));
+          this->Update(vGs[pos], this->man->Or(this->man->LitNot(x), vGs[*it]));
+          this->DecRef(x);
+        }
+      }
+      Connect(*it, pos << 1, false, false, vGs[pos]);
+      vObjs.insert(it, pos);
+      Build(pos, vFs);
+    }
+    return count;
+  }
+  inline int BalancedDecomposeOne(std::list<int>::iterator const &it, int &pos) {
+    if(nVerbose > 3)
+      std::cout << "\t\t\tBalanced decompose " << *it << std::endl;
+    assert(fLevel);
+    assert(vvFis[*it].size() > 2);
+    for(int p = 1; p < (int)vvFis[*it].size(); p++) {
+      int f = vvFis[*it][p];
+      lit c = vvCs[*it][p];
+      int q = p - 1;
+      for(; q >= 0 && vLevels[f >> 1] > vLevels[vvFis[*it][q] >> 1]; q--) {
+        vvFis[*it][q + 1] = vvFis[*it][q];
+        vvCs[*it][q + 1] = vvCs[*it][q];
+      }
+      if(q + 1 != p) {
+        vvFis[*it][q + 1] = f;
+        vvCs[*it][q + 1] = c;
+      }
+    }
+    int count = 2 - vvFis[*it].size();
+    while(vvFis[*it].size() > 2) {
+      int f0 = vvFis[*it].back();
+      lit c0 = vvCs[*it].back();
+      Disconnect(*it, f0 >> 1, vvFis[*it].size() - 1, false, false);
+      int f1 = vvFis[*it].back();
+      lit c1 = vvCs[*it].back();
+      Disconnect(*it, f1 >> 1, vvFis[*it].size() - 1, false, false);
+      NewGate(pos);
+      Connect(pos, f1, false, false, c1);
+      Connect(pos, f0, false, false, c0);
+      Connect(*it, pos << 1, false, false);
+      Build(pos, vFs);
+      vLevels[pos] = std::max(vLevels[f0 >> 1], vLevels[f1 >> 1]) + 1;
+      vObjs.insert(it, pos);
+      int f = vvFis[*it].back();
+      lit c = vvCs[*it].back();
+      int q = (int)vvFis[*it].size() - 2;
+      for(; q >= 0 && vLevels[f >> 1] > vLevels[vvFis[*it][q] >> 1]; q--) {
+        vvFis[*it][q + 1] = vvFis[*it][q];
+        vvCs[*it][q + 1] = vvCs[*it][q];
+      }
+      if(q + 1 != (int)vvFis[*it].size() - 1) {
+        vvFis[*it][q + 1] = f;
+        vvCs[*it][q + 1] = c;
+      }
+    }
+    vPfUpdates[*it] = true;
+    return count;
+  }
+
+public: // Merge/decompose
+  int TrivialMerge() {
+    if(nVerbose > 2)
+      std::cout << "\t\tTrivial merge" << std::endl;
+    int count = 0;
+    for(std::list<int>::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend();) {
+      count += TrivialMergeOne(*it);
+      it++;
+    }
+    return count;
+  }
+  int TrivialDecompose() {
+    if(nVerbose > 2)
+      std::cout << "\t\tTrivial decompose" << std::endl;
+    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;
+  }
+  int Decompose() {
+    if(nVerbose)
+      std::cout << "Decompose" << std::endl;
+    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(), inserter(s, s.begin()));
+        if(s.size() > 1) {
+          if(s == s1) {
+            if(s == s2) {
+              if(nVerbose > 1)
+                std::cout << "\tReplace " << *it2 << " by " << *it << std::endl;
+              count += Replace(*it2, *it << 1, false);
+              it2 = vObjs.erase(it2);
+              it2--;
+            } else {
+              if(nVerbose > 1)
+                std::cout << "\tDecompose " << *it2 << " by " << *it << std::endl;
+              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 > 1)
+              std::cout << "\tCreate " << pos << " for intersection of " << *it << " and " << *it2  << std::endl;
+            if(nVerbose > 2) {
+              std::cout << "\t\tIntersection :";
+              for(std::set<int>::iterator it3 = s.begin(); it3 != s.end(); it3++)
+                std::cout << " " << (*it3 >> 1) << "(" << (*it3 & 1) << ")";
+              std::cout << std::endl;
+            }
+            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) {
+        if(nVerbose > 1)
+          std::cout << "\tTrivial decompose " << *it << std::endl;
+        count += TrivialDecomposeOne(it, pos);
+      }
+    }
+    return count;
+  }
+
+private: // Save/load
+  inline void Save(TransductionBackup<Man, lit, LitMax> &b) const {
+    b.man = this->man;
+    b.nObjsAlloc = nObjsAlloc;
+    b.state = state;
+    b.vObjs = vObjs;
+    b.vvFis = vvFis;
+    b.vvFos = vvFos;
+    b.vLevels = vLevels;
+    b.vSlacks = vSlacks;
+    b.vvFiSlacks = vvFiSlacks;
+    this->CopyVec(b.vFs, vFs);
+    this->CopyVec(b.vGs, vGs);
+    this->CopyVec(b.vvCs, vvCs);
+    b.vUpdates = vUpdates;
+    b.vPfUpdates = vPfUpdates;
+    b.vFoConeShared = vFoConeShared;
+  }
+  inline void Load(TransductionBackup<Man, lit, LitMax> const &b) {
+    nObjsAlloc = b.nObjsAlloc;
+    state = b.state;
+    vObjs = b.vObjs;
+    vvFis = b.vvFis;
+    vvFos = b.vvFos;
+    vLevels = b.vLevels;
+    vSlacks = b.vSlacks;
+    vvFiSlacks = b.vvFiSlacks;
+    this->CopyVec(vFs, b.vFs);
+    this->CopyVec(vGs, b.vGs);
+    this->CopyVec(vvCs, b.vvCs);
+    vUpdates = b.vUpdates;
+    vPfUpdates = b.vPfUpdates;
+    vFoConeShared = b.vFoConeShared;
+  }
+
+private: // Connectable condition
+  inline bool TryConnect(int i, int i0, bool c0) {
+    int f = (i0 << 1) ^ (int)c0;
+    if(find(vvFis[i].begin(), vvFis[i].end(), f) == vvFis[i].end()) {
+      lit x = this->man->Or(this->man->LitNot(vFs[i]), vGs[i]);
+      this->IncRef(x);
+      if(this->man->IsConst1(this->man->Or(x, this->man->LitNotCond(vFs[i0], c0)))) {
+        this->DecRef(x);
+        if(nVerbose > 3)
+          std::cout << "\t\t\tConnect " << i0 << "(" << c0 << ")" << std::endl;
+        Connect(i, f, true);
+        return true;
+      }
+      this->DecRef(x);
+    }
+    return false;
+  }
+
+public: // Resubs
+  int Resub(bool fMspf) {
+    if(nVerbose)
+      std::cout << "Resubstitution" << std::endl;
+    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::cout << "\tResubstitute " << *it << std::endl;
+      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;
+    }
+    return count;
+  }
+  int ResubMono(bool fMspf) {
+    if(nVerbose)
+      std::cout << "Resubstitution mono" << std::endl;
+    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::cout << "\tResubstitute mono " << *it << std::endl;
+      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(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(!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);
+      }
+    }
+    return count;
+  }
+  int ResubShared(bool fMspf) {
+    if(nVerbose)
+      std::cout << "Merge" << std::endl;
+    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::cout << "\tMerge " << *it << std::endl;
+      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);
+        }
+      }
+    }
+    return count + Decompose();
+  }
+
+public: // Optimization scripts
+  int RepeatResub(bool fMono, bool fMspf) {
+    int count = 0;
+    while(int diff = fMono? ResubMono(fMspf): Resub(fMspf))
+      count += diff;
+    return count;
+  }
+  int RepeatResubInner(bool fMspf, bool fInner) {
+    int count = 0;
+    while(int diff = RepeatResub(true, fMspf) + RepeatResub(false, fMspf)) {
+      count += diff;
+      if(!fInner)
+        break;
+    }
+    return count;
+  }
+  int RepeatResubOuter(bool fMspf, bool fInner, bool fOuter) {
+    int count = 0;
+    while(int diff = fMspf? RepeatResubInner(false, fInner) + RepeatResubInner(true, fInner): RepeatResubInner(false, fInner)) {
+      count += diff;
+      if(!fOuter)
+        break;
+    }
+    return count;
+  }
+  int Optimize(bool fFirstMerge, bool fMspfMerge, bool fMspfResub, bool fInner, bool fOuter) {
+    TransductionBackup<Man, lit, LitMax> b;
+    Save(b);
+    int count = 0;
+    int diff = 0;
+    if(fFirstMerge)
+      diff = ResubShared(fMspfMerge);
+    diff += RepeatResubOuter(fMspfResub, fInner, fOuter);
+    if(diff > 0) {
+      count = diff;
+      Save(b);
+      diff = 0;
+    }
+    while(true) {
+      diff += ResubShared(fMspfMerge) + RepeatResubOuter(fMspfResub, fInner, fOuter);
+      if(diff > 0) {
+        count += diff;
+        Save(b);
+        diff = 0;
+      } else {
+        Load(b);
+        break;
+      }
+    }
+    return count;
+  }
+
+public: // Cspf/mspf
+  int Cspf() {
+    return Cspf(true);
+  }
+  int Mspf() {
+    return Mspf(true);
+  }
+
+private: // Setup
+  void ImportAig(Gia_Man_t *pGia) {
+    int i;
+    Gia_Obj_t *pObj;
+    if(nVerbose > 2)
+      std::cout << "\t\tImport aig" << std::endl;
+    nObjsAlloc = Gia_ManObjNum(pGia);
+    vvFis.resize(nObjsAlloc);
+    vvFos.resize(nObjsAlloc);
+    if(fLevel) {
+      vLevels.resize(nObjsAlloc);
+      vSlacks.resize(nObjsAlloc);
+      vvFiSlacks.resize(nObjsAlloc);
+    }
+    vFs.resize(nObjsAlloc, LitMax);
+    vGs.resize(nObjsAlloc, LitMax);
+    vvCs.resize(nObjsAlloc);
+    vUpdates.resize(nObjsAlloc);
+    vPfUpdates.resize(nObjsAlloc);
+    std::vector<int> v(Gia_ManObjNum(pGia), -1);
+    int nObjs = 0;
+    v[Gia_ObjId(pGia, Gia_ManConst0(pGia))] = nObjs << 1;
+    nObjs++;
+    Gia_ManForEachCi(pGia, pObj, i) {
+      v[Gia_ObjId(pGia, pObj)] = nObjs << 1;
+      vPis.push_back(nObjs);
+      nObjs++;
+    }
+    Gia_ManForEachAnd(pGia, pObj, i) {
+      int id = Gia_ObjId(pGia, pObj);
+      if(nVerbose > 3)
+        std::cout << "\t\t\tImport node " << id << std::endl;
+      int i0 = Gia_ObjId(pGia, Gia_ObjFanin0(pObj));
+      int i1 = Gia_ObjId(pGia, Gia_ObjFanin1(pObj));
+      int c0 = Gia_ObjFaninC0(pObj);
+      int c1 = Gia_ObjFaninC1(pObj);
+      if(i0 == i1) {
+        if(c0 == c1)
+          v[id] = v[i0] ^ c0;
+        else
+          v[id] = 0;
+      } else {
+        Connect(nObjs , v[i0] ^ c0);
+        Connect(nObjs, v[i1] ^ c1);
+        v[id] = nObjs << 1;
+        vObjs.push_back(nObjs);
+        nObjs++;
+      }
+    }
+    Gia_ManForEachCo(pGia, pObj, i) {
+      if(nVerbose > 3)
+        std::cout << "\t\t\tImport po " << i << std::endl;
+      int i0 = Gia_ObjId(pGia, Gia_ObjFanin0(pObj));
+      bool c0 = Gia_ObjFaninC0(pObj);
+      Connect(nObjs, v[i0] ^ c0);
+      vPos.push_back(nObjs);
+      nObjs++;
+    }
+  }
+  void Aig2Bdd(Gia_Man_t *pGia, std::vector<lit> &vNodes) {
+    int i;
+    Gia_Obj_t *pObj;
+    std::vector<int> vCounts(pGia->nObjs);
+    Gia_ManStaticFanoutStart(pGia);
+    Gia_ManForEachAnd(pGia, pObj, i)
+      vCounts[Gia_ObjId(pGia, pObj)] = Gia_ObjFanoutNum(pGia, pObj);
+    Gia_ManStaticFanoutStop(pGia);
+    std::vector<lit> nodes(pGia->nObjs);
+    nodes[Gia_ObjId(pGia, Gia_ManConst0(pGia))] = this->man->Const0();
+    Gia_ManForEachCi(pGia, pObj, i)
+      nodes[Gia_ObjId(pGia, pObj)] = this->man->IthVar(i);
+    Gia_ManForEachAnd(pGia, pObj, i) {
+      int id = Gia_ObjId(pGia, pObj);
+      if(nVerbose > 3)
+        std::cout << "Aig2Bdd: gate " << i << " / " << Gia_ManAndNum(pGia) << std::endl;
+      int i0 = Gia_ObjId(pGia, Gia_ObjFanin0(pObj));
+      int i1 = Gia_ObjId(pGia, Gia_ObjFanin1(pObj));
+      bool c0 = Gia_ObjFaninC0(pObj);
+      bool c1 = Gia_ObjFaninC1(pObj);
+      nodes[id] = this->man->And(this->man->LitNotCond(nodes[i0], c0), this->man->LitNotCond(nodes[i1], c1));
+      this->IncRef(nodes[id]);
+      vCounts[i0]--;
+      if(!vCounts[i0])
+        this->DecRef(nodes[i0]);
+      vCounts[i1]--;
+      if(!vCounts[i1])
+        this->DecRef(nodes[i1]);
+    }
+    Gia_ManForEachCo(pGia, pObj, i) {
+      int i0 = Gia_ObjId(pGia, Gia_ObjFanin0(pObj));
+      bool c0 = Gia_ObjFaninC0(pObj);
+      vNodes.push_back(this->man->LitNotCond(nodes[i0], c0));
+    }
+  }
+  void RemoveConstOutputs() {
+    bool fRemoved = false;
+    for(unsigned i = 0; i < vPos.size(); i++) {
+      int i0 = vvFis[vPos[i]][0] >> 1;
+      lit c = vvCs[vPos[i]][0];
+      if(i0) {
+        if(this->man->IsConst1(this->man->Or(LitFi(vPos[i], 0), c))) {
+          if(nVerbose > 3)
+            std::cout << "\t\t\tConst 1 output : po " << i << std::endl;
+          Disconnect(vPos[i], i0, 0, false, false);
+          Connect(vPos[i], 1, false, false, c);
+          fRemoved |= vvFos[i0].empty();
+        } else if(this->man->IsConst1(this->man->Or(this->man->LitNot(LitFi(vPos[i], 0)), c))) {
+          if(nVerbose > 3)
+            std::cout << "\t\t\tConst 0 output : po " << i << std::endl;
+          Disconnect(vPos[i], i0, 0, false, false);
+          Connect(vPos[i], 0, false, false, c);
+          fRemoved |= vvFos[i0].empty();
+        }
+      }
+    }
+    if(fRemoved) {
+      if(nVerbose > 3)
+        std::cout << "\t\t\tRemove unused" << std::endl;
+      for(std::list<int>::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend();) {
+        if(vvFos[*it].empty()) {
+          Remove(*it, false);
+          it = std::list<int>::reverse_iterator(vObjs.erase(--(it.base())));
+          continue;
+        }
+        it++;
+      }
+    }
+  }
+
+public: // Constructor
+  Transduction(Gia_Man_t *pGia, int nVerbose, int nSortType, int nPiShuffle, bool fLevel, Gia_Man_t *pExdc, Param &p): nVerbose(nVerbose), nSortType(nSortType), fLevel(fLevel) {
+    p.nGbc = 1;
+    p.nReo = 4000;
+    if(nSortType)
+      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 = PfState::none;
+    if(nPiShuffle)
+      ShufflePis(nPiShuffle);
+    if(fLevel)
+      ComputeLevel();
+  }
+  ~Transduction() {
+    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;
+  }
+
+public:  // Output
+  Gia_Man_t *GenerateAig() const {
+    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;
+  }
+
+public: // Debug and print
+  PfState State() const {
+    return state;
+  }
+  bool BuildDebug() {
+    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;
+  }
+  bool CspfDebug() {
+    std::vector<lit> vGsOld;
+    this->CopyVec(vGsOld, vGs);
+    std::vector<std::vector<lit> > vvCsOld;
+    this->CopyVec(vvCsOld, vvCs);
+    state = PfState::none;
+    Cspf(false);
+    bool r = this->LitVecIsEq(vGsOld, vGs) && this->LitVecIsEq(vvCsOld, vvCs);
+    this->DelVec(vGsOld);
+    this->DelVec(vvCsOld);
+    return r;
+  }
+  bool MspfDebug() {
+    std::vector<lit> vGsOld;
+    this->CopyVec(vGsOld, vGs);
+    std::vector<std::vector<lit> > vvCsOld;
+    this->CopyVec(vvCsOld, vvCs);
+    state = PfState::none;
+    Mspf(false);
+    bool r = this->LitVecIsEq(vGsOld, vGs) && this->LitVecIsEq(vvCsOld, vvCs);
+    this->DelVec(vGsOld);
+    this->DelVec(vvCsOld);
+    return r;
+  }
+  bool Verify() const {
+    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;
+  }
+  void PrintStats() const {
+    int gates = CountGates();
+    int wires = CountWires();
+    int nodes = wires - gates;
+    std::cout << "nodes = " << std::setw(5) << nodes << ", "
+              << "gates = " << std::setw(5) << gates << ", "
+              << "wires = " << std::setw(5) << wires;
+    if(fLevel)
+      std::cout << ", level = " << std::setw(5) << CountLevels();
+    std::cout << std::endl;
+  }
+  void PrintObjs() const {
+    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;
+    }
+  }
+};
+
+}
+
+#endif

src/aig/gia/module.make

@@ -103,6 +103,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaSwitch.c \
     src/aig/gia/giaTim.c \
     src/aig/gia/giaTis.c \
+    src/aig/gia/giaTransduction.cpp \
     src/aig/gia/giaTruth.c \
     src/aig/gia/giaTsim.c \
     src/aig/gia/giaTtopt.cpp \

src/base/abci/abc.c

@@ -503,6 +503,7 @@ static int Abc_CommandAbc9LNetEval           ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9LNetOpt            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //#ifndef _WIN32
 static int Abc_CommandAbc9Ttopt              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Transduction       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //#endif
 static int Abc_CommandAbc9LNetMap            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Unmap              ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1260,6 +1261,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&lnetopt",      Abc_CommandAbc9LNetOpt,      0 );
 //#ifndef _WIN32
     Cmd_CommandAdd( pAbc, "ABC9",         "&ttopt",        Abc_CommandAbc9Ttopt,        0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&transduction", Abc_CommandAbc9Transduction, 0 );
 //#endif
     Cmd_CommandAdd( pAbc, "ABC9",         "&lnetmap",      Abc_CommandAbc9LNetMap,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&unmap",        Abc_CommandAbc9Unmap,        0 );
@@ -42581,6 +42583,158 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Transduction( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp, * pExdc = NULL;
+    int c, nType = 8, fMspf = 1, nRandom = 0, nSortType = 0, nPiShuffle = 0, nParameter = 0, fLevel = 0, fBdd = 0, nVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "TSIPRVbml" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nType = 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;
+            }
+            nRandom = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nSortType = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nPiShuffle = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nParameter = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'V':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-V\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nVerbose = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'b':
+            fBdd ^= 1;
+            break;
+        case 'm':
+            fMspf ^= 1;
+            break;
+        case 'l':
+            fLevel ^= 1;
+            break;
+        case 'h':
+        default:
+            goto usage;
+        }
+    }
+    if ( argc > globalUtilOptind + 1 )
+    {
+        Abc_Print( -1, "Wrong number of auguments.\n" );
+        goto usage;
+    }
+    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, "Cannot open input file \"%s\". ", argv[globalUtilOptind] );
+            return 1;
+        }
+        fclose( pFile );
+        pExdc = Gia_AigerRead( argv[globalUtilOptind], 0, 0, 0 );
+        if ( pExdc == NULL )
+        {
+            Abc_Print( -1, "Reading AIGER has failed.\n" );
+            return 1;
+        }
+    }
+
+    if ( fBdd )
+        pTemp = Gia_ManTransductionBdd( pAbc->pGia, nType, fMspf, nRandom, nSortType, nPiShuffle, nParameter, fLevel, pExdc, nVerbose );
+    else
+        pTemp = Gia_ManTransductionTt( pAbc->pGia, nType, fMspf, nRandom, nSortType, nPiShuffle, nParameter, fLevel, pExdc, nVerbose );
+    if ( pExdc != NULL )
+        Gia_ManStop( pExdc );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &transduction [-TSIPRV num] [-bmlh] <file>\n" );
+    Abc_Print( -2, "\t           performs transduction-based AIG optimization\n" );
+    Abc_Print( -2, "\t-T num   : transduction type [default = %d]\n",                                  nType );
+    Abc_Print( -2, "\t                0: remove simply redundant nodes\n" );
+    Abc_Print( -2, "\t                1: Resub\n" );
+    Abc_Print( -2, "\t                2: ResubMono\n" );
+    Abc_Print( -2, "\t                3: ResubShared\n" );
+    Abc_Print( -2, "\t                4: repeat Resub\n" );
+    Abc_Print( -2, "\t                5: repeat ResubMono\n" );
+    Abc_Print( -2, "\t                6: RepeatResubInner\n" );
+    Abc_Print( -2, "\t                7: RepeatResubOuter\n" );
+    Abc_Print( -2, "\t                8: Optimize\n" );
+    Abc_Print( -2, "\t-S num   : fanin sort type [default = %d]\n",                                    nSortType );
+    Abc_Print( -2, "\t-I num   : random seed to shuffle pis (0 = no shuffle) [default = %d]\n",        nPiShuffle );
+    Abc_Print( -2, "\t-P num   : internal parameter [default = %d]\n",                                 nParameter );
+    Abc_Print( -2, "\t-R num   : random seed to set all parameters (0 = no random) ([default = %d]\n", nRandom );
+    Abc_Print( -2, "\t-V num   : verbosity level [default = %d]\n",                                    nVerbose);
+    Abc_Print( -2, "\t-b       : toggles using BDD instead of truth table [default = %s]\n", fBdd? "yes": "no" );
+    Abc_Print( -2, "\t-m       : toggles using MSPF [default = %s]\n", fMspf? "yes": "no" );
+    Abc_Print( -2, "\t-l       : toggles level preserving optimization [default = %s]\n", fLevel? "yes": "no" );
+    Abc_Print( -2, "\t-h       : prints the command usage\n");
+    Abc_Print( -2, "\t<file>   : AIGER specifying external don't-cares\n");
+    Abc_Print( -2, "\t\n" );
+    Abc_Print( -2, "\t           This command was contributed by Yukio Miyasaka.\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 );