feat: enable projected compilation via new d4

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,14 @@ 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.
+    #[cfg(feature = "d4")]
+    #[cfg_attr(feature = "uniffi", uniffi::constructor)]
+    fn from_file_projected(path: String, features: Option<u32>) -> Self {
+        crate::parser::build_ddnnf_projected(&path.clone(), features)
     }
 
     /// 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.