diff --git a/lib/src/adf.rs b/lib/src/adf.rs index c466709..3678f0d 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -1142,6 +1142,44 @@ mod test { r.iter().collect::>(), vec![vec![Term(1), Term(0)], vec![Term(0), Term(1)]] ); + + // multi-threaded usage + let (s, r) = unbounded(); + let solving = std::thread::spawn(move || { + let parser = AdfParser::default(); + parser.parse()("s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,b).ac(c,and(a,b)).ac(d,neg(b)).\ns(e).ac(e,and(b,or(neg(b),c(f)))).s(f).\n\nac(f,xor(a,e)).") + .unwrap(); + let mut adf = Adf::from_parser(&parser); + adf.stable_nogood_channel(Heuristic::MinModMaxVarImpMinPaths, s.clone()); + adf.stable_nogood_channel(Heuristic::MinModMinPathsMaxVarImp, s); + }); + + let mut result_vec = Vec::new(); + while let Ok(result) = r.recv() { + result_vec.push(result); + } + assert_eq!( + result_vec, + vec![ + vec![ + Term::TOP, + Term::BOT, + Term::BOT, + Term::TOP, + Term::BOT, + Term::TOP + ], + vec![ + Term::TOP, + Term::BOT, + Term::BOT, + Term::TOP, + Term::BOT, + Term::TOP + ] + ] + ); + solving.join().unwrap(); } #[test] diff --git a/lib/src/lib.rs b/lib/src/lib.rs index 5fba465..f826d7c 100644 --- a/lib/src/lib.rs +++ b/lib/src/lib.rs @@ -159,6 +159,39 @@ let printer = adf.print_dictionary(); for model in adf.complete() { print!("{}", printer.print_interpretation(&model)); } +``` + +### Using the [`NoGood`]-learner approach, together with the [`crossbeam-channel`] implementation +This can be used to have a worker and a consumer thread to print the results as they are computed. +Please note that the [`NoGood`]-learner needs a heuristics function to work. +The enum [`Heuristic`][adf_bdd::adf::heuristics::Heuristic] allows one to choose a pre-defined heuristic, or implement a `Custom` one. +```rust +use adf_bdd::parser::AdfParser; +use adf_bdd::adf::Adf; +use adf_bdd::adf::heuristics::Heuristic; +use adf_bdd::datatypes::Term; +// create a channel +let (s, r) = crossbeam_channel::unbounded(); +// spawn a solver thread +let solving = std::thread::spawn(move || { + // use the above example as input + let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d)."; + let parser = AdfParser::default(); + parser.parse()(&input).expect("parsing worked well"); + // use hybrid approach + let mut adf = adf_bdd::adfbiodivine::Adf::from_parser(&parser).hybrid_step(); + // compute stable with the simple heuristic + adf.stable_nogood_channel(Heuristic::Simple, s); +}); + +// print results as they are computed +while let Ok(result) = r.recv() { + println!("stable model: {:?}", result); +# assert_eq!(result, vec![Term(1),Term(1),Term(0),Term(0)]); +} +// waiting for the other thread to close +solving.join().unwrap(); + ``` */ #![deny(