feat: enable projected compilation

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);
+    }
 }

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);

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);
 }

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);
+}