Support multithreading

Cargo.toml

@@ -20,11 +20,13 @@ either = "1"
 indexmap = "2"
 itertools = "0.13"
 lazy_static = "1"
+num_cpus = "1"
 pest = "2"
 pest_derive = "2"
 petgraph = "0.6"
 regex = "1"
 thiserror = "1"
+threadpool = "1"
 walkdir = "2"
 
 [dev-dependencies]

src/command_line/arguments.rs

@@ -62,10 +62,18 @@ pub enum Command {
         #[arg(long, action)]
         no_proof_search: bool,
 
-        /// The time limit in seconds to prove each conjecture passed to an ATP
+        /// The time limit in seconds to prove each problem passed to a prover
         #[arg(long, short, default_value_t = 60)]
         time_limit: usize,
 
+        /// The number of prover instances to spawn
+        #[arg(long, short = 'n', default_value_t = 1)]
+        prover_instances: usize,
+
+        /// The number of threads each prover may use
+        #[arg(long, short = 'm', default_value_t = 1)]
+        prover_cores: usize,
+
         /// The destination directory for the problem files
         #[arg(long)]
         save_problems: Option<PathBuf>,

src/command_line/procedures.rs

@@ -72,6 +72,8 @@ pub fn main() -> Result<()> {
             no_eq_break,
             no_proof_search,
             time_limit,
+            prover_instances,
+            prover_cores,
             save_problems: out_dir,
             files,
         } => {
@@ -138,21 +140,66 @@ pub fn main() -> Result<()> {
             }
 
             if !no_proof_search {
+                let prover = Vampire {
+                    time_limit,
+                    instances: prover_instances,
+                    cores: prover_cores,
+                };
+
+                let problems = problems.into_iter().inspect(|problem| {
+                    println!("> Proving {}...", problem.name);
+                    println!("Axioms:");
+                    for axiom in problem.axioms() {
+                        println!("    {}", axiom.formula);
+                    }
+                    println!();
+                    println!("Conjectures:");
+                    for conjecture in problem.conjectures() {
+                        println!("    {}", conjecture.formula);
+                    }
+                    println!();
+                });
+
                 let mut success = true;
-                for problem in problems {
-                    // TODO: Handle the error cases properly
-                    let report = Vampire { time_limit }.prove(problem)?;
-                    if !matches!(report.status()?, Status::Success(Success::Theorem)) {
-                        success = false;
+                for result in prover.prove_all(problems) {
+                    match result {
+                        Ok(report) => match report.status() {
+                            Ok(status) => {
+                                println!(
+                                    "> Proving {} ended with a SZS status",
+                                    report.problem.name
+                                );
+                                println!("Status: {status}");
+                                if !matches!(status, Status::Success(Success::Theorem)) {
+                                    success = false;
+                                }
+                            }
+                            Err(error) => {
+                                println!(
+                                    "> Proving {} ended without a SZS status",
+                                    report.problem.name
+                                );
+                                println!("Output/stdout:");
+                                println!("{}", report.output.stdout);
+                                println!("Output/stderr:");
+                                println!("{}", report.output.stderr);
+                                println!("Error: {error}");
+                                success = false;
+                            }
+                        },
+                        Err(error) => {
+                            println!("> Proving <a problem> ended with an error"); // TODO: Get the name of the problem
+                            println!("Error: {error}");
+                            success = false;
+                        }
                     }
-                    println!("{report}");
+                    println!();
                 }
 
-                println!("--- Summary ---");
                 if success {
-                    println!("Success! Anthem found a proof of equivalence.");
+                    println!("> Success! Anthem found a proof of equivalence.")
                 } else {
-                    println!("Failure! Anthem was unable to find a proof of equivalence.");
+                    println!("> Failure! Anthem was unable to find a proof of equivalence.")
                 }
             }
 

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,42 @@ 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;
+
+    fn cores(&self) -> usize;
 
     fn prove(&self, problem: Problem) -> Result<Self::Report, Self::Error>;
+
+    fn prove_all(
+        &self,
+        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,21 +77,42 @@ impl Display for VampireReport {
     }
 }
 
+#[derive(Debug, Clone)]
 pub struct Vampire {
     pub time_limit: usize,
+    pub instances: usize,
+    pub cores: usize,
 }
 
 impl Prover for Vampire {
     type Error = VampireError;
     type Report = VampireReport;
 
+    fn instances(&self) -> usize {
+        if self.instances == 0 {
+            std::cmp::max(num_cpus::get() / self.cores(), 1)
+        } else {
+            self.instances
+        }
+    }
+
+    fn cores(&self) -> usize {
+        if self.cores == 0 {
+            num_cpus::get()
+        } else {
+            self.cores
+        }
+    }
+
     fn prove(&self, problem: Problem) -> Result<Self::Report, Self::Error> {
         let mut child = Command::new("vampire")
             .args([
                 "--mode",
                 "casc",
                 "--time_limit",
                 &self.time_limit.to_string(),
+                "--cores",
+                &self.cores().to_string(),
             ])
             .stdin(Stdio::piped())
             .stdout(Stdio::piped())