diff --git a/src/serialize/ser_bdd.rs b/src/serialize/ser_bdd.rs index 6c3cb06b..023b0693 100644 --- a/src/serialize/ser_bdd.rs +++ b/src/serialize/ser_bdd.rs @@ -2,6 +2,8 @@ use std::collections::HashMap; +use petgraph::{dot::Dot, graph::NodeIndex, Graph}; + use crate::repr::{ bdd::{BddNode, BddPtr}, ddnnf::DDNNFPtr, @@ -78,4 +80,68 @@ impl BDDSerializer { roots: vec![r], } } + + pub fn to_dot(&self) -> String { + let mut graph = Graph::<_, _>::new(); + graph.add_node(String::from("F")); + graph.add_node(String::from("T")); + + for node in self.nodes.iter() { + graph.add_node(format!("{}", node.topvar + 1)); + } + + fn node_petgraph_index(ptr: &SerBDDPtr) -> NodeIndex { + match ptr { + SerBDDPtr::Ptr { index, compl: _ } => NodeIndex::new(index + 2), + SerBDDPtr::True => NodeIndex::new(1), + SerBDDPtr::False => NodeIndex::new(0), + } + } + + for (index, node) in self.nodes.iter().enumerate() { + graph.add_edge( + NodeIndex::new(index + 2), + node_petgraph_index(&node.low), + "low", + ); + graph.add_edge( + NodeIndex::new(index + 2), + node_petgraph_index(&node.high), + "high", + ); + } + + format!("{:?}", Dot::with_config(&graph, &[])) + } +} + +#[cfg(test)] +mod tests { + use crate::{ + builder::{ + bdd::{BddBuilder, RobddBuilder}, + cache::lru_app::BddApplyTable, + }, + repr::{bdd::BddPtr, cnf::Cnf}, + }; + + use super::BDDSerializer; + + #[test] + fn test_dot() { + static CNF: &str = " + p cnf 2 2 + 1 0 + 2 0 + "; + let cnf = Cnf::from_dimacs(CNF); + + let builder: RobddBuilder<'_, BddApplyTable>> = + RobddBuilder::>::new_default_order_lru(cnf.num_vars()); + let bdd = builder.compile_cnf(&cnf); + + let serialized = BDDSerializer::from_bdd(bdd); + + println!("{}", serialized.to_dot()); + } } diff --git a/src/serialize/ser_sdd.rs b/src/serialize/ser_sdd.rs index a4c34a51..544aa4e2 100644 --- a/src/serialize/ser_sdd.rs +++ b/src/serialize/ser_sdd.rs @@ -2,6 +2,8 @@ use std::collections::HashMap; +use petgraph::{Graph, graph::NodeIndex, dot::Dot}; + use crate::repr::sdd::SddPtr; #[derive(Clone, Copy, Debug, Serialize, Deserialize)] @@ -114,4 +116,27 @@ impl SDDSerializer { roots: vec![r], } } + + pub fn to_dot(&self) -> String { + let mut graph = Graph::<_, _>::new(); + graph.add_node(String::from("F")); + graph.add_node(String::from("T")); + + for node in self.nodes.iter() { + graph.add_node(String::from("hi")); + } + + fn node_petgraph_index(ptr: &SerSDDPtr) -> NodeIndex { + match ptr { + SerSDDPtr::True => NodeIndex::new(1), + SerSDDPtr::False => NodeIndex::new(0), + SerSDDPtr::Ptr { index, compl } => NodeIndex::new(index + 2), + SerSDDPtr::Literal { label, polarity } => todo!(), + } + } + + graph.add_edge(NodeIndex::new(0), NodeIndex::new(1), String::from("hi")); + + format!("{:?}", Dot::with_config(&graph, &[])) + } } diff --git a/src/serialize/ser_vtree.rs b/src/serialize/ser_vtree.rs index 1e6b0977..a40f45fa 100644 --- a/src/serialize/ser_vtree.rs +++ b/src/serialize/ser_vtree.rs @@ -42,6 +42,7 @@ //! ``` use crate::repr::vtree::VTree; +use petgraph::{dot::Dot, graph::NodeIndex, Graph}; #[derive(Clone, Debug, Serialize, Deserialize)] pub enum SerVTree { @@ -75,4 +76,47 @@ impl VTreeSerializer { let root = helper(vtree); VTreeSerializer { root: *root } } + + pub fn to_dot(&self) -> String { + let mut graph = Graph::<_, _>::new(); + + fn to_dot_helper(vtree: &SerVTree, graph: &mut Graph) -> NodeIndex { + match vtree { + SerVTree::Leaf(v) => graph.add_node(format!("{v}")), + SerVTree::Node { left, right } => { + let index = graph.add_node(String::from("")); + let left = to_dot_helper(left, graph); + let right = to_dot_helper(right, graph); + graph.add_edge(index, left, "left"); + graph.add_edge(index, right, "right"); + index + } + } + } + + to_dot_helper(&self.root, &mut graph); + + format!("{:?}", Dot::with_config(&graph, &[])) + } +} + +#[cfg(test)] +mod tests { + use crate::{ + repr::{var_label::VarLabel, vtree::VTree}, + serialize::VTreeSerializer, + }; + + #[test] + fn test_dot() { + let v0 = VarLabel::new_usize(0); + let v1 = VarLabel::new_usize(1); + let v2 = VarLabel::new_usize(2); + + let vtree = VTree::right_linear(&[v0, v1, v2]); + + let serialized = VTreeSerializer::from_vtree(&vtree); + + println!("{}", serialized.to_dot()); + } }