diff --git a/sdd-rs-lib/dot_writer.rs b/sdd-rs-lib/dot_writer.rs index c335c4a..63eeaa6 100644 --- a/sdd-rs-lib/dot_writer.rs +++ b/sdd-rs-lib/dot_writer.rs @@ -1,13 +1,29 @@ -use crate::manager::Result; +use crate::Result; pub trait Dot { fn draw(&self, writer: &mut DotWriter); } +pub enum Edge { + Simple(usize, usize), + Prime(usize, usize), + Sub(usize, usize), +} + +impl std::fmt::Display for Edge { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + Edge::Simple(from, to) => write!(f, "{from} -> {to}"), + Edge::Prime(from, to) => write!(f, "{from}:f0 -> {to}"), + Edge::Sub(from, to) => write!(f, "{from}:f1 -> {to}"), + } + } +} + #[derive(Default)] pub struct DotWriter { nodes: Vec<(usize, NodeType)>, - edges: Vec<((usize, Option), usize)>, + edges: Vec, } pub enum NodeType { @@ -51,8 +67,8 @@ impl DotWriter { self.nodes.push((node_idx, node_type)); } - pub fn add_edge(&mut self, from: (usize, Option), to: usize) { - self.edges.push((from, to)); + pub fn add_edge(&mut self, edge: Edge) { + self.edges.push(edge); } /// # Errors @@ -63,21 +79,16 @@ impl DotWriter { for (node, node_type) in &self.nodes { write!( writer, - "\n {} [{} {} {}]", - node, + "\n {node} [{} {} {}]", node_type.shape(), node_type.label(), NodeType::metadata(), )?; } - for ((from, from_child), to) in &self.edges { - if let Some(from_child) = from_child { - // TODO: Make the edge begin in the middle of the child. - write!(writer, "\n {from}:f{from_child} -> {to} [arrowsize=.50]")?; - } else { - write!(writer, "\n {from} -> {to} [arrowsize=.50]")?; - } + for edge in &self.edges { + // TODO: Make the edge begin in the middle of the child. + write!(writer, "\n {edge} [arrowsize=.50]")?; } write!(writer, "\n}}")?; diff --git a/sdd-rs-lib/lib.rs b/sdd-rs-lib/lib.rs index 9a28921..eb23c22 100644 --- a/sdd-rs-lib/lib.rs +++ b/sdd-rs-lib/lib.rs @@ -6,3 +6,5 @@ pub mod sdd; pub mod util; pub mod dot_writer; pub mod vtree; + +pub type Result = std::result::Result>; diff --git a/sdd-rs-lib/manager.rs b/sdd-rs-lib/manager.rs index fbb6d92..3fbe878 100644 --- a/sdd-rs-lib/manager.rs +++ b/sdd-rs-lib/manager.rs @@ -5,8 +5,7 @@ use crate::literal::VarLabelManager; use crate::options::SddOptions; use crate::sdd::{Node, Sdd}; use crate::vtree::VTreeManager; - -pub type Result = std::result::Result>; +use crate::Result; #[allow(clippy::module_name_repetitions)] pub struct SddManager<'a> { @@ -22,7 +21,7 @@ pub struct SddManager<'a> { // Unique table holding all the decision nodes. // More details can be found in [Algorithms and Data Structures in VLSI Design](https://link.springer.com/book/10.1007/978-3-642-58940-9). - unqiue_table: HashMap>, + unqiue_table: HashMap>, // u64 is the hash of sdd::Decision // TODO: Should we store sdd::Decision or sdd::Node? } @@ -41,18 +40,25 @@ impl<'a> SddManager<'a> { // TODO: This function should be removed as user should not be able to fill the unique_table // directly. #[must_use] - pub fn new_with_nodes(options: SddOptions, nodes: HashMap>) -> SddManager { + pub fn new_with_nodes(options: SddOptions, sdds: &'a [&'a Sdd<'a>]) -> SddManager<'a> { + let mut table = HashMap::new(); + for sdd in sdds { + table.insert(sdd.id(), *sdd); + } + SddManager { options, vtree_manager: VTreeManager::new(), var_label_manager: VarLabelManager::new(), - unqiue_table: nodes, + unqiue_table: table, } } + /// # Panics + /// Function panics if there is no such node with the corresponding id in the unique table. #[must_use] - pub fn get_node(&self, id: &u64) -> Option<&'a Sdd> { - self.unqiue_table.get(id) + pub fn get_node(&self, id: usize) -> &'a Sdd { + self.unqiue_table.get(&id).unwrap() } pub fn conjoin(&self, _fst: &Node, _snd: &Node) {} diff --git a/sdd-rs-lib/sdd.rs b/sdd-rs-lib/sdd.rs index 2287da0..ec0ef2b 100644 --- a/sdd-rs-lib/sdd.rs +++ b/sdd-rs-lib/sdd.rs @@ -1,7 +1,7 @@ use std::collections::{BTreeSet, HashSet}; use std::hash::Hash; -use crate::dot_writer::{Dot, DotWriter, NodeType}; +use crate::dot_writer::{Dot, DotWriter, Edge, NodeType}; use crate::literal::Literal; use crate::manager::SddManager; @@ -60,10 +60,10 @@ impl<'a> Dot for Element<'a> { ); if let Sdd::DecisionRegular(node) | Sdd::DecisionComplement(node) = self.prime { - writer.add_edge((idx, Some(0)), fxhash::hash(node)); + writer.add_edge(Edge::Prime(idx, fxhash::hash(node))); } if let Sdd::DecisionRegular(node) | Sdd::DecisionComplement(node) = self.sub { - writer.add_edge((idx, Some(1)), fxhash::hash(node)); + writer.add_edge(Edge::Sub(idx, fxhash::hash(node))); }; } } @@ -88,7 +88,7 @@ impl<'a> Dot for Sdd<'a> { idx = fxhash::hash(node); for elem in &node.elements { elem.draw(writer); - writer.add_edge((idx, None), fxhash::hash(elem)); + writer.add_edge(Edge::Simple(idx, fxhash::hash(elem))); } // TODO: Add proper vtree index to the NodeType::Circle once implemented. NodeType::Circle(42) @@ -100,6 +100,16 @@ impl<'a> Dot for Sdd<'a> { } impl<'a> Sdd<'a> { + #[must_use] + pub fn id(&self) -> usize { + match self { + Sdd::DecisionComplement(decision) | Sdd::DecisionRegular(decision) => { + fxhash::hash(decision) + } + _ => fxhash::hash(self), + } + } + fn is_true(&self) -> bool { matches!(self, Sdd::True) } diff --git a/sdd-rs-lib/sdd_test.rs b/sdd-rs-lib/sdd_test.rs index d4c6e6b..a55f667 100644 --- a/sdd-rs-lib/sdd_test.rs +++ b/sdd-rs-lib/sdd_test.rs @@ -1,7 +1,5 @@ #[allow(clippy::module_inception)] mod sdd_test { - use std::collections::HashMap; - use crate::{ btreeset, literal::{Literal, Polarity, VarLabel}, @@ -15,25 +13,22 @@ mod sdd_test { #[test] fn not_trimmed_simple() { - // TODO: Remove the hardcoded indices once the hashing scheme is implemented. let element = Element { prime: &Sdd::True, sub: &Sdd::False, }; - let decision = Decision { + + // Decomposition `{(true, false)}`. + let decision = &Decision { elements: btreeset!(&element), }; + let sdd = &Sdd::DecisionRegular(decision); - let manager = SddManager::new_with_nodes( - SddOptions::new(), - HashMap::from([ - // Decomposition `{(true, false)}`. - (0_u64, Sdd::DecisionRegular(&decision)), - ]), - ); + let decisions = &vec![sdd]; + let manager = SddManager::new_with_nodes(SddOptions::new(), decisions); // Decomposition {(True, False)} is not trimmed. - let node = manager.get_node(&0_u64).unwrap(); + let node = manager.get_node(sdd.id()); assert!(!node.is_trimmed(&manager)); } @@ -43,20 +38,18 @@ mod sdd_test { prime: &Sdd::True, sub: &boxed_literal(Polarity::Positive, "A"), }; - let decision = Decision { + + // Decomposition `{(true, A)}`. + let decision = &Decision { elements: btreeset!(&element), }; + let sdd = &Sdd::DecisionRegular(decision); - let manager = SddManager::new_with_nodes( - SddOptions::new(), - HashMap::from([ - // Decomposition `{(true, A)}`. - (0_u64, Sdd::DecisionRegular(&decision)), - ]), - ); + let decisions = &vec![sdd]; + let manager = SddManager::new_with_nodes(SddOptions::new(), decisions); // Decomposition {(A, true)} is not trimmed. - let node = manager.get_node(&0_u64).unwrap(); + let node = manager.get_node(sdd.id()); assert!(!node.is_trimmed(&manager)); } @@ -70,20 +63,18 @@ mod sdd_test { prime: &boxed_literal(Polarity::Negative, "A"), sub: &Sdd::False, }; - let decision = Decision { + + // Decomposition `{(A, true), (!A, false)}`. + let decision = &Decision { elements: btreeset!(&element_1, &element_2), }; + let sdd = &Sdd::DecisionRegular(decision); - let manager = SddManager::new_with_nodes( - SddOptions::new(), - HashMap::from([ - // Decomposition `{(A, true), (!A, false)}`. - (0_u64, Sdd::DecisionRegular(&decision)), - ]), - ); + let decisions = &vec![sdd]; + let manager = SddManager::new_with_nodes(SddOptions::new(), decisions); // Decomposition `{(A, true), (!A, false)}` is not trimmed. - let node = manager.get_node(&0_u64).unwrap(); + let node = manager.get_node(sdd.id()); assert!(!node.is_trimmed(&manager)); } @@ -94,32 +85,35 @@ mod sdd_test { prime: &Sdd::True, sub: &boxed_literal(Polarity::Negative, "B"), }; + + // Decomposition `{(true, !B)}`. This is where the SDD stops being trimmed. let decision_1 = &Decision { elements: btreeset!(&element_1_1), }; + + let sdd_1 = &Sdd::DecisionRegular(decision_1); + let element_2_1 = Element { prime: &boxed_literal(Polarity::Positive, "A"), sub: &Sdd::True, }; + let element_2_2 = Element { prime: &Sdd::DecisionRegular(decision_1), sub: &Sdd::False, }; - let decision_2 = Decision { + + // Decomposition `{(A, true), (ptr, false)}` where ptr is the decomposition `{(true, !B)}`. + let decision_2 = &Decision { elements: btreeset!(&element_2_1, &element_2_2), }; - let manager = SddManager::new_with_nodes( - SddOptions::new(), - HashMap::from([ - // Decomposition `{(true, !B)}`. This is where the SDD stops being trimmed. - (0_u64, Sdd::DecisionRegular(&decision_1)), - // Decomposition `{(A, true), (ptr, false)}` where ptr is the decomposition `{(true, !B)}`. - (1_u64, Sdd::DecisionRegular(&decision_2)), - ]), - ); + let sdd_2 = &Sdd::DecisionRegular(decision_2); - let node = manager.get_node(&1_u64).unwrap(); + let decisions = &vec![sdd_1, sdd_2]; + let manager = SddManager::new_with_nodes(SddOptions::new(), decisions); + + let node = manager.get_node(sdd_2.id()); assert!(!node.is_trimmed(&manager)); } @@ -133,20 +127,18 @@ mod sdd_test { prime: &boxed_literal(Polarity::Positive, "A"), sub: &Sdd::False, }; - let decision = Decision { + + // Decomposition `{(A, true), (B, false)}`. + let decision = &Decision { elements: btreeset!(&element_1, &element_2), }; + let sdd = &Sdd::DecisionRegular(decision); - let manager = SddManager::new_with_nodes( - SddOptions::new(), - HashMap::from([ - // Decomposition `{(A, true), (B, false)}`. - (0_u64, Sdd::DecisionRegular(&decision)), - ]), - ); + let decisions = &vec![sdd]; + let manager = SddManager::new_with_nodes(SddOptions::new(), decisions); // Decomposition {(A, true), (B, false)} is trimmed. - let node = manager.get_node(&0_u64).unwrap(); + let node = manager.get_node(sdd.id()); assert!(node.is_trimmed(&manager)); } @@ -156,33 +148,32 @@ mod sdd_test { prime: &boxed_literal(Polarity::Negative, "B"), sub: &Sdd::True, }; + + // Decomposition `{(!B, true)}`. let decision_1 = &Decision { elements: btreeset!(&element_1_1), }; + let sdd_1 = &Sdd::DecisionRegular(decision_1); let element_2_1 = Element { prime: &boxed_literal(Polarity::Positive, "A"), sub: &Sdd::True, }; let element_2_2 = Element { - prime: &Sdd::DecisionRegular(decision_1), + prime: sdd_1, sub: &Sdd::False, }; - let decision_2 = Decision { + + // Decomposition `{(A, true), (ptr, false)}`, where ptr is `{(!B, true)}`. + let decision_2 = &Decision { elements: btreeset!(&element_2_1, &element_2_2), }; + let sdd_2 = &Sdd::DecisionRegular(decision_2); - let manager = SddManager::new_with_nodes( - SddOptions::new(), - HashMap::from([ - // Decomposition `{(!B, true)}`. - (0_u64, Sdd::DecisionRegular(&decision_1)), - // Decomposition `{(A, true), (ptr, false)}`, where ptr is `{(!B, true)}`. - (1_u64, Sdd::DecisionRegular(&decision_2)), - ]), - ); + let decisions = &vec![sdd_1, sdd_2]; + let manager = SddManager::new_with_nodes(SddOptions::new(), decisions); - let node = manager.get_node(&1_u64).unwrap(); + let node = manager.get_node(sdd_2.id()); assert!(node.is_trimmed(&manager)); }