diff --git a/src/aig/gia/giaRrr.cpp b/src/aig/gia/giaRrr.cpp index 1eccd4dc23..8483641b26 100644 --- a/src/aig/gia/giaRrr.cpp +++ b/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; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2875b3a1be..b4e47da0b5 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -45457,7 +45457,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 ) { @@ -45576,6 +45576,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 ); @@ -45599,10 +45644,10 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv ) 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 : 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-D num : distance between nodes (0 = no limit) [default = %d]\n", nDistance ); + Abc_Print( -2, "\t-K num : maximum partition size (0 = no partitioning) [default = %d]\n", nPartitionSize ); + Abc_Print( -2, "\t-L num : minimum partition size [default = %d]\n", nPartitionSizeMin ); + Abc_Print( -2, "\t-B num : maximum number of partitions in parallel [default = %d]\n", nParallelPartitions ); + 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 ); @@ -45617,7 +45662,7 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv ) 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; diff --git a/src/opt/rrr/rrrAbc.h b/src/opt/rrr/rrrAbc.h index 307d5e0d05..5df597a548 100644 --- a/src/opt/rrr/rrrAbc.h +++ b/src/opt/rrr/rrrAbc.h @@ -29,9 +29,11 @@ namespace rrr { } template - 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 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); + pNtk->Read(Abc_FrameReadGia(pAbc), GiaReader, false); } } diff --git a/src/opt/rrr/rrrAnalyzer.h b/src/opt/rrr/rrrAnalyzer.h index 0689a3d115..75bc241ac4 100644 --- a/src/opt/rrr/rrrAnalyzer.h +++ b/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 GetStatsSummary() const; + summary GetTimesSummary() const; }; /* {{{ Constructors */ @@ -39,12 +44,12 @@ namespace rrr { sim(pPar), sol(pPar) { } - + template - void Analyzer::UpdateNetwork(Ntk *pNtk_, bool fSame) { + void Analyzer::AssignNetwork(Ntk *pNtk_, bool fReuse) { pNtk = pNtk_; - sim.UpdateNetwork(pNtk, fSame); - sol.UpdateNetwork(pNtk, fSame); + sim.AssignNetwork(pNtk, fReuse); + 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,11 +102,41 @@ 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 + void Analyzer::ResetSummary() { + sim.ResetSummary(); + sol.ResetSummary(); + } + + template + summary Analyzer::GetStatsSummary() const { + summary v = sim.GetStatsSummary(); + summary v2 = sol.GetStatsSummary(); + v.insert(v.end(), v2.begin(), v2.end()); + return v; + } + + template + summary Analyzer::GetTimesSummary() const { + summary v = sim.GetTimesSummary(); + summary v2 = sol.GetTimesSummary(); + v.insert(v.end(), v2.begin(), v2.end()); + return v; + } + + /* }}} */ } diff --git a/src/opt/rrr/rrrAndNetwork.h b/src/opt/rrr/rrrAndNetwork.h index f39bbdc4d0..036b8cd43a 100644 --- a/src/opt/rrr/rrrAndNetwork.h +++ b/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 - 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 - void AndNetwork::Read(Ntk *pFrom, Reader &reader) { - Clear(); + void AndNetwork::Read(Ntk *pFrom, Reader &reader, bool fNew) { + 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 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; } diff --git a/src/opt/rrr/rrrBddAnalyzer.h b/src/opt/rrr/rrrBddAnalyzer.h index a9112a9ba8..0f5d88d684 100644 --- a/src/opt/rrr/rrrBddAnalyzer.h +++ b/src/opt/rrr/rrrBddAnalyzer.h @@ -22,6 +22,7 @@ namespace rrr { int nVerbose; // data + bool fInitialized; NewBdd::Man *pBdd; int target; std::vector vFs; @@ -35,6 +36,14 @@ namespace rrr { // backups std::vector 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 GetStatsSummary() const; + summary GetTimesSummary() const; }; /* {{{ BDD utils */ @@ -163,103 +181,136 @@ namespace rrr { void BddAnalyzer::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]) { - for(int fi: action.vFanins) { - vGUpdates[fi] = true; + 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]); } - 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(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]); } - 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; + 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]); } - 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: { - if(vGUpdates[action.fi] || vCUpdates[action.fi]) { - vCUpdates[action.id] = true; + case TRIVIAL_COLLAPSE: + if(fInitialized) { + if(vGUpdates[action.fi] || vCUpdates[action.fi]) { + vCUpdates[action.id] = true; + } + std::vector::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); } - std::vector::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); - Assign(vGs[action.fi], vGs[action.id]); - std::vector::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 vCs = vvCs[action.id]; - vvCs[action.id].clear(); - for(int index: action.vIndices) { - vvCs[action.id].push_back(vCs[index]); + 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::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]; } - if(!fResim && target != -1 && target != action.id) { - pNtk->ForEachTfo(target, false, [&](int fo) { - if(fResim) { - return; - } - if(fo == action.id) { - fResim = true; - } - }); + break; + case SORT_FANINS: + if(fInitialized) { + std::vector 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 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; } - vCUpdates[action.id] = true; break; - } + case READ: + Reset(!action.fNew); + break; case SAVE: Save(action.idx); break; @@ -306,6 +357,7 @@ namespace rrr { template void BddAnalyzer::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 void BddAnalyzer::Cspf(int id, bool fC) { + time_point timeStart = GetCurrentTime(); if(id != -1) { pNtk->ForEachTfoReverse(id, false, [&](int fo) { CspfNode(fo); @@ -427,10 +481,82 @@ namespace rrr { CspfNode(id); }); } + durationPf += Duration(timeStart, GetCurrentTime()); } /* }}} */ + /* {{{ Preparation */ + + template + void BddAnalyzer::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 + void BddAnalyzer::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; + } + + /* }}} */ + /* {{{ Save & load */ template @@ -468,7 +594,7 @@ namespace rrr { vBackups.pop_back(); } - /* }}} Save & load end */ + /* }}} */ /* {{{ Constructors */ @@ -476,94 +602,35 @@ namespace rrr { BddAnalyzer::BddAnalyzer() : pNtk(NULL), nVerbose(0), + fInitialized(false), pBdd(NULL), target(-1), fResim(false) { + ResetSummary(); } template BddAnalyzer::BddAnalyzer(Parameter const *pPar) : pNtk(NULL), nVerbose(pPar->nAnalyzerVerbose), + fInitialized(false), pBdd(NULL), target(-1), fResim(false) { + ResetSummary(); + } + + template + BddAnalyzer::~BddAnalyzer() { + Reset(); } template - void BddAnalyzer::UpdateNetwork(Ntk *pNtk_, bool fSame) { - // clear - while(!vBackups.empty()) { - PopBack(); - } - DelVec(vFs); - DelVec(vGs); - DelVecVec(vvCs); + void BddAnalyzer::AssignNetwork(Ntk *pNtk_, bool fReuse) { + Reset(fReuse); 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::ActionCallback, this, std::placeholders::_1)); } - - template - BddAnalyzer::~BddAnalyzer() { - while(!vBackups.empty()) { - PopBack(); - } - DelVec(vFs); - DelVec(vGs); - DelVecVec(vvCs); - if(pBdd) { - pBdd->PrintStats(); - } - delete pBdd; - } /* }}} */ @@ -571,20 +638,22 @@ namespace rrr { template bool BddAnalyzer::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) { - std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is redundant" << std::endl; - } - return true; + fRedundant = 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 bool BddAnalyzer::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) { - std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is feasible" << std::endl; - } - return true; + fFeasible = 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 + void BddAnalyzer::ResetSummary() { + if(pBdd) { + nNodesOld = pBdd->GetNumTotalCreatedNodes(); + } else { + nNodesOld = 0; + } + nNodesAccumulated = 0; + durationSimulation = 0; + durationPf = 0; + durationCheck = 0; + durationReorder = 0; + } + + template + summary BddAnalyzer::GetStatsSummary() const { + summary v; + v.emplace_back("bdd node", pBdd->GetNumTotalCreatedNodes() - nNodesOld + nNodesAccumulated); + return v; + } + + template + summary BddAnalyzer::GetTimesSummary() const { + summary 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; } /* }}} */ diff --git a/src/opt/rrr/rrrBddManager.h b/src/opt/rrr/rrrBddManager.h index 1227147c01..af0f8b10fc 100644 --- a/src/opt/rrr/rrrBddManager.h +++ b/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; + } }; } diff --git a/src/opt/rrr/rrrBddMspfAnalyzer.h b/src/opt/rrr/rrrBddMspfAnalyzer.h index 400fd9e6ca..3119c4605f 100644 --- a/src/opt/rrr/rrrBddMspfAnalyzer.h +++ b/src/opt/rrr/rrrBddMspfAnalyzer.h @@ -22,6 +22,7 @@ namespace rrr { int nVerbose; // data + bool fInitialized; NewBdd::Man *pBdd; std::vector vFs; std::vector vGs; @@ -35,6 +36,14 @@ namespace rrr { // backups std::vector 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 GetStatsSummary() const; + summary GetTimesSummary() const; }; /* {{{ BDD utils */ @@ -165,6 +183,7 @@ namespace rrr { void BddMspfAnalyzer::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]) { - for(int fi: action.vFanins) { - vGUpdates[fi] = true; + 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]); } - 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(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]); } - 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; + 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; } - } - 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: { - if(vGUpdates[action.fi] || vCUpdates[action.fi]) { - vCUpdates[action.id] = true; + case TRIVIAL_COLLAPSE: + if(fInitialized) { + if(vGUpdates[action.fi] || vCUpdates[action.fi]) { + vCUpdates[action.id] = true; + } + std::vector::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); } - std::vector::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::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))); + 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::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); } - 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; } - } 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; } - 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: { - std::vector vCs = vvCs[action.id]; - vvCs[action.id].clear(); - for(int index: action.vIndices) { - vvCs[action.id].push_back(vCs[index]); + case SORT_FANINS: + if(fInitialized) { + std::vector 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 void BddMspfAnalyzer::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 void BddMspfAnalyzer::Mspf(int id, bool fC) { + time_point timeStart = GetCurrentTime(); if(id != -1) { pNtk->ForEachTfoReverse(id, false, [&](int fo) { MspfNode(fo); @@ -524,10 +560,82 @@ namespace rrr { MspfNode(id); }); } + durationPf += Duration(timeStart, GetCurrentTime()); } /* }}} */ + /* {{{ Preparation */ + + template + void BddMspfAnalyzer::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 + void BddMspfAnalyzer::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; + } + + /* }}} */ + /* {{{ Save & load */ template @@ -575,113 +683,56 @@ namespace rrr { BddMspfAnalyzer::BddMspfAnalyzer() : pNtk(NULL), nVerbose(0), - pBdd(NULL) { + fInitialized(false), + pBdd(NULL), + fUpdate(false) { + ResetSummary(); } template BddMspfAnalyzer::BddMspfAnalyzer(Parameter const *pPar) : pNtk(NULL), nVerbose(pPar->nAnalyzerVerbose), + fInitialized(false), pBdd(NULL), fUpdate(false) { + ResetSummary(); } template - void BddMspfAnalyzer::UpdateNetwork(Ntk *pNtk_, bool fSame) { - // clear - while(!vBackups.empty()) { - PopBack(); - } - DelVec(vFs); - DelVec(vGs); - DelVecVec(vvCs); + BddMspfAnalyzer::~BddMspfAnalyzer() { + Reset(); + } + + template + void BddMspfAnalyzer::AssignNetwork(Ntk *pNtk_, bool fReuse) { + Reset(fReuse); 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::ActionCallback, this, std::placeholders::_1)); } - template - BddMspfAnalyzer::~BddMspfAnalyzer() { - while(!vBackups.empty()) { - PopBack(); - } - DelVec(vFs); - DelVec(vGs); - DelVecVec(vvCs); - if(pBdd) { - pBdd->PrintStats(); - } - delete pBdd; - } - /* }}} */ /* {{{ Checks */ template bool BddMspfAnalyzer::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) { - std::cout << "node " << id << " fanin " << (pNtk->GetCompl(id, idx)? "!": "") << pNtk->GetFanin(id, idx) << " index " << idx << " is redundant" << std::endl; - } - return true; + fRedundant = 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 bool BddMspfAnalyzer::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) { - std::cout << "node " << id << " fanin " << (c? "!": "") << fi << " is feasible" << std::endl; - } + fFeasible = true; 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 + void BddMspfAnalyzer::ResetSummary() { + if(pBdd) { + nNodesOld = pBdd->GetNumTotalCreatedNodes(); + } else { + nNodesOld = 0; + } + nNodesAccumulated = 0; + durationSimulation = 0; + durationPf = 0; + durationCheck = 0; + durationReorder = 0; + } + + template + summary BddMspfAnalyzer::GetStatsSummary() const { + summary v; + v.emplace_back("bdd node", pBdd->GetNumTotalCreatedNodes() - nNodesOld + nNodesAccumulated); + return v; + } + + template + summary BddMspfAnalyzer::GetTimesSummary() const { + summary 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; } /* }}} */ diff --git a/src/opt/rrr/rrrLevelBasePartitioner.h b/src/opt/rrr/rrrLevelBasePartitioner.h index 5225cc5a77..5693c38e5e 100644 --- a/src/opt/rrr/rrrLevelBasePartitioner.h +++ b/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 - void LevelBasePartitioner::UpdateNetwork(Ntk *pNtk_) { + void LevelBasePartitioner::AssignNetwork(Ntk *pNtk_) { pNtk = pNtk_; assert(mSubNtk2Io.empty()); assert(sBlocked.empty()); diff --git a/src/opt/rrr/rrrOptimizer.h b/src/opt/rrr/rrrOptimizer.h index 8314562958..eacb0a0ad1 100644 --- a/src/opt/rrr/rrrOptimizer.h +++ b/src/opt/rrr/rrrOptimizer.h @@ -21,7 +21,7 @@ namespace rrr { using citr = std::vector::const_iterator; using ritr = std::vector::reverse_iterator; using critr = std::vector::const_reverse_iterator; - + // pointer to network Ntk *pNtk; @@ -35,7 +35,7 @@ namespace rrr { bool fCompatible; bool fGreedy; seconds nTimeout; // assigned upon Run - std::string strVerbosePrefix; + std::function PrintLine; // data Ana ana; @@ -52,6 +52,11 @@ namespace rrr { int target; std::vector vTfoMarks; + // statistics + struct Stats; + std::map stats; + Stats statsLocal; + // print template 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 T SingleAdd(int id, T begin, T end); int MultiAdd(int id, std::vector const &vCands, int nMax = 0); + void Undo(); // resub void SingleResub(int id, std::vector const &vCands); @@ -108,25 +114,81 @@ namespace rrr { public: // constructors Optimizer(Parameter const *pPar, std::function CostFunction); - void UpdateNetwork(Ntk *pNtk_, bool fSame = false); + void AssignNetwork(Ntk *pNtk_, bool fReuse = false); + void SetPrintLine(std::function const &PrintLine_); // run void Run(int iSeed = 0, seconds nTimeout_ = 0); - + + // summary + void ResetSummary(); + summary GetStatsSummary() const; + summary GetTimesSummary() const; }; - /* {{{ Print */ + /* {{{ Stats */ + + template + struct Optimizer::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 template inline void Optimizer::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...); - std::cout << std::endl; + PrintNext(ss, args...); + PrintLine(ss.str()); } } @@ -136,13 +198,13 @@ namespace rrr { template void Optimizer::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 inline bool Optimizer::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 - bool Optimizer::Reduce() { + bool Optimizer::Reduce(bool fSubRoutine) { + time_point timeStart = GetCurrentTime(); bool fReduced = false; std::vector 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 - void Optimizer::RemoveRedundancy() { + bool Optimizer::RemoveRedundancy() { + time_point timeStart = GetCurrentTime(); + bool fReduced = false; if(fCompatible) { - while(Reduce()) { + while(Reduce(true)) { + fReduced = true; SortFanins(); } - return; - } - std::vector vInts = pNtk->GetInts(); - for(critr it = vInts.rbegin(); it != vInts.rend();) { - if(!pNtk->IsInt(*it)) { - it++; - continue; - } - if(pNtk->GetNumFanouts(*it) == 0) { - pNtk->RemoveUnused(*it); - it++; - continue; - } - SortFanins(*it); - bool fReduced = ReduceFanins(*it); - if(pNtk->GetNumFanins(*it) <= 1) { - pNtk->Propagate(*it); - } - if(fReduced) { - it = vInts.rbegin(); - } else { - it++; + } else { + std::vector vInts = pNtk->GetInts(); + for(critr it = vInts.rbegin(); it != vInts.rend();) { + if(!pNtk->IsInt(*it)) { + it++; + continue; + } + if(pNtk->GetNumFanouts(*it) == 0) { + pNtk->RemoveUnused(*it); + it++; + continue; + } + SortFanins(*it); + bool fReduced_ = ReduceFanins(*it); + fReduced |= fReduced_; + if(pNtk->GetNumFanins(*it) <= 1) { + pNtk->Propagate(*it); + } + if(fReduced_) { + it = vInts.rbegin(); + } else { + it++; + } } } + time_point timeEnd = GetCurrentTime(); + statsLocal.durationReduce += Duration(timeStart, timeEnd); + return fReduced; } /* @@ -656,6 +733,7 @@ namespace rrr { template template T Optimizer::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 int Optimizer::MultiAdd(int id, std::vector 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++; - if(nAdded == nMax) { + nAddedFis_++; + 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 + void Optimizer::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(id, it, vCands.end()); if(it == vCands.end()) { break; } - Print(1, "cand", *it, "(", int_distance(vCands.begin(), it) + 1, "/", int_size(vCands), "):", "cost", "=", dCost); - RemoveRedundancy(); - mapNewFanins.clear(); - double dNewCost = CostFunction(pNtk); - Print(2, "cost:", dCost, "->", dNewCost); - if(fGreedy) { - if(dNewCost <= dCost) { - pNtk->Save(slot); - dCost = dNewCost; + fAdded = true; + Print(2, "cand", *it, "(", int_distance(vCands.begin(), it) + 1, "/", int_size(vCands), ")", ":", "cost", "=", cost); + if(RemoveRedundancy()) { + double costNew = CostFunction(pNtk); + // stats + statsLocal.nChanged++; + if(costNew < cost) { + statsLocal.nDowns++; + } 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 @@ -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); - RemoveRedundancy(); - mapNewFanins.clear(); - // TODO: we could quit here if nothing has been removed - RemoveRedundancy(); - double dNewCost = CostFunction(pNtk); - Print(1, "cost:", dCost, "->", dNewCost); - if(fGreedy && dNewCost > dCost) { - pNtk->Load(slot); + double cost = CostFunction(pNtk); + if(MultiAdd(id, vCands, nMax)) { + statsLocal.nAdded++; + if(RemoveRedundancy()) { + mapNewFanins.clear(); + RemoveRedundancy(); + double costNew = CostFunction(pNtk); + // stats + 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 - int slot0 = pNtk->Save(); + Print(2, "method", "=", "single"); // collapse pNtk->TrivialCollapse(id); - // save after trivial collapse + // save int slot = pNtk->Save(); - double dCost = CostFunction(pNtk); // remember fanins std::set 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(id, it, vCands.end()); if(it == vCands.end()) { break; } - Print(1, "cand", *it, "(", int_distance(vCands.begin(), it) + 1, "/", int_size(vCands), "):", "cost", "=", dCost); - RemoveRedundancy(); - mapNewFanins.clear(); - double dNewCost = CostFunction(pNtk); - Print(2, "cost:", dCost, "->", dNewCost); - if(dNewCost <= dCost) { - bool fChanged = false; - if(dNewCost < dCost || !pNtk->IsInt(id)) { - fChanged = true; - } else { - std::set sNewFanins = pNtk->GetExtendedFanins(id); - Print(2, "new extended fanins:", sNewFanins); - if(sFanins != sNewFanins) { + fAdded = true; + Print(3, "cand", *it, "(", int_distance(vCands.begin(), it) + 1, "/", int_size(vCands), ")", ":", "cost", "=", cost); + if(RemoveRedundancy()) { + mapNewFanins.clear(); + double costNew = CostFunction(pNtk); + if(costNew <= cost) { + fChanged = false; + if(costNew < cost || !pNtk->IsInt(id)) { fChanged = true; + } else { + std::set sNewFanins = pNtk->GetExtendedFanins(id); + Print(3, "new extended fanins", ":", sNewFanins); + if(sFanins != sNewFanins) { + fChanged = true; + } } - } - if(fChanged) { - if(pNtk->IsInt(id)) { - pNtk->TrivialDecompose(id); + if(fChanged) { + statsLocal.nChanged++; + if(costNew < cost) { + statsLocal.nDowns++; + } else if (costNew == cost) { + statsLocal.nEqs++; + } else { + statsLocal.nUps++; + } + break; } - pNtk->PopBack(); // slot - pNtk->PopBack(); // slot0 - return true; } + pNtk->Load(slot); + } else { + if(fCompatible) { + pNtk->Load(slot); + } else { + Undo(); + } + mapNewFanins.clear(); } - pNtk->Load(slot); } - pNtk->PopBack(); // slot - pNtk->Load(slot0); - pNtk->PopBack(); // slot0 - return false; + if(pNtk->IsInt(id)) { + pNtk->TrivialDecompose(id); + } + pNtk->PopBack(); + if(fTried) { + statsLocal.nTried++; + } + if(fAdded) { + statsLocal.nAdded++; + } + return fChanged; } template @@ -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 sFanins = pNtk->GetExtendedFanins(id); - Print(2, "extended fanins:", sFanins); + Print(3, "extended fanins", ":", sFanins); // collapse pNtk->TrivialCollapse(id); // resub - MultiAdd(id, vCands, nMax); - RemoveRedundancy(); - mapNewFanins.clear(); - // TODO: we could quit here if nothing has been removed - RemoveRedundancy(); - double dNewCost = CostFunction(pNtk); - Print(1, "cost:", dCost, "->", dNewCost); - if(!fGreedy || dNewCost <= dCost) { - bool fChanged = false; - if(dNewCost < dCost || !pNtk->IsInt(id)) { - fChanged = true; - } else { - std::set sNewFanins = pNtk->GetExtendedFanins(id); - Print(2, "new extended fanins:", sNewFanins); - if(sFanins != sNewFanins) { - fChanged = true; + bool fChanged = false; + double cost = CostFunction(pNtk); + if(MultiAdd(id, vCands, nMax)) { + statsLocal.nAdded++; + if(RemoveRedundancy()) { + mapNewFanins.clear(); + RemoveRedundancy(); + double costNew = CostFunction(pNtk); + if(!fGreedy || costNew <= cost) { + fChanged = false; + if(costNew < cost || !pNtk->IsInt(id)) { + fChanged = true; + } else { + std::set 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 { + mapNewFanins.clear(); } - if(fChanged) { - if(pNtk->IsInt(id)) { - pNtk->TrivialDecompose(id); - } - pNtk->PopBack(); - return true; + } + if(fChanged) { + if(pNtk->IsInt(id)) { + pNtk->TrivialDecompose(id); } + } else { + pNtk->Load(slot); } - 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> vsFanins; for(int id: vTargets) { // get candidates @@ -961,7 +1141,7 @@ namespace rrr { std::shuffle(vCands.begin(), vCands.end(), rng); // remember fanins std::set 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 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::ApplyCombinationRandomlyStop(int k, std::function const &)> const &func) { std::vector 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 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 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 vTargets(k); for(int i = 0; i < k; i++) { vTargets[i] = vInts[vIdxs[i]]; @@ -1109,11 +1289,16 @@ namespace rrr { } template - void Optimizer::UpdateNetwork(Ntk *pNtk_, bool fSame) { + void Optimizer::AssignNetwork(Ntk *pNtk_, bool fReuse) { pNtk = pNtk_; target = -1; pNtk->AddCallback(std::bind(&Optimizer::ActionCallback, this, std::placeholders::_1)); - ana.UpdateNetwork(pNtk, fSame); + ana.AssignNetwork(pNtk, fReuse); + } + + template + void Optimizer::SetPrintLine(std::function 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 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 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 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 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: { @@ -1221,6 +1428,46 @@ namespace rrr { } /* }}} */ + + /* {{{ Summary */ + + template + void Optimizer::ResetSummary() { + stats.clear(); + ana.ResetSummary(); + } + + template + summary Optimizer::GetStatsSummary() const { + summary 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 v2 = ana.GetStatsSummary(); + v.insert(v.end(), v2.begin(), v2.end()); + return v; + } + + template + summary Optimizer::GetTimesSummary() const { + summary 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 v2 = ana.GetTimesSummary(); + v.insert(v.end(), v2.begin(), v2.end()); + return v; + } + + /* }}} */ } diff --git a/src/opt/rrr/rrrParameter.h b/src/opt/rrr/rrrParameter.h index e6b5ccb8c9..c80171c430 100644 --- a/src/opt/rrr/rrrParameter.h +++ b/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; diff --git a/src/opt/rrr/rrrPartitioner.h b/src/opt/rrr/rrrPartitioner.h index 16819f0758..da14344fce 100644 --- a/src/opt/rrr/rrrPartitioner.h +++ b/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 - void Partitioner::UpdateNetwork(Ntk *pNtk_) { + void Partitioner::AssignNetwork(Ntk *pNtk_) { pNtk = pNtk_; assert(mSubNtk2Io.empty()); assert(sBlocked.empty()); diff --git a/src/opt/rrr/rrrSatSolver.h b/src/opt/rrr/rrrSatSolver.h index b1bf01f357..1f51017531 100644 --- a/src/opt/rrr/rrrSatSolver.h +++ b/src/opt/rrr/rrrSatSolver.h @@ -28,10 +28,12 @@ namespace rrr { std::vector 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 GetCex(); + + // stats + void ResetSummary(); + summary GetStatsSummary() const; + summary 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), - nCalls(0), - nSats(0), - nUnsats(0) { + fUpdate(false) { + ResetSummary(); } template SatSolver::~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 - void SatSolver::UpdateNetwork(Ntk *pNtk_, bool fSame) { - (void)fSame; - pNtk = pNtk_; + void SatSolver::AssignNetwork(Ntk *pNtk_, bool fReuse) { + (void)fReuse; status = false; target = -1; fUpdate = false; + pNtk = pNtk_; pNtk->AddCallback(std::bind(&SatSolver::ActionCallback, this, std::placeholders::_1)); } @@ -287,11 +297,13 @@ namespace rrr { template SatResult SatSolver::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 SatResult SatSolver::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 + void SatSolver::ResetSummary() { + nCalls = 0; + nSats = 0; + nUnsats = 0; + durationRedundancy = 0; + durationFeasibility = 0; + } + + template + summary SatSolver::GetStatsSummary() const { + summary v; + v.emplace_back("sat call", nCalls); + v.emplace_back("sat satisfiable", nSats); + v.emplace_back("sat unsatisfiable", nUnsats); + return v; + } + + template + summary SatSolver::GetTimesSummary() const { + summary v; + v.emplace_back("sat redundancy", durationRedundancy); + v.emplace_back("sat feasibility", durationFeasibility); + return v; + } + + /* }}} */ + } ABC_NAMESPACE_CXX_HEADER_END diff --git a/src/opt/rrr/rrrScheduler.h b/src/opt/rrr/rrrScheduler.h index ced6da047a..2db2fc4c4e 100644 --- a/src/opt/rrr/rrrScheduler.h +++ b/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 qPendingJobs; Opt *pOpt; // used only in case of single thread execution + std::vector vStatsSummaryKeys; + std::map mStatsSummary; + std::vector vTimesSummaryKeys; + std::map mTimesSummary; #ifdef ABC_USE_PTHREADS bool fTerminate; std::vector 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 + 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 const &func); // thread @@ -79,6 +89,10 @@ namespace rrr { void Thread(Parameter const *pPar); #endif + // summary + template + void AddToSummary(std::vector &keys, std::map &m, summary 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 stats; + summary 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 + template + inline void Scheduler::Print(int nVerboseLevel, std::string prefix, Args... args) { + if(nVerbose <= nVerboseLevel) { + return; + } +#ifdef ABC_USE_PTHREADS + if(fMultiThreading) { + { + std::unique_lock 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 - seconds Scheduler::GetRemainingTime() const { + inline seconds Scheduler::GetRemainingTime() const { if(nTimeout == 0) { return 0; } - time_point current = GetCurrentTime(); - seconds nRemainingTime = nTimeout - DurationInSeconds(start, current); + time_point timeCurrent = GetCurrentTime(); + seconds nRemainingTime = nTimeout - DurationInSeconds(timeStart, timeCurrent); if(nRemainingTime == 0) { // avoid glitch return -1; } return nRemainingTime; } + template + inline double Scheduler::GetElapsedTime() const { + time_point timeCurrent = GetCurrentTime(); + return Duration(timeStart, timeCurrent); + } + /* }}} */ /* {{{ Abc */ @@ -153,8 +208,12 @@ namespace rrr { /* {{{ Run jobs */ template - void Scheduler::RunJob(Opt &opt, Job const *pJob) { - opt.UpdateNetwork(pJob->pNtk); + void Scheduler::RunJob(Opt &opt, Job *pJob) { + 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 dBestCost = dCost; + double cost = pJob->costInitial; + 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); - opt.UpdateNetwork(pJob->pNtk, true); - if(nVerbose) { - std::cout << "hop " << std::setw(3) << i << ": cost = " << dCost << std::endl; - } + cost = CostFunction(pJob->pNtk); + Print(1, pJob->prefix, "hop", i, ":", "cost", "=", cost); } 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); - if(nVerbose) { - std::cout << "\tite " << std::setw(3) << j << ": cost = " << dNewCost << std::endl; - } - if(dNewCost < dCost) { - dCost = dNewCost; - opt.UpdateNetwork(pJob->pNtk, true); + double costNew = CostFunction(pJob->pNtk); + Print(1, pJob->prefix, "ite", j, ":", "cost", "=", costNew); + if(costNew < cost) { + cost = costNew; } else { break; } } - if(dCost < dBestCost) { - dBestCost = dCost; + if(cost < costBest) { + 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) { - std::cout << "ite " << std::setw(6) << i << ": cost = " << CostFunction(pJob->pNtk) << std::endl; - } + Print(1, pJob->prefix, "ite", i, ":", "cost", "=", CostFunction(pJob->pNtk)); // 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) { - std::cout << "\trrr " << std::setw(6) << j << ": cost = " << CostFunction(pJob->pNtk) << std::endl; - } + Print(1, pJob->prefix, "rrr", j, ":", "cost", "=", CostFunction(pJob->pNtk)); } // eval - double dNewCost = CostFunction(pJob->pNtk); - if(dNewCost < dCost) { - dCost = dNewCost; + double costNew = CostFunction(pJob->pNtk); + if(costNew < cost) { + 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 - void Scheduler::CreateJob(Ntk *pNtk_, int iSeed_) { - Job *pJob = new Job(nCreatedJobs++, pNtk_, iSeed_); + typename Scheduler::Job *Scheduler::CreateJob(Ntk *pNtk_, int iSeed_, double cost) { + 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 @@ -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 + template + void Scheduler::AddToSummary(std::vector &keys, std::map &m, summary const &result) const { + std::vector::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 @@ -439,74 +507,90 @@ namespace rrr { template void Scheduler::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); - std::cout << "job " << nCreatedJobs - 1 << " created (size = " << pSubNtk->GetNumInts() << ")" << std::endl; + Job *pJob = CreateJob(pSubNtk, iSeed + nCreatedJobs, CostFunction(pSubNtk)); + 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); - if(nVerbose) { - std::cout << "run " << pJob->id << ": cost = " << dNewCost << std::endl; - } - if(dNewCost < dCost) { - dCost = dNewCost; + 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"); + if(cost < costBest) { + costBest = cost; *pNtk = *(pJob->pNtk); } delete pJob->pNtk; }); } } else { - CreateJob(pNtk, iSeed); - OnJobEnd([&](Job *pJob) { (void)pJob; }); + CreateJob(pNtk, iSeed, costStart); + 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"); + }); + } + double cost = CostFunction(pNtk); + double duration = GetElapsedTime(); + Print(0, "\n", "stats summary", ":"); + for(std::string key: vStatsSummaryKeys) { + Print(0, "\t", SW{30, true}, key, ":", SW{10}, mStatsSummary[key]); } - time_point end = GetCurrentTime(); - double elapsed_seconds = Duration(start, end); - if(nVerbose) { - std::cout << "elapsed: " << std::fixed << std::setprecision(3) << elapsed_seconds << "s" << std::endl; + 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"); } /* }}} */ diff --git a/src/opt/rrr/rrrSimulator.h b/src/opt/rrr/rrrSimulator.h index b1d7296e79..6bc3bb19d0 100644 --- a/src/opt/rrr/rrrSimulator.h +++ b/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 vValues; std::vector vValues2; // simulation with an inverter @@ -46,9 +48,14 @@ namespace rrr { // backups std::vector vBackups; - // statistics - int nAdds; - int nResets; + // stats + int nCex; + int nDiscarded; + int nPackedCountOld; + std::vector vPackedCount; + std::vector 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 UpdateNetwork(Ntk *pNtk_, bool fSame); + void AssignNetwork(Ntk *pNtk_, bool fReuse); // checks bool CheckRedundancy(int id, int idx); @@ -94,6 +103,11 @@ namespace rrr { // cex void AddCex(std::vector const &vCex); + + // summary + void ResetSummary(); + summary GetStatsSummary() const; + summary GetTimesSummary() const; }; @@ -195,53 +209,71 @@ namespace rrr { template void Simulator::ActionCallback(Action const &action) { - if(target == -1) { - return; - } switch(action.type) { case REMOVE_FANIN: - if(action.id == target) { - fUpdate = true; - } else { - sUpdates.insert(action.id); + assert(fInitialized); + if(target != -1) { + if(action.id == target) { + fUpdate = true; + } else { + sUpdates.insert(action.id); + } } break; case REMOVE_UNUSED: break; case REMOVE_BUFFER: case REMOVE_CONST: - if(action.id == target) { - if(fUpdate) { - for(int fo: action.vFanouts) { - sUpdates.insert(fo); - } - fUpdate = false; - } - target = -1; - } else { - if(sUpdates.count(action.id)) { - sUpdates.erase(action.id); - for(int fo: action.vFanouts) { - sUpdates.insert(fo); + if(fInitialized) { + if(target != -1) { + if(action.id == target) { + if(fUpdate) { + for(int fo: action.vFanouts) { + sUpdates.insert(fo); + } + fUpdate = false; + } + target = -1; + } else { + if(sUpdates.count(action.id)) { + sUpdates.erase(action.id); + for(int fo: action.vFanouts) { + sUpdates.insert(fo); + } + } } } } break; case ADD_FANIN: - if(action.id == target) { - fUpdate = true; - } else { - sUpdates.insert(action.id); + assert(fInitialized); + if(target != -1) { + if(action.id == target) { + fUpdate = true; + } else { + sUpdates.insert(action.id); + } } break; case TRIVIAL_COLLAPSE: break; case TRIVIAL_DECOMPOSE: - vValues.resize(nWords * pNtk->GetNumNodes()); - SimulateNode(vValues, action.fi); + if(fInitialized) { + 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 void Simulator::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 void Simulator::Resimulate() { + time_point timeStart = GetCurrentTime(); if(nVerbose) { std::cout << "resimulating" << std::endl; } @@ -382,10 +417,12 @@ namespace rrr { } }); */ + durationSimulation += Duration(timeStart, GetCurrentTime()); } template void Simulator::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,10 +524,40 @@ namespace rrr { Print(nWords, care.begin()); std::cout << std::endl; } + durationCare += Duration(timeStart, GetCurrentTime()); } /* }}} */ + /* {{{ Preparation */ + + template + void Simulator::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; + } + + /* }}} */ + /* {{{ Save & load */ template @@ -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 @@ -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 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), - nAdds(0), - nResets(0) { + fUpdate(false) { + ResetSummary(); } template @@ -594,38 +676,27 @@ namespace rrr { pNtk(NULL), nVerbose(pPar->nSimulatorVerbose), nWords(pPar->nWords), + fGenerated(false), + fInitialized(false), target(-1), iPivot(0), - fUpdate(false), - nAdds(0), - nResets(0) { + fUpdate(false) { care.resize(nWords); tmp.resize(nWords); + ResetSummary(); } template - Simulator::~Simulator() { - if(pNtk) { - std::cout << "simulator stats: added CEXs = " << nAdds << ", resets = " << nResets << std::endl; + void Simulator::AssignNetwork(Ntk *pNtk_, bool fReuse) { + if(!fReuse) { + fGenerated = false; } - } - - template - void Simulator::UpdateNetwork(Ntk *pNtk_, bool fSame) { - pNtk = pNtk_; - pNtk->AddCallback(std::bind(&Simulator::ActionCallback, this, std::placeholders::_1)); - // TODO: what if nWords has changed? shall we reset it to default? - vValues.resize(nWords * pNtk->GetNumNodes()); + fInitialized = false; target = -1; fUpdate = false; sUpdates.clear(); - if(!fSame) { // reset stimuli if network function changed - iPivot = 0; - vAssignedStimuli.clear(); - vAssignedStimuli.resize(nWords * pNtk->GetNumPis()); - GenerateRandomStimuli(); - } - Simulate(); + pNtk = pNtk_; + pNtk->AddCallback(std::bind(&Simulator::ActionCallback, this, std::placeholders::_1)); } /* }}} */ @@ -634,6 +705,9 @@ namespace rrr { template bool Simulator::CheckRedundancy(int id, int idx) { + if(!fInitialized) { + Initialize(); + } ComputeCare(id); switch(pNtk->GetNodeType(id)) { case AND: { @@ -671,6 +745,9 @@ namespace rrr { template bool Simulator::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,10 +921,56 @@ namespace rrr { std::cout << std::endl; } } - nAdds++; + durationCare += Duration(timeStart, GetCurrentTime()); + nCex++; } /* }}} */ + + /* {{{ Summary */ + + template + void Simulator::ResetSummary() { + nCex = 0; + nDiscarded = 0; + nPackedCountOld = 0; + for(int count: vPackedCount) { + if(count) { + nPackedCountOld++; + } + } + vPackedCountEvicted.clear(); + durationSimulation = 0; + durationCare = 0; + }; + + template + summary Simulator::GetStatsSummary() const { + summary 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 + summary Simulator::GetTimesSummary() const { + summary v; + v.emplace_back("sim simulation", durationSimulation); + v.emplace_back("sim care computation", durationCare); + return v; + }; + + /* }}} */ } diff --git a/src/opt/rrr/rrrTypes.h b/src/opt/rrr/rrrTypes.h index 858b65a5f5..66f50a6d5f 100644 --- a/src/opt/rrr/rrrTypes.h +++ b/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 vFanins; std::vector vIndices; std::vector vFanouts; @@ -60,6 +62,9 @@ namespace rrr { using clock_type = std::chrono::steady_clock; using time_point = std::chrono::time_point; + template + using summary = std::vector>; + } ABC_NAMESPACE_CXX_HEADER_END diff --git a/src/opt/rrr/rrrUtils.h b/src/opt/rrr/rrrUtils.h index b05a476256..85709f4cee 100644 --- a/src/opt/rrr/rrrUtils.h +++ b/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 void PrintNext(std::ostream &os, T t, Args... args); + static inline void PrintNext(std::ostream &os, int t) { + os << std::setw(4) << t; + } + + template + 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 - 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 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 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 static inline void PrintNext(std::ostream& os, std::vector const &arg) { - std::string delim; - os << "["; + os << "[ "; for(T const &e: arg) { - os << delim; PrintNext(os, e); - delim = ", "; + os << " "; } os << "]"; } template static inline void PrintNext(std::ostream& os, std::vector 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 static inline void PrintNext(std::ostream& os, std::set const &arg) { - std::string delim; - os << "{"; + os << "{ "; for(T const &e: arg) { - os << delim; PrintNext(os, e); - delim = ", "; + os << " "; } os << "}"; } template static inline void PrintNext(std::ostream& os, std::set 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 &v, int n, int k, std::function 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;