From b983cc8e378f9888a5f051714a1d52399d97d703 Mon Sep 17 00:00:00 2001 From: Tim Beurskens Date: Sat, 13 Aug 2022 15:07:40 +0200 Subject: [PATCH] implement fromstr for argument parsing of TruthTableEntry --- Cargo.lock | 14 +++++++------- Cargo.toml | 4 ++-- src/bdd.rs | 30 ++++++++++++++++++++++++++++++ src/main.rs | 14 ++++---------- 4 files changed, 43 insertions(+), 19 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index e228865..27ed992 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -190,9 +190,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.126" +version = "0.2.131" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "349d5a591cd28b49e1d1037471617a32ddcda5731b99419008085f72d5a53836" +checksum = "04c3b4822ccebfa39c02fc03d1534441b22ead323fa0f48bb7ddd8e6ba076a40" [[package]] name = "memchr" @@ -315,7 +315,7 @@ checksum = "a3f87b73ce11b1619a3c6332f45341e0047173771e8b8b73f87bfeefb7b56244" [[package]] name = "rsbdd" -version = "0.9.3" +version = "0.10.0" dependencies = [ "clap", "csv", @@ -335,15 +335,15 @@ checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2" [[package]] name = "ryu" -version = "1.0.10" +version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f3f6f92acf49d1b98f7a81226834412ada05458b7364277387724a237f062695" +checksum = "4501abdff3ae82a1c1b477a17252eb69cee9e66eb915c1abaa4f44d873df9f09" [[package]] name = "serde" -version = "1.0.140" +version = "1.0.143" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fc855a42c7967b7c369eb5860f7164ef1f6f81c20c7cc1141f2a604e18723b03" +checksum = "53e8e5d5b70924f74ff5c6d64d9a5acd91422117c60f48c4e07855238a254553" [[package]] name = "strsim" diff --git a/Cargo.toml b/Cargo.toml index a82bff8..233426a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "rsbdd" -version = "0.9.3" +version = "0.10.0" edition = "2021" authors = ["Tim Beurskens "] description = "A BDD-based SAT solver" @@ -12,7 +12,7 @@ dot = "0.1.4" itertools = "0.10.3" clap = { version = "3.2.17", features = ["derive"] } lazy_static = "1.4.0" -regex = "1" +regex = "1.6.0" csv = "1.1.6" rand = "0.8.5" rustc-hash = "1.1.0" diff --git a/src/bdd.rs b/src/bdd.rs index 6fcaef4..640be36 100644 --- a/src/bdd.rs +++ b/src/bdd.rs @@ -2,10 +2,12 @@ use itertools::Itertools; use rustc_hash::FxHashMap; use std::cell::RefCell; use std::collections::hash_map::DefaultHasher; +use std::error::Error; use std::fmt; use std::fmt::{Debug, Display}; use std::hash::{Hash, Hasher}; use std::rc::Rc; +use std::str::FromStr; pub trait BDDSymbol: Ord + Display + Debug + Clone + Hash {} @@ -89,6 +91,34 @@ pub enum TruthTableEntry { Any, } +#[derive(Debug)] +pub struct TruthTableEntryParseError { + pub input: String, +} + +impl Error for TruthTableEntryParseError {} + +impl Display for TruthTableEntryParseError { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "Could not parse truth table entry: {}", self.input) + } +} + +impl FromStr for TruthTableEntry { + type Err = TruthTableEntryParseError; + + fn from_str(s: &str) -> Result { + match s { + "true" | "True" | "t" | "T" | "1" => Ok(TruthTableEntry::True), + "false" | "False" | "f" | "F" | "0" => Ok(TruthTableEntry::False), + "any" | "Any" | "a" | "A" => Ok(TruthTableEntry::Any), + _ => Err(TruthTableEntryParseError { + input: s.to_string(), + }), + } + } +} + impl Display for TruthTableEntry { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { f.pad(match self { diff --git a/src/main.rs b/src/main.rs index 7e80d8a..3f770cf 100644 --- a/src/main.rs +++ b/src/main.rs @@ -41,8 +41,8 @@ struct Args { vars: bool, /// Only show true or false entries in the output. - #[clap(short, long, value_parser)] - filter: Option, + #[clap(short, long, value_parser, default_value_t = TruthTableEntry::Any)] + filter: TruthTableEntry, /// Repeat the solving process n times for more accurate performance reports. #[clap(short, long, value_parser, value_name = "N")] @@ -132,12 +132,6 @@ fn main() { result = input_parsed.env.borrow().model(result); } - 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, - }; - // show ordered variable list if args.export_ordering { @@ -185,7 +179,7 @@ fn main() { .iter() .map(|_| TruthTableEntry::Any) .collect(), - filter, + args.filter, &input_parsed, &widths, ); @@ -207,7 +201,7 @@ fn main() { 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); + let graph = BDDGraph::new(&result, args.filter); graph .render_dot(&mut f)