vtree: represent via Rc<RefCell>

sdd-rs-lib/dot_writer.rs

@@ -22,6 +22,8 @@ impl std::fmt::Display for Edge {
 
 #[derive(Default)]
 pub struct DotWriter {
+ graph_name: String,
+
  nodes: Vec<(usize, NodeType)>,
  edges: Vec<Edge>,
 }
@@ -61,8 +63,11 @@ impl NodeType {
 
 impl DotWriter {
  #[must_use]
- pub fn new() -> DotWriter {
- DotWriter::default()
+ pub fn new(graph_name: String) -> DotWriter {
+ DotWriter {
+ graph_name,
+ ..Default::default()
+ }
  }
 
  pub fn add_node(&mut self, node_idx: usize, node_type: NodeType) {
@@ -76,7 +81,7 @@ impl DotWriter {
  /// # Errors
  /// Function returns an error if the writing to a file or flushing fails.
  pub fn write(&self, writer: &mut dyn std::io::Write) -> Result<()> {
- write!(writer, "digraph sdd {{\n overlap=false")?;
+ write!(writer, "digraph {} {{\n overlap=false", self.graph_name)?;
 
  for (node, node_type) in &self.nodes {
  write!(

sdd-rs-lib/manager.rs

@@ -5,7 +5,7 @@ use crate::{
  literal::VarLabel,
  options::SddOptions,
  sdd::{Node, Sdd},
- vtree::{VTree, VTreeManager},
+ vtree::VTreeManager,
  Result,
 };
 
@@ -28,10 +28,10 @@ pub struct SddManager<'a> {
 
 impl<'a> SddManager<'a> {
  #[must_use]
- pub fn new(options: SddOptions, vtree: Option<VTree>) -> SddManager<'a> {
+ pub fn new(options: SddOptions) -> SddManager<'a> {
  SddManager {
  options,
- vtree_manager: VTreeManager::new(vtree),
+ vtree_manager: VTreeManager::new(),
  var_labels: HashSet::new(),
  unqiue_table: HashMap::new(),
  }
@@ -40,24 +40,24 @@ 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,
- sdds: &'a [&'a Sdd<'a>],
- vtree: Option<VTree>,
- ) -> SddManager<'a> {
+ 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(vtree),
+ vtree_manager: VTreeManager::new(),
  var_labels: HashSet::new(),
  unqiue_table: table,
  }
  }
 
+ pub fn add_variable(&mut self, variable: VarLabel) {
+ self.vtree_manager.add_variable(variable);
+ }
+
  pub fn tautology(&self) {}
  pub fn contradiction(&self) {}
 
@@ -81,7 +81,7 @@ impl<'a> SddManager<'a> {
  /// # Errors
  /// Returns an error if TBD.
  pub fn draw_sdd_graph(&self, writer: &mut dyn std::io::Write) -> Result<()> {
- let mut dot_writer = DotWriter::new();
+ let mut dot_writer = DotWriter::new(String::from("sdd"));
  for node in self.unqiue_table.values() {
  node.draw(&mut dot_writer);
  }
@@ -91,7 +91,7 @@ impl<'a> SddManager<'a> {
  /// # Errors
  /// Returns an error if TBD.
  pub fn draw_vtree_graph(&self, writer: &mut dyn std::io::Write) -> Result<()> {
- let mut dot_writer = DotWriter::new();
+ let mut dot_writer = DotWriter::new(String::from("vtree"));
  self.vtree_manager.draw(&mut dot_writer);
  dot_writer.write(writer)
  }

sdd-rs-lib/sdd.rs

@@ -7,10 +7,6 @@ use crate::{
  manager::SddManager,
 };
 
-#[cfg(test)]
-#[path = "./sdd_test.rs"]
-mod sdd_test;
-
 #[derive(PartialEq, Eq, Clone, Hash)]
 pub struct Node<'a> {
  decision: &'a Decision<'a>,
@@ -208,8 +204,8 @@ impl<'a> Sdd<'a> {
 
  fn dot_repr(&self) -> String {
  match self {
- Sdd::True => "⊤".to_owned(),
- Sdd::False => "⊥".to_owned(),
+ Sdd::True => String::from("⊤"),
+ Sdd::False => String::from("⊥"),
  Sdd::Literal(literal) => format!("{literal}"),
  _ => String::new(),
  }
@@ -299,3 +295,220 @@ impl<'a> Decision<'a> {
  todo!("Implement me!")
  }
 }
+
+#[cfg(test)]
+mod test {
+ use crate::{
+ btreeset,
+ literal::{Literal, Polarity, VarLabel},
+ options::SddOptions,
+ sdd::{Decision, Element, Sdd, SddManager},
+ };
+
+ fn boxed_literal<'a>(polarity: Polarity, var_label: &str) -> Sdd<'a> {
+ Sdd::Literal(Literal::new(polarity, VarLabel::new(var_label)))
+ }
+
+ #[test]
+ fn not_trimmed_simple() {
+ let element = Element {
+ prime: &Sdd::True,
+ sub: &Sdd::False,
+ };
+
+ // Decomposition `{(true, false)}`.
+ let decision = &Decision {
+ elements: btreeset!(&element),
+ };
+ let sdd = &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(sdd.id());
+ assert!(!node.is_trimmed(&manager));
+ }
+
+ #[test]
+ fn not_trimmed_simple_2() {
+ let element = Element {
+ prime: &Sdd::True,
+ sub: &boxed_literal(Polarity::Positive, "A"),
+ };
+
+ // Decomposition `{(true, A)}`.
+ let decision = &Decision {
+ elements: btreeset!(&element),
+ };
+ let sdd = &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(sdd.id());
+ assert!(!node.is_trimmed(&manager));
+ }
+
+ #[test]
+ fn not_trimmed_complex() {
+ 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::False,
+ };
+
+ // Decomposition `{(A, true), (!A, false)}`.
+ let decision = &Decision {
+ elements: btreeset!(&element_1, &element_2),
+ };
+ let sdd = &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(sdd.id());
+ assert!(!node.is_trimmed(&manager));
+ }
+
+ #[test]
+ fn not_trimmed_recursive() {
+ // Check that decomposition is recursivelly checked.
+ let element_1_1 = Element {
+ 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,
+ };
+
+ // 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 sdd_2 = &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(sdd_2.id());
+ assert!(!node.is_trimmed(&manager));
+ }
+
+ #[test]
+ fn trimmed_complex() {
+ let element_1 = Element {
+ prime: &boxed_literal(Polarity::Positive, "A"),
+ sub: &Sdd::True,
+ };
+ let element_2 = Element {
+ prime: &boxed_literal(Polarity::Positive, "A"),
+ sub: &Sdd::False,
+ };
+
+ // Decomposition `{(A, true), (B, false)}`.
+ let decision = &Decision {
+ elements: btreeset!(&element_1, &element_2),
+ };
+ let sdd = &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(sdd.id());
+ assert!(node.is_trimmed(&manager));
+ }
+
+ #[test]
+ fn trimmed_recursive() {
+ let element_1_1 = Element {
+ 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_1,
+ sub: &Sdd::False,
+ };
+
+ // 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 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));
+ }
+
+ #[test]
+ fn not_compressed() {
+ // TODO: Implement me!
+ }
+
+ #[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());
+ }
+}