From 9aee3d56c51c70bebbf3c79a0380eb5de8136265 Mon Sep 17 00:00:00 2001 From: Jan Baudisch Date: Sat, 30 Nov 2024 00:13:51 +0100 Subject: [PATCH] feat: enable projected compilation via new d4 --- Cargo.lock | 130 +++++++++++++++++++++++++++++++++++++--- ddnnife/Cargo.toml | 2 +- ddnnife/src/ddnnf.rs | 10 +++- ddnnife/src/parser.rs | 26 ++++++++ ddnnife_bin/src/main.rs | 15 +++++ 5 files changed, 171 insertions(+), 12 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 5707ac3..2e4b304 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -277,6 +277,15 @@ version = "0.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1462739cb27611015575c0c11df5df7601141071f07518d56fcc1be504cbec97" +[[package]] +name = "cmake" +version = "0.1.52" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c682c223677e0e5b6b7f63a64b9351844c3f1b1678a68b7ee617e30fb082620e" +dependencies = [ + "cc", +] + [[package]] name = "codespan-reporting" version = "0.11.1" @@ -358,19 +367,100 @@ dependencies = [ "syn", ] +[[package]] +name = "d4-arjun-sys" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3d1884953f5291054b879008b38200a92f4db3ee6b297f30dd81753a6260bb0d" +dependencies = [ + "cmake", + "d4-cryptominisat-sys", + "gmp-mpfr-sys", +] + +[[package]] +name = "d4-cadiback-sys" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "485597d03ccb4519a4836caa7de00ae813bea6cc97e554868cd3fdab972442ac" +dependencies = [ + "cmake", + "d4-cadical-sys", +] + +[[package]] +name = "d4-cadical-sys" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c19a08dbae54dbc5da83f86f25c1945eb552113b02a3a8cc5664ac9384a6a4e6" +dependencies = [ + "cmake", +] + +[[package]] +name = "d4-cryptominisat-sys" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "804b915a8679c1daa54323d6eae2ee09b06720ec7bb3c9491147fc958457fbdf" +dependencies = [ + "cmake", + "d4-cadiback-sys", + "d4-cadical-sys", +] + +[[package]] +name = "d4-glucose-sys" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f39a3211bd062eff44dfe48ff8b17eb26b42b4a1d2248468e5913b14ce9dcac2" +dependencies = [ + "cmake", + "libz-sys", +] + +[[package]] +name = "d4-gpmc-sys" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68d537b5745821e523a4b6901a8fe6c6628fd4813a0862023770327827e64a31" +dependencies = [ + "cmake", + "d4-arjun-sys", + "d4-cryptominisat-sys", + "gmp-mpfr-sys", + "libz-sys", +] + [[package]] name = "d4-oxide" -version = "0.4.2" +version = "0.5.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b67903bc877566c257a6ad006d4bc1c562ecd3045bad3ade4868cf8da4e332cd" +checksum = "9b5616f57f734eac693b09fe97fc42ed0bc5add66c442017c397f9d0a37b1243" dependencies = [ "cxx", "cxx-build", + "d4-arjun-sys", + "d4-cadiback-sys", + "d4-cadical-sys", + "d4-cryptominisat-sys", + "d4-glucose-sys", + "d4-gpmc-sys", + "d4-sbva-sys", "glob", - "mt-kahypar-sys", + "gmp-mpfr-sys", + "libz-sys", "pkg-config", ] +[[package]] +name = "d4-sbva-sys" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e959892432cd6aa46517d5e2de06a0cbc70a3a765077e428f1763d2b0817bef6" +dependencies = [ + "cmake", +] + [[package]] name = "dashmap" version = "5.5.3" @@ -611,6 +701,16 @@ version = "0.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" +[[package]] +name = "gmp-mpfr-sys" +version = "1.6.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b0205cd82059bc63b63cf516d714352a30c44f2c74da9961dfda2617ae6b5918" +dependencies = [ + "libc", + "windows-sys 0.52.0", +] + [[package]] name = "goblin" version = "0.8.2" @@ -725,6 +825,18 @@ dependencies = [ "libc", ] +[[package]] +name = "libz-sys" +version = "1.1.20" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d2d16453e800a8cf6dd2fc3eb4bc99b786a9b90c663b8559a5b1a041bf89e472" +dependencies = [ + "cc", + "libc", + "pkg-config", + "vcpkg", +] + [[package]] name = "link-cplusplus" version = "1.0.9" @@ -793,12 +905,6 @@ 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" @@ -1506,6 +1612,12 @@ version = "0.2.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821" +[[package]] +name = "vcpkg" +version = "0.2.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "accd4ea62f7bb7a82fe23066fb0957d48ef677f6eeb8215f372f52e48bb32426" + [[package]] name = "version_check" version = "0.9.5" diff --git a/ddnnife/Cargo.toml b/ddnnife/Cargo.toml index f090111..bb85afa 100644 --- a/ddnnife/Cargo.toml +++ b/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" diff --git a/ddnnife/src/ddnnf.rs b/ddnnife/src/ddnnf.rs index 455bc68..242a35f 100644 --- a/ddnnife/src/ddnnf.rs +++ b/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) -> 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) -> Self { + crate::parser::build_ddnnf_projected(&path.clone(), features) } /// Returns the current count of the root node in the d-DNNF. diff --git a/ddnnife/src/parser.rs b/ddnnife/src/parser.rs index f797cdd..a7138fa 100644 --- a/ddnnife/src/parser.rs +++ b/ddnnife/src/parser.rs @@ -115,6 +115,32 @@ pub fn build_ddnnf(path: &str, mut total_features: Option) -> Ddnnf { } } +#[cfg(feature = "d4")] +#[inline] +pub fn build_ddnnf_projected(path: &str, total_features: Option) -> 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::>(); + + 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. diff --git a/ddnnife_bin/src/main.rs b/ddnnife_bin/src/main.rs index 6208003..1f85059 100644 --- a/ddnnife_bin/src/main.rs +++ b/ddnnife_bin/src/main.rs @@ -38,6 +38,11 @@ struct Cli { #[arg(long, verbatim_doc_comment)] save_ddnnf: Option, + /// 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.