From d09d88bfb01fa5a371803fdacdc45bfdaf6d65ef Mon Sep 17 00:00:00 2001 From: Jan Baudisch Date: Thu, 25 Jan 2024 13:45:39 +0100 Subject: [PATCH] feat(parser): replace d4 binary with d4-oxide --- .github/workflows/CI.yml | 222 ++++++++++++++++----------- Cargo.lock | 300 +++++++++++++++++++++---------------- Cargo.toml | 38 ++--- README.md | 45 ++++-- build.rs | 72 --------- doc/built/linux-d4.md | 27 ++++ doc/built/linux.md | 15 ++ doc/built/macos-d4.md | 38 +++++ doc/built/macos.md | 1 + doc/built/windows-d4.md | 1 + doc/built/windows.md | 17 +++ package-msys.bash | 83 ++++++++++ src/parser.rs | 45 +++--- src/parser/d4v2_wrapper.rs | 81 ---------- 14 files changed, 569 insertions(+), 416 deletions(-) delete mode 100644 build.rs create mode 100644 doc/built/linux-d4.md create mode 100644 doc/built/linux.md create mode 100644 doc/built/macos-d4.md create mode 120000 doc/built/macos.md create mode 120000 doc/built/windows-d4.md create mode 100644 doc/built/windows.md create mode 100755 package-msys.bash delete mode 100644 src/parser/d4v2_wrapper.rs diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 3ee6066..b6444b8 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -1,110 +1,154 @@ name: CI -on: [workflow_dispatch, push] +on: + - push env: CARGO_TERM_COLOR: always + CMAKE_GENERATOR: Ninja + CMAKE_C_COMPILER_LAUNCHER: sccache + CMAKE_CXX_COMPILER_LAUNCHER: sccache + RUSTC_WRAPPER: sccache + SCCACHE_GHA_ENABLED: true + # FIXME: cc-rs on mac currently won't set the C++ standard correctly (https://github.com/dtolnay/cxx/issues/1217). + CXXFLAGS: -std=c++17 jobs: Format: runs-on: ubuntu-latest steps: - name: Checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Format run: cargo fmt --check - Build-Linux: - runs-on: ubuntu-latest - strategy: - fail-fast: false - matrix: - target: [x86_64-unknown-linux-gnu] - steps: - - name: Checkout - uses: actions/checkout@v3 - - name: Cache - uses: Swatinem/rust-cache@v2 - - name: d4v2 build dependencies - run: sudo apt-get install libboost-all-dev ninja-build - - name: Build target - run: cargo build --release --target ${{ matrix.target }} - - name: Archieve Binary - uses: actions/upload-artifact@v3 - with: - name: ddnnife_${{ matrix.target }} - path: target/${{ matrix.target }}/release/ddnnife - - Build-wo-d4v2-Macos: - runs-on: macos-latest + Build: strategy: fail-fast: false matrix: - target: [x86_64-apple-darwin] + target: + - os: linux + runner: ubuntu-latest + triple: x86_64-unknown-linux-gnu + shell: bash + coverage: true + - os: macos + runner: macos-latest + triple: x86_64-apple-darwin + shell: bash + - os: windows + runner: windows-latest + triple: x86_64-pc-windows-gnu + shell: msys2 + msystem: ucrt64 + toolchain: + - stable + d4: + - include + - exclude + runs-on: ${{ matrix.target.runner }} + defaults: + run: + shell: ${{ matrix.target.shell }} {0} + env: + CARGO_BUILD_TARGET: ${{ matrix.target.triple }} steps: - name: Checkout - uses: actions/checkout@v3 - - name: Cache - uses: Swatinem/rust-cache@v2 - - name: Build target - run: EXCLUDE_D4V2=TRUE cargo build --release --target ${{ matrix.target }} - - name: Archieve Binary - uses: actions/upload-artifact@v3 + uses: actions/checkout@v4 + - name: Setup MSYS2 (Windows) + if: ${{ matrix.target.os == 'windows' }} + uses: msys2/setup-msys2@v2 with: - name: ddnnife_${{ matrix.target }} - path: target/${{ matrix.target }}/release/ddnnife - - - #Build-wo-d4v2-Windows: - # runs-on: ubuntu-latest - # strategy: - # fail-fast: false - # steps: - # - uses: actions/checkout@v3 - # - uses: Swatinem/rust-cache@v2 - # - name: Set env variable - # run: export EXCLUDE_D4V2=TRUE - # - name: Install dependencies - # run: | - # rustup target add x86_64-pc-windows-gnu - # - name: Build - # uses: actions-rs/cargo@v1 - # with: - # use-cross: true - # command: build - # args: --target x86_64-pc-windows-gnu --release - # - name: Archieve Binary - # uses: actions/upload-artifact@v3 - # with: - # name: ddnnife - # path: target/release/ddnnife.exe - - Doc-tests: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v3 - - uses: Swatinem/rust-cache@v2 - - name: d4v2 build dependencies - run: sudo apt-get install libboost-all-dev; sudo apt-get install ninja-build - - name: Doc-tests - run: cargo test --doc - - Integration-tests: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v3 - - uses: Swatinem/rust-cache@v2 - - name: d4v2 build dependencies - run: sudo apt-get install libboost-all-dev; sudo apt-get install ninja-build - - name: Integration-tests - run: cargo test --release --tests - - Coverage: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v3 - - uses: Swatinem/rust-cache@v2 - - name: d4v2 build dependencies - run: sudo apt-get install libboost-all-dev; sudo apt-get install ninja-build + path-type: inherit + msystem: ${{ matrix.target.msystem }} + pacboy: git m4 cmake:p ninja:p + - name: Install dependencies (Linux) + if: ${{ matrix.target.os == 'linux' }} + run: sudo apt-get install ninja-build libtbb-dev libhwloc-dev libboost-program-options-dev + - name: Install dependencies (macOS) + if: ${{ matrix.target.os == 'macos' }} + run: brew install ninja boost hwloc tbb + - name: Install dependencies (Windows) + if: ${{ matrix.target.os == 'windows' }} + run: | + pacboy -S --noconfirm toolchain:p tbb:p hwloc:p boost:p + mv /${{ matrix.target.msystem }}/lib/libtbb12.dll.a /${{ matrix.target.msystem }}/lib/libtbb.dll.a + - name: Setup sccache + uses: mozilla-actions/sccache-action@v0.0.3 + - name: Setup environment + run: | + export BUILD_ROOT=$(mktemp -d) + echo BUILD_ROOT=$BUILD_ROOT >> $GITHUB_ENV + echo MTKAHYPAR_DIR=$BUILD_ROOT >> $GITHUB_ENV + echo BUILD_ROOT_EXPORT=$(python3 -c "import os; print(os.environ['BUILD_ROOT'])") >> $GITHUB_ENV + echo LD_LIBRARY_PATH="$LD_LIBRARY_PATH:$BUILD_ROOT/lib:$BUILD_ROOT/lib64" >> $GITHUB_ENV + echo PATH="$PATH:$BUILD_ROOT/bin" >> $GITHUB_ENV + - name: Setup Rust + run: | + rustup update ${{ matrix.toolchain }}-${{ matrix.target.triple }} + rustup default ${{ matrix.toolchain }}-${{ matrix.target.triple }} + - name: Build Mt-KaHyPar + if: ${{ matrix.d4 == 'include' }} + run: | + cd $(mktemp -d) + git clone --recursive https://github.com/kahypar/mt-kahypar.git . + cmake -B build -D CMAKE_INSTALL_PREFIX=$BUILD_ROOT -D MT_KAHYPAR_DISABLE_BOOST=true + cmake --build build --target mtkahypar + cmake --install build + mkdir -p $BUILD_ROOT/licenses/mt-kahypar + cp LICENSE $BUILD_ROOT/licenses/mt-kahypar/ +# TODO: currently, macOS is only supported on master, move below clone to check out latest version when released. +# git checkout $(git describe --tags $(git rev-list --tags --max-count=1)) + - name: Build (including d4) + if: ${{ matrix.d4 == 'include' }} + run: cargo build + - name: Build (excluding d4) + if: ${{ matrix.d4 == 'exclude' }} + run: cargo build --no-default-features + - name: Test + # FIXME: Some tests are currently not platform independent and fail on macos and windows and without d4 + if: ${{ matrix.d4 == 'include' && matrix.target.os != 'macos' && matrix.target.os != 'windows' }} + run: cargo test + - name: Install coverage tool + if: ${{ matrix.target.coverage }} + uses: taiki-e/install-action@cargo-llvm-cov - name: Coverage - run: cargo +stable install cargo-llvm-cov; cargo llvm-cov + if: ${{ matrix.target.coverage && matrix.d4 == 'include' }} + run: cargo llvm-cov + - name: Package + run: | + mkdir -p $BUILD_ROOT/bin + cp target/${{ matrix.target.triple }}/debug/{ddnnife,dhone} $BUILD_ROOT/bin/ + rm -rf $BUILD_ROOT/include + rm -rf $BUILD_ROOT/share + mkdir -p $BUILD_ROOT/licenses/d-ddnnf-reasoner + cp LICENSE $BUILD_ROOT/licenses/d-ddnnf-reasoner/ + - name: Package documentation (including d4) + if: ${{ matrix.d4 == 'include' }} + run: | + cp doc/built/${{ matrix.target.os }}-d4.md $BUILD_ROOT/README.md + - name: Package documentation (excluding d4) + if: ${{ matrix.d4 == 'exclude' }} + run: | + cp doc/built/${{ matrix.target.os }}.md $BUILD_ROOT/README.md + - name: Package dependencies (Windows) + if: ${{ matrix.target.os == 'windows' }} + run: | + ./package-msys.bash $BUILD_ROOT $BUILD_ROOT/bin/* + rm -f $BUILD_ROOT/bin/b2 + rm -f $BUILD_ROOT/bin/bjam + rm -f $BUILD_ROOT/bin/hwloc* + rm -f $BUILD_ROOT/bin/lstopo* + rm -rf $BUILD_ROOT/lib + - name: Upload (including d4) + if: ${{ matrix.d4 == 'include' }} + uses: actions/upload-artifact@v4 + with: + name: ddnnife-d4-${{ matrix.target.triple }} + path: ${{ env.BUILD_ROOT_EXPORT }} + - name: Upload (excluding d4) + if: ${{ matrix.d4 == 'exclude' }} + uses: actions/upload-artifact@v4 + with: + name: ddnnife-${{ matrix.target.triple }} + path: ${{ env.BUILD_ROOT_EXPORT }} diff --git a/Cargo.lock b/Cargo.lock index e1179ea..ba64bec 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -13,16 +13,15 @@ dependencies = [ [[package]] name = "anstream" -version = "0.3.2" +version = "0.6.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0ca84f3628370c59db74ee214b3263d58f9aadd9b4fe7e711fd87dc452b7f163" +checksum = "6e2e1ebcb11de5c03c67de28a7df593d32191b44939c482e97702baaaa6ab6a5" dependencies = [ "anstyle", "anstyle-parse", "anstyle-query", "anstyle-wincon", "colorchoice", - "is-terminal", "utf8parse", ] @@ -52,12 +51,12 @@ dependencies = [ [[package]] name = "anstyle-wincon" -version = "1.0.2" +version = "3.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c677ab05e09154296dd37acecd46420c17b9713e8366facafa8fc0885167cf4c" +checksum = "1cd54b81ec8d6180e24654d0b371ad22fc3dd083b6ff8ba325b72e00c87660a7" dependencies = [ "anstyle", - "windows-sys 0.48.0", + "windows-sys 0.52.0", ] [[package]] @@ -95,9 +94,9 @@ checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" [[package]] name = "bitflags" -version = "2.4.0" +version = "2.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4682ae6287fcf752ecaabbfcc7b6f9b72aa33933dc23a554d853aea8eea8635" +checksum = "ed570934406eb16438a4e976b1b4500774099c13b8cb96eec99f620f05090ddf" [[package]] name = "bitvec" @@ -128,6 +127,7 @@ version = "1.0.83" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f1174fb0b6ec23863f8b971027804a42614e347eafb0a95bf0b12cdae21fc4d0" dependencies = [ + "jobserver", "libc", ] @@ -139,33 +139,31 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.3.23" +version = "4.4.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "03aef18ddf7d879c15ce20f04826ef8418101c7e528014c3eeea13321047dca3" +checksum = "1e578d6ec4194633722ccf9544794b71b1385c3c027efe0c55db226fc880865c" dependencies = [ "clap_builder", "clap_derive", - "once_cell", ] [[package]] name = "clap_builder" -version = "4.3.23" +version = "4.4.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f8ce6fffb678c9b80a70b6b6de0aad31df727623a70fd9a842c30cd573e2fa98" +checksum = "4df4df40ec50c46000231c914968278b1eb05098cf8f1b3a518a95030e71d1c7" dependencies = [ "anstream", "anstyle", "clap_lex", - "once_cell", "strsim", ] [[package]] name = "clap_derive" -version = "4.3.12" +version = "4.4.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "54a9bb5758fc5dfe728d1019941681eccaf0cf8a4189b692a0ee2f2ecf90a050" +checksum = "cf9804afaaf59a91e75b022a30fb7229a7901f60c755489cc61c9b423b836442" dependencies = [ "heck", "proc-macro2", @@ -175,9 +173,19 @@ dependencies = [ [[package]] name = "clap_lex" -version = "0.5.0" +version = "0.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2da6da31387c7e4ef160ffab6d5e7f00c42626fe39aea70a7b0f1773f7dd6c1b" +checksum = "702fc72eb24e5a1e48ce58027a675bc24edd52096d5397d4aea7c6dd9eca0bd1" + +[[package]] +name = "codespan-reporting" +version = "0.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3538270d33cc669650c4b093848450d380def10c331d38c768e34cac80576e6e" +dependencies = [ + "termcolor", + "unicode-width", +] [[package]] name = "colorchoice" @@ -206,6 +214,64 @@ dependencies = [ "memchr", ] +[[package]] +name = "cxx" +version = "1.0.112" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "58ab30434ea0ff6aa640a08dda5284026a366d47565496fd40b6cbfbdd7e31a2" +dependencies = [ + "cc", + "cxxbridge-flags", + "cxxbridge-macro", + "link-cplusplus", +] + +[[package]] +name = "cxx-build" +version = "1.0.112" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b649d7dfae8268450d53d109388b337b9352c7cba1fc10db4a1bc23c3dc189fb" +dependencies = [ + "cc", + "codespan-reporting", + "once_cell", + "proc-macro2", + "quote", + "scratch", + "syn", +] + +[[package]] +name = "cxxbridge-flags" +version = "1.0.112" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "42281b20eba5218c539295c667c18e2f50211bb11902419194c6ed1ae808e547" + +[[package]] +name = "cxxbridge-macro" +version = "1.0.112" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b45506e3c66512b0a65d291a6b452128b7b1dd9841e20d1e151addbd2c00ea50" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "d4-oxide" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6d8ca2e9b41176531112806df46bb9c18c65bea424320fa3dfb4c901307dfb72" +dependencies = [ + "cxx", + "cxx-build", + "glob", + "gmp-mpfr-sys", + "mt-kahypar-sys", + "pkg-config", +] + [[package]] name = "dashmap" version = "5.5.0" @@ -227,9 +293,10 @@ dependencies = [ "bitvec", "clap", "csv", + "d4-oxide", "file_diff", "gmp-mpfr-sys", - "itertools 0.11.0", + "itertools", "mimalloc", "nom", "once_cell", @@ -242,7 +309,6 @@ dependencies = [ "serial_test", "streaming-iterator", "tempfile", - "winapi", "workctl", ] @@ -401,14 +467,20 @@ dependencies = [ "wasi", ] +[[package]] +name = "glob" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" + [[package]] name = "gmp-mpfr-sys" -version = "1.6.0" +version = "1.6.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "87010f41b33d28887e0379114e7b065ad39f34e2589a8e8e0fe02c8559c68466" +checksum = "362a6cc3cbe9f41aebe49c03b91aee8fa8fc69d32fb90533f6ed965a882e08e3" dependencies = [ "libc", - "windows-sys 0.42.0", + "windows-sys 0.52.0", ] [[package]] @@ -423,12 +495,6 @@ version = "0.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8" -[[package]] -name = "hermit-abi" -version = "0.3.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "443144c8cdadd93ebf52ddb4056d257f5b52c04d3c804e657d19eb73fc33668b" - [[package]] name = "indexmap" version = "2.0.0" @@ -439,31 +505,11 @@ dependencies = [ "hashbrown", ] -[[package]] -name = "is-terminal" -version = "0.4.9" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cb0889898416213fab133e1d33a0e5858a48177452750691bde3666d0fdbaf8b" -dependencies = [ - "hermit-abi", - "rustix", - "windows-sys 0.48.0", -] - [[package]] name = "itertools" -version = "0.10.5" +version = "0.12.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b0fd2260e829bddf4cb6ea802289de2f86d6a7a690192fbe91b3f46e0f2c8473" -dependencies = [ - "either", -] - -[[package]] -name = "itertools" -version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57" +checksum = "25db6b064527c5d482d0423354fcd07a89a2dfe07b67892e62411946db7f07b0" dependencies = [ "either", ] @@ -474,6 +520,15 @@ version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38" +[[package]] +name = "jobserver" +version = "0.1.27" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8c37f63953c4c63420ed5fd3d6d398c719489b9f872b9fa683262f8edd363c7d" +dependencies = [ + "libc", +] + [[package]] name = "lazy_static" version = "1.4.0" @@ -482,9 +537,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.151" +version = "0.2.152" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "302d7ab3130588088d277783b1e2d2e10c9e9e4a16dd9050e6ec93fb3e7048f4" +checksum = "13e3bf6590cbc649f4d1a3eefc9d5d6eb746f5200ffb04e5e142700b8faa56e7" [[package]] name = "libm" @@ -494,19 +549,28 @@ checksum = "f7012b1bbb0719e1097c47611d3898568c546d597c2e74d66f6087edd5233ff4" [[package]] name = "libmimalloc-sys" -version = "0.1.33" +version = "0.1.35" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f4ac0e912c8ef1b735e92369695618dc5b1819f5a7bf3f167301a3ba1cea515e" +checksum = "3979b5c37ece694f1f5e51e7ecc871fdb0f517ed04ee45f88d15d6d553cb9664" dependencies = [ "cc", "libc", ] +[[package]] +name = "link-cplusplus" +version = "1.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9d240c6f7e1ba3a28b0249f774e6a9dd0175054b52dfbb61b16eb8505c3785c9" +dependencies = [ + "cc", +] + [[package]] name = "linux-raw-sys" -version = "0.4.12" +version = "0.4.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c4cd1a83af159aa67994778be9070f0ae1bd732942279cabb14f86f986a21456" +checksum = "01cda141df6706de531b6c46c3a33ecca755538219bd484262fa09410c13539c" [[package]] name = "lock_api" @@ -532,9 +596,9 @@ checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d" [[package]] name = "mimalloc" -version = "0.1.37" +version = "0.1.39" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4e2894987a3459f3ffb755608bd82188f8ed00d0ae077f1edea29c068d639d98" +checksum = "fa01922b5ea280a911e323e4d2fd24b7fe5cc4042e0d2cda3c40775cdc4bdc9c" dependencies = [ "libmimalloc-sys", ] @@ -545,6 +609,12 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" +[[package]] +name = "mt-kahypar-sys" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1f998f740bfb7280489d8f16c0b8258463b07d919afc8eadad26ea5906d54da4" + [[package]] name = "nom" version = "7.1.3" @@ -573,9 +643,9 @@ dependencies = [ [[package]] name = "once_cell" -version = "1.18.0" +version = "1.19.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d" +checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92" [[package]] name = "parking_lot" @@ -622,6 +692,12 @@ version = "0.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8b870d8c151b6f2fb93e84a13146138f05d02ed11c7e7c54f8826aaaf7c9f184" +[[package]] +name = "pkg-config" +version = "0.3.29" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2900ede94e305130c13ddd391e0ab7cbaeb783945ae07a279c268cb05109c6cb" + [[package]] name = "ppv-lite86" version = "0.2.17" @@ -630,14 +706,13 @@ checksum = "5b40af805b3121feab8a3c29f04d8ad262fa8e0561883e7653e024ae4479e6de" [[package]] name = "predicates" -version = "3.0.3" +version = "3.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09963355b9f467184c04017ced4a2ba2d75cbcb4e7462690d388233253d4b1a9" +checksum = "68b87bfd4605926cdfefc1c3b5f8fe560e3feca9d5552cf68c466d3d8236c7e8" dependencies = [ "anstyle", "difflib", "float-cmp", - "itertools 0.10.5", "normalize-line-endings", "predicates-core", "regex", @@ -781,9 +856,9 @@ checksum = "e5ea92a5b6195c6ef2a0295ea818b312502c6fc94dde986c5553242e18fd4ce2" [[package]] name = "rug" -version = "1.20.1" +version = "1.23.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "240ad7cbc5fc7cea4592203f8f6100835e8ad083196491b8a9c84ce84711ff68" +checksum = "eaf1855d294a2bd8f38c5a3a6dc456144aeaf15827beeb880300296923100d49" dependencies = [ "az", "gmp-mpfr-sys", @@ -792,11 +867,11 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.28" +version = "0.38.30" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72e572a5e8ca657d7366229cdde4bd14c4eb5499a9573d4d366fe1b599daa316" +checksum = "322394588aaf33c24007e8bb3238ee3e4c5c09c084ab32bc73890b99ff326bca" dependencies = [ - "bitflags 2.4.0", + "bitflags 2.4.2", "errno", "libc", "linux-raw-sys", @@ -815,6 +890,12 @@ version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" +[[package]] +name = "scratch" +version = "1.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a3cf7c11c38cb994f3d40e8a8cde3bbd1f72a435e4c49e85d6553d8312306152" + [[package]] name = "serde" version = "1.0.185" @@ -903,6 +984,15 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "termcolor" +version = "1.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "06794f8f6c5c898b3275aebefa6b8a1cb24cd2c6c79397ab15774837a0bc5755" +dependencies = [ + "winapi-util", +] + [[package]] name = "termtree" version = "0.4.1" @@ -915,6 +1005,12 @@ version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "301abaae475aa91687eb82514b328ab47a211a533026cb25fc3e519b86adfc3c" +[[package]] +name = "unicode-width" +version = "0.1.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e51733f11c9c4f72aa0c160008246859e340b00807569a0da0e7a1079b27ba85" + [[package]] name = "utf8parse" version = "0.2.1" @@ -953,25 +1049,19 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" [[package]] -name = "winapi-x86_64-pc-windows-gnu" -version = "0.4.0" +name = "winapi-util" +version = "0.1.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" +checksum = "f29e6f9198ba0d26b4c9f07dbe6f9ed633e1f3d5b8b414090084349e46a52596" +dependencies = [ + "winapi", +] [[package]] -name = "windows-sys" -version = "0.42.0" +name = "winapi-x86_64-pc-windows-gnu" +version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5a3e1820f08b8513f676f7ab6c1f99ff312fb97b553d30ff4dd86f9f15728aa7" -dependencies = [ - "windows_aarch64_gnullvm 0.42.2", - "windows_aarch64_msvc 0.42.2", - "windows_i686_gnu 0.42.2", - "windows_i686_msvc 0.42.2", - "windows_x86_64_gnu 0.42.2", - "windows_x86_64_gnullvm 0.42.2", - "windows_x86_64_msvc 0.42.2", -] +checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" [[package]] name = "windows-sys" @@ -1021,12 +1111,6 @@ dependencies = [ "windows_x86_64_msvc 0.52.0", ] -[[package]] -name = "windows_aarch64_gnullvm" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "597a5118570b68bc08d8d59125332c54f1ba9d9adeedeef5b99b02ba2b0698f8" - [[package]] name = "windows_aarch64_gnullvm" version = "0.48.5" @@ -1039,12 +1123,6 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cb7764e35d4db8a7921e09562a0304bf2f93e0a51bfccee0bd0bb0b666b015ea" -[[package]] -name = "windows_aarch64_msvc" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e08e8864a60f06ef0d0ff4ba04124db8b0fb3be5776a5cd47641e942e58c4d43" - [[package]] name = "windows_aarch64_msvc" version = "0.48.5" @@ -1057,12 +1135,6 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bbaa0368d4f1d2aaefc55b6fcfee13f41544ddf36801e793edbbfd7d7df075ef" -[[package]] -name = "windows_i686_gnu" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c61d927d8da41da96a81f029489353e68739737d3beca43145c8afec9a31a84f" - [[package]] name = "windows_i686_gnu" version = "0.48.5" @@ -1075,12 +1147,6 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a28637cb1fa3560a16915793afb20081aba2c92ee8af57b4d5f28e4b3e7df313" -[[package]] -name = "windows_i686_msvc" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "44d840b6ec649f480a41c8d80f9c65108b92d89345dd94027bfe06ac444d1060" - [[package]] name = "windows_i686_msvc" version = "0.48.5" @@ -1093,12 +1159,6 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ffe5e8e31046ce6230cc7215707b816e339ff4d4d67c65dffa206fd0f7aa7b9a" -[[package]] -name = "windows_x86_64_gnu" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8de912b8b8feb55c064867cf047dda097f92d51efad5b491dfb98f6bbb70cb36" - [[package]] name = "windows_x86_64_gnu" version = "0.48.5" @@ -1111,12 +1171,6 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3d6fa32db2bc4a2f5abeacf2b69f7992cd09dca97498da74a151a3132c26befd" -[[package]] -name = "windows_x86_64_gnullvm" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "26d41b46a36d453748aedef1486d5c7a85db22e56aff34643984ea85514e94a3" - [[package]] name = "windows_x86_64_gnullvm" version = "0.48.5" @@ -1129,12 +1183,6 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1a657e1e9d3f514745a572a6846d3c7aa7dbe1658c056ed9c3344c4109a6949e" -[[package]] -name = "windows_x86_64_msvc" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9aec5da331524158c6d1a4ac0ab1541149c0b9505fde06423b02f5ef0106b9f0" - [[package]] name = "windows_x86_64_msvc" version = "0.48.5" diff --git a/Cargo.toml b/Cargo.toml index 392616f..b8b18cf 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,10 +1,9 @@ [package] name = "ddnnife" version = "0.6.0" -authors = ["Heiko Raab; heiko.raab@uni-ulm-de", "Chico Sundermann; chico.sundermann@uni-ulm.de"] +authors = ["Heiko Raab ", "Chico Sundermann ", "Jan Baudisch "] edition = "2021" -license = "GNU LGPL-2.1" -build = "build.rs" +license = "LGPL-3.0-or-later" [lib] name = "ddnnf_lib" @@ -18,43 +17,46 @@ path = "src/bin/ddnnife.rs" name = "dhone" path = "src/bin/dhone.rs" -# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html - [profile.release] -lto = "fat" # enables link-time optimization -codegen-units = 1 # forbid parallel compiling -panic = "abort" +lto = true +codegen-units = 1 # for performance graphs: debug = true +[features] +default = ["d4"] +d4 = ["dep:d4-oxide"] + [dependencies] -clap = { version = "4.3.22", features = ["cargo", "derive", "color"] } -mimalloc = { version = "0.1.37", default-features = false } +clap = { version = "4.4.11", features = ["cargo", "derive", "color"] } +mimalloc = { version = "0.1.39", default-features = false } nom = "7.1.3" csv = "1.2.2" workctl = "0.2.0" # parallelisation file_diff = "1.0.0" -petgraph = "0.6.3" +petgraph = "0.6.4" rand_pcg = "0.3.1" rand = "0.8.5" rand_distr = "0.4.3" -itertools = "0.11.0" -once_cell = "1.18.0" +itertools = "0.12.0" +once_cell = "1.19.0" bitvec = "1.0.1" streaming-iterator = "0.1.9" -winapi = { version = "0.3.9", features = ["winnt"] } tempfile = "3.9.0" +[target.'cfg(any(target_os = "linux", target_os = "macos", target_os = "windows"))'.dependencies] +d4-oxide = { version = "0.2.1", optional = true } + [dependencies.gmp-mpfr-sys] -version = "1.6.0" +version = "1.6.1" default-features = false -features = ["force-cross"] +features = ["c-no-tests"] [dependencies.rug] -version = "1.20.1" +version = "1.22.0" default-features = false features = ["integer", "float", "rational"] [dev-dependencies] assert_cmd = "2.0.12" -predicates = "3.0.3" +predicates = "3.0.4" serial_test = "2.0.0" diff --git a/README.md b/README.md index 8c9a2b3..dc135f8 100644 --- a/README.md +++ b/README.md @@ -26,21 +26,40 @@ In the following, we describe the process to compile ddnnife. As an alternative, ## Requirements for Building -First, if not done already, you have to [install rust](https://www.rust-lang.org/tools/install). The recommended way is the following, using curl and rustup: -```properties -curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh +- [Rust][rust] +- [Boost][boost] +- [GMP][gmp] (with C++ bindings) +- [Mt-KaHyPar][mtkahypar] +- GCC or Clang + +### Linux + +- diffutils +- m4 +- make + +### macOS + +The commandline developer tools have to be present: + +``` +xcode-select --install ``` -After that, we recommend entering "1" to proceed with the installation (without customizations). -Additionally, we use rug for the computations. Make sure to install everything mentioned on rugs [crates.io page](https://crates.io/crates/rug) to use rug and our software. There it says: +### Windows -*Rug [...] depends on the [GMP](https://gmplib.org/), [MPFR](https://www.mpfr.org/) and [MPC](https://www.multiprecision.org/mpc/) libraries through the low-level FFI bindings in the [gmp-mpfr-sys crate](https://crates.io/crates/gmp-mpfr-sys), which needs some setup to build; the [gmp-mpfr-sys documentation](https://docs.rs/gmp-mpfr-sys/1.4.7/gmp_mpfr_sys/index.html) has some details on usage under [different os][...].* +On Windows, [MSYS2][msys2] is required to build the project. +The UCRT64 or CLANG64 environment is used depending on the compiler (GCC or Clang). +All dependencies must be installed for the environment. +This can be achieved by using `pacboy`: -To build on GNU/Linux, make sure you have ```diffutils, gcc, m4``` and ```make``` installed on your system. For example on Ubuntu: -```properties -sudo apt-get update && apt-get install diffutils gcc m4 make +``` +pacman -S pactoys +pacboy -S toolchain:p boost:p ``` +Mt-KaHyPar has to be present in the MSYS2 environment as well. + ## Build the Binaries Make sure that the current working directory is the one including the Cargo.toml file. @@ -316,4 +335,10 @@ docker run --platform linux/amd64 -i --rm -v [HOST FOLDER ABSOLUTE]:/data ddnnif After that arguments for ```ddnnife``` can be passed. It is important that to access the files mounted via the volume, you need to add the ```/data/``` prefix to all the input and output files. An example to compute the cardinality of features for ```auto1``` can look like the following. ```properties docker run --platform linux/amd64 -i --rm -v ~/Documents/d-dnnf-reasoner/example_input:/data ddnnife /data/auto1.cnf count-features /data/result -``` \ No newline at end of file +``` + +[rust]: https://rust-lang.org +[boost]: https://boost.org +[gmp]: https://gmplib.org +[mtkahypar]: https://github.com/kahypar/mt-kahypar +[msys2]: https://msys2.org diff --git a/build.rs b/build.rs deleted file mode 100644 index ecdd3a9..0000000 --- a/build.rs +++ /dev/null @@ -1,72 +0,0 @@ -use std::{ - env, - fs::File, - io::Write, - path::Path, - process::{exit, Command}, -}; - -fn main() { - // Include or exclude d4v2 depending on the enviroment variable - println!("cargo:rerun-if-changed=EXCLUDE_D4V2"); - - #[cfg(windows)] - let mut out = File::create("src\\bin\\d4v2.bin").unwrap(); - #[cfg(unix)] - let mut out = File::create("src/bin/d4v2.bin").unwrap(); - - let exclude_d4 = std::env::var("EXCLUDE_D4V2"); - - // not set -> we expect that the user wants to use d4 - if let Ok(val) = exclude_d4 { - if val == "TRUE" { - println!("Not including d4v2"); - // create an empty binary file so the constant referencing it has a value - out.write_all(b"").unwrap(); - exit(0); - } - } - - // Force rerunning this build script if src/parser/d4v2.bin gets deleted or changed in any way - // to make sure it works properly - #[cfg(windows)] - println!("cargo:rerun-if-changed=src\\bin\\d4v2.bin"); - #[cfg(unix)] - println!("cargo:rerun-if-changed=src/bin/d4v2.bin"); - - if !Path::new("d4v2/build/d4").exists() { - println!("cloning and building d4..."); - - // Set up a local copy of the repository. We choose the forked version of d4v2 due to a missing library in the origin repo. - Command::new("rm").args(["-rf", "d4v2"]).output().unwrap(); - Command::new("mkdir") - .arg("d4v2") - .output() - .expect("wasn't able to create the 'd4v2' folder"); - Command::new("git") - .args([ - "clone", - "https://github.com/SoftVarE-Group/d4v2.git", - "d4v2/.", - ]) - .output() - .expect("could not clone the d4v2 repository"); - - // build the d4v2 binary - let current_dir = &env::current_dir().unwrap(); - env::set_current_dir(current_dir.canonicalize().unwrap().join("d4v2").as_path()).unwrap(); - match Command::new("./build.sh").output() { - Ok(_) => (), - Err(err) => eprintln!( - "An error occured while trying to build the d4v2 binary: {}", - err - ), - } - env::set_current_dir(current_dir).unwrap(); - } - - // Include the binary data of d4v2 in the source files. - // This allows us to staticlly bind it to the ddnnife binary. - out.write_all(&std::fs::read("d4v2/build/d4").unwrap()) - .unwrap(); -} diff --git a/doc/built/linux-d4.md b/doc/built/linux-d4.md new file mode 100644 index 0000000..76a0e29 --- /dev/null +++ b/doc/built/linux-d4.md @@ -0,0 +1,27 @@ +# d-ddnnf-reasoner + +This is a built version of ddnnife and dhone. +The project is licensed under the LGPL-3.0 and the source can be found at https://github.com/SoftVarE-Group/d-dnnf-reasoner. + +## Dependencies + +The Mt-KaHyPar dependency is bundled with this build, other dependencies have to be installed: + +- TBB (https://github.com/oneapi-src/oneTBB) +- hwloc (https://open-mpi.org/projects/hwloc) + +## Usage + +The binaries `ddnnife` and `dhone` are inside `bin`. +The Mt-KaHyPar library has to be available for `ddnnife` to run. +This can either be accomplished by moving the `lib` directories contents to the global library path (such as `/usr/lib`) +or by setting the `LD_LIBRARY_PATH` environment variable to include the `lib` directory. +Then, the linker will be able to find `libmtkahypar.so` required by `ddnnife`. + +To show the help message, use: + +``` +ddnnife --help +``` + +For full usage instructions, see the README at https://github.com/SoftVarE-Group/d-dnnf-reasoner diff --git a/doc/built/linux.md b/doc/built/linux.md new file mode 100644 index 0000000..8af1367 --- /dev/null +++ b/doc/built/linux.md @@ -0,0 +1,15 @@ +# d-ddnnf-reasoner + +This is a built version of ddnnife and dhone. +The project is licensed under the LGPL-3.0 and the source can be found at https://github.com/SoftVarE-Group/d-dnnf-reasoner. + +## Usage + +The binaries `ddnife` and `dhone` are inside `bin`. +To show the help message, use: + +``` +ddnife --help +``` + +For full usage instructions, see the README at https://github.com/SoftVarE-Group/d-dnnf-reasoner diff --git a/doc/built/macos-d4.md b/doc/built/macos-d4.md new file mode 100644 index 0000000..5b73d04 --- /dev/null +++ b/doc/built/macos-d4.md @@ -0,0 +1,38 @@ +# d-ddnnf-reasoner + +This is a built version of ddnnife and dhone. +The project is licensed under the LGPL-3.0 and the source can be found at https://github.com/SoftVarE-Group/d-dnnf-reasoner. + +## Dependencies + +The Mt-KaHyPar dependency is bundled with this build, other dependencies have to be installed: + +- TBB (https://github.com/oneapi-src/oneTBB) +- hwloc (https://open-mpi.org/projects/hwloc) + +## Gatekeeper + +The execution of downloaded binaries might be blocked by Gatekeeper. +To resolve this, the attribute `com.apple.quarantine` has to be removed from `bin/ddnife`, `bin/dhone` and `lib/libmtkahypar.dylib`: + +``` +xattr -d com.apple.quarantine bin/ddnife +xattr -d com.apple.quarantine bin/dhone +xattr -d com.apple.quarantine lib/libmtkahypar.dylib +``` + +## Usage + +The binaries `ddnnife` and `dhone` are inside `bin`. +The Mt-KaHyPar library has to be available for `ddnnife` to run. +This can either be accomplished by moving the `lib` directories contents to the global library path (such as `/usr/lib`) +or by setting the `DYLD_LIBRARY_PATH` environment variable to include the `lib` directory. +Then, the linker will be able to find `libmtkahypar.dylib` required by `ddnife`. + +To show the help message, use: + +``` +ddnife --help +``` + +For full usage instructions, see the README at https://github.com/SoftVarE-Group/d-dnnf-reasoner diff --git a/doc/built/macos.md b/doc/built/macos.md new file mode 120000 index 0000000..dba520c --- /dev/null +++ b/doc/built/macos.md @@ -0,0 +1 @@ +linux.md \ No newline at end of file diff --git a/doc/built/windows-d4.md b/doc/built/windows-d4.md new file mode 120000 index 0000000..002730a --- /dev/null +++ b/doc/built/windows-d4.md @@ -0,0 +1 @@ +windows.md \ No newline at end of file diff --git a/doc/built/windows.md b/doc/built/windows.md new file mode 100644 index 0000000..c464779 --- /dev/null +++ b/doc/built/windows.md @@ -0,0 +1,17 @@ +# d-ddnnf-reasoner + +This is a built version of ddnnife and dhone. +The project is licensed under the LGPL-3.0 and the source can be found at https://github.com/SoftVarE-Group/d-dnnf-reasoner. + +All dependencies are in `bin`. + +## Usage + +The binaries `ddnife.exe` and `dhone.exe` are inside `bin`. +To show the help message, use: + +``` +ddnife.exe --help +``` + +For full usage instructions, see the README at https://github.com/SoftVarE-Group/d-dnnf-reasoner diff --git a/package-msys.bash b/package-msys.bash new file mode 100755 index 0000000..b5d6042 --- /dev/null +++ b/package-msys.bash @@ -0,0 +1,83 @@ +#!/bin/bash + +# Check if running from within MSYS2. +if [ -z "$MSYSTEM" ]; +then + >&2 echo "This is intended to be run from within an MSYS2 environment." + exit 1 +fi + +# Check arguments for correct length. +if [ "$#" -lt 2 ]; then + >&2 echo "Usage: $0 []" + exit 1 +fi + +# Setup variables from environment. +system=$(echo "$MSYSTEM" | tr '[:upper:]' '[:lower:]') +destination=$1 +files=${@:2} + +# Check for MSYS2 environment to be present. +if [ ! -d /"$MSYSTEM" ]; +then + >&2 echo "Path of MSYS2 $MSYSTEM environment not found." + exit 1 +fi + +# Check for destination to be present. +if [ ! -d "$destination" ]; +then + >&2 echo "Destination does not exist." + exit 1 +fi + +# Check for all (to be processed) files to be present. +for file in $files +do + if [ ! -f "$file" ]; + then + >&2 echo "No such file: $file" + exit 1 + fi +done + +# Generate list of needed packages. +packages=() + +for file in $files +do + dlls=$(ldd "$file" | grep /"$system" | sed 's/.dll.*/.dll/') + + for dll in $dlls + do + package=$(pacman -Qqo "$dll") + echo "[Library]: $dll ($package)" + packages+=("$package") + done +done + +# Remove duplicates. +packages=$(echo "${packages[@]}" | tr ' ' '\n' | sort -u) + +echo "[Required]: $(echo "$packages" | tr '\n' ' ')" + +# Extract packages. +cwd=$PWD +tmp=$(mktemp -d) +cd "$tmp" || exit 1 + +for package in $packages +do + path=$(pacman -Sp "$package" | grep -oP 'file://\K\S+') + echo "[Extract]: $package ($path)" + tar -xf "$path" +done + +# Copy files to destination. +cp -r "$tmp/$system/bin" "$destination" +cp -r "$tmp/$system/share/licenses" "$destination" + +# Cleanup. +cd "$cwd" || exit 1 +rm -r "$tmp" diff --git a/src/parser.rs b/src/parser.rs index 0fb6806..c577ef5 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -7,9 +7,6 @@ use d4_lexer::{lex_line_d4, D4Token}; pub mod from_cnf; use from_cnf::{check_for_cnf_header, CNFToken}; -pub mod d4v2_wrapper; -use crate::parser::d4v2_wrapper::compile_cnf; - pub mod persisting; pub mod util; @@ -60,26 +57,34 @@ pub fn build_ddnnf(mut path: &str, mut total_features: Option) -> Ddnnf { let mut clauses = BTreeSet::new(); if let Some(extension) = Path::new(path).extension().and_then(OsStr::to_str) { if extension == "dimacs" || extension == "cnf" { - let file = open_file_savely(path); - let lines = BufReader::new(file).lines(); - for line in lines { - let line = line.expect("Unable to read line"); - match check_for_cnf_header(line.as_str()).unwrap().1 { - CNFToken::Header { - total_features: total_features_header, - total_clauses: _, - } => { - let ddnnf_file = ".intermediate.nnf"; - compile_cnf(path, ddnnf_file); - path = ddnnf_file; - total_features = Some(total_features_header as u32); - } - CNFToken::Clause { features } => { - clauses.insert(features); + #[cfg(feature = "d4")] + { + let file = open_file_savely(path); + let lines = BufReader::new(file).lines(); + for line in lines { + let line = line.expect("Unable to read line"); + match check_for_cnf_header(line.as_str()).unwrap().1 { + CNFToken::Header { + total_features: total_features_header, + total_clauses: _, + } => { + let ddnnf_file = ".intermediate.nnf"; + d4_oxide::compile_ddnnf(path.to_string(), ddnnf_file.to_string()); + path = ddnnf_file; + total_features = Some(total_features_header as u32); + } + CNFToken::Clause { features } => { + clauses.insert(features); + } + CNFToken::Comment => (), } - CNFToken::Comment => (), } } + + #[cfg(not(feature = "d4"))] + { + panic!("CNF to d-DNNF compilation is only possible when including d4."); + } } } diff --git a/src/parser/d4v2_wrapper.rs b/src/parser/d4v2_wrapper.rs deleted file mode 100644 index bcd72d8..0000000 --- a/src/parser/d4v2_wrapper.rs +++ /dev/null @@ -1,81 +0,0 @@ -use std::{ - fs, - process::{self, Command}, -}; - -#[cfg(windows)] -const D4V2: &[u8] = include_bytes!("..\\bin\\d4v2.bin"); // relative from source file -#[cfg(unix)] -const D4V2: &[u8] = include_bytes!("../bin/d4v2.bin"); -const EXECUTABLE_PATH: &str = ".d4v2"; // relative from the root of the project - -/// Using the d4v2 CNF to dDNNF compiler from cril, -/// we take a CNF from path_in and write the dDNNF to path_out -pub fn compile_cnf(path_in: &str, path_out: &str) { - // If the byte array is empty, we did not include d4v2. Consequently, we can't compile and have to exit. - if D4V2.is_empty() { - // Bold, Red, Foreground Color (see https://gist.github.com/fnky/458719343aabd01cfb17a3a4f7296797) - eprintln!("\x1b[1;38;5;196m\nERROR: d4v2 is not part of that binary! \ - Hence, CNF files can not be handled by this binary file. \ - Compile again with 'EXCLUDE_D4V2=FALSE cargo build --release' to use d4v2.\nAborting..."); - process::exit(1); - } - - // persist the binary data to a callable file - std::fs::write(EXECUTABLE_PATH, D4V2).expect("failed to write file"); - set_permissions(); - - // execute the command to compile a dDNNF from a CNF file - Command::new(String::from("./") + EXECUTABLE_PATH) - .args([ - "-i", - path_in, - "-m", - "ddnnf-compiler", - "--dump-ddnnf", - path_out, - ]) - .output() - .unwrap(); - - // Remove it again, after the call. This operation is very cheap! - fs::remove_file(EXECUTABLE_PATH).unwrap(); -} - -// When writing the stored bytes of the binary to a file, -// we have to adjust the permissions of that file to execute commands on that binary. -fn set_permissions() { - // Set executable permissions on Unix systems - #[cfg(unix)] - { - use std::os::unix::fs::PermissionsExt; - let mut perms = std::fs::metadata(EXECUTABLE_PATH) - .expect("failed to get metadata") - .permissions(); - perms.set_mode(0o755); - std::fs::set_permissions(EXECUTABLE_PATH, perms).expect("failed to set permissions"); - } - - // Set executable permissions on Windows systems - #[cfg(windows)] - { - use std::fs::OpenOptions; - use std::os::windows::fs::OpenOptionsExt; - use winapi::um::winnt::FILE_ATTRIBUTE_NORMAL; - - let mut options = OpenOptions::new(); - options - .write(true) - .create(true) - .truncate(true) - .custom_flags(FILE_ATTRIBUTE_NORMAL); - let file = options.open(EXECUTABLE_PATH).expect("failed to open file"); - let mut permissions = file - .metadata() - .expect("failed to get metadata") - .permissions(); - permissions.set_readonly(false); - file.set_permissions(permissions) - .expect("failed to set permissions"); - } -}