Finish first version of interactive prover

This commit is contained in:
Patrick Lühne 2019-11-02 07:23:34 +01:00
parent 228b2032f7
commit 52d8c84bc0
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
6 changed files with 290 additions and 31 deletions

View File

@ -10,3 +10,4 @@ edition = "2018"
clap = "2.33" clap = "2.33"
foliage = {path = "foliage"} foliage = {path = "foliage"}
nom = "5.0" nom = "5.0"
regex = "1.3"

101
src/error.rs Normal file
View File

@ -0,0 +1,101 @@
pub type Source = Box<dyn std::error::Error>;
pub enum Kind
{
ParseProject,
NotAFile(std::path::PathBuf),
WriteFile(std::path::PathBuf),
RunVampire,
InterpretVampireOutput(String, String),
}
pub struct Error
{
pub kind: Kind,
pub source: Option<Source>,
}
impl Error
{
pub fn new(kind: Kind) -> Self
{
Self
{
kind,
source: None,
}
}
pub fn with<S: Into<Source>>(mut self, source: S) -> Self
{
self.source = Some(source.into());
self
}
pub fn new_parse_project<S: Into<Source>>(source: S) -> Self
{
Self::new(Kind::ParseProject).with(source)
}
pub fn new_not_a_file(path: std::path::PathBuf) -> Self
{
Self::new(Kind::NotAFile(path))
}
pub fn new_write_file<S: Into<Source>>(path: std::path::PathBuf, source: S) -> Self
{
Self::new(Kind::WriteFile(path)).with(source)
}
pub fn new_run_vampire<S: Into<Source>>(source: S) -> Self
{
Self::new(Kind::RunVampire).with(source)
}
pub fn new_interpret_vampire_output(stdout: String, stderr: String) -> Self
{
Self::new(Kind::InterpretVampireOutput(stdout, stderr))
}
}
impl std::fmt::Debug for Error
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match self.kind
{
Kind::ParseProject => write!(formatter, "could not parse project file")?,
Kind::NotAFile(ref file_path) => write!(formatter, "specified path is not a file ({})", file_path.display())?,
Kind::WriteFile(ref file_path) => write!(formatter, "could not write file ({})", file_path.display())?,
Kind::RunVampire => write!(formatter, "could not run Vampire")?,
Kind::InterpretVampireOutput(ref stdout, ref stderr) => write!(formatter, "could not interpret Vampire output\n\n======== stdout =========\n{}\n\n======== stderr =========\n{}", stdout, stderr)?,
}
if let Some(source) = &self.source
{
write!(formatter, "\nerror source: {}", source)?;
}
Ok(())
}
}
impl std::fmt::Display for Error
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", self)
}
}
impl std::error::Error for Error
{
fn source(&self) -> Option<&(dyn std::error::Error + 'static)>
{
match &self.source
{
Some(source) => Some(source.as_ref()),
None => None,
}
}
}

View File

@ -209,7 +209,11 @@ struct PredicateDeclarationDisplay<'a>(&'a foliage::PredicateDeclaration);
struct TermDisplay<'a>(&'a foliage::Term); struct TermDisplay<'a>(&'a foliage::Term);
struct FormulaDisplay<'a>(&'a foliage::Formula); struct FormulaDisplay<'a>(&'a foliage::Formula);
struct StatementKindDisplay<'a>(&'a crate::project::StatementKind); struct StatementKindDisplay<'a>(&'a crate::project::StatementKind);
pub struct ProjectDisplay<'a>(&'a crate::project::Project); pub struct ProjectDisplay<'a>
{
project: &'a crate::project::Project,
conjecture: (crate::project::StatementKind, &'a foliage::Formula),
}
impl<'a> DisplayTPTP<'a, VariableDeclarationDisplay<'a>> for foliage::VariableDeclaration impl<'a> DisplayTPTP<'a, VariableDeclarationDisplay<'a>> for foliage::VariableDeclaration
{ {
@ -251,11 +255,13 @@ impl<'a> DisplayTPTP<'a, StatementKindDisplay<'a>> for crate::project::Statement
} }
} }
impl<'a> DisplayTPTP<'a, ProjectDisplay<'a>> for crate::project::Project pub fn display_project_with_conjecture_tptp<'a>(project: &'a crate::Project,
conjecture: (crate::project::StatementKind, &'a foliage::Formula)) -> ProjectDisplay<'a>
{ {
fn display_tptp(&'a self) -> ProjectDisplay<'a> ProjectDisplay
{ {
ProjectDisplay(self) project,
conjecture,
} }
} }
@ -569,8 +575,8 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a>
let tptp_preamble_anthem_axioms = include_str!("tptp_preamble_anthem_axioms.tptp").trim_end(); let tptp_preamble_anthem_axioms = include_str!("tptp_preamble_anthem_axioms.tptp").trim_end();
write!(format, "\n{}", tptp_preamble_anthem_axioms)?; write!(format, "\n{}", tptp_preamble_anthem_axioms)?;
let predicate_declarations = collect_predicate_declarations_in_project(self.0); let predicate_declarations = collect_predicate_declarations_in_project(self.project);
let symbolic_constants = collect_symbolic_constants_in_project(self.0); let symbolic_constants = collect_symbolic_constants_in_project(self.project);
if !predicate_declarations.is_empty() || !symbolic_constants.is_empty() if !predicate_declarations.is_empty() || !symbolic_constants.is_empty()
{ {
@ -587,7 +593,7 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a>
} }
} }
if let Some(axioms) = self.0.statements.get(&crate::project::StatementKind::Axiom) if let Some(axioms) = self.project.statements.get(&crate::project::StatementKind::Axiom)
{ {
write_title(format, "\n\n", "axioms")?; write_title(format, "\n\n", "axioms")?;
@ -597,27 +603,26 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a>
} }
} }
if let Some(lemmas) = self.0.statements.get(&crate::project::StatementKind::Lemma) match self.conjecture
{ {
write_title(format, "\n\n", "lemmas")?; (crate::project::StatementKind::Lemma, ref lemma) =>
{
write_title(format, "\n\n", "lemma")?;
for lemma in lemmas
{
write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Lemma.display_tptp(), lemma.display_tptp())?; write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Lemma.display_tptp(), lemma.display_tptp())?;
}
}
if let Some(conjectures) = self.0.statements.get(&crate::project::StatementKind::Conjecture)
{
write_title(format, "\n\n", "conjectures")?;
for conjecture in conjectures
{
write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Conjecture.display_tptp(), conjecture.display_tptp())?;
}
}
Ok(()) Ok(())
},
(crate::project::StatementKind::Conjecture, ref conjecture) =>
{
write_title(format, "\n\n", "conjecture")?;
write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Conjecture.display_tptp(), conjecture.display_tptp())?;
Ok(())
},
(crate::project::StatementKind::Axiom, _) => panic!("unexpected axiom"),
}
} }
} }

View File

@ -1,6 +1,8 @@
mod error;
pub mod format; pub mod format;
pub mod format_tptp; pub mod format_tptp;
pub mod parse; pub mod parse;
mod project; pub mod project;
pub use error::Error;
pub use project::Project; pub use project::Project;

View File

@ -1,22 +1,172 @@
use ask_dracula::format_tptp::DisplayTPTP; 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) -> Option<(ask_dracula::project::StatementKind, &'a foliage::Formula)>
{
if let Some(lemmas) = project.statements.get(&ask_dracula::project::StatementKind::Lemma)
{
if let Some(lemma) = lemmas.first()
{
return Some((ask_dracula::project::StatementKind::Lemma, lemma));
}
}
if let Some(conjectures) = project.statements.get(&ask_dracula::project::StatementKind::Conjecture)
{
if let Some(conjecture) = conjectures.first()
{
return Some((ask_dracula::project::StatementKind::Conjecture, conjecture));
}
}
None
}
enum VampireResult
{
ProofNotFound,
Refutation,
Satisfiable,
}
fn run_vampire<I, S>(input: &str, arguments: Option<I>)
-> Result<VampireResult, 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,
};
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(VampireResult::ProofNotFound);
}
return Err(ask_dracula::Error::new_run_vampire(
format!("Vampire returned unsuccessful exit code ({})\n\n======== stderr ========\n{}", output.status, std::str::from_utf8(&output.stdout).unwrap_or("(not valid UTF-8)").trim())));
}
let refutation_regex = regex::Regex::new(r"% \(\d+\)Termination reason: Refutation").unwrap();
if refutation_regex.is_match(stdout)
{
return Ok(VampireResult::Refutation);
}
Err(ask_dracula::Error::new_interpret_vampire_output(stdout.to_string(), stderr.to_string()))
}
fn main() -> Result<(), Box<dyn std::error::Error>> fn main() -> Result<(), Box<dyn std::error::Error>>
{ {
let matches = clap::App::new("Ask Dracula: Using Vampire as an interactive theorem prover") let matches = clap::App::new("Ask Dracula: Using Vampire as an interactive theorem prover")
.arg(clap::Arg::with_name("file").long("file").short("f").takes_value(true).required(true)) .arg(clap::Arg::with_name("file").takes_value(true).required(true))
.after_help("example: ask_dracula -f program") .arg(clap::Arg::with_name("vampire_arguments").multiple(true))
.after_help("example: ask_dracula <project file> -- --mode casc --cores 8")
.get_matches(); .get_matches();
let file = matches.value_of("file").unwrap().to_string(); let file = matches.value_of("file").unwrap().to_string();
let file_path = std::path::Path::new(&file); let file_path = std::path::Path::new(&file);
let file_content = std::fs::read_to_string(&file_path)?; let file_content = std::fs::read_to_string(&file_path)?;
let (_, project) = ask_dracula::parse::project(&file_content) let (_, mut project) = ask_dracula::parse::project(&file_content)
.map_err(|_| "couldnt parse input file")?; .map_err(|_| "couldnt parse input file")?;
eprintln!("{}", project); match find_conjecture(&project)
{
None =>
{
eprintln!("no lemma or conjecture found, nothing to do");
Ok(())
},
Some((ref statement_kind, ref conjecture)) =>
{
eprintln!("verifying conjecture: {}", conjecture);
println!("{}", project.display_tptp()); let tptp_content = format!("{}", ask_dracula::format_tptp::display_project_with_conjecture_tptp(&project, (statement_kind.clone(), conjecture)));
match run_vampire(&tptp_content, matches.values_of("vampire_arguments").map(|value| value))?
{
VampireResult::ProofNotFound =>
{
println!("proof not found");
Ok(())
},
VampireResult::Refutation =>
{
println!("conjecture proven");
let axiom = project.statements.get_mut(statement_kind).unwrap().remove(0);
project.statements.entry(ask_dracula::project::StatementKind::Axiom).or_insert_with(Vec::new).push(axiom);
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))?;
Ok(()) Ok(())
},
VampireResult::Satisfiable =>
{
println!("conjecture disproven");
Ok(())
},
}
},
}
} }

View File

@ -8,5 +8,5 @@ pub enum StatementKind
pub struct Project pub struct Project
{ {
pub(crate) statements: std::collections::HashMap<StatementKind, Vec<foliage::Formula>>, pub statements: std::collections::HashMap<StatementKind, Vec<foliage::Formula>>,
} }