add: sdd hashing

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>), usize)>,
+ edges: Vec<Edge>,
 }
 
 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<usize>), 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}}")?;

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<T> = std::result::Result<T, Box<dyn std::error::Error>>;

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<T> = std::result::Result<T, Box<dyn std::error::Error>>;
+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<u64, Sdd<'a>>,
+ unqiue_table: HashMap<usize, &'a Sdd<'a>>,
  // 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<u64, Sdd<'a>>) -> 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) {}

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

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