diff --git a/src/format_tptp.rs b/src/format_tptp.rs index a17cb23..b2de09d 100644 --- a/src/format_tptp.rs +++ b/src/format_tptp.rs @@ -1,9 +1,28 @@ +#[derive(Clone, Copy, Eq, Hash, PartialEq)] +pub enum ProofDirection +{ + Forward, + Backward, +} + pub trait DisplayTPTP<'a, DisplayType> where DisplayType: 'a + std::fmt::Debug + std::fmt::Display { fn display_tptp(&'a self) -> DisplayType; } +pub fn is_statement_kind_conjecture(statement_kind: crate::project::StatementKind, + proof_direction: ProofDirection) -> bool +{ + match proof_direction + { + ProofDirection::Forward => + statement_kind == crate::project::StatementKind::Assertion, + ProofDirection::Backward => + statement_kind == crate::project::StatementKind::Completion, + } +} + fn is_arithmetic_term(term: &foliage::Term) -> bool { match term @@ -221,11 +240,16 @@ struct VariableDeclarationDisplay<'a>(&'a foliage::VariableDeclaration); 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); +struct StatementKindDisplay +{ + statement_kind: crate::project::StatementKind, + proof_direction: ProofDirection, +} pub struct ProjectDisplay<'a> { project: &'a crate::project::Project, conjecture: &'a crate::project::Statement, + proof_direction: ProofDirection, } impl<'a> DisplayTPTP<'a, VariableDeclarationDisplay<'a>> for foliage::VariableDeclaration @@ -260,21 +284,26 @@ impl<'a> DisplayTPTP<'a, FormulaDisplay<'a>> for foliage::Formula } } -impl<'a> DisplayTPTP<'a, StatementKindDisplay<'a>> for crate::project::StatementKind +fn display_statement_kind_tptp(statement_kind: crate::project::StatementKind, + proof_direction: ProofDirection) + -> StatementKindDisplay { - fn display_tptp(&'a self) -> StatementKindDisplay<'a> + StatementKindDisplay { - StatementKindDisplay(self) + statement_kind, + proof_direction, } } pub fn display_project_with_conjecture_tptp<'a>(project: &'a crate::Project, - conjecture: &'a crate::project::Statement) -> ProjectDisplay<'a> + conjecture: &'a crate::project::Statement, proof_direction: ProofDirection) + -> ProjectDisplay<'a> { ProjectDisplay { project, conjecture, + proof_direction, } } @@ -548,21 +577,23 @@ impl<'a> std::fmt::Display for FormulaDisplay<'a> } } -impl<'a> std::fmt::Debug for StatementKindDisplay<'a> +impl std::fmt::Debug for StatementKindDisplay { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - match &self.0 + match (self.statement_kind, self.proof_direction) { - crate::project::StatementKind::Axiom => write!(format, "axiom, axiom"), - crate::project::StatementKind::Completion => write!(format, "completion, axiom"), - crate::project::StatementKind::Assumption => write!(format, "assumption, axiom"), - crate::project::StatementKind::Assertion => write!(format, "assertion, conjecture"), + (crate::project::StatementKind::Axiom, _) => write!(format, "axiom, axiom"), + (crate::project::StatementKind::Assumption, _) => write!(format, "assumption, axiom"), + (crate::project::StatementKind::Completion, ProofDirection::Forward) => write!(format, "completion, axiom"), + (crate::project::StatementKind::Completion, ProofDirection::Backward) => write!(format, "completion, conjecture"), + (crate::project::StatementKind::Assertion, ProofDirection::Forward) => write!(format, "assertion, conjecture"), + (crate::project::StatementKind::Assertion, ProofDirection::Backward) => write!(format, "assertion, axiom"), } } } -impl<'a> std::fmt::Display for StatementKindDisplay<'a> +impl std::fmt::Display for StatementKindDisplay { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -616,34 +647,25 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> { crate::project::Block::Whitespace(_) => None, crate::project::Block::Statement(ref statement) => - match statement.kind + match is_statement_kind_conjecture(statement.kind, self.proof_direction) { - crate::project::StatementKind::Axiom - | crate::project::StatementKind::Completion - | crate::project::StatementKind::Assumption => Some(statement), - crate::project::StatementKind::Assertion => None, + false => Some(statement), + true => None, } }); for axiom in axioms { - write!(format, "\ntff({:?}, {:?}).", axiom.kind.display_tptp(), axiom.formula.display_tptp())?; + write!(format, "\ntff({:?}, {:?}).", + display_statement_kind_tptp(axiom.kind, self.proof_direction), axiom.formula.display_tptp())?; } - match self.conjecture.kind - { - crate::project::StatementKind::Assertion => - { - write_title(format, "\n\n", "assertion")?; + write_title(format, "\n\n", "assertion")?; - write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Assertion.display_tptp(), self.conjecture.formula.display_tptp())?; + write!(format, "\ntff({:?}, {:?}).", + display_statement_kind_tptp(self.conjecture.kind, self.proof_direction), self.conjecture.formula.display_tptp())?; - Ok(()) - }, - crate::project::StatementKind::Axiom => panic!("unexpected axiom statement"), - crate::project::StatementKind::Completion => panic!("unexpected completion statement"), - crate::project::StatementKind::Assumption => panic!("unexpected assumption statement"), - } + Ok(()) } } diff --git a/src/main.rs b/src/main.rs index b79fd64..431d12b 100644 --- a/src/main.rs +++ b/src/main.rs @@ -19,13 +19,15 @@ fn backup_file_path(file_path: &std::path::Path) -> Result(project: &'a ask_dracula::Project) -> Option<&'a ask_dracula::project::Statement> +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 statement.kind == ask_dracula::project::StatementKind::Assertion + if ask_dracula::format_tptp::is_statement_kind_conjecture(statement.kind, proof_direction) { return Some(statement) } @@ -35,13 +37,15 @@ fn find_conjecture<'a>(project: &'a ask_dracula::Project) -> Option<&'a ask_drac None } -fn find_conjecture_mut<'a>(project: &'a mut ask_dracula::Project) -> Option<&'a mut ask_dracula::project::Statement> +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 statement.kind == ask_dracula::project::StatementKind::Assertion + if ask_dracula::format_tptp::is_statement_kind_conjecture(statement.kind, proof_direction) { return Some(statement) } @@ -123,6 +127,7 @@ fn main() -> Result<(), Box> { 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 -- --mode casc --cores 8") .get_matches(); @@ -136,59 +141,72 @@ fn main() -> Result<(), Box> let replace_statement_kind_regex = regex::Regex::new(r"(assertion)").unwrap(); - loop + let proof_directions = match matches.value_of("proof-direction").unwrap() { - let conjecture = find_conjecture(&project); + "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), + }; - let vampire_result = match conjecture + for proof_direction in proof_directions + { + loop { - None => + let conjecture = find_conjecture(&project, proof_direction); + + 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, 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 { - eprintln!("verifying assertion: {}", 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"); - return Ok(()); - }, - ProofResult::Refutation => - { - 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(()); - }, + // 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(()) } diff --git a/src/project.rs b/src/project.rs index 97adcb7..e6b5a89 100644 --- a/src/project.rs +++ b/src/project.rs @@ -1,4 +1,4 @@ -#[derive(Clone, Eq, Hash, PartialEq)] +#[derive(Clone, Copy, Eq, Hash, PartialEq)] pub enum StatementKind { Axiom,