From 8ae3c392882643b6654678d920c0bbce12fcbfef Mon Sep 17 00:00:00 2001 From: Heiko Raab Date: Fri, 19 Aug 2022 18:27:49 +0200 Subject: [PATCH] improved caching, made the code more compact, and removed computations of unnecessary information --- Cargo.lock | 2 +- Cargo.toml | 2 +- src/bin/ddnnife.rs | 6 +- src/data_structure/mod.rs | 4 +- src/parser/d4_lexer.rs | 64 ++----- src/parser/mod.rs | 385 +++++++++++++++++--------------------- 6 files changed, 200 insertions(+), 263 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index fdfff60..98200f6 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -166,7 +166,7 @@ dependencies = [ [[package]] name = "ddnnf_reasoning" -version = "0.2.0" +version = "0.4.0" dependencies = [ "clap", "colour", diff --git a/Cargo.toml b/Cargo.toml index c73d197..14ed49a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "ddnnf_reasoning" -version = "0.2.0" +version = "0.4.0" authors = ["Heiko Raab; heiko.raab@uni-ulm-de", "Chico Sundermann; chico.sundermann@uni-ulm.de"] edition = "2018" license = "GNU LGPL-2.1" diff --git a/src/bin/ddnnife.rs b/src/bin/ddnnife.rs index 2b4f9ee..cf685e5 100644 --- a/src/bin/ddnnife.rs +++ b/src/bin/ddnnife.rs @@ -119,7 +119,8 @@ fn main() { println!( "Ddnnf overall count: {:#?}\n Elapsed time for parsing and overall count in seconds: {:.3}s.", - ddnnf.nodes[ddnnf.number_of_nodes - 1].count.clone(), elapsed_time + ddnnf.nodes[ddnnf.number_of_nodes - 1].count.clone(), + elapsed_time ); } else { ddnnf = dparser::build_ddnnf_tree_with_extras( @@ -129,7 +130,8 @@ fn main() { println!( "Ddnnf overall count: {:#?}\n Elapsed time for parsing and overall count in seconds: {:.3}s.", - ddnnf.nodes[ddnnf.number_of_nodes - 1].count.clone(), elapsed_time + ddnnf.nodes[ddnnf.number_of_nodes - 1].count.clone(), + elapsed_time ); } diff --git a/src/data_structure/mod.rs b/src/data_structure/mod.rs index 32e1e2f..f3d551c 100644 --- a/src/data_structure/mod.rs +++ b/src/data_structure/mod.rs @@ -53,7 +53,7 @@ static mut COUNTER: u64 = 0; impl Node { #[inline] /// Creates a new And node - pub fn new_and(children: Vec, overall_count: Integer) -> Node { + pub fn new_and(overall_count: Integer, children: Vec) -> Node { Node { marker: false, count: overall_count, @@ -69,8 +69,8 @@ impl Node { /// Creates a new Or node pub fn new_or( var_number: i32, - children: Vec, overall_count: Integer, + children: Vec, ) -> Node { Node { marker: false, diff --git a/src/parser/d4_lexer.rs b/src/parser/d4_lexer.rs index 85049e5..e0b856c 100644 --- a/src/parser/d4_lexer.rs +++ b/src/parser/d4_lexer.rs @@ -2,7 +2,7 @@ use nom::{ branch::alt, bytes::complete::tag, character::complete::{char, digit1, space1}, - combinator::{map, recognize}, + combinator::{map, recognize, value}, multi::many_m_n, sequence::{pair, preceded, terminated}, IResult, @@ -12,13 +12,13 @@ use nom::{ /// Every token gets an enum instance for the D4lexing progress pub enum D4Token { /// An inner node that contains atleast one child - And { position: i32 }, - /// An inner node that contains exactly two child nodes - Or { position: i32 }, + And, + /// An inner node that contains atleast one child + Or, /// A True node which is the sink of of the DAG - True { position: i32 }, + True, /// A False node can exist, but is rather an exception than the norm - False { position: i32 }, + False, /// An Edge between two nodes, with Edge { from: i32, @@ -74,50 +74,22 @@ fn neg_digit1(line: &str) -> IResult<&str, &str> { // Lexes an And node which is a inner node with the format "a N 0" with N as Node number. fn lex_and(line: &str) -> IResult<&str, D4Token> { - map(preceded(tag("a "), digit1), |out: &str| D4Token::And { - position: out.parse::().unwrap_or_else(|_| { - panic!( - "Was not able to parse i32 after \"a \". String was :{}", - out - ) - }), - })(line) + value(D4Token::And, preceded(tag("a "), digit1))(line) } // Lexes an Or node which is a inner node with the format "o N 0" with N as Node number. fn lex_or(line: &str) -> IResult<&str, D4Token> { - map(preceded(tag("o "), digit1), |out: &str| D4Token::Or { - position: out.parse::().unwrap_or_else(|_| { - panic!( - "Was not able to parse i32 after \"o \". String was: {}", - out - ) - }), - })(line) + value(D4Token::Or, preceded(tag("o "), digit1))(line) } // Lexes a True node which is a leaf node with the format "t N 0" with N as Node number. fn lex_true(line: &str) -> IResult<&str, D4Token> { - map(preceded(tag("t "), digit1), |out: &str| D4Token::True { - position: out.parse::().unwrap_or_else(|_| { - panic!( - "Was not able to parse i32 after \"t \". String was: {}", - out - ) - }), - })(line) + value(D4Token::True, preceded(tag("t "), digit1))(line) } // Lexes a False node which is a leaf node with the format "f N 0" with N as Node number. fn lex_false(line: &str) -> IResult<&str, D4Token> { - map(preceded(tag("f "), digit1), |out: &str| D4Token::False { - position: out.parse::().unwrap_or_else(|_| { - panic!( - "Was not able to parse i32 after \"f \". String was: {}", - out - ) - }), - })(line) + value(D4Token::False, preceded(tag("f "), digit1))(line) } #[cfg(test)] @@ -132,33 +104,33 @@ mod test { let false_str = "f 4 0"; let edge_str = "2 3 4 -5 0"; - assert_eq!(lex_and(and_str).unwrap().1, D4Token::And { position: 1 },); + assert_eq!(lex_and(and_str).unwrap().1, D4Token::And); assert_eq!( lex_line_d4(and_str).unwrap().1, - D4Token::And { position: 1 }, + D4Token::And, ); - assert_eq!(lex_or(or_str).unwrap().1, D4Token::Or { position: 2 },); - assert_eq!(lex_line_d4(or_str).unwrap().1, D4Token::Or { position: 2 },); + assert_eq!(lex_or(or_str).unwrap().1, D4Token::Or); + assert_eq!(lex_line_d4(or_str).unwrap().1, D4Token::Or); assert_eq!( lex_true(true_str).unwrap().1, - D4Token::True { position: 3 }, + D4Token::True, ); assert_eq!( lex_line_d4(true_str).unwrap().1, - D4Token::True { position: 3 }, + D4Token::True, ); assert_eq!( lex_false(false_str).unwrap().1, - D4Token::False { position: 4 }, + D4Token::False, ); assert_eq!( lex_line_d4(false_str).unwrap().1, - D4Token::False { position: 4 }, + D4Token::False, ); assert_eq!( diff --git a/src/parser/mod.rs b/src/parser/mod.rs index 45eb3d7..235536f 100644 --- a/src/parser/mod.rs +++ b/src/parser/mod.rs @@ -8,7 +8,7 @@ use core::panic; use std::{ cell::RefCell, collections::{HashMap, HashSet}, - rc::Rc + rc::Rc, }; use rug::{Complete, Integer}; @@ -21,11 +21,12 @@ use crate::data_structure::{ NodeType::{And, False, Literal, Or, True}, }; +use petgraph::Graph; use petgraph::{ - graph::{NodeIndex, EdgeIndex}, - visit::{DfsPostOrder}, Direction::Outgoing, + graph::{EdgeIndex, NodeIndex}, + visit::DfsPostOrder, + Direction::Outgoing, }; -use petgraph::{Graph}; /// Parses a ddnnf, referenced by the file path. The file gets parsed and we create /// the corresponding data structure. @@ -65,8 +66,8 @@ pub fn build_ddnnf_tree(path: &str) -> Ddnnf { (TId::PositiveLiteral, v) => Node::new_literal(v[0] as i32), (TId::NegativeLiteral, v) => Node::new_literal(-(v[0] as i32)), (TId::And, v) => Node::new_and( - v.clone(), calc_overall_and_count(&mut parsed_nodes, &v), + v, ), (TId::Or, v) => { let v_num = v.clone().remove(0) as i32; @@ -74,8 +75,8 @@ pub fn build_ddnnf_tree(path: &str) -> Ddnnf { children.remove(0); Node::new_or( v_num, - children, calc_overall_or_count(&mut parsed_nodes, &v), + children, ) } (TId::True, _) => Node::new_bool(True), @@ -98,7 +99,7 @@ pub fn build_ddnnf_tree_with_extras(path: &str) -> Ddnnf { let mut buf_reader = BufReaderMl::open(path).expect("Unable to open file"); let first_line = buf_reader.next().expect("Unable to read line").unwrap(); - let header = lex_line(first_line.trim()).unwrap().1 .1; + let header = lex_line(first_line.trim()).unwrap().1.1; let mut parsed_nodes: Vec = Vec::with_capacity(header[0]); @@ -114,17 +115,16 @@ pub fn build_ddnnf_tree_with_extras(path: &str) -> Ddnnf { (TId::PositiveLiteral, v) => Node::new_literal(v[0] as i32), (TId::NegativeLiteral, v) => Node::new_literal(-(v[0] as i32)), (TId::And, v) => Node::new_and( - v.clone(), calc_overall_and_count(&mut parsed_nodes, &v), + v, ), (TId::Or, v) => { - let v_num = v.clone().remove(0) as i32; let mut children = v.clone(); - children.remove(0); + let v_num = children.remove(0) as i32; Node::new_or( v_num, - children, calc_overall_or_count(&mut parsed_nodes, &v), + children, ) } (TId::True, _) => Node::new_bool(True), @@ -136,23 +136,15 @@ pub fn build_ddnnf_tree_with_extras(path: &str) -> Ddnnf { // fill the parent node pointer if next.node_type == And || next.node_type == Or { - let next_childs: Vec = next.children.clone().unwrap(); - let next_indize: usize = parsed_nodes.len(); - for i in next_childs { + for i in next.children.clone().unwrap() { parsed_nodes[i].parents.push(next_indize); } } // fill the HashMap with the literals if next.node_type == Literal { - if literals.contains_key(&next.var_number.unwrap()) { - panic!( - "Literal {:?} occured at least twice. This violates the standard!", - next.var_number.unwrap() - ); - } literals.insert(next.var_number.unwrap(), parsed_nodes.len()); } @@ -165,84 +157,16 @@ pub fn build_ddnnf_tree_with_extras(path: &str) -> Ddnnf { /// Parses a ddnnf, referenced by the file path. /// This function uses D4Tokens which specify a d-DNNF in d4 format. /// The file gets parsed and we create the corresponding data structure. -/// TODO actually return a smooth! d-DNNF #[inline] pub fn build_d4_ddnnf_tree(path: &str, ommited_features: u32) -> Ddnnf { let buf_reader = BufReaderMl::open(path).expect("Unable to open file"); - let mut ddnnf_graph = Graph::>::new(); - - // We have to remember the state of our literals because only two occurence of - // each literal (one positive and one negative) are allowed - #[derive(PartialEq, Debug, Clone)] - enum LiteralOcc { - Neither, - Positive, - Negative, - Both, - } - - let literal_occurences: Rc>> = - Rc::new(RefCell::new(vec![ - LiteralOcc::Neither; - (ommited_features + 1) as usize - ])); - - let lit_occ_change = |f: &i32| { - use LiteralOcc::*; - let mut lo = literal_occurences.borrow_mut(); - let f_abs = f.abs() as usize; - match (lo[f_abs].clone(), f > &0) { - (Neither, true) => lo[f_abs] = Positive, - (Neither, false) => lo[f_abs] = Negative, - (Positive, true) => (), - (Positive, false) => lo[f_abs] = Both, - (Negative, true) => lo[f_abs] = Both, - (Negative, false) => (), - (Both, _) => (), - } - }; - - let mut indices: HashMap = HashMap::new(); + let mut ddnnf_graph = Graph::::new(); - // opens the file with a BufReaderMl which is similar to a regular BufReader - // works off each line of the file data seperatly - for line in buf_reader { - let line = line.expect("Unable to read line"); - - let next: D4Token = lex_line_d4(line.as_ref()).unwrap().1; - - use D4Token::*; - match next { - Edge { from, to, features } => { - for f in &features { - lit_occ_change(f); - } - ddnnf_graph.add_edge( - indices.get(&from).unwrap().to_owned(), - indices.get(&to).unwrap().to_owned(), - features, - ); - } - And { position } => { - indices.insert(position, ddnnf_graph.add_node(TId::And)); - } - Or { position } => { - indices.insert(position, ddnnf_graph.add_node(TId::Or)); - } - True { position } => { - let tx = ddnnf_graph.add_node(TId::True); - indices.insert(position, tx); - } - False { position } => { - indices.insert(position, ddnnf_graph.add_node(TId::False)); - } - } - } + let literal_occurences: Rc>> = + Rc::new(RefCell::new(vec![false; (ommited_features + 1) as usize])); - let root = ddnnf_graph.add_node(TId::And); - let old_root: NodeIndex = NodeIndex::new(0); - ddnnf_graph.add_edge(root, old_root, Vec::new()); + let mut indices: Vec = Vec::new(); // With the help of the literals node state, we can add the required nodes // for the balancing of the or nodes to archieve smoothness @@ -251,40 +175,9 @@ pub fn build_d4_ddnnf_tree(path: &str, ommited_features: u32) -> Ddnnf { let literals_nx: Rc>> = Rc::new(RefCell::new(HashMap::new())); - let add_literal_node = - |ddnnf_graph: &mut Graph>, f_u32: u32, attach: NodeIndex| { - let f = f_u32 as i32; // we enforce f as u32 to avoid signum issues - let mut nx_lit = nx_literals.borrow_mut(); - let mut lit_nx = literals_nx.borrow_mut(); - - lit_occ_change(&(f as i32)); - let or = ddnnf_graph.add_node(TId::Or); - let pos_lit = match lit_nx.get(&f) { - Some(x) => *x, - None => { - let nx = ddnnf_graph.add_node(TId::PositiveLiteral); - nx_lit.insert(nx, f); - lit_nx.insert(f, nx); - nx - } - }; - let neg_lit = match lit_nx.get(&-f) { - Some(x) => *x, - None => { - let nx = ddnnf_graph.add_node(TId::NegativeLiteral); - nx_lit.insert(nx, -f); - lit_nx.insert(-f, nx); - nx - } - }; - - ddnnf_graph.add_edge(attach, or, Vec::new()); - ddnnf_graph.add_edge(or, pos_lit, Vec::new()); - ddnnf_graph.add_edge(or, neg_lit, Vec::new()); - }; - - let get_literal_indices = - |ddnnf_graph: &mut Graph>, literals: Vec| -> Vec { + let get_literal_indices = |ddnnf_graph: &mut Graph, + literals: Vec| + -> Vec { let mut nx_lit = nx_literals.borrow_mut(); let mut lit_nx = literals_nx.borrow_mut(); @@ -313,110 +206,172 @@ pub fn build_d4_ddnnf_tree(path: &str, ommited_features: u32) -> Ddnnf { }) } } - literal_nodes }; + // while parsing: + // remove the weighted edges and substitute it with the corresponding + // structure that uses AND-Nodes and Literal-Nodes. Example: + // + // n1 n1 + // / \ / \ + // Ln| |Lm into AND AND + // \ / / \ / \ + // n2 Ln n2 Lm + // + // let resolve_weighted_edge = - |ddnnf_graph: &mut Graph>, from: NodeIndex, to: NodeIndex, edge: EdgeIndex| { + |ddnnf_graph: &mut Graph, + from: NodeIndex, + to: NodeIndex, + edge: EdgeIndex, + weights: Vec| { let and_node = ddnnf_graph.add_node(TId::And); - let literal_nodes = get_literal_indices(ddnnf_graph, ddnnf_graph.edge_weight(edge).unwrap().clone()); + let literal_nodes = get_literal_indices( + ddnnf_graph, + weights, + ); ddnnf_graph.remove_edge(edge); - ddnnf_graph.add_edge(from, and_node, Vec::new()); + ddnnf_graph.add_edge(from, and_node, ()); for node in literal_nodes { - ddnnf_graph.add_edge(and_node, node, Vec::new()); + ddnnf_graph.add_edge(and_node, node, ()); } - ddnnf_graph.add_edge(and_node, to, Vec::new()); + ddnnf_graph.add_edge(and_node, to, ()); }; - let balance_or_children = - |ddnnf_graph: &mut Graph>, from: NodeIndex, children: Vec<(NodeIndex, HashSet)>| { - if children.is_empty() { return; } + // opens the file with a BufReaderMl which is similar to a regular BufReader + // works off each line of the file data seperatly + for line in buf_reader { + let line = line.expect("Unable to read line"); - for child in children { - if child.1.is_empty() { continue; } + let next: D4Token = lex_line_d4(line.as_ref()).unwrap().1; + + use D4Token::*; + match next { + Edge { from, to, features } => { + for f in &features { + literal_occurences.borrow_mut()[f.abs() as usize] = true; + } + let from_n = indices[from as usize - 1]; + let to_n = indices[to as usize - 1]; + let edge = ddnnf_graph.add_edge( + from_n, + to_n, + () + ); + resolve_weighted_edge(&mut ddnnf_graph, from_n, to_n, edge, features); + } + And => { + indices.push(ddnnf_graph.add_node(TId::And)); + } + Or => { + indices.push(ddnnf_graph.add_node(TId::Or)); + } + True => { + indices.push(ddnnf_graph.add_node(TId::True)); + } + False => { + indices.push(ddnnf_graph.add_node(TId::False)); + } + } + } - let and_node = ddnnf_graph.add_node(TId::And); + let or_triangles: Rc>>> = Rc::new(RefCell::new(vec![None; (ommited_features + 1) as usize])); - // place the newly created and node between the or node and its child - ddnnf_graph.remove_edge(ddnnf_graph.find_edge(from, child.0).unwrap()); - ddnnf_graph.add_edge(from, and_node, Vec::new()); - ddnnf_graph.add_edge(and_node, child.0, Vec::new()); + let add_literal_node = |ddnnf_graph: &mut Graph, + f_u32: u32, + attach: NodeIndex| { + let f = f_u32 as i32; + let mut ort = or_triangles.borrow_mut(); - for literal in child.1 { - add_literal_node(ddnnf_graph, literal, and_node); - } + if ort[f_u32 as usize].is_some() { + ddnnf_graph.add_edge(attach, ort[f_u32 as usize].unwrap(), ()); + } else { + let or = ddnnf_graph.add_node(TId::Or); + ort[f_u32 as usize] = Some(or); + + let pos_lit = get_literal_indices(ddnnf_graph, vec![f])[0]; + let neg_lit = get_literal_indices(ddnnf_graph, vec![-f])[0]; + + ddnnf_graph.add_edge(attach, or, ()); + ddnnf_graph.add_edge(or, pos_lit, ()); + ddnnf_graph.add_edge(or, neg_lit, ()); } }; + let balance_or_children = + |ddnnf_graph: &mut Graph, + from: NodeIndex, + children: Vec<(NodeIndex, HashSet)>| { + for child in children { + let and_node = ddnnf_graph.add_node(TId::And); + + // place the newly created and node between the or node and its child + ddnnf_graph + .remove_edge(ddnnf_graph.find_edge(from, child.0).unwrap()); + ddnnf_graph.add_edge(from, and_node, ()); + ddnnf_graph.add_edge(and_node, child.0, ()); + + for literal in child.1 { + add_literal_node(ddnnf_graph, literal, and_node); + } + } + }; + + // add a new root which hold the unmentioned variables within the ommited_features range + let root = ddnnf_graph.add_node(TId::And); + ddnnf_graph.add_edge(root, NodeIndex::new(0), ()); + // add literals that are not mentioned in the ddnnf to the new root node for i in 1..ommited_features + 1 { - if literal_occurences.borrow()[i as usize] == LiteralOcc::Neither { + if !literal_occurences.borrow()[i as usize] { add_literal_node(&mut ddnnf_graph, i, root); } } - // first dfs: - // remove the weighted edges and substitute it with the corresponding - // structure that uses AND-Nodes and Literal-Nodes. Example: - // - // n1 n1 - // / \ / \ - // Ln| |Lm into AND AND - // \ / / \ / \ - // n2 Ln n2 Lm - // - // - let mut dfs = DfsPostOrder::new(&ddnnf_graph, root); - while let Some(nx) = dfs.next(&ddnnf_graph) { - // edges between going from an and node to another node do not - // have any weights attached to them. Therefore, we can skip them - if ddnnf_graph[nx] != TId::Or { continue; } - let mut neighbors = ddnnf_graph.neighbors_directed(nx, Outgoing).detach(); - - while let Some(neighbor) = neighbors.next(&ddnnf_graph) { - if ddnnf_graph.edge_weight(neighbor.0).unwrap().is_empty() { continue; } - resolve_weighted_edge(&mut ddnnf_graph, nx, neighbor.1, neighbor.0); - } - } - // snd dfs: // Look at each or node. For each outgoing edge: // 1. Compute all literals that occur in the children of that edge // 2. Determine which literals occur only in the other paths // 3. Add those literals in the path we are currently looking at // Example: - // - // OR + // + // OR // OR / \ // / \ / \ // Ln AND into AND AND // / \ / \ / \ // Lm -Ln Ln OR | -Ln // / \ / - // -Lm Lm + // -Lm Lm // - let mut safe: HashMap> = HashMap::new(); - dfs = DfsPostOrder::new(&ddnnf_graph, root); + let mut dfs = DfsPostOrder::new(&ddnnf_graph, root); while let Some(nx) = dfs.next(&ddnnf_graph) { // edges between going from an and node to another node do not // have any weights attached to them. Therefore, we can skip them - if ddnnf_graph[nx] != TId::Or { continue; } - let diffrences = get_literal_diff(&ddnnf_graph, &mut safe, &nx_literals.borrow(), nx); - balance_or_children(&mut ddnnf_graph, nx, diffrences); + if ddnnf_graph[nx] == TId::Or { + let diffrences = get_literal_diff( + &ddnnf_graph, + &mut safe, + &nx_literals.borrow(), + nx, + ); + balance_or_children(&mut ddnnf_graph, nx, diffrences); + } } // perform a depth first search to get the nodes ordered such // that child nodes are listed before their parents // transform that interim representation into a node vector - let mut dfs = DfsPostOrder::new(&ddnnf_graph, root); + dfs = DfsPostOrder::new(&ddnnf_graph, root); let mut nd_to_usize: HashMap = HashMap::new(); - let mut parsed_nodes: Vec = Vec::new(); + let mut parsed_nodes: Vec = Vec::with_capacity(ddnnf_graph.node_count()); let mut literals: HashMap = HashMap::new(); + let nx_lit = nx_literals.borrow(); while let Some(nx) = dfs.next(&ddnnf_graph) { nd_to_usize.insert(nx, parsed_nodes.len()); @@ -426,21 +381,19 @@ pub fn build_d4_ddnnf_tree(path: &str, ommited_features: u32) -> Ddnnf { .collect::>(); let next: Node = match ddnnf_graph[nx] { // extract the parsed Token - TId::PositiveLiteral => { - Node::new_literal(*nx_literals.borrow().get(&nx).unwrap()) - } + TId::PositiveLiteral | TId::NegativeLiteral => { - Node::new_literal(*nx_literals.borrow().get(&nx).unwrap()) + Node::new_literal(nx_lit.get(&nx).unwrap().to_owned()) } TId::And => Node::new_and( - neighs.clone(), calc_overall_and_count(&mut parsed_nodes, &neighs), + neighs, ), TId::Or => Node::new_or( 0, - neighs.clone(), calc_overall_or_count_multiple_children(&mut parsed_nodes, &neighs), + neighs, ), TId::True => Node::new_bool(True), TId::False => Node::new_bool(False), @@ -451,23 +404,14 @@ pub fn build_d4_ddnnf_tree(path: &str, ommited_features: u32) -> Ddnnf { // fill the parent node pointer if next.node_type == And || next.node_type == Or { - let next_childs: Vec = next.children.clone().unwrap(); - let next_indize: usize = parsed_nodes.len(); - - for i in next_childs { + for i in next.children.clone().unwrap() { parsed_nodes[i].parents.push(next_indize); } } // fill the HashMap with the literals if next.node_type == Literal { - if literals.contains_key(&next.var_number.unwrap()) { - panic!( - "Literal {:?} occured at least twice. This violates the standard!", - next.var_number.unwrap() - ); - } literals.insert(next.var_number.unwrap(), parsed_nodes.len()); } @@ -479,28 +423,43 @@ pub fn build_d4_ddnnf_tree(path: &str, ommited_features: u32) -> Ddnnf { } // determine the differences in literal-nodes occuring in the child nodes -fn get_literal_diff(graph: &Graph>, safe: &mut HashMap>, nx_literals: &HashMap, or_node: NodeIndex) -> Vec<(NodeIndex, HashSet)> { +fn get_literal_diff( + graph: &Graph, + safe: &mut HashMap>, + nx_literals: &HashMap, + or_node: NodeIndex, +) -> Vec<(NodeIndex, HashSet)> { let mut inter_res = Vec::new(); let neighbors = graph.neighbors_directed(or_node, Outgoing); - + for neighbor in neighbors { - inter_res.push((neighbor, get_literals(graph, safe, nx_literals, neighbor))); + inter_res + .push((neighbor, get_literals(graph, safe, nx_literals, neighbor))); } let mut res: Vec<(NodeIndex, HashSet)> = Vec::new(); for i in 0..inter_res.len() { let mut val: HashSet = HashSet::new(); for (j, i_res) in inter_res.iter().enumerate() { - if i == j { continue; } - val.extend(&i_res.1); + if i != j { + val.extend(&i_res.1); + } + } + val = &val - &inter_res[i].1; + if !val.is_empty() { + res.push((inter_res[i].0, val)); } - res.push((inter_res[i].0, &val - &inter_res[i].1)); } res } // determine what literal-nodes the current node is or which occur in its children -fn get_literals(graph: &Graph>, safe: &mut HashMap>, nx_literals: &HashMap, or_child: NodeIndex) -> HashSet { +fn get_literals( + graph: &Graph, + safe: &mut HashMap>, + nx_literals: &HashMap, + or_child: NodeIndex, +) -> HashSet { let lookup = safe.get(&or_child); if let Some(x) = lookup { return x.clone(); @@ -509,12 +468,17 @@ fn get_literals(graph: &Graph>, safe: &mut HashMap { graph.neighbors_directed(or_child, Outgoing) - .for_each(|n| res.extend(get_literals(graph, safe, nx_literals, n))); safe.insert(or_child, res.clone()); }, - PositiveLiteral | NegativeLiteral - => { res.insert(nx_literals.get(&or_child).unwrap().abs() as u32); safe.insert(or_child, res.clone()); }, - _ => { safe.insert(or_child, res.clone()); }, + And | Or => { + graph.neighbors_directed(or_child, Outgoing).for_each(|n| { + res.extend(get_literals(graph, safe, nx_literals, n)) + }); + safe.insert(or_child, res.clone()); + } + PositiveLiteral | NegativeLiteral => { + res.insert(nx_literals.get(&or_child).unwrap().abs() as u32); + safe.insert(or_child, res.clone()); + } + _ => () } res } @@ -537,8 +501,7 @@ fn calc_overall_or_count_multiple_children( nodes: &mut Vec, indizes: &[usize], ) -> Integer { - Integer::sum(indizes.iter().map(|indize| &nodes[*indize].count)) - .complete() + Integer::sum(indizes.iter().map(|indize| &nodes[*indize].count)).complete() } /// Is used to parse the queries in the config files