Skip to content

[d4] Add d4 symbolic compiler v2.0.0#13453

Open
SSJ0406 wants to merge 9 commits intoJuliaPackaging:masterfrom
SSJ0406:sm/d4
Open

[d4] Add d4 symbolic compiler v2.0.0#13453
SSJ0406 wants to merge 9 commits intoJuliaPackaging:masterfrom
SSJ0406:sm/d4

Conversation

@SSJ0406
Copy link
Copy Markdown

@SSJ0406 SSJ0406 commented Apr 6, 2026

This compiler is used for d-DNNF knowledge compilation.

Key changes in this version:

  • Compatibility: Enforced the C++17 standard and added patches to ensure compatibility with selected C++20 features.
  • Shared Library: Switched from a static library to a shared library (libd4) to enable JLL loading.
  • Build System: Fully integrated the CLI tool and third-party components (Bipe, flowCutter, Glucose) into a clean CMake-based build system.
  • ABI Stability: Migrated to GCC 11 and ensured compatibility with Julia 1.10 to support the Boost 1.87 ABI, along with the addition of expand_cxxstring_abis().
  • Windows Support: Used CompilerSupportLibraries_jll to safely bundle runtime libraries (libgcc, libstdc++, libwinpthread).
  • Clean-up: Removed legacy support for the PaToH partitioner and fixed global uintXX_t types to improve cross-platform portability.

Comment thread D/d4/build_tarballs.jl Outdated
@StefanKarpinski
Copy link
Copy Markdown
Contributor

Here's what Claude says:

Critical Issues

1. preferred_gcc_version=v"11" conflicts with julia_compat="1.6"

The CONTRIBUTING.md explicitly warns: "avoid using GCC 11+ when building C++, as that would be incompatible with Julia v1.6." GCC 11 introduces a new libstdc++ ABI that Julia 1.6's bundled libstdc++ doesn't support. Either:

  • Lower preferred_gcc_version to v"9" or v"10" (preferred — maximizes compat), or
  • Bump julia_compat to "1.10" or later if GCC 11 features are truly required.

Since the upstream requires C++20 but the recipe downgrades to C++17 and patches out C++20 features (.contains().count(), .starts_with().find()), it's likely GCC 9 or 10 would suffice.

2. FileProduct("lib/libd4.a", :libd4_a) — static library as a product

BinaryBuilder/Yggdrasil strongly favors shared libraries. A static .a file:

  • Can't be dlopen()'d, so Julia's JLL machinery can't load it.
  • Creates linkage headaches for downstream consumers.
  • The upstream CMakeLists.txt already has a build mode for a shared library. The recipe should build libd4.so/libd4.dylib/libd4.dll and use LibraryProduct("libd4", :libd4) instead of FileProduct.

3. Windows DLL bundling is dangerous (lines 99-103)

find ${TOOLCHAIN_ROOT} -name "*.dll" -exec cp {} ${prefix}/bin/ \; 2>/dev/null || true

This blindly copies every DLL from the cross-compilation toolchain into the artifact. This is:

  • A licensing risk (bundling compiler runtime libraries without explicit attribution).
  • A conflict risk (these DLLs may clash with versions provided by Julia or other JLLs).
  • Unnecessary — BinaryBuilder's toolchain already handles libgcc_s, libstdc++, libwinpthread through the CompilerSupportLibraries_jll dependency. Just add Dependency("CompilerSupportLibraries_jll") instead.

4. BinaryBuilderBase import is unnecessary

Line 1: using BinaryBuilder, BinaryBuilderBase — standard recipes only need using BinaryBuilder. BinaryBuilderBase is an internal dependency that shouldn't be directly imported.

Major Concerns

5. Extremely fragile source patching

The build script has ~70 lines of sed and find -exec sed commands that:

  • Blindly prepend #include <cstdint> to every .cpp, .hpp, .cc, .h file in the tree.
  • Use fragile text patterns like s/handler);/handler);\n#endif/g that will break on any unrelated line matching handler);.
  • Comment out / delete upstream code (PartitionerPatoh.cpp, PartitionerPatoh.hpp) without proper guards.
  • Replace Glucose solver API calls with incompatible shims (solveLimitedsolve, dropping analyzeFinal, priorityVar, etc.) — this changes the solver's semantics and could produce wrong results.

A better approach would be to use Patch sources with proper .patch files, which are:

  • Reviewable (you can see the exact diff).
  • Maintainable (can be rebased when upstream updates).
  • Less likely to have unintended side effects.

6. Missing expand_cxxstring_abis()

Since d4 is a C++ project that links to Boost (which exposes std::string in its ABI), the platforms should likely be expanded with expand_cxxstring_abis() to handle the GCC cxx03/cxx11 ABI split. Without this, the resulting binaries may crash or produce undefined behavior when used with Julia packages built against a different C++ string ABI.

7. Manual compilation of the executable bypasses CMake

Lines 83-92 manually invoke ${CXX} to compile the d4 CLI tool instead of using the CMake build system. This:

  • Loses all the build system's dependency tracking.
  • Hardcodes library names and include paths.
  • Is fragile across platform differences.
  • The demo/compiler should be built as part of the CMake build, or the CMakeLists.txt should be patched to include it.

Minor Issues

8. No Zlib_jll dependency

The manual link line includes -lz, and the upstream CMakeLists references -lz, but Zlib_jll is not listed as a dependency. It may work by accident (BinaryBuilder base image has zlib), but it should be declared explicitly.

9. Commented-out code left in patching

sed -i 's/#include "PartitionerPatoh.hpp"/\/\/ #include "PartitionerPatoh.hpp"/' ...

Rather than commenting out includes, the recipe deletes PartitionerPatoh.cpp but leaves a dead #include comment. A proper patch would cleanly remove the PaToH partitioner support.

10. Upstream uses C++20, recipe forces C++17

The upstream CMakeLists.txt specifies CMAKE_CXX_STANDARD_REQUIRED 20. The recipe overrides this to C++17 and patches out C++20 features. This is a divergence that could cause subtle bugs — the sed replacements for .contains() and .starts_with() may not cover all C++20 usage. It would be worth filing an upstream issue to request C++17 compatibility, or at minimum documenting why C++20 can't be used.

11. Version mismatch

The recipe declares version = v"2.0.0" but the upstream repo doesn't appear to have tags or releases with this version number. The pinned commit 201e821 is just a point on main. The version should match an actual upstream release, or be clearly documented as a snapshot.

Summary

The recipe works (CI passes), but it has fundamental issues that should be addressed before merge:

Priority Issue
Must fix GCC 11 + julia_compat 1.6 incompatibility
Must fix Ship shared library, not static .a
Must fix Remove wildcard DLL copying; use CompilerSupportLibraries_jll
Must fix Remove BinaryBuilderBase import
Should fix Convert sed patches to .patch files
Should fix Add expand_cxxstring_abis()
Should fix Add Zlib_jll dependency
Should fix Build executable via CMake, not manual ${CXX}
Nice to have File upstream issue for C++17 compatibility
Nice to have Use a tagged upstream release

@SSJ0406
Copy link
Copy Markdown
Author

SSJ0406 commented Apr 15, 2026 via email

@SSJ0406
Copy link
Copy Markdown
Author

SSJ0406 commented Apr 17, 2026

@StefanKarpinski
Hello Stefan.
What do you think now that I've made the fixes?

@jd-foster
Copy link
Copy Markdown
Contributor

This recipe seems to use a personal fork; the original project repo is
https://github.com/crillab/d4v2
as far as I can see.

Comment thread D/d4/build_tarballs.jl Outdated
Comment on lines +15 to +49
# 1. Fixes for headers and C++ compatibility
find . -type f \( -name "*.cpp" -o -name "*.hpp" -o -name "*.cc" -o -name "*.h" \) -exec sed -i '1i #include <cstdint>\n#include <stdexcept>' {} +
find . -type f \( -name "*.cpp" -o -name "*.hpp" -o -name "*.cc" -o -name "*.h" \) -exec sed -i 's|#include <bits/stdint-uintn.h>||g' {} +
find . -type f \( -name "*.cpp" -o -name "*.hpp" -o -name "*.cc" -o -name "*.h" \) -exec sed -i 's|#include <bits/types/clock_t.h>||g' {} +

# Fix for fpu_control.h
sed -i 's/#include <fpu_control.h>/\n#if defined(__linux__) \&\& defined(__GLIBC__)\n#include <fpu_control.h>\n#else\n#define fpu_control_t unsigned int\n#endif\n/g' 3rdParty/glucose-3.0/utils/System.h
find 3rdParty/glucose-3.0 -name "System.cc" -exec sed -i 's/fpu_control_t/#if defined(__linux__) \&\& defined(__GLIBC__)\nfpu_control_t/g' {} +
sed -i 's/__setfpucw/\n#if defined(__linux__) \&\& defined(__GLIBC__)\n__setfpucw/g' 3rdParty/glucose-3.0/utils/System.cc

# Fix for PAGE_SIZE and u_int types
find . -type f \( -name "*.cpp" -o -name "*.hpp" -o -name "*.cc" -o -name "*.h" \) -exec sed -i 's/\bPAGE_SIZE\b/D4_PAGE_SIZE/g' {} +
find . -type f \( -name "*.cpp" -o -name "*.hpp" -o -name "*.cc" -o -name "*.h" \) -exec sed -i 's/u_int\([0-9]\+\)_t/uint\1_t/g' {} +
find . -type f \( -name "*.cpp" -o -name "*.hpp" -o -name "*.cc" -o -name "*.h" \) -exec sed -i 's/1UL << 32/1ULL << 32/g' {} +

# Windows signal fixes
if [[ "${target}" == *mingw* ]]; then
find . -type f \( -name "*.cpp" -o -name "*.hpp" -o -name "*.cc" -o -name "*.h" \) -exec sed -i 's/signal(SIGALRM, /#ifndef _WIN32\nsignal(SIGALRM, /g' {} +
find . -type f \( -name "*.cpp" -o -name "*.hpp" -o -name "*.cc" -o -name "*.h" \) -exec sed -i 's/handler);/handler);\n#endif/g' {} +
find . -type f \( -name "*.cpp" -o -name "*.hpp" -o -name "*.cc" -o -name "*.h" \) -exec sed -i 's/alarm(\([^)]*\));/#ifndef _WIN32\nalarm(\1);\n#endif/g' {} +
fi

# Compatibility and API fixes
sed -i 's/namespace d4 {/namespace d4 { \n class ProblemInputTypeManager; \n using InputTypeManager = ProblemInputTypeManager;/' src/problem/ProblemTypes.hpp
sed -i 's/\.contains(/.count(/g' src/problem/circuit/ParserCircuit.cpp
sed -i 's/line.starts_with("c w ")/0 == line.find("c w ")/g' src/problem/circuit/ParserCircuit.cpp
find 3rdParty -type f \( -name "*.cc" -o -name "*.cpp" -o -name "*.h" -o -name "*.hpp" \) -exec sed -i 's/%"PRIu64"/%" PRIu64 "/g' {} +
find 3rdParty -type f \( -name "*.cc" -o -name "*.cpp" -o -name "*.h" -o -name "*.hpp" \) -exec sed -i 's/%-12"PRIu64"/%-12" PRIu64 "/g' {} +

sed -i 's/s.addClauseInit(addCl);/s.addClause_(addCl);/' 3rdParty/bipe/src/solver/WrapperGlucose.cpp
sed -i 's/s.limitSelector = lastIndex;//' 3rdParty/bipe/src/solver/WrapperGlucose.cpp
sed -i 's/Glucose::lbool res = s.solveLimited(nbConflict);/bool success = s.solve(); Glucose::lbool res = success ? Glucose::lbool((uint8_t)0) : Glucose::lbool((uint8_t)1);/' 3rdParty/bipe/src/solver/WrapperGlucose.cpp
sed -i 's/s.analyzeFinal(confl, learnt_clause);//' 3rdParty/bipe/src/solver/WrapperGlucose.cpp
sed -i 's/s.priorityVar.clear();//' 3rdParty/bipe/src/solver/WrapperGlucose.cpp
sed -i 's/for (auto v : priority) s.priorityVar.push(v);//' 3rdParty/bipe/src/solver/WrapperGlucose.cpp
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

sed-way of patching files is brittle, and unmaintainable. At very least this should be a separate patch, but really, if there are bugs in the source code they should be fixed upstream with a PR, so we don't need to carry any patch at all.

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, agreed - sed patches are brittle.

This was a quick way to unblock cross-platform builds (Linux + MinGW) without maintaining forks of multiple dependencies. I’ll follow up by moving this to proper patch files and upstreaming fixes where possible 👍

Comment thread D/d4/build_tarballs.jl Outdated
Comment on lines +51 to +90
# 2. Generate clean CMakeLists.txt
cat <<'EOF' > CMakeLists.txt
cmake_minimum_required(VERSION 3.10)
project(D4 VERSION 2.0.0)
set(CMAKE_CXX_STANDARD 17)
set(CMAKE_CXX_STANDARD_REQUIRED ON)
set(CMAKE_POSITION_INDEPENDENT_CODE ON)

find_package(Boost REQUIRED COMPONENTS program_options)
find_package(TBB REQUIRED)
find_package(ZLIB REQUIRED)
find_path(GMP_INCLUDE_DIR gmp.h)
find_library(GMP_LIBRARY NAMES gmp)
find_library(GMPXX_LIBRARY NAMES gmpxx)

include_directories(${CMAKE_SOURCE_DIR})
include_directories(${CMAKE_SOURCE_DIR}/src)
include_directories(${CMAKE_SOURCE_DIR}/3rdParty/bipe)
include_directories(${CMAKE_SOURCE_DIR}/3rdParty/bipe/src)
include_directories(${CMAKE_SOURCE_DIR}/3rdParty/glucose-3.0)
include_directories(${CMAKE_SOURCE_DIR}/3rdParty/flowCutter/src)
include_directories(${GMP_INCLUDE_DIR} ${Boost_INCLUDE_DIRS} ${TBB_INCLUDE_DIRS})

file(GLOB_RECURSE SRC_FILES "src/*.cpp" "src/*.cc")
file(GLOB_RECURSE BIPE_FILES "3rdParty/bipe/src/*.cpp" "3rdParty/bipe/src/*.cc")
file(GLOB_RECURSE FLOW_FILES "3rdParty/flowCutter/src/*.cpp" "3rdParty/flowCutter/src/*.cc")
set(SOURCES ${SRC_FILES} ${BIPE_FILES} ${FLOW_FILES} "3rdParty/glucose-3.0/core/Solver.cc")
list(FILTER SOURCES EXCLUDE REGEX "PartitionerPatoh")

add_library(d4 SHARED ${SOURCES})
target_compile_definitions(d4 PRIVATE NOMAIN)
target_link_libraries(d4 ${GMPXX_LIBRARY} ${GMP_LIBRARY} ${Boost_LIBRARIES} TBB::tbb ZLIB::ZLIB)

add_executable(d4-bin demo/compiler/src/Main.cpp demo/compiler/src/CompilerDemo.cpp demo/compiler/src/ParseOption.cpp)
set_target_properties(d4-bin PROPERTIES OUTPUT_NAME d4)
target_link_libraries(d4-bin d4 ${Boost_LIBRARIES} TBB::tbb)

install(TARGETS d4 d4-bin RUNTIME DESTINATION bin LIBRARY DESTINATION lib ARCHIVE DESTINATION lib)
install(DIRECTORY src/ DESTINATION include/d4 FILES_MATCHING PATTERN "*.hpp" PATTERN "*.h")
EOF
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Likewise, this should at very least a separate file, but really, if the upstream project doesn't have a build system (is that even possible?) you should contribute it there, not here.

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks - that’s a fair point.
This was added to make the project buildable in our environment since upstream doesn’t provide a usable CMake setup. The goal was just to unblock packaging.
I agree it shouldn’t live inline like this. I can move it to a separate file, and longer term I’m happy to contribute it upstream so we don’t have to maintain it here 👍

Comment thread D/d4/build_tarballs.jl Outdated
Comment on lines +92 to +95
# Remove Patoh support
sed -i 's/#include "PartitionerPatoh.hpp"/\/\/ #include "PartitionerPatoh.hpp"/' src/partitioner/PartitionerManager.cpp
sed -i 's/return new PartitionerPatoh(infoHyperGraph, out);/throw(std::runtime_error("Partitioner PaToH not supported"));/' src/partitioner/PartitionerManager.cpp
rm -f src/partitioner/PartitionerPatoh.cpp src/partitioner/PartitionerPatoh.hpp
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same comment as above for the patches

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks - agreed, same concern applies here.

This was a quick workaround to disable PaToH (since it’s not available in our build environment), but I agree it shouldn’t be done via inline sed.

I’ll move this to a proper patch, and if possible look into a cleaner upstream-compatible way (e.g. optional feature flag)

Comment thread D/d4/build_tarballs.jl Outdated
]

dependencies = [
Dependency("GMP_jll"),
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
Dependency("GMP_jll"),
Dependency("GMP_jll"; compat="6.2.1"),

Comment thread D/d4/build_tarballs.jl Outdated

dependencies = [
Dependency("GMP_jll"),
Dependency("boost_jll"),
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
Dependency("boost_jll"),
Dependency("boost_jll"; compat="1.79.0"),

Comment thread D/d4/build_tarballs.jl Outdated
Dependency("boost_jll"),
Dependency("oneTBB_jll"),
Dependency("Zlib_jll"),
Dependency("CompilerSupportLibraries_jll"; platforms=filter(p -> Sys.iswindows(p), platforms)),
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this needed only on Windows?

For what is worth

Suggested change
Dependency("CompilerSupportLibraries_jll"; platforms=filter(p -> Sys.iswindows(p), platforms)),
Dependency("CompilerSupportLibraries_jll"; platforms=filter(Sys.iswindows, platforms)),

is shorter, but I'd first like to understand why this would be needed only on Windows.

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good question.

This is currently limited to Windows because the GCC runtime (libstdc++, libgcc, etc.) isn’t reliably available there, so CompilerSupportLibraries_jll is needed to provide it.

On Linux and macOS these are typically provided by the system toolchain, so it hasn’t been required so far.

That said, if you think it’s safer to make this unconditional for consistency, I can test and update

@SSJ0406
Copy link
Copy Markdown
Author

SSJ0406 commented Apr 24, 2026

This recipe seems to use a personal fork; the original project repo is https://github.com/crillab/d4v2 as far as I can see.

Good point.

This currently uses a fork because a number of fixes (build system, portability, dependency handling) were needed to make it work in this environment.

I agree these changes should ideally go upstream - I’ll look into contributing them back to the main repository so we can eventually depend on the original source instead

@SSJ0406 SSJ0406 marked this pull request as draft April 27, 2026 21:32
@SSJ0406 SSJ0406 marked this pull request as ready for review April 27, 2026 21:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants