diff --git a/Cargo.lock b/Cargo.lock index c04deae..aef79e4 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -218,7 +218,7 @@ checksum = "f497285884f3fcff424ffc933e56d7cbca511def0c9831a7f9b5f6153e3cc89b" [[package]] name = "rsbdd" -version = "0.6.6" +version = "0.7.0" dependencies = [ "clap", "csv", diff --git a/Cargo.toml b/Cargo.toml index 568b09b..6d93f9f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "rsbdd" -version = "0.6.6" +version = "0.7.0" edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html diff --git a/src/bdd.rs b/src/bdd.rs index 72e4d0c..2981d6d 100644 --- a/src/bdd.rs +++ b/src/bdd.rs @@ -89,6 +89,16 @@ pub enum TruthTableEntry { Any, } +impl Display for TruthTableEntry { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.pad(match self { + TruthTableEntry::True => "True", + TruthTableEntry::False => "False", + TruthTableEntry::Any => "Any", + }) + } +} + impl Default for BDD { fn default() -> Self { BDD::False diff --git a/src/main.rs b/src/main.rs index 0771dcc..e7ff4cd 100644 --- a/src/main.rs +++ b/src/main.rs @@ -3,6 +3,7 @@ use rsbdd::bdd_io::*; use rsbdd::parser::*; use rsbdd::parser_io::*; use rsbdd::plot::*; +use std::cmp::max; use std::fs::File; use std::io; use std::io::{BufRead, BufReader}; @@ -93,8 +94,24 @@ fn main() { _ => TruthTableEntry::Any, }; + let widths: Vec = input_parsed + .free_vars + .iter() + .map(|v| max(5, v.len()) as usize) + .collect(); + if args.is_present("show_truth_table") { - println!("{:?}", input_parsed.free_vars); + print!("|"); + for free_var in &input_parsed.free_vars { + let len = 1 + max(5, free_var.len()); + print!(" {:indent$}|", free_var, indent = len); + } + println!(); + for width in &widths { + print!("|{:->width$}", "", width = *width + 2); + } + println!("|"); + // println!("{:?}", input_parsed.free_vars.join("|")); print_truth_table_recursive( &result, input_parsed @@ -104,6 +121,7 @@ fn main() { .collect(), filter, &input_parsed, + &widths, ); } @@ -191,6 +209,7 @@ fn plot_performance_results(results: &[Duration]) { .expect("Could not wait for gnuplot to finish"); } +// print all variables which can take a 'true' value in the bdd fn print_true_vars_recursive( root: &Rc>, values: Vec, @@ -230,24 +249,29 @@ fn print_truth_table_recursive( vars: Vec, filter: TruthTableEntry, parsed: &ParsedFormula, + sizes: &[usize], ) { match root.as_ref() { BDD::Choice(ref l, s, ref r) => { // first visit the false subtree let mut r_vars = vars.clone(); r_vars[parsed.to_free_index(s)] = TruthTableEntry::False; - print_truth_table_recursive(r, r_vars, filter, parsed); + print_truth_table_recursive(r, r_vars, filter, parsed, sizes); // then visit the true subtree let mut l_vars = vars; l_vars[parsed.to_free_index(s)] = TruthTableEntry::True; - print_truth_table_recursive(l, l_vars, filter, parsed); + print_truth_table_recursive(l, l_vars, filter, parsed, sizes); } c if (filter == TruthTableEntry::Any) || (filter == TruthTableEntry::True && *c == BDD::True) || (filter == TruthTableEntry::False && *c == BDD::False) => { - println!("{:?} {:?}", vars, c) + print!("|"); + for (i, var) in vars.iter().enumerate() { + print!(" {:indent$} |", var, indent = sizes[i]); + } + println!(" {:?}", c); } _ => {} }