Implement backward proofs

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::Axiom, _) => write!(format, "axiom, axiom"),
-			crate::project::StatementKind::Completion => write!(format, "completion, axiom"),
+			(crate::project::StatementKind::Assumption, _) => write!(format, "assumption, axiom"),
-			crate::project::StatementKind::Assumption => write!(format, "assumption, axiom"),
+			(crate::project::StatementKind::Completion, ProofDirection::Forward) => write!(format, "completion, axiom"),
-			crate::project::StatementKind::Assertion => write!(format, "assertion, conjecture"),
+			(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
+							false => Some(statement),
-								| crate::project::StatementKind::Completion
+							true => None,
-								| crate::project::StatementKind::Assumption => Some(statement),
-							crate::project::StatementKind::Assertion => 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
+		write_title(format, "\n\n", "assertion")?;
-		{
-			crate::project::StatementKind::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(())
+		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"),
-		}
 	}
 }
 

src/main.rs

@@ -19,13 +19,15 @@ fn backup_file_path(file_path: &std::path::Path) -> Result<std::path::PathBuf, a
 	}
 }
 
-fn find_conjecture<'a>(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<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();
@@ -136,59 +141,72 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
 
 	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");
+				None =>
-				return Ok(());
+				{
-			},
+					eprintln!("nothing to prove, exiting");
-			Some(ref conjecture) =>
+					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
+					// Write updated version of the file
-		{
+					let file_content = format!("{}", project);
-			ProofResult::ProofNotFound =>
+					std::fs::write(file_path, &file_content)
-			{
+						.map_err(|error| ask_dracula::Error::new_write_file(file_path.to_owned(), error))?;
-				println!("proof not found");
+				},
-				return Ok(());
+				ProofResult::Satisfiable =>
-			},
+				{
-			ProofResult::Refutation =>
+					println!("assertion disproven");
-			{
+					return Ok(());
-				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(())
 }

src/project.rs

@@ -1,4 +1,4 @@
-#[derive(Clone, Eq, Hash, PartialEq)]
+#[derive(Clone, Copy, Eq, Hash, PartialEq)]
 pub enum StatementKind
 {
 	Axiom,