From 4e399641d697df507652a53527ad4bd2df3c72ca Mon Sep 17 00:00:00 2001
From: Tobias Stolzmann <tobias.stolzmann@potassco.com>
Date: Fri, 23 Aug 2024 09:35:38 +0200
Subject: [PATCH] Add an option to pass a time limit to vampire

---
 src/command_line/arguments.rs   |  4 ++++
 src/command_line/procedures.rs  |  3 ++-
 src/verifying/prover/vampire.rs | 11 +++++++++--
 3 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/src/command_line/arguments.rs b/src/command_line/arguments.rs
index 6a39f919..d8227542 100644
--- a/src/command_line/arguments.rs
+++ b/src/command_line/arguments.rs
@@ -62,6 +62,10 @@ pub enum Command {
         #[arg(long, action)]
         no_proof_search: bool,
 
+        /// The time limit in seconds to prove each conjecture passed to an ATP
+        #[arg(long, short, default_value_t = 60)]
+        time_limit: usize,
+
         /// The destination directory for the problem files
         #[arg(long)]
         save_problems: Option<PathBuf>,
diff --git a/src/command_line/procedures.rs b/src/command_line/procedures.rs
index 815535f1..7a53b562 100644
--- a/src/command_line/procedures.rs
+++ b/src/command_line/procedures.rs
@@ -71,6 +71,7 @@ pub fn main() -> Result<()> {
             no_simplify,
             no_eq_break,
             no_proof_search,
+            time_limit,
             save_problems: out_dir,
             files,
         } => {
@@ -140,7 +141,7 @@ pub fn main() -> Result<()> {
                 let mut success = true;
                 for problem in problems {
                     // TODO: Handle the error cases properly
-                    let report = Vampire.prove(problem)?;
+                    let report = Vampire { time_limit }.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 ad98a691..cf618daa 100644
--- a/src/verifying/prover/vampire.rs
+++ b/src/verifying/prover/vampire.rs
@@ -77,7 +77,9 @@ impl Display for VampireReport {
     }
 }
 
-pub struct Vampire;
+pub struct Vampire {
+    pub time_limit: usize,
+}
 
 impl Prover for Vampire {
     type Error = VampireError;
@@ -85,7 +87,12 @@ impl Prover for Vampire {
 
     fn prove(&self, problem: Problem) -> Result<Self::Report, Self::Error> {
         let mut child = Command::new("vampire")
-            .args(["--mode", "casc"])
+            .args([
+                "--mode",
+                "casc",
+                "--time_limit",
+                &self.time_limit.to_string(),
+            ])
             .stdin(Stdio::piped())
             .stdout(Stdio::piped())
             .stderr(Stdio::piped())