Update to new d4 version with projected d-DNNF compilation (#43)

feat: enable projected compilation via new d4

bindings/kotlin/src/main/kotlin/de/softvare/ddnnife/java-utils.kt

@@ -19,6 +19,21 @@ fun ddnnfFromFile(path: String, features: Int?): Ddnnf {
     return Ddnnf.fromFile(path, features?.toUInt())
 }
 
+/**
+ * Loads a d-DNNF from file, using the projected d-DNNF compilation.
+ *
+ * @param path Where to load the d-DNNF from.
+ * @param features How many features the corresponding model has.
+ * Can be `null` in which case this will be determined by compilation or from building the d-DNNF.
+ * */
+fun ddnnfFromFileProjected(path: String, features: Int?): Ddnnf {
+    if (features != null) {
+        require(features >= 0) { "Features amount must be positive." }
+    }
+
+    return Ddnnf.fromFileProjected(path, features?.toUInt())
+}
+
 fun toUInt(i: Int): UInt {
     require(i >= 0) { "Integer must be positive." }
     return i.toUInt()

ddnnife/Cargo.toml

@@ -34,7 +34,7 @@ uniffi = { workspace = true, optional = true }
 workctl = "0.2"
 
 [target.'cfg(any(target_os = "linux", target_os = "macos", target_os = "windows"))'.dependencies]
-d4-oxide = { version = "0.4", optional = true }
+d4-oxide = { version = "0.5", optional = true }
 
 [dev-dependencies]
 assert_cmd = "2.0"

ddnnife/src/ddnnf.rs

@@ -7,7 +7,6 @@ pub mod node;
 pub mod stream;
 
 use self::{clause_cache::ClauseCache, node::Node};
-use crate::parser::build_ddnnf;
 use itertools::Either;
 use num::BigInt;
 use std::collections::{BTreeSet, HashMap, HashSet};
@@ -58,7 +57,18 @@ impl Ddnnf {
     /// Loads a d-DNNF from file.
     #[cfg_attr(feature = "uniffi", uniffi::constructor)]
     fn from_file(path: String, features: Option<u32>) -> Self {
-        build_ddnnf(&path.clone(), features)
+        crate::parser::build_ddnnf(&path.clone(), features)
+    }
+
+    /// Loads a d-DNNF from file, using the projected d-DNNF compilation.
+    ///
+    /// Panics when not including d4 as it is required for projected compilation.
+    #[cfg_attr(feature = "uniffi", uniffi::constructor)]
+    fn from_file_projected(path: String, features: Option<u32>) -> Self {
+        #[cfg(feature = "d4")]
+        return crate::parser::build_ddnnf_projected(&path.clone(), features);
+        #[cfg(not(feature = "d4"))]
+        panic!("d4 is required for projected compilation.");
     }
 
     /// Returns the current count of the root node in the d-DNNF.

ddnnife/src/parser.rs

@@ -115,6 +115,32 @@ pub fn build_ddnnf(path: &str, mut total_features: Option<u32>) -> Ddnnf {
     }
 }
 
+#[cfg(feature = "d4")]
+#[inline]
+pub fn build_ddnnf_projected(path: &str, total_features: Option<u32>) -> Ddnnf {
+    let temporary_ddnnf = NamedTempFile::new().expect("Failed to create temporary d-DNNF file.");
+
+    d4_oxide::compile_ddnnf_proj(
+        path.to_string(),
+        temporary_ddnnf
+            .path()
+            .to_str()
+            .expect("Failed to serialize temporary d-DNNF path.")
+            .to_string(),
+    );
+
+    let ddnnf = temporary_ddnnf
+        .reopen()
+        .expect("Failed to open temporary d-DNNF.");
+
+    let lines = BufReader::new(ddnnf)
+        .lines()
+        .map(|line| line.expect("Unable to read line"))
+        .collect::<Vec<String>>();
+
+    distribute_building(lines, total_features, None)
+}
+
 /// Chooses, depending on the first read line, which building implmentation to choose.
 /// Either the first line is a header and therefore the c2d format or total_features
 /// is supplied and its the d4 format.

ddnnife_bin/src/main.rs

@@ -38,6 +38,11 @@ struct Cli {
     #[arg(long, verbatim_doc_comment)]
     save_ddnnf: Option<String>,
 
+    /// Whether to use projected d-DNNF compilation for the input.
+    #[cfg(feature = "d4")]
+    #[arg(short, long, verbatim_doc_comment)]
+    projected: bool,
+
     /// Provides information about the type of nodes, their connection, and the different paths.
     #[arg(long, verbatim_doc_comment)]
     heuristics: bool,
@@ -173,6 +178,16 @@ fn main() {
 
     let mut ddnnf = if let Some(path) = &cli.input {
         // Read from file.
+        #[cfg(feature = "d4")]
+        {
+            if cli.projected {
+                dparser::build_ddnnf_projected(path, cli.total_features)
+            } else {
+                dparser::build_ddnnf(path, cli.total_features)
+            }
+        }
+
+        #[cfg(not(feature = "d4"))]
         dparser::build_ddnnf(path, cli.total_features)
     } else {
         // Read from stdin.

deny.toml

@@ -5,5 +5,5 @@ allow = [
     "LGPL-3.0",
     "MIT",
     "MPL-2.0",
-    "Unicode-DFS-2016",
+    "Unicode-3.0",
 ]

nix/ddnnife.nix

@@ -21,14 +21,25 @@ let
   buildSystem = buildPkgs.stdenv.system;
   hostSystem = hostPkgs.stdenv.system;
 
+  # The default MinGW GCC in Nix comes with mcfgthreads which seems to be unable
+  # to produce static Rust binaries with C dependencies.
+  cc-windows = hostPkgs.buildPackages.wrapCC (
+    hostPkgs.buildPackages.gcc-unwrapped.override ({
+      threadsCross = {
+        model = "win32";
+        package = null;
+      };
+    })
+  );
+
   rust = import ./rust.nix { inherit fenix; };
   static = hostPkgs.hostPlatform.isStatic;
   target = if static then rust.map.${hostSystem}.static else rust.map.${hostSystem}.default;
   craneLib = (crane.mkLib buildPkgs).overrideToolchain (rust.toolchain buildSystem target);
 
   metadata = craneLib.crateNameFromCargoToml { cargoToml = ../ddnnife/Cargo.toml; };
 
-  features-deps = lib.optionalString d4 "--features d4";
+  features-deps = lib.optionalString d4 "-vv --features d4";
   features =
     if (d4 || library) then
       lib.concatStrings (
@@ -74,14 +85,30 @@ let
       buildInputs =
         lib.optionals d4 [
           hostPkgs.boost.dev
-          hostPkgs.gmp.dev
           mt-kahypar.dev
         ]
+        ++ lib.optionals (d4 && hostPkgs.stdenv.hostPlatform.isLinux) [
+          hostPkgs.pkgsStatic.gmp.dev
+          hostPkgs.pkgsStatic.mpfr.dev
+        ]
+        ++ lib.optionals (d4 && hostPkgs.stdenv.hostPlatform.isDarwin) [
+          (hostPkgs.gmp.override {
+            withStatic = true;
+          })
+          hostPkgs.mpfr.dev
+        ]
+        ++ lib.optionals (d4 && hostPkgs.stdenv.hostPlatform.isWindows) [
+          (hostPkgs.gmp.override {
+            stdenv = hostPkgs.overrideCC hostPkgs.stdenv cc-windows;
+            withStatic = true;
+          })
+          hostPkgs.mpfr.dev
+        ]
         ++ lib.optionals hostPkgs.stdenv.isDarwin [ hostPkgs.libiconv ];
 
       nativeBuildInputs =
         lib.optionals d4 [
-          buildPkgs.m4
+          buildPkgs.cmake
           buildPkgs.pkg-config
         ]
         ++ lib.optionals pythonLib [ buildPkgs.maturin ];
@@ -93,44 +120,30 @@ let
 
       doCheck = test;
     }
-    // lib.optionalAttrs hostPkgs.stdenv.hostPlatform.isWindows (
-      let
-        # The default MinGW GCC in nix comes with mcfgthreads which seems to be unable
-        # to produce static Rust binaries with C dependencies.
-        cc = hostPkgs.buildPackages.wrapCC (
-          hostPkgs.buildPackages.gcc-unwrapped.override ({
-            threadsCross = {
-              model = "win32";
-              package = null;
-            };
-          })
-        );
-      in
-      {
-        TARGET_CC = "${cc}/bin/${cc.targetPrefix}cc";
-        TARGET_CXX = "${cc}/bin/${cc.targetPrefix}cc";
-
-        depsBuildBuild = [
-          cc
-          hostPkgs.windows.pthreads
-        ];
-
-        CARGO_TARGET_X86_64_PC_WINDOWS_GNU_RUNNER = (
-          buildPkgs.writeShellScript "wine-wrapped" ''
-            export WINEPREFIX=''$(mktemp -d)
-            export WINEDEBUG=-all
-            ${buildPkgs.wineWow64Packages.minimal}/bin/wine $@
-          ''
-        );
-      }
-    )
+    // lib.optionalAttrs hostPkgs.stdenv.hostPlatform.isWindows {
+      TARGET_CC = "${cc-windows}/bin/${cc-windows.targetPrefix}cc";
+      TARGET_CXX = "${cc-windows}/bin/${cc-windows.targetPrefix}cc";
+
+      depsBuildBuild = [
+        cc-windows
+        hostPkgs.windows.pthreads
+      ];
+
+      CARGO_TARGET_X86_64_PC_WINDOWS_GNU_RUNNER = (
+        buildPkgs.writeShellScript "wine-wrapped" ''
+          export WINEPREFIX=''$(mktemp -d)
+          export WINEDEBUG=-all
+          ${buildPkgs.wineWow64Packages.minimal}/bin/wine $@
+        ''
+      );
+    }
     // lib.optionalAttrs (d4 && hostPkgs.stdenv.system == "x86_64-darwin") {
       # FIXME: Tests with d4 are currently unable to run on x86_64-darwin.
       doCheck = false;
     }
     // lib.optionalAttrs (d4 && hostPkgs.stdenv.hostPlatform.isWindows) {
       # The Windows cross-build won't find the correct include and library directories by default.
-      CXXFLAGS = "-I ${hostPkgs.boost.dev}/include -I ${hostPkgs.gmp.dev}/include -I ${mt-kahypar.dev}/include";
+      CXXFLAGS = "-I ${hostPkgs.boost.dev}/include -I ${mt-kahypar.dev}/include";
       CARGO_BUILD_RUSTFLAGS = "-L ${mt-kahypar}/lib";
 
       # FIXME: Tests with d4 are currently unable to run on x86_64-windows.
@@ -153,7 +166,7 @@ craneLib.${craneAction} (
     inherit cargoArtifacts;
   }
   // lib.optionalAttrs hostPkgs.stdenv.isAarch64 {
-    # FIXME: Doc-tests currently fail on aarch64-{darwin, linuxy}.
+    # FIXME: Doc-tests currently fail on aarch64-{darwin, linux}.
     cargoTestExtraArgs = "--workspace --all-targets";
   }
   // lib.optionalAttrs pythonLib {