diff --git a/Cargo.lock b/Cargo.lock index 9020db4..93655cb 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -21,7 +21,7 @@ dependencies = [ [[package]] name = "adf_bdd" -version = "0.3.0" +version = "0.3.1" dependencies = [ "biodivine-lib-bdd", "crossbeam-channel", diff --git a/bin/Cargo.toml b/bin/Cargo.toml index b52a669..c019462 100644 --- a/bin/Cargo.toml +++ b/bin/Cargo.toml @@ -16,7 +16,7 @@ name = "adf-bdd" path = "src/main.rs" [dependencies] -adf_bdd = { version="0.3.0", path="../lib", default-features = false } +adf_bdd = { version="0.3.1", path="../lib", default-features = false } clap = {version = "3.2.16", features = [ "derive", "cargo", "env" ]} log = { version = "0.4", features = [ "max_level_trace", "release_max_level_info" ] } serde = { version = "1.0", features = ["derive","rc"] } @@ -31,10 +31,11 @@ predicates = "2.1" assert_fs = "1.0" [features] -default = ["adhoccounting", "variablelist", "adf_bdd/default" ] +default = ["adhoccounting", "variablelist", "adf_bdd/default", "frontend"] adhoccounting = ["adf_bdd/adhoccounting"] # count models ad-hoc - disable if counting is not needed importexport = ["adf_bdd/importexport"] variablelist = [ "HashSet", "adf_bdd/variablelist" ] HashSet = ["adf_bdd/HashSet"] adhoccountmodels = ["adf_bdd/adhoccountmodels"] -benchmark = ["adf_bdd/benchmark"] \ No newline at end of file +benchmark = ["adf_bdd/benchmark"] +frontend = ["adf_bdd/frontend"] \ No newline at end of file diff --git a/lib/Cargo.toml b/lib/Cargo.toml index 5147496..0eccff8 100644 --- a/lib/Cargo.toml +++ b/lib/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "adf_bdd" -version = "0.3.0" +version = "0.3.1" authors = ["Stefan Ellmauthaler "] edition = "2021" homepage = "https://ellmau.github.io/adf-obdd/" @@ -42,10 +42,11 @@ quickcheck = "1" quickcheck_macros = "1" [features] -default = ["adhoccounting", "variablelist" ] +default = ["adhoccounting", "variablelist", "frontend" ] adhoccounting = [] # count paths ad-hoc - disable if counting is not needed importexport = [] variablelist = [ "HashSet" ] HashSet = [] adhoccountmodels = [ "adhoccounting" ] # count models as well as paths ad-hoc note that facet methods will need this feature too benchmark = ["adhoccounting", "variablelist"] # set of features for speed benchmarks +frontend = [] \ No newline at end of file diff --git a/lib/src/datatypes/bdd.rs b/lib/src/datatypes/bdd.rs index 5324b03..4eb3161 100644 --- a/lib/src/datatypes/bdd.rs +++ b/lib/src/datatypes/bdd.rs @@ -145,7 +145,7 @@ impl Var { /// Intuitively this is a binary tree structure, where the diagram is allowed to /// pool same values to the same Node. #[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy, Serialize, Deserialize)] -pub(crate) struct BddNode { +pub struct BddNode { var: Var, lo: Term, hi: Term, @@ -157,6 +157,12 @@ impl Display for BddNode { } } +impl Default for BddNode { + fn default() -> Self { + Self::top_node() + } +} + impl BddNode { /// Creates a new Node. pub fn new(var: Var, lo: Term, hi: Term) -> Self { diff --git a/lib/src/obdd.rs b/lib/src/obdd.rs index 10acea2..d349202 100644 --- a/lib/src/obdd.rs +++ b/lib/src/obdd.rs @@ -1,5 +1,7 @@ //! Module which represents obdds. //! +#[cfg(feature = "frontend")] +pub mod frontend; pub mod vectorize; use crate::datatypes::*; use serde::{Deserialize, Serialize}; @@ -19,6 +21,12 @@ pub struct Bdd { cache: HashMap, #[serde(skip, default = "Bdd::default_count_cache")] count_cache: RefCell>, + #[cfg(feature = "frontend")] + #[serde(skip)] + sender: Option>, + #[cfg(feature = "frontend")] + #[serde(skip)] + receiver: Option>, #[serde(skip)] ite_cache: HashMap<(Term, Term, Term), Term>, #[serde(skip)] @@ -42,7 +50,7 @@ impl Default for Bdd { } impl Bdd { - /// Instantiate a new roBDD structures. + /// Instantiate a new roBDD structure. /// Constants for the [`⊤`][crate::datatypes::Term::TOP] and [`⊥`][crate::datatypes::Term::BOT] concepts are prepared in that step too. pub fn new() -> Self { #[cfg(not(feature = "adhoccounting"))] @@ -53,6 +61,10 @@ impl Bdd { var_deps: vec![HashSet::new(), HashSet::new()], cache: HashMap::new(), count_cache: RefCell::new(HashMap::new()), + #[cfg(feature = "frontend")] + sender: None, + #[cfg(feature = "frontend")] + receiver: None, ite_cache: HashMap::new(), restrict_cache: HashMap::new(), } @@ -65,6 +77,10 @@ impl Bdd { var_deps: vec![HashSet::new(), HashSet::new()], cache: HashMap::new(), count_cache: RefCell::new(HashMap::new()), + #[cfg(feature = "frontend")] + sender: None, + #[cfg(feature = "frontend")] + receiver: None, ite_cache: HashMap::new(), restrict_cache: HashMap::new(), }; @@ -264,6 +280,15 @@ impl Bdd { let new_term = Term(self.nodes.len()); self.nodes.push(node); self.cache.insert(node, new_term); + #[cfg(feature = "frontend")] + if let Some(send) = &self.sender { + match send.send(node) { + Ok(_) => log::trace!("Sent {node} to the channel."), + Err(e) => { + log::error!("Error {e} occurred when sending {node} to {:?}", send) + } + } + } #[cfg(feature = "variablelist")] { let mut var_set: HashSet = self.var_deps[lo.value()] diff --git a/lib/src/obdd/frontend.rs b/lib/src/obdd/frontend.rs new file mode 100644 index 0000000..4bc1381 --- /dev/null +++ b/lib/src/obdd/frontend.rs @@ -0,0 +1,266 @@ +//! Implementation of frontend-feature related methods and functions +//! See the Structs in the [obdd-module][super] for most of the implementations + +use crate::datatypes::Term; + +use super::BddNode; +impl super::Bdd { + /// Instantiate a new [roBDD][super::Bdd] structure. + /// Constants for the [`⊤`][crate::datatypes::Term::TOP] and [`⊥`][crate::datatypes::Term::BOT] concepts are prepared in that step too. + /// # Attention + /// Constants for [`⊤`][crate::datatypes::Term::TOP] and [`⊥`][crate::datatypes::Term::BOT] concepts are not sent, as they are considered to be existing in every [Bdd][super::Bdd] structure. + pub fn with_sender(sender: crossbeam_channel::Sender) -> Self { + // TODO nicer handling of the initialisation though overhead is not an issue here + let mut result = Self::new(); + result.set_sender(sender); + result + } + + /// Instantiate a new [roBDD][super::Bdd] structure. + /// Constants for the [`⊤`][crate::datatypes::Term::TOP] and [`⊥`][crate::datatypes::Term::BOT] concepts are prepared in that step too. + /// # Attention + /// Note that mixing manipulating operations and utilising the communication channel for a receiving [roBDD][super::Bdd] may end up in inconsistent data. + /// So far, only manipulate the [roBDD][super::Bdd] if no further [recv][Self::recv] will be called. + pub fn with_receiver(receiver: crossbeam_channel::Receiver) -> Self { + // TODO nicer handling of the initialisation though overhead is not an issue here + let mut result = Self::new(); + result.set_receiver(receiver); + result + } + + /// Instantiate a new [roBDD][super::Bdd] structure. + /// Constants for the [`⊤`][crate::datatypes::Term::TOP] and [`⊥`][crate::datatypes::Term::BOT] concepts are prepared in that step too. + /// # Attention + /// - Constants for [`⊤`][crate::datatypes::Term::TOP] and [`⊥`][crate::datatypes::Term::BOT] concepts are not sent, as they are considered to be existing in every [Bdd][super::Bdd] structure. + /// - Mixing manipulating operations and utilising the communication channel for a receiving [roBDD][super::Bdd] may end up in inconsistent data. + /// So far, only manipulate the [roBDD][super::Bdd] if no further [recv][Self::recv] will be called. + pub fn with_sender_receiver( + sender: crossbeam_channel::Sender, + receiver: crossbeam_channel::Receiver, + ) -> Self { + let mut result = Self::new(); + result.set_receiver(receiver); + result.set_sender(sender); + result + } + + /// Updates the currently used [sender][crossbeam_channel::Sender] + pub fn set_sender(&mut self, sender: crossbeam_channel::Sender) { + self.sender = Some(sender); + } + + /// Updates the currently used [receiver][crossbeam_channel::Receiver] + pub fn set_receiver(&mut self, receiver: crossbeam_channel::Receiver) { + self.receiver = Some(receiver); + } + + /// Receives all information till the looked for [`Term`][crate::datatypes::Term] is either found or all data is read. + /// Note that the values are read, consumed, and added to the [Bdd][super::Bdd]. + /// # Returns + /// - [`true`] if the [term][crate::datatypes::Term] is found (either in the [Bdd][super::Bdd] or in the channel. + /// - [`false`] if neither the [Bdd][super::Bdd] nor the channel contains the [term][crate::datatypes::Term]. + pub fn recv(&mut self, term: Term) -> bool { + if term.value() < self.nodes.len() { + true + } else if let Some(recv) = &self.receiver { + loop { + match recv.try_recv() { + Ok(node) => { + let new_term = Term(self.nodes.len()); + self.nodes.push(node); + self.cache.insert(node, new_term); + if let Some(send) = &self.sender { + match send.send(node) { + Ok(_) => log::trace!("Sent {node} to the channel."), + Err(e) => { + log::error!( + "Error {e} occurred when sending {node} to {:?}", + send + ) + } + } + } + if new_term == term { + return true; + } + } + Err(_) => return false, + } + } + } else { + false + } + } +} + +#[cfg(test)] +mod test { + use super::super::*; + + #[test] + fn get_bdd_updates() { + let (send, recv) = crossbeam_channel::unbounded(); + let mut bdd = Bdd::with_sender(send); + + let solving = std::thread::spawn(move || { + let v1 = bdd.variable(Var(0)); + let v2 = bdd.variable(Var(1)); + + assert_eq!(v1, Term(2)); + assert_eq!(v2, Term(3)); + + let t1 = bdd.and(v1, v2); + let nt1 = bdd.not(t1); + let ft = bdd.or(v1, nt1); + + assert_eq!(ft, Term::TOP); + + let v3 = bdd.variable(Var(2)); + let nv3 = bdd.not(v3); + assert_eq!(bdd.and(v3, nv3), Term::BOT); + + let conj = bdd.and(v1, v2); + assert_eq!(bdd.restrict(conj, Var(0), false), Term::BOT); + assert_eq!(bdd.restrict(conj, Var(0), true), v2); + + let a = bdd.and(v3, v2); + let b = bdd.or(v2, v1); + + let con1 = bdd.and(a, conj); + + let end = bdd.or(con1, b); + log::debug!("Restrict test: restrict({},{},false)", end, Var(1)); + let x = bdd.restrict(end, Var(1), false); + assert_eq!(x, Term(2)); + }); + + let updates: Vec = recv.iter().collect(); + assert_eq!( + updates, + vec![ + BddNode::new(Var(0), Term(0), Term(1)), + BddNode::new(Var(1), Term(0), Term(1)), + BddNode::new(Var(0), Term(0), Term(3)), + BddNode::new(Var(1), Term(1), Term(0)), + BddNode::new(Var(0), Term(1), Term(5)), + BddNode::new(Var(2), Term(0), Term(1)), + BddNode::new(Var(2), Term(1), Term(0)), + BddNode::new(Var(1), Term(0), Term(7)), + BddNode::new(Var(0), Term(3), Term(1)), + BddNode::new(Var(0), Term(0), Term(9)), + ] + ); + solving.join().expect("Both threads should terminate"); + } + + #[test] + fn recv_send() { + let (send1, recv1) = crossbeam_channel::unbounded(); + let (send2, recv2) = crossbeam_channel::unbounded(); + let mut bdd1 = Bdd::with_sender(send1); + let mut bddm = Bdd::with_sender_receiver(send2, recv1); + let mut bddl = Bdd::with_receiver(recv2); + + let solving = std::thread::spawn(move || { + let v1 = bdd1.variable(Var(0)); + let v2 = bdd1.variable(Var(1)); + + assert_eq!(v1, Term(2)); + assert_eq!(v2, Term(3)); + + let t1 = bdd1.and(v1, v2); + let nt1 = bdd1.not(t1); + let ft = bdd1.or(v1, nt1); + + assert_eq!(ft, Term::TOP); + + let v3 = bdd1.variable(Var(2)); + let nv3 = bdd1.not(v3); + assert_eq!(bdd1.and(v3, nv3), Term::BOT); + + let conj = bdd1.and(v1, v2); + assert_eq!(bdd1.restrict(conj, Var(0), false), Term::BOT); + assert_eq!(bdd1.restrict(conj, Var(0), true), v2); + + let a = bdd1.and(v3, v2); + let b = bdd1.or(v2, v1); + + let con1 = bdd1.and(a, conj); + + let end = bdd1.or(con1, b); + log::debug!("Restrict test: restrict({},{},false)", end, Var(1)); + let x = bdd1.restrict(end, Var(1), false); + assert_eq!(x, Term(2)); + }); + // allow the worker to fill the channels + std::thread::sleep(std::time::Duration::from_millis(10)); + // both are initialised, no updates so far + assert_eq!(bddm.nodes, bddl.nodes); + // receiving a truth constant should work without changing the bdd + assert!(bddm.recv(Term::TOP)); + assert_eq!(bddm.nodes, bddl.nodes); + // receiving some element works for middle -> last, but not last -> middle + assert!(bddm.recv(Term(2))); + assert!(bddl.recv(Term(2))); + assert_eq!(bddl.nodes.len(), 3); + assert!(!bddl.recv(Term(5))); + // get all elements into middle bdd1 + assert!(!bddm.recv(Term(usize::MAX))); + + assert_eq!( + bddm.nodes, + vec![ + BddNode::bot_node(), + BddNode::top_node(), + BddNode::new(Var(0), Term(0), Term(1)), + BddNode::new(Var(1), Term(0), Term(1)), + BddNode::new(Var(0), Term(0), Term(3)), + BddNode::new(Var(1), Term(1), Term(0)), + BddNode::new(Var(0), Term(1), Term(5)), + BddNode::new(Var(2), Term(0), Term(1)), + BddNode::new(Var(2), Term(1), Term(0)), + BddNode::new(Var(1), Term(0), Term(7)), + BddNode::new(Var(0), Term(3), Term(1)), + BddNode::new(Var(0), Term(0), Term(9)), + ] + ); + + // last bdd is still in the previous state + assert_eq!( + bddl.nodes, + vec![ + BddNode::bot_node(), + BddNode::top_node(), + BddNode::new(Var(0), Term(0), Term(1)), + ] + ); + + // and now catch up till 10 + assert!(bddl.recv(Term(10))); + + assert_eq!( + bddl.nodes, + vec![ + BddNode::bot_node(), + BddNode::top_node(), + BddNode::new(Var(0), Term(0), Term(1)), + BddNode::new(Var(1), Term(0), Term(1)), + BddNode::new(Var(0), Term(0), Term(3)), + BddNode::new(Var(1), Term(1), Term(0)), + BddNode::new(Var(0), Term(1), Term(5)), + BddNode::new(Var(2), Term(0), Term(1)), + BddNode::new(Var(2), Term(1), Term(0)), + BddNode::new(Var(1), Term(0), Term(7)), + BddNode::new(Var(0), Term(3), Term(1)), + ] + ); + + solving.join().expect("Both threads should terminate"); + + // asking for 10 again works too + assert!(bddl.recv(Term(10))); + // fully catch up with the last bdd + assert!(bddl.recv(Term(11))); + assert_eq!(bddl.nodes, bddm.nodes); + } +}