diff --git a/src/_macro_bdd.rs b/src/_macro_bdd.rs index b9a74ed..712dda6 100644 --- a/src/_macro_bdd.rs +++ b/src/_macro_bdd.rs @@ -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 `<=>`. /// @@ -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)) }; @@ -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::*; @@ -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); + } } diff --git a/src/lib.rs b/src/lib.rs index 3835807..7b90238 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -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; +} diff --git a/src/tutorial/p03_bdd_manipulation.rs b/src/tutorial/p03_bdd_manipulation.rs index 75b3cdb..b409701 100644 --- a/src/tutorial/p03_bdd_manipulation.rs +++ b/src/tutorial/p03_bdd_manipulation.rs @@ -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);