Skip to content

Commit

Permalink
Merge pull request #44 from timbeurskens/feature/argparser
Browse files Browse the repository at this point in the history
Move to derived argument parsing to simplify CLI
  • Loading branch information
timbeurskens authored Aug 13, 2022
2 parents c2e8f8e + b983cc8 commit 0a9c9e8
Show file tree
Hide file tree
Showing 4 changed files with 264 additions and 87 deletions.
189 changes: 156 additions & 33 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

8 changes: 5 additions & 3 deletions Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,16 +1,18 @@
[package]
name = "rsbdd"
version = "0.9.3"
version = "0.10.0"
edition = "2021"
authors = ["Tim Beurskens <[email protected]>"]
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"
regex = "1.6.0"
csv = "1.1.6"
rand = "0.8.5"
rustc-hash = "1.1.0"
40 changes: 34 additions & 6 deletions src/bdd.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {}

Expand Down Expand Up @@ -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<Self, Self::Err> {
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 {
Expand Down Expand Up @@ -515,11 +545,9 @@ impl<S: BDDSymbol> BDDEnv<S> {

// simplify removes a choice node if both subtrees are equivalent
pub fn simplify(&self, a: &Rc<BDD<S>>) -> Rc<BDD<S>> {
let result = match a.as_ref() {
&BDD::Choice(ref t, _, ref f) if t.as_ref() == f.as_ref() => t,
_ => a,
};

Rc::clone(result)
match a.as_ref() {
&BDD::Choice(ref t, _, ref f) if t.as_ref() == f.as_ref() => Rc::clone(t),
_ => Rc::clone(a),
}
}
}
Loading

0 comments on commit 0a9c9e8

Please sign in to comment.