diff --git a/Cargo.lock b/Cargo.lock index 0c579a1..e228865 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -11,15 +11,6 @@ dependencies = [ "memchr", ] -[[package]] -name = "ansi_term" -version = "0.12.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d52a9bb7ec0cf484c551830a7ce27bd20d67eac647e1befb56b0be4ee39a55d2" -dependencies = [ - "winapi", -] - [[package]] name = "atty" version = "0.2.14" @@ -31,6 +22,12 @@ dependencies = [ "winapi", ] +[[package]] +name = "autocfg" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa" + [[package]] name = "bitflags" version = "1.3.2" @@ -57,17 +54,41 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "2.34.0" +version = "3.2.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a0610544180c38b88101fecf2dd634b174a62eef6946f84dfc6a7127512b381c" +checksum = "29e724a68d9319343bb3328c9cc2dfde263f4b3142ee1059a9980580171c954b" dependencies = [ - "ansi_term", "atty", "bitflags", + "clap_derive", + "clap_lex", + "indexmap", + "once_cell", "strsim", + "termcolor", "textwrap", - "unicode-width", - "vec_map", +] + +[[package]] +name = "clap_derive" +version = "3.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "13547f7012c01ab4a0e8f8967730ada8f9fdf419e8b6c792788f39cf4e46eefa" +dependencies = [ + "heck", + "proc-macro-error", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "clap_lex" +version = "0.2.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2850f2f5a82cbf437dd5af4d49848fbdfc27c157c3d010345776f952765261c5" +dependencies = [ + "os_str_bytes", ] [[package]] @@ -115,6 +136,18 @@ dependencies = [ "wasi", ] +[[package]] +name = "hashbrown" +version = "0.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" + +[[package]] +name = "heck" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2540771e65fc8cb83cd6e8a237f70c319bd5c29f78ed1084ba5d50eeac86f7f9" + [[package]] name = "hermit-abi" version = "0.1.19" @@ -124,6 +157,16 @@ dependencies = [ "libc", ] +[[package]] +name = "indexmap" +version = "1.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "10a35a97730320ffe8e2d410b5d3b69279b98d2c14bdb8b70ea89ecf7888d41e" +dependencies = [ + "autocfg", + "hashbrown", +] + [[package]] name = "itertools" version = "0.10.3" @@ -157,12 +200,66 @@ version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d" +[[package]] +name = "once_cell" +version = "1.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "18a6dbe30758c9f83eb00cbea4ac95966305f5a7772f3f42ebfc7fc7eddbd8e1" + +[[package]] +name = "os_str_bytes" +version = "6.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "648001efe5d5c0102d8cea768e348da85d90af8ba91f0bea908f157951493cd4" + [[package]] name = "ppv-lite86" version = "0.2.16" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "eb9f9e6e233e5c4a35559a617bf40a4ec447db2e84c20b55a6f83167b7e57872" +[[package]] +name = "proc-macro-error" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" +dependencies = [ + "proc-macro-error-attr", + "proc-macro2", + "quote", + "syn", + "version_check", +] + +[[package]] +name = "proc-macro-error-attr" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" +dependencies = [ + "proc-macro2", + "quote", + "version_check", +] + +[[package]] +name = "proc-macro2" +version = "1.0.43" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0a2ca2c61bc9f3d74d2886294ab7b9853abd9c1ad903a3ac7815c58989bb7bab" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bbe448f377a7d6961e30f5955f9b8d106c3f5e449d493ee1b125c1d43c2b5179" +dependencies = [ + "proc-macro2", +] + [[package]] name = "rand" version = "0.8.5" @@ -250,30 +347,47 @@ checksum = "fc855a42c7967b7c369eb5860f7164ef1f6f81c20c7cc1141f2a604e18723b03" [[package]] name = "strsim" -version = "0.8.0" +version = "0.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a" +checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623" [[package]] -name = "textwrap" -version = "0.11.0" +name = "syn" +version = "1.0.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d326610f408c7a4eb6f51c37c330e496b08506c9457c9d34287ecc38809fb060" +checksum = "58dbef6ec655055e20b86b15a8cc6d439cca19b667537ac6a1369572d151ab13" dependencies = [ - "unicode-width", + "proc-macro2", + "quote", + "unicode-ident", ] [[package]] -name = "unicode-width" -version = "0.1.9" +name = "termcolor" +version = "1.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bab24d30b911b2376f3a13cc2cd443142f0c81dda04c118693e35b3835757755" +dependencies = [ + "winapi-util", +] + +[[package]] +name = "textwrap" +version = "0.15.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b1141d4d61095b28419e22cb0bbf02755f5e54e0526f97f1e3d1d160e60885fb" + +[[package]] +name = "unicode-ident" +version = "1.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3ed742d4ea2bd1176e236172c8429aaf54486e7ac098db29ffe6529e0ce50973" +checksum = "c4f5b37a154999a8f3f98cc23a628d850e154479cd94decf3414696e12e31aaf" [[package]] -name = "vec_map" -version = "0.8.2" +name = "version_check" +version = "0.9.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191" +checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" [[package]] name = "wasi" @@ -297,6 +411,15 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" +[[package]] +name = "winapi-util" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "70ec6ce85bb158151cae5e5c87f95a8e97d2c0c4b001223f33a334e3ce5de178" +dependencies = [ + "winapi", +] + [[package]] name = "winapi-x86_64-pc-windows-gnu" version = "0.4.0" diff --git a/Cargo.toml b/Cargo.toml index 9fde54c..a82bff8 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -2,13 +2,15 @@ name = "rsbdd" version = "0.9.3" edition = "2021" +authors = ["Tim Beurskens <timbeurskens.97@gmail.com>"] +description = "A BDD-based SAT solver" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] dot = "0.1.4" itertools = "0.10.3" -clap = "2.33.3" +clap = { version = "3.2.17", features = ["derive"] } lazy_static = "1.4.0" regex = "1" csv = "1.1.6" diff --git a/src/main.rs b/src/main.rs index ad8a685..7e80d8a 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,3 +1,4 @@ +use clap::Parser; use rsbdd::bdd::*; use rsbdd::bdd_io::*; use rsbdd::parser::*; @@ -7,43 +8,72 @@ use std::cmp::max; use std::fs::File; use std::io; use std::io::{BufRead, BufReader}; +use std::path::PathBuf; use std::process::{Command, Stdio}; use std::rc::Rc; use std::time::{Duration, Instant}; -#[macro_use] -extern crate clap; +#[derive(Parser, Debug)] +#[clap(author, version, about, long_about = None)] +struct Args { + #[clap(value_parser, value_name = "FILE")] + /// The input file containing a logic formula in rsbdd format. + input: Option<PathBuf>, + + #[clap(short, long, value_parser)] + /// Write the parse tree in dot format to the specified file. + parsetree: Option<PathBuf>, + + #[clap(short, long)] + /// Print the truth table to stdout. + truthtable: bool, + + #[clap(short, long, value_parser)] + /// Write the bdd to a dot graphviz file. + dot: Option<PathBuf>, + + /// Compute a single satisfying model as output. + #[clap(short, long)] + model: bool, + + /// Print all satisfying variables leading to a truth value. + #[clap(short, long)] + vars: bool, + + /// Only show true or false entries in the output. + #[clap(short, long, value_parser)] + filter: Option<String>, + + /// Repeat the solving process n times for more accurate performance reports. + #[clap(short, long, value_parser, value_name = "N")] + benchmark: Option<usize>, + + /// Use GNUPlot to plot the runtime distribution. + #[clap(short = 'g', long)] + plot: bool, + + /// Parse the formula as string. + #[clap(short, long, value_parser)] + evaluate: Option<String>, + + /// Read a custom variable ordering from file. + #[clap(short, long, value_parser)] + ordering: Option<PathBuf>, + + /// Export the automatically derived ordering to stdout. + #[clap(short = 'r', long)] + export_ordering: bool, +} fn main() { - let args = clap_app!(Solver => - (version: env!("CARGO_PKG_VERSION")) - (author: "Tim Beurskens") - (about: "A BDD-based SAT solver") - (@arg input: -i --input +takes_value "logic input file") - (@arg show_parsetree: -p --parsetree +takes_value "write the parse tree in dot format to this file") - (@arg show_truth_table: -t --truthtable !takes_value "print the truth-table to stdout") - (@arg show_dot: -d --dot +takes_value "write the bdd to a dot graphviz file") - (@arg model: -m --model !takes_value "use a model of the bdd as output (instead of the satisfying assignment)") - (@arg vars: -v --vars !takes_value "print all true variables leading to a truth evaluation") - (@arg filter: -f --filter +takes_value "only show true or false entries in the truth-table") - (@arg benchmark: -b --benchmark +takes_value "Repeat the solving process n times for more accurate performance reports") - (@arg show_plot: -g --plot !takes_value "show a distribution plot of the runtime") - (@arg evaluate: -e --eval +takes_value "Inline evaluate the given formula") - (@arg ordering: -o --order +takes_value "Provide a custom variable ordering") - (@arg export_ordering: -r --ordering !takes_value "Print the variable ordering to stdout") - ) - .get_matches(); + let args = Args::parse(); - let repeat = args - .value_of("benchmark") - .unwrap_or("1") - .parse::<usize>() - .expect("Could not parse benchmark value as usize"); + let repeat = args.benchmark.unwrap_or(1); - let inline_eval = args.value_of("evaluate"); - let input_filename = args.value_of("input"); + let inline_eval = args.evaluate; + let input_filename = args.input; - let mut reader = if let Some(inline_str) = inline_eval { + let mut reader = if let Some(inline_str) = &inline_eval { Box::new(BufReader::new(inline_str.as_bytes())) as Box<dyn BufRead> } else if let Some(some_input_filename) = input_filename { let file = File::open(some_input_filename).expect("Could not open input file"); @@ -52,7 +82,7 @@ fn main() { Box::new(BufReader::new(io::stdin())) as Box<dyn BufRead> }; - let pre_variable_ordering = if let Some(ord_filename) = args.value_of("ordering") { + let pre_variable_ordering = if let Some(ord_filename) = args.ordering { let file = File::open(ord_filename).expect("Could not open variable ordering file"); let mut contents = Box::new(BufReader::new(file)) as Box<dyn BufRead>; let tokens = SymbolicBDD::tokenize(&mut contents, None) @@ -66,7 +96,7 @@ fn main() { let input_parsed = ParsedFormula::new(&mut reader, pre_variable_ordering).expect("Could not parse input file"); - if let Some(parsetree_filename) = args.value_of("show_parsetree") { + if let Some(parsetree_filename) = args.parsetree { let mut f = File::create(parsetree_filename).expect("Could not create parsetree dot file"); let graph = SymbolicParseTree::new(&input_parsed.bdd); @@ -89,20 +119,20 @@ fn main() { } // only print performance results when the benchmark flag is available, and more than 1 run has completed - if args.is_present("benchmark") && repeat > 0 { + if args.benchmark.is_some() && repeat > 0 { print_performance_results(&exec_times); - if args.is_present("show_plot") { + if args.plot { plot_performance_results(&exec_times); } } // reduce the bdd to a single path from root to a single 'true' node - if args.is_present("model") { + if args.model { result = input_parsed.env.borrow().model(result); } - let filter = match args.value_of("filter") { + let filter = match args.filter.as_deref() { Some("true" | "True" | "t" | "T" | "1") => TruthTableEntry::True, Some("false" | "False" | "f" | "F" | "0") => TruthTableEntry::False, _ => TruthTableEntry::Any, @@ -110,7 +140,7 @@ fn main() { // show ordered variable list - if args.is_present("export_ordering") { + if args.export_ordering { let mut ordered_variables = input_parsed.vars.clone(); ordered_variables.sort_by(|a, b| a.id.partial_cmp(&b.id).unwrap()); let ordered_variable_names = ordered_variables @@ -136,7 +166,7 @@ fn main() { let widths: Vec<usize> = headers.iter().map(|v| max(5, v.len()) as usize).collect(); - if args.is_present("show_truth_table") { + if args.truthtable { print!("|"); for free_var in &headers { let len = 1 + max(5, free_var.len()); @@ -161,7 +191,7 @@ fn main() { ); } - if args.is_present("vars") { + if args.vars { print_true_vars_recursive( &result, input_parsed @@ -174,7 +204,7 @@ fn main() { ); } - if let Some(dot_filename) = args.value_of("show_dot") { + if let Some(dot_filename) = args.dot { let mut f = File::create(dot_filename).expect("Could not create dot file"); let graph = BDDGraph::new(&result, filter);