From 1536809aaca8e46c8c0040ff87b346bfae0ec1fc Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Thu, 5 Feb 2026 14:19:47 +0100 Subject: [PATCH 1/5] build primary points fix --- src/strategies/miter/BuildPrimaryOutputClauses.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/strategies/miter/BuildPrimaryOutputClauses.cpp b/src/strategies/miter/BuildPrimaryOutputClauses.cpp index c0081e0c..93b99552 100644 --- a/src/strategies/miter/BuildPrimaryOutputClauses.cpp +++ b/src/strategies/miter/BuildPrimaryOutputClauses.cpp @@ -122,7 +122,7 @@ std::vector BuildPrimaryOutputClauses::collectInputs() { SNLBitTerm::Direction::Input) { auto deps = SNLDesignModeling::getCombinatorialInputs(term.getSnlBitTerm()); - const auto& tt = SNLDesignModeling::getTruthTable(term.getSnlBitTerm()->getDesign(), + const auto tt = SNLDesignModeling::getTruthTable(term.getSnlBitTerm()->getDesign(), term.getSnlBitTerm()->getOrderID()); if (!tt.isInitialized()) { assert(termId < naja::DNL::get()->getDNLTerms().size()); @@ -266,7 +266,7 @@ std::vector BuildPrimaryOutputClauses::collectOutputs() { SNLBitTerm::Direction::Input) { continue; } - const auto& tt = SNLDesignModeling::getTruthTable(tTerm.getSnlBitTerm()->getDesign(), + const auto tt = SNLDesignModeling::getTruthTable(tTerm.getSnlBitTerm()->getDesign(), tTerm.getSnlBitTerm()->getOrderID()); if (tt.isInitialized()) { tts.emplace_back(tt); @@ -279,8 +279,8 @@ std::vector BuildPrimaryOutputClauses::collectOutputs() { } } bool inTermInTTDeps = false; - for (const auto& tt : tts) { - const auto& ttDeps = + for (const auto tt : tts) { + const auto ttDeps = tt.getDependencies(); // expect std::vector // WRONG!!! We need the input's "orderID" not general terminal orderID //uint64_t orderID = @@ -443,7 +443,7 @@ void BuildPrimaryOutputClauses::initVarNames() { const DNLTerminalFull& tTerm = naja::DNL::get()->getDNLTerminalFromID(inputs_[i]); // If direction is input, skip if (!tTerm.isTopPort()) { - const auto& tt = SNLDesignModeling::getTruthTable(tTerm.getSnlBitTerm()->getDesign(), + const auto tt = SNLDesignModeling::getTruthTable(tTerm.getSnlBitTerm()->getDesign(), tTerm.getSnlBitTerm()->getOrderID()); if (tt.isInitialized()) { if (tt.all0()) { @@ -734,7 +734,7 @@ void BuildPrimaryOutputClauses::setOutputs2OutputsIDs() { // if (iter != ttCache_.end()) { // return iter->second; // } -// const auto& tt = SNLDesignModeling::getTruthTable(design, orderID); +// const auto tt = SNLDesignModeling::getTruthTable(design, orderID); // ttCache_[{designID, orderID}] = tt; // return tt; // } \ No newline at end of file From 4a3a500fedae340a9cb2f7e4d774edf883359d2b Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Thu, 5 Feb 2026 22:09:28 +0100 Subject: [PATCH 2/5] cleaning --- src/clauses/SNLLogicCloud.cpp | 166 +++++++++--------- src/clauses/SNLTruthTableTree.cpp | 150 +++------------- src/clauses/Tree2BoolExpr.cpp | 164 ++++++++--------- .../miter/BuildPrimaryOutputClauses.cpp | 88 ---------- 4 files changed, 193 insertions(+), 375 deletions(-) diff --git a/src/clauses/SNLLogicCloud.cpp b/src/clauses/SNLLogicCloud.cpp index f699628a..c1000eb1 100644 --- a/src/clauses/SNLLogicCloud.cpp +++ b/src/clauses/SNLLogicCloud.cpp @@ -24,67 +24,67 @@ using namespace naja::DNL; typedef std::pair< std::vector>, size_t> - IterationInputsETSPair; + IterationInputsPair; -thread_local IterationInputsETSPair currentIterationInputsETS; +thread_local IterationInputsPair currentIterationInputs; -IterationInputsETSPair& getCurrentIterationInputsETS() { - return currentIterationInputsETS; +IterationInputsPair& getCurrentIterationInputs() { + return currentIterationInputs; } -thread_local IterationInputsETSPair newIterationInputsETS; +thread_local IterationInputsPair newIterationInputs; -IterationInputsETSPair& getNewIterationInputsETS() { - return newIterationInputsETS; +IterationInputsPair& getNewIterationInputs() { + return newIterationInputs; } -void clearCurrentIterationInputsETS() { - auto& currentIterationInputs = getCurrentIterationInputsETS(); +void clearCurrentIterationInputs() { + auto& currentIterationInputs = getCurrentIterationInputs(); currentIterationInputs.first.clear(); } -void pushBackCurrentIterationInputsETS(naja::DNL::DNLID input) { - auto& currentIterationInputs = getCurrentIterationInputsETS(); +void pushBackCurrentIterationInputs(naja::DNL::DNLID input) { + auto& currentIterationInputs = getCurrentIterationInputs(); currentIterationInputs.first.emplace_back(input); } -size_t sizeOfCurrentIterationInputsETS() { - return getCurrentIterationInputsETS().first.size(); +size_t sizeOfCurrentIterationInputs() { + return getCurrentIterationInputs().first.size(); } -void copyCurrentIterationInputsETS(std::vector>& res) { +void copyCurrentIterationInputs(std::vector>& res) { res.clear(); - auto& current = getCurrentIterationInputsETS(); + auto& current = getCurrentIterationInputs(); res = std::move(current.first); } -void clearNewIterationInputsETS() { - auto& newIterationInputs = getNewIterationInputsETS(); +void clearNewIterationInputs() { + auto& newIterationInputs = getNewIterationInputs(); newIterationInputs.first.clear(); } -void pushBackNewIterationInputsETS(naja::DNL::DNLID input) { - getNewIterationInputsETS().first.emplace_back(input); +void pushBackNewIterationInputs(naja::DNL::DNLID input) { + getNewIterationInputs().first.emplace_back(input); } -bool emptyNewIterationInputsETS() { - return getNewIterationInputsETS().first.empty(); +bool emptyNewIterationInputs() { + return getNewIterationInputs().first.empty(); } -size_t sizeOfNewIterationInputsETS() { - return getNewIterationInputsETS().first.size(); +size_t sizeOfNewIterationInputs() { + return getNewIterationInputs().first.size(); } -void copyNewIterationInputsETStoCurrent() { - auto& newIterationInputs = getNewIterationInputsETS(); - auto& currentIterationInputs = getCurrentIterationInputsETS(); +void copyNewIterationInputstoCurrent() { + auto& newIterationInputs = getNewIterationInputs(); + auto& currentIterationInputs = getCurrentIterationInputs(); #ifdef DEBUG_CHECKS size_t newSize = newIterationInputs.first.size(); #endif currentIterationInputs = std::move(newIterationInputs); #ifdef DEBUG_CHECKS assert(currentIterationInputs.first.size() == newSize && - "copyNewIterationInputsETStoCurrent: size mismatch after copy"); + "copyNewIterationInputstoCurrent: size mismatch after copy"); #endif } @@ -93,27 +93,27 @@ thread_local std::pair< tbb::tbb_allocator>>, size_t> - inputsToMergeETS; + inputsToMerge; std::pair, tbb::tbb_allocator>>, size_t>& -getInputsToMergeETS() { - return inputsToMergeETS; +getInputsToMerge() { + return inputsToMerge; } -void clearInputsToMergeETS() { - auto& inputsToMerge = getInputsToMergeETS(); +void clearInputsToMerge() { + auto& inputsToMerge = getInputsToMerge(); inputsToMerge.first.clear(); } -void pushBackInputsToMergeETS( +void pushBackInputsToMerge( const std::pair& input) { - getInputsToMergeETS().first.emplace_back(input); + getInputsToMerge().first.emplace_back(input); } -size_t sizeOfInputsToMergeETS() { - return getInputsToMergeETS().first.size(); +size_t sizeOfInputsToMerge() { + return getInputsToMerge().first.size(); } // 2 level vector visited terms pair - 1st: termID, 2nd: termID @@ -128,7 +128,7 @@ typedef std::vector< tbb::tbb_allocator>>> VisitedTermsPairsVec; -thread_local VisitedTermsPairsVec visitedTermsPairsETS; +thread_local VisitedTermsPairsVec visitedTermsPairs; struct PairHash { size_t operator()(const std::pair& p) const noexcept { @@ -148,19 +148,19 @@ struct PairHash { PairHash, PairEq, tbb::tbb_allocator>>; -thread_local HandledSet visitedTermsPairsETSSet; +thread_local HandledSet visitedTermsPairsSet; -void clearVisitedTermsPairsETS() { - visitedTermsPairsETSSet.clear(); +void clearVisitedTermsPairs() { + visitedTermsPairsSet.clear(); } -thread_local std::pair tempPairETS; +thread_local std::pair tempPair; -bool isPairVisitedETS(naja::DNL::DNLID termA, +bool isPairVisited(naja::DNL::DNLID termA, naja::DNL::DNLID termB) { - tempPairETS.first = termA; - tempPairETS.second = termB; - if (!(visitedTermsPairsETSSet.insert(tempPairETS)).second) { + tempPair.first = termA; + tempPair.second = termB; + if (!(visitedTermsPairsSet.insert(tempPair)).second) { return true; } return false; @@ -175,8 +175,8 @@ bool SNLLogicCloud::isOutput(naja::DNL::DNLID termID) { } void SNLLogicCloud::compute() { - clearNewIterationInputsETS(); - clearCurrentIterationInputsETS(); + clearNewIterationInputs(); + clearCurrentIterationInputs(); DEBUG_LOG("---- Begin!!\n"); if (dnl_.getDNLTerminalFromID(seedOutputTerm_).isTopPort() || isOutput(seedOutputTerm_)) { @@ -206,7 +206,7 @@ void SNLLogicCloud::compute() { const auto& driver = iso.getDrivers().front(); auto& inst = dnl_.getDNLTerminalFromID(driver).getDNLInstance(); if (isInput(driver)) { - pushBackCurrentIterationInputsETS(driver); + pushBackCurrentIterationInputs(driver); table_ = SNLTruthTableTree(inst.getID(), driver, SNLTruthTableTree::Node::Type::P); return; @@ -218,7 +218,7 @@ void SNLLogicCloud::compute() { const DNLTerminalFull& term = dnl_.getDNLTerminalFromID(termID); if (term.getSnlBitTerm()->getDirection() != SNLBitTerm::Direction::Output) { - pushBackNewIterationInputsETS(termID); + pushBackNewIterationInputs(termID); DEBUG_LOG("Add input with id: %zu\n", termID); } } @@ -240,7 +240,7 @@ void SNLLogicCloud::compute() { if (term.getSnlBitTerm()->getDirection() != SNLBitTerm::Direction::Output) { // newIterationInputs.emplace_back(termID); - pushBackNewIterationInputsETS(termID); + pushBackNewIterationInputs(termID); DEBUG_LOG("Add input with id: %zu\n", termID); } } @@ -251,17 +251,17 @@ void SNLLogicCloud::compute() { "Truth table for seed output term is not initialized"); } - if (emptyNewIterationInputsETS()) { + if (emptyNewIterationInputs()) { DEBUG_LOG("No inputs found for seed output term %zu\n", seedOutputTerm_); return; } bool reachedPIs = true; - size_t size = sizeOfNewIterationInputsETS(); + size_t size = sizeOfNewIterationInputs(); for (size_t i = 0; i < size; i++) { if (!isInput( - getNewIterationInputsETS().first - [i]) /* && !isOutput(getNewIterationInputsETS().first[i])*/) { + getNewIterationInputs().first + [i]) /* && !isOutput(getNewIterationInputs().first[i])*/) { reachedPIs = false; break; } @@ -269,31 +269,31 @@ void SNLLogicCloud::compute() { // HandledSet handledTerms; // handledTerms.reserve(naja::DNL::get()->getDNLTerms().size() / 4); - clearVisitedTermsPairsETS(); + clearVisitedTermsPairs(); size_t iter = 0; while (!reachedPIs) { DEBUG_LOG("---iter %lu---\n", iter); DEBUG_LOG("Current iteration inputs size: %zu\n", - sizeOfNewIterationInputsETS()); - copyNewIterationInputsETStoCurrent(); + sizeOfNewIterationInputs()); + copyNewIterationInputstoCurrent(); - clearNewIterationInputsETS(); + clearNewIterationInputs(); DEBUG_LOG("table size: %zu, currentIterationInputs_ size: %zu\n", - table_.size(), sizeOfCurrentIterationInputsETS()); - clearInputsToMergeETS(); - size_t sizeOfCurrentInputs = sizeOfCurrentIterationInputsETS(); + table_.size(), sizeOfCurrentIterationInputs()); + clearInputsToMerge(); + size_t sizeOfCurrentInputs = sizeOfCurrentIterationInputs(); for (size_t i = 0; i < sizeOfCurrentInputs; i++) { - const auto& input = getCurrentIterationInputsETS().first[i]; + const auto& input = getCurrentIterationInputs().first[i]; if (isInput(input) /*|| isOutput(input)*/) { - pushBackNewIterationInputsETS(input); + pushBackNewIterationInputs(input); DEBUG_LOG("Adding input id: %zu %s\n", input, dnl_.getDNLTerminalFromID(input) .getSnlBitTerm() ->getName() .getString() .c_str()); - pushBackInputsToMergeETS( + pushBackInputsToMerge( {naja::DNL::DNLID_MAX, input}); // Placeholder for PI/PO continue; } @@ -353,7 +353,7 @@ void SNLLogicCloud::compute() { if (isInput(driver) /* || isOutput(driver)*/ || (Tree2BoolExpr::iso2boolExpr_.find(iso.getIsoID()) != Tree2BoolExpr::iso2boolExpr_.end() && iter > 0)) { - pushBackNewIterationInputsETS(driver); + pushBackNewIterationInputs(driver); DEBUG_LOG( "- %lu After analyzing input %s(%lu), addings driver %s(%lu) is a " "primary input\n", @@ -370,7 +370,7 @@ void SNLLogicCloud::compute() { .getString() .c_str(), driver); - pushBackInputsToMergeETS( + pushBackInputsToMerge( {naja::DNL::DNLID_MAX, driver}); // Placeholder for PI/PO continue; } @@ -390,14 +390,14 @@ void SNLLogicCloud::compute() { ->getName() .getString() .c_str()); - pushBackInputsToMergeETS({inst.getID(), driver}); + pushBackInputsToMerge({inst.getID(), driver}); for (DNLID termID = inst.getTermIndexes().first; termID <= inst.getTermIndexes().second; termID++) { const DNLTerminalFull& term = dnl_.getDNLTerminalFromID(termID); if (term.getSnlBitTerm()->getDirection() != SNLBitTerm::Direction::Output) { - if (isPairVisitedETS(driver, termID)) { + if (isPairVisited(driver, termID)) { DEBUG_LOG( "#### iter %lu 1 Term (%zu) %s of inst %s already handled, " "skipping\n", @@ -411,38 +411,38 @@ void SNLLogicCloud::compute() { naja::DNL::get() ->getDNLTerminalFromID(input) .getDNLInstance() - .getSNLModel() + ->getSNLModel() ->getName() .getString() .c_str()); continue; } - pushBackNewIterationInputsETS(termID); + pushBackNewIterationInputs(termID); } } } - if (sizeOfInputsToMergeETS() == 0) { + if (sizeOfInputsToMerge() == 0) { break; } DEBUG_LOG("--- Merging truth tables with %zu inputs\n", - sizeOfInputsToMergeETS()); - table_.concatFull(getInputsToMergeETS().first, - sizeOfInputsToMergeETS()); + sizeOfInputsToMerge()); + table_.concatFull(getInputsToMerge().first, + sizeOfInputsToMerge()); reachedPIs = true; - size_t sizeOfNewInputs = sizeOfNewIterationInputsETS(); + size_t sizeOfNewInputs = sizeOfNewIterationInputs(); for (size_t i = 0; i < sizeOfNewInputs; i++) { auto iso = dnl_.getDNLIsoDB().getIsoFromIsoIDconst( dnl_.getDNLTerminalFromID( - getNewIterationInputsETS().first[i]) + getNewIterationInputs().first[i]) .getIsoID()); - if (!isInput(getNewIterationInputsETS().first[i]) && + if (!isInput(getNewIterationInputs().first[i]) && (Tree2BoolExpr::iso2boolExpr_.find( dnl_.getDNLTerminalFromID( - getNewIterationInputsETS().first[i]) + getNewIterationInputs().first[i]) .getIsoID()) == Tree2BoolExpr::iso2boolExpr_.end() || - iso.getDrivers().front() != getNewIterationInputsETS().first[i])) { + iso.getDrivers().front() != getNewIterationInputs().first[i])) { reachedPIs = false; break; } @@ -451,15 +451,15 @@ void SNLLogicCloud::compute() { iter++; } - copyNewIterationInputsETStoCurrent(); + copyNewIterationInputstoCurrent(); #ifdef DEBUG_CHECKS - size_t finalSize = sizeOfCurrentIterationInputsETS(); + size_t finalSize = sizeOfCurrentIterationInputs(); #endif - copyCurrentIterationInputsETS(currentIterationInputs_); + copyCurrentIterationInputs(currentIterationInputs_); #ifdef DEBUG_CHECKS assert(finalSize == currentIterationInputs_.size() && "compute: size mismatch after final copy"); - //assert(currentIterationInputs_.size() == sizeOfCurrentIterationInputsETS()); + //assert(currentIterationInputs_.size() == sizeOfCurrentIterationInputs()); for (const auto& input : currentIterationInputs_) { auto iso = dnl_.getDNLIsoDB().getIsoFromIsoIDconst( dnl_.getDNLTerminalFromID(input).getIsoID()); diff --git a/src/clauses/SNLTruthTableTree.cpp b/src/clauses/SNLTruthTableTree.cpp index d4858a54..715e1e0b 100644 --- a/src/clauses/SNLTruthTableTree.cpp +++ b/src/clauses/SNLTruthTableTree.cpp @@ -29,55 +29,22 @@ using namespace KEPLER_FORMAL; typedef std::pair>, size_t> BorderLeavesPair; -// ets for std::vector> newBorderLeaves; -// tbb::enumerable_thread_specific newBorderLeavesETS; - -// tbb::concurrent_vector -// newBorderLeavesETSVector = -// tbb::concurrent_vector(40, nullptr); - -// void initNewBorderLeavesETS() { -// size_t idx = tbb::this_task_arena::current_thread_index() >= 0 ? tbb::this_task_arena::current_thread_index() : 0; -// if (newBorderLeavesETSVector.size() <= idx) { -// for (size_t i = newBorderLeavesETSVector.size(); i <= idx; i++) { -// newBorderLeavesETSVector.emplace_back(nullptr); -// } -// } -// if (newBorderLeavesETSVector -// [idx] == nullptr) { -// newBorderLeavesETSVector[idx] = -// &newBorderLeavesETS.local(); -// } -// } - -thread_local BorderLeavesPair newBorderLeavesETS; - -BorderLeavesPair& getNewBorderLeavesETS() { - //size_t idx = tbb::this_task_arena::current_thread_index() >= 0 ? tbb::this_task_arena::current_thread_index() : 0; - //return *newBorderLeavesETSVector[idx]; - return newBorderLeavesETS; +thread_local BorderLeavesPair newBorderLeavesTLS; + +BorderLeavesPair& getNewBorderLeaves() { + return newBorderLeavesTLS; } -size_t getSizeOfNewBorderLeavesETS() { - return getNewBorderLeavesETS().first.size(); +size_t getSizeOfNewBorderLeaves() { + return getNewBorderLeaves().first.size(); } -void pushBackNewBorderLeavesETS(const KEPLER_FORMAL::SNLTruthTableTree::BorderLeaf& leaf) { - // auto& pair = getNewBorderLeavesETS(); - // auto& vec = pair.first; - // auto& sz = pair.second; - // if (vec.size() > sz) { - // vec[sz] = leaf; - // sz++; - // return; - // } - // vec.emplace_back(leaf); - // sz++; - getNewBorderLeavesETS().first.emplace_back(leaf); +void pushBackNewBorderLeaves(const KEPLER_FORMAL::SNLTruthTableTree::BorderLeaf& leaf) { + getNewBorderLeaves().first.emplace_back(leaf); } -void clearNewBorderLeavesETS() { - auto& pair = getNewBorderLeavesETS(); +void clearNewBorderLeaves() { + auto& pair = getNewBorderLeaves(); pair.first.clear(); } @@ -91,39 +58,14 @@ using NodeRaw = SNLTruthTableTree::Node*; using NodeVecRaw = std::vector>; using NodeVecVecRaw = std::vector>; using ResolvedChildrenPairRaw = std::pair; -// tbb::enumerable_thread_specific resolvedChildrenETS; - -// tbb::concurrent_vector -// resolvedChildrenETSVector = -// tbb::concurrent_vector(40, nullptr); - -// void initResolvedChildrenETS() { -// size_t idx = tbb::this_task_arena::current_thread_index() >= 0 ? tbb::this_task_arena::current_thread_index() : 0; -// if (resolvedChildrenETSVector.size() <= -// idx) { -// for (size_t i = resolvedChildrenETSVector.size(); -// i <= idx; i++) { -// resolvedChildrenETSVector.emplace_back(nullptr); -// } -// } -// if (resolvedChildrenETSVector -// [idx] == nullptr) { -// resolvedChildrenETSVector[idx] = -// &resolvedChildrenETS.local(); -// } -// } - -thread_local ResolvedChildrenPairRaw resolvedChildrenETS; - -ResolvedChildrenPairRaw& getResolvedChildrenETS() { - //size_t idx = tbb::this_task_arena::current_thread_index() >= 0 ? tbb::this_task_arena::current_thread_index() : 0; - //return *resolvedChildrenETSVector - // [idx]; - return resolvedChildrenETS; +thread_local ResolvedChildrenPairRaw resolvedChildrenTLS; + +ResolvedChildrenPairRaw& getResolvedChildren() { + return resolvedChildrenTLS; } -void reserveResolvedChildrenETS(size_t n) { - auto& pair = getResolvedChildrenETS(); +void reserveResolvedChildren(size_t n) { + auto& pair = getResolvedChildren(); for (size_t i = 0; i < pair.first.size(); ++i) { pair.first[i].clear(); } @@ -412,15 +354,11 @@ void SNLTruthTableTree::updateBorderLeaves() { //---------------------------------------------------------------------- SNLTruthTableTree::SNLTruthTableTree() : rootId_(kInvalidId), numExternalInputs_(0) { - //initNewBorderLeavesETS(); - //initResolvedChildrenETS(); } SNLTruthTableTree::SNLTruthTableTree(naja::DNL::DNLID instid, naja::DNL::DNLID termid, Node::Type type) { - //initNewBorderLeavesETS(); - //initResolvedChildrenETS(); auto rootNode = std::make_shared(this, instid, termid, type); uint32_t id = allocateNode(rootNode); rootId_ = id; @@ -758,47 +696,27 @@ void SNLTruthTableTree::concatFull( #endif // FUNC START - //std::vector> newBorderLeaves; - auto& newBorderLeaves = getNewBorderLeavesETS(); - clearNewBorderLeavesETS(); + auto& newBorderLeaves = getNewBorderLeaves(); + clearNewBorderLeaves(); size_t newInputs = 0; size_t index = 0; assert(size == borderLeaves_.size()); numExternalInputs_ = 0; for (size_t i = 0; i < size; ++i) { - // For each entry in table to merge - //assert(newBorderLeaves.size() == newInputs); - assert(getSizeOfNewBorderLeavesETS() == newInputs); - // Get the relevant border leaf based on order -> assuming identical order - // between tables and border leaves + assert(getSizeOfNewBorderLeaves() == newInputs); const auto& borderLeaf = borderLeaves_[i]; - // Get parent node of current border leaf auto parentPtr = nodeFromId(borderLeaf.parentId).get(); - // if (!parentPtr) { - // // No parent so it is the root - // index++; - // newBorderLeaves.emplace_back(borderLeaf); - // DEBUG_LOG("--- concatBody: null parent for border leaf index %zu\n", - // index-1); newInputs += 1; assert(newBorderLeaves.size() == newInputs); - // assert(rootId_ == borderLeaf.parentId && "concatFull: null parent is - // not root"); continue; - // } if (parentPtr->type == Node::Type::P) { - // If it is a PI border leaf, keep the same leaf and continue, no need to - // chain PIs index++; - //newBorderLeaves.emplace_back(borderLeaf); - pushBackNewBorderLeavesETS(borderLeaf); + pushBackNewBorderLeaves(borderLeaf); DEBUG_LOG("--- concatBody: skipping PI border leaf index %zu\n", index - 1); newInputs += 1; - //assert(newBorderLeaves.size() == newInputs); - assert(getSizeOfNewBorderLeavesETS() == newInputs); + assert(getSizeOfNewBorderLeaves() == newInputs); continue; } const auto& n = concatBody(index, tables[i].first, tables[i].second); if (n.parentIds.size() <= 1 || n.type == Node::Type::P) { - // if new node is not reused, expand border leaves DEBUG_LOG("ConcatBody expanding border leaf index %zu termid %zu %s %s\n", index, tables[i].second, naja::DNL::get() @@ -814,16 +732,10 @@ void SNLTruthTableTree::concatFull( ->getName() .getString() .c_str()); - // Now we will create new border leaves for each input of the newly - // inserted node It is in the place of the original border leaf uint32_t insertedId = parentPtr->childrenIds[borderLeaf.childPos]; - // assert that insertedId is an input node - // assert(nodeFromId(insertedId)->type != Node::Type::Input && - // "concatFull: inserted node is input after concatBody"); auto insertedSp = nodeFromId(insertedId).get(); assert(insertedSp->type != Node::Type::Input && "concatFull: inserted node is input after concatBody"); - // assert the input node have only one parent assert(insertedSp->parentIds.size() == 1 && "concatFull: inserted node has multiple parents after concatBody"); if (!insertedSp) { @@ -838,23 +750,18 @@ void SNLTruthTableTree::concatFull( .getString() .c_str()); DEBUG_LOG("children count: %zu\n", insertedSp->childrenIds.size()); - // now next is to add border leaf on top of each input node of insertedSp for (size_t j = 0; j < insertedSp->childrenIds.size(); ++j) { uint32_t cid = insertedSp->childrenIds[j]; - auto ch = nodeFromId(cid).get(); assert(ch); - // assert that cid is an input node assert(ch->type == Node::Type::Input && "concatFull: inserted node child is not input after concatBody"); - if (ch->type == Node::Type::Input) { - // Now concat a border leaf for this input BorderLeaf bl; bl.parentId = (insertedId); bl.childPos = j; - bl.extIndex = ch->data.inputIndex; // Set correctly in concatBody - pushBackNewBorderLeavesETS(bl); + bl.extIndex = ch->data.inputIndex; + pushBackNewBorderLeaves(bl); DEBUG_LOG( "--- new border leaf extIndex %zu from inserted node id %u " "childPos %zu\n", @@ -874,8 +781,7 @@ void SNLTruthTableTree::concatFull( .getString() .c_str()); newInputs += 1; - //assert(newBorderLeaves.size() == newInputs); - assert(getSizeOfNewBorderLeavesETS() == newInputs); + assert(getSizeOfNewBorderLeaves() == newInputs); } else { assert(false); } @@ -1185,12 +1091,12 @@ void SNLTruthTableTree::finalize() { if (sp->nodeID != 0) mapByNodeID[sp->nodeID] = sp; } - reserveResolvedChildrenETS(nodeSize); + reserveResolvedChildren(nodeSize); for (size_t i = 0; i < nodeSize; ++i) { Node* sp = nodes_[i].get(); if (!sp) continue; - getResolvedChildrenETS().first[i].reserve(sp->childrenIds.size()); + getResolvedChildren().first[i].reserve(sp->childrenIds.size()); for (size_t j = 0; j < sp->childrenIds.size(); ++j) { uint32_t cid = sp->childrenIds[j]; Node* target = nullptr; @@ -1225,7 +1131,7 @@ void SNLTruthTableTree::finalize() { // LCOV_EXCL_STOP } //resolvedChildren[i].emplace_back(target); - getResolvedChildrenETS().first[i].emplace_back(target); + getResolvedChildren().first[i].emplace_back(target); } } @@ -1250,7 +1156,7 @@ void SNLTruthTableTree::finalize() { for (size_t i = 0; i < nodeSize; ++i) { Node* sp = nodes_[i].get(); sp->childrenIds.clear(); - const auto& resolvedChilde = getResolvedChildrenETS().first[i]; + const auto& resolvedChilde = getResolvedChildren().first[i]; sp->childrenIds.reserve(resolvedChilde.size()); for (size_t j = 0; j < resolvedChilde.size(); ++j) { auto targ = resolvedChilde[j]; diff --git a/src/clauses/Tree2BoolExpr.cpp b/src/clauses/Tree2BoolExpr.cpp index 77582d81..0fe91511 100644 --- a/src/clauses/Tree2BoolExpr.cpp +++ b/src/clauses/Tree2BoolExpr.cpp @@ -45,63 +45,63 @@ tbb::concurrent_unordered_map Tree2BoolExpr::iso2bo typedef std::vector> TermsPair; // Thread-local storage for DNF terms while building expressions for a node. -thread_local TermsPair termsETS; +thread_local TermsPair terms; -TermsPair& getTErmsETS() { - return termsETS; +TermsPair& getTErms() { + return terms; } -size_t sizeOfTermsETS() { - return getTErmsETS().size(); +size_t sizeOfTerms() { + return getTErms().size(); } -void clearTermsETS() { - auto& termsLocal = getTErmsETS(); +void clearTerms() { + auto& termsLocal = getTErms(); termsLocal.clear(); } -void pushBackTermsETS(BoolExpr* term) { - getTErmsETS().emplace_back(term); +void pushBackTerms(BoolExpr* term) { + getTErms().emplace_back(term); } -bool emptyTermsETS() { - return getTErmsETS().empty(); +bool emptyTerms() { + return getTErms().empty(); } // Relevant inputs bitset per node: which child inputs actually affect the table. // Stored as a vector (bool-like) with a logical size. typedef std::pair>, size_t> RelevantPair; -thread_local RelevantPair relevantETS; +thread_local RelevantPair relevant; -RelevantPair& getRelevantETS() { - return relevantETS; +RelevantPair& getRelevant() { + return relevant; } -size_t sizeOfRelevantETS() { - return getRelevantETS().second; +size_t sizeOfRelevant() { + return getRelevant().second; } -void clearRelevantETS() { - auto& relevantLocal = getRelevantETS(); +void clearRelevant() { + auto& relevantLocal = getRelevant(); relevantLocal.first.clear(); } -void setRelevantETS(size_t i, bool b) { - auto& relevantLocal = getRelevantETS(); +void setRelevant(size_t i, bool b) { + auto& relevantLocal = getRelevant(); if (i >= relevantLocal.second) { // LCOV_EXCL_START - assert(false && "setRelevantETS: index out of range"); + assert(false && "setRelevant: index out of range"); // LCOV_EXCL_STOP } relevantLocal.first[i] = b; } -bool getRelevantETS(size_t i) { - auto& relevantLocal = getRelevantETS(); +bool getRelevant(size_t i) { + auto& relevantLocal = getRelevant(); if (i >= relevantLocal.second) { // LCOV_EXCL_START - throw std::out_of_range("getRelevantETS: index out of range"); + throw std::out_of_range("getRelevant: index out of range"); // LCOV_EXCL_STOP } return relevantLocal.first[i]; @@ -109,8 +109,8 @@ bool getRelevantETS(size_t i) { // Ensure the relevant vector has at least n entries and initialize them to false. // The logical size is stored in the second element of the pair. -void reserveRelevantETSwithFalse(size_t n) { - auto& relevantLocal = getRelevantETS(); +void reserveRelevantwithFalse(size_t n) { + auto& relevantLocal = getRelevant(); auto& vec = relevantLocal.first; auto& sz = relevantLocal.second; if (vec.size() >= n) { @@ -128,21 +128,21 @@ void reserveRelevantETSwithFalse(size_t n) { // The vector is preallocated and indexed by node ID for O(1) lookup. typedef std::pair>, size_t> MemoPair; -thread_local MemoPair memoETS; +thread_local MemoPair memo; -MemoPair& getMemoETS() { - return memoETS; +MemoPair& getMemo() { + return memo; } -void clearMemoETS() { - auto& memoLocal = getMemoETS(); +void clearMemo() { + auto& memoLocal = getMemo(); memoLocal.first.clear(); } // Reserve and initialize the memo table to a given logical size. // The vector elements are set to nullptr to indicate "not computed". -void reserveMemoETS(size_t n) { - auto& memoLocal = getMemoETS(); +void reserveMemo(size_t n) { + auto& memoLocal = getMemo(); auto& vec = memoLocal.first; auto& sz = memoLocal.second; if (vec.size() >= n) { @@ -155,35 +155,35 @@ void reserveMemoETS(size_t n) { vec.assign(n, nullptr); } -void setMemoETS(size_t i, BoolExpr* expr) { - auto& memoLocal = getMemoETS(); - assert(i < memoLocal.second && "setMemoETS: index out of range"); +void setMemo(size_t i, BoolExpr* expr) { + auto& memoLocal = getMemo(); + assert(i < memoLocal.second && "setMemo: index out of range"); memoLocal.first[i] = expr; } -BoolExpr* getMemoETS(size_t i) { - auto& memoLocal = getMemoETS(); - assert(i < memoLocal.second && "getMemoETS: index out of range"); +BoolExpr* getMemo(size_t i) { + auto& memoLocal = getMemo(); + assert(i < memoLocal.second && "getMemo: index out of range"); return memoLocal.first[i]; } // Temporary storage for child BoolExpr pointers while processing a table node. -typedef std::pair>, size_t> ChildFETSPair; +typedef std::pair>, size_t> ChildFPair; -thread_local ChildFETSPair childFETS; +thread_local ChildFPair childF; -ChildFETSPair& getChildFETS() { - return childFETS; +ChildFPair& getChildF() { + return childF; } -void clearChildFETS() { - auto& childLocal = getChildFETS(); +void clearChildF() { + auto& childLocal = getChildF(); childLocal.second = 0; } // Reserve child storage and initialize entries to nullptr. -void reserveChildFETS(size_t n) { - auto& childLocal = getChildFETS(); +void reserveChildF(size_t n) { + auto& childLocal = getChildF(); auto& vec = childLocal.first; auto& sz = childLocal.second; if (vec.size() >= n) { @@ -196,15 +196,15 @@ void reserveChildFETS(size_t n) { vec.assign(n, nullptr); } -BoolExpr* getChildFETS(size_t i) { - auto& childLocal = getChildFETS(); - assert(i < childLocal.second && "getChildFETS: index out of range"); +BoolExpr* getChildF(size_t i) { + auto& childLocal = getChildF(); + assert(i < childLocal.second && "getChildF: index out of range"); return childLocal.first[i]; } -void setChildFETS(size_t i, BoolExpr* expr) { - auto& childLocal = getChildFETS(); - assert(i < childLocal.second && "setChildFETS: index out of range"); +void setChildF(size_t i, BoolExpr* expr) { + auto& childLocal = getChildF(); + assert(i < childLocal.second && "setChildF: index out of range"); childLocal.first[i] = expr; } @@ -212,10 +212,10 @@ void setChildFETS(size_t i, BoolExpr* expr) { // Each frame holds a pointer to a node and a boolean indicating whether // the node has been visited (post-visit) or not (pre-visit). using Frame = std::pair; -thread_local std::vector> stackETS; +thread_local std::vector> stack; -std::vector>& getStackETS() { - return stackETS; +std::vector>& getStack() { + return stack; } // Main conversion routine: converts an SNLTruthTableTree into a BoolExpr. @@ -231,11 +231,11 @@ BoolExpr* Tree2BoolExpr::convert( size_t maxID = tree.getMaxID(); // 2) memo table: clear and reserve memoization storage for all node IDs. - clearMemoETS(); - reserveMemoETS(maxID + 1); + clearMemo(); + reserveMemo(maxID + 1); // 3) post-order build using an explicit stack to avoid recursion. - auto & stack = getStackETS(); + auto & stack = getStack(); stack.clear(); stack.emplace_back(root.get(), false); @@ -260,11 +260,11 @@ BoolExpr* Tree2BoolExpr::convert( if (node->type != SNLTruthTableTree::Node::Type::Input) { isoID = naja::DNL::get()->getDNLTerminalFromID(node->data.termid).getIsoID(); if (iso2boolExpr_.find(isoID) != iso2boolExpr_.end() && isoID != naja::DNL::DNLID_MAX) { - setMemoETS(id, iso2boolExpr_[isoID]); + setMemo(id, iso2boolExpr_[isoID]); } } // If memo already contains an expression for this node, skip processing. - if (getMemoETS(id) != nullptr) continue; + if (getMemo(id) != nullptr) continue; // If node is a Table or P node, push it back as visited and push children. if (node->type == SNLTruthTableTree::Node::Type::Table || node->type == SNLTruthTableTree::Node::Type::P) { @@ -301,14 +301,14 @@ BoolExpr* Tree2BoolExpr::convert( } // Special handling for constant mappings: 0 -> false, 1 -> true. if (name == 0) { - setMemoETS(id, BoolExpr::createFalse()); + setMemo(id, BoolExpr::createFalse()); iso2boolExpr_[isoID] = BoolExpr::createFalse(); } else if (name == 1) { - setMemoETS(id, BoolExpr::createTrue()); + setMemo(id, BoolExpr::createTrue()); iso2boolExpr_[isoID] = BoolExpr::createTrue(); } else { // Normal variable mapping. - setMemoETS(id, BoolExpr::Var(name)); + setMemo(id, BoolExpr::Var(name)); iso2boolExpr_[isoID] = BoolExpr::Var(name); } } @@ -326,35 +326,35 @@ BoolExpr* Tree2BoolExpr::convert( { // Gather child BoolExpr pointers into a temporary array for quick access. - clearChildFETS(); - reserveChildFETS(k); + clearChildF(); + reserveChildF(k); for (uint32_t i = 0; i < k; ++i) { size_t cid = node->tree->nodeFromId(node->childrenIds[i])->nodeID; - setChildFETS(i, getMemoETS(cid)); + setChildF(i, getMemo(cid)); } // Determine which inputs actually matter for this truth table. // For each input j, check if flipping bit j changes the table output. - clearRelevantETS(); - reserveRelevantETSwithFalse(k); + clearRelevant(); + reserveRelevantwithFalse(k); for (uint32_t j = 0; j < k; ++j) { for (uint64_t m = 0; m < rows; ++m) { bool b0 = tbl.bits().bit(m); bool b1 = tbl.bits().bit(m ^ (uint64_t{1} << j)); - if (b0 != b1) { setRelevantETS(j, true); break; } + if (b0 != b1) { setRelevant(j, true); break; } } } // Count how many inputs are relevant. size_t numRelIdx = 0; - for (uint32_t j = 0; j < k; ++j) { if (getRelevantETS(j)) numRelIdx++; } + for (uint32_t j = 0; j < k; ++j) { if (getRelevant(j)) numRelIdx++; } // The algorithm expects at least one relevant input for a PI node. assert(numRelIdx > 0 && "No relevant inputs for node"); { // Build DNF terms by iterating over rows where the table output is 1. // For each such row, create a conjunction of literals for relevant inputs. - clearTermsETS(); + clearTerms(); for (uint64_t m = 0; m < rows; ++m) { if (!tbl.bits().bit(m)) continue; BoolExpr* term = nullptr; @@ -363,31 +363,31 @@ BoolExpr* Tree2BoolExpr::convert( // For each relevant input, pick the literal (child or its negation) // according to the bit value in row m. for (uint32_t j = 0; j < k; ++j) { - if (!getRelevantETS(j)) { + if (!getRelevant(j)) { continue; } bool bit1 = ((m >> j) & 1) != 0; - lit = bit1 ? getChildFETS(j) : BoolExpr::Not(getChildFETS(j)); + lit = bit1 ? getChildF(j) : BoolExpr::Not(getChildF(j)); if (firstLit) { term = lit; firstLit = false; } else { assert(term != nullptr); assert(lit != nullptr); term = BoolExpr::And(term, lit); } } // Only push the term if at least one literal was included. - if (term) { pushBackTermsETS(std::move(term)); } + if (term) { pushBackTerms(std::move(term)); } } // There must be at least one term for a PI node. - assert(!emptyTermsETS()); // Should be a PI + assert(!emptyTerms()); // Should be a PI { // Fold the list of terms into a single expression by OR-ing them. - BoolExpr* expr = getTErmsETS()[0]; - DEBUG_LOG("number of rows for node ID %zu: %zu\n", id, sizeOfTermsETS()); - for (size_t t = 1; t < sizeOfTermsETS(); ++t) { - expr = BoolExpr::Or(expr, getTErmsETS()[t]); + BoolExpr* expr = getTErms()[0]; + DEBUG_LOG("number of rows for node ID %zu: %zu\n", id, sizeOfTerms()); + for (size_t t = 1; t < sizeOfTerms(); ++t) { + expr = BoolExpr::Or(expr, getTErms()[t]); DEBUG_LOG("Intermediate OR expr for node ID %zu: %s\n", id, expr->toString().c_str()); } // Store the resulting expression in the memo table and in the iso map. - setMemoETS(id, expr); + setMemo(id, expr); iso2boolExpr_[isoID] = expr; DEBUG_LOG("Bool expression for node ID %zu: %s\n", id, expr->toString().c_str()); } @@ -397,5 +397,5 @@ BoolExpr* Tree2BoolExpr::convert( } // 4) return root expression from memo table. - return getMemoETS(root->nodeID); + return getMemo(root->nodeID); } diff --git a/src/strategies/miter/BuildPrimaryOutputClauses.cpp b/src/strategies/miter/BuildPrimaryOutputClauses.cpp index 93b99552..b4ecea2c 100644 --- a/src/strategies/miter/BuildPrimaryOutputClauses.cpp +++ b/src/strategies/miter/BuildPrimaryOutputClauses.cpp @@ -541,65 +541,6 @@ void BuildPrimaryOutputClauses::build() { std::chrono::duration elapsed_seconds_comp = endComp - startComp; printf("Computation time for %lu: %f seconds\n", i, elapsed_seconds_comp.count()); #endif - // //cloud.SNLDesignModeling::getTruthTable().print(); - // std::vector test1; - // std::vector test2; - // for (auto in : cloud.getAllInputs()) { - // printf("Input in tree cloud: %lu\n", in); - // // if (in >= cloud.getInputs().size()) { - // // printf("size of inputs in cloud: %lu\n", - // cloud.getInputs().size()); - // // //assert(false && "Input in cloud is out of range"); - // // } - // test1.emplace_back(in); - // } - // for (auto in : cloud.getInputs()) { - // printf("Input in cloud: %lu\n", in); - // test2.emplace_back(in); - // } - // std::sort(test1.begin(), test1.end()); - // std::sort(test2.begin(), test2.end()); - // assert(test1 == test2); - // std::vector varNames; - /*for (auto input : cloud.getInputs()) { - DNLTerminalFull term = get()->getDNLTerminalFromID(input); - if (term.getSnlTerm() != nullptr) { - auto net = term.getSnlTerm()->getNet(); - if (net != nullptr) { - if (net->isConstant0()) { - varNames.emplace_back("0"); - continue; - } else if (net->isConstant1()) { - varNames.emplace_back("1"); - continue; - } - } - auto model = const_cast( - term.getSnlBitTerm()->getDesign()); - auto tt = model->SNLDesignModeling::getTruthTable(term.getSnlBitTerm()->getOrderID()); - if (tt.isInitialized()) { - if (tt.all0()) { - varNames.emplace_back("0"); - continue; - } else if (tt.all1()) { - varNames.emplace_back("1"); - continue; - } - } - } - // find the index of input in inputs_ - auto it = std::find(inputs_.begin(), inputs_.end(), input); - // printf("Input: %s\n", - // - get()->getDNLTerminalFromID(input).getSnlBitTerm()->getName().getString().c_str()); - // printf("Model: %s\n", - // - get()->getDNLTerminalFromID(input).getSnlBitTerm()->getDesign()->getName().getString().c_str()); - assert(it != inputs_.end()); - size_t index = std::distance(inputs_.begin(), it); - varNames.emplace_back(std::to_string(index + 2)); // +2 to avoid 0 and 1 - which are reserved for constants - }*/ #ifdef DEBUG_CHECKS assert(cloud.SNLDesignModeling::getTruthTable().isInitialized()); #endif @@ -709,32 +650,3 @@ void BuildPrimaryOutputClauses::setOutputs2OutputsIDs() { } // Sort functions are retierd for now as they break the mapping between the 2 circuits, normalize is used instead - -// void BuildPrimaryOutputClauses::sortInputs() { -// // Sort based on inputs2inputsIDs_ content -// std::sort(inputs_.begin(), inputs_.end(), -// [this](const DNLID& a, const DNLID& b) { -// return inputs2inputsIDs_[a].first < inputs2inputsIDs_[b].first && -// inputs2inputsIDs_[a].second < inputs2inputsIDs_[b].second; -// }); -// } - -// void BuildPrimaryOutputClauses::sortOutputs() { -// // Sort based on outputs2outputsIDs_ content -// std::sort( -// outputs_.begin(), outputs_.end(), [this](const DNLID& a, const DNLID& b) { -// return outputs2outputsIDs_[a].first < outputs2outputsIDs_[b].first && -// outputs2outputsIDs_[a].second < outputs2outputsIDs_[b].second; -// }); -// } - -// const naja::NL::SNLTruthTable& BuildPrimaryOutputClauses::getTruthTable(naja::NL::SNLDesign* design, size_t orderID) { -// auto designID = design->getID(); -// auto iter = ttCache_.find({designID, orderID}); -// if (iter != ttCache_.end()) { -// return iter->second; -// } -// const auto tt = SNLDesignModeling::getTruthTable(design, orderID); -// ttCache_[{designID, orderID}] = tt; -// return tt; -// } \ No newline at end of file From a2367ca06fdaafbec0df972e07ea0b6b646c595a Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Thu, 5 Feb 2026 22:58:21 +0100 Subject: [PATCH 3/5] cleaning --- src/clauses/Tree2BoolExpr.cpp | 288 +++++++++++++++++----------------- 1 file changed, 142 insertions(+), 146 deletions(-) diff --git a/src/clauses/Tree2BoolExpr.cpp b/src/clauses/Tree2BoolExpr.cpp index 0fe91511..01b0b9eb 100644 --- a/src/clauses/Tree2BoolExpr.cpp +++ b/src/clauses/Tree2BoolExpr.cpp @@ -38,113 +38,104 @@ using namespace KEPLER_FORMAL; tbb::concurrent_unordered_map Tree2BoolExpr::iso2boolExpr_ = tbb::concurrent_unordered_map(); -// Helper typedefs for thread-local containers. Each pair stores a vector -// allocated with TBB allocator and a size_t representing the logical size. -// These thread-local containers avoid repeated allocations during traversal. - -typedef std::vector> TermsPair; - -// Thread-local storage for DNF terms while building expressions for a node. -thread_local TermsPair terms; - -TermsPair& getTErms() { - return terms; +// Temporary storage for DNF terms (as BoolExpr*) while building expressions for a node. +// Used to accumulate DNF terms before folding them into an OR expression. +typedef std::vector> TempDNFTermsVec; +// Thread-local storage for DNF terms during node processing. +thread_local TempDNFTermsVec tempDNFTerms; +// Accessor for thread-local DNF terms vector. +TempDNFTermsVec& getTempDNFTerms() { + return tempDNFTerms; } - -size_t sizeOfTerms() { - return getTErms().size(); +// Returns the number of DNF terms currently stored. +size_t sizeOfTempDNFTerms() { + return getTempDNFTerms().size(); } - -void clearTerms() { - auto& termsLocal = getTErms(); - termsLocal.clear(); +// Clears the DNF terms vector. +void clearTempDNFTerms() { + auto& local = getTempDNFTerms(); + local.clear(); } - -void pushBackTerms(BoolExpr* term) { - getTErms().emplace_back(term); +// Appends a DNF term (BoolExpr*) to the vector. +void pushTempDNFTerm(BoolExpr* term) { + getTempDNFTerms().emplace_back(term); } - -bool emptyTerms() { - return getTErms().empty(); +// Returns true if no DNF terms are present. +bool emptyTempDNFTerms() { + return getTempDNFTerms().empty(); } -// Relevant inputs bitset per node: which child inputs actually affect the table. -// Stored as a vector (bool-like) with a logical size. -typedef std::pair>, size_t> RelevantPair; - -thread_local RelevantPair relevant; - -RelevantPair& getRelevant() { - return relevant; +// Bitset per node indicating which child inputs actually affect the table (relevant inputs). +// Used to optimize DNF generation by ignoring irrelevant inputs. +typedef std::pair>, size_t> RelevantInputsPair; +// Thread-local storage for relevant input bits and logical size. +thread_local RelevantInputsPair relevantInputs; +// Accessor for thread-local relevant input bits. +RelevantInputsPair& getRelevantInputs() { + return relevantInputs; } - -size_t sizeOfRelevant() { - return getRelevant().second; +// Returns the current logical size of relevant inputs. +size_t sizeOfRelevantInputs() { + return getRelevantInputs().second; } - -void clearRelevant() { - auto& relevantLocal = getRelevant(); - relevantLocal.first.clear(); +// Clears the relevant inputs vector. +void clearRelevantInputs() { + auto& local = getRelevantInputs(); + local.first.clear(); } - -void setRelevant(size_t i, bool b) { - auto& relevantLocal = getRelevant(); - if (i >= relevantLocal.second) { +// Sets the relevant flag for input i. +void setRelevantInput(size_t i, bool b) { + auto& local = getRelevantInputs(); + if (i >= local.second) { // LCOV_EXCL_START - assert(false && "setRelevant: index out of range"); + assert(false && "setRelevantInput: index out of range"); // LCOV_EXCL_STOP } - relevantLocal.first[i] = b; + local.first[i] = b; } - -bool getRelevant(size_t i) { - auto& relevantLocal = getRelevant(); - if (i >= relevantLocal.second) { +// Gets the relevant flag for input i. +bool getRelevantInput(size_t i) { + auto& local = getRelevantInputs(); + if (i >= local.second) { // LCOV_EXCL_START - throw std::out_of_range("getRelevant: index out of range"); + throw std::out_of_range("getRelevantInput: index out of range"); // LCOV_EXCL_STOP } - return relevantLocal.first[i]; + return local.first[i]; } - -// Ensure the relevant vector has at least n entries and initialize them to false. -// The logical size is stored in the second element of the pair. -void reserveRelevantwithFalse(size_t n) { - auto& relevantLocal = getRelevant(); - auto& vec = relevantLocal.first; - auto& sz = relevantLocal.second; +// Ensure the relevant inputs vector has at least n entries and initialize them to false. +void reserveRelevantInputsWithFalse(size_t n) { + auto& local = getRelevantInputs(); + auto& vec = local.first; + auto& sz = local.second; if (vec.size() >= n) { vec.assign(n, false); sz = n; return; } - size_t oldSize = vec.size(); vec.resize(n, false); vec.assign(n, false); sz = n; } // Memoization table (thread-local) mapping node IDs to BoolExpr* results. -// The vector is preallocated and indexed by node ID for O(1) lookup. -typedef std::pair>, size_t> MemoPair; - -thread_local MemoPair memo; - -MemoPair& getMemo() { - return memo; +// Used to cache results of subtrees during traversal. +typedef std::pair>, size_t> NodeExprCachePair; +thread_local NodeExprCachePair nodeExprCache; +// Accessor for thread-local node expression cache. +NodeExprCachePair& getNodeExprCache() { + return nodeExprCache; } - -void clearMemo() { - auto& memoLocal = getMemo(); - memoLocal.first.clear(); +// Clears the node expression cache. +void clearNodeExprCache() { + auto& local = getNodeExprCache(); + local.first.clear(); } - -// Reserve and initialize the memo table to a given logical size. -// The vector elements are set to nullptr to indicate "not computed". -void reserveMemo(size_t n) { - auto& memoLocal = getMemo(); - auto& vec = memoLocal.first; - auto& sz = memoLocal.second; +// Reserve and initialize the node expression cache to a given logical size. +void reserveNodeExprCache(size_t n) { + auto& local = getNodeExprCache(); + auto& vec = local.first; + auto& sz = local.second; if (vec.size() >= n) { sz = n; vec.assign(n, nullptr); @@ -154,38 +145,37 @@ void reserveMemo(size_t n) { sz = n; vec.assign(n, nullptr); } - -void setMemo(size_t i, BoolExpr* expr) { - auto& memoLocal = getMemo(); - assert(i < memoLocal.second && "setMemo: index out of range"); - memoLocal.first[i] = expr; +// Sets the cached BoolExpr* for node i. +void setNodeExprCache(size_t i, BoolExpr* expr) { + auto& local = getNodeExprCache(); + assert(i < local.second && "setNodeExprCache: index out of range"); + local.first[i] = expr; } - -BoolExpr* getMemo(size_t i) { - auto& memoLocal = getMemo(); - assert(i < memoLocal.second && "getMemo: index out of range"); - return memoLocal.first[i]; +// Gets the cached BoolExpr* for node i. +BoolExpr* getNodeExprCache(size_t i) { + auto& local = getNodeExprCache(); + assert(i < local.second && "getNodeExprCache: index out of range"); + return local.first[i]; } // Temporary storage for child BoolExpr pointers while processing a table node. -typedef std::pair>, size_t> ChildFPair; - -thread_local ChildFPair childF; - -ChildFPair& getChildF() { - return childF; +// Used to gather child expressions of the current node for DNF construction. +typedef std::pair>, size_t> ChildExprsPair; +thread_local ChildExprsPair childExprs; +// Accessor for thread-local child expressions. +ChildExprsPair& getChildExprs() { + return childExprs; } - -void clearChildF() { - auto& childLocal = getChildF(); - childLocal.second = 0; +// Clears the child expressions (sets logical size to 0). +void clearChildExprs() { + auto& local = getChildExprs(); + local.second = 0; } - -// Reserve child storage and initialize entries to nullptr. -void reserveChildF(size_t n) { - auto& childLocal = getChildF(); - auto& vec = childLocal.first; - auto& sz = childLocal.second; +// Reserve child expression storage and initialize entries to nullptr. +void reserveChildExprs(size_t n) { + auto& local = getChildExprs(); + auto& vec = local.first; + auto& sz = local.second; if (vec.size() >= n) { sz = n; vec.assign(n, nullptr); @@ -195,27 +185,28 @@ void reserveChildF(size_t n) { sz = n; vec.assign(n, nullptr); } - -BoolExpr* getChildF(size_t i) { - auto& childLocal = getChildF(); - assert(i < childLocal.second && "getChildF: index out of range"); - return childLocal.first[i]; +// Gets the child expression at index i. +BoolExpr* getChildExpr(size_t i) { + auto& local = getChildExprs(); + assert(i < local.second && "getChildExpr: index out of range"); + return local.first[i]; } - -void setChildF(size_t i, BoolExpr* expr) { - auto& childLocal = getChildF(); - assert(i < childLocal.second && "setChildF: index out of range"); - childLocal.first[i] = expr; +// Sets the child expression at index i. +void setChildExpr(size_t i, BoolExpr* expr) { + auto& local = getChildExprs(); + assert(i < local.second && "setChildExpr: index out of range"); + local.first[i] = expr; } // Frame type used for explicit stack-based post-order traversal. // Each frame holds a pointer to a node and a boolean indicating whether // the node has been visited (post-visit) or not (pre-visit). using Frame = std::pair; -thread_local std::vector> stack; - -std::vector>& getStack() { - return stack; +// Explicit traversal stack used to avoid recursion during tree traversal. +thread_local std::vector> traversalStack; +// Accessor for thread-local traversal stack. +std::vector>& getTraversalStack() { + return traversalStack; } // Main conversion routine: converts an SNLTruthTableTree into a BoolExpr. @@ -230,12 +221,12 @@ BoolExpr* Tree2BoolExpr::convert( // Determine maximum node ID to size memoization structures. size_t maxID = tree.getMaxID(); - // 2) memo table: clear and reserve memoization storage for all node IDs. - clearMemo(); - reserveMemo(maxID + 1); + // 2) node expression cache: clear and reserve memoization storage for all node IDs. + clearNodeExprCache(); + reserveNodeExprCache(maxID + 1); // 3) post-order build using an explicit stack to avoid recursion. - auto & stack = getStack(); + auto & stack = getTraversalStack(); stack.clear(); stack.emplace_back(root.get(), false); @@ -260,11 +251,11 @@ BoolExpr* Tree2BoolExpr::convert( if (node->type != SNLTruthTableTree::Node::Type::Input) { isoID = naja::DNL::get()->getDNLTerminalFromID(node->data.termid).getIsoID(); if (iso2boolExpr_.find(isoID) != iso2boolExpr_.end() && isoID != naja::DNL::DNLID_MAX) { - setMemo(id, iso2boolExpr_[isoID]); + setNodeExprCache(id, iso2boolExpr_[isoID]); } } // If memo already contains an expression for this node, skip processing. - if (getMemo(id) != nullptr) continue; + if (getNodeExprCache(id) != nullptr) continue; // If node is a Table or P node, push it back as visited and push children. if (node->type == SNLTruthTableTree::Node::Type::Table || node->type == SNLTruthTableTree::Node::Type::P) { @@ -301,14 +292,14 @@ BoolExpr* Tree2BoolExpr::convert( } // Special handling for constant mappings: 0 -> false, 1 -> true. if (name == 0) { - setMemo(id, BoolExpr::createFalse()); + setNodeExprCache(id, BoolExpr::createFalse()); iso2boolExpr_[isoID] = BoolExpr::createFalse(); } else if (name == 1) { - setMemo(id, BoolExpr::createTrue()); + setNodeExprCache(id, BoolExpr::createTrue()); iso2boolExpr_[isoID] = BoolExpr::createTrue(); } else { // Normal variable mapping. - setMemo(id, BoolExpr::Var(name)); + setNodeExprCache(id, BoolExpr::Var(name)); iso2boolExpr_[isoID] = BoolExpr::Var(name); } } @@ -326,35 +317,40 @@ BoolExpr* Tree2BoolExpr::convert( { // Gather child BoolExpr pointers into a temporary array for quick access. - clearChildF(); - reserveChildF(k); + clearChildExprs(); + reserveChildExprs(k); for (uint32_t i = 0; i < k; ++i) { size_t cid = node->tree->nodeFromId(node->childrenIds[i])->nodeID; - setChildF(i, getMemo(cid)); + setChildExpr(i, getNodeExprCache(cid)); } // Determine which inputs actually matter for this truth table. // For each input j, check if flipping bit j changes the table output. - clearRelevant(); - reserveRelevantwithFalse(k); + clearRelevantInputs(); + reserveRelevantInputsWithFalse(k); for (uint32_t j = 0; j < k; ++j) { for (uint64_t m = 0; m < rows; ++m) { bool b0 = tbl.bits().bit(m); bool b1 = tbl.bits().bit(m ^ (uint64_t{1} << j)); - if (b0 != b1) { setRelevant(j, true); break; } + if (b0 != b1) { setRelevantInput(j, true); break; } } } // Count how many inputs are relevant. size_t numRelIdx = 0; - for (uint32_t j = 0; j < k; ++j) { if (getRelevant(j)) numRelIdx++; } + for (uint32_t j = 0; j < k; ++j) { if (getRelevantInput(j)) numRelIdx++; } // The algorithm expects at least one relevant input for a PI node. assert(numRelIdx > 0 && "No relevant inputs for node"); { + // DNF (Disjunctive Normal Form) construction: + // For each row in the truth table where the output is 1, create a term that is + // an AND of literals corresponding to the relevant inputs (child expressions + // or their negations depending on the row). Then these terms will be OR-ed + // together to form the full expression for this node. // Build DNF terms by iterating over rows where the table output is 1. // For each such row, create a conjunction of literals for relevant inputs. - clearTerms(); + clearTempDNFTerms(); for (uint64_t m = 0; m < rows; ++m) { if (!tbl.bits().bit(m)) continue; BoolExpr* term = nullptr; @@ -363,31 +359,31 @@ BoolExpr* Tree2BoolExpr::convert( // For each relevant input, pick the literal (child or its negation) // according to the bit value in row m. for (uint32_t j = 0; j < k; ++j) { - if (!getRelevant(j)) { + if (!getRelevantInput(j)) { continue; } bool bit1 = ((m >> j) & 1) != 0; - lit = bit1 ? getChildF(j) : BoolExpr::Not(getChildF(j)); + lit = bit1 ? getChildExpr(j) : BoolExpr::Not(getChildExpr(j)); if (firstLit) { term = lit; firstLit = false; } else { assert(term != nullptr); assert(lit != nullptr); term = BoolExpr::And(term, lit); } } // Only push the term if at least one literal was included. - if (term) { pushBackTerms(std::move(term)); } + if (term) { pushTempDNFTerm(std::move(term)); } } // There must be at least one term for a PI node. - assert(!emptyTerms()); // Should be a PI + assert(!emptyTempDNFTerms()); // Should be a PI { // Fold the list of terms into a single expression by OR-ing them. - BoolExpr* expr = getTErms()[0]; - DEBUG_LOG("number of rows for node ID %zu: %zu\n", id, sizeOfTerms()); - for (size_t t = 1; t < sizeOfTerms(); ++t) { - expr = BoolExpr::Or(expr, getTErms()[t]); + BoolExpr* expr = getTempDNFTerms()[0]; + DEBUG_LOG("number of rows for node ID %zu: %zu\n", id, sizeOfTempDNFTerms()); + for (size_t t = 1; t < sizeOfTempDNFTerms(); ++t) { + expr = BoolExpr::Or(expr, getTempDNFTerms()[t]); DEBUG_LOG("Intermediate OR expr for node ID %zu: %s\n", id, expr->toString().c_str()); } - // Store the resulting expression in the memo table and in the iso map. - setMemo(id, expr); + // Store the resulting expression in the node expression cache and in the iso map. + setNodeExprCache(id, expr); iso2boolExpr_[isoID] = expr; DEBUG_LOG("Bool expression for node ID %zu: %s\n", id, expr->toString().c_str()); } @@ -396,6 +392,6 @@ BoolExpr* Tree2BoolExpr::convert( } } - // 4) return root expression from memo table. - return getMemo(root->nodeID); + // 4) return root expression from node expression cache. + return getNodeExprCache(root->nodeID); } From 98c6045356414ebf617cc48d199af0e8fc84fa98 Mon Sep 17 00:00:00 2001 From: nanocoh Date: Thu, 12 Feb 2026 21:00:30 +0100 Subject: [PATCH 4/5] fixes --- src/bin/KeplerFormal.cpp | 10 ++++++++-- src/scope/ScopeExtraction.cpp | 1 + thirdparty/naja | 2 +- 3 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/bin/KeplerFormal.cpp b/src/bin/KeplerFormal.cpp index 0d61f338..67d29798 100644 --- a/src/bin/KeplerFormal.cpp +++ b/src/bin/KeplerFormal.cpp @@ -219,7 +219,10 @@ int main(int argc, char** argv) { } } else { // SNL std::printf("Loading Naja IF: %s\n", inputPaths[0].c_str()); - db0 = SNLCapnP::load(inputPaths[0].c_str(), primitivesAreLoaded); + naja::NL::SNLCapnP::LoadingConfiguration config; + config.primitiveConflictPolicy_ = primitivesAreLoaded ? naja::NL::SNLCapnP::LoadingConfiguration::PrimitiveConflictPolicy::PreferExisting : + naja::NL::SNLCapnP::LoadingConfiguration::PrimitiveConflictPolicy::ForbidConflicts; + db0 = SNLCapnP::load(inputPaths[0].c_str(), config); if (!db0) { // LCOV_EXCL_START SPDLOG_CRITICAL("Failed to load Naja IF: {}", inputPaths[0]); @@ -269,7 +272,10 @@ int main(int argc, char** argv) { } } else { // SNL std::printf("Loading Naja IF: %s\n", inputPaths[1].c_str()); - db1 = SNLCapnP::load(inputPaths[1].c_str(), primitivesAreLoaded); + naja::NL::SNLCapnP::LoadingConfiguration config; + config.primitiveConflictPolicy_ = primitivesAreLoaded ? naja::NL::SNLCapnP::LoadingConfiguration::PrimitiveConflictPolicy::PreferExisting : + naja::NL::SNLCapnP::LoadingConfiguration::PrimitiveConflictPolicy::ForbidConflicts; + db0 = SNLCapnP::load(inputPaths[1].c_str(), config); if (!db1) { // LCOV_EXCL_START SPDLOG_CRITICAL("Failed to load Naja IF: {}", inputPaths[1]); diff --git a/src/scope/ScopeExtraction.cpp b/src/scope/ScopeExtraction.cpp index 8d506623..0f1208cc 100644 --- a/src/scope/ScopeExtraction.cpp +++ b/src/scope/ScopeExtraction.cpp @@ -6,6 +6,7 @@ #include "RemoveLoadlessLogic.h" #include "SNLDesign.h" #include "SNLLogicCone.h" +#include "SNLBitNet.h" #include // #define DEBUG_PRINTS diff --git a/thirdparty/naja b/thirdparty/naja index fdf658ab..d4f8d5dd 160000 --- a/thirdparty/naja +++ b/thirdparty/naja @@ -1 +1 @@ -Subproject commit fdf658ab6e40701e57b33d1509aa775e1b71f0f1 +Subproject commit d4f8d5dda35ed0999886af873bfd4641a2d6e9bb From e2a114ebe880bd04ff3a9d9e8dfa86aebb6d53ec Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Thu, 12 Feb 2026 21:08:52 +0100 Subject: [PATCH 5/5] renaming --- src/clauses/SNLTruthTableTree.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/clauses/SNLTruthTableTree.cpp b/src/clauses/SNLTruthTableTree.cpp index 715e1e0b..2757a57a 100644 --- a/src/clauses/SNLTruthTableTree.cpp +++ b/src/clauses/SNLTruthTableTree.cpp @@ -29,10 +29,10 @@ using namespace KEPLER_FORMAL; typedef std::pair>, size_t> BorderLeavesPair; -thread_local BorderLeavesPair newBorderLeavesTLS; +thread_local BorderLeavesPair newBorderLeaves; BorderLeavesPair& getNewBorderLeaves() { - return newBorderLeavesTLS; + return newBorderLeaves; } size_t getSizeOfNewBorderLeaves() { @@ -58,10 +58,10 @@ using NodeRaw = SNLTruthTableTree::Node*; using NodeVecRaw = std::vector>; using NodeVecVecRaw = std::vector>; using ResolvedChildrenPairRaw = std::pair; -thread_local ResolvedChildrenPairRaw resolvedChildrenTLS; +thread_local ResolvedChildrenPairRaw resolvedChildren; ResolvedChildrenPairRaw& getResolvedChildren() { - return resolvedChildrenTLS; + return resolvedChildren; } void reserveResolvedChildren(size_t n) {