vtree: add basic graphviz support

sdd-rs-lib/dot_writer.rs

@@ -29,6 +29,7 @@ pub struct DotWriter {
 pub enum NodeType {
  Box(String),
  Circle(u32),
+ CircleStr(String),
  Record(String, String),
 }
 
@@ -37,7 +38,7 @@ impl NodeType {
  let shape_type = match self {
  NodeType::Box(_) => "box",
  NodeType::Record(_, _) => "record",
- NodeType::Circle(_) => "circle",
+ NodeType::Circle(_) | NodeType::CircleStr(_) => "circle",
  }
  .to_owned();
 
@@ -48,6 +49,7 @@ impl NodeType {
  match self {
  NodeType::Record(fst, snd) => format!("label=\"<f0> {fst} | <f1> {snd}\""),
  NodeType::Circle(label) => format!("label=\"{label}\""),
+ NodeType::CircleStr(label) => format!("label=\"{label}\""),
  NodeType::Box(_) => String::new(),
  }
  }

sdd-rs-lib/literal.rs

@@ -1,31 +1,17 @@
 use std::fmt::Display;
 
 #[derive(Hash, Eq, PartialEq, Debug, Clone, PartialOrd, Ord)]
-// TODO: Do we want String labels?
 pub struct VarLabel(String);
 
 impl VarLabel {
  #[must_use]
  pub fn new(v: &str) -> VarLabel {
  VarLabel(v.to_owned())
  }
-}
-
-pub struct VarLabelManager {
- // TODO: bitset?, vector, hashmap?
-}
-
-impl VarLabelManager {
- #[must_use]
- pub fn new() -> VarLabelManager {
- VarLabelManager {}
- }
-}
 
-impl Default for VarLabelManager {
  #[must_use]
- fn default() -> Self {
- VarLabelManager::new()
+ pub fn str(&self) -> String {
+ self.0.clone()
  }
 }
 

sdd-rs-lib/manager.rs

@@ -1,11 +1,13 @@
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
 
-use crate::dot_writer::{Dot, DotWriter};
-use crate::literal::VarLabelManager;
-use crate::options::SddOptions;
-use crate::sdd::{Node, Sdd};
-use crate::vtree::VTreeManager;
-use crate::Result;
+use crate::{
+ dot_writer::{Dot, DotWriter},
+ literal::VarLabel,
+ options::SddOptions,
+ sdd::{Node, Sdd},
+ vtree::{VTree, VTreeManager},
+ Result,
+};
 
 #[allow(clippy::module_name_repetitions)]
 pub struct SddManager<'a> {
@@ -17,43 +19,48 @@ pub struct SddManager<'a> {
  vtree_manager: VTreeManager,
 
  #[allow(unused)]
- var_label_manager: VarLabelManager,
+ var_labels: HashSet<VarLabel>,
 
  // 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<usize, &'a Sdd<'a>>,
- // u64 is the hash of sdd::Decision
- // TODO: Should we store sdd::Decision or sdd::Node?
 }
 
 impl<'a> SddManager<'a> {
  #[must_use]
- pub fn new(options: SddOptions) -> SddManager<'a> {
+ pub fn new(options: SddOptions, vtree: Option<VTree>) -> SddManager<'a> {
  SddManager {
  options,
- vtree_manager: VTreeManager::new(),
- var_label_manager: VarLabelManager::new(),
+ vtree_manager: VTreeManager::new(vtree),
+ var_labels: HashSet::new(),
  unqiue_table: HashMap::new(),
  }
  }
 
  // 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, sdds: &'a [&'a Sdd<'a>]) -> SddManager<'a> {
+ pub fn new_with_nodes(
+ options: SddOptions,
+ sdds: &'a [&'a Sdd<'a>],
+ vtree: Option<VTree>,
+ ) -> 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(),
+ vtree_manager: VTreeManager::new(vtree),
+ var_labels: HashSet::new(),
  unqiue_table: table,
  }
  }
 
+ pub fn tautology(&self) {}
+ pub fn contradiction(&self) {}
+
  /// # Panics
  /// Function panics if there is no such node with the corresponding id in the unique table.
  #[must_use]
@@ -84,14 +91,9 @@ impl<'a> SddManager<'a> {
  /// # Errors
  /// Returns an error if TBD.
  pub fn draw_vtree_graph(&self, writer: &mut dyn std::io::Write) -> Result<()> {
- // TODO: Delete the function body and implement draw for vtree.
  let mut dot_writer = DotWriter::new();
- for node in self.unqiue_table.values() {
- node.draw(&mut dot_writer);
- }
- dot_writer.write(writer)?;
-
- unimplemented!("TBD")
+ self.vtree_manager.draw(&mut dot_writer);
+ dot_writer.write(writer)
  }
  // TODO: expose operations manipulating the vtree.
 }

sdd-rs-lib/sdd_test.rs

@@ -25,7 +25,7 @@ mod sdd_test {
  let sdd = &Sdd::DecisionRegular(decision);
 
  let decisions = &vec![sdd];
- let manager = SddManager::new_with_nodes(SddOptions::new(), decisions);
+ let manager = SddManager::new_with_nodes(SddOptions::new(), decisions, None);
 
  // Decomposition {(True, False)} is not trimmed.
  let node = manager.get_node(sdd.id());
@@ -46,7 +46,7 @@ mod sdd_test {
  let sdd = &Sdd::DecisionRegular(decision);
 
  let decisions = &vec![sdd];
- let manager = SddManager::new_with_nodes(SddOptions::new(), decisions);
+ let manager = SddManager::new_with_nodes(SddOptions::new(), decisions, None);
 
  // Decomposition {(A, true)} is not trimmed.
  let node = manager.get_node(sdd.id());
@@ -71,7 +71,7 @@ mod sdd_test {
  let sdd = &Sdd::DecisionRegular(decision);
 
  let decisions = &vec![sdd];
- let manager = SddManager::new_with_nodes(SddOptions::new(), decisions);
+ let manager = SddManager::new_with_nodes(SddOptions::new(), decisions, None);
 
  // Decomposition `{(A, true), (!A, false)}` is not trimmed.
  let node = manager.get_node(sdd.id());
@@ -111,7 +111,7 @@ mod sdd_test {
  let sdd_2 = &Sdd::DecisionRegular(decision_2);
 
  let decisions = &vec![sdd_1, sdd_2];
- let manager = SddManager::new_with_nodes(SddOptions::new(), decisions);
+ let manager = SddManager::new_with_nodes(SddOptions::new(), decisions, None);
 
  let node = manager.get_node(sdd_2.id());
  assert!(!node.is_trimmed(&manager));
@@ -135,7 +135,7 @@ mod sdd_test {
  let sdd = &Sdd::DecisionRegular(decision);
 
  let decisions = &vec![sdd];
- let manager = SddManager::new_with_nodes(SddOptions::new(), decisions);
+ let manager = SddManager::new_with_nodes(SddOptions::new(), decisions, None);
 
  // Decomposition {(A, true), (B, false)} is trimmed.
  let node = manager.get_node(sdd.id());
@@ -171,7 +171,7 @@ mod sdd_test {
  let sdd_2 = &Sdd::DecisionRegular(decision_2);
 
  let decisions = &vec![sdd_1, sdd_2];
- let manager = SddManager::new_with_nodes(SddOptions::new(), decisions);
+ let manager = SddManager::new_with_nodes(SddOptions::new(), decisions, None);
 
  let node = manager.get_node(sdd_2.id());
  assert!(node.is_trimmed(&manager));
@@ -186,4 +186,31 @@ mod sdd_test {
  fn compressed() {
  // TODO: Implement me!
  }
+
+ #[test]
+ fn sdd_hashing() {
+ let element_1 = Element {
+ prime: &boxed_literal(Polarity::Positive, "A"),
+ sub: &Sdd::True,
+ };
+
+ let element_2 = Element {
+ prime: &boxed_literal(Polarity::Negative, "A"),
+ sub: &Sdd::True,
+ };
+
+ let decision_1 = &Decision {
+ elements: btreeset!(&element_1),
+ };
+
+ let decision_2 = &Decision {
+ elements: btreeset!(&element_2),
+ };
+
+ assert!(
+ &Sdd::DecisionRegular(decision_1).id() == &Sdd::DecisionComplement(decision_1).id()
+ );
+
+ assert!(&Sdd::DecisionRegular(decision_1).id() != &Sdd::DecisionRegular(decision_2).id());
+ }
 }