From 8005405ed7cf61873b07c0ae9581680081064dc9 Mon Sep 17 00:00:00 2001
From: MyskYko <yoyuohlhjl@yahoo.co.jp>
Date: Wed, 5 Mar 2025 14:44:12 -0800
Subject: [PATCH] update rrr

---
 src/aig/gia/gia.h                |   2 +-
 src/aig/gia/giaRrr.cpp           |  10 +-
 src/base/abci/abc.c              |  51 +-
 src/opt/rrr/rrr.h                |   6 +-
 src/opt/rrr/rrrAbc.h             |   4 +-
 src/opt/rrr/rrrAnalyzer.h        |  13 +-
 src/opt/rrr/rrrAndNetwork.h      | 605 +++++++++++++++++-----
 src/opt/rrr/rrrBddAnalyzer.h     |  57 +--
 src/opt/rrr/rrrBddManager.h      | 848 +++++++++++++++++++++++++++++++
 src/opt/rrr/rrrBddMspfAnalyzer.h |  60 +--
 src/opt/rrr/rrrOptimizer.h       | 214 ++++----
 src/opt/rrr/rrrParameter.h       |   8 +-
 src/opt/rrr/rrrPartitioner.h     | 323 ++++++++++++
 src/opt/rrr/rrrSatSolver.h       |  18 +-
 src/opt/rrr/rrrScheduler.h       | 399 ++++++++++++---
 src/opt/rrr/rrrSimulator.h       |  40 +-
 src/opt/rrr/rrrTypes.h           | 146 +-----
 src/opt/rrr/rrrUtils.h           | 215 ++++++++
 18 files changed, 2448 insertions(+), 571 deletions(-)
 create mode 100644 src/opt/rrr/rrrBddManager.h
 create mode 100644 src/opt/rrr/rrrPartitioner.h
 create mode 100644 src/opt/rrr/rrrUtils.h

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index a8f3c4875..b950da4be 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1808,7 +1808,7 @@ extern Gia_Man_t *         Gia_ManTransductionBdd( Gia_Man_t * pGia, int nType,
 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 fNewLine, int nVerbose );
 
 /*=== giaRrr.cpp ===========================================================*/
-extern Gia_Man_t *         Gia_ManRrr( Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int nSchedulerVerbose, int nOptimizerVerbose, int nAnalyzerVerbose, int nSimulatorVerbose, int nSatSolverVerbose, int fUseBddCspf, int fUseBddMspf, int nConflictLimit, int nSortType, int nOptimizerFlow, int nSchedulerFlow );
+extern Gia_Man_t *         Gia_ManRrr( Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int nSchedulerVerbose, int nPartitionerVerbose, int nOptimizerVerbose, int nAnalyzerVerbose, int nSimulatorVerbose, int nSatSolverVerbose, int fUseBddCspf, int fUseBddMspf, int nConflictLimit, int nSortType, int nOptimizerFlow, int nSchedulerFlow, int nDistance, int nRestarts, int nThreads, int nWindowSize, int fDeterministic );
 
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
diff --git a/src/aig/gia/giaRrr.cpp b/src/aig/gia/giaRrr.cpp
index 21e343337..df3b91e60 100644
--- a/src/aig/gia/giaRrr.cpp
+++ b/src/aig/gia/giaRrr.cpp
@@ -5,14 +5,15 @@
 
 ABC_NAMESPACE_IMPL_START
 
-Gia_Man_t *Gia_ManRrr(Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int nSchedulerVerbose, int nOptimizerVerbose, int nAnalyzerVerbose, int nSimulatorVerbose, int nSatSolverVerbose, int fUseBddCspf, int fUseBddMspf, int nConflictLimit, int nSortType, int nOptimizerFlow, int nSchedulerFlow) {
+Gia_Man_t *Gia_ManRrr(Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int nSchedulerVerbose, int nPartitionerVerbose, int nOptimizerVerbose, int nAnalyzerVerbose, int nSimulatorVerbose, int nSatSolverVerbose, int fUseBddCspf, int fUseBddMspf, int nConflictLimit, int nSortType, int nOptimizerFlow, int nSchedulerFlow, int nDistance, int nRestarts, int nThreads, int nWindowSize, int fDeterministic) {
   rrr::AndNetwork ntk;
-  ntk.Read<Gia_Man_t>(pGia, rrr::GiaReader<rrr::AndNetwork>);
+  ntk.Read(pGia, rrr::GiaReader<rrr::AndNetwork>);
   rrr::Parameter Par;
   Par.iSeed = iSeed;
   Par.nWords = nWords;
   Par.nTimeout = nTimeout;
   Par.nSchedulerVerbose = nSchedulerVerbose;
+  Par.nPartitionerVerbose = nPartitionerVerbose;
   Par.nOptimizerVerbose = nOptimizerVerbose;
   Par.nAnalyzerVerbose = nAnalyzerVerbose;
   Par.nSimulatorVerbose = nSimulatorVerbose;
@@ -23,6 +24,11 @@ Gia_Man_t *Gia_ManRrr(Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int
   Par.nSortType = nSortType;
   Par.nOptimizerFlow = nOptimizerFlow;
   Par.nSchedulerFlow = nSchedulerFlow;
+  Par.nDistance = nDistance;
+  Par.nRestarts = nRestarts;
+  Par.nThreads = nThreads;
+  Par.nWindowSize = nWindowSize;
+  Par.fDeterministic = fDeterministic;
   rrr::Perform(&ntk, &Par);
   Gia_Man_t *pNew = rrr::CreateGia(&ntk);
   return pNew;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 04b70102a..4bf22bd88 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -45457,9 +45457,9 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t *pNew;
     int c;
-    int iSeed = 0, nWords = 10, nTimeout = 0, nSchedulerVerbose = 1, nOptimizerVerbose = 0, nAnalyzerVerbose = 0, nSimulatorVerbose = 0, nSatSolverVerbose = 0, fUseBddCspf = 0, fUseBddMspf = 0, nConflictLimit = 0, nSortType = 12, nOptimizerFlow = 0, nSchedulerFlow = 0;
+    int iSeed = 0, nWords = 10, nTimeout = 0, nSchedulerVerbose = 1, nPartitionerVerbose = 0, nOptimizerVerbose = 0, nAnalyzerVerbose = 0, nSimulatorVerbose = 0, nSatSolverVerbose = 0, fUseBddCspf = 0, fUseBddMspf = 0, nConflictLimit = 0, nSortType = 12, nOptimizerFlow = 0, nSchedulerFlow = 0, nDistance = 0, nRestarts = 0, nThreads = 1, nWindowSize = 0, fDeterministic = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "XYRWTCGSOAPQabh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "XYNJKDRWTCGVPOAQSabdh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -45471,6 +45471,22 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
             nSchedulerFlow = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
+        case 'N':
+            nRestarts = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'J':
+            nThreads = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'K':
+            nWindowSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'D':
+            nDistance = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
         case 'R':
             iSeed = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
@@ -45491,10 +45507,14 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
             nSortType = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
-        case 'S':
+        case 'V':
             nSchedulerVerbose = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
+        case 'P':
+            nPartitionerVerbose = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
         case 'O':
             nOptimizerVerbose = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
@@ -45503,11 +45523,11 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
             nAnalyzerVerbose = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
-        case 'P':
+        case 'Q':
             nSimulatorVerbose = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
-        case 'Q':
+        case 'S':
             nSatSolverVerbose = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
@@ -45517,6 +45537,9 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'b':
             fUseBddMspf ^= 1;
             break;
+        case 'd':
+            fDeterministic ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -45535,14 +45558,14 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     
-    pNew = Gia_ManRrr( pAbc->pGia, iSeed, nWords, nTimeout, nSchedulerVerbose, nOptimizerVerbose, nAnalyzerVerbose, nSimulatorVerbose, nSatSolverVerbose, fUseBddCspf, fUseBddMspf, nConflictLimit, nSortType, nOptimizerFlow, nSchedulerFlow );
+    pNew = Gia_ManRrr( pAbc->pGia, iSeed, nWords, nTimeout, nSchedulerVerbose, nPartitionerVerbose, nOptimizerVerbose, nAnalyzerVerbose, nSimulatorVerbose, nSatSolverVerbose, fUseBddCspf, fUseBddMspf, nConflictLimit, nSortType, nOptimizerFlow, nSchedulerFlow, nDistance, nRestarts, nThreads, nWindowSize, fDeterministic );
 
     Abc_FrameUpdateGia( pAbc, pNew );
     
     return 0;
 
 usage:
-      Abc_Print( -2, "usage: rrr [-XYRWTCGSOAPQ num] [-abh]\n" );
+      Abc_Print( -2, "usage: rrr [-XYNJKDRWTCGVPOAQS num] [-abdh]\n" );
       Abc_Print( -2, "\t        perform optimization\n" );
       Abc_Print( -2, "\t-X num : method [default = %d]\n", nOptimizerFlow );
       Abc_Print( -2, "\t                0: single-add resub\n" );
@@ -45552,18 +45575,24 @@ usage:
       Abc_Print( -2, "\t                0: apply method once\n" );
       Abc_Print( -2, "\t                1: iterate like transtoch\n" );
       Abc_Print( -2, "\t                2: iterate like deepsyn\n" );
+      Abc_Print( -2, "\t-N num : number of restarts or windows [default = %d]\n", nRestarts );
+      Abc_Print( -2, "\t-J num : number of threads [default = %d]\n", nThreads );
+      Abc_Print( -2, "\t-K num : window size (0 = no partitioning) [default = %d]\n", nWindowSize );
+      Abc_Print( -2, "\t-D num : distance between nodes (0 = no limit) [default = %d]\n", nDistance );
       Abc_Print( -2, "\t-R num : random number generator seed [default = %d]\n", iSeed );
       Abc_Print( -2, "\t-W num : number of simulation words [default = %d]\n", nWords );
       Abc_Print( -2, "\t-T num : timeout in seconds (0 = no timeout) [default = %d]\n", nTimeout );
-      Abc_Print( -2, "\t-C num : conflict limit [default = %d]\n", nConflictLimit );
+      Abc_Print( -2, "\t-C num : conflict limit (0 = no limit) [default = %d]\n", nConflictLimit );
       Abc_Print( -2, "\t-G num : fanin cost function [default = %d]\n", nSortType );
-      Abc_Print( -2, "\t-S num : scheduler verbosity level [default = %d]\n", nSchedulerVerbose );
+      Abc_Print( -2, "\t-V num : scheduler verbosity level [default = %d]\n", nSchedulerVerbose );
+      Abc_Print( -2, "\t-P num : partitioner verbosity level [default = %d]\n", nPartitionerVerbose );
       Abc_Print( -2, "\t-O num : optimizer verbosity level [default = %d]\n", nOptimizerVerbose );
       Abc_Print( -2, "\t-A num : analyzer verbosity level [default = %d]\n", nAnalyzerVerbose );
-      Abc_Print( -2, "\t-P num : simulator verbosity level [default = %d]\n", nSimulatorVerbose );
-      Abc_Print( -2, "\t-Q num : SAT solver verbosity level [default = %d]\n", nSatSolverVerbose );
+      Abc_Print( -2, "\t-Q num : simulator verbosity level [default = %d]\n", nSimulatorVerbose );
+      Abc_Print( -2, "\t-S num : SAT solver verbosity level [default = %d]\n", nSatSolverVerbose );
       Abc_Print( -2, "\t-a     : use BDD-based analyzer (CSPF) [default = %s]\n", fUseBddCspf? "yes": "no" );
       Abc_Print( -2, "\t-b     : use BDD-based analyzer (MSPF) [default = %s]\n", fUseBddMspf? "yes": "no" );
+      Abc_Print( -2, "\t-d     : ensure deterministic execution [default = %s]\n", fDeterministic? "yes": "no" );
       Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
diff --git a/src/opt/rrr/rrr.h b/src/opt/rrr/rrr.h
index d306da3af..f737b7ffc 100644
--- a/src/opt/rrr/rrr.h
+++ b/src/opt/rrr/rrr.h
@@ -1,15 +1,11 @@
 #pragma once
 
-#include <cassert>
-
-#include "rrrParameter.h"
-#include "rrrTypes.h"
 #include "rrrAndNetwork.h"
 #include "rrrScheduler.h"
 #include "rrrOptimizer.h"
-#include "rrrAnalyzer.h"
 #include "rrrBddAnalyzer.h"
 #include "rrrBddMspfAnalyzer.h"
+#include "rrrAnalyzer.h"
 #include "rrrSatSolver.h"
 #include "rrrSimulator.h"
 
diff --git a/src/opt/rrr/rrrAbc.h b/src/opt/rrr/rrrAbc.h
index 5fc2e1ff5..307d5e0d0 100644
--- a/src/opt/rrr/rrrAbc.h
+++ b/src/opt/rrr/rrrAbc.h
@@ -1,11 +1,11 @@
 #pragma once
 
-#include <string>
-
 #include "aig/gia/gia.h"
 #include "base/main/main.h"
 #include "base/cmd/cmd.h"
 
+#include "rrrUtils.h"
+
 ABC_NAMESPACE_CXX_HEADER_START
 
 namespace rrr {
diff --git a/src/opt/rrr/rrrAnalyzer.h b/src/opt/rrr/rrrAnalyzer.h
index a01d811c7..0689a3d11 100644
--- a/src/opt/rrr/rrrAnalyzer.h
+++ b/src/opt/rrr/rrrAnalyzer.h
@@ -1,8 +1,7 @@
 #pragma once
 
-#include <iostream>
-
 #include "rrrParameter.h"
+#include "rrrUtils.h"
 
 ABC_NAMESPACE_CXX_HEADER_START
 
@@ -23,7 +22,7 @@ namespace rrr {
 
   public:
     // constructors
-    Analyzer(Ntk *pNtk, Parameter const *pPar);
+    Analyzer(Parameter const *pPar);
     void UpdateNetwork(Ntk *pNtk_, bool fSame);
 
     // checks
@@ -34,11 +33,11 @@ namespace rrr {
   /* {{{ Constructors */
   
   template <typename Ntk, typename Sim, typename Sol>
-  Analyzer<Ntk, Sim, Sol>::Analyzer(Ntk *pNtk, Parameter const *pPar) :
-    pNtk(pNtk),
+  Analyzer<Ntk, Sim, Sol>::Analyzer(Parameter const *pPar) :
+    pNtk(NULL),
     nVerbose(pPar->nAnalyzerVerbose),
-    sim(pNtk, pPar),
-    sol(pNtk, pPar) {
+    sim(pPar),
+    sol(pPar) {
   }
   
   template <typename Ntk, typename Sim, typename Sol>
diff --git a/src/opt/rrr/rrrAndNetwork.h b/src/opt/rrr/rrrAndNetwork.h
index 2d321186c..00afd2386 100644
--- a/src/opt/rrr/rrrAndNetwork.h
+++ b/src/opt/rrr/rrrAndNetwork.h
@@ -1,17 +1,12 @@
 #pragma once
 
-#include <iostream>
-#include <vector>
+#include <utility>
 #include <list>
-#include <set>
-#include <initializer_list>
-#include <string>
-#include <functional>
+#include <map>
 #include <algorithm>
-#include <limits>
 
 #include "rrrParameter.h"
-#include "rrrTypes.h"
+#include "rrrUtils.h"
 
 ABC_NAMESPACE_CXX_HEADER_START
 
@@ -57,8 +52,9 @@ namespace rrr {
     // other private functions
     int  CreateNode();
     void SortInts(itr it);
-    void StartTraversal();
+    unsigned StartTraversal(int n = 1);
     void EndTraversal();
+    void ForEachTfiRec(int id, std::function<void(int)> const &f);
     void TakenAction(Action const &action) const;
 
   public:
@@ -71,8 +67,8 @@ namespace rrr {
     void Clear();
     void Reserve(int nReserve);
     int  AddPi();
-    int  AddPo(int id, bool c);
     int  AddAnd(int id0, int id1, bool c0, bool c1);
+    int  AddPo(int id, bool c);
     template <typename Ntk, typename Reader>
     void Read(Ntk *pFrom, Reader &reader);
 
@@ -84,6 +80,7 @@ namespace rrr {
     int  GetNumPos() const;
     int  GetConst0() const;
     int  GetPi(int idx) const;
+    int  GetPo(int idx) const;
     std::vector<int> GetPis() const;
     std::vector<int> GetInts() const;
     std::vector<int> GetPisInts() const;
@@ -104,17 +101,31 @@ namespace rrr {
     bool GetCompl(int id, int idx) const;
     int  FindFanin(int id, int fi) const;
     bool IsReconvergent(int id);
+    std::vector<int> GetNeighbors(int id, bool fPis, int nHops);
+    template <template <typename...> typename Container, typename ... Ts, template <typename...> typename Container2, typename ... Ts2>
+    bool IsReachable(Container<Ts...> const &srcs, Container2<Ts2...> const &dsts);
+    template <template <typename...> typename Container, typename ... Ts, template <typename...> typename Container2, typename ... Ts2>
+    std::vector<int> GetInners(Container<Ts...> const &srcs, Container2<Ts2...> const &dsts);
 
     // network traversal
     void ForEachPi(std::function<void(int)> const &func) const;
     void ForEachInt(std::function<void(int)> const &func) const;
     void ForEachIntReverse(std::function<void(int)> const &func) const;
+    void ForEachPiInt(std::function<void(int)> const &func) const;
     void ForEachPo(std::function<void(int)> const &func) const;
-    void ForEachPoDriver(std::function<void(int, bool)> const &func) const;
-    void ForEachFanin(int id, std::function<void(int, bool)> const &func) const;
-    void ForEachFaninIdx(int id, std::function<void(int, int, bool)> const &func) const; // func(fi, c, index of fi in fanin list of id)
-    void ForEachFanout(int id, bool fPos, std::function<void(int, bool)> const &func) const;
-    void ForEachFanoutRidx(int id, bool fPos, std::function<void(int, bool, int)> const &func) const; // func(fo, c, index of id in fanin list of fo)
+    template <typename Func>
+    void ForEachPoDriver(Func const &func) const;
+    template <typename Func>
+    void ForEachFanin(int id, Func const &func) const;
+    template <typename Func>
+    void ForEachFaninIdx(int id, Func const &func) const; // func(index of fi in fanin list of id, fi[, c])
+    template <typename Func>
+    void ForEachFanout(int id, bool fPos, Func const &func) const;
+    template <typename Func>
+    void ForEachFanoutRidx(int id, bool fPos, Func const &func) const; // func(fo[, c], index of id in fanin list of fo)
+    void ForEachTfi(int id, bool fPis, std::function<void(int)> const &func);
+    template <template <typename...> typename Container, typename ... Ts>
+    void ForEachTfiEnd(int id, Container<Ts...> const &ends, std::function<void(int)> const &func);
     void ForEachTfo(int id, bool fPos, std::function<void(int)> const &func);
     void ForEachTfoReverse(int id, bool fPos, std::function<void(int)> const &func);
     void ForEachTfoUpdate(int id, bool fPos, std::function<bool(int)> const &func);
@@ -123,19 +134,25 @@ namespace rrr {
     template <template <typename...> typename Container, typename ... Ts>
     void ForEachTfosUpdate(Container<Ts...> const &ids, bool fPos, std::function<bool(int)> const &func);
 
-    // Actions
+    // extraction
+    template <template <typename...> typename Container, typename ... Ts>
+    AndNetwork *Extract(Container<Ts...> const &ids, std::vector<int> const &vInputs, std::vector<int> const &vOutputs);
+
+    // actions
     void RemoveFanin(int id, int idx);
-    void RemoveUnused(int id, bool fRecursive = false);
+    void RemoveUnused(int id, bool fRecursive = false, bool fSweeping = false);
     void RemoveBuffer(int id);
     void RemoveConst(int id);
     void AddFanin(int id, int fi, bool c);
     void TrivialCollapse(int id);
     void TrivialDecompose(int id);
-    void SortFanins(int id, std::function<bool(int, bool, int, bool)> const &cost);
+    template <typename Func>
+    void SortFanins(int id, Func const &cost);
+    std::pair<std::vector<int>, std::vector<bool>> Insert(AndNetwork *pNtk, std::vector<int> const &vInputs, std::vector<bool> const &vCompls, std::vector<int> const &vOutputs);
 
     // Network cleanup
     void Propagate(int id = -1); // all nodes unless specified
-    void Sweep(bool fPropagate);
+    void Sweep(bool fPropagate = true);
 
     // save & load
     int  Save(int slot = -1); // slot is assigned automatically unless specified
@@ -153,12 +170,12 @@ namespace rrr {
     // TODO: reuse already allocated but dead nodes? or perform garbage collection?
     vvFaninEdges.emplace_back();
     vRefs.push_back(0);
-    assert(nNodes != std::numeric_limits<int>::max());
+    assert(!check_int_max(nNodes));
     return nNodes++;
   }
 
   void AndNetwork::SortInts(itr it) {
-    ForEachFanin(*it, [&](int fi, bool c) {
+    ForEachFanin(*it, [&](int fi) {
       itr it2 = std::find(it, lInts.end(), fi);
       if(it2 != lInts.end()) {
         lInts.erase(it2);
@@ -168,18 +185,38 @@ namespace rrr {
     });
   }
 
-  inline void AndNetwork::StartTraversal() {
+  inline unsigned AndNetwork::StartTraversal(int n) {
     assert(!fLockTrav);
     fLockTrav = true;
+    do {
+      for(int i = 0; i < n; i++) {
+        iTrav++;
+        if(iTrav == 0) {
+          vTrav.clear();
+          break;
+        }
+      }
+    } while(iTrav == 0);
     vTrav.resize(nNodes);
-    iTrav++;
-    assert(iTrav != 0); //TODO: handle this overflow
+    return iTrav - n + 1;
   }
   
   inline void AndNetwork::EndTraversal() {
     assert(fLockTrav);
     fLockTrav = false;
   }
+
+  void AndNetwork::ForEachTfiRec(int id, std::function<void(int)> const &func) {
+    for(int fi_edge: vvFaninEdges[id]) {
+      int fi = Edge2Node(fi_edge);
+      if(vTrav[fi] == iTrav) {
+        continue;
+      }
+      func(fi);
+      vTrav[fi] = iTrav;
+      ForEachTfiRec(fi, func);
+    }
+  }
   
   inline void AndNetwork::TakenAction(Action const &action) const {
     for(Callback const &callback: vCallbacks) {
@@ -259,7 +296,7 @@ namespace rrr {
     vPis.push_back(nNodes);
     vvFaninEdges.emplace_back();
     vRefs.push_back(0);
-    assert(nNodes != std::numeric_limits<int>::max());
+    assert(!check_int_max(nNodes));
     return nNodes++;
   }
   
@@ -273,7 +310,7 @@ namespace rrr {
     vRefs[id1]++;
     vvFaninEdges.emplace_back(std::initializer_list<int>({Node2Edge(id0, c0), Node2Edge(id1, c1)}));
     vRefs.push_back(0);
-    assert(nNodes != std::numeric_limits<int>::max());
+    assert(!check_int_max(nNodes));
     return nNodes++;
   }
 
@@ -283,7 +320,7 @@ namespace rrr {
     vRefs[id]++;
     vvFaninEdges.emplace_back(std::initializer_list<int>({Node2Edge(id, c)}));
     vRefs.push_back(0);
-    assert(nNodes != std::numeric_limits<int>::max());
+    assert(!check_int_max(nNodes));
     return nNodes++;
   }
 
@@ -306,18 +343,15 @@ namespace rrr {
   }
 
   inline int AndNetwork::GetNumPis() const {
-    assert(vPis.size() <= (std::vector<int>::size_type)std::numeric_limits<int>::max());
-    return vPis.size();
+    return int_size(vPis);
   }
   
   inline int AndNetwork::GetNumInts() const {
-    assert(lInts.size() <= (std::vector<int>::size_type)std::numeric_limits<int>::max());
-    return lInts.size();
+    return int_size(lInts);
   }
   
   inline int AndNetwork::GetNumPos() const {
-    assert(vPos.size() <= (std::vector<int>::size_type)std::numeric_limits<int>::max());
-    return vPos.size();
+    return int_size(vPos);
   }
 
   inline int AndNetwork::GetConst0() const {
@@ -328,6 +362,10 @@ namespace rrr {
     return vPis[idx];
   }
 
+  inline int AndNetwork::GetPo(int idx) const {
+    return vPos[idx];
+  }
+
   inline std::vector<int> AndNetwork::GetPis() const {
     return vPis;
   }
@@ -381,39 +419,38 @@ namespace rrr {
     return false;
   }
 
-  int AndNetwork::GetPiIndex(int id) const {
+  inline int AndNetwork::GetPiIndex(int id) const {
     assert(IsPi(id));
-    assert(vPis.size() <= (std::vector<int>::size_type)std::numeric_limits<int>::max());
+    assert(check_int_size(vPis));
     std::vector<int>::const_iterator it = std::find(vPis.begin(), vPis.end(), id);
     assert(it != vPis.end());
     return std::distance(vPis.begin(), it);
   }
   
-  int AndNetwork::GetIntIndex(int id) const {
+  inline int AndNetwork::GetIntIndex(int id) const {
+    assert(check_int_size(lInts));
     int index = 0;
     citr it = lInts.begin();
     for(; it != lInts.end(); it++) {
       if(*it == id) {
         break;
       }
-      assert(index < (std::vector<int>::size_type)std::numeric_limits<int>::max());
       index++;
     }
     assert(it != lInts.end());
     return index;
   }
 
-  int AndNetwork::GetPoIndex(int id) const {
+  inline int AndNetwork::GetPoIndex(int id) const {
     assert(IsPo(id));
-    assert(vPos.size() <= (std::vector<int>::size_type)std::numeric_limits<int>::max());
+    assert(check_int_size(vPos));
     std::vector<int>::const_iterator it = std::find(vPos.begin(), vPos.end(), id);
     assert(it != vPos.end());
     return std::distance(vPos.begin(), it);
   }
   
   inline int AndNetwork::GetNumFanins(int id) const {
-    //assert(vvFaninEdges[id].size() <= (std::vector<int>::size_type)std::numeric_limits<int>::max());
-    return vvFaninEdges[id].size();
+    return int_size(vvFaninEdges[id]);
   }
 
   inline int AndNetwork::GetNumFanouts(int id) const {
@@ -441,16 +478,14 @@ namespace rrr {
     if(GetNumFanouts(id) <= 1) {
       return false;
     }
-    StartTraversal();
-    unsigned iTravStart = iTrav;
-    ForEachFanout(id, false, [&](int fo, bool c) {
-      vTrav[fo] = iTrav;
-      iTrav++;
-      assert(iTrav != 0); //TODO: handle this overflow
+    unsigned iTravStart = StartTraversal(GetNumFanouts(id));
+    int idx = 0;
+    ForEachFanout(id, false, [&](int fo) {
+      vTrav[fo] = iTravStart + idx;
+      idx++;
     });
-    iTrav--;
-    if(iTrav <= iTravStart) {
-      // less than one fanouts excluding POs
+    if(idx <= 1) {
+      // less than two fanouts excluding POs
       EndTraversal();
       return false;
     }
@@ -475,6 +510,161 @@ namespace rrr {
     return false;
   }
 
+  inline std::vector<int> AndNetwork::GetNeighbors(int id, bool fPis, int nHops) {
+    StartTraversal();
+    vTrav[id] = iTrav;
+    std::vector<int> vPrevs, vNexts;
+    vNexts.push_back(id);
+    for(int i = 0; i < nHops; i++) {
+      vPrevs.swap(vNexts);
+      for(int id: vPrevs) {
+        ForEachFanin(id, [&](int fi) {
+          if(vTrav[fi] != iTrav) {
+            vNexts.push_back(fi);
+            vTrav[fi] = iTrav;
+          }
+        });
+        ForEachFanout(id, false, [&](int fo) {
+          if(vTrav[fo] != iTrav) {
+            vNexts.push_back(fo);
+            vTrav[fo] = iTrav;
+          }
+        });
+      }
+      vPrevs.clear();
+    }
+    vTrav[id] = 0;
+    std::vector<int> v;
+    if(fPis) {
+      ForEachPiInt([&](int id) {
+        if(vTrav[id] == iTrav) {
+          v.push_back(id);
+        }
+      });
+    } else {
+      ForEachInt([&](int id) {
+        if(vTrav[id] == iTrav) {
+          v.push_back(id);
+        }
+      });
+    }
+    EndTraversal();
+    return v;
+  }
+
+  template <template <typename...> typename Container, typename ... Ts, template <typename...> typename Container2, typename ... Ts2>
+  inline bool AndNetwork::IsReachable(Container<Ts...> const &srcs, Container2<Ts2...> const &dsts) {
+    if(srcs.empty() || dsts.empty()) {
+      return false;
+    }
+    // mark destinations
+    unsigned iTravStart = StartTraversal(2);
+    for(int id: dsts) {
+      vTrav[id] = iTravStart;
+    }
+    // mark sources
+    for(int id: srcs) {
+      if(vTrav[id] == iTravStart) {
+        EndTraversal();
+        return true;
+      }
+      vTrav[id] = iTrav;
+    }
+    // find the first source
+    citr it = lInts.begin();
+    while(vTrav[*it] != iTrav && it != lInts.end()) {
+      it++;
+    }
+    // check if sources are reachable to destinations
+    for(; it != lInts.end(); it++) {
+      if(vTrav[*it] == iTrav) {
+        continue;
+      }
+      for(int fi_edge: vvFaninEdges[*it]) {
+        if(vTrav[Edge2Node(fi_edge)] == iTrav) {
+          if(vTrav[*it] == iTravStart) {
+            EndTraversal();
+            return true;
+          }
+          vTrav[*it] = iTrav;
+          break;
+        }
+      }
+    }
+    for(int po: vPos) {
+      if(vTrav[po] == iTrav) {
+        continue;
+      }
+      if(vTrav[GetFanin(po, 0)] == iTrav) {
+        if(vTrav[po] == iTravStart) {
+          EndTraversal();
+          return true;
+        }
+        vTrav[po] = iTrav;
+      }
+    }
+    EndTraversal();
+    return false;
+  }
+
+  template <template <typename...> typename Container, typename ... Ts, template <typename...> typename Container2, typename ... Ts2>
+  inline std::vector<int> AndNetwork::GetInners(Container<Ts...> const &srcs, Container2<Ts2...> const &dsts) {
+    // this includes sources and destinations that are connected
+    if(srcs.empty() || dsts.empty()) {
+      return std::vector<int>();
+    }
+    unsigned iTravStart = StartTraversal(4);
+    unsigned iDst = iTravStart;
+    unsigned iTfo = iTravStart + 1;
+    unsigned iInner = iTravStart + 2;
+    // mark destinations (to prevent nodes between destinations to sources being included)
+    for(int id: dsts) {
+      vTrav[id] = iDst;
+    }
+    // mark TFOs of sources until destinations, which will be marekd as inner
+    for(int id: srcs) {
+      if(vTrav[id] == iDst) {
+        vTrav[id] = iInner;
+      } else {
+        vTrav[id] = iTfo;
+      }
+    }
+    citr it = lInts.begin();
+    while(vTrav[*it] != iTfo && it != lInts.end()) {
+      it++;
+    }
+    for(; it != lInts.end(); it++) {
+      if(vTrav[*it] >= iTfo) { // TFO or inner
+        continue;
+      }
+      for(int fi_edge: vvFaninEdges[*it]) {
+        if(vTrav[Edge2Node(fi_edge)] == iTfo) {
+          if(vTrav[*it] == iDst) {
+            vTrav[*it] = iInner;
+          } else {
+            vTrav[*it] = iTfo;
+          }
+          break;
+        }
+      }
+    }
+    // traverse TFIs of connected destinations
+    std::vector<int> vInners;
+    for(int id: dsts) {
+      if(vTrav[id] == iInner) {
+        vInners.push_back(id);
+        vTrav[id] = iTrav;
+        ForEachTfiRec(id, [&](int fi) {
+          if(vTrav[fi] == iTfo || vTrav[fi] == iInner) {
+            vInners.push_back(fi);
+          }
+        });
+      }
+    }
+    EndTraversal();
+    return vInners;
+  }
+
   /* }}} */
 
   /* {{{ Network traversal */
@@ -497,49 +687,89 @@ namespace rrr {
     }
   }
 
+  inline void AndNetwork::ForEachPiInt(std::function<void(int)> const &func) const {
+    for(int pi: vPis) {
+      func(pi);
+    }
+    for(int id: lInts) {
+      func(id);
+    }
+  }
+  
   inline void AndNetwork::ForEachPo(std::function<void(int)> const &func) const {
     for(int po: vPos) {
       func(po);
     }
   }
-  
-  inline void AndNetwork::ForEachPoDriver(std::function<void(int, bool)> const &func) const {
+
+  template <typename Func>
+  inline void AndNetwork::ForEachPoDriver(Func const &func) const {
+    static_assert(is_invokable<Func, int>::value || is_invokable<Func, int, bool>::value, "for each edge function format error");
     for(int po: vPos) {
-      func(GetFanin(po, 0), GetCompl(po, 0));
-    }
-  }
-  
-  inline void AndNetwork::ForEachFanin(int id, std::function<void(int, bool)> const &func) const {
-    for(int fi_edge: vvFaninEdges[id]) {
-      func(Edge2Node(fi_edge), EdgeIsCompl(fi_edge));
+      if constexpr(is_invokable<Func, int>::value) {
+        func(GetFanin(po, 0));
+      } else if constexpr(is_invokable<Func, int, bool>::value) {
+        func(GetFanin(po, 0), GetCompl(po, 0));
+      }
     }
   }
 
-  inline void AndNetwork::ForEachFaninIdx(int id, std::function<void(int, int, bool)> const &func) const {
+  template <typename Func>
+  inline void AndNetwork::ForEachFanin(int id, Func const &func) const {
+    static_assert(is_invokable<Func, int>::value || is_invokable<Func, int, bool>::value, "for each edge function format error");
+    for(int fi_edge: vvFaninEdges[id]) {
+      if constexpr(is_invokable<Func, int>::value) {
+        func(Edge2Node(fi_edge));
+      } else if constexpr(is_invokable<Func, int, bool>::value) {
+        func(Edge2Node(fi_edge), EdgeIsCompl(fi_edge));
+      }
+    }
+  }
+
+  template <typename Func>
+  inline void AndNetwork::ForEachFaninIdx(int id, Func const &func) const {
+    static_assert(is_invokable<Func, int, int>::value || is_invokable<Func, int, int, bool>::value, "for each edge function format error");
     for(int idx = 0; idx < GetNumFanins(id); idx++) {
-      func(idx, GetFanin(id, idx), GetCompl(id, idx));
+      if constexpr(is_invokable<Func, int, int>::value) {
+        func(idx, GetFanin(id, idx));
+      } else if constexpr(is_invokable<Func, int, int, bool>::value) {
+        func(idx, GetFanin(id, idx), GetCompl(id, idx));
+      }
     }
   }
   
-  inline void AndNetwork::ForEachFanout(int id, bool fPos, std::function<void(int, bool)> const &func) const {
+  template <typename Func>
+  inline void AndNetwork::ForEachFanout(int id, bool fPos, Func const &func) const {
+    static_assert(is_invokable<Func, int>::value || is_invokable<Func, int, bool>::value, "for each edge function format error");
     if(vRefs[id] == 0) {
       return;
     }
-    citr it = std::find(lInts.begin(), lInts.end(), id);
-    assert(it != lInts.end());
-    it++;
+    citr it = lInts.begin();
+    if(IsInt(id)) {
+      it = std::find(it, lInts.end(), id);
+      assert(it != lInts.end());
+      it++;
+    }
     int nRefs = vRefs[id];
     for(; nRefs != 0 && it != lInts.end(); it++) {
       int idx = FindFanin(*it, id);
       if(idx >= 0) {
-        func(*it, GetCompl(*it, idx));
+        if constexpr(is_invokable<Func, int>::value) {
+          func(*it);
+        } else if constexpr(is_invokable<Func, int, bool>::value) {
+          func(*it, GetCompl(*it, idx));
+        }
         nRefs--;
       }
     }
     if(fPos && nRefs != 0) {
       for(int po: vPos) {
         if(GetFanin(po, 0) == id) {
-          func(po, GetCompl(po, 0));
+          if constexpr(is_invokable<Func, int>::value) {
+            func(po);
+          } else if constexpr(is_invokable<Func, int, bool>::value) {
+            func(po, GetCompl(po, 0));
+          }
           nRefs--;
           if(nRefs == 0) {
             break;
@@ -549,26 +779,39 @@ namespace rrr {
     }
     assert(!fPos || nRefs == 0);
   }
-  
-  inline void AndNetwork::ForEachFanoutRidx(int id, bool fPos, std::function<void(int, bool, int)> const &func) const {
+
+  template <typename Func>
+  inline void AndNetwork::ForEachFanoutRidx(int id, bool fPos, Func const &func) const {
+    static_assert(is_invokable<Func, int, int>::value || is_invokable<Func, int, bool, int>::value, "for each edge function format error");
     if(vRefs[id] == 0) {
       return;
     }
-    citr it = std::find(lInts.begin(), lInts.end(), id);
-    assert(it != lInts.end());
-    it++;
+    citr it = lInts.begin();
+    if(IsInt(id)) {
+      it = std::find(it, lInts.end(), id);
+      assert(it != lInts.end());
+      it++;
+    }
     int nRefs = vRefs[id];
     for(; nRefs != 0 && it != lInts.end(); it++) {
       int idx = FindFanin(*it, id);
       if(idx >= 0) {
-        func(*it, GetCompl(*it, idx), idx);
+        if constexpr(is_invokable<Func, int, int>::value) {
+          func(*it, idx);
+        } else if constexpr(is_invokable<Func, int, bool, int>::value) {
+          func(*it, GetCompl(*it, idx), idx);
+        }
         nRefs--;
       }
     }
     if(fPos && nRefs != 0) {
       for(int po: vPos) {
         if(GetFanin(po, 0) == id) {
-          func(po, GetCompl(po, 0), 0);
+          if constexpr(is_invokable<Func, int, int>::value) {
+            func(po, 0);
+          } else if constexpr(is_invokable<Func, int, bool, int>::value) {
+            func(po, GetCompl(po, 0), 0);
+          }
           nRefs--;
           if(nRefs == 0) {
             break;
@@ -578,7 +821,30 @@ namespace rrr {
     }
     assert(!fPos || nRefs == 0);
   }
-  
+
+  inline void AndNetwork::ForEachTfi(int id, bool fPis, std::function<void(int)> const &func) {
+    // this does not include id itself
+    StartTraversal();
+    if(!fPis) {
+      for(int pi: vPis) {
+        vTrav[pi] = iTrav;
+      }
+    }
+    ForEachTfiRec(id, func);
+    EndTraversal();
+  }
+
+  template <template <typename...> typename Container, typename ... Ts>
+  inline void AndNetwork::ForEachTfiEnd(int id, Container<Ts...> const &ends, std::function<void(int)> const &func) {
+    // this does not include id itself
+    StartTraversal();
+    for(int end: ends) {
+      vTrav[end] = iTrav;
+    }
+    ForEachTfiRec(id, func);
+    EndTraversal();
+  }
+
   inline void AndNetwork::ForEachTfo(int id, bool fPos, std::function<void(int)> const &func) {
     // this does not include id itself
     if(vRefs[id] == 0) {
@@ -763,6 +1029,44 @@ namespace rrr {
     EndTraversal();
   }
 
+  /* }}} */
+
+  /* {{{ Extraction */
+
+  template <template <typename...> typename Container, typename ... Ts>
+  AndNetwork *AndNetwork::Extract(Container<Ts...> const &ids, std::vector<int> const &vInputs, std::vector<int> const &vOutputs) {
+    AndNetwork *pNtk = new AndNetwork;
+    pNtk->Reserve(int_size(vInputs) + int_size(ids) + int_size(vOutputs));
+    std::map<int, int> m;
+    m[GetConst0()] = pNtk->GetConst0();
+    for(int id: vInputs) {
+      m[id] = pNtk->AddPi();
+    }
+    StartTraversal();
+    for(int id: ids) {
+      vTrav[id] = iTrav;
+    }
+    ForEachInt([&](int id) {
+      if(vTrav[id] == iTrav) {
+        m[id] = pNtk->CreateNode();
+        pNtk->lInts.push_back(m[id]);
+        pNtk->sInts.insert(m[id]);
+        pNtk->vvFaninEdges[m[id]].resize(GetNumFanins(id));
+        ForEachFaninIdx(id, [&](int idx, int fi, bool c) {
+          assert(m.count(fi));
+          pNtk->vvFaninEdges[m[id]][idx] = pNtk->Node2Edge(m[fi], c);
+          pNtk->vRefs[m[fi]]++;
+        });
+      }
+    });
+    EndTraversal();
+    for(int id: vOutputs) {
+      assert(m.count(id));
+      pNtk->AddPo(m[id], false);
+    }
+    return pNtk;
+  }
+  
   /* }}} */
   
   /* {{{ Actions */
@@ -781,24 +1085,26 @@ namespace rrr {
     TakenAction(action);
   }
 
-  void AndNetwork::RemoveUnused(int id, bool fRecursive) {
+  void AndNetwork::RemoveUnused(int id, bool fRecursive, bool fSweeping) {
     assert(vRefs[id] == 0);
     Action action;
     action.type = REMOVE_UNUSED;
     action.id = id;
-    ForEachFanin(id, [&](int fi, bool c) {
+    ForEachFanin(id, [&](int fi) {
       action.vFanins.push_back(fi);
       vRefs[fi]--;
     });
     vvFaninEdges[id].clear();
-    itr it = std::find(lInts.begin(), lInts.end(), id);
-    lInts.erase(it);
+    if(!fSweeping) {
+      itr it = std::find(lInts.begin(), lInts.end(), id);
+      lInts.erase(it);
+    }
     sInts.erase(id);
     TakenAction(action);
     if(fRecursive) {
       for(int fi: action.vFanins) {
-        if(vRefs[fi] == 0) {
-          RemoveUnused(fi, true);
+        if(vRefs[fi] == 0 && IsInt(fi)) {
+          RemoveUnused(fi, fRecursive, fSweeping);
         }
       }
     }
@@ -885,7 +1191,7 @@ namespace rrr {
     });
     // remove node
     vRefs[id] = 0;
-    ForEachFanin(id, [&](int fi, bool c) {
+    ForEachFanin(id, [&](int fi) {
       vRefs[fi]--;
       action.vFanins.push_back(fi);
     });
@@ -904,7 +1210,7 @@ namespace rrr {
     Action action;
     action.type = ADD_FANIN;
     action.id = id;
-    action.idx = vvFaninEdges[id].size();
+    action.idx = GetNumFanins(id);
     action.fi = fi;
     action.c = c;
     itr it = std::find(lInts.begin(), lInts.end(), id);
@@ -934,7 +1240,7 @@ namespace rrr {
         std::vector<int>::iterator it = vvFaninEdges[id].begin() + idx;
         it = vvFaninEdges[id].erase(it);
         vvFaninEdges[id].insert(it, vvFaninEdges[fi].begin(), vvFaninEdges[fi].end());
-        ForEachFanin(fi, [&](int fi, bool c) {
+        ForEachFanin(fi, [&](int fi) {
           action.vFanins.push_back(fi);
         });
         // remove collapsed fanin
@@ -954,7 +1260,7 @@ namespace rrr {
       Action action;
       action.type = TRIVIAL_DECOMPOSE;
       action.id = id;
-      action.idx = vvFaninEdges[id].size() - 2;
+      action.idx = GetNumFanins(id) - 2;
       int new_fi = CreateNode();
       action.fi = new_fi;
       int fi_edge1 = vvFaninEdges[id].back();
@@ -974,10 +1280,16 @@ namespace rrr {
     }
   }
 
-  void AndNetwork::SortFanins(int id, std::function<bool(int, bool, int, bool)> const &comp) {
+  template <typename Func>
+  void AndNetwork::SortFanins(int id, Func const &comp) {
+    static_assert(is_invokable<Func, int, int>::value || is_invokable<Func, int, bool, int, bool>::value, "fanin cost function format error");
     std::vector<int> vFaninEdges = vvFaninEdges[id];
     std::sort(vvFaninEdges[id].begin(), vvFaninEdges[id].end(), [&](int i, int j) {
-      return comp(Edge2Node(i), EdgeIsCompl(i), Edge2Node(j), EdgeIsCompl(j));
+      if constexpr(is_invokable<Func, int, int>::value) {
+        return comp(Edge2Node(i), Edge2Node(j));
+      } else if constexpr(is_invokable<Func, int, bool, int, bool>::value) {
+        return comp(Edge2Node(i), EdgeIsCompl(i), Edge2Node(j), EdgeIsCompl(j));
+      }
     });
     if(vFaninEdges == vvFaninEdges[id]) {
       return;
@@ -985,7 +1297,7 @@ namespace rrr {
     Action action;
     action.type = SORT_FANINS;
     action.id = id;
-    assert(vFaninEdges.size() <= (std::vector<int>::size_type)std::numeric_limits<int>::max());
+    assert(check_int_size(vFaninEdges));
     for(int fanin_edge: vvFaninEdges[id]) {
       std::vector<int>::const_iterator it = std::find(vFaninEdges.begin(), vFaninEdges.end(), fanin_edge);
       action.vIndices.push_back(std::distance(vFaninEdges.cbegin(), it));
@@ -993,6 +1305,79 @@ namespace rrr {
     TakenAction(action);
   }
 
+  std::pair<std::vector<int>, std::vector<bool>> AndNetwork::Insert(AndNetwork *pNtk, std::vector<int> const &vInputs, std::vector<bool> const &vCompls, std::vector<int> const &vOutputs) {
+    Reserve(nNodes + pNtk->GetNumInts());
+    std::map<int, std::pair<int, bool>> m;
+    m[pNtk->GetConst0()] = std::make_pair(GetConst0(), false);
+    assert(pNtk->GetNumPis() == int_size(vInputs));
+    assert(vInputs.size() == vCompls.size());
+    for(int i = 0; i < pNtk->GetNumPis(); i++) {
+      assert(IsInt(vInputs[i]) || IsPi(vInputs[i]));
+      m[pNtk->GetPi(i)] = std::make_pair(vInputs[i], vCompls[i]);
+    }
+    pNtk->ForEachInt([&](int id) {
+      int id2 = CreateNode();
+      lInts.push_back(id2);
+      sInts.insert(id2);
+      vvFaninEdges[id2].resize(pNtk->GetNumFanins(id));
+      pNtk->ForEachFaninIdx(id, [&](int idx, int fi, bool c) {
+        assert(m.count(fi));
+        vvFaninEdges[id2][idx] = Node2Edge(m[fi].first, c ^ m[fi].second);
+        vRefs[m[fi].first]++;
+      });
+      m[id] = std::make_pair(id2, false);
+    });
+    assert(pNtk->GetNumPos() == int_size(vOutputs));
+    std::vector<int> vNewOutputs(pNtk->GetNumPos());
+    std::vector<bool> vNewCompls(pNtk->GetNumPos());
+    for(int i = 0; i < pNtk->GetNumPos(); i++) {
+      int id = vOutputs[i];
+      int po = pNtk->GetPo(i);
+      assert(m.count(pNtk->GetFanin(po, 0)));
+      int fi = m[pNtk->GetFanin(po, 0)].first;
+      bool c = pNtk->GetCompl(po, 0) ^ m[pNtk->GetFanin(po, 0)].second;
+      assert(id != fi);
+      vNewOutputs[i] = fi;
+      vNewCompls[i] = c;
+      // remove if substitution would lead to duplication with the same polarity
+      ForEachFanoutRidx(id, false, [&](int fo, bool foc, int idx) {
+        int idx2 = FindFanin(fo, fi);
+        if(idx2 != -1 && GetCompl(fo, idx2) == (c ^ foc)) {
+          RemoveFanin(fo, idx);
+        }
+      });
+      ForEachFanoutRidx(id, true, [&](int fo, bool foc, int idx) {
+        int idx2 = FindFanin(fo, fi);
+        if(idx2 != -1) { // substitute with const-0 in case of duplication
+          assert(GetCompl(fo, idx2) != (c ^ foc)); // of a different polarity
+          vRefs[GetConst0()]++;
+          vvFaninEdges[fo][idx] = Node2Edge(GetConst0(), 0);
+        } else { // otherwise, substitute with fanin
+          vvFaninEdges[fo][idx] = Node2Edge(fi, c ^ foc);
+          vRefs[fi]++;
+          // sort internal nodes
+          itr it = std::find(lInts.begin(), lInts.end(), id);
+          itr it2 = std::find(it, lInts.end(), fi);
+          if(it2 != lInts.end()) {
+            lInts.erase(it2);
+            it2 = lInts.insert(it, fi);
+            SortInts(it2);
+          }
+        }
+      });
+      vRefs[id] = 0;
+    }
+    Action action;
+    action.type = INSERT;
+    action.vFanins = vInputs;
+    action.vFanouts = vOutputs;
+    TakenAction(action);
+    for(int id: vOutputs) {
+      RemoveUnused(id, true);
+    }
+    return std::make_pair(std::move(vNewOutputs), std::move(vNewCompls));
+  }
+
   /* }}} */
 
   /* {{{ Network cleanup */
@@ -1037,7 +1422,7 @@ namespace rrr {
     }
     for(ritr it = lInts.rbegin(); it != lInts.rend();) {
       if(vRefs[*it] == 0) {
-        RemoveUnused(*it);
+        RemoveUnused(*it, false, true);
         it = ritr(lInts.erase(--it.base()));
       } else {
         it++;
@@ -1053,10 +1438,11 @@ namespace rrr {
     Action action;
     action.type = SAVE;
     if(slot < 0) {
-      slot = vBackups.size();
+      slot = int_size(vBackups);
       vBackups.push_back(*this);
+      assert(check_int_size(vBackups));
     } else {
-      assert(slot < vBackups.size());
+      assert(slot < int_size(vBackups));
       vBackups[slot] = *this;
     }
     action.idx = slot;
@@ -1065,7 +1451,8 @@ namespace rrr {
   }
 
   void AndNetwork::Load(int slot) {
-    assert(slot < vBackups.size());
+    assert(slot >= 0);
+    assert(slot < int_size(vBackups));
     Action action;
     action.type = LOAD;
     action.idx = slot;
@@ -1077,7 +1464,7 @@ namespace rrr {
     assert(!vBackups.empty());
     Action action;
     action.type = POP_BACK;
-    action.idx = vBackups.size() - 1;
+    action.idx = int_size(vBackups) - 1;
     vBackups.pop_back();
     TakenAction(action);
   }
@@ -1091,41 +1478,19 @@ namespace rrr {
   }
   
   void AndNetwork::Print() const {
-    std::cout << "pi: ";
-    std::string delim = "";
-    ForEachPi([&](int id) {
-      std::cout << delim << id;
-      delim = ", ";
-    });
-    std::cout << std::endl;
+    std::cout << "inputs: " << vPis << std::endl;
     ForEachInt([&](int id) {
       std::cout << "node " << id << ": ";
-      delim = "";
-      ForEachFanin(id, [&](int fi, bool c) {
-        std::cout << delim;
-        if(c) {
-          std::cout << "!";
-        }
-        std::cout << fi;
-        delim = ", ";
-      });
+      PrintComplementedEdges(std::bind(&AndNetwork::ForEachFanin<std::function<void(int, bool)>>, this, id, std::placeholders::_1));
       std::cout << " (ref = " << vRefs[id] << ")";
       std::cout << std::endl;
     });
-    std::cout << "po: ";
-    delim = "";
-    ForEachPoDriver([&](int fi, bool c) {
-      std::cout << delim;
-      if(c) {
-        std::cout << "!";
-      }
-      std::cout << fi;
-      delim = ", ";
-    });
+    std::cout << "outputs: ";
+    PrintComplementedEdges(std::bind(&AndNetwork::ForEachPoDriver<std::function<void(int, bool)>>, this, std::placeholders::_1));
     std::cout << std::endl;
   }
 
-  /* }}} Misc end */
+  /* }}} */
 
 }
 
diff --git a/src/opt/rrr/rrrBddAnalyzer.h b/src/opt/rrr/rrrBddAnalyzer.h
index 842e7714e..a9112a9ba 100644
--- a/src/opt/rrr/rrrBddAnalyzer.h
+++ b/src/opt/rrr/rrrBddAnalyzer.h
@@ -1,12 +1,8 @@
 #pragma once
 
-#include <iostream>
-#include <vector>
-
-#include <aig/gia/giaNewBdd.h>
-
 #include "rrrParameter.h"
-#include "rrrTypes.h"
+#include "rrrUtils.h"
+#include "rrrBddManager.h"
 
 ABC_NAMESPACE_CXX_HEADER_START
 
@@ -73,7 +69,7 @@ namespace rrr {
   public:
     // constructors
     BddAnalyzer();
-    BddAnalyzer(Ntk *pNtk, Parameter const *pPar);
+    BddAnalyzer(Parameter const *pPar);
     ~BddAnalyzer();
     void UpdateNetwork(Ntk *pNtk_, bool fSame);
 
@@ -320,7 +316,7 @@ namespace rrr {
         SimulateNode(id, vFs);
         DecRef(x);
         if(!pBdd->LitIsEq(x, vFs[id])) {
-          pNtk->ForEachFanout(id, false, [&](int fo, bool c) {
+          pNtk->ForEachFanout(id, false, [&](int fo) {
             vUpdates[fo] = true;
             vCUpdates[fo] = true;
           });
@@ -345,7 +341,7 @@ namespace rrr {
     }
     lit x = pBdd->Const1();
     IncRef(x);
-    pNtk->ForEachFanoutRidx(id, true, [&](int fo, bool c, int idx) {
+    pNtk->ForEachFanoutRidx(id, true, [&](int fo, int idx) {
       Assign(x, pBdd->And(x, vvCs[fo][idx]));
     });
     if(pBdd->LitIsEq(vGs[id], x)) {
@@ -374,7 +370,7 @@ namespace rrr {
     for(int idx = 0; idx < nFanins; idx++) {
       lit x = pBdd->Const1();
       IncRef(x);
-      for(unsigned idx2 = idx + 1; idx2 < nFanins; idx2++) {
+      for(int idx2 = idx + 1; idx2 < nFanins; idx2++) {
         int fi = pNtk->GetFanin(id, idx2);
         bool c = pNtk->GetCompl(id, idx2);
         Assign(x, pBdd->And(x, pBdd->LitNotCond(vFs[fi], c)));
@@ -439,7 +435,7 @@ namespace rrr {
 
   template <typename Ntk>
   void BddAnalyzer<Ntk>::Save(int slot) {
-    if(slot >= vBackups.size()) {
+    if(slot >= int_size(vBackups)) {
       vBackups.resize(slot + 1);
     }
     vBackups[slot].target = target;
@@ -453,7 +449,7 @@ namespace rrr {
 
   template <typename Ntk>
   void BddAnalyzer<Ntk>::Load(int slot) {
-    assert(slot < vBackups.size());
+    assert(slot < int_size(vBackups));
     target = vBackups[slot].target;
     CopyVec(vFs, vBackups[slot].vFs);
     CopyVec(vGs, vBackups[slot].vGs);
@@ -486,41 +482,12 @@ namespace rrr {
   }
   
   template <typename Ntk>
-  BddAnalyzer<Ntk>::BddAnalyzer(Ntk *pNtk, Parameter const *pPar) :
-    pNtk(pNtk),
+  BddAnalyzer<Ntk>::BddAnalyzer(Parameter const *pPar) :
+    pNtk(NULL),
     nVerbose(pPar->nAnalyzerVerbose),
+    pBdd(NULL),
     target(-1),
     fResim(false) {
-    NewBdd::Param Par;
-    Par.nObjsMaxLog = 25;
-    Par.nCacheMaxLog = 20;
-    Par.fCountOnes = true;
-    Par.nGbc = 1;
-    Par.nReo = 4000;
-    pBdd = new NewBdd::Man(pNtk->GetNumPis(), Par);
-    Allocate();
-    Assign(vFs[0], pBdd->Const0());
-    int idx = 0;
-    pNtk->ForEachPi([&](int id) {
-      Assign(vFs[id], pBdd->IthVar(idx));
-      idx++;
-    });
-    pNtk->ForEachInt([&](int id) {
-      vUpdates[id] = true;
-    });
-    Simulate();
-    pBdd->Reorder();
-    pBdd->TurnOffReo();
-    pNtk->ForEachInt([&](int id) {
-      vvCs[id].resize(pNtk->GetNumFanins(id), LitMax);
-    });
-    pNtk->ForEachPo([&](int id) {
-      vvCs[id].resize(1, LitMax);
-      Assign(vvCs[id][0], pBdd->Const0());
-      int fi = pNtk->GetFanin(id, 0);
-      vGUpdates[fi]  = true;
-    });
-    pNtk->AddCallback(std::bind(&BddAnalyzer<Ntk>::ActionCallback, this, std::placeholders::_1));
   }
 
   template <typename Ntk>
@@ -540,7 +507,7 @@ namespace rrr {
     vCUpdates.clear();
     // alloc
     bool fUseReo = false;
-    if(pBdd->GetNumVars() != pNtk->GetNumPis()) {
+    if(!pBdd || pBdd->GetNumVars() != pNtk->GetNumPis()) {
       // need to reset manager
       delete pBdd;
       NewBdd::Param Par;
diff --git a/src/opt/rrr/rrrBddManager.h b/src/opt/rrr/rrrBddManager.h
new file mode 100644
index 000000000..1227147c0
--- /dev/null
+++ b/src/opt/rrr/rrrBddManager.h
@@ -0,0 +1,848 @@
+#pragma once
+
+#include <cstdlib>
+#include <limits>
+#include <vector>
+#include <iostream>
+#include <iomanip>
+#include <cmath>
+
+ABC_NAMESPACE_CXX_HEADER_START
+
+namespace rrr {
+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;            }
+
+  static inline void fatal_error(const char* message) {
+    std::cerr << message << std::endl;
+    std::abort();
+  }
+
+  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)
+        fatal_error("nCacheMax must not be smaller than nCacheSize");
+      nMax = (cac)1 << nCacheMaxLog;
+      if(!(nMax << 1))
+        fatal_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;
+    int    nObjsMaxLog;
+    int    nUniqueSizeLog;
+    double UniqueDensity;
+    int    nCacheSizeLog;
+    int    nCacheMaxLog;
+    int    nCacheVerbose;
+    bool   fCountOnes;
+    int    nGbc;
+    bvar   nReo;
+    double MaxGrowth;
+    bool   fReoVerbose;
+    int    nVerbose;
+    std::vector<var> *pVar2Level;
+    Param() {
+      nObjsAllocLog  = 20;
+      nObjsMaxLog    = 25;
+      nUniqueSizeLog = 10;
+      UniqueDensity  = 4;
+      nCacheSizeLog  = 15;
+      nCacheMaxLog   = 20;
+      nCacheVerbose  = 0;
+      fCountOnes     = false;
+      nGbc           = 0;
+      nReo           = BvarMax();
+      MaxGrowth      = 1.2;
+      fReoVerbose    = false;
+      nVerbose       = 0;
+      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())
+        fatal_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()))
+            fatal_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)
+        fatal_error("nObjsMax must not be smaller than nObjsAlloc");
+      if(nVars_ >= (int)VarMax())
+        fatal_error("Memout (nVars) in init");
+      nVars = nVars_;
+      lit nObjsMaxLit = (lit)1 << p.nObjsMaxLog;
+      if(!nObjsMaxLit)
+        fatal_error("Memout (nObjsMax) in init");
+      if(nObjsMaxLit > (lit)BvarMax())
+        nObjsMax = BvarMax();
+      else
+        nObjsMax = (bvar)nObjsMaxLit;
+      lit nObjsAllocLit = (lit)1 << p.nObjsAllocLog;
+      if(!nObjsAllocLit)
+        fatal_error("Memout (nObjsAlloc) in init");
+      if(nObjsAllocLit > (lit)BvarMax())
+        nObjsAlloc = BvarMax();
+      else
+        nObjsAlloc = (bvar)nObjsAllocLit;
+      if(nObjsAlloc <= (bvar)nVars)
+        fatal_error("nObjsAlloc must be larger than nVars");
+      uniq nUniqueSize = (uniq)1 << p.nUniqueSizeLog;
+      if(!nUniqueSize)
+        fatal_error("Memout (nUniqueSize) in init");
+      // allocation
+      if(nVerbose)
+        std::cout << "Allocating " << nObjsAlloc << " nodes and " << nVars << " x " << nUniqueSize << " unique table entries" << std::endl;
+      vVars.resize(nObjsAlloc);
+      vObjs.resize((lit)nObjsAlloc * 2);
+      vNexts.resize(nObjsAlloc);
+      vMarks.resize(nObjsAlloc);
+      vvUnique.resize(nVars);
+      vUniqueMasks.resize(nVars);
+      vUniqueCounts.resize(nVars);
+      vUniqueTholds.resize(nVars);
+      for(var v = 0; v < nVars; v++) {
+        vvUnique[v].resize(nUniqueSize);
+        vUniqueMasks[v] = nUniqueSize - 1;
+        if((lit)(nUniqueSize * p.UniqueDensity) > (lit)BvarMax())
+          vUniqueTholds[v] = BvarMax();
+        else
+          vUniqueTholds[v] = (bvar)(nUniqueSize * p.UniqueDensity);
+      }
+      if(p.fCountOnes) {
+        if(nVars > 1023)
+          fatal_error("nVars must be less than 1024 to count ones");
+        vOneCounts.resize(nObjsAlloc);
+      }
+      // set up cache
+      cache = new Cache(p.nCacheSizeLog, p.nCacheMaxLog, p.nCacheVerbose);
+      // create nodes for variables
+      nObjs = 1;
+      vVars[0] = VarMax();
+      for(var v = 0; v < nVars; v++)
+        UniqueCreateInt(v, 1, 0);
+      // set up variable order
+      Var2Level.resize(nVars);
+      Level2Var.resize(nVars);
+      for(var v = 0; v < nVars; v++) {
+        if(p.pVar2Level)
+          Var2Level[v] = (*p.pVar2Level)[v];
+        else
+          Var2Level[v] = v;
+        Level2Var[Var2Level[v]] = v;
+      }
+      // set other parameters
+      RemovedHead = 0;
+      nGbc = p.nGbc;
+      nReo = p.nReo;
+      MaxGrowth = p.MaxGrowth;
+      fReoVerbose = p.fReoVerbose;
+      if(nGbc || nReo != BvarMax())
+        vRefs.resize(nObjsAlloc);
+    }
+    ~Man() {
+      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 RemoveRefIfUnused() {
+      if(!nGbc && nReo == BvarMax())
+        vRefs.clear();
+    }
+    void TurnOnReo(int nReo_ = 0, std::vector<lit> const *vLits = NULL) {
+      if(nReo_)
+        nReo = nReo_;
+      else
+        nReo = nObjs << 1;
+      if((lit)nReo > (lit)BvarMax())
+        nReo = BvarMax();
+      if(vRefs.empty()) {
+        if(vLits)
+          SetRef(*vLits);
+        else
+          vRefs.resize(nObjsAlloc);
+      }
+    }
+    void TurnOffReo() {
+      nReo = BvarMax();
+    }
+    var GetNumVars() const {
+      return nVars;
+    }
+    void GetOrdering(std::vector<int> &Var2Level_) {
+      Var2Level_.resize(nVars);
+      for(var v = 0; v < nVars; v++)
+        Var2Level_[v] = Var2Level[v];
+    }
+    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;
+    }
+  };
+
+}
+}
+
+ABC_NAMESPACE_CXX_HEADER_END
diff --git a/src/opt/rrr/rrrBddMspfAnalyzer.h b/src/opt/rrr/rrrBddMspfAnalyzer.h
index 6c3b057ed..1634a5fd6 100644
--- a/src/opt/rrr/rrrBddMspfAnalyzer.h
+++ b/src/opt/rrr/rrrBddMspfAnalyzer.h
@@ -1,12 +1,8 @@
 #pragma once
 
-#include <iostream>
-#include <vector>
-
-#include <aig/gia/giaNewBdd.h>
-
 #include "rrrParameter.h"
-#include "rrrTypes.h"
+#include "rrrUtils.h"
+#include "rrrBddManager.h"
 
 ABC_NAMESPACE_CXX_HEADER_START
 
@@ -75,7 +71,7 @@ namespace rrr {
   public:
     // constructors
     BddMspfAnalyzer();
-    BddMspfAnalyzer(Ntk *pNtk, Parameter const *pPar);
+    BddMspfAnalyzer(Parameter const *pPar);
     ~BddMspfAnalyzer();
     void UpdateNetwork(Ntk *pNtk_, bool fSame);
 
@@ -256,6 +252,9 @@ namespace rrr {
           Assign(vGs[action.fi], pBdd->Or(pBdd->LitNot(x), vGs[action.id]));
           DecRef(x);
         }
+      } else {
+        // otherwise mark the node for future update
+        vCUpdates[action.id] = true;
       }
       vvCs[action.id].resize(action.idx + 1, LitMax);
       Assign(vvCs[action.id][action.idx], vGs[action.fi]);
@@ -333,7 +332,7 @@ namespace rrr {
     pNtk->ForEachInt([&](int id) {
       if(vUpdates[id]) {
         if(SimulateNode(id, vFs)) {
-          pNtk->ForEachFanout(id, false, [&](int fo, bool c) {
+          pNtk->ForEachFanout(id, false, [&](int fo) {
             vUpdates[fo] = true;
             vCUpdates[fo] = true;
           });
@@ -357,7 +356,7 @@ namespace rrr {
     });
     lit x = pBdd->Const1();
     IncRef(x);
-    pNtk->ForEachPoDriver([&](int fi, bool c) {
+    pNtk->ForEachPoDriver([&](int fi) {
       lit y = Xor(vFs[fi], v[fi]);
       IncRef(y);
       Assign(x, pBdd->And(x, pBdd->LitNot(y)));
@@ -385,7 +384,7 @@ namespace rrr {
     }
     lit x = pBdd->Const1();
     IncRef(x);
-    pNtk->ForEachFanoutRidx(id, true, [&](int fo, bool c, int idx) {
+    pNtk->ForEachFanoutRidx(id, true, [&](int fo, int idx) {
       Assign(x, pBdd->And(x, vvCs[fo][idx]));
     });
     if(pBdd->LitIsEq(vGs[id], x)) {
@@ -533,7 +532,7 @@ namespace rrr {
 
   template <typename Ntk>
   void BddMspfAnalyzer<Ntk>::Save(int slot) {
-    if(slot >= vBackups.size()) {
+    if(slot >= int_size(vBackups)) {
       vBackups.resize(slot + 1);
     }
     CopyVec(vBackups[slot].vFs, vFs);
@@ -548,7 +547,7 @@ namespace rrr {
 
   template <typename Ntk>
   void BddMspfAnalyzer<Ntk>::Load(int slot) {
-    assert(slot < vBackups.size());
+    assert(slot < int_size(vBackups));
     CopyVec(vFs, vBackups[slot].vFs);
     CopyVec(vGs, vBackups[slot].vGs);
     CopyVecVec(vvCs, vBackups[slot].vvCs);
@@ -580,40 +579,11 @@ namespace rrr {
   }
   
   template <typename Ntk>
-  BddMspfAnalyzer<Ntk>::BddMspfAnalyzer(Ntk *pNtk, Parameter const *pPar) :
-    pNtk(pNtk),
+  BddMspfAnalyzer<Ntk>::BddMspfAnalyzer(Parameter const *pPar) :
+    pNtk(NULL),
     nVerbose(pPar->nAnalyzerVerbose),
+    pBdd(NULL),
     fUpdate(false) {
-    NewBdd::Param Par;
-    Par.nObjsMaxLog = 25;
-    Par.nCacheMaxLog = 20;
-    Par.fCountOnes = true;
-    Par.nGbc = 1;
-    Par.nReo = 4000;
-    pBdd = new NewBdd::Man(pNtk->GetNumPis(), Par);
-    Allocate();
-    Assign(vFs[0], pBdd->Const0());
-    int idx = 0;
-    pNtk->ForEachPi([&](int id) {
-      Assign(vFs[id], pBdd->IthVar(idx));
-      idx++;
-    });
-    pNtk->ForEachInt([&](int id) {
-      vUpdates[id] = true;
-    });
-    Simulate();
-    pBdd->Reorder();
-    pBdd->TurnOffReo();
-    pNtk->ForEachInt([&](int id) {
-      vvCs[id].resize(pNtk->GetNumFanins(id), LitMax);
-    });
-    pNtk->ForEachPo([&](int id) {
-      vvCs[id].resize(1, LitMax);
-      Assign(vvCs[id][0], pBdd->Const0());
-      int fi = pNtk->GetFanin(id, 0);
-      vGUpdates[fi]  = true;
-    });
-    pNtk->AddCallback(std::bind(&BddMspfAnalyzer<Ntk>::ActionCallback, this, std::placeholders::_1));
   }
 
   template <typename Ntk>
@@ -633,7 +603,7 @@ namespace rrr {
     vVisits.clear();
     // alloc
     bool fUseReo = false;
-    if(pBdd->GetNumVars() != pNtk->GetNumPis()) {
+    if(!pBdd || pBdd->GetNumVars() != pNtk->GetNumPis()) {
       // need to reset manager
       delete pBdd;
       NewBdd::Param Par;
diff --git a/src/opt/rrr/rrrOptimizer.h b/src/opt/rrr/rrrOptimizer.h
index c114bfe3b..8d30368f1 100644
--- a/src/opt/rrr/rrrOptimizer.h
+++ b/src/opt/rrr/rrrOptimizer.h
@@ -1,14 +1,12 @@
 #pragma once
 
-#include <vector>
 #include <map>
 #include <iterator>
 #include <random>
 #include <numeric>
-#include <limits>
 
 #include "rrrParameter.h"
-#include "rrrTypes.h"
+#include "rrrUtils.h"
 
 ABC_NAMESPACE_CXX_HEADER_START
 
@@ -31,10 +29,12 @@ namespace rrr {
     std::function<double(Ntk *)> CostFunction;
     int nSortType;
     int nFlow;
+    int nDistance;
+    bool fCompatible;
     seconds nTimeout; // assigned upon Run
 
     // data
-    Ana *pAna;
+    Ana ana;
     std::mt19937 rng;
     std::vector<int> vTmp;
     std::map<int, std::set<int>> mapNewFanins;
@@ -46,7 +46,7 @@ namespace rrr {
 
     // marks
     int target;
-    std::vector<bool> vMarks;
+    std::vector<bool> vTfoMarks;
     
     // callback
     void ActionCallback(Action const &action);
@@ -61,13 +61,14 @@ namespace rrr {
     void SetRandPiOrder();
     void SetRandCosts();
     void SortFanins(int id);
+    void SortFanins();
 
-    // reduce fanin
-    bool ReduceFanin(int id, bool fRemoveUnused = false);
-    bool ReduceFaninOneRandom(int id, bool fRemoveUnused = false);
+    // reduce fanins
+    bool ReduceFanins(int id, bool fRemoveUnused = false);
+    bool ReduceFaninsOneRandom(int id, bool fRemoveUnused = false);
 
     // reduce
-    void Reduce();
+    bool Reduce();
     void ReduceRandom();
 
     // remove redundancy
@@ -88,13 +89,13 @@ namespace rrr {
     
   public:
     // constructors
-    Optimizer(Ntk *pNtk, Parameter const *pPar, std::function<double(Ntk *)> CostFunction);
-    ~Optimizer();
-    void UpdateNetwork(Ntk *pNtk_, bool fSame);
+    Optimizer(Parameter const *pPar, std::function<double(Ntk *)> CostFunction);
+    void UpdateNetwork(Ntk *pNtk_, bool fSame = false);
 
     // run
     void Run(seconds nTimeout_ = 0);
-    void Randomize();
+    void ResetSeed(int iSeed);
+    void Randomize(int iSeed);
     
   };
 
@@ -154,11 +155,11 @@ namespace rrr {
       return;
     }
     target = id;
-    vMarks.clear();
-    vMarks.resize(pNtk->GetNumNodes());
-    vMarks[id] = true;
+    vTfoMarks.clear();
+    vTfoMarks.resize(pNtk->GetNumNodes());
+    vTfoMarks[id] = true;
     pNtk->ForEachTfo(id, false, [&](int fo) {
-      vMarks[fo] = true;
+      vTfoMarks[fo] = true;
     });
   }
 
@@ -183,8 +184,7 @@ namespace rrr {
 
   template <typename Ntk, typename Ana>
   inline void Optimizer<Ntk, Ana>::SetRandPiOrder() {
-    assert(vRandPiOrder.size() <= (std::vector<int>::size_type)std::numeric_limits<int>::max());
-    if((int)vRandPiOrder.size() != pNtk->GetNumPis()) {
+    if(int_size(vRandPiOrder) != pNtk->GetNumPis()) {
       vRandPiOrder.clear();
       vRandPiOrder.resize(pNtk->GetNumPis());
       std::iota(vRandPiOrder.begin(), vRandPiOrder.end(), 0);
@@ -195,8 +195,7 @@ namespace rrr {
   template <typename Ntk, typename Ana>
   inline void Optimizer<Ntk, Ana>::SetRandCosts() {
     std::uniform_real_distribution<> dis(std::numeric_limits<double>::lowest(), std::numeric_limits<double>::max());
-    assert(vRandCosts.size() <= (std::vector<int>::size_type)std::numeric_limits<int>::max());
-    while((int)vRandCosts.size() < pNtk->GetNumNodes()) {
+    while(int_size(vRandCosts) < pNtk->GetNumNodes()) {
       vRandCosts.push_back(dis(rng));
     }
   }
@@ -207,12 +206,12 @@ namespace rrr {
     case 0: // no sorting
       break;
     case 1: // prioritize internals
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         return !pNtk->IsPi(i) && pNtk->IsPi(j);
       });
       break;
     case 2: // prioritize internals with (reversely) sorted PIs
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         if(pNtk->IsPi(i) && pNtk->IsPi(j)) {
           return pNtk->GetPiIndex(i) > pNtk->GetPiIndex(j);
         }
@@ -221,7 +220,7 @@ namespace rrr {
       break;
     case 3: // prioritize internals with random PI order
       SetRandPiOrder();
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         if(pNtk->IsPi(i) && pNtk->IsPi(j)) {
           return vRandPiOrder[pNtk->GetPiIndex(i)] > vRandPiOrder[pNtk->GetPiIndex(j)];
         }
@@ -229,12 +228,12 @@ namespace rrr {
       });
       break;
     case 4: // smaller fanout takes larger cost
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         return pNtk->GetNumFanouts(i) < pNtk->GetNumFanouts(j);
       });
       break;
     case 5: // fanout + PI
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         if(pNtk->IsPi(i) && !pNtk->IsPi(j)) {
           return false;
         }
@@ -245,7 +244,7 @@ namespace rrr {
       });
       break;
     case 6: // fanout + sorted PI
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         if(pNtk->IsPi(i) && pNtk->IsPi(j)) {
           return pNtk->GetPiIndex(i) > pNtk->GetPiIndex(j);
         }
@@ -260,7 +259,7 @@ namespace rrr {
       break;
     case 7: // fanout + random PI
       SetRandPiOrder();
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         if(pNtk->IsPi(i) && pNtk->IsPi(j)) {
           return vRandPiOrder[pNtk->GetPiIndex(i)] > vRandPiOrder[pNtk->GetPiIndex(j)];
         }
@@ -274,7 +273,7 @@ namespace rrr {
       });
       break;
     case 8: // reverse topological order + PI
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         if(pNtk->IsPi(i) && pNtk->IsPi(j)) {
           return false;
         }
@@ -288,7 +287,7 @@ namespace rrr {
       });
       break;
     case 9: // reverse topological order + sorted PI
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         if(pNtk->IsPi(i) && pNtk->IsPi(j)) {
           return pNtk->GetPiIndex(i) > pNtk->GetPiIndex(j);
         }
@@ -303,7 +302,7 @@ namespace rrr {
       break;
     case 10: // reverse topological order + random PI
       SetRandPiOrder();
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         if(pNtk->IsPi(i) && pNtk->IsPi(j)) {
           return vRandPiOrder[pNtk->GetPiIndex(i)] > vRandPiOrder[pNtk->GetPiIndex(j)];
         }
@@ -317,7 +316,7 @@ namespace rrr {
       });
       break;
     case 11: // topo + fanout + PI
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         if(pNtk->IsPi(i) && !pNtk->IsPi(j)) {
           return false;
         }
@@ -337,7 +336,7 @@ namespace rrr {
       });
       break;
     case 12: // topo + fanout + sorted PI
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         if(pNtk->IsPi(i) && pNtk->IsPi(j)) {
           return pNtk->GetPiIndex(i) > pNtk->GetPiIndex(j);
         }
@@ -358,7 +357,7 @@ namespace rrr {
       break;
     case 13: // topo + fanout + random PI
       SetRandPiOrder();
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         if(pNtk->IsPi(i) && pNtk->IsPi(j)) {
           return vRandPiOrder[pNtk->GetPiIndex(i)] > vRandPiOrder[pNtk->GetPiIndex(j)];
         }
@@ -379,13 +378,13 @@ namespace rrr {
       break;
     case 14: // random order
       SetRandCosts();
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         return vRandCosts[i] > vRandCosts[j];
       });
       break;
     case 15: // random + PI
       SetRandCosts();
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         if(pNtk->IsPi(i) && !pNtk->IsPi(j)) {
           return false;
         }
@@ -397,7 +396,7 @@ namespace rrr {
       break;
     case 16: // random + fanout
       SetRandCosts();
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         if(pNtk->GetNumFanouts(i) > pNtk->GetNumFanouts(j)) {
           return false;
         }
@@ -409,7 +408,7 @@ namespace rrr {
       break;
     case 17: // random + fanout + PI
       SetRandCosts();
-      pNtk->SortFanins(id, [&](int i, bool ci, int j, bool cj) {
+      pNtk->SortFanins(id, [&](int i, int j) {
         if(pNtk->IsPi(i) && !pNtk->IsPi(j)) {
           return false;
         }
@@ -430,14 +429,20 @@ namespace rrr {
     }
   }
   
+  template <typename Ntk, typename Ana>
+  inline void Optimizer<Ntk, Ana>::SortFanins() {
+    pNtk->ForEachInt([&](int id) {
+      SortFanins(id);
+    });
+  }
+  
   /* }}} */
   
-  /* {{{ Reduce fanin */
+  /* {{{ Reduce fanins */
   
   template <typename Ntk, typename Ana>
-  inline bool Optimizer<Ntk, Ana>::ReduceFanin(int id, bool fRemoveUnused) {
+  inline bool Optimizer<Ntk, Ana>::ReduceFanins(int id, bool fRemoveUnused) {
     assert(pNtk->GetNumFanouts(id) > 0);
-    SortFanins(id);
     bool fRemoved = false;
     for(int idx = 0; idx < pNtk->GetNumFanins(id); idx++) {
       // skip fanins that were just added
@@ -448,7 +453,7 @@ namespace rrr {
         }
       }
       // reduce
-      if(pAna->CheckRedundancy(id, idx)) {
+      if(ana.CheckRedundancy(id, idx)) {
         int fi = pNtk->GetFanin(id, idx);
         pNtk->RemoveFanin(id, idx);
         fRemoved = true;
@@ -461,8 +466,9 @@ namespace rrr {
     return fRemoved;
   }
 
+  /*
   template <typename Ntk, typename Ana>
-  inline bool Optimizer<Ntk, Ana>::ReduceFaninOneRandom(int id, bool fRemoveUnused) {
+  inline bool Optimizer<Ntk, Ana>::ReduceFaninsOneRandom(int id, bool fRemoveUnused) {
     assert(pNtk->GetNumFanouts(id) > 0);
     // generate random order
     vTmp.resize(pNtk->GetNumFanins(id));
@@ -477,7 +483,7 @@ namespace rrr {
         }
       }
       // reduce
-      if(pAna->CheckRedundancy(id, idx)) {
+      if(ana.CheckRedundancy(id, idx)) {
         int fi = pNtk->GetFanin(id, idx);
         pNtk->RemoveFanin(id, idx);
         if(fRemoveUnused && pNtk->GetNumFanouts(fi) == 0) {
@@ -488,6 +494,7 @@ namespace rrr {
     }
     return false;
   }
+  */
   
   // TODO: add a method to minimize the size of fanins (check singles, pairs, trios, and so on)?
   
@@ -496,7 +503,8 @@ namespace rrr {
   /* {{{ Reduce */
 
   template <typename Ntk, typename Ana>
-  void Optimizer<Ntk, Ana>::Reduce() {
+  bool Optimizer<Ntk, Ana>::Reduce() {
+    bool fReduced = false;
     std::vector<int> vInts = pNtk->GetInts();
     for(critr it = vInts.rbegin(); it != vInts.rend(); it++) {
       if(!pNtk->IsInt(*it)) {
@@ -506,21 +514,15 @@ namespace rrr {
         pNtk->RemoveUnused(*it);
         continue;
       }
-      ReduceFanin(*it);
+      fReduced |= ReduceFanins(*it);
       if(pNtk->GetNumFanins(*it) <= 1) {
         pNtk->Propagate(*it);
       }
-      /*
-      if(pNtk->GetNumFanins(*it) == 1) {
-        pNtk->RemoveBuffer(*it);
-      }
-      if(pNtk->GetNumFanins(*it) == 0) {
-        pNtk->RemoveConst(*it);
-      }
-      */
     }
+    return fReduced;
   }
 
+  /*
   template <typename Ntk, typename Ana>
   void Optimizer<Ntk, Ana>::ReduceRandom() {
     pNtk->Sweep(false);
@@ -534,12 +536,13 @@ namespace rrr {
         pNtk->RemoveUnused(*it);
         continue;
       }
-      ReduceFanin(*it, true);
+      ReduceFanins(*it, true);
       if(pNtk->GetNumFanins(*it) <= 1) {
         pNtk->Propagate(*it);
       }
     }
   }
+  */
 
   /* }}} */
 
@@ -547,6 +550,12 @@ namespace rrr {
   
   template <typename Ntk, typename Ana>
   void Optimizer<Ntk, Ana>::RemoveRedundancy() {
+    if(fCompatible) {
+      while(Reduce()) {
+        SortFanins();
+      }
+      return;
+    }
     std::vector<int> vInts = pNtk->GetInts();
     for(critr it = vInts.rbegin(); it != vInts.rend();) {
       if(!pNtk->IsInt(*it)) {
@@ -558,7 +567,8 @@ namespace rrr {
         it++;
         continue;
       }
-      bool fReduced = ReduceFanin(*it);
+      SortFanins(*it);
+      bool fReduced = ReduceFanins(*it);
       if(pNtk->GetNumFanins(*it) <= 1) {
         pNtk->Propagate(*it);
       }
@@ -570,6 +580,7 @@ namespace rrr {
     }
   }
 
+  /*
   template <typename Ntk, typename Ana>
   void Optimizer<Ntk, Ana>::RemoveRedundancyRandom() {
     pNtk->Sweep(false);
@@ -585,7 +596,7 @@ namespace rrr {
         it++;
         continue;
       }
-      bool fReduced = ReduceFaninOneRandom(*it, true);
+      bool fReduced = ReduceFaninsOneRandom(*it, true);
       if(pNtk->GetNumFanins(*it) <= 1) {
         pNtk->Propagate(*it);
       }
@@ -597,6 +608,7 @@ namespace rrr {
       }
     }
   }
+  */
 
   /* }}} */
 
@@ -606,20 +618,20 @@ namespace rrr {
   template <typename T>
   T Optimizer<Ntk, Ana>::SingleAdd(int id, T begin, T end) {
     MarkTfo(id);
-    pNtk->ForEachFanin(id, [&](int fi, bool c) {
-      vMarks[fi] = true;
+    pNtk->ForEachFanin(id, [&](int fi) {
+      vTfoMarks[fi] = true;
     });
     T it = begin;
     for(; it != end; it++) {
       if(!pNtk->IsInt(*it) && !pNtk->IsPi(*it)) {
         continue;
       }
-      if(vMarks[*it]) {
+      if(vTfoMarks[*it]) {
         continue;
       }
-      if(pAna->CheckFeasibility(id, *it, false)) {
+      if(ana.CheckFeasibility(id, *it, false)) {
         pNtk->AddFanin(id, *it, false);
-      } else if(pNtk->UseComplementedEdges() && pAna->CheckFeasibility(id, *it, true)) {
+      } else if(pNtk->UseComplementedEdges() && ana.CheckFeasibility(id, *it, true)) {
         pNtk->AddFanin(id, *it, true);
       } else {
         continue;
@@ -627,8 +639,8 @@ namespace rrr {
       mapNewFanins[id].insert(*it);
       break;
     }
-    pNtk->ForEachFanin(id, [&](int fi, bool c) {
-      vMarks[fi] = false;
+    pNtk->ForEachFanin(id, [&](int fi) {
+      vTfoMarks[fi] = false;
     });
     return it;
   }
@@ -636,20 +648,20 @@ namespace rrr {
   template <typename Ntk, typename Ana>
   int Optimizer<Ntk, Ana>::MultiAdd(int id, std::vector<int> const &vCands, int nMax) {
     MarkTfo(id);
-    pNtk->ForEachFanin(id, [&](int fi, bool c) {
-      vMarks[fi] = true;
+    pNtk->ForEachFanin(id, [&](int fi) {
+      vTfoMarks[fi] = true;
     });
     int nAdded = 0;
     for(int cand: vCands) {
       if(!pNtk->IsInt(cand) && !pNtk->IsPi(cand)) {
         continue;
       }
-      if(vMarks[cand]) {
+      if(vTfoMarks[cand]) {
         continue;
       }
-      if(pAna->CheckFeasibility(id, cand, false)) {
+      if(ana.CheckFeasibility(id, cand, false)) {
         pNtk->AddFanin(id, cand, false);
-      } else if(pNtk->UseComplementedEdges() && pAna->CheckFeasibility(id, cand, true)) {
+      } else if(pNtk->UseComplementedEdges() && ana.CheckFeasibility(id, cand, true)) {
         pNtk->AddFanin(id, cand, true);
       } else {
         continue;
@@ -660,8 +672,8 @@ namespace rrr {
         break;
       }
     }
-    pNtk->ForEachFanin(id, [&](int fi, bool c) {
-      vMarks[fi] = false;
+    pNtk->ForEachFanin(id, [&](int fi) {
+      vTfoMarks[fi] = false;
     });
     return nAdded;
   }
@@ -715,6 +727,10 @@ namespace rrr {
     }
     if(pNtk->IsInt(id)) {
       pNtk->TrivialDecompose(id);
+      SortFanins();
+      if(fCompatible) {
+        RemoveRedundancy();
+      }
     }
     if(fGreedy) {
       pNtk->PopBack();
@@ -781,21 +797,16 @@ namespace rrr {
   /* {{{ Constructors */
   
   template <typename Ntk, typename Ana>
-  Optimizer<Ntk, Ana>::Optimizer(Ntk *pNtk, Parameter const *pPar, std::function<double(Ntk *)> CostFunction) :
-    pNtk(pNtk),
+  Optimizer<Ntk, Ana>::Optimizer(Parameter const *pPar, std::function<double(Ntk *)> CostFunction) :
+    pNtk(NULL),
     nVerbose(pPar->nOptimizerVerbose),
     CostFunction(CostFunction),
     nSortType(pPar->nSortType),
     nFlow(pPar->nOptimizerFlow),
+    nDistance(pPar->nDistance),
+    fCompatible(pPar->fUseBddCspf),
+    ana(pPar),
     target(-1) {
-    pNtk->AddCallback(std::bind(&Optimizer<Ntk, Ana>::ActionCallback, this, std::placeholders::_1));
-    pAna = new Ana(pNtk, pPar);
-    rng.seed(pPar->iSeed);
-  }
-  
-  template <typename Ntk, typename Ana>
-  Optimizer<Ntk, Ana>::~Optimizer() {
-    delete pAna;
   }
   
   template <typename Ntk, typename Ana>
@@ -803,7 +814,7 @@ namespace rrr {
     pNtk = pNtk_;
     target = -1;
     pNtk->AddCallback(std::bind(&Optimizer<Ntk, Ana>::ActionCallback, this, std::placeholders::_1));
-    pAna->UpdateNetwork(pNtk, fSame);
+    ana.UpdateNetwork(pNtk, fSame);
   }
   
   /* }}} */
@@ -818,14 +829,24 @@ namespace rrr {
     case 0:
       RemoveRedundancy();
       ApplyReverseTopologically([&](int id) {
-        std::vector<int> vCands = pNtk->GetPisInts();
+        std::vector<int> vCands;
+        if(nDistance) {
+          vCands = pNtk->GetNeighbors(id, true, nDistance);
+        } else {
+          vCands = pNtk->GetPisInts();
+        }
         SingleResub(id, vCands);
       });
       break;
     case 1:
       RemoveRedundancy();
       ApplyReverseTopologically([&](int id) {
-        std::vector<int> vCands = pNtk->GetInts();
+        std::vector<int> vCands;
+        if(nDistance) {
+          vCands = pNtk->GetNeighbors(id, true, nDistance);
+        } else {
+          vCands = pNtk->GetPisInts();
+        }
         MultiResub(id, vCands);
       });
       break;
@@ -834,11 +855,22 @@ namespace rrr {
       double dCost = CostFunction(pNtk);
       while(true) {
         ApplyReverseTopologically([&](int id) {
-          std::vector<int> vCands = pNtk->GetPisInts();
+          std::vector<int> vCands;
+          if(nDistance) {
+            vCands = pNtk->GetNeighbors(id, true, nDistance);
+          } else {
+            vCands = pNtk->GetPisInts();
+          }
           SingleResub(id, vCands);
         });
         ApplyReverseTopologically([&](int id) {
-          std::vector<int> vCands = pNtk->GetInts();
+          std::vector<int> vCands;
+          if(nDistance) {
+            vCands = pNtk->GetNeighbors(id, true, nDistance);
+          } else {
+            vCands = pNtk->GetPisInts();
+            // vCands = pNtk->GetInts();
+          }
           MultiResub(id, vCands);
         });
         double dNewCost = CostFunction(pNtk);
@@ -856,12 +888,18 @@ namespace rrr {
   }
 
   template <typename Ntk, typename Ana>
-  void Optimizer<Ntk, Ana>::Randomize() {
-    nSortType = rng() % 18;
+  void Optimizer<Ntk, Ana>::ResetSeed(int iSeed) {
+    rng.seed(iSeed);
     vRandPiOrder.clear();
     vRandCosts.clear();
   }
   
+  template <typename Ntk, typename Ana>
+  void Optimizer<Ntk, Ana>::Randomize(int iSeed) {
+    ResetSeed(iSeed);
+    nSortType = rng() % 18;
+  }
+  
   /* }}} */
   
 }
diff --git a/src/opt/rrr/rrrParameter.h b/src/opt/rrr/rrrParameter.h
index 571ded31f..22429511b 100644
--- a/src/opt/rrr/rrrParameter.h
+++ b/src/opt/rrr/rrrParameter.h
@@ -9,6 +9,7 @@ namespace rrr {
     int nWords = 10;
     int nTimeout = 0;
     int nSchedulerVerbose = 1;
+    int nPartitionerVerbose = 0;
     int nOptimizerVerbose = 0;
     int nAnalyzerVerbose = 0;
     int nSimulatorVerbose = 0;
@@ -16,9 +17,14 @@ namespace rrr {
     bool fUseBddCspf = false;
     bool fUseBddMspf = false;
     int nConflictLimit = 0;
-    int nSortType = 0;
+    int nSortType = 12;
     int nOptimizerFlow = 0;
     int nSchedulerFlow = 0;
+    int nDistance = 0;
+    int nRestarts = 0;
+    int nThreads = 1;
+    int nWindowSize = 0;
+    bool fDeterministic = true;
   };
   
 }
diff --git a/src/opt/rrr/rrrPartitioner.h b/src/opt/rrr/rrrPartitioner.h
new file mode 100644
index 000000000..a2993e8e8
--- /dev/null
+++ b/src/opt/rrr/rrrPartitioner.h
@@ -0,0 +1,323 @@
+#pragma once
+
+#include <utility>
+#include <map>
+#include <tuple>
+#include <random>
+
+#include "rrrParameter.h"
+#include "rrrUtils.h"
+
+ABC_NAMESPACE_CXX_HEADER_START
+
+namespace rrr {
+
+  template <typename Ntk>
+  class Partitioner {
+  private:
+    // pointer to network
+    Ntk *pNtk;
+
+    // parameters
+    int nVerbose;
+    int nWindowSize;
+
+    // data
+    std::map<Ntk *, std::tuple<std::set<int>, std::vector<int>, std::vector<bool>, std::vector<int>>> mSubNtk2Io;
+    std::set<int> sBlocked;
+
+    // subroutines
+    Ntk *ExtractDisjoint(int id);
+    
+  public:
+    // constructors
+    Partitioner(Parameter const *pPar);
+    void UpdateNetwork(Ntk *pNtk);
+
+    // APIs
+    Ntk *Extract(int iSeed);
+    void Insert(Ntk *pSubNtk);
+  };
+
+  /* {{{ Subroutines */
+
+  template <typename Ntk>
+  Ntk *Partitioner<Ntk>::ExtractDisjoint(int id) {
+    // collect neighbor
+    assert(!sBlocked.count(id));
+    if(nVerbose) {
+      std::cout << "extracting with a center node " << id << std::endl;
+    }
+    int nRadius = 2;
+    std::vector<int> vNodes = pNtk->GetNeighbors(id, false, nRadius);
+    std::vector<int> vNodesNew = pNtk->GetNeighbors(id, false, nRadius + 1);
+    // gradually increase radius until it hits window size limit
+    while(int_size(vNodesNew) < nWindowSize) {
+      if(int_size(vNodes) == int_size(vNodesNew)) { // already maximum
+        break;
+      }
+      vNodes = vNodesNew;
+      nRadius++;
+      vNodesNew = pNtk->GetNeighbors(id, false, nRadius + 1);
+    }
+    std::set<int> sNodes(vNodes.begin(), vNodes.end());
+    sNodes.insert(id);
+    if(nVerbose) {
+      std::cout << "neighbors: " << sNodes << std::endl;
+    }
+    // remove nodes that are already blocked
+    for(std::set<int>::iterator it = sNodes.begin(); it != sNodes.end();) {
+      if(sBlocked.count(*it)) {
+        it = sNodes.erase(it);
+      } else {
+        it++;
+      }
+    }
+    if(nVerbose) {
+      std::cout << "disjoint neighbors: " << sNodes << std::endl;
+    }
+    // get tentative window IO
+    std::set<int> sInputs, sOutputs;
+    for(int id: sNodes) {
+      pNtk->ForEachFanin(id, [&](int fi) {
+        if(!sNodes.count(fi)) {
+          sInputs.insert(fi);
+        }
+      });
+      bool fOutput = false;
+      pNtk->ForEachFanout(id, true, [&](int fo) {
+        if(!sNodes.count(fo)) {
+          fOutput = true;
+        }
+      });
+      if(fOutput) {
+        sOutputs.insert(id);
+      }
+    }
+    if(nVerbose) {
+      std::cout << "\tinputs: " << sInputs << std::endl;
+      std::cout << "\toutputs: " << sOutputs << std::endl;
+    }
+    // prevent potential loops while ensuring disjointness
+    // first by including inner nodes
+    std::set<int> sFanouts;
+    for(int id: sOutputs) {
+      pNtk->ForEachFanout(id, false, [&](int fo) {
+        if(!sNodes.count(fo)) {
+          sFanouts.insert(fo);
+        }
+      });
+    }
+    std::vector<int> vInners = pNtk->GetInners(sFanouts, sInputs);
+    while(!vInners.empty()) {
+      if(nVerbose) {
+        std::cout << "inners: " << vInners << std::endl;
+      }
+      if(int_size(sNodes) + int_size(vInners) > 2 * nWindowSize) {
+        // TODO: parametrize
+        break;
+      }
+      bool fOverlap = false;
+      for(int i: vInners) {
+        if(sBlocked.count(i)) {
+          fOverlap = true;
+          break;
+        }
+      }
+      if(fOverlap) {
+        break;
+      }
+      sNodes.insert(vInners.begin(), vInners.end());
+      if(nVerbose) {
+        std::cout << "new neighbors: " << sNodes << std::endl;
+      }
+      sInputs.clear();
+      sOutputs.clear();
+      for(int id: sNodes) {
+        pNtk->ForEachFanin(id, [&](int fi) {
+          if(!sNodes.count(fi)) {
+            sInputs.insert(fi);
+          }
+        });
+        bool fOutput = false;
+        pNtk->ForEachFanout(id, true, [&](int fo) {
+          if(!sNodes.count(fo)) {
+            fOutput = true;
+          }
+        });
+        if(fOutput) {
+          sOutputs.insert(id);
+        }
+      }
+      if(nVerbose) {
+        std::cout << "\tnew inputs: " << sInputs << std::endl;
+        std::cout << "\tnew outputs: " << sOutputs << std::endl;
+      }
+      sFanouts.clear();
+      for(int id: sOutputs) {
+        pNtk->ForEachFanout(id, false, [&](int fo) {
+          if(!sNodes.count(fo)) {
+            sFanouts.insert(fo);
+          }
+        });
+      }
+      vInners = pNtk->GetInners(sFanouts, sInputs);
+    }
+    if(!vInners.empty()) {
+      // fall back method by removing TFI of outputs reachable to inputs
+      for(int id: sOutputs) {
+        if(!sNodes.count(id)) { // already removed
+          continue;
+        }
+        sFanouts.clear();
+        pNtk->ForEachFanout(id, false, [&](int fo) {
+          if(!sNodes.count(fo)) {
+            sFanouts.insert(fo);
+          }
+        });
+        if(pNtk->IsReachable(sFanouts, sInputs)) {
+          if(nVerbose) {
+            std::cout << id << " is reachable to inputs" << std::endl;
+          }
+          sNodes.erase(id);
+          pNtk->ForEachTfiEnd(id, sInputs, [&](int fi) {
+            int r = sNodes.erase(fi);
+            assert(r);
+          });
+          if(nVerbose) {
+            std::cout << "new neighbors: " << sNodes << std::endl;
+          }
+          if(sNodes.empty()) {
+            if(nVerbose) {
+              std::cout << "IS EMPTY" << std::endl;
+            }
+            return NULL;
+          }
+          // recompute inputs
+          sInputs.clear();
+          for(int id: sNodes) {
+            pNtk->ForEachFanin(id, [&](int fi) {
+              if(!sNodes.count(fi)) {
+                sInputs.insert(fi);
+              }
+            });
+          }
+          if(nVerbose) {
+            std::cout << "\tnew inputs: " << sInputs << std::endl;
+          }
+        }
+      }
+      // recompute outputs
+      for(std::set<int>::iterator it = sOutputs.begin(); it != sOutputs.end();) {
+        if(!sNodes.count(*it)) {
+          it = sOutputs.erase(it);
+        } else {
+          it++;
+        }
+      }
+      if(nVerbose) {
+        std::cout << "\tnew outputs: " << sOutputs << std::endl;
+      }
+    }
+    // ensure outputs of both windows do not reach each other's inputs at the same time
+    for(auto const &entry: mSubNtk2Io) {
+      if(!pNtk->IsReachable(sOutputs, std::get<1>(entry.second))) {
+        continue;
+      }
+      if(!pNtk->IsReachable(std::get<3>(entry.second), sInputs)) {
+        continue;
+      }
+      if(nVerbose) {
+        std::cout << "POTENTIAL LOOPS" << std::endl;
+      }
+      return NULL;
+    }
+    if(int_size(sNodes) < nWindowSize / 2) {
+      // too small
+      // TODO: fix this parameterized
+      return NULL;
+    }
+    // extract by inputs, internals, and outputs (no checks needed in ntk side)
+    std::vector<int> vInputs(sInputs.begin(), sInputs.end());
+    std::vector<int> vOutputs(sOutputs.begin(), sOutputs.end());
+    Ntk *pSubNtk = pNtk->Extract(sNodes, vInputs, vOutputs);
+    // return subntk to be modified, while remember IOs
+    for(int i: sNodes) {
+      sBlocked.insert(i);
+    }
+    mSubNtk2Io.emplace(pSubNtk, std::make_tuple(std::move(sNodes), std::move(vInputs), std::vector<bool>(vInputs.size()), std::move(vOutputs)));
+    return pSubNtk;
+  }
+  
+  /* }}} */
+
+  /* {{{ Constructors */
+  
+  template <typename Ntk>
+  Partitioner<Ntk>::Partitioner(Parameter const *pPar) :
+    nVerbose(pPar->nPartitionerVerbose),
+    nWindowSize(pPar->nWindowSize) {
+  }
+
+  template <typename Ntk>
+  void Partitioner<Ntk>::UpdateNetwork(Ntk *pNtk_) {
+    pNtk = pNtk_;
+  }
+
+  /* }}} */
+
+  /* {{{ APIs */
+  
+  template <typename Ntk>
+  Ntk *Partitioner<Ntk>::Extract(int iSeed) {
+    // pick a center node from candidates that do not belong to any other ongoing windows
+    std::mt19937 rng(iSeed);
+    std::vector<int> vInts = pNtk->GetInts();
+    std::shuffle(vInts.begin(), vInts.end(), rng);
+    for(int id: vInts) {
+      if(!sBlocked.count(id)) {
+        Ntk *pSubNtk = ExtractDisjoint(id);
+        if(pSubNtk) {
+          return pSubNtk;
+        }
+      }
+    }
+    return NULL;
+  }
+
+  template <typename Ntk>
+  void Partitioner<Ntk>::Insert(Ntk *pSubNtk) {
+    for(int i: std::get<0>(mSubNtk2Io[pSubNtk])) {
+      sBlocked.erase(i);
+    }
+    std::pair<std::vector<int>, std::vector<bool>> vNewSignals = pNtk->Insert(pSubNtk, std::get<1>(mSubNtk2Io[pSubNtk]), std::get<2>(mSubNtk2Io[pSubNtk]), std::get<3>(mSubNtk2Io[pSubNtk]));
+    std::vector<int> &vOldOutputs = std::get<3>(mSubNtk2Io[pSubNtk]);
+    std::vector<int> &vNewOutputs = vNewSignals.first;
+    std::vector<bool> &vNewCompls = vNewSignals.second;
+    // need to remap updated outputs that are used as inputs in other windows
+    std::map<int, int> mOutput2Idx;
+    for(int idx = 0; idx < int_size(vOldOutputs); idx++) {
+      mOutput2Idx[vOldOutputs[idx]] = idx;
+    }
+    for(auto &entry: mSubNtk2Io) {
+      if(entry.first != pSubNtk) {
+        std::vector<int> &vInputs = std::get<1>(entry.second);
+        std::vector<bool> &vCompls = std::get<2>(entry.second);
+        for(int i = 0; i < int_size(vInputs); i++) {
+          if(mOutput2Idx.count(vInputs[i])) {
+            int idx = mOutput2Idx[vInputs[i]];
+            vInputs[i] = vNewOutputs[idx];
+            vCompls[i] = vCompls[i] ^ vNewCompls[idx];
+          }
+        }
+      }
+    }
+    delete pSubNtk;
+    mSubNtk2Io.erase(pSubNtk);
+  }
+
+  /* }}} */
+  
+}
+
+ABC_NAMESPACE_CXX_HEADER_END
diff --git a/src/opt/rrr/rrrSatSolver.h b/src/opt/rrr/rrrSatSolver.h
index 6966eb807..ac9fa4c45 100644
--- a/src/opt/rrr/rrrSatSolver.h
+++ b/src/opt/rrr/rrrSatSolver.h
@@ -1,13 +1,9 @@
 #pragma once
 
-#include <iostream>
-#include <iomanip>
-#include <vector>
-
 #include <sat/bsat/satSolver.h>
 
 #include "rrrParameter.h"
-#include "rrrTypes.h"
+#include "rrrUtils.h"
 
 ABC_NAMESPACE_CXX_HEADER_START
 
@@ -47,7 +43,7 @@ namespace rrr {
     
   public:
     // constructors
-    SatSolver(Ntk *pNtk, Parameter const *pPar);
+    SatSolver(Parameter const *pPar);
     ~SatSolver();
     void UpdateNetwork(Ntk *pNtk_, bool fSame);
     
@@ -190,7 +186,7 @@ namespace rrr {
     }
     // store po vars (NOTE: it's not a lit)
     vLits.clear();
-    pNtk->ForEachPoDriver([&](int fi, bool c) {
+    pNtk->ForEachPoDriver([&](int fi) {
       vLits.push_back(v[fi]);
     });
     // encode an inverted copy
@@ -207,7 +203,7 @@ namespace rrr {
     }
     int idx = 0;
     int n = 0;
-    pNtk->ForEachPoDriver([&](int fi, bool c) {
+    pNtk->ForEachPoDriver([&](int fi) {
       assert(fi != id);
       if(v[fi] != vLits[idx]) {
         int x = sat_solver_addvar(p);
@@ -256,8 +252,8 @@ namespace rrr {
   /* {{{ Constructors */
 
   template <typename Ntk>
-  SatSolver<Ntk>::SatSolver(Ntk *pNtk, Parameter const *pPar) :
-    pNtk(pNtk),
+  SatSolver<Ntk>::SatSolver(Parameter const *pPar) :
+    pNtk(NULL),
     nVerbose(pPar->nSatSolverVerbose),
     nConflictLimit(pPar->nConflictLimit),
     pSat(sat_solver_new()),
@@ -267,7 +263,6 @@ namespace rrr {
     nCalls(0),
     nSats(0),
     nUnsats(0) {
-    pNtk->AddCallback(std::bind(&SatSolver<Ntk>::ActionCallback, this, std::placeholders::_1));
   }
 
   template <typename Ntk>
@@ -278,6 +273,7 @@ namespace rrr {
 
   template <typename Ntk>
   void SatSolver<Ntk>::UpdateNetwork(Ntk *pNtk_, bool fSame) {
+    (void)fSame;
     pNtk = pNtk_;
     status = false;
     target = -1;
diff --git a/src/opt/rrr/rrrScheduler.h b/src/opt/rrr/rrrScheduler.h
index 3b7f3457d..c8b5a16a0 100644
--- a/src/opt/rrr/rrrScheduler.h
+++ b/src/opt/rrr/rrrScheduler.h
@@ -1,12 +1,17 @@
 #pragma once
 
-#include <iostream>
-#include <iomanip>
+#include <queue>
 #include <random>
 
-#include "rrrParameter.h"
-#include "rrrTypes.h"
+#ifdef ABC_USE_PTHREADS
+#include <thread>
+#include <mutex>
+#include <condition_variable>
+#endif
 
+#include "rrrParameter.h"
+#include "rrrUtils.h"
+#include "rrrPartitioner.h"
 #include "rrrAbc.h"
 
 ABC_NAMESPACE_CXX_HEADER_START
@@ -16,87 +21,147 @@ namespace rrr {
   template <typename Ntk, typename Opt>
   class Scheduler {
   private:
+    // job
+    struct Job;
+    struct CompareJobPointers;
+    
     // pointer to network
     Ntk *pNtk;
 
     // parameters
     int nVerbose;
+    int iSeed;
     int nFlow;
-
-    // copy of parameter (maybe updated during the run)
-    Parameter Par;
-
+    int nRestarts;
+    bool fMultiThreading;
+    bool fPartitioning;
+    bool fDeterministic;
+    seconds nTimeout;
+    std::function<double(Ntk *)> CostFunction;
+    
     // data
+    int nJobs;
+    int nFinishedJobs;
     time_point start;
+    Partitioner<Ntk> par;
+    std::queue<Job *> qPendingJobs;
+    Opt *pOpt; // used only in case of single thread execution
+#ifdef ABC_USE_PTHREADS
+    bool fTerminate;
+    std::vector<std::thread> vThreads;
+    std::priority_queue<Job *, std::vector<Job *>, CompareJobPointers> qFinishedJobs;
+    std::mutex mutexAbc;
+    std::mutex mutexPendingJobs;
+    std::mutex mutexFinishedJobs;
+    std::condition_variable condPendingJobs;
+    std::condition_variable condFinishedJobs;
+#endif
 
     // time
-    seconds GetRemainingTime();
+    seconds GetRemainingTime() const;
 
+    // abc
+    void CallAbc(Ntk *pNtk_, std::string Command);
+
+    // run jobs
+    void RunJob(Opt &opt, Job const *pJob);
+
+    // manage jobs
+    void CreateJob(Ntk *pNtk_, int iSeed_);
+    void OnJobEnd(std::function<void(Job *pJob)> const &func);
+
+    // thread
+#ifdef ABC_USE_PTHREADS
+    void Thread(Parameter const *pPar);
+#endif
+    
   public:
-    // constructor
+    // constructors
     Scheduler(Ntk *pNtk, Parameter const *pPar);
-
+    ~Scheduler();
+    
     // run
     void Run();
   };
 
-  /* {{{ time */
+  /* {{{ Job */
+  
+  template <typename Ntk, typename Opt>
+  struct Scheduler<Ntk, Opt>::Job {
+    // data
+    int id;
+    Ntk *pNtk;
+    int iSeed;
+    
+    // constructor
+    Job(int id, Ntk *pNtk, int iSeed) :
+      id(id),
+      pNtk(pNtk),
+      iSeed(iSeed) {
+    }
+  };
 
   template <typename Ntk, typename Opt>
-  seconds Scheduler<Ntk, Opt>::GetRemainingTime() {
-    if(Par.nTimeout == 0) {
+  struct Scheduler<Ntk, Opt>::CompareJobPointers {
+    // smaller id comes first in priority_queue
+    bool operator()(Job const *lhs, Job const *rhs) const {
+      return lhs->id > rhs->id;
+    }
+  };
+  
+  /* }}} */
+
+  /* {{{ Time */
+
+  template <typename Ntk, typename Opt>
+  seconds Scheduler<Ntk, Opt>::GetRemainingTime() const {
+    if(nTimeout == 0) {
       return 0;
     }
     time_point current = GetCurrentTime();
-    seconds nTimeout = Par.nTimeout - DurationInSeconds(start, current);
-    if(nTimeout == 0) { // avoid glitch
+    seconds nRemainingTime = nTimeout - DurationInSeconds(start, current);
+    if(nRemainingTime == 0) { // avoid glitch
       return -1;
     }
-    return nTimeout;
+    return nRemainingTime;
   }
 
   /* }}} */
 
-  /* {{{ Constructor */
-  
+  /* {{{ Abc */
+
   template <typename Ntk, typename Opt>
-  Scheduler<Ntk, Opt>::Scheduler(Ntk *pNtk, Parameter const *pPar) :
-    pNtk(pNtk),
-    nVerbose(pPar->nSchedulerVerbose),
-    nFlow(pPar->nSchedulerFlow),
-    Par(*pPar) {
-    // TODO: allocations and other preparations should be done here
+  inline void Scheduler<Ntk, Opt>::CallAbc(Ntk *pNtk_, std::string Command) {
+#ifdef ABC_USE_PTHREADS
+    if(fMultiThreading) {
+      {
+        std::unique_lock<std::mutex> l(mutexAbc);
+        Abc9Execute(pNtk_, Command);
+      }
+      return;
+    }
+#endif
+    Abc9Execute(pNtk_, Command);
   }
 
   /* }}} */
+  
+  /* {{{ Run jobs */
 
-  /* {{{ Run */
-  
-  // TODO: have multiplie optimizers running on different windows/partitions
-  // TODO: run ABC on those windows or even on the entire network, maybe as a separate class
-  
   template <typename Ntk, typename Opt>
-  void Scheduler<Ntk, Opt>::Run() {
-    start = GetCurrentTime();
-    // prepare cost function
-    std::function<double(Ntk *)> CostFunction;
-    CostFunction = [](Ntk *pNtk) {
-      int nTwoInputSize = 0;
-      pNtk->ForEachInt([&](int id) {
-        nTwoInputSize += pNtk->GetNumFanins(id) - 1;
-      });
-      return nTwoInputSize;
-    };
+  void Scheduler<Ntk, Opt>::RunJob(Opt &opt, Job const *pJob) {
+    opt.UpdateNetwork(pJob->pNtk);
     // start flow
-    Opt opt(pNtk, &Par, CostFunction);
     switch(nFlow) {
     case 0:
+      opt.ResetSeed(pJob->iSeed);
       opt.Run(GetRemainingTime());
       break;
     case 1: { // transtoch
-      double dCost = CostFunction(pNtk);
+      std::mt19937 rng(pJob->iSeed);
+      double dCost = CostFunction(pJob->pNtk);
       double dBestCost = dCost;
-      Ntk best(*pNtk);
+      Ntk best(*(pJob->pNtk));
       if(nVerbose) {
         std::cout << "start: cost = " << dCost << std::endl;
       }
@@ -105,9 +170,9 @@ namespace rrr {
           break;
         }
         if(i != 0) {
-          Abc9Execute(pNtk, "&if -K 6; &mfs; &st");
-          dCost = CostFunction(pNtk);
-          opt.UpdateNetwork(pNtk, true);
+          CallAbc(pJob->pNtk, "&if -K 6; &mfs; &st");
+          dCost = CostFunction(pJob->pNtk);
+          opt.UpdateNetwork(pJob->pNtk, true);
           if(nVerbose) {
             std::cout << "hop " << std::setw(3) << i << ": cost = " << dCost << std::endl;
           }
@@ -116,37 +181,37 @@ namespace rrr {
           if(GetRemainingTime() < 0) {
             break;
           }
-          opt.Randomize();
+          opt.Randomize(rng());
           opt.Run(GetRemainingTime());
-          Abc9Execute(pNtk, "&dc2");
-          double dNewCost = CostFunction(pNtk);
+          CallAbc(pJob->pNtk, "&dc2");
+          double dNewCost = CostFunction(pJob->pNtk);
           if(nVerbose) {
             std::cout << "\tite " << std::setw(3) << j << ": cost = " << dNewCost << std::endl;
           }
           if(dNewCost < dCost) {
             dCost = dNewCost;
-            opt.UpdateNetwork(pNtk, true);
+            opt.UpdateNetwork(pJob->pNtk, true);
           } else {
             break;
           }
         }
         if(dCost < dBestCost) {
           dBestCost = dCost;
-          best = *pNtk;
+          best = *(pJob->pNtk);
           i = 0;
         }
       }
-      *pNtk = best;
+      *(pJob->pNtk) = best;
       if(nVerbose) {
         std::cout << "end: cost = " << dBestCost << std::endl;
       }
       break;
     }
     case 2: { // deep
-      double dCost = CostFunction(pNtk);
-      Ntk best(*pNtk);
+      std::mt19937 rng(pJob->iSeed);
       int n = 0;
-      std::mt19937 rng(Par.iSeed);
+      double dCost = CostFunction(pJob->pNtk);
+      Ntk best(*(pJob->pNtk));
       if(nVerbose) {
         std::cout << "start: cost = " << dCost << std::endl;
       }
@@ -179,37 +244,37 @@ namespace rrr {
         if(fFx)
           Command += "; &fx; &st";
         Command += pComp;
-        Abc9Execute(pNtk, Command);
+        CallAbc(pJob->pNtk, Command);
         if(nVerbose) {
-          std::cout << "ite " << std::setw(6) << i << ": cost = " << CostFunction(pNtk) << std::endl;
+          std::cout << "ite " << std::setw(6) << i << ": cost = " << CostFunction(pJob->pNtk) << std::endl;
         }
         // rrr
         for(int j = 0; j < n; j++) {
           if(GetRemainingTime() < 0) {
             break;
           }
-          opt.Randomize();
-          opt.UpdateNetwork(pNtk, true);
+          opt.UpdateNetwork(pJob->pNtk, true);
+          opt.Randomize(rng());
           opt.Run(GetRemainingTime());
           if(rng() & 1) {
-            Abc9Execute(pNtk, "&dc2");
+            CallAbc(pJob->pNtk, "&dc2");
           } else {
-            Abc9Execute(pNtk, "&put; " + pCompress2rs + "; &get");
+            CallAbc(pJob->pNtk, "&put; " + pCompress2rs + "; &get");
           }
           if(nVerbose) {
-            std::cout << "\trrr " << std::setw(6) << j << ": cost = " << CostFunction(pNtk) << std::endl;
+            std::cout << "\trrr " << std::setw(6) << j << ": cost = " << CostFunction(pJob->pNtk) << std::endl;
           }
         }
         // eval
-        double dNewCost = CostFunction(pNtk);
+        double dNewCost = CostFunction(pJob->pNtk);
         if(dNewCost < dCost) {
           dCost = dNewCost;
-          best = *pNtk;
+          best = *(pJob->pNtk);
         } else {
           n++;
         }
       }
-      *pNtk = best;
+      *(pJob->pNtk) = best;
       if(nVerbose) {
         std::cout << "end: cost = " << dCost << std::endl;
       }
@@ -218,6 +283,208 @@ namespace rrr {
     default:
       assert(0);
     }
+  }
+
+  /* }}} */
+
+  /* {{{ Manage jobs */
+
+  template <typename Ntk, typename Opt>
+  void Scheduler<Ntk, Opt>::CreateJob(Ntk *pNtk_, int iSeed_) {
+    Job *pJob = new Job(nJobs++, pNtk_, iSeed_);
+#ifdef ABC_USE_PTHREADS
+    if(fMultiThreading) {
+      {
+        std::unique_lock<std::mutex> l(mutexPendingJobs);
+        qPendingJobs.push(pJob);
+        condPendingJobs.notify_one();
+      }
+      return;
+    }
+#endif
+    qPendingJobs.push(pJob);
+  }
+  
+  template <typename Ntk, typename Opt>
+  void Scheduler<Ntk, Opt>::OnJobEnd(std::function<void(Job *pJob)> const &func) {
+#ifdef ABC_USE_PTHREADS
+    if(fMultiThreading) {
+      Job *pJob = NULL;
+      {
+        std::unique_lock<std::mutex> l(mutexFinishedJobs);
+        while(qFinishedJobs.empty() || (fDeterministic && qFinishedJobs.top()->id != nFinishedJobs)) {
+          condFinishedJobs.wait(l);
+        }
+        pJob = qFinishedJobs.top();
+        qFinishedJobs.pop();
+      }
+      assert(pJob != NULL);
+      func(pJob);
+      delete pJob;
+      nFinishedJobs++;
+      return;
+    }
+#endif
+    // if single thread
+    assert(!qPendingJobs.empty());
+    Job *pJob = qPendingJobs.front();
+    qPendingJobs.pop();
+    RunJob(*pOpt, pJob);
+    func(pJob);
+    delete pJob;
+    nFinishedJobs++;
+  }
+  
+  /* }}} */
+
+  /* {{{ Thread */
+
+#ifdef ABC_USE_PTHREADS
+  template <typename Ntk, typename Opt>
+  void Scheduler<Ntk, Opt>::Thread(Parameter const *pPar) {
+    Opt opt(pPar, CostFunction);
+    while(true) {
+      Job *pJob = NULL;
+      {
+        std::unique_lock<std::mutex> l(mutexPendingJobs);
+        while(!fTerminate && qPendingJobs.empty()) {
+          condPendingJobs.wait(l);
+        }
+        if(fTerminate) {
+          assert(qPendingJobs.empty());
+          return;
+        }
+        pJob = qPendingJobs.front();
+        qPendingJobs.pop();
+      }
+      assert(pJob != NULL);
+      RunJob(opt, pJob);
+      {
+        std::unique_lock<std::mutex> l(mutexFinishedJobs);
+        qFinishedJobs.push(pJob);
+        condFinishedJobs.notify_one();
+      }
+    }
+  }
+#endif
+
+  /* }}} */
+  
+  /* {{{ Constructors */
+  
+  template <typename Ntk, typename Opt>
+  Scheduler<Ntk, Opt>::Scheduler(Ntk *pNtk, Parameter const *pPar) :
+    pNtk(pNtk),
+    nVerbose(pPar->nSchedulerVerbose),
+    iSeed(pPar->iSeed),
+    nFlow(pPar->nSchedulerFlow),
+    nRestarts(pPar->nRestarts),
+    fMultiThreading(pPar->nThreads > 1),
+    fPartitioning(pPar->nWindowSize > 0),
+    fDeterministic(pPar->fDeterministic),
+    nTimeout(pPar->nTimeout),
+    nJobs(0),
+    nFinishedJobs(0),
+    par(pPar),
+    pOpt(NULL) {
+    // prepare cost function
+    CostFunction = [](Ntk *pNtk) {
+      int nTwoInputSize = 0;
+      pNtk->ForEachInt([&](int id) {
+        nTwoInputSize += pNtk->GetNumFanins(id) - 1;
+      });
+      return nTwoInputSize;
+    };
+#ifdef ABC_USE_PTHREADS
+    fTerminate = false;
+    if(fMultiThreading) {
+      vThreads.reserve(pPar->nThreads);
+      for(int i = 0; i < pPar->nThreads; i++) {
+        vThreads.emplace_back(std::bind(&Scheduler::Thread, this, pPar));
+      }
+      return;
+    }
+#endif
+    assert(!fMultiThreading);
+    pOpt = new Opt(pPar, CostFunction);
+  }
+
+  template <typename Ntk, typename Opt>
+  Scheduler<Ntk, Opt>::~Scheduler() {
+#ifdef ABC_USE_PTHREADS
+    if(fMultiThreading) {
+      {
+        std::unique_lock<std::mutex> l(mutexPendingJobs);
+        fTerminate = true;
+        condPendingJobs.notify_all();
+      }
+      for(std::thread &t: vThreads) {
+        t.join();
+      }
+      return;
+    }
+#endif
+    delete pOpt;
+  }
+
+  /* }}} */
+
+  /* {{{ Run */
+  
+  template <typename Ntk, typename Opt>
+  void Scheduler<Ntk, Opt>::Run() {
+    start = GetCurrentTime();
+    if(fPartitioning) {
+      pNtk->Sweep();
+      par.UpdateNetwork(pNtk);
+      while(nJobs < nRestarts) {
+        Ntk *pSubNtk = par.Extract(iSeed + nJobs);
+        if(pSubNtk == NULL) {
+          if(nJobs == nFinishedJobs) {
+            std::cout << "failed to extract a window" << std::endl;
+            break;
+          }
+          while(nFinishedJobs < nJobs) {
+            OnJobEnd([&](Job *pJob) {
+              std::cout << "job " << pJob->id << " finished (size = " << pJob->pNtk->GetNumInts() << ")" << std::endl;
+              par.Insert(pJob->pNtk);
+            });
+          }
+        } else {
+          CreateJob(pSubNtk, iSeed + nJobs);
+          std::cout << "job " << nJobs - 1 << " created (size = " << pSubNtk->GetNumInts() << ")" << std::endl;
+        }
+      }
+      while(nFinishedJobs < nJobs) {
+        OnJobEnd([&](Job *pJob) {
+          std::cout << "job " << pJob->id << " finished (size = " << pJob->pNtk->GetNumInts() << ")" << std::endl;
+          par.Insert(pJob->pNtk);
+        });
+      }
+    } else if(nRestarts > 0) {
+      fDeterministic = false; // it is deterministic anyways
+      double dCost = CostFunction(pNtk);
+      for(int i = 0; i < 1 + nRestarts; i++) {
+        Ntk *pCopy = new Ntk(*pNtk);
+        CreateJob(pCopy, iSeed + i);
+      }
+      for(int i = 0; i < 1 + nRestarts; i++) {
+        OnJobEnd([&](Job *pJob) {
+          double dNewCost = CostFunction(pJob->pNtk);
+          if(nVerbose) {
+            std::cout << "run " << pJob->id << ": cost = " << dNewCost << std::endl;
+          }
+          if(dNewCost < dCost) {
+            dCost = dNewCost;
+            *pNtk = *(pJob->pNtk);
+          }
+          delete pJob->pNtk;
+        });
+      }
+    } else {
+      CreateJob(pNtk, iSeed);
+      OnJobEnd([&](Job *pJob) { (void)pJob; });
+    }
     time_point end = GetCurrentTime();
     double elapsed_seconds = Duration(start, end);
     if(nVerbose) {
diff --git a/src/opt/rrr/rrrSimulator.h b/src/opt/rrr/rrrSimulator.h
index 67a6c7738..8d5c80c87 100644
--- a/src/opt/rrr/rrrSimulator.h
+++ b/src/opt/rrr/rrrSimulator.h
@@ -1,15 +1,11 @@
 #pragma once
 
-#include <iostream>
-#include <iomanip>
-#include <vector>
-#include <set>
 #include <algorithm>
 #include <random>
 #include <bitset>
 
 #include "rrrParameter.h"
-#include "rrrTypes.h"
+#include "rrrUtils.h"
 
 ABC_NAMESPACE_CXX_HEADER_START
 
@@ -87,7 +83,7 @@ namespace rrr {
   public:
     // constructors
     Simulator();
-    Simulator(Ntk *pNtk, Parameter const *pPar);
+    Simulator(Parameter const *pPar);
     ~Simulator();
     void UpdateNetwork(Ntk *pNtk_, bool fSame);
 
@@ -267,7 +263,7 @@ namespace rrr {
   void Simulator<Ntk>::SimulateNode(std::vector<word> &v, int id, int to_negate) {
     itr x = v.end();
     itr y = v.begin() + id * nWords;
-    bool cx;
+    bool cx = false;
     switch(pNtk->GetNodeType(id)) {
     case AND:
       pNtk->ForEachFanin(id, [&](int fi, bool c) {
@@ -292,7 +288,7 @@ namespace rrr {
   template <typename Ntk>
   bool Simulator<Ntk>::ResimulateNode(std::vector<word> &v, int id, int to_negate) {
     itr x = v.end();
-    bool cx;
+    bool cx = false;
     switch(pNtk->GetNodeType(id)) {
     case AND:
       pNtk->ForEachFanin(id, [&](int fi, bool c) {
@@ -324,7 +320,7 @@ namespace rrr {
   void Simulator<Ntk>::SimulateOneWordNode(std::vector<word> &v, int id, int offset, int to_negate) {
     itr x = v.end();
     itr y = v.begin() + id * nWords + offset;
-    bool cx;
+    bool cx = false;
     switch(pNtk->GetNodeType(id)) {
     case AND:
       pNtk->ForEachFanin(id, [&](int fi, bool c) {
@@ -476,7 +472,7 @@ namespace rrr {
     });
     */
     Clear(nWords, care.begin());
-    pNtk->ForEachPoDriver([&](int fi, bool c) {
+    pNtk->ForEachPoDriver([&](int fi) {
       assert(fi != target);
       for(int i = 0; i < nWords; i++) {
         care[i] = care[i] | (vValues[fi * nWords + i] ^ vValues2[fi * nWords + i]);
@@ -495,7 +491,9 @@ namespace rrr {
 
   template <typename Ntk>
   void Simulator<Ntk>::Save(int slot) {
-    if(slot >= vBackups.size()) {
+    assert(slot >= 0);
+    assert(!check_int_max(slot));
+    if(slot >= int_size(vBackups)) {
       vBackups.resize(slot + 1);
     }
     vBackups[slot].nWords = nWords;
@@ -522,7 +520,8 @@ namespace rrr {
 
   template <typename Ntk>
   void Simulator<Ntk>::Load(int slot) {
-    assert(slot < vBackups.size());
+    assert(slot >= 0);
+    assert(slot < int_size(vBackups));
     nWords  = vBackups[slot].nWords;
     target  = vBackups[slot].target;
     vValues = vBackups[slot].vValues;
@@ -551,8 +550,8 @@ namespace rrr {
   }
   
   template <typename Ntk>
-  Simulator<Ntk>::Simulator(Ntk *pNtk, Parameter const *pPar) :
-    pNtk(pNtk),
+  Simulator<Ntk>::Simulator(Parameter const *pPar) :
+    pNtk(NULL),
     nVerbose(pPar->nSimulatorVerbose),
     nWords(pPar->nWords),
     target(-1),
@@ -560,13 +559,8 @@ namespace rrr {
     fUpdate(false),
     nAdds(0),
     nResets(0) {
-    pNtk->AddCallback(std::bind(&Simulator<Ntk>::ActionCallback, this, std::placeholders::_1));
-    vValues.resize(nWords * pNtk->GetNumNodes());
     care.resize(nWords);
     tmp.resize(nWords);
-    vAssignedStimuli.resize(nWords * pNtk->GetNumPis());
-    GenerateRandomStimuli();
-    Simulate();
   }
 
   template <typename Ntk>
@@ -603,7 +597,7 @@ namespace rrr {
     switch(pNtk->GetNodeType(id)) {
     case AND: {
       itr x = vValues.end();
-      bool cx;
+      bool cx = false;
       pNtk->ForEachFaninIdx(id, [&](int idx2, int fi, bool c) {
         if(idx == idx2) {
           return;
@@ -640,7 +634,7 @@ namespace rrr {
     switch(pNtk->GetNodeType(id)) {
     case AND: {
       itr x = vValues.end();
-      bool cx;
+      bool cx = false;
       pNtk->ForEachFanin(id, [&](int fi, bool c) {
         if(x == vValues.end()) {
           x = vValues.begin() + fi * nWords;
@@ -680,7 +674,7 @@ namespace rrr {
       std::cout << std::endl;
     }
     // record care pi indices
-    assert((int)vCex.size() == pNtk->GetNumPis());
+    assert(int_size(vCex) == pNtk->GetNumPis());
     std::vector<int> vCarePiIdxs;
     for(int idx = 0; idx < pNtk->GetNumPis(); idx++) {
       switch(vCex[idx]) {
@@ -792,7 +786,7 @@ namespace rrr {
         }
       });
       Clear(1, care.begin() + iWord);
-      pNtk->ForEachPoDriver([&](int fi, bool c) {
+      pNtk->ForEachPoDriver([&](int fi) {
         assert(fi != target);
         care[iWord] = care[iWord] | (vValues[fi * nWords + iWord] ^ vValues2[fi * nWords + iWord]);
       });
diff --git a/src/opt/rrr/rrrTypes.h b/src/opt/rrr/rrrTypes.h
index f98c3fd37..858b65a5f 100644
--- a/src/opt/rrr/rrrTypes.h
+++ b/src/opt/rrr/rrrTypes.h
@@ -1,10 +1,7 @@
 #pragma once
 
-#include <iostream>
 #include <vector>
-#include <string>
 #include <chrono>
-#include <cassert>
 
 ABC_NAMESPACE_CXX_HEADER_START
 
@@ -32,44 +29,6 @@ namespace rrr {
     TEMP_FALSE
   };
 
-  /* {{{ VarValue functions */
-  
-  static inline VarValue DecideVarValue(VarValue x) {
-    switch(x) {
-    case UNDEF:
-      assert(0);
-    case TRUE:
-      return TRUE;
-    case FALSE:
-      return FALSE;
-    case TEMP_TRUE:
-      return TRUE;
-    case TEMP_FALSE:
-      return FALSE;
-    default:
-      assert(0);
-    }
-  }
-
-  static inline char GetVarValueChar(VarValue x) {
-    switch(x) {
-    case UNDEF:
-      return 'x';
-    case TRUE:
-      return '1';
-    case FALSE:
-      return '0';
-    case TEMP_TRUE:
-      return 't';
-    case TEMP_FALSE:
-      return 'f';
-    default:
-      assert(0);
-    }
-  }
-
-  /* }}} */
-
   enum ActionType {
     NONE,
     REMOVE_FANIN,
@@ -82,7 +41,8 @@ namespace rrr {
     SORT_FANINS,
     SAVE,
     LOAD,
-    POP_BACK
+    POP_BACK,
+    INSERT
   };
 
   struct Action {
@@ -96,112 +56,10 @@ namespace rrr {
     std::vector<int> vFanouts;
   };
 
-  /* {{{ Action functions */
-
-  static inline void PrintAction(Action action) {
-    switch(action.type) {
-    case REMOVE_FANIN:
-      std::cout << "remove fanin";
-      break;
-    case REMOVE_UNUSED:
-      std::cout << "remove unused";
-      break;
-    case REMOVE_BUFFER:
-      std::cout << "remove buffer";
-      break;
-    case REMOVE_CONST:
-      std::cout << "remove const";
-      break;
-    case ADD_FANIN:
-      std::cout << "add fanin";
-      break;
-    case TRIVIAL_COLLAPSE:
-      std::cout << "trivial collapse";
-      break;
-    case TRIVIAL_DECOMPOSE:
-      std::cout << "trivial decompose";
-      break;
-    case SORT_FANINS:
-      std::cout << "sort fanins";
-      break;
-    case SAVE:
-      std::cout << "save";
-      break;
-    case LOAD:
-      std::cout << "load";
-      break;
-    case POP_BACK:
-      std::cout << "pop back";
-      break;
-    default:
-      assert(0);
-    }
-    std::cout << ":";
-    if(action.id != -1) {
-      std::cout << " node " << action.id;
-    }
-    if(action.fi != -1) {
-      std::cout << " fanin " << (action.c? "!": "") << action.fi;
-    }
-    if(action.idx != -1) {
-      std::cout << " index " << action.idx;
-    }
-    std::cout << std::endl;
-    if(!action.vFanins.empty()) {
-      std::cout << "\t" << "fanins: ";
-      std::string delim = "";
-      for(int fi: action.vFanins) {
-        std::cout << delim << fi;
-        delim = ", ";
-      }
-      std::cout << std::endl;
-    }
-    if(!action.vIndices.empty()) {
-      std::cout << "\t" << "indices: ";
-      std::string delim = "";
-      for(int fi: action.vIndices) {
-        std::cout << delim << fi;
-        delim = ", ";
-      }
-      std::cout << std::endl;
-    }
-    if(!action.vFanouts.empty()) {
-      std::cout << "\t" << "fanouts: ";
-      std::string delim = "";
-      for(int fo: action.vFanouts) {
-        std::cout << delim << fo;
-        delim = ", ";
-      }
-      std::cout << std::endl;
-    }
-  }
-
-  /* }}} */
-
   using seconds = int64_t;
   using clock_type = std::chrono::steady_clock;
   using time_point = std::chrono::time_point<clock_type>;
-  
-  /* {{{ Time functions */
-  
-  static inline time_point GetCurrentTime() {
-    return clock_type::now();
-  }
 
-  static inline seconds DurationInSeconds(time_point start, time_point end) {
-    seconds t = (std::chrono::duration_cast<std::chrono::seconds>(end - start)).count();
-    assert(t >= 0);
-    return t;
-  }
-
-  static inline double Duration(time_point start, time_point end) {
-    double t = (std::chrono::duration<double>(end - start)).count();
-    assert(t >= 0);
-    return t;
-  }
-
-  /* }}} */
-  
 }
 
 ABC_NAMESPACE_CXX_HEADER_END
diff --git a/src/opt/rrr/rrrUtils.h b/src/opt/rrr/rrrUtils.h
new file mode 100644
index 000000000..f41593d52
--- /dev/null
+++ b/src/opt/rrr/rrrUtils.h
@@ -0,0 +1,215 @@
+#pragma once
+
+#include <iostream>
+#include <iomanip>
+#include <vector>
+#include <set>
+#include <string>
+#include <functional>
+#include <limits>
+#include <type_traits>
+#include <cassert>
+
+#include "rrrTypes.h"
+
+ABC_NAMESPACE_CXX_HEADER_START
+
+namespace rrr {
+
+  /* {{{ Invocable */
+
+#if defined(__cpp_lib_is_invocable)
+  template <typename Fn, typename... Args>
+  using is_invokable = std::is_invocable<Fn, Args...>;
+#else
+  template <typename Fn, typename... Args>
+  struct is_invokable: std::is_constructible<std::function<void(Args...)>, std::reference_wrapper<typename std::remove_reference<Fn>::type>> {};
+#endif
+
+  /* }}} */
+
+  /* {{{ Int size */
+  
+  template <template <typename...> typename Container, typename ... Ts>
+  static inline int int_size(Container<Ts...> const &c) {
+    assert(c.size() <= (typename Container<Ts...>::size_type)std::numeric_limits<int>::max());
+    return c.size();
+  }
+
+  template <template <typename...> typename Container, typename ... Ts>
+  static inline bool check_int_size(Container<Ts...> const &c) {
+    return c.size() <= (typename Container<Ts...>::size_type)std::numeric_limits<int>::max();
+  }
+
+  static inline bool check_int_max(int i) {
+    return i == std::numeric_limits<int>::max();
+  }
+  
+  /* }}} */
+  
+  /* {{{ Print helpers */
+
+  template <typename T>
+  std::ostream& operator<<(std::ostream& os, const std::vector<T>& v) {
+    std::string delim;
+    os << "[";
+    for(T const &e: v) {
+      os << delim << e;
+      delim = ", ";
+    }
+    os << "]";
+    return os;
+  }
+  
+  template <typename T>
+  std::ostream& operator<<(std::ostream& os, const std::set<T>& s) {
+    std::string delim;
+    os << "{";
+    for(T const &e: s) {
+      os << delim << e;
+      delim = ", ";
+    }
+    os << "}";
+    return os;
+  }
+
+  void PrintComplementedEdges(std::function<void(std::function<void(int, bool)> const &)> const &ForEachEdge) {
+    std::string delim;
+    std::cout << "[";
+    ForEachEdge([&] (int id, bool c) {
+      std::cout << delim << (c? "!": "") << id;
+      delim = ", ";
+    });
+    std::cout << "]";
+  }
+
+  /* }}} */
+  
+  /* {{{ VarValue functions */
+  
+  static inline VarValue DecideVarValue(VarValue x) {
+    switch(x) {
+    case UNDEF:
+      assert(0);
+    case TRUE:
+      return TRUE;
+    case FALSE:
+      return FALSE;
+    case TEMP_TRUE:
+      return TRUE;
+    case TEMP_FALSE:
+      return FALSE;
+    default:
+      assert(0);
+    }
+  }
+
+  static inline char GetVarValueChar(VarValue x) {
+    switch(x) {
+    case UNDEF:
+      return 'x';
+    case TRUE:
+      return '1';
+    case FALSE:
+      return '0';
+    case TEMP_TRUE:
+      return 't';
+    case TEMP_FALSE:
+      return 'f';
+    default:
+      assert(0);
+    }
+  }
+
+  /* }}} */
+
+  /* {{{ Action functions */
+
+  static inline void PrintAction(Action action) {
+    switch(action.type) {
+    case REMOVE_FANIN:
+      std::cout << "remove fanin";
+      break;
+    case REMOVE_UNUSED:
+      std::cout << "remove unused";
+      break;
+    case REMOVE_BUFFER:
+      std::cout << "remove buffer";
+      break;
+    case REMOVE_CONST:
+      std::cout << "remove const";
+      break;
+    case ADD_FANIN:
+      std::cout << "add fanin";
+      break;
+    case TRIVIAL_COLLAPSE:
+      std::cout << "trivial collapse";
+      break;
+    case TRIVIAL_DECOMPOSE:
+      std::cout << "trivial decompose";
+      break;
+    case SORT_FANINS:
+      std::cout << "sort fanins";
+      break;
+    case SAVE:
+      std::cout << "save";
+      break;
+    case LOAD:
+      std::cout << "load";
+      break;
+    case POP_BACK:
+      std::cout << "pop back";
+      break;
+    case INSERT:
+      std::cout << "insert";
+      break;
+    default:
+      assert(0);
+    }
+    std::cout << ":";
+    if(action.id != -1) {
+      std::cout << " node " << action.id;
+    }
+    if(action.fi != -1) {
+      std::cout << " fanin " << (action.c? "!": "") << action.fi;
+    }
+    if(action.idx != -1) {
+      std::cout << " index " << action.idx;
+    }
+    std::cout << std::endl;
+    if(!action.vFanins.empty()) {
+      std::cout << "\t" << "fanins: " << action.vFanins << std::endl;
+    }
+    if(!action.vIndices.empty()) {
+      std::cout << "\t" << "indices: " << action.vIndices << std::endl;
+    }
+    if(!action.vFanouts.empty()) {
+      std::cout << "\t" << "fanouts: " << action.vFanouts << std::endl;
+    }
+  }
+
+  /* }}} */
+  
+  /* {{{ Time functions */
+  
+  static inline time_point GetCurrentTime() {
+    return clock_type::now();
+  }
+
+  static inline seconds DurationInSeconds(time_point start, time_point end) {
+    seconds t = (std::chrono::duration_cast<std::chrono::seconds>(end - start)).count();
+    assert(t >= 0);
+    return t;
+  }
+
+  static inline double Duration(time_point start, time_point end) {
+    double t = (std::chrono::duration<double>(end - start)).count();
+    assert(t >= 0);
+    return t;
+  }
+
+  /* }}} */
+
+}
+
+ABC_NAMESPACE_CXX_HEADER_END