Add an option to pass a time limit to vampire

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>,

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;
                     }

src/verifying/prover/vampire.rs

@@ -77,15 +77,22 @@ impl Display for VampireReport {
     }
 }
 
-pub struct Vampire;
+pub struct Vampire {
+    pub time_limit: usize,
+}
 
 impl Prover for Vampire {
     type Error = VampireError;
     type Report = VampireReport;
 
     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())