diff --git a/d4-oxide/examples/ddnnf-compiler.rs b/d4-oxide/examples/ddnnf-compiler.rs index abb537c..b4e5179 100644 --- a/d4-oxide/examples/ddnnf-compiler.rs +++ b/d4-oxide/examples/ddnnf-compiler.rs @@ -1,5 +1,5 @@ use clap::Parser; -use d4_oxide::compile_ddnnf; +use d4_oxide::{compile_ddnnf, compile_ddnnf_proj}; #[derive(Parser, Debug)] #[command(author, version, about, long_about = None)] @@ -11,9 +11,18 @@ struct Args { /// Output file to write d-DNNF to. #[arg(short, long)] output: String, + + /// Whether to do projected compilation. + #[arg(short, long)] + projected: bool, } fn main() { let args = Args::parse(); - compile_ddnnf(args.input, args.output); + + if args.projected { + compile_ddnnf_proj(args.input, args.output); + } else { + compile_ddnnf(args.input, args.output); + } } diff --git a/d4-oxide/include/Adapter.h b/d4-oxide/include/Adapter.h index 9850ce7..cca964c 100644 --- a/d4-oxide/include/Adapter.h +++ b/d4-oxide/include/Adapter.h @@ -1,3 +1,4 @@ #include "rust/cxx.h" void compile_ddnnf(rust::String input, rust::String output); +void compile_ddnnf_proj(rust::String input, rust::String output); diff --git a/d4-oxide/src/Adapter.cc b/d4-oxide/src/Adapter.cc index 04bc4cd..e86289c 100644 --- a/d4-oxide/src/Adapter.cc +++ b/d4-oxide/src/Adapter.cc @@ -6,15 +6,25 @@ #include "src/config/ConfigConverter.hpp" #include "src/methods/MethodManager.hpp" -void compile_ddnnf(rust::String input, rust::String output) { +void run(d4::Config config) { std::ostringstream out; + d4::MethodManager *methodManager = d4::MethodManager::makeMethodManager(config, out); + methodManager->run(config); + delete methodManager; +} +void compile_ddnnf(rust::String input, rust::String output) { d4::Config config = d4::Config::default_values(); config.method = "ddnnf-compiler"; config.input = std::string(input); config.dump_ddnnf = std::string(output); + run(config); +} - d4::MethodManager *methodManager = d4::MethodManager::makeMethodManager(config, out); - methodManager->run(config); - delete methodManager; +void compile_ddnnf_proj(rust::String input, rust::String output) { + d4::Config config = d4::Config::default_values(); + config.method = "proj-ddnnf-compiler"; + config.input = std::string(input); + config.dump_ddnnf = std::string(output); + run(config); } diff --git a/d4-oxide/src/lib.rs b/d4-oxide/src/lib.rs index 6247f3c..073d276 100644 --- a/d4-oxide/src/lib.rs +++ b/d4-oxide/src/lib.rs @@ -4,6 +4,7 @@ mod ffi { include!("Adapter.h"); fn compile_ddnnf(input: String, output: String); + fn compile_ddnnf_proj(input: String, output: String); } } @@ -13,3 +14,10 @@ mod ffi { pub fn compile_ddnnf(input: String, output: String) { ffi::compile_ddnnf(input, output); } + +/// Compiles the projected CNF from the input file into a d-DNNF and saves it in the output file. +/// +/// This is equivalent to running `d4 -i input -m proj-ddnnf-compiler --dump-ddnnf output`. +pub fn compile_ddnnf_proj(input: String, output: String) { + ffi::compile_ddnnf_proj(input, output); +}