226 lines
6.6 KiB
Rust
226 lines
6.6 KiB
Rust
fn backup_file_path(file_path: &std::path::Path) -> Result<std::path::PathBuf, ask_dracula::Error>
|
||
{
|
||
let file_name = file_path.file_name()
|
||
.ok_or(ask_dracula::Error::new_not_a_file(file_path.to_owned()))?;
|
||
|
||
let mut i = 0;
|
||
|
||
loop
|
||
{
|
||
i += 1;
|
||
|
||
let backup_file_name = format!("{}.{}~", file_name.to_string_lossy(), i);
|
||
let backup_file_path = file_path.with_file_name(backup_file_name);
|
||
|
||
if !backup_file_path.exists()
|
||
{
|
||
return Ok(backup_file_path);
|
||
}
|
||
}
|
||
}
|
||
|
||
fn find_conjecture<'a>(project: &'a ask_dracula::Project,
|
||
proof_direction: ask_dracula::format_tptp::ProofDirection)
|
||
-> Option<&'a ask_dracula::project::Statement>
|
||
{
|
||
for block in &project.blocks
|
||
{
|
||
if let ask_dracula::project::Block::Statement(ref statement) = block
|
||
{
|
||
if ask_dracula::format_tptp::is_statement_kind_conjecture(&statement.kind, proof_direction)
|
||
{
|
||
return Some(statement)
|
||
}
|
||
}
|
||
}
|
||
|
||
None
|
||
}
|
||
|
||
fn find_conjecture_mut<'a>(project: &'a mut ask_dracula::Project,
|
||
proof_direction: ask_dracula::format_tptp::ProofDirection)
|
||
-> Option<&'a mut ask_dracula::project::Statement>
|
||
{
|
||
for block in &mut project.blocks
|
||
{
|
||
if let ask_dracula::project::Block::Statement(ref mut statement) = block
|
||
{
|
||
if ask_dracula::format_tptp::is_statement_kind_conjecture(&statement.kind, proof_direction)
|
||
{
|
||
return Some(statement)
|
||
}
|
||
}
|
||
}
|
||
|
||
None
|
||
}
|
||
|
||
enum ProofResult
|
||
{
|
||
ProofNotFound,
|
||
Refutation,
|
||
Satisfiable,
|
||
}
|
||
|
||
fn run_vampire<I, S>(input: &str, arguments: Option<I>)
|
||
-> 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");
|
||
|
||
let vampire = match arguments
|
||
{
|
||
Some(arguments) => vampire.args(arguments),
|
||
None => &mut vampire,
|
||
};
|
||
|
||
//eprintln!("{}", input);
|
||
|
||
let mut vampire = vampire
|
||
.stdin(std::process::Stdio::piped())
|
||
.stdout(std::process::Stdio::piped())
|
||
.stderr(std::process::Stdio::piped())
|
||
.spawn()
|
||
.map_err(|error| ask_dracula::Error::new_run_vampire(error))?;
|
||
|
||
{
|
||
use std::io::Write;
|
||
|
||
let vampire_stdin = vampire.stdin.as_mut().unwrap();
|
||
vampire_stdin.write_all(input.as_bytes())
|
||
.map_err(|error| ask_dracula::Error::new_run_vampire(error))?;
|
||
}
|
||
|
||
let output = vampire.wait_with_output()
|
||
.map_err(|error| ask_dracula::Error::new_run_vampire(error))?;
|
||
|
||
let stdout = std::str::from_utf8(&output.stdout)
|
||
.map_err(|error| ask_dracula::Error::new_run_vampire(error))?;
|
||
|
||
let stderr = std::str::from_utf8(&output.stderr)
|
||
.map_err(|error| ask_dracula::Error::new_run_vampire(error))?;
|
||
|
||
if !output.status.success()
|
||
{
|
||
let proof_not_found_regex = regex::Regex::new(r"% \(\d+\)Proof not found in time").unwrap();
|
||
|
||
if proof_not_found_regex.is_match(stdout)
|
||
{
|
||
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, proof_time));
|
||
}
|
||
|
||
Err(ask_dracula::Error::new_interpret_vampire_output(stdout.to_string(), stderr.to_string()))
|
||
}
|
||
|
||
fn main() -> Result<(), Box<dyn std::error::Error>>
|
||
{
|
||
let matches = clap::App::new("Ask Dracula: Using Vampire as an interactive theorem prover")
|
||
.arg(clap::Arg::with_name("file").takes_value(true).required(true))
|
||
.arg(clap::Arg::with_name("proof-direction").long("proof-direction").takes_value(true).default_value("forward"))
|
||
.arg(clap::Arg::with_name("vampire_arguments").multiple(true))
|
||
.after_help("example: ask_dracula <project file> -- --mode casc --cores 8")
|
||
.get_matches();
|
||
|
||
let file = matches.value_of("file").unwrap().to_string();
|
||
let file_path = std::path::Path::new(&file);
|
||
|
||
let file_content = std::fs::read_to_string(&file_path)?;
|
||
let (_, mut project) = ask_dracula::parse::project(&file_content)
|
||
.map_err(|_| "couldn’t parse input file")?;
|
||
|
||
let replace_statement_kind_regex = regex::Regex::new(r"(assertion)").unwrap();
|
||
|
||
let proof_directions = match matches.value_of("proof-direction").unwrap()
|
||
{
|
||
"forward" => vec![ask_dracula::format_tptp::ProofDirection::Forward],
|
||
"backward" => vec![ask_dracula::format_tptp::ProofDirection::Backward],
|
||
"both" => vec![ask_dracula::format_tptp::ProofDirection::Forward, ask_dracula::format_tptp::ProofDirection::Backward],
|
||
proof_direction => panic!("unrecognized proof direction “{}”", proof_direction),
|
||
};
|
||
|
||
for proof_direction in proof_directions
|
||
{
|
||
loop
|
||
{
|
||
let conjecture = find_conjecture(&project, proof_direction);
|
||
|
||
let (vampire_result, proof_time) = match conjecture
|
||
{
|
||
None =>
|
||
{
|
||
eprintln!("nothing to prove, exiting");
|
||
return Ok(());
|
||
},
|
||
Some(ref conjecture) =>
|
||
{
|
||
eprintln!("verifying assertion: {}", conjecture.formula);
|
||
|
||
let tptp_content = format!("{}", ask_dracula::format_tptp::display_project_with_conjecture_tptp(&project, conjecture, proof_direction));
|
||
|
||
run_vampire(&tptp_content, matches.values_of("vampire_arguments").map(|value| value))?
|
||
},
|
||
};
|
||
|
||
let conjecture = find_conjecture_mut(&mut project, proof_direction).unwrap();
|
||
|
||
match vampire_result
|
||
{
|
||
ProofResult::ProofNotFound =>
|
||
{
|
||
println!("proof not found");
|
||
return Ok(());
|
||
},
|
||
ProofResult::Refutation =>
|
||
{
|
||
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();
|
||
|
||
let backup_file_path = backup_file_path(file_path)?;
|
||
|
||
// Make backup of old file
|
||
std::fs::rename(file_path, backup_file_path)
|
||
.map_err(|error| ask_dracula::Error::new_write_file(file_path.to_owned(), error))?;
|
||
|
||
// Write updated version of the file
|
||
let file_content = format!("{}", project);
|
||
std::fs::write(file_path, &file_content)
|
||
.map_err(|error| ask_dracula::Error::new_write_file(file_path.to_owned(), error))?;
|
||
},
|
||
ProofResult::Satisfiable =>
|
||
{
|
||
println!("assertion disproven");
|
||
return Ok(());
|
||
},
|
||
}
|
||
}
|
||
}
|
||
|
||
Ok(())
|
||
}
|