Merge pull request #405 from MyskYko/rrr

update rrr

src/aig/gia/giaRrr.cpp

@@ -35,7 +35,7 @@ Gia_Man_t *Gia_ManRrr(Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int
   Par.fOptOnInsert = fOptOnInsert;
   Par.fGreedy = fGreedy;
   rrr::Perform(&ntk, &Par);
-  Gia_Man_t *pNew = rrr::CreateGia(&ntk);
+  Gia_Man_t *pNew = rrr::CreateGia(&ntk, false);
   return pNew;
 }
 

src/base/abci/abc.c

@@ -46327,7 +46327,7 @@ 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, nPartitionerVerbose = 0, nOptimizerVerbose = 0, nAnalyzerVerbose = 0, nSimulatorVerbose = 0, nSatSolverVerbose = 0, fUseBddCspf = 0, fUseBddMspf = 0, nConflictLimit = 0, nSortType = -1, nOptimizerFlow = 0, nSchedulerFlow = 0, nPartitionType = 0, nDistance = 0, nJobs = 1, nThreads = 1, nPartitionSize = 0, nPartitionSizeMin = 0, fDeterministic = 1, nParallelPartitions = 1, fOptOnInsert = 0, fGreedy = 1;
+    int iSeed = 0, nWords = 10, nTimeout = 0, nSchedulerVerbose = 0, nPartitionerVerbose = 0, nOptimizerVerbose = 0, nAnalyzerVerbose = 0, nSimulatorVerbose = 0, nSatSolverVerbose = 0, fUseBddCspf = 0, fUseBddMspf = 0, nConflictLimit = 0, nSortType = -1, nOptimizerFlow = 0, nSchedulerFlow = 0, nPartitionType = 0, nDistance = 0, nJobs = 1, nThreads = 1, nPartitionSize = 0, nPartitionSizeMin = 0, fDeterministic = 1, nParallelPartitions = 1, fOptOnInsert = 0, fGreedy = 1;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "XYZNJKLBDRWTCGVPOAQSabdegh" ) ) != EOF )
     {
@@ -46446,6 +46446,51 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     
+    if ( nSchedulerVerbose )
+    {
+        Abc_Print( 2, "Using the following parameters :\n" );
+        Abc_Print( 2, "\t-X %3d : method ", nOptimizerFlow );
+        switch( nOptimizerFlow )
+        {
+        case 0:
+            Abc_Print( 2, "(0 = single-add resub)" );
+            break;
+        case 1:
+            Abc_Print( 2, "(1 = multi-add resub)" );
+            break;
+        case 2:
+            Abc_Print( 2, "(2 = repeat single-add and multi-add resubs)" );
+            break;
+        case 3:
+            Abc_Print( 2, "(3 = random one meaningful resub)" );
+            break;
+        }
+        Abc_Print( 2, "\n" );
+        Abc_Print( 2, "\t-Y %3d : flow ", nSchedulerFlow );
+        switch ( nSchedulerFlow )
+        {
+        case 0:
+            Abc_Print( 2, "(0 = apply method once)" );
+            break;
+        case 1:
+            Abc_Print( 2, "(1 = iterate like transtoch)" );
+            break;
+        case 2:
+            Abc_Print( 2, "(2 = iterate like deepsyn)" );
+            break;
+        }
+        Abc_Print( 2, "\n" );
+        Abc_Print( 2, "\t-N %3d : number of jobs to create by restarting or partitioning\n", nJobs );
+        Abc_Print( 2, "\t-J %3d : number of threads\n", nThreads );
+        Abc_Print( 2, "\t-K %3d : maximum partition size (0 = no partitioning)\n", nPartitionSize );
+        Abc_Print( 2, "\t-L %3d : minimum partition size\n", nPartitionSizeMin );
+        Abc_Print( 2, "\t-B %3d : maximum number of partitions to optimize in parallel\n", nParallelPartitions );
+        Abc_Print( 2, "\t-R %3d : random number generator seed\n", iSeed );
+        Abc_Print( 2, "\t-T %3d : timeout in seconds (0 = no timeout)\n", nTimeout );
+        Abc_Print( 2, "\t-C %3d : conflict limit (0 = no limit)\n", nConflictLimit );
+        Abc_Print( 2, "Use command line switch \"-h\" to see more options\n\n" );
+    }
+    
     pNew = Gia_ManRrr( pAbc->pGia, iSeed, nWords, nTimeout, nSchedulerVerbose, nPartitionerVerbose, nOptimizerVerbose, nAnalyzerVerbose, nSimulatorVerbose, nSatSolverVerbose, fUseBddCspf, fUseBddMspf, nConflictLimit, nSortType, nOptimizerFlow, nSchedulerFlow, nPartitionType, nDistance, nJobs, nThreads, nPartitionSize, nPartitionSizeMin, fDeterministic, nParallelPartitions, fOptOnInsert, fGreedy );
 
     Abc_FrameUpdateGia( pAbc, pNew );
@@ -46469,10 +46514,10 @@ usage:
       Abc_Print( -2, "\t                1: level base\n" );
       Abc_Print( -2, "\t-N num : number of jobs to create by restarting or partitioning [default = %d]\n", nJobs );
       Abc_Print( -2, "\t-J num : number of threads [default = %d]\n", nThreads );
-      Abc_Print( -2, "\t-K num : partition size (0 = no partitioning) [default = %d]\n", nPartitionSize );
+      Abc_Print( -2, "\t-K num : maximum partition size (0 = no partitioning) [default = %d]\n", nPartitionSize );
-      Abc_Print( -2, "\t-K num : minimum partition size [default = %d]\n", nPartitionSizeMin );
+      Abc_Print( -2, "\t-L num : minimum partition size [default = %d]\n", nPartitionSizeMin );
-      Abc_Print( -2, "\t-B num : max number of partitions in parallel [default = %d]\n", nParallelPartitions );
+      Abc_Print( -2, "\t-B num : maximum number of partitions in parallel [default = %d]\n", nParallelPartitions );
-      Abc_Print( -2, "\t-D num : distance between nodes (0 = no limit) [default = %d]\n", nDistance );
+      Abc_Print( -2, "\t-D num : maximum distance between node and new fanin (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 );
@@ -46487,7 +46532,7 @@ usage:
       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-e     : apply c2rs; dc2 after importing changes of partitions [default = %s]\n", fOptOnInsert? "yes": "no" );
+      Abc_Print( -2, "\t-e     : apply \"c2rs; dc2\" after importing changes of partitions [default = %s]\n", fOptOnInsert? "yes": "no" );
       Abc_Print( -2, "\t-g     : discard changes that increased the cost [default = %s]\n", fGreedy? "yes": "no" );
       Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;

src/opt/rrr/rrrAbc.h

@@ -29,9 +29,11 @@ namespace rrr {
   }
 
   template <typename Ntk>
-  Gia_Man_t *CreateGia(Ntk *pNtk) {
+  Gia_Man_t *CreateGia(Ntk *pNtk, bool fHash = true) {
     Gia_Man_t *pGia = Gia_ManStart(pNtk->GetNumNodes());
-    Gia_ManHashStart(pGia);
+    if(fHash) {
+      Gia_ManHashStart(pGia);
+    }
     std::vector<int> v(pNtk->GetNumNodes());
     v[0] = Gia_ManConst0Lit();
     pNtk->ForEachPi([&](int id) {
@@ -43,8 +45,10 @@ namespace rrr {
       pNtk->ForEachFanin(id, [&](int fi, bool c) {
         if(x == -1) {
           x = Abc_LitNotCond(v[fi], c);
-        } else {
+        } else if(fHash) {
           x = Gia_ManHashAnd(pGia, x, Abc_LitNotCond(v[fi], c));
+        } else {
+          x = Gia_ManAppendAnd(pGia, x, Abc_LitNotCond(v[fi], c));
         }
       });
       if(x == -1) {
@@ -55,7 +59,9 @@ namespace rrr {
     pNtk->ForEachPoDriver([&](int fi, bool c) {
       Gia_ManAppendCo(pGia, Abc_LitNotCond(v[fi], c));
     });
-    Gia_ManHashStop(pGia);
+    if(fHash) {
+      Gia_ManHashStop(pGia);
+    }
     return pGia;  
   }
 
@@ -72,7 +78,7 @@ namespace rrr {
       assert(r == 0);
       Abc_FrameSetBatchMode(0);
     }
-    pNtk->Read(Abc_FrameReadGia(pAbc), GiaReader<Ntk>);
+    pNtk->Read(Abc_FrameReadGia(pAbc), GiaReader<Ntk>, false);
   }
 
 }

src/opt/rrr/rrrAnalyzer.h

@@ -23,11 +23,16 @@ namespace rrr {
   public:
     // constructors
     Analyzer(Parameter const *pPar);
-    void UpdateNetwork(Ntk *pNtk_, bool fSame);
+    void AssignNetwork(Ntk *pNtk_, bool fReuse);
 
     // checks
     bool CheckRedundancy(int id, int idx);
     bool CheckFeasibility(int id, int fi, bool c);
+
+    // summary
+    void ResetSummary();
+    summary<int> GetStatsSummary() const;
+    summary<double> GetTimesSummary() const;
   };
 
   /* {{{ Constructors */
@@ -41,10 +46,10 @@ namespace rrr {
   }
 
   template <typename Ntk, typename Sim, typename Sol>
-  void Analyzer<Ntk, Sim, Sol>::UpdateNetwork(Ntk *pNtk_, bool fSame) {
+  void Analyzer<Ntk, Sim, Sol>::AssignNetwork(Ntk *pNtk_, bool fReuse) {
     pNtk = pNtk_;
-    sim.UpdateNetwork(pNtk, fSame);
+    sim.AssignNetwork(pNtk, fReuse);
-    sol.UpdateNetwork(pNtk, fSame);
+    sol.AssignNetwork(pNtk, fReuse);
   }
 
   /* }}} */
@@ -70,6 +75,10 @@ namespace rrr {
         }
         sim.AddCex(sol.GetCex());
       }
+    } else {
+      // if(nVerbose) {
+      //   std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is not redundant" << std::endl;
+      // }
     }
     return false;
   }
@@ -93,12 +102,42 @@ namespace rrr {
         }
         sim.AddCex(sol.GetCex());
       }
+    } else {
+      // if(nVerbose) {
+      //   std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is not feasible" << std::endl;
+      // }
     }
     return false;
   }
 
   /* }}} */
 
+  /* {{{ Summary */
+  
+  template <typename Ntk, typename Sim, typename Sol>
+  void Analyzer<Ntk, Sim, Sol>::ResetSummary() {
+    sim.ResetSummary();
+    sol.ResetSummary();
+  }
+  
+  template <typename Ntk, typename Sim, typename Sol>
+  summary<int> Analyzer<Ntk, Sim, Sol>::GetStatsSummary() const {
+    summary<int> v = sim.GetStatsSummary();
+    summary<int> v2 = sol.GetStatsSummary();
+    v.insert(v.end(), v2.begin(), v2.end());
+    return v;
+  }
+
+  template <typename Ntk, typename Sim, typename Sol>
+  summary<double> Analyzer<Ntk, Sim, Sol>::GetTimesSummary() const {
+    summary<double> v = sim.GetTimesSummary();
+    summary<double> v2 = sol.GetTimesSummary();
+    v.insert(v.end(), v2.begin(), v2.end());
+    return v;
+  }
+
+  /* }}} */
+  
 }
 
 ABC_NAMESPACE_CXX_HEADER_END

src/opt/rrr/rrrAndNetwork.h

@@ -64,13 +64,13 @@ namespace rrr {
     AndNetwork &operator=(AndNetwork const &x);
 
     // initialization APIs (should not be called after optimization has started)
-    void Clear();
+    void Clear(bool fClearCallbacks = true);
     void Reserve(int nReserve);
     int  AddPi();
     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);
+    void Read(Ntk *pFrom, Reader &reader, bool fNew = true);
 
     // network properties
     bool UseComplementedEdges() const;
@@ -78,6 +78,7 @@ namespace rrr {
     int  GetNumPis() const;
     int  GetNumInts() const;
     int  GetNumPos() const;
+    int  GetNumLevels() const;
     int  GetConst0() const;
     int  GetPi(int idx) const;
     int  GetPo(int idx) const;
@@ -272,7 +273,7 @@ namespace rrr {
 
   /* {{{ Initialization APIs */
 
-  void AndNetwork::Clear() {
+  void AndNetwork::Clear(bool fClearCallbacks) {
     nNodes = 0;
     vPis.clear();
     lInts.clear();
@@ -284,7 +285,9 @@ namespace rrr {
     iTrav = 0;
     vTrav.clear();
     fPropagating = false;
-    vCallbacks.clear();
+    if(fClearCallbacks) {
+      vCallbacks.clear();
+    }
     vBackups.clear();
     // add constant node
     vvFaninEdges.emplace_back();
@@ -330,9 +333,13 @@ namespace rrr {
   }
 
   template <typename Ntk, typename Reader>
-  void AndNetwork::Read(Ntk *pFrom, Reader &reader) {
+  void AndNetwork::Read(Ntk *pFrom, Reader &reader, bool fNew) {
-    Clear();
+    Clear(false);
     reader(pFrom, this);
+    Action action;
+    action.type = READ;
+    action.fNew = fNew;
+    TakenAction(action);
   }
   
   /* }}} */
@@ -359,6 +366,23 @@ namespace rrr {
     return int_size(vPos);
   }
 
+  int AndNetwork::GetNumLevels() const {
+    int nMaxLevel = 0;
+    std::vector<int> vLevels(nNodes);
+    ForEachInt([&](int id) {
+      ForEachFanin(id, [&](int fi) {
+        if(vLevels[id] < vLevels[fi]) {
+          vLevels[id] = vLevels[fi];
+        }
+      });
+      vLevels[id] += 1;
+      if(nMaxLevel < vLevels[id]) {
+        nMaxLevel = vLevels[id];
+      }
+    });
+    return nMaxLevel;
+  }
+
   inline int AndNetwork::GetConst0() const {
     return 0;
   }

src/opt/rrr/rrrBddAnalyzer.h

@@ -22,6 +22,7 @@ namespace rrr {
     int nVerbose;
     
     // data
+    bool fInitialized;
     NewBdd::Man *pBdd;
     int target;
     std::vector<lit> vFs;
@@ -35,6 +36,14 @@ namespace rrr {
     // backups
     std::vector<BddAnalyzer> vBackups;
 
+    // stats
+    uint64_t nNodesOld;
+    uint64_t nNodesAccumulated;
+    double durationSimulation;
+    double durationPf;
+    double durationCheck;
+    double durationReorder;
+
     // BDD utils
     void IncRef(lit x) const;
     void DecRef(lit x) const;
@@ -61,6 +70,10 @@ namespace rrr {
     void CspfNode(int id);
     void Cspf(int id = -1, bool fC = true);
 
+    // preparation
+    void Reset(bool fReuse = false);
+    void Initialize();
+
     // save & load
     void Save(int slot);
     void Load(int slot);
@@ -71,11 +84,16 @@ namespace rrr {
     BddAnalyzer();
     BddAnalyzer(Parameter const *pPar);
     ~BddAnalyzer();
-    void UpdateNetwork(Ntk *pNtk_, bool fSame);
+    void AssignNetwork(Ntk *pNtk_, bool fReuse);
 
     // checks
     bool CheckRedundancy(int id, int idx);
     bool CheckFeasibility(int id, int fi, bool c);
+
+    // summary
+    void ResetSummary();
+    summary<int> GetStatsSummary() const;
+    summary<double> GetTimesSummary() const;
   };
   
   /* {{{ BDD utils */
@@ -163,103 +181,136 @@ namespace rrr {
   void BddAnalyzer<Ntk>::ActionCallback(Action const &action) {
     switch(action.type) {
     case REMOVE_FANIN:
+      assert(fInitialized);
       vUpdates[action.id] = true;
       vGUpdates[action.fi] = true;
       DecRef(vvCs[action.id][action.idx]);
       vvCs[action.id].erase(vvCs[action.id].begin() + action.idx);
+      if(target != action.id) {
+        // require resimulate before next fesibility check
+        // (this is not mandatory if no pending updates are in TFI of new fanin, but we would rather update than checking every time)
+        target = -1;
+      }
       break;
     case REMOVE_UNUSED:
-      if(vGUpdates[action.id] || vCUpdates[action.id]) {
+      if(fInitialized) {
+        if(vGUpdates[action.id] || vCUpdates[action.id]) {
+          for(int fi: action.vFanins) {
+            vGUpdates[fi] = true;
+          }
+        }
+        Assign(vFs[action.id], LitMax);
+        Assign(vGs[action.id], LitMax);
+        DelVec(vvCs[action.id]);
+      }
+      break;
+    case REMOVE_BUFFER:
+      if(fInitialized) {
+        if(vUpdates[action.id]) {
+          for(int fo: action.vFanouts) {
+            vUpdates[fo] = true;
+            vCUpdates[fo] = true;
+          }
+        }
+        if(vGUpdates[action.id] || vCUpdates[action.id]) {
+          vGUpdates[action.fi] = true;
+        }
+        Assign(vFs[action.id], LitMax);
+        Assign(vGs[action.id], LitMax);
+        DelVec(vvCs[action.id]);
+      }
+      break;
+    case REMOVE_CONST:
+      if(fInitialized) {
+        if(vUpdates[action.id]) {
+          for(int fo: action.vFanouts) {
+            vUpdates[fo] = true;
+            vCUpdates[fo] = true;
+          }
+        }
         for(int fi: action.vFanins) {
           vGUpdates[fi] = true;
         }
+        Assign(vFs[action.id], LitMax);
+        Assign(vGs[action.id], LitMax);
+        DelVec(vvCs[action.id]);
       }
-      Assign(vFs[action.id], LitMax);
-      Assign(vGs[action.id], LitMax);
-      DelVec(vvCs[action.id]);
-      break;
-    case REMOVE_BUFFER:
-      if(vUpdates[action.id]) {
-        for(int fo: action.vFanouts) {
-          vUpdates[fo] = true;
-          vCUpdates[fo] = true;
-        }
-      }
-      if(vGUpdates[action.id] || vCUpdates[action.id]) {
-        vGUpdates[action.fi] = true;
-      }
-      Assign(vFs[action.id], LitMax);
-      Assign(vGs[action.id], LitMax);
-      DelVec(vvCs[action.id]);
-      break;
-    case REMOVE_CONST:
-      if(vUpdates[action.id]) {
-        for(int fo: action.vFanouts) {
-          vUpdates[fo] = true;
-          vCUpdates[fo] = true;
-        }
-      }
-      for(int fi: action.vFanins) {
-        vGUpdates[fi] = true;
-      }
-      Assign(vFs[action.id], LitMax);
-      Assign(vGs[action.id], LitMax);
-      DelVec(vvCs[action.id]);
       break;
     case ADD_FANIN:
+      assert(action.id == target);
+      assert(fInitialized);
       vUpdates[action.id] = true;
       vCUpdates[action.id] = true;
       vvCs[action.id].insert(vvCs[action.id].begin() + action.idx, LitMax);
       break;
-    case TRIVIAL_COLLAPSE: {
+    case TRIVIAL_COLLAPSE:
-      if(vGUpdates[action.fi] || vCUpdates[action.fi]) {
+      if(fInitialized) {
+        if(vGUpdates[action.fi] || vCUpdates[action.fi]) {
+          vCUpdates[action.id] = true;
+        }
+        std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
+        DecRef(*it);
+        it = vvCs[action.id].erase(it);
+        vvCs[action.id].insert(it,  vvCs[action.fi].begin(), vvCs[action.fi].end());
+        vvCs[action.fi].clear();
+        Assign(vFs[action.fi], LitMax);
+        Assign(vGs[action.fi], LitMax);
+      }
+      break;
+    case TRIVIAL_DECOMPOSE:
+      if(fInitialized) {
+        Allocate();
+        SimulateNode(action.fi, vFs);
+        // time of this simulation is not measured for simplicity sake
+        assert(vGs[action.fi] == LitMax);
+        Assign(vGs[action.fi], vGs[action.id]);
+        std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
+        assert(vvCs[action.fi].empty());
+        vvCs[action.fi].insert(vvCs[action.fi].begin(), it, vvCs[action.id].end());
+        vvCs[action.id].erase(it, vvCs[action.id].end());
+        assert(vvCs[action.id].size() == action.idx);
+        vvCs[action.id].resize(action.idx + 1, LitMax);
+        Assign(vvCs[action.id][action.idx], vGs[action.fi]);
+        vUpdates[action.fi] = false;
+        vGUpdates[action.fi] = false;
+        vCUpdates[action.fi] = vCUpdates[action.id];
+      }
+      break;
+    case SORT_FANINS:
+      if(fInitialized) {
+        std::vector<lit> vCs = vvCs[action.id];
+        vvCs[action.id].clear();
+        for(int index: action.vIndices) {
+          vvCs[action.id].push_back(vCs[index]);
+        }
+        if(!fResim) {
+          fResim = true;
+          /* commenting out the following because it might not be worth checking
+          // if sorted node is in TFO of functionally updated nodes, resimulation is required
+          std::vector<int> vFanouts;
+          pNtk->ForEachInt([&](int id) {
+            if(vUpdates[id]) {
+              pNtk->ForEachFanout(id, false, [&](int fo) {
+                vFanouts.push_back(fo);
+              });
+            }
+          });
+          pNtk->ForEachTfos(vFanouts, false, [&](int fo) {
+            if(fResim) {
+              return;
+            }
+            if(fo == action.id) {
+              fResim = true;
+            }
+          });
+          */
+        }
         vCUpdates[action.id] = true;
       }
-      std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
-      DecRef(*it);
-      it = vvCs[action.id].erase(it);
-      vvCs[action.id].insert(it,  vvCs[action.fi].begin(), vvCs[action.fi].end());
-      vvCs[action.fi].clear();
-      Assign(vFs[action.fi], LitMax);
-      Assign(vGs[action.fi], LitMax);
       break;
-    }
+    case READ:
-    case TRIVIAL_DECOMPOSE: {
+      Reset(!action.fNew);
-      Allocate();
-      SimulateNode(action.fi, vFs);
-      assert(vGs[action.fi] == LitMax);
-      Assign(vGs[action.fi], vGs[action.id]);
-      std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
-      assert(vvCs[action.fi].empty());
-      vvCs[action.fi].insert(vvCs[action.fi].begin(), it, vvCs[action.id].end());
-      vvCs[action.id].erase(it, vvCs[action.id].end());
-      assert(vvCs[action.id].size() == action.idx);
-      vvCs[action.id].resize(action.idx + 1, LitMax);
-      Assign(vvCs[action.id][action.idx], vGs[action.fi]);
-      vUpdates[action.fi] = false;
-      vGUpdates[action.fi] = false;
-      vCUpdates[action.fi] = vCUpdates[action.id];
       break;
-    }
-    case SORT_FANINS: {
-      std::vector<lit> vCs = vvCs[action.id];
-      vvCs[action.id].clear();
-      for(int index: action.vIndices) {
-        vvCs[action.id].push_back(vCs[index]);
-      }
-      if(!fResim && target != -1 && target != action.id) {
-        pNtk->ForEachTfo(target, false, [&](int fo) {
-          if(fResim) {
-            return;
-          }
-          if(fo == action.id) {
-            fResim = true;
-          }
-        });
-      }
-      vCUpdates[action.id] = true;
-      break;
-    }
     case SAVE:
       Save(action.idx);
       break;
@@ -306,6 +357,7 @@ namespace rrr {
   
   template <typename Ntk>
   void BddAnalyzer<Ntk>::Simulate() {
+    time_point timeStart = GetCurrentTime();
     if(nVerbose) {
       std::cout << "symbolic simulation with BDD" << std::endl;
     }
@@ -324,6 +376,7 @@ namespace rrr {
         vUpdates[id] = false;
       }
     });
+    durationSimulation += Duration(timeStart, GetCurrentTime());
   }
 
   /* }}} */
@@ -410,6 +463,7 @@ namespace rrr {
   
   template <typename Ntk>
   void BddAnalyzer<Ntk>::Cspf(int id, bool fC) {
+    time_point timeStart = GetCurrentTime();
     if(id != -1) {
       pNtk->ForEachTfoReverse(id, false, [&](int fo) {
         CspfNode(fo);
@@ -427,6 +481,78 @@ namespace rrr {
         CspfNode(id);
       });
     }
+    durationPf += Duration(timeStart, GetCurrentTime());
+  }
+
+  /* }}} */
+
+  /* {{{ Preparation */
+  
+  template <typename Ntk>
+  void BddAnalyzer<Ntk>::Reset(bool fReuse) {
+    while(!vBackups.empty()) {
+      PopBack();
+    }
+    DelVec(vFs);
+    DelVec(vGs);
+    DelVecVec(vvCs);
+    fInitialized = false;
+    target = -1;
+    fResim = false;
+    vUpdates.clear();
+    vGUpdates.clear();
+    vCUpdates.clear();
+    if(!fReuse) {
+      nNodesOld = 0;
+      if(pBdd) {
+        nNodesAccumulated += pBdd->GetNumTotalCreatedNodes();
+      }
+      delete pBdd;
+      pBdd = NULL;
+    }
+  }
+
+  template <typename Ntk>
+  void BddAnalyzer<Ntk>::Initialize() {
+    bool fUseReo = false;
+    if(!pBdd) {
+      NewBdd::Param Par;
+      Par.nObjsMaxLog = 25;
+      Par.nCacheMaxLog = 20;
+      Par.fCountOnes = false;
+      Par.nGbc = 1;
+      Par.nReo = 4000;
+      pBdd = new NewBdd::Man(pNtk->GetNumPis(), Par);
+      fUseReo = true;
+    }
+    assert(pBdd->GetNumVars() == pNtk->GetNumPis());
+    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();
+    if(fUseReo) {
+      time_point timeStart = GetCurrentTime();
+      pBdd->Reorder();
+      pBdd->TurnOffReo();
+      durationReorder += Duration(timeStart, GetCurrentTime());
+    }
+    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;
+    });
+    fInitialized = true;
   }
   
   /* }}} */
@@ -468,7 +594,7 @@ namespace rrr {
     vBackups.pop_back();
   }
 
-  /* }}} Save & load end */
+  /* }}} */
   
   /* {{{ Constructors */
 
@@ -476,93 +602,34 @@ namespace rrr {
   BddAnalyzer<Ntk>::BddAnalyzer() :
     pNtk(NULL),
     nVerbose(0),
+    fInitialized(false),
     pBdd(NULL),
     target(-1),
     fResim(false) {
+    ResetSummary();
   }
   
   template <typename Ntk>
   BddAnalyzer<Ntk>::BddAnalyzer(Parameter const *pPar) :
     pNtk(NULL),
     nVerbose(pPar->nAnalyzerVerbose),
+    fInitialized(false),
     pBdd(NULL),
     target(-1),
     fResim(false) {
-  }
+    ResetSummary();
-
-  template <typename Ntk>
-  void BddAnalyzer<Ntk>::UpdateNetwork(Ntk *pNtk_, bool fSame) {
-    // clear
-    while(!vBackups.empty()) {
-      PopBack();
-    }
-    DelVec(vFs);
-    DelVec(vGs);
-    DelVecVec(vvCs);
-    pNtk = pNtk_;
-    target = -1;
-    fResim = false;
-    vUpdates.clear();
-    vGUpdates.clear();
-    vCUpdates.clear();
-    // alloc
-    bool fUseReo = false;
-    if(!pBdd || pBdd->GetNumVars() != pNtk->GetNumPis()) {
-      // need to reset manager
-      delete pBdd;
-      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);
-      fUseReo = true;
-    } else if(!fSame) {
-      // turning on reordering if network function changed
-      pBdd->TurnOnReo();
-      fUseReo = true;
-    }
-    Allocate();
-    // prepare
-    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();
-    if(fUseReo) {
-      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>
   BddAnalyzer<Ntk>::~BddAnalyzer() {
-    while(!vBackups.empty()) {
+    Reset();
-      PopBack();
+  }
-    }
+
-    DelVec(vFs);
+  template <typename Ntk>
-    DelVec(vGs);
+  void BddAnalyzer<Ntk>::AssignNetwork(Ntk *pNtk_, bool fReuse) {
-    DelVecVec(vvCs);
+    Reset(fReuse);
-    if(pBdd) {
+    pNtk = pNtk_;
-      pBdd->PrintStats();
+    pNtk->AddCallback(std::bind(&BddAnalyzer<Ntk>::ActionCallback, this, std::placeholders::_1));
-    }
-    delete pBdd;
   }
 
   /* }}} */
@@ -571,20 +638,22 @@ namespace rrr {
   
   template <typename Ntk>
   bool BddAnalyzer<Ntk>::CheckRedundancy(int id, int idx) {
-    if(fResim) {
+    if(!fInitialized) {
+      Initialize();
+    } else if(fResim) {
       Simulate();
+      fResim = false;
     }
     Cspf(id);
+    time_point timeStart = GetCurrentTime();
+    bool fRedundant = false;
     switch(pNtk->GetNodeType(id)) {
     case AND: {
       int fi = pNtk->GetFanin(id, idx);
       bool c = pNtk->GetCompl(id, idx);
       lit x = pBdd->Or(pBdd->LitNotCond(vFs[fi], c), vvCs[id][idx]);
       if(pBdd->IsConst1(x)) {
-        if(nVerbose) {
+        fRedundant = true;
-          std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is redundant" << std::endl;
-        }
-        return true;
       }
       break;
     }
@@ -592,18 +661,30 @@ namespace rrr {
       assert(0);
     }
     if(nVerbose) {
-      std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is NOT redundant" << std::endl;
+      if(fRedundant) {
+        std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is redundant" << std::endl;
+      } else {
+        std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is NOT redundant" << std::endl;
+      }
     }
-    return false;
+    durationCheck += Duration(timeStart, GetCurrentTime());
+    return fRedundant;
   }
   
   template <typename Ntk>
   bool BddAnalyzer<Ntk>::CheckFeasibility(int id, int fi, bool c) {
-    if(target != id) { // simualte if there has been update in non-tfo of this node
+    if(!fInitialized) {
+      Initialize();
+    } else if(target != id && (target == -1 || vUpdates[target])) {
+      // resimulation is required if there are pending updates in TFI of new fanin
+      // but it seems not worthwhile to check that condition every time
+      // so we update if pending updates are not only at current target
       Simulate();
-      target = id;
     }
+    target = id;
     Cspf(id, false);
+    time_point timeStart = GetCurrentTime();
+    bool fFeasible = false;
     switch(pNtk->GetNodeType(id)) {
     case AND: {
       lit x = pBdd->Or(pBdd->LitNot(vFs[id]), vGs[id]);
@@ -611,10 +692,7 @@ namespace rrr {
       lit y = pBdd->Or(x, pBdd->LitNotCond(vFs[fi], c));
       DecRef(x);
       if(pBdd->IsConst1(y)) {
-        if(nVerbose) {
+        fFeasible = true;
-          std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is feasible" << std::endl;
-        }
-        return true;
       }
       break;
     }
@@ -622,9 +700,49 @@ namespace rrr {
       assert(0);
     }
     if(nVerbose) {
-      std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is NOT feasible" << std::endl;
+      if(fFeasible) {
+        std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is feasible" << std::endl;
+      } else {
+        std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is NOT feasible" << std::endl;
+      }
     }
-    return false;
+    durationCheck += Duration(timeStart, GetCurrentTime());
+    return fFeasible;
+  }
+
+  /* }}} */
+
+  /* {{{ Summary */
+
+  template <typename Ntk>
+  void BddAnalyzer<Ntk>::ResetSummary() {
+    if(pBdd) {
+      nNodesOld = pBdd->GetNumTotalCreatedNodes();
+    } else {
+      nNodesOld = 0;
+    }
+    nNodesAccumulated = 0;
+    durationSimulation = 0;
+    durationPf = 0;
+    durationCheck = 0;
+    durationReorder = 0;
+  }
+  
+  template <typename Ntk>
+  summary<int> BddAnalyzer<Ntk>::GetStatsSummary() const {
+    summary<int> v;
+    v.emplace_back("bdd node", pBdd->GetNumTotalCreatedNodes() - nNodesOld + nNodesAccumulated);
+    return v;
+  }
+  
+  template <typename Ntk>
+  summary<double> BddAnalyzer<Ntk>::GetTimesSummary() const {
+    summary<double> v;
+    v.emplace_back("bdd symbolic simulation", durationSimulation);
+    v.emplace_back("bdd care computation", durationPf);
+    v.emplace_back("bdd check", durationCheck);
+    v.emplace_back("bdd reorder", durationReorder);
+    return v;
   }
 
   /* }}} */

src/opt/rrr/rrrBddManager.h

@@ -181,6 +181,7 @@ namespace NewBdd {
     bvar   nObjs;
     bvar   nObjsAlloc;
     bvar   nObjsMax;
+    unsigned long long nCreatedTotal;
     bvar   RemovedHead;
     int    nGbc;
     bvar   nReo;
@@ -396,6 +397,7 @@ namespace NewBdd {
       for(; *q; q = vNexts.begin() + *q)
         if(VarOfBvar(*q) == v && ThenOfBvar(*q) == x1 && ElseOfBvar(*q) == x0)
           return Bvar2Lit(*q);
+      nCreatedTotal++;
       bvar next = *p;
       if(nObjs < nObjsAlloc)
         *p = nObjs++;
@@ -642,6 +644,7 @@ namespace NewBdd {
 
   public:
     Man(int nVars_, Param p) {
+      nCreatedTotal = 0;
       nVerbose = p.nVerbose;
       // parameter sanity check
       if(p.nObjsMaxLog < p.nObjsAllocLog)
@@ -840,6 +843,9 @@ namespace NewBdd {
                 << "alloc: " << std::setw(10) << nObjsAlloc
                 << std::endl;
     }
+    unsigned long long GetNumTotalCreatedNodes() {
+      return nCreatedTotal;
+    }
   };
 
 }

src/opt/rrr/rrrBddMspfAnalyzer.h

@@ -22,6 +22,7 @@ namespace rrr {
     int nVerbose;
     
     // data
+    bool fInitialized;
     NewBdd::Man *pBdd;
     std::vector<lit> vFs;
     std::vector<lit> vGs;
@@ -35,6 +36,14 @@ namespace rrr {
     // backups
     std::vector<BddMspfAnalyzer> vBackups;
 
+    // stats
+    uint64_t nNodesOld;
+    uint64_t nNodesAccumulated;
+    double durationSimulation;
+    double durationPf;
+    double durationCheck;
+    double durationReorder;
+    
     // BDD utils
     void IncRef(lit x) const;
     void DecRef(lit x) const;
@@ -63,6 +72,10 @@ namespace rrr {
     void MspfNode(int id);
     void Mspf(int id = -1, bool fC = true);
 
+    // preparation
+    void Reset(bool fReuse = false);
+    void Initialize();
+
     // save & load
     void Save(int slot);
     void Load(int slot);
@@ -73,11 +86,16 @@ namespace rrr {
     BddMspfAnalyzer();
     BddMspfAnalyzer(Parameter const *pPar);
     ~BddMspfAnalyzer();
-    void UpdateNetwork(Ntk *pNtk_, bool fSame);
+    void AssignNetwork(Ntk *pNtk_, bool fReuse);
 
     // checks
     bool CheckRedundancy(int id, int idx);
     bool CheckFeasibility(int id, int fi, bool c);
+    
+    // summary
+    void ResetSummary();
+    summary<int> GetStatsSummary() const;
+    summary<double> GetTimesSummary() const;
   };
   
   /* {{{ BDD utils */
@@ -165,6 +183,7 @@ namespace rrr {
   void BddMspfAnalyzer<Ntk>::ActionCallback(Action const &action) {
     switch(action.type) {
     case REMOVE_FANIN:
+      assert(fInitialized);
       fUpdate = true;
       std::fill(vVisits.begin(), vVisits.end(), false);
       vUpdates[action.id] = true;
@@ -174,103 +193,117 @@ namespace rrr {
       vvCs[action.id].erase(vvCs[action.id].begin() + action.idx);
       break;
     case REMOVE_UNUSED:
-      if(vGUpdates[action.id] || vCUpdates[action.id]) {
+      if(fInitialized) {
+        if(vGUpdates[action.id] || vCUpdates[action.id]) {
+          for(int fi: action.vFanins) {
+            vGUpdates[fi] = true;
+          }
+        }
+        Assign(vGs[action.id], LitMax);
+        DelVec(vvCs[action.id]);
+      }
+      break;
+    case REMOVE_BUFFER:
+      if(fInitialized) {
+        if(vUpdates[action.id]) {
+          fUpdate = true;
+          for(int fo: action.vFanouts) {
+            vUpdates[fo] = true;
+            vCUpdates[fo] = true;
+          }
+        }
+        if(vGUpdates[action.id] || vCUpdates[action.id]) {
+          vGUpdates[action.fi] = true;
+        }
+        Assign(vGs[action.id], LitMax);
+        DelVec(vvCs[action.id]);
+      }
+      break;
+    case REMOVE_CONST:
+      if(fInitialized) {
+        if(vUpdates[action.id]) {
+          fUpdate = true;
+          for(int fo: action.vFanouts) {
+            vUpdates[fo] = true;
+            vCUpdates[fo] = true;
+          }
+        }
         for(int fi: action.vFanins) {
           vGUpdates[fi] = true;
         }
       }
-      Assign(vGs[action.id], LitMax);
-      DelVec(vvCs[action.id]);
-      break;
-    case REMOVE_BUFFER:
-      if(vUpdates[action.id]) {
-        fUpdate = true;
-        for(int fo: action.vFanouts) {
-          vUpdates[fo] = true;
-          vCUpdates[fo] = true;
-        }
-      }
-      if(vGUpdates[action.id] || vCUpdates[action.id]) {
-        vGUpdates[action.fi] = true;
-      }
-      Assign(vGs[action.id], LitMax);
-      DelVec(vvCs[action.id]);
-      break;
-    case REMOVE_CONST:
-      if(vUpdates[action.id]) {
-        fUpdate = true;
-        for(int fo: action.vFanouts) {
-          vUpdates[fo] = true;
-          vCUpdates[fo] = true;
-        }
-      }
-      for(int fi: action.vFanins) {
-        vGUpdates[fi] = true;
-      }
       break;
     case ADD_FANIN:
+      assert(fInitialized);
       fUpdate = true;
       std::fill(vVisits.begin(), vVisits.end(), false);
       vUpdates[action.id] = true;
       vCUpdates[action.id] = true;
       vvCs[action.id].insert(vvCs[action.id].begin() + action.idx, LitMax);
       break;
-    case TRIVIAL_COLLAPSE: {
+    case TRIVIAL_COLLAPSE:
-      if(vGUpdates[action.fi] || vCUpdates[action.fi]) {
+      if(fInitialized) {
-        vCUpdates[action.id] = true;
+        if(vGUpdates[action.fi] || vCUpdates[action.fi]) {
-      }
+          vCUpdates[action.id] = true;
-      std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
-      DecRef(*it);
-      it = vvCs[action.id].erase(it);
-      vvCs[action.id].insert(it,  vvCs[action.fi].begin(), vvCs[action.fi].end());
-      vvCs[action.fi].clear();
-      Assign(vFs[action.fi], LitMax);
-      Assign(vGs[action.fi], LitMax);
-      break;
-    }
-    case TRIVIAL_DECOMPOSE: {
-      Allocate();
-      SimulateNode(action.fi, vFs);
-      assert(vGs[action.fi] == LitMax);
-      std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
-      assert(vvCs[action.fi].empty());
-      vvCs[action.fi].insert(vvCs[action.fi].begin(), it, vvCs[action.id].end());
-      vvCs[action.id].erase(it, vvCs[action.id].end());
-      assert(vvCs[action.id].size() == action.idx);
-      if(!vGUpdates[action.id] && !vCUpdates[action.id]) {
-        // recompute here only when updates are unlikely to happen
-        if(pBdd->IsConst1(vGs[action.id])) {
-          Assign(vGs[action.fi], pBdd->Const1());
-        } else {
-          lit x = pBdd->Const1();
-          IncRef(x);
-          for(int idx2 = 0; idx2 < action.idx; idx2++) {
-            int fi = pNtk->GetFanin(action.id, idx2);
-            bool c = pNtk->GetCompl(action.id, idx2);
-            Assign(x, pBdd->And(x, pBdd->LitNotCond(vFs[fi], c)));
-          }
-          Assign(vGs[action.fi], pBdd->Or(pBdd->LitNot(x), vGs[action.id]));
-          DecRef(x);
         }
-      } else {
+        std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
-        // otherwise mark the node for future update
+        DecRef(*it);
-        vCUpdates[action.id] = true;
+        it = vvCs[action.id].erase(it);
-      }
+        vvCs[action.id].insert(it,  vvCs[action.fi].begin(), vvCs[action.fi].end());
-      vvCs[action.id].resize(action.idx + 1, LitMax);
+        vvCs[action.fi].clear();
-      Assign(vvCs[action.id][action.idx], vGs[action.fi]);
+        Assign(vFs[action.fi], LitMax);
-      vUpdates[action.fi] = false;
+        Assign(vGs[action.fi], LitMax);
-      vGUpdates[action.fi] = false;
-      vCUpdates[action.fi] = false;
-      break;
-    }
-    case SORT_FANINS: {
-      std::vector<lit> vCs = vvCs[action.id];
-      vvCs[action.id].clear();
-      for(int index: action.vIndices) {
-        vvCs[action.id].push_back(vCs[index]);
       }
       break;
-    }
+    case TRIVIAL_DECOMPOSE:
+      if(fInitialized) {
+        Allocate();
+        SimulateNode(action.fi, vFs);
+        // time of this simulation is not measured for simplicity sake
+        assert(vGs[action.fi] == LitMax);
+        std::vector<lit>::iterator it = vvCs[action.id].begin() + action.idx;
+        assert(vvCs[action.fi].empty());
+        vvCs[action.fi].insert(vvCs[action.fi].begin(), it, vvCs[action.id].end());
+        vvCs[action.id].erase(it, vvCs[action.id].end());
+        assert(vvCs[action.id].size() == action.idx);
+        if(!vGUpdates[action.id] && !vCUpdates[action.id]) {
+          // recompute here only when updates are unlikely to happen
+          if(pBdd->IsConst1(vGs[action.id])) {
+            Assign(vGs[action.fi], pBdd->Const1());
+          } else {
+            lit x = pBdd->Const1();
+            IncRef(x);
+            for(int idx2 = 0; idx2 < action.idx; idx2++) {
+              int fi = pNtk->GetFanin(action.id, idx2);
+              bool c = pNtk->GetCompl(action.id, idx2);
+              Assign(x, pBdd->And(x, pBdd->LitNotCond(vFs[fi], c)));
+            }
+            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]);
+        vUpdates[action.fi] = false;
+        vGUpdates[action.fi] = false;
+        vCUpdates[action.fi] = false;
+      }
+      break;
+    case SORT_FANINS:
+      if(fInitialized) {
+        std::vector<lit> vCs = vvCs[action.id];
+        vvCs[action.id].clear();
+        for(int index: action.vIndices) {
+          vvCs[action.id].push_back(vCs[index]);
+        }
+      }
+      break;
+    case READ:
+      Reset(!action.fNew);
+      break;
     case SAVE:
       Save(action.idx);
       break;
@@ -326,6 +359,7 @@ namespace rrr {
   
   template <typename Ntk>
   void BddMspfAnalyzer<Ntk>::Simulate() {
+    time_point timeStart = GetCurrentTime();
     if(nVerbose) {
       std::cout << "symbolic simulation with BDD" << std::endl;
     }
@@ -340,6 +374,7 @@ namespace rrr {
         vUpdates[id] = false;
       }
     });
+    durationSimulation += Duration(timeStart, GetCurrentTime());
   }
 
   /* }}} */
@@ -507,6 +542,7 @@ namespace rrr {
 
   template <typename pNtk>
   void BddMspfAnalyzer<pNtk>::Mspf(int id, bool fC) {
+    time_point timeStart = GetCurrentTime();
     if(id != -1) {
       pNtk->ForEachTfoReverse(id, false, [&](int fo) {
         MspfNode(fo);
@@ -524,6 +560,78 @@ namespace rrr {
         MspfNode(id);
       });
     }
+    durationPf += Duration(timeStart, GetCurrentTime());
+  }
+
+  /* }}} */
+
+  /* {{{ Preparation */
+
+  template <typename Ntk>
+  void BddMspfAnalyzer<Ntk>::Reset(bool fReuse) {
+    while(!vBackups.empty()) {
+      PopBack();
+    }
+    DelVec(vFs);
+    DelVec(vGs);
+    DelVecVec(vvCs);
+    fInitialized = false;
+    fUpdate = false;
+    vUpdates.clear();
+    vGUpdates.clear();
+    vCUpdates.clear();
+    vVisits.clear();
+    if(!fReuse) {
+      nNodesOld = 0;
+      if(pBdd) {
+        nNodesAccumulated += pBdd->GetNumTotalCreatedNodes();
+      }
+      delete pBdd;
+      pBdd = NULL;
+    }
+  }
+
+  template <typename Ntk>
+  void BddMspfAnalyzer<Ntk>::Initialize() {
+    bool fUseReo = false;
+    if(!pBdd) {
+      NewBdd::Param Par;
+      Par.nObjsMaxLog = 25;
+      Par.nCacheMaxLog = 20;
+      Par.fCountOnes = false;
+      Par.nGbc = 1;
+      Par.nReo = 4000;
+      pBdd = new NewBdd::Man(pNtk->GetNumPis(), Par);
+      fUseReo = true;
+    }
+    assert(pBdd->GetNumVars() == pNtk->GetNumPis());
+    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();
+    if(fUseReo) {
+      time_point timeStart = GetCurrentTime();
+      pBdd->Reorder();
+      pBdd->TurnOffReo();
+      durationReorder += Duration(timeStart, GetCurrentTime());
+    }
+    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;
+    });
+    fInitialized = true;
   }
 
   /* }}} */
@@ -575,90 +683,32 @@ namespace rrr {
   BddMspfAnalyzer<Ntk>::BddMspfAnalyzer() :
     pNtk(NULL),
     nVerbose(0),
-    pBdd(NULL) {
+    fInitialized(false),
+    pBdd(NULL),
+    fUpdate(false) {
+    ResetSummary();
   }
   
   template <typename Ntk>
   BddMspfAnalyzer<Ntk>::BddMspfAnalyzer(Parameter const *pPar) :
     pNtk(NULL),
     nVerbose(pPar->nAnalyzerVerbose),
+    fInitialized(false),
     pBdd(NULL),
     fUpdate(false) {
-  }
+    ResetSummary();
-
-  template <typename Ntk>
-  void BddMspfAnalyzer<Ntk>::UpdateNetwork(Ntk *pNtk_, bool fSame) {
-    // clear
-    while(!vBackups.empty()) {
-      PopBack();
-    }
-    DelVec(vFs);
-    DelVec(vGs);
-    DelVecVec(vvCs);
-    pNtk = pNtk_;
-    fUpdate = false;
-    vUpdates.clear();
-    vGUpdates.clear();
-    vCUpdates.clear();
-    vVisits.clear();
-    // alloc
-    bool fUseReo = false;
-    if(!pBdd || pBdd->GetNumVars() != pNtk->GetNumPis()) {
-      // need to reset manager
-      delete pBdd;
-      NewBdd::Param Par;
-      Par.nObjsMaxLog = 25;
-      Par.nCacheMaxLog = 20;
-      Par.fCountOnes = false;
-      Par.nGbc = 1;
-      Par.nReo = 4000;
-      pBdd = new NewBdd::Man(pNtk->GetNumPis(), Par);
-      fUseReo = true;
-    } else if(!fSame) {
-      // turning on reordering if network function changed
-      pBdd->TurnOnReo();
-      fUseReo = true;
-    }
-    Allocate();
-    // prepare
-    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();
-    if(fUseReo) {
-      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>
   BddMspfAnalyzer<Ntk>::~BddMspfAnalyzer() {
-    while(!vBackups.empty()) {
+    Reset();
-      PopBack();
+  }
-    }
+
-    DelVec(vFs);
+  template <typename Ntk>
-    DelVec(vGs);
+  void BddMspfAnalyzer<Ntk>::AssignNetwork(Ntk *pNtk_, bool fReuse) {
-    DelVecVec(vvCs);
+    Reset(fReuse);
-    if(pBdd) {
+    pNtk = pNtk_;
-      pBdd->PrintStats();
+    pNtk->AddCallback(std::bind(&BddMspfAnalyzer<Ntk>::ActionCallback, this, std::placeholders::_1));
-    }
-    delete pBdd;
   }
   
   /* }}} */
@@ -667,21 +717,22 @@ namespace rrr {
   
   template <typename Ntk>
   bool BddMspfAnalyzer<Ntk>::CheckRedundancy(int id, int idx) {
-    if(fUpdate) {
+    if(!fInitialized) {
+      Initialize();
+    } else if(fUpdate) {
       Simulate();
       fUpdate = false;
     }
     Mspf(id);
+    time_point timeStart = GetCurrentTime();
+    bool fRedundant = false;
     switch(pNtk->GetNodeType(id)) {
     case AND: {
       int fi = pNtk->GetFanin(id, idx);
       bool c = pNtk->GetCompl(id, idx);
       lit x = pBdd->Or(pBdd->LitNotCond(vFs[fi], c), vvCs[id][idx]);
       if(pBdd->IsConst1(x)) {
-        if(nVerbose) {
+        fRedundant = true;
-          std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is redundant" << std::endl;
-        }
-        return true;
       }
       break;
     }
@@ -689,18 +740,27 @@ namespace rrr {
       assert(0);
     }
     if(nVerbose) {
-      std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is NOT redundant" << std::endl;
+      if(fRedundant) {
+        std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is redundant" << std::endl;
+      } else {
+        std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is NOT redundant" << std::endl;
+      }
     }
-    return false;
+    durationCheck += Duration(timeStart, GetCurrentTime());
+    return fRedundant;
   }
   
   template <typename Ntk>
   bool BddMspfAnalyzer<Ntk>::CheckFeasibility(int id, int fi, bool c) {
-    if(fUpdate) {
+    if(!fInitialized) {
+      Initialize();
+    } else if(fUpdate) {
       Simulate();
       fUpdate = false;
     }
     Mspf(id, false);
+    time_point timeStart = GetCurrentTime();
+    bool fFeasible = false;
     switch(pNtk->GetNodeType(id)) {
     case AND: {
       lit x = pBdd->Or(pBdd->LitNot(vFs[id]), vGs[id]);
@@ -708,9 +768,7 @@ namespace rrr {
       lit y = pBdd->Or(x, pBdd->LitNotCond(vFs[fi], c));
       DecRef(x);
       if(pBdd->IsConst1(y)) {
-        if(nVerbose) {
+        fFeasible = true;
-          std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is feasible" << std::endl;
-        }
         return true;
       }
       break;
@@ -719,9 +777,49 @@ namespace rrr {
       assert(0);
     }
     if(nVerbose) {
-      std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is NOT feasible" << std::endl;
+      if(fFeasible) {
+        std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is feasible" << std::endl;
+      } else {
+        std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is NOT feasible" << std::endl;
+      }
     }
-    return false;
+    durationCheck += Duration(timeStart, GetCurrentTime());
+    return fFeasible;
+  }
+
+  /* }}} */
+  
+  /* {{{ Summary */
+
+  template <typename Ntk>
+  void BddMspfAnalyzer<Ntk>::ResetSummary() {
+    if(pBdd) {
+      nNodesOld = pBdd->GetNumTotalCreatedNodes();
+    } else {
+      nNodesOld = 0;
+    }
+    nNodesAccumulated = 0;
+    durationSimulation = 0;
+    durationPf = 0;
+    durationCheck = 0;
+    durationReorder = 0;
+  }
+  
+  template <typename Ntk>
+  summary<int> BddMspfAnalyzer<Ntk>::GetStatsSummary() const {
+    summary<int> v;
+    v.emplace_back("bdd node", pBdd->GetNumTotalCreatedNodes() - nNodesOld + nNodesAccumulated);
+    return v;
+  }
+  
+  template <typename Ntk>
+  summary<double> BddMspfAnalyzer<Ntk>::GetTimesSummary() const {
+    summary<double> v;
+    v.emplace_back("bdd symbolic simulation", durationSimulation);
+    v.emplace_back("bdd care computation", durationPf);
+    v.emplace_back("bdd check", durationCheck);
+    v.emplace_back("bdd reorder", durationReorder);
+    return v;
   }
 
   /* }}} */

src/opt/rrr/rrrLevelBasePartitioner.h

@@ -43,7 +43,7 @@ namespace rrr {
   public:
     // constructors
     LevelBasePartitioner(Parameter const *pPar);
-    void UpdateNetwork(Ntk *pNtk);
+    void AssignNetwork(Ntk *pNtk);
 
     // APIs
     Ntk *Extract(int iSeed);
@@ -214,7 +214,7 @@ namespace rrr {
   }
 
   template <typename Ntk>
-  void LevelBasePartitioner<Ntk>::UpdateNetwork(Ntk *pNtk_) {
+  void LevelBasePartitioner<Ntk>::AssignNetwork(Ntk *pNtk_) {
     pNtk = pNtk_;
     assert(mSubNtk2Io.empty());
     assert(sBlocked.empty());

src/opt/rrr/rrrOptimizer.h

@@ -35,7 +35,7 @@ namespace rrr {
     bool fCompatible;
     bool fGreedy;
     seconds nTimeout; // assigned upon Run
-    std::string strVerbosePrefix;
+    std::function<void(std::string)> PrintLine;
 
     // data
     Ana ana;
@@ -52,6 +52,11 @@ namespace rrr {
     int target;
     std::vector<bool> vTfoMarks;
 
+    // statistics
+    struct Stats;
+    std::map<std::string, Stats> stats;
+    Stats statsLocal;
+
     // print
     template<typename... Args>
     void Print(int nVerboseLevel, Args... args);
@@ -76,17 +81,18 @@ namespace rrr {
     bool ReduceFaninsOneRandom(int id, bool fRemoveUnused = false);
 
     // reduce
-    bool Reduce();
+    bool Reduce(bool fSubRoutine = false);
     void ReduceRandom();
 
     // remove redundancy
-    void RemoveRedundancy();
+    bool RemoveRedundancy();
     void RemoveRedundancyRandom();
 
     // addition
     template <typename T>
     T SingleAdd(int id, T begin, T end);
     int  MultiAdd(int id, std::vector<int> const &vCands, int nMax = 0);
+    void Undo();
 
     // resub
     void SingleResub(int id, std::vector<int> const &vCands);
@@ -108,25 +114,81 @@ namespace rrr {
   public:
     // constructors
     Optimizer(Parameter const *pPar, std::function<double(Ntk *)> CostFunction);
-    void UpdateNetwork(Ntk *pNtk_, bool fSame = false);
+    void AssignNetwork(Ntk *pNtk_, bool fReuse = false);
+    void SetPrintLine(std::function<void(std::string)> const &PrintLine_);
 
     // run
     void Run(int iSeed = 0, seconds nTimeout_ = 0);
 
+    // summary
+    void ResetSummary();
+    summary<int> GetStatsSummary() const;
+    summary<double> GetTimesSummary() const;
   };
 
+  /* {{{ Stats */
+  
+  template <typename Ntk, typename Ana>
+  struct Optimizer<Ntk, Ana>::Stats {
+    int nTriedFis = 0;
+    int nAddedFis = 0;
+    int nTried = 0;
+    int nAdded = 0;
+    int nChanged = 0;
+    int nUps = 0;
+    int nEqs = 0;
+    int nDowns = 0;
+    double durationAdd = 0;
+    double durationReduce = 0;
+
+    void Reset() {
+      nTriedFis = 0;
+      nAddedFis = 0;
+      nTried = 0;
+      nAdded = 0;
+      nChanged = 0;
+      nUps = 0;
+      nEqs = 0;
+      nDowns = 0;
+      durationAdd = 0;
+      durationReduce = 0;
+    }
+
+    Stats& operator+=(Stats const &other) {
+      this->nTriedFis += other.nTriedFis;
+      this->nAddedFis += other.nAddedFis;
+      this->nTried    += other.nTried;
+      this->nAdded    += other.nAdded;
+      this->nChanged  += other.nChanged;
+      this->nUps      += other.nUps;
+      this->nEqs      += other.nEqs;
+      this->nDowns    += other.nDowns;
+      this->durationAdd    += other.durationAdd;
+      this->durationReduce += other.durationReduce;
+      return *this;
+    }
+
+    std::string GetString() const {
+      std::stringstream ss;
+      PrintNext(ss, "tried node/fanin", "=", nTried, "/", nTriedFis, ",", "added node/fanin", "=", nAdded, "/", nAddedFis, ",", "changed", "=", nChanged, ",", "up/eq/dn", "=", nUps, "/", nEqs, "/", nDowns);
+      return ss.str();
+    }
+  };
+  
+  /* }}} */
+
   /* {{{ Print */
 
   template <typename Ntk, typename Ana>
   template <typename... Args>
   inline void Optimizer<Ntk, Ana>::Print(int nVerboseLevel, Args... args) {
     if(nVerbose > nVerboseLevel) {
-      std::cout << strVerbosePrefix;
+      std::stringstream ss;
       for(int i = 0; i < nVerboseLevel; i++) {
-        std::cout << "\t";
+        ss << "\t";
       }
-      PrintNext(std::cout, args...);
+      PrintNext(ss, args...);
-      std::cout << std::endl;
+      PrintLine(ss.str());
     }
   }
   
@@ -136,13 +198,13 @@ namespace rrr {
   
   template <typename Ntk, typename Ana>
   void Optimizer<Ntk, Ana>::ActionCallback(Action const &action) {
-    if(nVerbose > 2) {
+    if(nVerbose > 4) {
       std::stringstream ss = GetActionDescription(action);
       std::string str;
       std::getline(ss, str);
-      Print(2, str);
+      Print(4, str);
       while(std::getline(ss, str)) {
-        Print(3, str);
+        Print(5, str);
       }
     }
     switch(action.type) {
@@ -171,6 +233,9 @@ namespace rrr {
       break;
     case SORT_FANINS:
       break;
+    case READ:
+      target = -1;
+      break;
     case SAVE:
       break;
     case LOAD:
@@ -482,7 +547,7 @@ namespace rrr {
   template <typename Ntk, typename Ana>
   inline bool Optimizer<Ntk, Ana>::ReduceFanins(int id, bool fRemoveUnused) {
     assert(pNtk->GetNumFanouts(id) > 0);
-    bool fRemoved = false;
+    bool fReduced = false;
     for(int idx = 0; idx < pNtk->GetNumFanins(id); idx++) {
       // skip fanins that were just added
       if(mapNewFanins.count(id)) {
@@ -495,14 +560,14 @@ namespace rrr {
       if(ana.CheckRedundancy(id, idx)) {
         int fi = pNtk->GetFanin(id, idx);
         pNtk->RemoveFanin(id, idx);
-        fRemoved = true;
+        fReduced = true;
         idx--;
         if(fRemoveUnused && pNtk->GetNumFanouts(fi) == 0) {
           pNtk->RemoveUnused(fi, true);
         }
       }
     }
-    return fRemoved;
+    return fReduced;
   }
 
   /*
@@ -542,7 +607,8 @@ namespace rrr {
   /* {{{ Reduce */
 
   template <typename Ntk, typename Ana>
-  bool Optimizer<Ntk, Ana>::Reduce() {
+  bool Optimizer<Ntk, Ana>::Reduce(bool fSubRoutine) {
+    time_point timeStart = GetCurrentTime();
     bool fReduced = false;
     std::vector<int> vInts = pNtk->GetInts();
     for(critr it = vInts.rbegin(); it != vInts.rend(); it++) {
@@ -558,6 +624,10 @@ namespace rrr {
         pNtk->Propagate(*it);
       }
     }
+    if(!fSubRoutine) {
+      time_point timeEnd = GetCurrentTime();
+      statsLocal.durationReduce += Duration(timeStart, timeEnd);
+    }
     return fReduced;
   }
 
@@ -588,35 +658,42 @@ namespace rrr {
   /* {{{ Redundancy removal */
   
   template <typename Ntk, typename Ana>
-  void Optimizer<Ntk, Ana>::RemoveRedundancy() {
+  bool Optimizer<Ntk, Ana>::RemoveRedundancy() {
+    time_point timeStart = GetCurrentTime();
+    bool fReduced = false;
     if(fCompatible) {
-      while(Reduce()) {
+      while(Reduce(true)) {
+        fReduced = true;
         SortFanins();
       }
-      return;
+    } else {
-    }
+      std::vector<int> vInts = pNtk->GetInts();
-    std::vector<int> vInts = pNtk->GetInts();
+      for(critr it = vInts.rbegin(); it != vInts.rend();) {
-    for(critr it = vInts.rbegin(); it != vInts.rend();) {
+        if(!pNtk->IsInt(*it)) {
-      if(!pNtk->IsInt(*it)) {
+          it++;
-        it++;
+          continue;
-        continue;
+        }
-      }
+        if(pNtk->GetNumFanouts(*it) == 0) {
-      if(pNtk->GetNumFanouts(*it) == 0) {
+          pNtk->RemoveUnused(*it);
-        pNtk->RemoveUnused(*it);
+          it++;
-        it++;
+          continue;
-        continue;
+        }
-      }
+        SortFanins(*it);
-      SortFanins(*it);
+        bool fReduced_ = ReduceFanins(*it);
-      bool fReduced = ReduceFanins(*it);
+        fReduced |= fReduced_;
-      if(pNtk->GetNumFanins(*it) <= 1) {
+        if(pNtk->GetNumFanins(*it) <= 1) {
-        pNtk->Propagate(*it);
+          pNtk->Propagate(*it);
-      }
+        }
-      if(fReduced) {
+        if(fReduced_) {
-        it = vInts.rbegin();
+          it = vInts.rbegin();
-      } else {
+        } else {
-        it++;
+          it++;
+        }
       }
     }
+    time_point timeEnd = GetCurrentTime();
+    statsLocal.durationReduce += Duration(timeStart, timeEnd);
+    return fReduced;
   }
 
   /*
@@ -656,6 +733,7 @@ namespace rrr {
   template <typename Ntk, typename Ana>
   template <typename T>
   T Optimizer<Ntk, Ana>::SingleAdd(int id, T begin, T end) {
+    time_point timeStart = GetCurrentTime();
     MarkTfo(id);
     pNtk->ForEachFanin(id, [&](int fi) {
       vTfoMarks[fi] = true;
@@ -668,10 +746,13 @@ namespace rrr {
       if(vTfoMarks[*it]) {
         continue;
       }
+      statsLocal.nTriedFis++;
       if(ana.CheckFeasibility(id, *it, false)) {
         pNtk->AddFanin(id, *it, false);
+        statsLocal.nAddedFis++;
       } else if(pNtk->UseComplementedEdges() && ana.CheckFeasibility(id, *it, true)) {
         pNtk->AddFanin(id, *it, true);
+        statsLocal.nAddedFis++;
       } else {
         continue;
       }
@@ -681,16 +762,19 @@ namespace rrr {
     pNtk->ForEachFanin(id, [&](int fi) {
       vTfoMarks[fi] = false;
     });
+    time_point timeEnd = GetCurrentTime();
+    statsLocal.durationAdd += Duration(timeStart, timeEnd);
     return it;
   }
 
   template <typename Ntk, typename Ana>
   int Optimizer<Ntk, Ana>::MultiAdd(int id, std::vector<int> const &vCands, int nMax) {
+    time_point timeStart = GetCurrentTime();
     MarkTfo(id);
     pNtk->ForEachFanin(id, [&](int fi) {
       vTfoMarks[fi] = true;
     });
-    int nAdded = 0;
+    int nAddedFis_ = 0;
     for(int cand: vCands) {
       if(!pNtk->IsInt(cand) && !pNtk->IsPi(cand)) {
         continue;
@@ -698,23 +782,39 @@ namespace rrr {
       if(vTfoMarks[cand]) {
         continue;
       }
+      statsLocal.nTriedFis++;
       if(ana.CheckFeasibility(id, cand, false)) {
         pNtk->AddFanin(id, cand, false);
+        statsLocal.nAddedFis++;
       } else if(pNtk->UseComplementedEdges() && ana.CheckFeasibility(id, cand, true)) {
         pNtk->AddFanin(id, cand, true);
+        statsLocal.nAddedFis++;
       } else {
         continue;
       }
       mapNewFanins[id].insert(cand);
-      nAdded++;
+      nAddedFis_++;
-      if(nAdded == nMax) {
+      if(nAddedFis_ == nMax) {
         break;
       }
     }
     pNtk->ForEachFanin(id, [&](int fi) {
       vTfoMarks[fi] = false;
     });
-    return nAdded;
+    time_point timeEnd = GetCurrentTime();
+    statsLocal.durationAdd += Duration(timeStart, timeEnd);
+    return nAddedFis_;
+  }
+
+  template <typename Ntk, typename Ana>
+  void Optimizer<Ntk, Ana>::Undo() {
+    for(auto const &entry: mapNewFanins) {
+      int id = entry.first;
+      for(int fi: entry.second) {
+        int idx = pNtk->FindFanin(id, fi);
+        pNtk->RemoveFanin(id, idx);
+      }
+    }
   }
 
   /* }}} */
@@ -731,11 +831,12 @@ namespace rrr {
     pNtk->TrivialCollapse(id);
     // save if wanted
     int slot = -2;
-    if(fGreedy) {
+    if(fGreedy || fCompatible) {
       slot = pNtk->Save();
     }
-    double dCost = CostFunction(pNtk);
     // main loop
+    double cost = CostFunction(pNtk);
+    bool fTried = false, fAdded = false;
     for(citr it = vCands.begin(); it != vCands.end(); it++) {
       if(Timeout()) {
         break;
@@ -743,25 +844,44 @@ namespace rrr {
       if(!pNtk->IsInt(id)) {
         break;
       }
+      fTried = true;
       it = SingleAdd<citr>(id, it, vCands.end());
       if(it == vCands.end()) {
         break;
       }
-      Print(1, "cand", *it, "(", int_distance(vCands.begin(), it) + 1, "/", int_size(vCands), "):", "cost", "=", dCost);
+      fAdded = true;
-      RemoveRedundancy();
+      Print(2, "cand", *it, "(", int_distance(vCands.begin(), it) + 1, "/", int_size(vCands), ")", ":", "cost", "=", cost);
-      mapNewFanins.clear();
+      if(RemoveRedundancy()) {
-      double dNewCost = CostFunction(pNtk);
+        double costNew = CostFunction(pNtk);
-      Print(2, "cost:", dCost, "->", dNewCost);
+        // stats
-      if(fGreedy) {
+        statsLocal.nChanged++;
-        if(dNewCost <= dCost) {
+        if(costNew < cost) {
-          pNtk->Save(slot);
+          statsLocal.nDowns++;
-          dCost = dNewCost;
+        } else if (costNew == cost) {
+          statsLocal.nEqs++;
         } else {
-          pNtk->Load(slot);
+          statsLocal.nUps++;
+        }
+        // greedy
+        if(fGreedy) {
+          if(costNew <= cost) {
+            pNtk->Save(slot);
+            cost = costNew;
+          } else {
+            pNtk->Load(slot);
+          }
+        } else {
+          cost = costNew;
         }
       } else {
-        dCost = dNewCost;
+        // assuming addition only always increases cost
+        if(fCompatible) {
+          pNtk->Load(slot);
+        } else {
+          Undo();
+        }
       }
+      mapNewFanins.clear();
     }
     if(pNtk->IsInt(id)) {
       pNtk->TrivialDecompose(id);
@@ -770,9 +890,15 @@ namespace rrr {
         RemoveRedundancy();
       }
     }
-    if(fGreedy) {
+    if(fGreedy || fCompatible) {
       pNtk->PopBack();
     }
+    if(fTried) {
+      statsLocal.nTried++;
+    }
+    if(fAdded) {
+      statsLocal.nAdded++;
+    }
   }
 
   template <typename Ntk, typename Ana>
@@ -781,24 +907,43 @@ namespace rrr {
     // let us assume the node is not trivially redundant for now
     assert(pNtk->GetNumFanouts(id) != 0);
     assert(pNtk->GetNumFanins(id) > 1);
+    statsLocal.nTried++;
     // save if wanted
     int slot = -2;
-    if(fGreedy) {
+    if(fGreedy || fCompatible) {
       slot = pNtk->Save();
     }
-    double dCost = CostFunction(pNtk);
     // collapse
     pNtk->TrivialCollapse(id);
     // resub
-    MultiAdd(id, vCands, nMax);
+    double cost = CostFunction(pNtk);
-    RemoveRedundancy();
+    if(MultiAdd(id, vCands, nMax)) {
-    mapNewFanins.clear();
+      statsLocal.nAdded++;
-    // TODO: we could quit here if nothing has been removed
+      if(RemoveRedundancy()) {
-    RemoveRedundancy();
+        mapNewFanins.clear();
-    double dNewCost = CostFunction(pNtk);
+        RemoveRedundancy();
-    Print(1, "cost:", dCost, "->", dNewCost);
+        double costNew = CostFunction(pNtk);
-    if(fGreedy && dNewCost > dCost) {
+        // stats
-      pNtk->Load(slot);
+        statsLocal.nChanged++;
+        if(costNew < cost) {
+          statsLocal.nDowns++;
+        } else if (costNew == cost) {
+          statsLocal.nEqs++;
+        } else {
+          statsLocal.nUps++;
+        }
+        // greedy
+        if(fGreedy && costNew > cost) {
+          pNtk->Load(slot);
+        }
+      } else {
+        if(fCompatible) {
+          pNtk->Load(slot);
+        } else {
+          Undo();
+        }
+        mapNewFanins.clear();
+      }
     }
     if(pNtk->IsInt(id)) {
       pNtk->TrivialDecompose(id);
@@ -807,7 +952,7 @@ namespace rrr {
         RemoveRedundancy();
       }
     }
-    if(fGreedy) {
+    if(fGreedy || fCompatible) {
       pNtk->PopBack();
     }
   }
@@ -824,57 +969,77 @@ namespace rrr {
     // let us assume the node is not trivially redundant for now
     assert(pNtk->GetNumFanouts(id) != 0);
     assert(pNtk->GetNumFanins(id) > 1);
-    // save before trivial collapse
+    Print(2, "method", "=", "single");
-    int slot0 = pNtk->Save();
     // collapse
     pNtk->TrivialCollapse(id);
-    // save after trivial collapse
+    // save
     int slot = pNtk->Save();
-    double dCost = CostFunction(pNtk);
     // remember fanins
     std::set<int> sFanins = pNtk->GetExtendedFanins(id);
-    Print(2, "extended fanins:", sFanins);
+    Print(3, "extended fanins", ":", sFanins);
     // main loop
+    bool fChanged = false;
+    double cost = CostFunction(pNtk);
+    bool fTried = false, fAdded = false;
     for(citr it = vCands.begin(); it != vCands.end(); it++) {
       if(Timeout()) {
         break;
       }
       assert(pNtk->IsInt(id));
+      fTried = true;
       it = SingleAdd<citr>(id, it, vCands.end());
       if(it == vCands.end()) {
         break;
       }
-      Print(1, "cand", *it, "(", int_distance(vCands.begin(), it) + 1, "/", int_size(vCands), "):", "cost", "=", dCost);
+      fAdded = true;
-      RemoveRedundancy();
+      Print(3, "cand", *it, "(", int_distance(vCands.begin(), it) + 1, "/", int_size(vCands), ")", ":", "cost", "=", cost);
-      mapNewFanins.clear();
+      if(RemoveRedundancy()) {
-      double dNewCost = CostFunction(pNtk);
+        mapNewFanins.clear();
-      Print(2, "cost:", dCost, "->", dNewCost);
+        double costNew = CostFunction(pNtk);
-      if(dNewCost <= dCost) {
+        if(costNew <= cost) {
-        bool fChanged = false;
+          fChanged = false;
-        if(dNewCost < dCost || !pNtk->IsInt(id)) {
+          if(costNew < cost || !pNtk->IsInt(id)) {
-          fChanged = true;
-        } else {
-          std::set<int> sNewFanins = pNtk->GetExtendedFanins(id);
-          Print(2, "new extended fanins:", sNewFanins);
-          if(sFanins != sNewFanins) {
             fChanged = true;
+          } else {
+            std::set<int> sNewFanins = pNtk->GetExtendedFanins(id);
+            Print(3, "new extended fanins", ":", sNewFanins);
+            if(sFanins != sNewFanins) {
+              fChanged = true;
+            }
+          }
+          if(fChanged) {
+            statsLocal.nChanged++;
+            if(costNew < cost) {
+              statsLocal.nDowns++;
+            } else if (costNew == cost) {
+              statsLocal.nEqs++;
+            } else {
+              statsLocal.nUps++;
+            }
+            break;
           }
         }
-        if(fChanged) {
+        pNtk->Load(slot);
-          if(pNtk->IsInt(id)) {
+      } else {
-            pNtk->TrivialDecompose(id);
+        if(fCompatible) {
-          }
+          pNtk->Load(slot);
-          pNtk->PopBack(); // slot
+        } else {
-          pNtk->PopBack(); // slot0
+          Undo();
-          return true;
         }
+        mapNewFanins.clear();
       }
-      pNtk->Load(slot);
     }
-    pNtk->PopBack(); // slot
+    if(pNtk->IsInt(id)) {
-    pNtk->Load(slot0);
+      pNtk->TrivialDecompose(id);
-    pNtk->PopBack(); // slot0
+    }
-    return false;
+    pNtk->PopBack();
+    if(fTried) {
+      statsLocal.nTried++;
+    }
+    if(fAdded) {
+      statsLocal.nAdded++;
+    }
+    return fChanged;
   }
 
   template <typename Ntk, typename Ana>
@@ -885,44 +1050,59 @@ namespace rrr {
     // let us assume the node is not trivially redundant for now
     assert(pNtk->GetNumFanouts(id) != 0);
     assert(pNtk->GetNumFanins(id) > 1);
+    Print(2, "method", "=", "multi");
+    statsLocal.nTried++;
     // save
     int slot = pNtk->Save();
-    double dCost = CostFunction(pNtk);
     // remember fanins
     std::set<int> sFanins = pNtk->GetExtendedFanins(id);
-    Print(2, "extended fanins:", sFanins);
+    Print(3, "extended fanins", ":", sFanins);
     // collapse
     pNtk->TrivialCollapse(id);
     // resub
-    MultiAdd(id, vCands, nMax);
+    bool fChanged = false;
-    RemoveRedundancy();
+    double cost = CostFunction(pNtk);
-    mapNewFanins.clear();
+    if(MultiAdd(id, vCands, nMax)) {
-    // TODO: we could quit here if nothing has been removed
+      statsLocal.nAdded++;
-    RemoveRedundancy();
+      if(RemoveRedundancy()) {
-    double dNewCost = CostFunction(pNtk);
+        mapNewFanins.clear();
-    Print(1, "cost:", dCost, "->", dNewCost);
+        RemoveRedundancy();
-    if(!fGreedy || dNewCost <= dCost) {
+        double costNew = CostFunction(pNtk);
-      bool fChanged = false;
+        if(!fGreedy || costNew <= cost) {
-      if(dNewCost < dCost || !pNtk->IsInt(id)) {
+          fChanged = false;
-        fChanged = true;
+          if(costNew < cost || !pNtk->IsInt(id)) {
+            fChanged = true;
+          } else {
+            std::set<int> sNewFanins = pNtk->GetExtendedFanins(id);
+            Print(3, "new extended fanins", ":", sNewFanins);
+            if(sFanins != sNewFanins) {
+              fChanged = true;
+            }
+          }
+          if(fChanged) {
+            statsLocal.nChanged++;
+            if(costNew < cost) {
+              statsLocal.nDowns++;
+            } else if (costNew == cost) {
+              statsLocal.nEqs++;
+            } else {
+              statsLocal.nUps++;
+            }
+          }
+        }
       } else {
-        std::set<int> sNewFanins = pNtk->GetExtendedFanins(id);
+        mapNewFanins.clear();
-        Print(2, "new extended fanins:", sNewFanins);
-        if(sFanins != sNewFanins) {
-          fChanged = true;
-        }
-      }
-      if(fChanged) {
-        if(pNtk->IsInt(id)) {
-          pNtk->TrivialDecompose(id);
-        }
-        pNtk->PopBack();
-        return true;
       }
     }
-    pNtk->Load(slot);
+    if(fChanged) {
+      if(pNtk->IsInt(id)) {
+        pNtk->TrivialDecompose(id);
+      }
+    } else {
+      pNtk->Load(slot);
+    }
     pNtk->PopBack();
-    return false;
+    return fChanged;
   }
   
   /* }}} */
@@ -948,7 +1128,7 @@ namespace rrr {
       }
     }
     // add while remembering extended fanins
-    Print(1, "targets:", vTargets);
+    Print(2, "targets", ":", vTargets);
     std::vector<std::set<int>> vsFanins;
     for(int id: vTargets) {
       // get candidates
@@ -961,7 +1141,7 @@ namespace rrr {
       std::shuffle(vCands.begin(), vCands.end(), rng);
       // remember fanins
       std::set<int> sFanins = pNtk->GetExtendedFanins(id);
-      Print(2, "extended fanins:", sFanins);
+      Print(3, "extended fanins", ":", sFanins);
       vsFanins.push_back(std::move(sFanins));
       // add
       MultiAdd(id, vCands, nMax);
@@ -972,7 +1152,7 @@ namespace rrr {
     // TODO: we could quit here if nothing has been removed
     RemoveRedundancy();
     double dNewCost = CostFunction(pNtk);
-    Print(1, "cost:", dCost, "->", dNewCost);
+    Print(2, "cost =", dCost, "->", dNewCost);
     if(!fGreedy || dNewCost <= dCost) {
       bool fChanged = false;
       if(dNewCost < dCost) {
@@ -986,7 +1166,7 @@ namespace rrr {
         }
         for(int i = 0; !fChanged && i < int_size(vTargets); i++) {
           std::set<int> sNewFanins = pNtk->GetExtendedFanins(vTargets[i]);
-          Print(2, "new extended fanins:", sNewFanins);
+          Print(3, "new extended fanins", ":", sNewFanins);
           if(vsFanins[i] != sNewFanins) {
             fChanged = true;
           }
@@ -1021,7 +1201,7 @@ namespace rrr {
       if(!pNtk->IsInt(*it)) {
         continue;
       }
-      Print(0, "node", *it, "(", int_distance(vInts.crbegin(), it) + 1, "/", int_size(vInts), "):", "cost", "=", CostFunction(pNtk));
+      Print(1, "node", *it, "(", int_distance(vInts.crbegin(), it) + 1, "/", int_size(vInts), ")", ":", "cost", "=", CostFunction(pNtk));
       func(*it);
     }
   }
@@ -1037,7 +1217,7 @@ namespace rrr {
       if(!pNtk->IsInt(*it)) {
         continue;
       }
-      Print(0, "node", *it, "(", int_distance(vInts.cbegin(), it) + 1, "/", int_size(vInts), "):", "cost", "=", CostFunction(pNtk));
+      Print(1, "node", *it, "(", int_distance(vInts.cbegin(), it) + 1, "/", int_size(vInts), ")", ":", "cost", "=", CostFunction(pNtk));
       if(func(*it)) {
         break;
       }
@@ -1048,10 +1228,10 @@ namespace rrr {
   void Optimizer<Ntk, Ana>::ApplyCombinationRandomlyStop(int k, std::function<bool(std::vector<int> const &)> const &func) {
     std::vector<int> vInts = pNtk->GetInts();
     std::shuffle(vInts.begin(), vInts.end(), rng); // order is decided here, so it's not truely exhaustive
-    int nTried = 0;
+    int nTried_ = 0;
     int nCombs = k * (k - 1) / 2;
     ForEachCombinationStop(int_size(vInts), k, [&](std::vector<int> const &vIdxs) {
-      Print(0, "comb", vIdxs, "(", ++nTried, "/", nCombs, ")");
+      Print(1, "comb", vIdxs, "(", ++nTried_, "/", nCombs, ")");
       assert(int_size(vIdxs) == k);
       if(Timeout()) {
         return true;
@@ -1078,7 +1258,7 @@ namespace rrr {
       }
       std::vector<int> vIdxs(sIdxs.begin(), sIdxs.end());
       std::shuffle(vIdxs.begin(), vIdxs.end(), rng);
-      Print(0, "comb", vIdxs, "(", i + 1, "/", nSamples, ")");
+      Print(1, "comb", vIdxs, "(", i + 1, "/", nSamples, ")");
       std::vector<int> vTargets(k);
       for(int i = 0; i < k; i++) {
         vTargets[i] = vInts[vIdxs[i]];
@@ -1109,11 +1289,16 @@ namespace rrr {
   }
   
   template <typename Ntk, typename Ana>
-  void Optimizer<Ntk, Ana>::UpdateNetwork(Ntk *pNtk_, bool fSame) {
+  void Optimizer<Ntk, Ana>::AssignNetwork(Ntk *pNtk_, bool fReuse) {
     pNtk = pNtk_;
     target = -1;
     pNtk->AddCallback(std::bind(&Optimizer<Ntk, Ana>::ActionCallback, this, std::placeholders::_1));
-    ana.UpdateNetwork(pNtk, fSame);
+    ana.AssignNetwork(pNtk, fReuse);
+  }
+  
+  template <typename Ntk, typename Ana>
+  void Optimizer<Ntk, Ana>::SetPrintLine(std::function<void(std::string)> const &PrintLine_) {
+    PrintLine = PrintLine_;
   }
   
   /* }}} */
@@ -1127,13 +1312,14 @@ namespace rrr {
     vRandCosts.clear();
     if(nSortTypeOriginal < 0) {
       nSortType = rng() % 18;
-      Print(0, "sorttype =", nSortType);
+      Print(0, "fanin cost function =", nSortType);
     }
     nTimeout = nTimeout_;
     start = GetCurrentTime();
     switch(nFlow) {
     case 0:
       RemoveRedundancy();
+      statsLocal.Reset();
       ApplyReverseTopologically([&](int id) {
         std::vector<int> vCands;
         if(nDistance) {
@@ -1143,9 +1329,12 @@ namespace rrr {
         }
         SingleResub(id, vCands);
       });
+      stats["single"] += statsLocal;
+      Print(0, statsLocal.GetString());
       break;
     case 1:
       RemoveRedundancy();
+      statsLocal.Reset();
       ApplyReverseTopologically([&](int id) {
         std::vector<int> vCands;
         if(nDistance) {
@@ -1155,11 +1344,14 @@ namespace rrr {
         }
         MultiResub(id, vCands);
       });
+      stats["multi"] += statsLocal;
+      Print(0, statsLocal.GetString());
       break;
     case 2: {
       RemoveRedundancy();
       double dCost = CostFunction(pNtk);
       while(true) {
+        statsLocal.Reset();
         ApplyReverseTopologically([&](int id) {
           std::vector<int> vCands;
           if(nDistance) {
@@ -1169,6 +1361,9 @@ namespace rrr {
           }
           SingleResub(id, vCands);
         });
+        stats["single"] += statsLocal;
+        Print(0, "single", ":", "cost", "=", CostFunction(pNtk), ",", statsLocal.GetString());
+        statsLocal.Reset();
         ApplyReverseTopologically([&](int id) {
           std::vector<int> vCands;
           if(nDistance) {
@@ -1179,6 +1374,8 @@ namespace rrr {
           }
           MultiResub(id, vCands);
         });
+        stats["multi"] += statsLocal;
+        Print(0, "multi ", ":", "cost", "=", CostFunction(pNtk), ",", statsLocal.GetString());
         double dNewCost = CostFunction(pNtk);
         if(dNewCost < dCost) {
           dCost = dNewCost;
@@ -1195,17 +1392,27 @@ namespace rrr {
         vCands = pNtk->GetPisInts();
         std::shuffle(vCands.begin(), vCands.end(), rng);
       }
+      Stats statsSingle, statsMulti;
       ApplyRandomlyStop([&](int id) {
+        statsLocal.Reset();
         if(nDistance) {
           vCands = pNtk->GetNeighbors(id, true, nDistance);
           std::shuffle(vCands.begin(), vCands.end(), rng);
         }
+        bool fChanged;
         if(rng() & 1) {
-          return SingleResubStop(id, vCands);
+          fChanged = SingleResubStop(id, vCands);
+          statsSingle += statsLocal;
         } else {
-          return MultiResubStop(id, vCands);
+          fChanged = MultiResubStop(id, vCands);
+          statsMulti += statsLocal;
         }
+        return fChanged;
       });
+      stats["single"] += statsSingle;
+      stats["multi"] += statsMulti;
+      Print(0, "single", ":", statsSingle.GetString());
+      Print(0, "multi ", ":", statsMulti.GetString());
       break;
     }
     case 4: {
@@ -1222,6 +1429,46 @@ namespace rrr {
   
   /* }}} */
 
+  /* {{{ Summary */
+
+  template <typename Ntk, typename Ana>
+  void Optimizer<Ntk, Ana>::ResetSummary() {
+    stats.clear();
+    ana.ResetSummary();
+  }
+  
+  template <typename Ntk, typename Ana>
+  summary<int> Optimizer<Ntk, Ana>::GetStatsSummary() const {
+    summary<int> v;
+    for(auto const &entry: stats) {
+      v.emplace_back("opt " + entry.first + " tried node", entry.second.nTried);
+      v.emplace_back("opt " + entry.first + " tried fanin", entry.second.nTriedFis);
+      v.emplace_back("opt " + entry.first + " added node", entry.second.nAdded);
+      v.emplace_back("opt " + entry.first + " added fanin", entry.second.nAddedFis);
+      v.emplace_back("opt " + entry.first + " changed", entry.second.nChanged);
+      v.emplace_back("opt " + entry.first + " up", entry.second.nUps);
+      v.emplace_back("opt " + entry.first + " eq", entry.second.nEqs);
+      v.emplace_back("opt " + entry.first + " dn", entry.second.nDowns);
+    }
+    summary<int> v2 = ana.GetStatsSummary();
+    v.insert(v.end(), v2.begin(), v2.end());
+    return v;
+  }
+
+  template <typename Ntk, typename Ana>
+  summary<double> Optimizer<Ntk, Ana>::GetTimesSummary() const {
+    summary<double> v;
+    for(auto const &entry: stats) {
+      v.emplace_back("opt " + entry.first + " add", entry.second.durationAdd);
+      v.emplace_back("opt " + entry.first + " reduce", entry.second.durationReduce);
+    }
+    summary<double> v2 = ana.GetTimesSummary();
+    v.insert(v.end(), v2.begin(), v2.end());
+    return v;
+  }
+  
+  /* }}} */
+  
 }
 
 ABC_NAMESPACE_CXX_HEADER_END

src/opt/rrr/rrrParameter.h

@@ -8,7 +8,7 @@ namespace rrr {
     int iSeed = 0;
     int nWords = 10;
     int nTimeout = 0;
-    int nSchedulerVerbose = 1;
+    int nSchedulerVerbose = 0;
     int nPartitionerVerbose = 0;
     int nOptimizerVerbose = 0;
     int nAnalyzerVerbose = 0;

src/opt/rrr/rrrPartitioner.h

@@ -42,7 +42,7 @@ namespace rrr {
   public:
     // constructors
     Partitioner(Parameter const *pPar);
-    void UpdateNetwork(Ntk *pNtk);
+    void AssignNetwork(Ntk *pNtk);
 
     // APIs
     Ntk *Extract(int iSeed);
@@ -270,7 +270,7 @@ namespace rrr {
   }
 
   template <typename Ntk>
-  void Partitioner<Ntk>::UpdateNetwork(Ntk *pNtk_) {
+  void Partitioner<Ntk>::AssignNetwork(Ntk *pNtk_) {
     pNtk = pNtk_;
     assert(mSubNtk2Io.empty());
     assert(sBlocked.empty());

src/opt/rrr/rrrSatSolver.h

@@ -28,10 +28,12 @@ namespace rrr {
     std::vector<VarValue> vValues; // values in satisfied problem
     bool fUpdate;
 
-    // statistics
+    // stats
     int nCalls;
     int nSats;
     int nUnsats;
+    double durationRedundancy;
+    double durationFeasibility;
 
     // callback
     void ActionCallback(Action const &action);
@@ -45,7 +47,7 @@ namespace rrr {
     // constructors
     SatSolver(Parameter const *pPar);
     ~SatSolver();
-    void UpdateNetwork(Ntk *pNtk_, bool fSame);
+    void AssignNetwork(Ntk *pNtk_, bool fReuse);
     
     // checks
     SatResult CheckRedundancy(int id, int idx);
@@ -53,6 +55,11 @@ namespace rrr {
 
     // cex
     std::vector<VarValue> GetCex();
+
+    // stats
+    void ResetSummary();
+    summary<int> GetStatsSummary() const;
+    summary<double> GetTimesSummary() const;
   };
 
   /* {{{ Callback */
@@ -88,6 +95,11 @@ namespace rrr {
       break;
     case SORT_FANINS:
       break;
+    case READ:
+      status = false;
+      target = -1;
+      fUpdate = false;
+      break;
     case SAVE:
       break;
     case LOAD:
@@ -259,25 +271,23 @@ namespace rrr {
     pSat(sat_solver_new()),
     status(false),
     target(-1),
-    fUpdate(false),
+    fUpdate(false) {
-    nCalls(0),
+    ResetSummary();
-    nSats(0),
-    nUnsats(0) {
   }
 
   template <typename Ntk>
   SatSolver<Ntk>::~SatSolver() {
     sat_solver_delete(pSat);
-    std::cout << "SAT solver stats: calls = " << nCalls << " (SAT = " << nSats << ", UNSAT = " << nUnsats << ", UNDET = " << nCalls - nSats - nUnsats << ")" << std::endl;
+    //std::cout << "SAT solver stats: calls = " << nCalls << " (SAT = " << nSats << ", UNSAT = " << nUnsats << ", UNDET = " << nCalls - nSats - nUnsats << ")" << std::endl;
   }
 
   template <typename Ntk>
-  void SatSolver<Ntk>::UpdateNetwork(Ntk *pNtk_, bool fSame) {
+  void SatSolver<Ntk>::AssignNetwork(Ntk *pNtk_, bool fReuse) {
-    (void)fSame;
+    (void)fReuse;
-    pNtk = pNtk_;
     status = false;
     target = -1;
     fUpdate = false;
+    pNtk = pNtk_;
     pNtk->AddCallback(std::bind(&SatSolver<Ntk>::ActionCallback, this, std::placeholders::_1));
   }
 
@@ -287,11 +297,13 @@ namespace rrr {
   
   template <typename Ntk>
   SatResult SatSolver<Ntk>::CheckRedundancy(int id, int idx) {
+    time_point timeStart = GetCurrentTime();
     SetTarget(id);
     if(!status) {
       if(nVerbose) {
         std::cout << "trivially UNSATISFIABLE" << std::endl;
       }
+      durationRedundancy += Duration(timeStart, GetCurrentTime());
       return UNSAT;
     }
     vLits.clear();
@@ -319,12 +331,14 @@ namespace rrr {
         std::cout << "UNSATISFIABLE" << std::endl;
       }
       nUnsats++;
+      durationRedundancy += Duration(timeStart, GetCurrentTime());
       return UNSAT;
     }
     if(res == l_Undef) {
       if(nVerbose) {
         std::cout << "UNDETERMINED" << std::endl;
       }
+      durationRedundancy += Duration(timeStart, GetCurrentTime());
       return UNDET;
     }
     assert(res == l_True);
@@ -353,16 +367,19 @@ namespace rrr {
       assert((vValues[fi] == TEMP_TRUE) ^ (idx == idx2) ^ c);
       vValues[fi] = DecideVarValue(vValues[fi]);
     });
+    durationRedundancy += Duration(timeStart, GetCurrentTime());
     return SAT;
   }
 
   template <typename Ntk>
   SatResult SatSolver<Ntk>::CheckFeasibility(int id, int fi, bool c) {
+    time_point timeStart = GetCurrentTime();
     SetTarget(id);
     if(!status) {
       if(nVerbose) {
         std::cout << "trivially UNSATISFIABLE" << std::endl;
       }
+      durationFeasibility += Duration(timeStart, GetCurrentTime());
       return UNSAT;
     }
     vLits.clear();
@@ -385,12 +402,14 @@ namespace rrr {
         std::cout << "UNSATISFIABLE" << std::endl;
       }
       nUnsats++;
+      durationFeasibility += Duration(timeStart, GetCurrentTime());
       return UNSAT;
     }
     if(res == l_Undef) {
       if(nVerbose) {
         std::cout << "UNDETERMINED" << std::endl;
       }
+      durationFeasibility += Duration(timeStart, GetCurrentTime());
       return UNDET;
     }
     assert(res == l_True);
@@ -419,6 +438,7 @@ namespace rrr {
     vValues[id] = DecideVarValue(vValues[id]);
     assert((vValues[fi] == TEMP_TRUE) ^ !c);
     vValues[fi] = DecideVarValue(vValues[fi]);
+    durationFeasibility += Duration(timeStart, GetCurrentTime());
     return SAT;
   }
   
@@ -537,6 +557,36 @@ namespace rrr {
 
   /* }}} */
 
+  /* {{{ Stats */
+
+  template <typename Ntk>
+  void SatSolver<Ntk>::ResetSummary() {
+    nCalls = 0;
+    nSats = 0;
+    nUnsats = 0;
+    durationRedundancy = 0;
+    durationFeasibility = 0;
+  }
+
+  template <typename Ntk>
+  summary<int> SatSolver<Ntk>::GetStatsSummary() const {
+    summary<int> v;
+    v.emplace_back("sat call", nCalls);
+    v.emplace_back("sat satisfiable", nSats);
+    v.emplace_back("sat unsatisfiable", nUnsats);
+    return v;
+  }
+
+  template <typename Ntk>
+  summary<double> SatSolver<Ntk>::GetTimesSummary() const {
+    summary<double> v;
+    v.emplace_back("sat redundancy", durationRedundancy);
+    v.emplace_back("sat feasibility", durationFeasibility);
+    return v;
+  }
+
+  /* }}} */
+  
 }
 
 ABC_NAMESPACE_CXX_HEADER_END

src/opt/rrr/rrrScheduler.h

@@ -46,10 +46,14 @@ namespace rrr {
     // data
     int nCreatedJobs;
     int nFinishedJobs;
-    time_point start;
+    time_point timeStart;
     Par par;
     std::queue<Job *> qPendingJobs;
     Opt *pOpt; // used only in case of single thread execution
+    std::vector<std::string> vStatsSummaryKeys;
+    std::map<std::string, int> mStatsSummary;
+    std::vector<std::string> vTimesSummaryKeys;
+    std::map<std::string, double> mTimesSummary;
 #ifdef ABC_USE_PTHREADS
     bool fTerminate;
     std::vector<std::thread> vThreads;
@@ -57,21 +61,27 @@ namespace rrr {
     std::mutex mutexAbc;
     std::mutex mutexPendingJobs;
     std::mutex mutexFinishedJobs;
+    std::mutex mutexPrint;
     std::condition_variable condPendingJobs;
     std::condition_variable condFinishedJobs;
 #endif
 
+    // print
+    template <typename... Args>
+    void Print(int nVerboseLevel, std::string prefix, Args... args);
+    
     // time
     seconds GetRemainingTime() const;
+    double GetElapsedTime() const;
 
     // abc
     void CallAbc(Ntk *pNtk_, std::string Command);
 
     // run jobs
-    void RunJob(Opt &opt, Job const *pJob);
+    void RunJob(Opt &opt, Job *pJob);
 
     // manage jobs
-    void CreateJob(Ntk *pNtk_, int iSeed_);
+    Job *CreateJob(Ntk *pNtk_, int iSeed_, double cost);
     void OnJobEnd(std::function<void(Job *pJob)> const &func);
 
     // thread
@@ -79,6 +89,10 @@ namespace rrr {
     void Thread(Parameter const *pPar);
 #endif
     
+    // summary
+    template <typename T>
+    void AddToSummary(std::vector<std::string> &keys, std::map<std::string, T> &m, summary<T> const &result) const;
+
   public:
     // constructors
     Scheduler(Ntk *pNtk, Parameter const *pPar);
@@ -96,12 +110,21 @@ namespace rrr {
     int id;
     Ntk *pNtk;
     int iSeed;
+    double costInitial;
+    std::string prefix;
+    double duration;
+    summary<int> stats;
+    summary<double> times;
     
     // constructor
-    Job(int id, Ntk *pNtk, int iSeed) :
+    Job(int id, Ntk *pNtk, int iSeed, double cost) :
       id(id),
       pNtk(pNtk),
-      iSeed(iSeed) {
+      iSeed(iSeed),
+      costInitial(cost) {
+      std::stringstream ss;
+      PrintNext(ss, "job", id, ":");
+      prefix = ss.str() + " ";
     }
   };
 
@@ -115,21 +138,53 @@ namespace rrr {
   
   /* }}} */
 
+  /* {{{ Print */
+  
+  template <typename Ntk, typename Opt, typename Par>
+  template<typename... Args>
+  inline void Scheduler<Ntk, Opt, Par>::Print(int nVerboseLevel, std::string prefix, Args... args) {
+    if(nVerbose <= nVerboseLevel) {
+      return;
+    }
+#ifdef ABC_USE_PTHREADS
+    if(fMultiThreading) {
+      {
+        std::unique_lock<std::mutex> l(mutexPrint);
+        std::cout << prefix;
+        PrintNext(std::cout, args...);
+        std::cout << std::endl;
+      }
+      return;
+    }
+#endif
+    std::cout << prefix;
+    PrintNext(std::cout, args...);
+    std::cout << std::endl;
+  }
+
+  /* }}} */
+  
   /* {{{ Time */
 
   template <typename Ntk, typename Opt, typename Par>
-  seconds Scheduler<Ntk, Opt, Par>::GetRemainingTime() const {
+  inline seconds Scheduler<Ntk, Opt, Par>::GetRemainingTime() const {
     if(nTimeout == 0) {
       return 0;
     }
-    time_point current = GetCurrentTime();
+    time_point timeCurrent = GetCurrentTime();
-    seconds nRemainingTime = nTimeout - DurationInSeconds(start, current);
+    seconds nRemainingTime = nTimeout - DurationInSeconds(timeStart, timeCurrent);
     if(nRemainingTime == 0) { // avoid glitch
       return -1;
     }
     return nRemainingTime;
   }
 
+  template <typename Ntk, typename Opt, typename Par>
+  inline double Scheduler<Ntk, Opt, Par>::GetElapsedTime() const {
+    time_point timeCurrent = GetCurrentTime();
+    return Duration(timeStart, timeCurrent);
+  }
+
   /* }}} */
 
   /* {{{ Abc */
@@ -153,8 +208,12 @@ namespace rrr {
   /* {{{ Run jobs */
 
   template <typename Ntk, typename Opt, typename Par>
-  void Scheduler<Ntk, Opt, Par>::RunJob(Opt &opt, Job const *pJob) {
+  void Scheduler<Ntk, Opt, Par>::RunJob(Opt &opt, Job *pJob) {
-    opt.UpdateNetwork(pJob->pNtk);
+    time_point timeStartLocal = GetCurrentTime();
+    opt.AssignNetwork(pJob->pNtk, !fPartitioning); // reuse backend if restarting
+    opt.SetPrintLine([&](std::string str) {
+      Print(-1, pJob->prefix, str);
+    });
     // start flow
     switch(nFlow) {
     case 0:
@@ -162,23 +221,17 @@ namespace rrr {
       break;
     case 1: { // transtoch
       std::mt19937 rng(pJob->iSeed);
-      double dCost = CostFunction(pJob->pNtk);
+      double cost = pJob->costInitial;
-      double dBestCost = dCost;
+      double costBest = cost;
       Ntk best(*(pJob->pNtk));
-      if(nVerbose) {
-        std::cout << "start: cost = " << dCost << std::endl;
-      }
       for(int i = 0; i < 10; i++) {
         if(GetRemainingTime() < 0) {
           break;
         }
         if(i != 0) {
           CallAbc(pJob->pNtk, "&if -K 6; &mfs; &st");
-          dCost = CostFunction(pJob->pNtk);
+          cost = CostFunction(pJob->pNtk);
-          opt.UpdateNetwork(pJob->pNtk, true);
+          Print(1, pJob->prefix, "hop", i, ":", "cost", "=", cost);
-          if(nVerbose) {
-            std::cout << "hop " << std::setw(3) << i << ": cost = " << dCost << std::endl;
-          }
         }
         for(int j = 0; true; j++) {
           if(GetRemainingTime() < 0) {
@@ -186,37 +239,28 @@ namespace rrr {
           }
           opt.Run(rng(), GetRemainingTime());
           CallAbc(pJob->pNtk, "&dc2");
-          double dNewCost = CostFunction(pJob->pNtk);
+          double costNew = CostFunction(pJob->pNtk);
-          if(nVerbose) {
+          Print(1, pJob->prefix, "ite", j, ":", "cost", "=", costNew);
-            std::cout << "\tite " << std::setw(3) << j << ": cost = " << dNewCost << std::endl;
+          if(costNew < cost) {
-          }
+            cost = costNew;
-          if(dNewCost < dCost) {
-            dCost = dNewCost;
-            opt.UpdateNetwork(pJob->pNtk, true);
           } else {
             break;
           }
         }
-        if(dCost < dBestCost) {
+        if(cost < costBest) {
-          dBestCost = dCost;
+          costBest = cost;
           best = *(pJob->pNtk);
           i = 0;
         }
       }
       *(pJob->pNtk) = best;
-      if(nVerbose) {
-        std::cout << "end: cost = " << dBestCost << std::endl;
-      }
       break;
     }
     case 2: { // deep
       std::mt19937 rng(pJob->iSeed);
       int n = 0;
-      double dCost = CostFunction(pJob->pNtk);
+      double cost = pJob->costInitial;
       Ntk best(*(pJob->pNtk));
-      if(nVerbose) {
-        std::cout << "start: cost = " << dCost << std::endl;
-      }
       for(int i = 0; i < 1000000; i++) {
         if(GetRemainingTime() < 0) {
           break;
@@ -246,38 +290,30 @@ namespace rrr {
           Command += "; &fx; &st";
         Command += pComp;
         CallAbc(pJob->pNtk, Command);
-        if(nVerbose) {
+        Print(1, pJob->prefix, "ite", i, ":", "cost", "=", CostFunction(pJob->pNtk));
-          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.UpdateNetwork(pJob->pNtk, true);
           opt.Run(rng(), GetRemainingTime());
           if(rng() & 1) {
             CallAbc(pJob->pNtk, "&dc2");
           } else {
             CallAbc(pJob->pNtk, std::string("&put; ") + pCompress2rs + "; &get");
           }
-          if(nVerbose) {
+          Print(1, pJob->prefix, "rrr", j, ":", "cost", "=", CostFunction(pJob->pNtk));
-            std::cout << "\trrr " << std::setw(6) << j << ": cost = " << CostFunction(pJob->pNtk) << std::endl;
-          }
         }
         // eval
-        double dNewCost = CostFunction(pJob->pNtk);
+        double costNew = CostFunction(pJob->pNtk);
-        if(dNewCost < dCost) {
+        if(costNew < cost) {
-          dCost = dNewCost;
+          cost = costNew;
           best = *(pJob->pNtk);
         } else {
           n++;
         }
       }
       *(pJob->pNtk) = best;
-      if(nVerbose) {
-        std::cout << "end: cost = " << dCost << std::endl;
-      }
       break;
     }
     case 3:
@@ -287,6 +323,11 @@ namespace rrr {
     default:
       assert(0);
     }
+    time_point timeEndLocal = GetCurrentTime();
+    pJob->duration = Duration(timeStartLocal, timeEndLocal);
+    pJob->stats = opt.GetStatsSummary();
+    pJob->times = opt.GetTimesSummary();
+    opt.ResetSummary();
   }
 
   /* }}} */
@@ -294,8 +335,8 @@ namespace rrr {
   /* {{{ Manage jobs */
 
   template <typename Ntk, typename Opt, typename Par>
-  void Scheduler<Ntk, Opt, Par>::CreateJob(Ntk *pNtk_, int iSeed_) {
+  typename Scheduler<Ntk, Opt, Par>::Job *Scheduler<Ntk, Opt, Par>::CreateJob(Ntk *pNtk_, int iSeed_, double cost) {
-    Job *pJob = new Job(nCreatedJobs++, pNtk_, iSeed_);
+    Job *pJob = new Job(nCreatedJobs++, pNtk_, iSeed_, cost);
 #ifdef ABC_USE_PTHREADS
     if(fMultiThreading) {
       {
@@ -303,10 +344,11 @@ namespace rrr {
         qPendingJobs.push(pJob);
         condPendingJobs.notify_one();
       }
-      return;
+      return pJob;
     }
 #endif
     qPendingJobs.push(pJob);
+    return pJob;
   }
   
   template <typename Ntk, typename Opt, typename Par>
@@ -324,6 +366,8 @@ namespace rrr {
       }
       assert(pJob != NULL);
       func(pJob);
+      AddToSummary(vStatsSummaryKeys, mStatsSummary, pJob->stats);
+      AddToSummary(vTimesSummaryKeys, mTimesSummary, pJob->times);
       delete pJob;
       nFinishedJobs++;
       return;
@@ -335,6 +379,8 @@ namespace rrr {
     qPendingJobs.pop();
     RunJob(*pOpt, pJob);
     func(pJob);
+    AddToSummary(vStatsSummaryKeys, mStatsSummary, pJob->stats);
+    AddToSummary(vTimesSummaryKeys, mTimesSummary, pJob->times);
     delete pJob;
     nFinishedJobs++;
   }
@@ -374,6 +420,28 @@ namespace rrr {
 
   /* }}} */
   
+  /* {{{ Summary */
+
+  template <typename Ntk, typename Opt, typename Par>
+  template <typename T>
+  void Scheduler<Ntk, Opt, Par>::AddToSummary(std::vector<std::string> &keys, std::map<std::string, T> &m, summary<T> const &result) const {
+    std::vector<std::string>::iterator it = keys.begin();
+    for(auto const &entry: result) {
+      if(m.count(entry.first)) {
+        m[entry.first] += entry.second;
+        it = std::find(it, keys.end(), entry.first);
+        assert(it != keys.end());
+        it++;
+      } else {
+        m[entry.first] = entry.second;
+        it = keys.insert(it, entry.first);
+        it++;          
+      }
+    }
+  }
+  
+  /* }}} */
+
   /* {{{ Constructors */
 
   template <typename Ntk, typename Opt, typename Par>
@@ -439,74 +507,90 @@ namespace rrr {
 
   template <typename Ntk, typename Opt, typename Par>
   void Scheduler<Ntk, Opt, Par>::Run() {
-    start = GetCurrentTime();
+    timeStart = GetCurrentTime();
+    double costStart = CostFunction(pNtk);
     if(fPartitioning) {
       fDeterministic = false; // it is deterministic anyways as we wait until all jobs finish each round
       pNtk->Sweep();
-      par.UpdateNetwork(pNtk);
+      par.AssignNetwork(pNtk);
       while(nCreatedJobs < nJobs) {
         assert(nParallelPartitions > 0);
         if(nCreatedJobs < nFinishedJobs + nParallelPartitions) {
           Ntk *pSubNtk = par.Extract(iSeed + nCreatedJobs);
           if(pSubNtk) {
-            CreateJob(pSubNtk, iSeed + nCreatedJobs);
+            Job *pJob = CreateJob(pSubNtk, iSeed + nCreatedJobs, CostFunction(pSubNtk));
-            std::cout << "job " << nCreatedJobs - 1 << " created (size = " << pSubNtk->GetNumInts() << ")" << std::endl;
+            Print(1, pJob->prefix, "created ", ":", "i/o", "=", pJob->pNtk->GetNumPis(), "/", pJob->pNtk->GetNumPos(), ",", "node", "=", pJob->pNtk->GetNumInts(), ",", "level", "=", pJob->pNtk->GetNumLevels(), ",", "cost", "=", pJob->costInitial);
             continue;
           }
         }
         if(nCreatedJobs == nFinishedJobs) {
-          std::cout << "failed to partition" << std::endl;
+          PrintWarning("failed to partition");
           break;
         }
         while(nFinishedJobs < nCreatedJobs) {
           OnJobEnd([&](Job *pJob) {
-            std::cout << "job " << pJob->id << " finished (size = " << pJob->pNtk->GetNumInts() << ")" << std::endl;
+            double cost = CostFunction(pJob->pNtk);
+            Print(1, pJob->prefix, "finished", ":", "i/o", "=", pJob->pNtk->GetNumPis(), "/", pJob->pNtk->GetNumPos(), ",", "node", "=", pJob->pNtk->GetNumInts(), ",", "level", "=", pJob->pNtk->GetNumLevels(), ",", "cost", "=", cost);
+            Print(0, "", "job", pJob->id, "(", nFinishedJobs + 1, "/", nJobs, ")", ":", "i/o", "=", pJob->pNtk->GetNumPis(), "/", pJob->pNtk->GetNumPos(), ",", "node", "=", pJob->pNtk->GetNumInts(), ",", "level", "=", pJob->pNtk->GetNumLevels(), ",", "cost", "=", cost, "(", 100 * (cost - pJob->costInitial) / pJob->costInitial, "%", ")", ",", "duration", "=", pJob->duration, "s", ",", "elapsed", "=", GetElapsedTime(), "s");
             par.Insert(pJob->pNtk);
           });
         }
         if(fOptOnInsert) {
+          time_point timeStartLocal = GetCurrentTime();
           CallAbc(pNtk, std::string("&put; ") + pCompress2rs + "; dc2; &get");
-          par.UpdateNetwork(pNtk);
+          time_point timeEndLocal = GetCurrentTime();
+          par.AssignNetwork(pNtk);
+          double cost = CostFunction(pNtk);
+          Print(0, "", "c2rs; dc2", ":", std::string(34, ' '), "node", "=", pNtk->GetNumInts(), ",", "level", "=", pNtk->GetNumLevels(), ",", "cost", "=", cost, "(", 100 * (cost - costStart) / costStart, "%", ")", ",", "duration", "=", Duration(timeStartLocal, timeEndLocal), "s", ",", "elapsed", "=", GetElapsedTime(), "s");
         }
       }
       while(nFinishedJobs < nCreatedJobs) {
         OnJobEnd([&](Job *pJob) {
-          std::cout << "job " << pJob->id << " finished (size = " << pJob->pNtk->GetNumInts() << ")" << std::endl;
+          double cost = CostFunction(pJob->pNtk);
+          Print(1, pJob->prefix, "finished", ":", "i/o", "=", pJob->pNtk->GetNumPis(), "/", pJob->pNtk->GetNumPos(), ",", "node", "=", pJob->pNtk->GetNumInts(), ",", "level", "=", pJob->pNtk->GetNumLevels(), ",", "cost", "=", CostFunction(pJob->pNtk));
+          Print(0, "", "job", pJob->id, "(", nFinishedJobs + 1, "/", nJobs, ")", ":", "i/o", "=", pJob->pNtk->GetNumPis(), "/", pJob->pNtk->GetNumPos(), ",", "node", "=", pJob->pNtk->GetNumInts(), ",", "level", "=", pJob->pNtk->GetNumLevels(), ",", "cost", "=", cost, "(", 100 * (cost - pJob->costInitial) / pJob->costInitial, "%", ")", ",", "duration", "=", pJob->duration, "s", ",", "elapsed", "=", GetElapsedTime(), "s");
           par.Insert(pJob->pNtk);
         });
       }
       if(fOptOnInsert) {
         CallAbc(pNtk, std::string("&put; ") + pCompress2rs + "; dc2; &get");
-        par.UpdateNetwork(pNtk);
+        par.AssignNetwork(pNtk);
       }
     } else if(nJobs > 1) {
-      double dCost = CostFunction(pNtk);
+      double costBest = costStart;
       for(int i = 0; i < nJobs; i++) {
         Ntk *pCopy = new Ntk(*pNtk);
-        CreateJob(pCopy, iSeed + i);
+        CreateJob(pCopy, iSeed + i, costBest);
       }
       for(int i = 0; i < nJobs; i++) {
         OnJobEnd([&](Job *pJob) {
-          double dNewCost = CostFunction(pJob->pNtk);
+          double cost = CostFunction(pJob->pNtk);
-          if(nVerbose) {
+          Print(0, "", "job", pJob->id, "(", nFinishedJobs + 1, "/", nJobs, ")", ":", "node", "=", pJob->pNtk->GetNumInts(), ",", "level", "=", pJob->pNtk->GetNumLevels(), ",", "cost", "=", cost, "(", 100 * (cost - pJob->costInitial) / pJob->costInitial, "%", ")", ",", "duration", "=", pJob->duration, "s", ",", "elapsed", "=", GetElapsedTime(), "s");
-            std::cout << "run " << pJob->id << ": cost = " << dNewCost << std::endl;
+          if(cost < costBest) {
-          }
+            costBest = cost;
-          if(dNewCost < dCost) {
-            dCost = dNewCost;
             *pNtk = *(pJob->pNtk);
           }
           delete pJob->pNtk;
         });
       }
     } else {
-      CreateJob(pNtk, iSeed);
+      CreateJob(pNtk, iSeed, costStart);
-      OnJobEnd([&](Job *pJob) { (void)pJob; });
+      OnJobEnd([&](Job *pJob) {
+        double cost = CostFunction(pJob->pNtk);
+        Print(0, "", "job", pJob->id, "(", nFinishedJobs + 1, "/", nJobs, ")", ":", "node", "=", pJob->pNtk->GetNumInts(), ",", "level", "=", pJob->pNtk->GetNumLevels(), ",", "cost", "=", cost, "(", 100 * (cost - pJob->costInitial) / pJob->costInitial, "%", ")", ",", "duration", "=", pJob->duration, "s", ",", "elapsed", "=", GetElapsedTime(), "s");
+      });
     }
-    time_point end = GetCurrentTime();
+    double cost = CostFunction(pNtk);
-    double elapsed_seconds = Duration(start, end);
+    double duration = GetElapsedTime();
-    if(nVerbose) {
+    Print(0, "\n", "stats summary", ":");
-      std::cout << "elapsed: " << std::fixed << std::setprecision(3) << elapsed_seconds << "s" << std::endl;
+    for(std::string key: vStatsSummaryKeys) {
+      Print(0, "\t", SW{30, true}, key, ":", SW{10}, mStatsSummary[key]);
     }
+    Print(0, "", "runtime summary", ":");
+    for(std::string key: vTimesSummaryKeys) {
+      Print(0, "\t", SW{30, true}, key, ":", mTimesSummary[key], "s", "(", 100 * mTimesSummary[key] / duration, "%", ")");
+    }
+    Print(0, "", "end", ":", "cost", "=", cost, "(", 100 * (cost - costStart) / costStart, "%", ")", ",", "time", "=", duration, "s");
   }
 
   /* }}} */

src/opt/rrr/rrrSimulator.h

@@ -29,6 +29,8 @@ namespace rrr {
     int nWords;
 
     // data
+    bool fGenerated;
+    bool fInitialized;
     int target; // node for which the careset has been computed
     std::vector<word> vValues;
     std::vector<word> vValues2; // simulation with an inverter
@@ -46,9 +48,14 @@ namespace rrr {
     // backups
     std::vector<Simulator> vBackups;
 
-    // statistics
+    // stats
-    int nAdds;
+    int nCex;
-    int nResets;
+    int nDiscarded;
+    int nPackedCountOld;
+    std::vector<int> vPackedCount;
+    std::vector<int> vPackedCountEvicted;
+    double durationSimulation;
+    double durationCare;
     
     // vector computations
     void Clear(int n, itr x) const;
@@ -77,6 +84,9 @@ namespace rrr {
     // careset computation
     void ComputeCare(int id);
 
+    // preparation
+    void Initialize();
+
     // save & load
     void Save(int slot);
     void Load(int slot);
@@ -85,8 +95,7 @@ namespace rrr {
     // constructors
     Simulator();
     Simulator(Parameter const *pPar);
-    ~Simulator();
+    void AssignNetwork(Ntk *pNtk_, bool fReuse);
-    void UpdateNetwork(Ntk *pNtk_, bool fSame);
 
     // checks
     bool CheckRedundancy(int id, int idx);
@@ -94,6 +103,11 @@ namespace rrr {
 
     // cex
     void AddCex(std::vector<VarValue> const &vCex);
+
+    // summary
+    void ResetSummary();
+    summary<int> GetStatsSummary() const;
+    summary<double> GetTimesSummary() const;
   };
 
 
@@ -195,53 +209,71 @@ namespace rrr {
   
   template <typename Ntk>
   void Simulator<Ntk>::ActionCallback(Action const &action) {
-    if(target == -1) {
-      return;
-    }
     switch(action.type) {
     case REMOVE_FANIN:
-      if(action.id == target) {
+      assert(fInitialized);
-        fUpdate = true;
+      if(target != -1) {
-      } else {
+        if(action.id == target) {
-        sUpdates.insert(action.id);
+          fUpdate = true;
+        } else {
+          sUpdates.insert(action.id);
+        }
       }
       break;
     case REMOVE_UNUSED:
       break;
     case REMOVE_BUFFER:
     case REMOVE_CONST:
-      if(action.id == target) {
+      if(fInitialized) {
-        if(fUpdate) {
+        if(target != -1) {
-          for(int fo: action.vFanouts) {
+          if(action.id == target) {
-            sUpdates.insert(fo);
+            if(fUpdate) {
-          }
+              for(int fo: action.vFanouts) {
-          fUpdate = false;
+                sUpdates.insert(fo);
-        }
+              }
-        target = -1;
+              fUpdate = false;
-      } else {
+            }
-        if(sUpdates.count(action.id)) {
+            target = -1;
-          sUpdates.erase(action.id);
+          } else {
-          for(int fo: action.vFanouts) {
+            if(sUpdates.count(action.id)) {
-            sUpdates.insert(fo);
+              sUpdates.erase(action.id);
+              for(int fo: action.vFanouts) {
+                sUpdates.insert(fo);
+              }
+            }
           }
         }
       }
       break;
     case ADD_FANIN:
-      if(action.id == target) {
+      assert(fInitialized);
-        fUpdate = true;
+      if(target != -1) {
-      } else {
+        if(action.id == target) {
-        sUpdates.insert(action.id);
+          fUpdate = true;
+        } else {
+          sUpdates.insert(action.id);
+        }
       }
       break;
     case TRIVIAL_COLLAPSE:
       break;
     case TRIVIAL_DECOMPOSE:
-      vValues.resize(nWords * pNtk->GetNumNodes());
+      if(fInitialized) {
-      SimulateNode(vValues, action.fi);
+        if(target != -1) {
+          vValues.resize(nWords * pNtk->GetNumNodes());
+          SimulateNode(vValues, action.fi);
+          // time of this simulation is not measured for simplicity sake
+        }
+      }
       break;
     case SORT_FANINS:
       break;
+    case READ:
+      fInitialized = false;
+      if(action.fNew) {
+        fGenerated = false;
+      }
+      break;
     case SAVE:
       Save(action.idx);
       break;
@@ -345,6 +377,7 @@ namespace rrr {
   
   template <typename Ntk>
   void Simulator<Ntk>::Simulate() {
+    time_point timeStart = GetCurrentTime();
     if(nVerbose) {
       std::cout << "simulating" << std::endl;
     }
@@ -356,10 +389,12 @@ namespace rrr {
         std::cout << std::endl;
       }
     });
+    durationSimulation += Duration(timeStart, GetCurrentTime());
   }
   
   template <typename Ntk>
   void Simulator<Ntk>::Resimulate() {
+    time_point timeStart = GetCurrentTime();
     if(nVerbose) {
       std::cout << "resimulating" << std::endl;
     }
@@ -382,10 +417,12 @@ namespace rrr {
       }
     });
     */
+    durationSimulation += Duration(timeStart, GetCurrentTime());
   }
 
   template <typename Ntk>
   void Simulator<Ntk>::SimulateOneWord(int offset) {
+    time_point timeStart = GetCurrentTime();
     if(nVerbose) {
       std::cout << "simulating word " << offset << std::endl;
     }
@@ -397,6 +434,7 @@ namespace rrr {
         std::cout << std::endl;
       }
     });
+    durationSimulation += Duration(timeStart, GetCurrentTime());
   }
 
   /* }}} */
@@ -440,6 +478,7 @@ namespace rrr {
       sUpdates.clear();
     }
     target = id;
+    time_point timeStart = GetCurrentTime();
     if(nVerbose) {
       std::cout << "computing careset of " << target << std::endl;
     }
@@ -450,6 +489,7 @@ namespace rrr {
         Print(nWords, care.begin());
         std::cout << std::endl;
       }
+      durationCare += Duration(timeStart, GetCurrentTime());
       return;
     }
     vValues2 = vValues;
@@ -484,6 +524,36 @@ namespace rrr {
       Print(nWords, care.begin());
       std::cout << std::endl;
     }
+    durationCare += Duration(timeStart, GetCurrentTime());
+  }
+  
+  /* }}} */
+
+  /* {{{ Preparation */
+
+  template <typename Ntk>
+  void Simulator<Ntk>::Initialize() {
+    if(!fGenerated) {
+      // TODO: reset nWords to default here maybe, if such a mechanism that changes nWords has been implemneted
+      vValues.resize(nWords * pNtk->GetNumNodes());
+      iPivot = 0;
+      vAssignedStimuli.clear();
+      vAssignedStimuli.resize(nWords * pNtk->GetNumPis());
+      for(int count: vPackedCount) {
+        if(count) {
+          vPackedCountEvicted.push_back(count);
+        }
+      }
+      vPackedCount.clear();
+      vPackedCount.resize(nWords * 64);
+      GenerateRandomStimuli();
+      fGenerated = true;
+    } else {
+      // use same nWords as we are reusing patterns even if nWords has changed
+      vValues.resize(nWords * pNtk->GetNumNodes());
+    }
+    Simulate();
+    fInitialized = true;
   }
 
   /* }}} */
@@ -517,6 +587,12 @@ namespace rrr {
     vBackups[slot].iPivot = iPivot;
     vBackups[slot].vAssignedStimuli = vAssignedStimuli;
     target = vBackups[slot].target; // assigned to -1 when careset needs updating
+    if(!fKeepStimula) {
+      vBackups[slot].nCex = nCex;
+      vBackups[slot].nPackedCountOld = nPackedCountOld;
+      vBackups[slot].vPackedCount = vPackedCount;
+      vBackups[slot].vPackedCountEvicted = vPackedCountEvicted;
+    }
   }
 
   template <typename Ntk>
@@ -532,6 +608,11 @@ namespace rrr {
       care    = vBackups[slot].care;
       iPivot  = vBackups[slot].iPivot;
       vAssignedStimuli = vBackups[slot].vAssignedStimuli;
+      nDiscarded += nCex - vBackups[slot].nCex;
+      nCex = vBackups[slot].nCex;
+      nPackedCountOld = vBackups[slot].nPackedCountOld;
+      vPackedCount = vBackups[slot].vPackedCount;
+      vPackedCountEvicted = vBackups[slot].vPackedCountEvicted;
       tmp.resize(nWords);
     } else {
       std::vector<int> vOffsets;
@@ -567,7 +648,7 @@ namespace rrr {
           }
         }
       } else {
-        // when nWords has changed
+        // TODO: when nWords has changed
         assert(0);
       }
     }
@@ -582,11 +663,12 @@ namespace rrr {
     pNtk(NULL),
     nVerbose(0),
     nWords(0),
+    fGenerated(false),
+    fInitialized(false),
     target(-1),
     iPivot(0),
-    fUpdate(false),
+    fUpdate(false) {
-    nAdds(0),
+    ResetSummary();
-    nResets(0) {
   }
   
   template <typename Ntk>
@@ -594,38 +676,27 @@ namespace rrr {
     pNtk(NULL),
     nVerbose(pPar->nSimulatorVerbose),
     nWords(pPar->nWords),
+    fGenerated(false),
+    fInitialized(false),
     target(-1),
     iPivot(0),
-    fUpdate(false),
+    fUpdate(false) {
-    nAdds(0),
-    nResets(0) {
     care.resize(nWords);
     tmp.resize(nWords);
+    ResetSummary();
   }
 
   template <typename Ntk>
-  Simulator<Ntk>::~Simulator() {
+  void Simulator<Ntk>::AssignNetwork(Ntk *pNtk_, bool fReuse) {
-    if(pNtk) {
+    if(!fReuse) {
-      std::cout << "simulator stats: added CEXs = " << nAdds << ", resets = " << nResets << std::endl;
+      fGenerated = false;
     }
-  }
+    fInitialized = false;
-
-  template <typename Ntk>
-  void Simulator<Ntk>::UpdateNetwork(Ntk *pNtk_, bool fSame) {
-    pNtk = pNtk_;
-    pNtk->AddCallback(std::bind(&Simulator<Ntk>::ActionCallback, this, std::placeholders::_1));
-    // TODO: what if nWords has changed? shall we reset it to default?
-    vValues.resize(nWords * pNtk->GetNumNodes());
     target = -1;
     fUpdate = false;
     sUpdates.clear();
-    if(!fSame) { // reset stimuli if network function changed
+    pNtk = pNtk_;
-      iPivot = 0;
+    pNtk->AddCallback(std::bind(&Simulator<Ntk>::ActionCallback, this, std::placeholders::_1));
-      vAssignedStimuli.clear();
-      vAssignedStimuli.resize(nWords * pNtk->GetNumPis());
-      GenerateRandomStimuli();
-    }
-    Simulate();
   }
 
   /* }}} */
@@ -634,6 +705,9 @@ namespace rrr {
   
   template <typename Ntk>
   bool Simulator<Ntk>::CheckRedundancy(int id, int idx) {
+    if(!fInitialized) {
+      Initialize();
+    }
     ComputeCare(id);
     switch(pNtk->GetNodeType(id)) {
     case AND: {
@@ -671,6 +745,9 @@ namespace rrr {
 
   template <typename Ntk>
   bool Simulator<Ntk>::CheckFeasibility(int id, int fi, bool c) {
+    if(!fInitialized) {
+      Initialize();
+    }
     ComputeCare(id);
     switch(pNtk->GetNodeType(id)) {
     case AND: {
@@ -768,6 +845,7 @@ namespace rrr {
       if(nVerbose) {
         std::cout << "fusing into stimulus word " << iWord << " bit " << iBit << std::endl;
       }
+      vPackedCount[iWord * 64 + iBit]++;
     } else {
       // no bits are compatible, so reset at pivot
       iWord = iPivot / 64;
@@ -775,6 +853,11 @@ namespace rrr {
       if(nVerbose) {
         std::cout << "resetting stimulus word " << iWord << " bit " << iBit << std::endl;
       }
+      if(vPackedCount[iWord * 64 + iBit]) {
+        // this can be zero only when stats has been reset
+        vPackedCountEvicted.push_back(vPackedCount[iWord * 64 + iBit]);
+      }
+      vPackedCount[iWord * 64 + iBit] = 1;
       word mask = 1ull << iBit;
       for(int idx = 0; idx < pNtk->GetNumPis(); idx++) {
         vAssignedStimuli[idx * nWords + iWord] &= ~mask;
@@ -783,7 +866,6 @@ namespace rrr {
       if(iPivot == 64 * nWords) {
         iPivot = 0;
       }
-      nResets++;
     }
     // update stimulus
     for(int idx: vCarePiIdxs) {
@@ -808,6 +890,7 @@ namespace rrr {
     // simulate
     SimulateOneWord(iWord);
     // recompute care with new stimulus
+    time_point timeStart = GetCurrentTime();
     if(target != -1 && !pNtk->IsPoDriver(target)) {
       if(nVerbose) {
         std::cout << "recomputing careset of " << target << std::endl;
@@ -838,11 +921,57 @@ namespace rrr {
         std::cout << std::endl;
       }
     }
-    nAdds++;
+    durationCare += Duration(timeStart, GetCurrentTime());
+    nCex++;
   }
   
   /* }}} */
 
+  /* {{{ Summary */
+  
+  template <typename Ntk>
+  void Simulator<Ntk>::ResetSummary() {
+    nCex = 0;
+    nDiscarded = 0;
+    nPackedCountOld = 0;
+    for(int count: vPackedCount) {
+      if(count) {
+        nPackedCountOld++;
+      }
+    }
+    vPackedCountEvicted.clear();
+    durationSimulation = 0;
+    durationCare = 0;
+  };
+  
+  template <typename Ntk>
+  summary<int> Simulator<Ntk>::GetStatsSummary() const {
+    summary<int> v;
+    v.emplace_back("sim cex", nCex);
+    if(!fKeepStimula) {
+      v.emplace_back("sim discarded cex", nDiscarded);
+    }
+    int nPackedCount = vPackedCountEvicted.size() - nPackedCountOld;
+    for(int count: vPackedCount) {
+      if(count) {
+        nPackedCount++;
+      }
+    }
+    v.emplace_back("sim packed pattern", nPackedCount);
+    v.emplace_back("sim evicted pattern", vPackedCountEvicted.size());
+    return v;
+  };
+  
+  template <typename Ntk>
+  summary<double> Simulator<Ntk>::GetTimesSummary() const {
+    summary<double> v;
+    v.emplace_back("sim simulation", durationSimulation);
+    v.emplace_back("sim care computation", durationCare);
+    return v;
+  };
+  
+  /* }}} */
+  
 }
 
 ABC_NAMESPACE_CXX_HEADER_END

src/opt/rrr/rrrTypes.h

@@ -39,6 +39,7 @@ namespace rrr {
     TRIVIAL_COLLAPSE,
     TRIVIAL_DECOMPOSE,
     SORT_FANINS,
+    READ,
     SAVE,
     LOAD,
     POP_BACK,
@@ -51,6 +52,7 @@ namespace rrr {
     int idx = -1;
     int fi = -1;
     bool c = false;
+    bool fNew = false;
     std::vector<int> vFanins;
     std::vector<int> vIndices;
     std::vector<int> vFanouts;
@@ -60,6 +62,9 @@ namespace rrr {
   using clock_type = std::chrono::steady_clock;
   using time_point = std::chrono::time_point<clock_type>;
 
+  template <typename T>
+  using summary = std::vector<std::pair<std::string, T>>;
+
 }
 
 ABC_NAMESPACE_CXX_HEADER_END

src/opt/rrr/rrrUtils.h

@@ -97,7 +97,8 @@ namespace rrr {
   /* {{{ Print next */
 
   struct SW {
-    int width;
+    int width = 0;
+    bool left = false;
   };
 
   struct NS {}; // no space
@@ -107,6 +108,16 @@ namespace rrr {
   template <typename T, typename... Args>
   void PrintNext(std::ostream &os, T t, Args... args);
   
+  static inline void PrintNext(std::ostream &os, int t) {
+    os << std::setw(4) << t;
+  }
+
+  template <typename... Args>
+  static inline void PrintNext(std::ostream &os, int t, Args... args) {
+    os << std::setw(4) << t << " ";
+    PrintNext(os, args...);
+  }
+
   static inline void PrintNext(std::ostream &os, bool arg) {
     os << arg;
   }
@@ -121,16 +132,6 @@ namespace rrr {
     PrintNext(os, args...);
   }
   
-  static inline void PrintNext(std::ostream &os, int t) {
-    os << std::setw(4) << t;
-  }
-
-  template <typename... Args>
-  static inline void PrintNext(std::ostream &os, int t, Args... args) {
-    os << std::setw(4) << t << " ";
-    PrintNext(os, args...);
-  }
-
   static inline void PrintNext(std::ostream &os, double t) {
     os << std::fixed << std::setprecision(2) << std::setw(8) << t;
   }
@@ -143,12 +144,24 @@ namespace rrr {
 
   template <typename T>
   static inline void PrintNext(std::ostream &os, SW sw, T arg) {
+    if(sw.left) {
+      os << std::left;
+    }
     os << std::setw(sw.width) << arg;
+    if(sw.left) {
+      os << std::right;
+    }
   }
 
   template <typename T, typename... Args>
   static inline void PrintNext(std::ostream &os, SW sw, T arg, Args... args) {
+    if(sw.left) {
+      os << std::left;
+    }
     os << std::setw(sw.width) << arg << " ";
+    if(sw.left) {
+      os << std::right;
+    }
     PrintNext(os, args...);
   }
 
@@ -161,24 +174,20 @@ namespace rrr {
   
   template <typename T>
   static inline void PrintNext(std::ostream& os, std::vector<T> const &arg) {
-    std::string delim;
+    os << "[ ";
-    os << "[";
     for(T const &e: arg) {
-      os << delim;
       PrintNext(os, e);
-      delim = ", ";
+      os << " ";
     }
     os << "]";
   }
 
   template <typename T, typename... Args>
   static inline void PrintNext(std::ostream& os, std::vector<T> const &arg, Args... args) {
-    std::string delim;
+    os << "[ ";
-    os << "[";
     for(T const &e: arg) {
-      os << delim;
       PrintNext(os, e);
-      delim = ", ";
+      os << " ";
     }
     os << "] ";
     PrintNext(os, args...);
@@ -186,24 +195,20 @@ namespace rrr {
 
   template <typename T>
   static inline void PrintNext(std::ostream& os, std::set<T> const &arg) {
-    std::string delim;
+    os << "{ ";
-    os << "{";
     for(T const &e: arg) {
-      os << delim;
       PrintNext(os, e);
-      delim = ", ";
+      os << " ";
     }
     os << "}";
   }
 
   template <typename T, typename... Args>
   static inline void PrintNext(std::ostream& os, std::set<T> const &arg, Args... args) {
-    std::string delim;
+    os << "{ ";
-    os << "{";
     for(T const &e: arg) {
-      os << delim;
       PrintNext(os, e);
-      delim = ", ";
+      os << " ";
     }
     os << "} ";
     PrintNext(os, args...);
@@ -222,6 +227,14 @@ namespace rrr {
   
   /* }}} */
 
+  /* {{{ Print others */
+
+  static inline void PrintWarning(std::string message) {
+    std::cerr << "[w] " << message << std::endl;
+  }
+
+  /* }}} */
+  
   /* {{{ Combination */
 
   bool ForEachCombinationStopRec(std::vector<int> &v, int n, int k, std::function<bool(std::vector<int> const &)> const &func) {
@@ -306,6 +319,8 @@ namespace rrr {
       return "trivial decompose";
     case SORT_FANINS:
       return "sort fanins";
+    case READ:
+      return "read";
     case SAVE:
       return "save";
     case LOAD:
@@ -323,32 +338,35 @@ namespace rrr {
   static inline std::stringstream GetActionDescription(Action const &action) {
     std::stringstream ss;
     ss << GetActionTypeCstr(action);
-    std::string delim = ": ";
+    std::string delim = " : ";
     if(action.id != -1) {
       ss << delim;
       PrintNext(ss, "node", action.id);
-      delim = ", ";
+      delim = " , ";
     }
     if(action.fi != -1) {
       ss << delim;
       PrintNext(ss, "fanin", (bool)action.c, action.fi);
-      delim = ", ";
+      delim = " , ";
     }
     if(action.idx != -1) {
       ss << delim;
       PrintNext(ss, "index", action.idx);
     }
+    if(action.fNew) {
+      ss << " new";
+    }
     ss << std::endl;
     if(!action.vFanins.empty()) {
-      ss << "fanins: ";
+      ss << "fanins : ";
       PrintNext(ss, action.vFanins);
     }
     if(!action.vIndices.empty()) {
-      ss << "indices: ";
+      ss << "indices : ";
       PrintNext(ss, action.vIndices);
     }
     if(!action.vFanouts.empty()) {
-      ss << "fanouts: ";
+      ss << "fanouts : ";
       PrintNext(ss, action.vFanouts);
     }
     return ss;