From cca72bb0d77d0391077644ad09c3d2f04606fb2c Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Fri, 23 Aug 2024 10:01:37 +0200 Subject: [PATCH 1/8] Enhance documentation --- src/command_line/arguments.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/command_line/arguments.rs b/src/command_line/arguments.rs index d8227542..1cbfcb9d 100644 --- a/src/command_line/arguments.rs +++ b/src/command_line/arguments.rs @@ -62,7 +62,7 @@ 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, From 820faedb8a0094556c49847084e346ab5b09fa6c Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Fri, 23 Aug 2024 10:15:32 +0200 Subject: [PATCH 2/8] Add CLI options to customize the number of prover instances and cores --- src/command_line/arguments.rs | 8 ++++++++ src/command_line/procedures.rs | 2 ++ 2 files changed, 10 insertions(+) diff --git a/src/command_line/arguments.rs b/src/command_line/arguments.rs index 1cbfcb9d..219136a7 100644 --- a/src/command_line/arguments.rs +++ b/src/command_line/arguments.rs @@ -66,6 +66,14 @@ pub enum Command { #[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, diff --git a/src/command_line/procedures.rs b/src/command_line/procedures.rs index 7a53b562..bcb2ebb9 100644 --- a/src/command_line/procedures.rs +++ b/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, } => { From c4d17da406253e9d45ef7691e74a1538c33793e7 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Sat, 24 Aug 2024 15:13:52 +0200 Subject: [PATCH 3/8] Pass the number cores to vampire --- src/command_line/procedures.rs | 6 +++++- src/verifying/prover/vampire.rs | 3 +++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/command_line/procedures.rs b/src/command_line/procedures.rs index bcb2ebb9..31349d53 100644 --- a/src/command_line/procedures.rs +++ b/src/command_line/procedures.rs @@ -143,7 +143,11 @@ pub fn main() -> Result<()> { let mut success = true; for problem in problems { // TODO: Handle the error cases properly - let report = Vampire { time_limit }.prove(problem)?; + let report = Vampire { + time_limit, + cores: prover_cores, + } + .prove(problem)?; if !matches!(report.status()?, Status::Success(Success::Theorem)) { success = false; } diff --git a/src/verifying/prover/vampire.rs b/src/verifying/prover/vampire.rs index cf618daa..f6caa695 100644 --- a/src/verifying/prover/vampire.rs +++ b/src/verifying/prover/vampire.rs @@ -79,6 +79,7 @@ impl Display for VampireReport { pub struct Vampire { pub time_limit: usize, + pub cores: usize, } impl Prover for Vampire { @@ -92,6 +93,8 @@ impl Prover for Vampire { "casc", "--time_limit", &self.time_limit.to_string(), + "--cores", + &self.cores.to_string(), ]) .stdin(Stdio::piped()) .stdout(Stdio::piped()) From f523cb0091254819c66fb178bc49166908c81c38 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Sat, 24 Aug 2024 15:42:20 +0200 Subject: [PATCH 4/8] Add a prove_all method to the Prover trait --- src/verifying/prover/mod.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/verifying/prover/mod.rs b/src/verifying/prover/mod.rs index 93cf123d..6efa8b18 100644 --- a/src/verifying/prover/mod.rs +++ b/src/verifying/prover/mod.rs @@ -96,4 +96,11 @@ pub trait Prover { type Error; fn prove(&self, problem: Problem) -> Result; + + fn prove_all( + &self, + problems: impl IntoIterator, + ) -> impl IntoIterator> { + problems.into_iter().map(|problem| self.prove(problem)) + } } From 4d61c85aa84a9064649fcd85a5f0e3552ef16d62 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Sat, 24 Aug 2024 15:42:39 +0200 Subject: [PATCH 5/8] Use prove_all in the command line procedures --- src/command_line/procedures.rs | 66 +++++++++++++++++++++++++++------- 1 file changed, 53 insertions(+), 13 deletions(-) diff --git a/src/command_line/procedures.rs b/src/command_line/procedures.rs index 31349d53..0ad28fc6 100644 --- a/src/command_line/procedures.rs +++ b/src/command_line/procedures.rs @@ -140,25 +140,65 @@ pub fn main() -> Result<()> { } if !no_proof_search { - let mut success = true; - for problem in problems { - // TODO: Handle the error cases properly - let report = Vampire { - time_limit, - cores: prover_cores, + let prover = Vampire { + time_limit, + 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); } - .prove(problem)?; - if !matches!(report.status()?, Status::Success(Success::Theorem)) { - success = false; + println!(); + }); + + let mut success = true; + 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 {} 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.") } } From 0ae4b1079835d5bab9b30b039b2d8680f69cad76 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Sat, 24 Aug 2024 15:48:26 +0200 Subject: [PATCH 6/8] Determine the number of instances and cores to use if 0 are requested --- Cargo.lock | 17 +++++++++++++++++ Cargo.toml | 1 + src/command_line/procedures.rs | 1 + src/verifying/prover/mod.rs | 4 ++++ src/verifying/prover/vampire.rs | 19 ++++++++++++++++++- 5 files changed, 41 insertions(+), 1 deletion(-) diff --git a/Cargo.lock b/Cargo.lock index 77692fe2..fa6668c7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -72,6 +72,7 @@ dependencies = [ "indexmap", "itertools", "lazy_static", + "num_cpus", "pest", "pest_derive", "petgraph", @@ -286,6 +287,12 @@ version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" +[[package]] +name = "hermit-abi" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d231dfb89cfffdbc30e7fc41579ed6066ad03abda9e567ccafae602b97ec5024" + [[package]] name = "indexmap" version = "2.4.0" @@ -329,6 +336,16 @@ version = "2.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" +[[package]] +name = "num_cpus" +version = "1.16.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4161fcb6d602d4d2081af7c3a45852d875a03dd337a6bfdd6e06407b61342a43" +dependencies = [ + "hermit-abi", + "libc", +] + [[package]] name = "once_cell" version = "1.19.0" diff --git a/Cargo.toml b/Cargo.toml index d1ccca34..9ad3efe6 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -20,6 +20,7 @@ either = "1" indexmap = "2" itertools = "0.13" lazy_static = "1" +num_cpus = "1" pest = "2" pest_derive = "2" petgraph = "0.6" diff --git a/src/command_line/procedures.rs b/src/command_line/procedures.rs index 0ad28fc6..482dd0f1 100644 --- a/src/command_line/procedures.rs +++ b/src/command_line/procedures.rs @@ -142,6 +142,7 @@ pub fn main() -> Result<()> { if !no_proof_search { let prover = Vampire { time_limit, + instances: prover_instances, cores: prover_cores, }; diff --git a/src/verifying/prover/mod.rs b/src/verifying/prover/mod.rs index 6efa8b18..d53a8dfa 100644 --- a/src/verifying/prover/mod.rs +++ b/src/verifying/prover/mod.rs @@ -95,6 +95,10 @@ pub trait Prover { type Report: Report; type Error; + fn instances(&self) -> usize; + + fn cores(&self) -> usize; + fn prove(&self, problem: Problem) -> Result; fn prove_all( diff --git a/src/verifying/prover/vampire.rs b/src/verifying/prover/vampire.rs index f6caa695..1324ecb5 100644 --- a/src/verifying/prover/vampire.rs +++ b/src/verifying/prover/vampire.rs @@ -79,6 +79,7 @@ impl Display for VampireReport { pub struct Vampire { pub time_limit: usize, + pub instances: usize, pub cores: usize, } @@ -86,6 +87,22 @@ 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 { let mut child = Command::new("vampire") .args([ @@ -94,7 +111,7 @@ impl Prover for Vampire { "--time_limit", &self.time_limit.to_string(), "--cores", - &self.cores.to_string(), + &self.cores().to_string(), ]) .stdin(Stdio::piped()) .stdout(Stdio::piped()) From 31ae0eb7591a557021603e59c9ab8da0aa063e90 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Sat, 24 Aug 2024 16:40:11 +0200 Subject: [PATCH 7/8] Run multiple prover instances simultaneously --- Cargo.lock | 10 +++++++++ Cargo.toml | 1 + src/verifying/prover/mod.rs | 36 +++++++++++++++++++++++++++------ src/verifying/prover/vampire.rs | 1 + 4 files changed, 42 insertions(+), 6 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index fa6668c7..732d5cd7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -78,6 +78,7 @@ dependencies = [ "petgraph", "regex", "thiserror", + "threadpool", "walkdir", ] @@ -564,6 +565,15 @@ dependencies = [ "syn", ] +[[package]] +name = "threadpool" +version = "1.8.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d050e60b33d41c19108b32cea32164033a9013fe3b46cbd4457559bfbf77afaa" +dependencies = [ + "num_cpus", +] + [[package]] name = "typenum" version = "1.17.0" diff --git a/Cargo.toml b/Cargo.toml index 9ad3efe6..3f86f3cd 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -26,6 +26,7 @@ pest_derive = "2" petgraph = "0.6" regex = "1" thiserror = "1" +threadpool = "1" walkdir = "2" [dev-dependencies] diff --git a/src/verifying/prover/mod.rs b/src/verifying/prover/mod.rs index d53a8dfa..7300fb88 100644 --- a/src/verifying/prover/mod.rs +++ b/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; } -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, - ) -> impl IntoIterator> { - problems.into_iter().map(|problem| self.prove(problem)) + problems: impl IntoIterator + 'static, + ) -> Box>> { + 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()) + } } } diff --git a/src/verifying/prover/vampire.rs b/src/verifying/prover/vampire.rs index 1324ecb5..80627723 100644 --- a/src/verifying/prover/vampire.rs +++ b/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, From 914e5b761637738c8c5b3b9decaec266b35297d5 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Sat, 24 Aug 2024 18:03:22 +0200 Subject: [PATCH 8/8] cargo clippy --fix --- src/command_line/procedures.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/command_line/procedures.rs b/src/command_line/procedures.rs index 482dd0f1..d4be68e6 100644 --- a/src/command_line/procedures.rs +++ b/src/command_line/procedures.rs @@ -188,7 +188,7 @@ pub fn main() -> Result<()> { } }, Err(error) => { - println!("> Proving {} ended with an error", ""); // TODO: Get the name of the problem + println!("> Proving ended with an error"); // TODO: Get the name of the problem println!("Error: {error}"); success = false; }