adding timing information for each conjecture

potassco · Dec 11, 2024 · 40e1993 · 40e1993
1 parent d8e9a3f
commit 40e1993
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 4 deletions.
diff --git a/src/command_line/procedures.rs b/src/command_line/procedures.rs
@@ -150,6 +150,7 @@ pub fn main() -> Result<()> {
             if !no_proof_search {
                 let prover = Vampire {
                     time_limit,
+                    time_execution: !no_timing,
                     instances: prover_instances,
                     cores: prover_cores,
                 };
@@ -177,7 +178,12 @@ pub fn main() -> Result<()> {
                                     "> Proving {} ended with a SZS status",
                                     report.problem.name
                                 );
-                                println!("Status: {status}");
+                                match report.elapsed_time {
+                                    Some(duration) => {
+                                        println!("Status: {status} ({} ms)", duration.as_millis())
+                                    }
+                                    None => println!("Status: {status}"),
+                                };
                                 if !matches!(status, Status::Success(Success::Theorem)) {
                                     success = false;
                                 }

diff --git a/src/verifying/prover/vampire.rs b/src/verifying/prover/vampire.rs
@@ -7,6 +7,7 @@ use {
         fmt::{self, Display},
         io::Write as _,
         process::{Command, Output, Stdio},
+        time::{Duration, Instant},
     },
     thiserror::Error,
 };
@@ -45,6 +46,7 @@ impl TryFrom<Output> for VampireOutput {
 pub struct VampireReport {
     pub problem: Problem,
     pub output: VampireOutput,
+    pub elapsed_time: Option<Duration>,
 }
 
 impl Report for VampireReport {
@@ -71,15 +73,21 @@ impl Display for VampireReport {
         writeln!(f)?;
 
         match self.status() {
-            Ok(status) => writeln!(f, "status: {status}"),
-            Err(error) => writeln!(f, "error: {error}"),
+            Ok(status) => write!(f, "status: {status}")?,
+            Err(error) => write!(f, "error: {error}")?,
+        }
+
+        match self.elapsed_time {
+            Some(duration) => writeln!(f, "({} ms)", duration.as_millis()),
+            None => writeln!(f),
         }
     }
 }
 
 #[derive(Debug, Clone)]
 pub struct Vampire {
     pub time_limit: usize,
+    pub time_execution: bool,
     pub instances: usize,
     pub cores: usize,
 }
@@ -105,6 +113,12 @@ impl Prover for Vampire {
     }
 
     fn prove(&self, problem: Problem) -> Result<Self::Report, Self::Error> {
+        let start_time = if self.time_execution {
+            Some(Instant::now())
+        } else {
+            None
+        };
+
         let mut child = Command::new("vampire")
             .args([
                 "--mode",
@@ -129,6 +143,10 @@ impl Prover for Vampire {
             .map_err(VampireError::UnableToWait)?
             .try_into()?;
 
-        Ok(VampireReport { problem, output })
+        Ok(VampireReport {
+            problem,
+            output,
+            elapsed_time: start_time.map(|start| start.elapsed()),
+        })
     }
 }