From c6f112b4ed207c90201904c2d1741e5db3602f5b Mon Sep 17 00:00:00 2001 From: Stefan Ellmauthaler Date: Tue, 26 Jul 2022 10:55:05 +0200 Subject: [PATCH] Add crossbeam-channel to represent an output-stream of stable models Uses a crossbeam-channel to fill a Queue, which can be used safely from outside the function. This rework is done to also allow ad-hoc output of results in a potentially multi-threaded setup. --- Cargo.lock | 11 +++++++++ lib/Cargo.toml | 1 + lib/src/adf.rs | 66 ++++++++++++++++++++++++++++++++++++++++---------- 3 files changed, 65 insertions(+), 13 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index de26c5e..9e7db04 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -7,6 +7,7 @@ name = "adf_bdd" version = "0.2.5" dependencies = [ "biodivine-lib-bdd", + "crossbeam-channel", "derivative", "env_logger 0.9.0", "lexical-sort", @@ -182,6 +183,16 @@ dependencies = [ "os_str_bytes", ] +[[package]] +name = "crossbeam-channel" +version = "0.5.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c2dd04ddaf88237dc3b8d8f9a3c1004b506b54b3313403944054d23c0870c521" +dependencies = [ + "cfg-if", + "crossbeam-utils", +] + [[package]] name = "crossbeam-utils" version = "0.8.7" diff --git a/lib/Cargo.toml b/lib/Cargo.toml index d13c6cb..ad05d20 100644 --- a/lib/Cargo.toml +++ b/lib/Cargo.toml @@ -32,6 +32,7 @@ biodivine-lib-bdd = "0.4.0" derivative = "2.2.0" roaring = "0.9.0" strum = { version = "0.24", features = ["derive"] } +crossbeam-channel = "0.5" [dev-dependencies] test-log = "0.2" diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 837910c..c466709 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -6,9 +6,6 @@ This module describes the abstract dialectical framework. */ pub mod heuristics; - -use serde::{Deserialize, Serialize}; - use crate::{ datatypes::{ adf::{ @@ -21,6 +18,7 @@ use crate::{ obdd::Bdd, parser::{AdfParser, Formula}, }; +use serde::{Deserialize, Serialize}; use self::heuristics::Heuristic; @@ -729,7 +727,7 @@ impl Adf { .collect::>() } - /// Computes the stable extensions of a given [`Adf`], using the [`NoGood`]-learner + /// Computes the stable extensions of a given [`Adf`], using the [`NoGood`]-learner. pub fn stable_nogood<'a, 'c>( &'a mut self, heuristic: Heuristic, @@ -739,14 +737,43 @@ impl Adf { { let grounded = self.grounded(); let heu = heuristic.get_heuristic(); - self.stable_nogood_internal(&grounded, heu).into_iter() + let (s, r) = crossbeam_channel::unbounded::>(); + self.stable_nogood_get_vec(&grounded, heu, s, r).into_iter() } - fn stable_nogood_internal(&mut self, interpretation: &[Term], heuristic: H) -> Vec> + /// Computes the stable extension of a given [`Adf`], using the [`NoGood`]-learner. + /// Needs a [`Sender`][crossbeam_channel::Sender>] where the results of the computation can be put to. + pub fn stable_nogood_channel( + &mut self, + heuristic: Heuristic, + sender: crossbeam_channel::Sender>, + ) { + let grounded = self.grounded(); + self.stable_nogood_internal(&grounded, heuristic.get_heuristic(), sender); + } + + fn stable_nogood_get_vec( + &mut self, + interpretation: &[Term], + heuristic: H, + s: crossbeam_channel::Sender>, + r: crossbeam_channel::Receiver>, + ) -> Vec> where H: Fn(&Self, &[Term]) -> Option<(Var, Term)>, { - let mut result = Vec::new(); + self.stable_nogood_internal(interpretation, heuristic, s); + r.iter().collect() + } + + fn stable_nogood_internal( + &mut self, + interpretation: &[Term], + heuristic: H, + s: crossbeam_channel::Sender>, + ) where + H: Fn(&Self, &[Term]) -> Option<(Var, Term)>, + { let mut cur_interpr = interpretation.to_vec(); let mut ng_store = NoGoodStore::new( self.ac @@ -843,7 +870,8 @@ impl Adf { } else if self.stability_check(&cur_interpr) { // stable model found stack.push((false, cur_interpr.as_slice().into())); - result.push(cur_interpr.clone()); + s.send(cur_interpr.clone()) + .expect("Sender should accept results"); backtrack = true; } else { // not stable @@ -855,13 +883,13 @@ impl Adf { } log::info!("{ng_store}"); log::debug!("{:?}", ng_store); - result } } #[cfg(test)] mod test { use super::*; + use crossbeam_channel::unbounded; use test_log::test; #[test] @@ -1050,10 +1078,11 @@ mod test { let mut adf = Adf::from_parser(&parser); let grounded = adf.grounded(); - let stable = adf.stable_nogood_internal(&grounded, crate::adf::heuristics::heu_simple); + let (s, r) = unbounded(); + adf.stable_nogood_internal(&grounded, crate::adf::heuristics::heu_simple, s); assert_eq!( - stable, + r.iter().collect::>(), vec![vec![ Term::TOP, Term::BOT, @@ -1081,8 +1110,13 @@ mod test { parser.parse()("s(a).s(b).ac(a,neg(b)).ac(b,neg(a)).").unwrap(); let mut adf = Adf::from_parser(&parser); let grounded = adf.grounded(); - let stable = adf.stable_nogood_internal(&grounded, crate::adf::heuristics::heu_simple); - assert_eq!(stable, vec![vec![Term(1), Term(0)], vec![Term(0), Term(1)]]); + let (s, r) = unbounded(); + adf.stable_nogood_internal(&grounded, crate::adf::heuristics::heu_simple, s.clone()); + let stable_result = r.try_iter().collect::>(); + assert_eq!( + stable_result, + vec![vec![Term(1), Term(0)], vec![Term(0), Term(1)]] + ); let stable = adf.stable_nogood(Heuristic::Simple); assert_eq!( @@ -1102,6 +1136,12 @@ mod test { stable.collect::>(), vec![vec![Term(0), Term(1)], vec![Term(1), Term(0)]] ); + + adf.stable_nogood_channel(Heuristic::Simple, s); + assert_eq!( + r.iter().collect::>(), + vec![vec![Term(1), Term(0)], vec![Term(0), Term(1)]] + ); } #[test]