Add test-case to show multi-threaded use of the ng solver

Added a bit of documentation on this new feature on the module-page

lib/src/adf.rs

@@ -1142,6 +1142,44 @@ mod test {
             r.iter().collect::<Vec<_>>(),
             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]

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(