Skip to content

Commit

Permalink
Support VariableId and &str as literals in bdd! macro via `Into…
Browse files Browse the repository at this point in the history
…Bdd` trait.
  • Loading branch information
daemontus committed Sep 1, 2021
1 parent 79ddaeb commit c818592
Show file tree
Hide file tree
Showing 3 changed files with 72 additions and 13 deletions.
53 changes: 52 additions & 1 deletion src/_macro_bdd.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
use crate::{Bdd, BddVariable, BddVariableSet, IntoBdd};
/// A macro for simplifying `Bdd` operations. It evaluates given expression over `Bdd`s where
/// you can use standard boolean operators `!`, `&`, `|`, `^`, `=>` and `<=>`.
///
Expand All @@ -9,8 +10,20 @@
/// See tutorial for usage examples.
#[macro_export]
macro_rules! bdd {
// Parenthesis elimination:
($vars:ident, ($($e:tt)*)) => { bdd!($vars, $($e)*) };
( ( $($e:tt)* ) ) => { bdd!($($e)*) };
( $bdd:ident ) => { $bdd };
// Literal resolution:
($vars:ident, $bdd:literal) => { $crate::IntoBdd::into_bdd($bdd, &$vars) };
($vars:ident, $bdd:ident) => { $crate::IntoBdd::into_bdd($bdd, &$vars) };
($bdd:ident) => { $bdd };
// Boolean operations:
($vars:ident, !$e:tt) => { bdd!($vars, $e).not() };
($vars:ident, $l:tt & $r:tt) => { bdd!($vars, $l).and(&bdd!($vars, $r)) };
($vars:ident, $l:tt | $r:tt) => { bdd!($vars, $l).or(&bdd!($vars, $r)) };
($vars:ident, $l:tt <=> $r:tt) => { bdd!($vars, $l).iff(&bdd!($vars, $r)) };
($vars:ident, $l:tt => $r:tt) => { bdd!($vars, $l).imp(&bdd!($vars, $r)) };
($vars:ident, $l:tt ^ $r:tt) => { bdd!($vars, $l).xor(&bdd!($vars, $r)) };
(!$e:tt) => { bdd!($e).not() };
($l:tt & $r:tt) => { bdd!($l).and(&bdd!($r)) };
($l:tt | $r:tt) => { bdd!($l).or(&bdd!($r)) };
Expand All @@ -19,6 +32,24 @@ macro_rules! bdd {
($l:tt ^ $r:tt) => { bdd!($l).xor(&bdd!($r)) };
}

impl IntoBdd for BddVariable {
fn into_bdd(self, variables: &BddVariableSet) -> Bdd {
variables.mk_var(self)
}
}

impl IntoBdd for Bdd {
fn into_bdd(self, _variables: &BddVariableSet) -> Bdd {
self
}
}

impl IntoBdd for &str {
fn into_bdd(self, variables: &BddVariableSet) -> Bdd {
variables.mk_var_by_name(self)
}
}

#[cfg(test)]
mod tests {
use super::super::*;
Expand All @@ -35,4 +66,24 @@ mod tests {
assert_eq!(v1.imp(&v2), bdd!(v1 => v2));
assert_eq!(v1.iff(&v2), bdd!(v1 <=> v2));
}

#[test]
fn bdd_macro_advanced() {
let mut builder = BddVariableSetBuilder::new();
let [a, b, c] = builder.make(&["a", "b", "c"]);
let variables = builder.build();
let bdd_a = variables.mk_var(a);
let bdd_b = variables.mk_var(b);
let bdd_c = variables.mk_var(c);

crate::_macro_bdd::IntoBdd::into_bdd(a, &variables);

let with_objects = bdd!((bdd_a <=> (!bdd_b)) | (bdd_c ^ bdd_a));
let with_variables = bdd!(variables, (a <=> (!b)) | (c ^ a));
let with_literals = bdd!(variables, ("a" <=> (!"b")) | ("c" ^ "a"));

assert_eq!(with_objects, with_variables);
assert_eq!(with_variables, with_literals);
assert_eq!(with_literals, with_objects);
}
}
6 changes: 6 additions & 0 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -203,3 +203,9 @@ struct BddNode {
pub low_link: BddPointer,
pub high_link: BddPointer,
}

/// A trait which allows quick conversion of a type into a `Bdd`, assuming an appropriate
/// `BddVariablesSet` is provided.
pub trait IntoBdd {
fn into_bdd(self, variables: &BddVariableSet) -> Bdd;
}
26 changes: 14 additions & 12 deletions src/tutorial/p03_bdd_manipulation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -56,30 +56,32 @@
//!
//! ## `bdd` macro
//!
//! When using expressions, you can't reuse existing `Bdd`s - secifically, expressions are
//! When using expressions, you can't reuse existing `Bdd`s - specifically, expressions are
//! awesome when creating small, self contained examples but don't work very well if you need
//! to pass `Bdd`s around and manipulate them.
//!
//! For this, you can use the `bdd` macro. Unfortunately, rust macro system is a bit more strict,
//! hence macros are not as permissive as expressions, but they still allow a fair amount of
//! succintness.
//! succinctness.
//!
//! The main difference compared to expressions is that in a macro, every operator (even `!`) must
//! be properly parenthesised (except the very top of the expression). On the other hand,
//! be properly parenthesised (except for the root of the expression). On the other hand,
//! you are no longer limited to variable names as atoms,
//! you can use any `Bdd` object in the current scope:
//! you can use any `Bdd` object in the current scope. Furthermore, if you specify
//! a `BddVariableSet`, you can also use ony `BddVariable`, or even `&str` (which will be
//! interpreted as a variable name).
//!
//! ```rust
//! use biodivine_lib_bdd::{BddVariableSet, bdd};
//! use biodivine_lib_bdd::{BddVariableSet, bdd, BddVariableSetBuilder};
//!
//! let variables = BddVariableSet::new(vec!["a", "b", "c"]);
//!
//! let a = variables.mk_var_by_name("a");
//! let b = variables.mk_var_by_name("b");
//! let c = variables.mk_var_by_name("c");
//! let mut builder = BddVariableSetBuilder::new();
//! let [a, b, c] = builder.make(&["a", "b", "c"]);
//! let variables = builder.build();
//!
//! let f1 = bdd!(a & ((!b) => (c ^ a)));
//! let f2 = bdd!((b | (a ^ c)) & a);
//! // Mixed usage of `BddVariable` and `&str` to create literals.
//! let f1 = bdd!(variables, a & ((!"b") => ("c" ^ a)));
//! let f2 = bdd!(variables, (b | ("a" ^ c)) & "a");
//! // If all literals are `Bdd` objects, you can omit the `BddVariableSet`.
//! let eq = bdd!(f1 <=> f2);
//!
//! assert_eq!(variables.mk_true(), eq);
Expand Down

0 comments on commit c818592

Please sign in to comment.