patrick/ask-dracula-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Show Vampire proof times

Browse Source
This commit is contained in:
Patrick Lühne 2019-11-06 19:05:15 -06:00
parent fa2110294a
commit 39a047e10a
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
1 changed files with 18 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
src/main.rs
View File

@ -63,7 +63,7 @@ enum ProofResult
}
fn run_vampire<I, S>(input: &str, arguments: Option<I>)
-> Result<ProofResult, ask_dracula::Error>
-> Result<(ProofResult, Option<f32>), ask_dracula::Error>
where I: IntoIterator<Item = S>, S: AsRef<std::ffi::OsStr>
{
let mut vampire = std::process::Command::new("vampire");
@ -106,18 +106,24 @@ fn run_vampire<I, S>(input: &str, arguments: Option<I>)
if proof_not_found_regex.is_match(stdout)
{
return Ok(ProofResult::ProofNotFound);
return Ok((ProofResult::ProofNotFound, None));
}
return Err(ask_dracula::Error::new_run_vampire(
format!("Vampire returned unsuccessful exit code ({})\n\n======== stdout ========\n{}\n\n======== stderr ========\n{}", output.status, std::str::from_utf8(&output.stdout).unwrap_or("(not valid UTF-8)").trim(), std::str::from_utf8(&output.stderr).unwrap_or("(not valid UTF-8)").trim())));
}
let proof_time_regex = regex::Regex::new(r"% \(\d+\)Success in time (\d+(?:\.\d+)?) s").unwrap();
let proof_time = proof_time_regex.captures(stdout)
.map(|captures| captures.get(1).unwrap().as_str().parse::<f32>().ok())
.unwrap_or(None);
let refutation_regex = regex::Regex::new(r"% \(\d+\)Termination reason: Refutation").unwrap();
if refutation_regex.is_match(stdout)
{
return Ok(ProofResult::Refutation);
return Ok((ProofResult::Refutation, proof_time));
}
Err(ask_dracula::Error::new_interpret_vampire_output(stdout.to_string(), stderr.to_string()))
@ -155,7 +161,7 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
{
let conjecture = find_conjecture(&project, proof_direction);
let vampire_result = match conjecture
let (vampire_result, proof_time) = match conjecture
{
None =>
{
@ -183,7 +189,14 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
},
ProofResult::Refutation =>
{
println!("assertion proven");
if let Some(proof_time) = proof_time
{
println!("assertion proven in {} seconds", proof_time);
}
else
{
println!("assertion proven");
}
conjecture.kind = ask_dracula::project::StatementKind::Axiom;
conjecture.original_text = replace_statement_kind_regex.replace(&conjecture.original_text, "axiom").to_string();