From d36d4a98d9f79edf21629a756969882e761b89c2 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Sun, 21 Dec 2025 14:04:44 +0100 Subject: [PATCH 1/2] update naja for gz liberty parser --- .github/workflows/c-cpp.yml | 2 +- .github/workflows/macOS.yml | 2 +- .github/workflows/regress.yml | 2 +- thirdparty/naja | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml index f9d60434..710738d9 100644 --- a/.github/workflows/c-cpp.yml +++ b/.github/workflows/c-cpp.yml @@ -30,7 +30,7 @@ jobs: sudo apt-get install -yq \ build-essential cmake ninja-build clang pkg-config \ libboost-dev libfl-dev libtbb-dev capnproto libcapnp-dev \ - libgtest-dev libspdlog-dev libfmt-dev + libgtest-dev libspdlog-dev libfmt-dev libboost-iostreams-dev zlib1g-dev - name: Configure CMake working-directory: ${{github.workspace}}/ diff --git a/.github/workflows/macOS.yml b/.github/workflows/macOS.yml index 0b72912f..2fdc1c70 100644 --- a/.github/workflows/macOS.yml +++ b/.github/workflows/macOS.yml @@ -27,7 +27,7 @@ jobs: run: git submodule update --init --recursive # install dependencies - name: Install dependencies - run: brew install cmake doxygen capnp tbb bison flex boost spdlog + run: brew install cmake doxygen capnp tbb bison flex boost spdlog zlib - name: set env variable run: | echo "/usr/local/opt/flex/bin" >> $GITHUB_PATH; echo "/usr/local/opt/bison/bin" >> $GITHUB_PATH; diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml index b6eff462..5ac73660 100644 --- a/.github/workflows/regress.yml +++ b/.github/workflows/regress.yml @@ -30,7 +30,7 @@ jobs: - name: Checkout submodules run: git submodule update --init --recursive - name: Install boost & capnproto - run: sudo apt-get update && sudo apt-get install -y pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libspdlog-dev + run: sudo apt-get update && sudo apt-get install -y pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libspdlog-dev libboost-iostreams-dev zlib1g-dev - name: Configure CMake run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20 diff --git a/thirdparty/naja b/thirdparty/naja index 7093e127..ee3d489e 160000 --- a/thirdparty/naja +++ b/thirdparty/naja @@ -1 +1 @@ -Subproject commit 7093e127c5ead385cd0044f105c72b25eac3eca5 +Subproject commit ee3d489e8f5d9b0d3d026b73eef6c965b83bbe3a From 8df7ad982a9854d9f947645c559fc9df5b48bf97 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Sun, 21 Dec 2025 15:03:35 +0100 Subject: [PATCH 2/2] fix (#35) --- src/clauses/Tree2BoolExpr.cpp | 233 ++++++++++++++-------------------- 1 file changed, 92 insertions(+), 141 deletions(-) diff --git a/src/clauses/Tree2BoolExpr.cpp b/src/clauses/Tree2BoolExpr.cpp index 0cf8f187..372b3410 100644 --- a/src/clauses/Tree2BoolExpr.cpp +++ b/src/clauses/Tree2BoolExpr.cpp @@ -5,44 +5,42 @@ #include "BoolExpr.h" #include "DNL.h" #include "SNLTruthTable.h" -#include "SNLTruthTableTree.h" // for SNLTruthTableTree::Node - +#include "SNLTruthTableTree.h" #include #include #include -#include // needed for bit-manipulation +#include #include #include #include -#include // for std::pair +#include #include using namespace naja::NL; using namespace KEPLER_FORMAL; -typedef std::pair, - tbb::tbb_allocator>>, - size_t> - TermsPair; +typedef std::pair, tbb::tbb_allocator>>, size_t> TermsPair; tbb::enumerable_thread_specific termsETS; tbb::concurrent_vector termsETSvector; void initTermsETS() { if (termsETSvector.size() <= tbb::this_task_arena::current_thread_index()) { - for (size_t i = termsETSvector.size(); - i <= tbb::this_task_arena::current_thread_index(); i++) { + for (size_t i = termsETSvector.size(); i <= tbb::this_task_arena::current_thread_index(); i++) { termsETSvector.push_back(nullptr); } } if (termsETSvector[tbb::this_task_arena::current_thread_index()] == nullptr) { - termsETSvector[tbb::this_task_arena::current_thread_index()] = - &termsETS.local(); + termsETSvector[tbb::this_task_arena::current_thread_index()] = &termsETS.local(); } } TermsPair& getTErmsETS() { - // initTermsETS(); - return *termsETSvector[tbb::this_task_arena::current_thread_index()]; + initTermsETS(); + size_t idx = tbb::this_task_arena::current_thread_index(); + if (idx >= termsETSvector.size() || termsETSvector[idx] == nullptr) { + throw std::runtime_error("getTErmsETS: not initialized for this thread"); + } + return *termsETSvector[idx]; } size_t sizeOfTermsETS() { @@ -73,8 +71,7 @@ void pushBackTermsETS(const std::shared_ptr& term) { void reserveTermsETS(size_t n) { auto& termsLocal = getTErmsETS(); - if (termsLocal.first.size() >= n) - return; + if (termsLocal.first.size() >= n) return; termsLocal.first.reserve(n); } @@ -83,29 +80,28 @@ bool emptyTermsETS() { } // same for std::vector> -typedef std::pair>, size_t> - RelevantPair; +typedef std::pair>, size_t> RelevantPair; tbb::enumerable_thread_specific relevantETS; tbb::concurrent_vector relevantETSvector; void initRelevantETS() { - if (relevantETSvector.size() <= - tbb::this_task_arena::current_thread_index()) { - for (size_t i = relevantETSvector.size(); - i <= tbb::this_task_arena::current_thread_index(); i++) { + if (relevantETSvector.size() <= tbb::this_task_arena::current_thread_index()) { + for (size_t i = relevantETSvector.size(); i <= tbb::this_task_arena::current_thread_index(); i++) { relevantETSvector.push_back(nullptr); } } - if (relevantETSvector[tbb::this_task_arena::current_thread_index()] == - nullptr) { - relevantETSvector[tbb::this_task_arena::current_thread_index()] = - &relevantETS.local(); + if (relevantETSvector[tbb::this_task_arena::current_thread_index()] == nullptr) { + relevantETSvector[tbb::this_task_arena::current_thread_index()] = &relevantETS.local(); } } RelevantPair& getRelevantETS() { - // initRelevantETS(); - return *relevantETSvector[tbb::this_task_arena::current_thread_index()]; + initRelevantETS(); + size_t idx = tbb::this_task_arena::current_thread_index(); + if (idx >= relevantETSvector.size() || relevantETSvector[idx] == nullptr) { + throw std::runtime_error("getRelevantETS: not initialized for this thread"); + } + return *relevantETSvector[idx]; } size_t sizeOfRelevantETS() { @@ -167,29 +163,28 @@ void reserveRelevantETSwithFalse(size_t n) { // do same for std::vector, // tbb::tbb_allocator>> memo; -typedef std::pair, - tbb::tbb_allocator>>, - size_t> - MemoPair; +typedef std::pair, tbb::tbb_allocator>>, size_t> MemoPair; tbb::enumerable_thread_specific memoETS; tbb::concurrent_vector memoETSvector; void initMemoETS() { if (memoETSvector.size() <= tbb::this_task_arena::current_thread_index()) { - for (size_t i = memoETSvector.size(); - i <= tbb::this_task_arena::current_thread_index(); i++) { + for (size_t i = memoETSvector.size(); i <= tbb::this_task_arena::current_thread_index(); i++) { memoETSvector.push_back(nullptr); } } if (memoETSvector[tbb::this_task_arena::current_thread_index()] == nullptr) { - memoETSvector[tbb::this_task_arena::current_thread_index()] = - &memoETS.local(); + memoETSvector[tbb::this_task_arena::current_thread_index()] = &memoETS.local(); } } MemoPair& getMemoETS() { - // initMemoETS(); - return *memoETSvector[tbb::this_task_arena::current_thread_index()]; + initMemoETS(); + size_t idx = tbb::this_task_arena::current_thread_index(); + if (idx >= memoETSvector.size() || memoETSvector[idx] == nullptr) { + throw std::runtime_error("getMemoETS: not initialized for this thread"); + } + return *memoETSvector[idx]; } size_t sizeOfMemoETS() { @@ -248,31 +243,30 @@ const std::shared_ptr& getMemoETS(size_t i) { return memoLocal.first[i]; } -// same for std::vector, +// same for std::vector>, // tbb::tbb_allocator>> childF; -typedef std::pair, - tbb::tbb_allocator>>, - size_t> - ChildFETSPair; +typedef std::pair, tbb::tbb_allocator>>, size_t> ChildFETSPair; tbb::enumerable_thread_specific childFETS; tbb::concurrent_vector childFETSvector; void initChildFETS() { if (childFETSvector.size() <= tbb::this_task_arena::current_thread_index()) { - for (size_t i = childFETSvector.size(); - i <= tbb::this_task_arena::current_thread_index(); i++) { + for (size_t i = childFETSvector.size(); i <= tbb::this_task_arena::current_thread_index(); i++) { childFETSvector.push_back(nullptr); } } - if (childFETSvector[tbb::this_task_arena::current_thread_index()] == - nullptr) { - childFETSvector[tbb::this_task_arena::current_thread_index()] = - &childFETS.local(); + if (childFETSvector[tbb::this_task_arena::current_thread_index()] == nullptr) { + childFETSvector[tbb::this_task_arena::current_thread_index()] = &childFETS.local(); } } ChildFETSPair& getChildFETS() { - return *childFETSvector[tbb::this_task_arena::current_thread_index()]; + initChildFETS(); + size_t idx = tbb::this_task_arena::current_thread_index(); + if (idx >= childFETSvector.size() || childFETSvector[idx] == nullptr) { + throw std::runtime_error("getChildFETS: not initialized for this thread"); + } + return *childFETSvector[idx]; } size_t sizeOfChildFETS() { @@ -335,83 +329,70 @@ size_t toSizeT(const std::string& s) { if (s.empty()) { assert(false && "toSizeT: empty string"); } - size_t result = 0; const size_t max = std::numeric_limits::max(); - for (unsigned char uc : s) { if (!std::isdigit(uc)) { - throw std::invalid_argument("toSizeT: invalid character '" + - std::string(1, static_cast(uc)) + - "' in input"); + throw std::invalid_argument("toSizeT: invalid character '" + std::string(1, static_cast(uc)) + "' in input"); } size_t digit = static_cast(uc - '0'); - // Check for overflow: result * 10 + digit > max if (result > (max - digit) / 10) { throw std::out_of_range("toSizeT: value out of range for size_t"); } - result = result * 10 + digit; } - return result; } // Fold a list of literals into a single AND static std::shared_ptr mkAnd( - const std::vector, - tbb::tbb_allocator>>& lits) { - if (lits.empty()) - return BoolExpr::createTrue(); + const std::vector, tbb::tbb_allocator>>& lits) { + if (lits.empty()) return BoolExpr::createTrue(); auto cur = lits[0]; - for (size_t i = 1; i < lits.size(); ++i) - cur = BoolExpr::And(cur, lits[i]); + for (size_t i = 1; i < lits.size(); ++i) cur = BoolExpr::And(cur, lits[i]); return cur; } // Fold a list of terms into a single OR static std::shared_ptr mkOr( - const std::vector, - tbb::tbb_allocator>>& terms) { - if (terms.empty()) - return BoolExpr::createFalse(); + const std::vector, tbb::tbb_allocator>>& terms) { + if (terms.empty()) return BoolExpr::createFalse(); auto cur = terms[0]; - for (size_t i = 1; i < terms.size(); ++i) - cur = BoolExpr::Or(cur, terms[i]); + for (size_t i = 1; i < terms.size(); ++i) cur = BoolExpr::Or(cur, terms[i]); return cur; } std::shared_ptr Tree2BoolExpr::convert( - const SNLTruthTableTree& tree, - const std::vector& varNames) { + const SNLTruthTableTree& tree, const std::vector& varNames) { + initChildFETS(); initMemoETS(); initRelevantETS(); initTermsETS(); + const auto root = tree.getRoot(); - if (!root) - return nullptr; + if (!root) return nullptr; // 1) find maxID // size_t maxID = 0; // { - // using NodePtr = const SNLTruthTableTree::Node*; - // std::vector> dfs; - // dfs.reserve(128); - // dfs.push_back(root.get()); - // while (!dfs.empty()) { - // NodePtr n = dfs.back(); dfs.pop_back(); - // maxID = std::max(maxID, (size_t) n->nodeID); - // if (n->type == SNLTruthTableTree::Node::Type::Table || - // n->type == SNLTruthTableTree::Node::Type::P) - // { - // for (const auto& c : n->childrenIds) { - // assert(n->tree->nodeFromId(c).get() != nullptr); - // dfs.push_back(n->tree->nodeFromId(c).get()); - // } - // } - // } + // using NodePtr = const SNLTruthTableTree::Node*; + // std::vector> dfs; + // dfs.reserve(128); + // dfs.push_back(root.get()); + // while (!dfs.empty()) { + // NodePtr n = dfs.back(); + // dfs.pop_back(); + // maxID = std::max(maxID, (size_t) n->nodeID); + // if (n->type == SNLTruthTableTree::Node::Type::Table || // n->type == SNLTruthTableTree::Node::Type::P) + // { + // for (const auto& c : n->childrenIds) { + // assert(n->tree->nodeFromId(c).get() != nullptr); + // dfs.push_back(n->tree->nodeFromId(c).get()); + // } + // } + // } // } size_t maxID = tree.getMaxID(); @@ -419,6 +400,7 @@ std::shared_ptr Tree2BoolExpr::convert( // 2) memo table clearMemoETS(); reserveMemoETS(maxID + 1); + // 3) post-order build using Frame = std::pair; std::vector> stack; @@ -433,42 +415,26 @@ std::shared_ptr Tree2BoolExpr::convert( size_t id = node->nodeID; if (!visited) { - if (getMemoETS(id) != nullptr) - continue; - - if (node->type == SNLTruthTableTree::Node::Type::Table || - node->type == SNLTruthTableTree::Node::Type::P) { + if (getMemoETS(id) != nullptr) continue; + if (node->type == SNLTruthTableTree::Node::Type::Table || node->type == SNLTruthTableTree::Node::Type::P) { stack.emplace_back(node, true); - for (const auto& c : node->childrenIds) - stack.emplace_back(node->tree->nodeFromId(c).get(), false); + for (const auto& c : node->childrenIds) stack.emplace_back(node->tree->nodeFromId(c).get(), false); } else { assert(node->type == SNLTruthTableTree::Node::Type::Input); if (node->parentIds.size() > 1) { for (const auto& pid : node->parentIds) { - printf("%s\n", - naja::DNL::get() - ->getDNLTerminalFromID(tree.nodeFromId(pid)->data.termid) - .getSnlBitTerm() - ->getString() - .c_str()); - printf("of model %s\n", - naja::DNL::get() - ->getDNLTerminalFromID(tree.nodeFromId(pid)->data.termid) - .getDNLInstance() - .getSNLModel() - ->getString() - .c_str()); + printf("%s\n", naja::DNL::get()->getDNLTerminalFromID(tree.nodeFromId(pid)->data.termid) + .getSnlBitTerm()->getString().c_str()); + printf("of model %s\n", naja::DNL::get()->getDNLTerminalFromID(tree.nodeFromId(pid)->data.termid) + .getDNLInstance().getSNLModel()->getString().c_str()); } } - if (node->parentIds.empty()) { - throw std::runtime_error("Input node has no parent"); - } + if (node->parentIds.empty()) { throw std::runtime_error("Input node has no parent"); } assert(node->parentIds.size() == 1); auto parent = node->tree->nodeFromId(node->parentIds[0]); assert(parent && parent->type == SNLTruthTableTree::Node::Type::P); if (parent->data.termid >= varNames.size()) { - printf("varNames size: %zu, parent data.termid: %zu\n", - varNames.size(), (size_t)parent->data.termid); + printf("varNames size: %zu, parent data.termid: %zu\n", varNames.size(), (size_t)parent->data.termid); assert(parent->data.termid < varNames.size()); } if (varNames[parent->data.termid] == (size_t)-1) { @@ -502,18 +468,14 @@ std::shared_ptr Tree2BoolExpr::convert( 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) { setRelevantETS(j, true); break; } } } + // collect the indices of relevant vars std::vector> relIdx; - for (uint32_t j = 0; j < k; ++j) { - if (getRelevantETS(j)) - relIdx.push_back(j); - } + for (uint32_t j = 0; j < k; ++j) { if (getRelevantETS(j)) relIdx.push_back(j); } + // if nothing matters, fall back to constant-false if (relIdx.empty()) { setMemoETS(id, BoolExpr::createFalse()); @@ -521,35 +483,24 @@ std::shared_ptr Tree2BoolExpr::convert( // build the DNF terms clearTermsETS(); reserveTermsETS(static_cast(rows)); - for (uint64_t m = 0; m < rows; ++m) { - if (!tbl.bits().bit(m)) - continue; - + if (!tbl.bits().bit(m)) continue; std::shared_ptr term = nullptr; bool firstLit = true; std::shared_ptr lit = nullptr; for (uint32_t j : relIdx) { bool bit1 = ((m >> j) & 1) != 0; lit = bit1 ? getChildFETS(j) : BoolExpr::Not(getChildFETS(j)); - if (firstLit) { - term = lit; - firstLit = false; - } else { - assert(term != nullptr); - assert(lit != nullptr); - term = BoolExpr::And(term, lit); - } + if (firstLit) { term = lit; firstLit = false; } + else { assert(term != nullptr); assert(lit != nullptr); term = BoolExpr::And(term, lit); } } // only push if we actually got a literal - if (term) { - pushBackTermsETS(std::move(term)); - } + if (term) { pushBackTermsETS(std::move(term)); } } + // guard against an empty terms list - if (emptyTermsETS()) { - setMemoETS(id, BoolExpr::createFalse()); - } else { + if (emptyTermsETS()) { setMemoETS(id, BoolExpr::createFalse()); } + else { // fold into OR std::shared_ptr expr = getTErmsETS().first[0]; for (size_t t = 1; t < sizeOfTermsETS(); ++t) {