feat: initial commit

.github/workflows/CI.yaml

@@ -0,0 +1,71 @@
+name: CI
+
+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
+
+jobs:
+  Format:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+      - name: Format
+        run: cargo fmt --check
+
+  Lint:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          submodules: 'recursive'
+      - name: Install dependencies
+        run: sudo apt-get install ninja-build libtbb-dev libhwloc-dev libboost-program-options-dev
+      - name: Setup sccache
+        uses: mozilla-actions/sccache-action@v0.0.3
+      - name: Setup environment
+        run: |
+          echo MTKAHYPAR_DIR=$(mktemp -d) >> $GITHUB_ENV
+      - name: Build Mt-KaHyPar
+        run: |
+          cd $(mktemp -d)
+          git clone --recursive https://github.com/kahypar/mt-kahypar.git .
+          git checkout $(git describe --tags $(git rev-list --tags --max-count=1))
+          cmake -B build -D CMAKE_INSTALL_PREFIX=$MTKAHYPAR_DIR
+          cmake --build build --target mtkahypar
+          cmake --install build
+      - name: Lint
+        run: cargo clippy -- --deny warnings
+
+  Build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          submodules: 'recursive'
+      - name: Install dependencies
+        run: sudo apt-get install ninja-build libtbb-dev libhwloc-dev libboost-program-options-dev
+      - name: Setup sccache
+        uses: mozilla-actions/sccache-action@v0.0.3
+      - name: Setup environment
+        run: |
+          echo MTKAHYPAR_DIR=$(mktemp -d) >> $GITHUB_ENV
+      - name: Build Mt-KaHyPar
+        run: |
+          cd $(mktemp -d)
+          git clone --recursive https://github.com/kahypar/mt-kahypar.git .
+          git checkout $(git describe --tags $(git rev-list --tags --max-count=1))
+          cmake -B build -D CMAKE_INSTALL_PREFIX=$MTKAHYPAR_DIR
+          cmake --build build --target mtkahypar
+          cmake --install build
+      - name: Build
+        run: cargo build

.github/workflows/Publish.yaml

@@ -0,0 +1,20 @@
+name: Publish
+
+on:
+  push:
+    tags:
+      - '*'
+
+env:
+  CARGO_TERM_COLOR: always
+
+jobs:
+  Publish:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+      - name: Publish
+        env:
+          CARGO_REGISTRY_TOKEN: ${{ secrets.CARGO_REGISTRY_TOKEN }}
+        run: cargo publish

.gitignore

@@ -0,0 +1,2 @@
+/target
+/Cargo.lock

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "d4"]
+	path = d4
+	url = https://github.com/SoftVarE-Group/d4v2.git

Cargo.toml

@@ -0,0 +1,24 @@
+[package]
+name = "d4-oxide"
+version = "0.1.0"
+description = "A Rust wrapper around d4."
+edition = "2021"
+build = "build.rs"
+license = "LGPL-3.0-or-later"
+authors = ["Jan Baudisch <jan.baudisch@uni-ulm.de>"]
+readme = "README.md"
+homepage = "https://github.com/SoftVarE-Group/d4-oxide"
+repository = "https://github.com/SoftVarE-Group/d4-oxide.git"
+
+[dependencies]
+cxx = "1.0"
+mt-kahypar-sys = "0.1"
+gmp-mpfr-sys = { version = "1.6", default-features = false }
+
+[build-dependencies]
+cxx-build = { version = "1.0", features = ["parallel"] }
+glob = "0.3"
+pkg-config = "0.3"
+
+[dev-dependencies]
+clap = { version = "4.4", features = ["derive"] }

LICENSE

@@ -0,0 +1,165 @@
+                   GNU LESSER GENERAL PUBLIC LICENSE
+                       Version 3, 29 June 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc. <https://fsf.org/>
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+
+  This version of the GNU Lesser General Public License incorporates
+the terms and conditions of version 3 of the GNU General Public
+License, supplemented by the additional permissions listed below.
+
+  0. Additional Definitions.
+
+  As used herein, "this License" refers to version 3 of the GNU Lesser
+General Public License, and the "GNU GPL" refers to version 3 of the GNU
+General Public License.
+
+  "The Library" refers to a covered work governed by this License,
+other than an Application or a Combined Work as defined below.
+
+  An "Application" is any work that makes use of an interface provided
+by the Library, but which is not otherwise based on the Library.
+Defining a subclass of a class defined by the Library is deemed a mode
+of using an interface provided by the Library.
+
+  A "Combined Work" is a work produced by combining or linking an
+Application with the Library.  The particular version of the Library
+with which the Combined Work was made is also called the "Linked
+Version".
+
+  The "Minimal Corresponding Source" for a Combined Work means the
+Corresponding Source for the Combined Work, excluding any source code
+for portions of the Combined Work that, considered in isolation, are
+based on the Application, and not on the Linked Version.
+
+  The "Corresponding Application Code" for a Combined Work means the
+object code and/or source code for the Application, including any data
+and utility programs needed for reproducing the Combined Work from the
+Application, but excluding the System Libraries of the Combined Work.
+
+  1. Exception to Section 3 of the GNU GPL.
+
+  You may convey a covered work under sections 3 and 4 of this License
+without being bound by section 3 of the GNU GPL.
+
+  2. Conveying Modified Versions.
+
+  If you modify a copy of the Library, and, in your modifications, a
+facility refers to a function or data to be supplied by an Application
+that uses the facility (other than as an argument passed when the
+facility is invoked), then you may convey a copy of the modified
+version:
+
+   a) under this License, provided that you make a good faith effort to
+   ensure that, in the event an Application does not supply the
+   function or data, the facility still operates, and performs
+   whatever part of its purpose remains meaningful, or
+
+   b) under the GNU GPL, with none of the additional permissions of
+   this License applicable to that copy.
+
+  3. Object Code Incorporating Material from Library Header Files.
+
+  The object code form of an Application may incorporate material from
+a header file that is part of the Library.  You may convey such object
+code under terms of your choice, provided that, if the incorporated
+material is not limited to numerical parameters, data structure
+layouts and accessors, or small macros, inline functions and templates
+(ten or fewer lines in length), you do both of the following:
+
+   a) Give prominent notice with each copy of the object code that the
+   Library is used in it and that the Library and its use are
+   covered by this License.
+
+   b) Accompany the object code with a copy of the GNU GPL and this license
+   document.
+
+  4. Combined Works.
+
+  You may convey a Combined Work under terms of your choice that,
+taken together, effectively do not restrict modification of the
+portions of the Library contained in the Combined Work and reverse
+engineering for debugging such modifications, if you also do each of
+the following:
+
+   a) Give prominent notice with each copy of the Combined Work that
+   the Library is used in it and that the Library and its use are
+   covered by this License.
+
+   b) Accompany the Combined Work with a copy of the GNU GPL and this license
+   document.
+
+   c) For a Combined Work that displays copyright notices during
+   execution, include the copyright notice for the Library among
+   these notices, as well as a reference directing the user to the
+   copies of the GNU GPL and this license document.
+
+   d) Do one of the following:
+
+       0) Convey the Minimal Corresponding Source under the terms of this
+       License, and the Corresponding Application Code in a form
+       suitable for, and under terms that permit, the user to
+       recombine or relink the Application with a modified version of
+       the Linked Version to produce a modified Combined Work, in the
+       manner specified by section 6 of the GNU GPL for conveying
+       Corresponding Source.
+
+       1) Use a suitable shared library mechanism for linking with the
+       Library.  A suitable mechanism is one that (a) uses at run time
+       a copy of the Library already present on the user's computer
+       system, and (b) will operate properly with a modified version
+       of the Library that is interface-compatible with the Linked
+       Version.
+
+   e) Provide Installation Information, but only if you would otherwise
+   be required to provide such information under section 6 of the
+   GNU GPL, and only to the extent that such information is
+   necessary to install and execute a modified version of the
+   Combined Work produced by recombining or relinking the
+   Application with a modified version of the Linked Version. (If
+   you use option 4d0, the Installation Information must accompany
+   the Minimal Corresponding Source and Corresponding Application
+   Code. If you use option 4d1, you must provide the Installation
+   Information in the manner specified by section 6 of the GNU GPL
+   for conveying Corresponding Source.)
+
+  5. Combined Libraries.
+
+  You may place library facilities that are a work based on the
+Library side by side in a single library together with other library
+facilities that are not Applications and are not covered by this
+License, and convey such a combined library under terms of your
+choice, if you do both of the following:
+
+   a) Accompany the combined library with a copy of the same work based
+   on the Library, uncombined with any other library facilities,
+   conveyed under the terms of this License.
+
+   b) Give prominent notice with the combined library that part of it
+   is a work based on the Library, and explaining where to find the
+   accompanying uncombined form of the same work.
+
+  6. Revised Versions of the GNU Lesser General Public License.
+
+  The Free Software Foundation may publish revised and/or new versions
+of the GNU Lesser General Public License from time to time. Such new
+versions will be similar in spirit to the present version, but may
+differ in detail to address new problems or concerns.
+
+  Each version is given a distinguishing version number. If the
+Library as you received it specifies that a certain numbered version
+of the GNU Lesser General Public License "or any later version"
+applies to it, you have the option of following the terms and
+conditions either of that published version or of any later version
+published by the Free Software Foundation. If the Library as you
+received it does not specify a version number of the GNU Lesser
+General Public License, you may choose any version of the GNU Lesser
+General Public License ever published by the Free Software Foundation.
+
+  If the Library as you received it specifies that a proxy can decide
+whether future versions of the GNU Lesser General Public License shall
+apply, that proxy's public statement of acceptance of any version is
+permanent authorization for you to choose that version for the
+Library.

README.md

@@ -0,0 +1,19 @@
+# d4-oxide
+
+> A Rust wrapper around [d4][d4].
+
+## Usage
+
+Add it as a dependency to your Cargo.toml:
+
+```toml
+[dependencies]
+d4-oxide = "0.1"
+```
+
+## Requirements
+
+- [Mt-KaHyPar][mtkahypar]
+
+[d4]: https://github.com/crillab/d4v2
+[mtkahypar]: https://github.com/kahypar/mt-kahypar

build.rs

@@ -0,0 +1,54 @@
+use glob::glob;
+use std::env;
+use std::path::PathBuf;
+
+fn main() {
+    // Find d4 sources to build.
+    let d4_sources: Vec<PathBuf> = glob("d4/src/**/*.cpp")
+        .expect("Failed to create glob pattern for d4 sources.")
+        .map(|result| result.expect("Failed to find d4 source file."))
+        .filter(|path| !path.ends_with("Main.cpp"))
+        .filter(|path| !path.ends_with("DdnnfCompilerRunnable.cpp"))
+        .filter(|path| !path.ends_with("WrapperGlucose.cpp"))
+        .collect();
+
+    // Setup include paths for compilation.
+    let mut includes = vec![
+        "include".to_string(),
+        "d4/include".to_string(),
+        "d4/src".to_string(),
+        "d4".to_string(),
+    ];
+
+    // Optionally add Mt-KaHyPar include path.
+    if let Ok(mtkahypar_include) = env::var("DEP_MTKAHYPAR_INCLUDE_DIR") {
+        includes.push(mtkahypar_include.clone());
+    }
+
+    // Build d4.
+    cxx_build::bridge("src/lib.rs")
+        .includes(includes)
+        .file("src/Adapter.cc")
+        .files(d4_sources)
+        .define("D4_SOLVER", "minisat")
+        .define("D4_PREPORC_SOLVER", "minisat")
+        .compile("d4");
+
+    // FIXME: Currently, `gmp-mpfr-sys` does not build the C++ interface. Once it does, GMPXX could be used from it.
+    // println!("cargo:rustc-link-search={}", env::var("DEP_GMP_OUT_DIR").expect("GMP library directory not passed."));
+
+    // Find and link the C++ interface of GMP.
+    let gmpxx_library = pkg_config::Config::new()
+        .statik(true)
+        .probe("gmpxx")
+        .expect("Failed to find GMP C++ library.");
+
+    for path in gmpxx_library.link_paths {
+        println!("cargo:rustc-link-search={}", path.display());
+    }
+
+    println!("cargo:rustc-link-lib=static=gmpxx");
+
+    // Link Mt-KaHyPar.
+    println!("cargo:rustc-link-lib=dylib=mtkahypar");
+}

examples/ddnnf-compiler.rs

@@ -0,0 +1,19 @@
+use clap::Parser;
+use d4_oxide::compile_ddnnf;
+
+#[derive(Parser, Debug)]
+#[command(author, version, about, long_about = None)]
+struct Args {
+    /// Input file to read CNF from.
+    #[arg(short, long)]
+    input: String,
+
+    /// Output file to write d-DNNF to.
+    #[arg(short, long)]
+    output: String,
+}
+
+fn main() {
+    let args = Args::parse();
+    compile_ddnnf(args.input, args.output);
+}

include/Adapter.h

@@ -0,0 +1,3 @@
+#include "rust/cxx.h"
+
+void compile_ddnnf(rust::String input, rust::String output);

src/Adapter.cc

@@ -0,0 +1,7 @@
+#include "Adapter.h"
+
+#include "DdnnfCompiler.hpp"
+
+void compile_ddnnf(rust::String input, rust::String output) {
+  d4::compile_ddnnf(std::string(input), std::string(output));
+}