Skip to content

cleaning #85

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
nanocoh wants to merge 7 commits into
base: main
Choose a base branch
from
Open

cleaning #85

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
1536809
build primary points fix
nanocoh Feb 5, 2026
4a3a500
cleaning
nanocoh Feb 5, 2026
56cb403
Merge branch 'main' into fix2
nanocoh Feb 5, 2026
a2367ca
cleaning
nanocoh Feb 5, 2026
8c6ec50
Merge branch 'fix2' of https://github.com/keplertech/kepler-formal in…
nanocoh Feb 5, 2026
98c6045
fixes
nanocoh Feb 12, 2026
e2a114e
renaming
nanocoh Feb 12, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 8 additions & 2 deletions src/bin/KeplerFormal.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]);
Expand Down Expand Up @@ -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]);
Expand Down
166 changes: 83 additions & 83 deletions src/clauses/SNLLogicCloud.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,67 +24,67 @@ using namespace naja::DNL;
typedef std::pair<
std::vector<naja::DNL::DNLID, tbb::tbb_allocator<naja::DNL::DNLID>>,
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<naja::DNL::DNLID, tbb::tbb_allocator<naja::DNL::DNLID>>& res) {
void copyCurrentIterationInputs(std::vector<naja::DNL::DNLID, tbb::tbb_allocator<naja::DNL::DNLID>>& 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
}

Expand All @@ -93,27 +93,27 @@ thread_local std::pair<
tbb::tbb_allocator<std::pair<naja::DNL::DNLID,
naja::DNL::DNLID>>>,
size_t>
inputsToMergeETS;
inputsToMerge;

std::pair<std::vector<std::pair<naja::DNL::DNLID, naja::DNL::DNLID>,
tbb::tbb_allocator<std::pair<naja::DNL::DNLID,
naja::DNL::DNLID>>>, 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<naja::DNL::DNLID, naja::DNL::DNLID>& 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
Expand All @@ -128,7 +128,7 @@ typedef std::vector<
tbb::tbb_allocator<naja::DNL::DNLID>>>>
VisitedTermsPairsVec;

thread_local VisitedTermsPairsVec visitedTermsPairsETS;
thread_local VisitedTermsPairsVec visitedTermsPairs;

struct PairHash {
size_t operator()(const std::pair<naja::DNL::DNLID,naja::DNL::DNLID>& p) const noexcept {
Expand All @@ -148,19 +148,19 @@ struct PairHash {
PairHash, PairEq,
tbb::tbb_allocator<std::pair<naja::DNL::DNLID, naja::DNL::DNLID>>>;

thread_local HandledSet visitedTermsPairsETSSet;
thread_local HandledSet visitedTermsPairsSet;

void clearVisitedTermsPairsETS() {
visitedTermsPairsETSSet.clear();
void clearVisitedTermsPairs() {
visitedTermsPairsSet.clear();
}

thread_local std::pair<naja::DNL::DNLID, naja::DNL::DNLID> tempPairETS;
thread_local std::pair<naja::DNL::DNLID, naja::DNL::DNLID> 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;
Expand All @@ -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_)) {
Expand Down Expand Up @@ -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;
Expand All @@ -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);
}
}
Expand All @@ -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);
}
}
Expand All @@ -251,49 +251,49 @@ 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;
}
} // allocator for buckets

// 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;
}
Expand Down Expand Up @@ -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",
Expand All @@ -370,7 +370,7 @@ void SNLLogicCloud::compute() {
.getString()
.c_str(),
driver);
pushBackInputsToMergeETS(
pushBackInputsToMerge(
{naja::DNL::DNLID_MAX, driver}); // Placeholder for PI/PO
continue;
}
Expand All @@ -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",
Expand All @@ -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;
}
Expand All @@ -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());
Expand Down
Loading
Loading