From bce9d8061c0e900c77f04e4c72c3bbbe90f462ba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Wed, 6 Nov 2019 04:36:51 -0600 Subject: [PATCH] Verify all assertions one after the other --- src/format.rs | 4 +- src/format_tptp.rs | 14 +++---- src/main.rs | 99 +++++++++++++++++++++++----------------------- src/parse.rs | 6 +-- src/project.rs | 14 +++---- 5 files changed, 69 insertions(+), 68 deletions(-) diff --git a/src/format.rs b/src/format.rs index 67bdb29..c4fbd57 100644 --- a/src/format.rs +++ b/src/format.rs @@ -20,7 +20,7 @@ impl std::fmt::Display for crate::project::StatementKind } } -impl<'input> std::fmt::Debug for crate::Project<'input> +impl std::fmt::Debug for crate::Project { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -38,7 +38,7 @@ impl<'input> std::fmt::Debug for crate::Project<'input> } } -impl<'input> std::fmt::Display for crate::Project<'input> +impl std::fmt::Display for crate::Project { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { diff --git a/src/format_tptp.rs b/src/format_tptp.rs index aa80588..a17cb23 100644 --- a/src/format_tptp.rs +++ b/src/format_tptp.rs @@ -222,10 +222,10 @@ struct PredicateDeclarationDisplay<'a>(&'a foliage::PredicateDeclaration); struct TermDisplay<'a>(&'a foliage::Term); struct FormulaDisplay<'a>(&'a foliage::Formula); struct StatementKindDisplay<'a>(&'a crate::project::StatementKind); -pub struct ProjectDisplay<'a, 'input> +pub struct ProjectDisplay<'a> { - project: &'a crate::project::Project<'input>, - conjecture: &'a crate::project::Statement<'input>, + project: &'a crate::project::Project, + conjecture: &'a crate::project::Statement, } impl<'a> DisplayTPTP<'a, VariableDeclarationDisplay<'a>> for foliage::VariableDeclaration @@ -268,8 +268,8 @@ impl<'a> DisplayTPTP<'a, StatementKindDisplay<'a>> for crate::project::Statement } } -pub fn display_project_with_conjecture_tptp<'a, 'input>(project: &'a crate::Project<'input>, - conjecture: &'a crate::project::Statement<'input>) -> ProjectDisplay<'a, 'input> +pub fn display_project_with_conjecture_tptp<'a>(project: &'a crate::Project, + conjecture: &'a crate::project::Statement) -> ProjectDisplay<'a> { ProjectDisplay { @@ -570,7 +570,7 @@ impl<'a> std::fmt::Display for StatementKindDisplay<'a> } } -impl<'a, 'input> std::fmt::Debug for ProjectDisplay<'a, 'input> +impl<'a> std::fmt::Debug for ProjectDisplay<'a> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -647,7 +647,7 @@ impl<'a, 'input> std::fmt::Debug for ProjectDisplay<'a, 'input> } } -impl<'a, 'input> std::fmt::Display for ProjectDisplay<'a, 'input> +impl<'a> std::fmt::Display for ProjectDisplay<'a> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { diff --git a/src/main.rs b/src/main.rs index ba22167..b79fd64 100644 --- a/src/main.rs +++ b/src/main.rs @@ -19,7 +19,7 @@ fn backup_file_path(file_path: &std::path::Path) -> Result(project: &'a ask_dracula::Project<'input>) -> Option<&'a ask_dracula::project::Statement<'input>> +fn find_conjecture<'a>(project: &'a ask_dracula::Project) -> Option<&'a ask_dracula::project::Statement> { for block in &project.blocks { @@ -35,7 +35,7 @@ fn find_conjecture<'a, 'input>(project: &'a ask_dracula::Project<'input>) -> Opt None } -fn find_conjecture_mut<'a, 'input>(project: &'a mut ask_dracula::Project<'input>) -> Option<&'a mut ask_dracula::project::Statement<'input>> +fn find_conjecture_mut<'a>(project: &'a mut ask_dracula::Project) -> Option<&'a mut ask_dracula::project::Statement> { for block in &mut project.blocks { @@ -134,60 +134,61 @@ fn main() -> Result<(), Box> let (_, mut project) = ask_dracula::parse::project(&file_content) .map_err(|_| "couldn’t parse input file")?; - let conjecture = find_conjecture(&project); + let replace_statement_kind_regex = regex::Regex::new(r"(assertion)").unwrap(); - let vampire_result = match conjecture + loop { - None => + let conjecture = find_conjecture(&project); + + let vampire_result = match conjecture { - eprintln!("nothing to prove, exiting"); - return Ok(()); - }, - Some(ref 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)); + + run_vampire(&tptp_content, matches.values_of("vampire_arguments").map(|value| value))? + }, + }; + + let conjecture = find_conjecture_mut(&mut project).unwrap(); + + match vampire_result { - eprintln!("verifying conjecture: {}", conjecture.formula); + ProofResult::ProofNotFound => + { + println!("proof not found"); + return Ok(()); + }, + ProofResult::Refutation => + { + println!("assertion proven"); - let tptp_content = format!("{}", ask_dracula::format_tptp::display_project_with_conjecture_tptp(&project, conjecture)); + conjecture.kind = ask_dracula::project::StatementKind::Axiom; + conjecture.original_text = replace_statement_kind_regex.replace(&conjecture.original_text, "axiom").to_string(); - run_vampire(&tptp_content, matches.values_of("vampire_arguments").map(|value| value))? - }, - }; + let backup_file_path = backup_file_path(file_path)?; - let conjecture = find_conjecture_mut(&mut project).unwrap(); + // 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))?; - match vampire_result - { - ProofResult::ProofNotFound => - { - println!("proof not found"); - Ok(()) - }, - ProofResult::Refutation => - { - println!("assertion proven"); - - conjecture.kind = ask_dracula::project::StatementKind::Axiom; - let replace_statement_kind_regex = regex::Regex::new(r"(assertion)").unwrap(); - let new_text = replace_statement_kind_regex.replace(conjecture.original_text, "axiom"); - conjecture.original_text = &new_text; - - 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(()) - }, - ProofResult::Satisfiable => - { - println!("conjecture disproven"); - Ok(()) - }, + // 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(()); + }, + } } } diff --git a/src/parse.rs b/src/parse.rs index 259ec27..4fbb691 100644 --- a/src/parse.rs +++ b/src/parse.rs @@ -109,13 +109,13 @@ pub fn project(i: &str) -> IResult<&str, crate::Project> if !whitespace_before.is_empty() { - blocks.push(crate::project::Block::Whitespace(whitespace_before)); + blocks.push(crate::project::Block::Whitespace(whitespace_before.to_string())); } let statement = crate::project::Statement { kind: statement_kind, - original_text: statement_original_text, + original_text: statement_original_text.to_string(), formula, }; @@ -123,7 +123,7 @@ pub fn project(i: &str) -> IResult<&str, crate::Project> if !whitespace_after.is_empty() { - blocks.push(crate::project::Block::Whitespace(whitespace_after)); + blocks.push(crate::project::Block::Whitespace(whitespace_after.to_string())); } statement_input = i; diff --git a/src/project.rs b/src/project.rs index 20ee70b..97adcb7 100644 --- a/src/project.rs +++ b/src/project.rs @@ -7,20 +7,20 @@ pub enum StatementKind Assertion, } -pub struct Statement<'input> +pub struct Statement { pub kind: StatementKind, - pub original_text: &'input str, + pub original_text: String, pub formula: foliage::Formula, } -pub enum Block<'input> +pub enum Block { - Statement(Statement<'input>), - Whitespace(&'input str), + Statement(Statement), + Whitespace(String), } -pub struct Project<'input> +pub struct Project { - pub blocks: Vec>, + pub blocks: Vec, }