Run multiple prover instances simultaneously

Cargo.toml

@@ -26,6 +26,7 @@ pest_derive = "2"
 petgraph = "0.6"
 regex = "1"
 thiserror = "1"
+threadpool = "1"
 walkdir = "2"
 
 [dev-dependencies]

src/verifying/prover/mod.rs

@@ -5,8 +5,10 @@ use {
     std::{
         fmt::{Debug, Display},
         str::FromStr,
+        sync::mpsc::channel,
     },
     thiserror::Error,
+    threadpool::ThreadPool,
 };
 
 pub mod vampire;
@@ -91,9 +93,9 @@ pub trait Report: Display + Debug + Clone {
     fn status(&self) -> Result<Status, StatusExtractionError>;
 }
 
-pub trait Prover {
-    type Report: Report;
-    type Error;
+pub trait Prover: Debug + Clone + Send + 'static {
+    type Report: Report + Send;
+    type Error: Send;
 
     fn instances(&self) -> usize;
 
@@ -103,8 +105,30 @@ pub trait Prover {
 
     fn prove_all(
         &self,
-        problems: impl IntoIterator<Item = Problem>,
-    ) -> impl IntoIterator<Item = Result<Self::Report, Self::Error>> {
-        problems.into_iter().map(|problem| self.prove(problem))
+        problems: impl IntoIterator<Item = Problem> + 'static,
+    ) -> Box<dyn Iterator<Item = Result<Self::Report, Self::Error>>> {
+        if self.instances() == 1 {
+            let prover = self.clone();
+            Box::new(
+                problems
+                    .into_iter()
+                    .map(move |problem| prover.prove(problem)),
+            )
+        } else {
+            let pool = ThreadPool::new(self.instances());
+            let (tx, rx) = channel();
+
+            for problem in problems {
+                let prover = self.clone();
+                let tx = tx.clone();
+
+                pool.execute(move || {
+                    let result = prover.prove(problem);
+                    tx.send(result).unwrap();
+                })
+            }
+
+            Box::new(rx.into_iter())
+        }
     }
 }

src/verifying/prover/vampire.rs

@@ -77,6 +77,7 @@ impl Display for VampireReport {
     }
 }
 
+#[derive(Debug, Clone)]
 pub struct Vampire {
     pub time_limit: usize,
     pub instances: usize,