Skip to content

Commit

Permalink
Merge pull request #37 from SoftVarE-Group/fix-parallel-compiling
Browse files Browse the repository at this point in the history
Use temporary file for compiling CNFs to d-DNNFs
  • Loading branch information
uulm-janbaudisch authored Aug 28, 2024
2 parents 1485b75 + e16d064 commit c4ba0ba
Show file tree
Hide file tree
Showing 3 changed files with 50 additions and 36 deletions.
32 changes: 16 additions & 16 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion ddnnife/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ rand = "0.8"
rand_distr = "0.4"
rand_pcg = "0.3"
streaming-iterator = "0.1"
tempfile = "3.10"
tempfile = "3.12"
uniffi = { workspace = true, optional = true }
workctl = "0.2"

Expand Down
52 changes: 33 additions & 19 deletions ddnnife/src/parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,32 +5,35 @@ pub mod d4_lexer;
use d4_lexer::{lex_line_d4, D4Token};

pub mod from_cnf;
use from_cnf::{check_for_cnf_header, CNFToken};

pub mod persisting;

use crate::ddnnf::{node::Node, node::NodeType, Ddnnf};
use core::panic;
use num::BigInt;
use petgraph::{
graph::{EdgeIndex, NodeIndex},
stable_graph::StableGraph,
visit::DfsPostOrder,
Direction::{Incoming, Outgoing},
};
use std::{
cell::RefCell,
cmp::max,
collections::{BTreeSet, HashMap, HashSet},
ffi::OsStr,
fs::{self, File},
fs::File,
io::{BufRead, BufReader},
path::Path,
process,
rc::Rc,
};

use crate::ddnnf::{node::Node, node::NodeType, Ddnnf};
#[cfg(feature = "d4")]
use tempfile::NamedTempFile;

use petgraph::{
graph::{EdgeIndex, NodeIndex},
stable_graph::StableGraph,
visit::DfsPostOrder,
Direction::{Incoming, Outgoing},
};
#[cfg(feature = "d4")]
use from_cnf::{check_for_cnf_header, CNFToken};

/// Parses a ddnnf, referenced by the file path. The file gets parsed and we create
/// the corresponding data structure.
Expand All @@ -50,8 +53,11 @@ use petgraph::{
///
/// The function panics for an invalid file path.
#[inline]
pub fn build_ddnnf(mut path: &str, mut total_features: Option<u32>) -> Ddnnf {
#[allow(unused_mut)]
pub fn build_ddnnf(path: &str, mut total_features: Option<u32>) -> Ddnnf {
let mut ddnnf = File::open(path).expect("Failed to open input file.");
let mut clauses = BTreeSet::new();

if let Some(extension) = Path::new(path).extension().and_then(OsStr::to_str) {
if extension == "dimacs" || extension == "cnf" {
#[cfg(feature = "d4")]
Expand All @@ -65,10 +71,23 @@ pub fn build_ddnnf(mut path: &str, mut total_features: Option<u32>) -> Ddnnf {
total_features: total_features_header,
total_clauses: _,
} => {
let ddnnf_file = ".intermediate.nnf";
d4_oxide::compile_ddnnf(path.to_string(), ddnnf_file.to_string());
path = ddnnf_file;
let temporary_ddnnf = NamedTempFile::new()
.expect("Failed to create temporary d-DNNF file.");

d4_oxide::compile_ddnnf(
path.to_string(),
temporary_ddnnf
.path()
.to_str()
.expect("Failed to serialize temporary d-DNNF path.")
.to_string(),
);

total_features = Some(total_features_header as u32);

ddnnf = temporary_ddnnf
.reopen()
.expect("Failed to open temporary d-DNNF.");
}
CNFToken::Clause { features } => {
clauses.insert(features);
Expand All @@ -85,16 +104,11 @@ pub fn build_ddnnf(mut path: &str, mut total_features: Option<u32>) -> Ddnnf {
}
}

let file = open_file_savely(path);
let lines = BufReader::new(file)
let lines = BufReader::new(ddnnf)
.lines()
.map(|line| line.expect("Unable to read line"))
.collect::<Vec<String>>();

if path == ".intermediate.nnf" {
fs::remove_file(path).unwrap();
}

if clauses.is_empty() {
distribute_building(lines, total_features, None)
} else {
Expand Down

0 comments on commit c4ba0ba

Please sign in to comment.