Add option for proof direction

src/commands/verify_program.rs

@@ -1,4 +1,4 @@
-pub fn run<P>(program_path: P, specification_path: P, output_format: crate::output::Format)
+pub fn run<P>(program_path: P, specification_path: P, proof_direction: crate::ProofDirection)
 where
 	P: AsRef<std::path::Path>
 {
@@ -43,7 +43,7 @@ where
 		}
 	}
 
-	match problem.prove(crate::ProofDirection::Both)
+	match problem.prove(proof_direction)
 	{
 		Ok(()) => (),
 		Err(error) =>

src/lib.rs

@@ -12,4 +12,4 @@ mod utils;
 pub use error::Error;
 pub use problem::Problem;
 pub(crate) use utils::*;
-pub use utils::{Domain, InputConstantDeclarationDomains};
+pub use utils::{Domain, InputConstantDeclarationDomains, ProofDirection};

src/main.rs

@@ -16,9 +16,9 @@ enum Command
 		/// Specification file path
 		specification_path: std::path::PathBuf,
 
-		/// Output format (human-readable, tptp)
-		#[structopt(long, default_value = "human-readable")]
-		output_format: anthem::output::Format,
+		/// Proof direction (forward, backward, both)
+		#[structopt(long, default_value = "forward")]
+		proof_direction: anthem::ProofDirection,
 	}
 }
 
@@ -34,9 +34,9 @@ fn main()
 		{
 			program_path,
 			specification_path,
-			output_format,
+			proof_direction,
 		}
 			=> anthem::commands::verify_program::run(&program_path, &specification_path,
-				output_format),
+				proof_direction),
 	}
 }

src/output/tptp.rs

@@ -340,8 +340,7 @@ where
 			let is_right_term_arithmetic = crate::is_term_arithmetic(right, self.context)
 				.expect("could not determine whether term is arithmetic");
 
-			match (!is_left_term_arithmetic && !is_right_term_arithmetic,
-				auxiliary_predicate_name)
+			match (!is_left_term_arithmetic || !is_right_term_arithmetic, auxiliary_predicate_name)
 			{
 				(true, Some(auxiliary_predicate_name)) =>
 				{

src/problem.rs

@@ -2,6 +2,7 @@
 pub enum StatementKind
 {
 	Axiom,
+	Program,
 	Assumption,
 	Lemma(crate::ProofDirection),
 	Assertion,
@@ -148,6 +149,7 @@ impl Problem
 					{
 						StatementKind::Axiom
 						| StatementKind::Assumption
+						| StatementKind::Program
 							=> statement.proof_status = ProofStatus::AssumedProven,
 						StatementKind::Lemma(crate::ProofDirection::Backward)
 							=> statement.proof_status = ProofStatus::Ignored,
@@ -178,6 +180,7 @@ impl Problem
 					match statement.kind
 					{
 						StatementKind::Axiom
+						| StatementKind::Assumption
 						| StatementKind::Assertion
 							=> statement.proof_status = ProofStatus::AssumedProven,
 						StatementKind::Lemma(crate::ProofDirection::Forward)

src/translate/verify_properties.rs

@@ -159,7 +159,7 @@ impl<'p> Translator<'p>
 				completed_definition(predicate_declaration, &mut self.definitions, self.problem);
 
 			let statement = crate::problem::Statement::new(
-				crate::problem::StatementKind::Assumption, completed_definition)
+				crate::problem::StatementKind::Program, completed_definition)
 				.with_name(format!("completed_definition_{}_{}", predicate_declaration.name,
 					predicate_declaration.arity))
 				.with_description(format!("completed definition of {}/{}",
@@ -315,7 +315,7 @@ impl<'p> Translator<'p>
 				*/
 
 				let statement = crate::problem::Statement::new(
-					crate::problem::StatementKind::Assumption, integrity_constraint)
+					crate::problem::StatementKind::Program, integrity_constraint)
 					.with_name("integrity_constraint".to_string())
 					.with_description("integrity constraint".to_string());
 

src/utils.rs

@@ -44,6 +44,61 @@ pub enum ProofDirection
 	Both,
 }
 
+impl std::fmt::Debug for ProofDirection
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match self
+		{
+			ProofDirection::Forward => write!(formatter, "forward"),
+			ProofDirection::Backward => write!(formatter, "backward"),
+			ProofDirection::Both => write!(formatter, "both"),
+		}
+	}
+}
+
+impl std::fmt::Display for ProofDirection
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(formatter, "{:?}", self)
+	}
+}
+
+pub struct InvalidProofDirectionError;
+
+impl std::fmt::Debug for InvalidProofDirectionError
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(formatter, "invalid proof direction")
+	}
+}
+
+impl std::fmt::Display for InvalidProofDirectionError
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(formatter, "{:?}", self)
+	}
+}
+
+impl std::str::FromStr for ProofDirection
+{
+	type Err = InvalidProofDirectionError;
+
+	fn from_str(s: &str) -> Result<Self, Self::Err>
+	{
+		match s
+		{
+			"forward" => Ok(ProofDirection::Forward),
+			"backward" => Ok(ProofDirection::Backward),
+			"both" => Ok(ProofDirection::Both),
+			_ => Err(InvalidProofDirectionError),
+		}
+	}
+}
+
 pub(crate) struct ScopedFormula
 {
 	pub free_variable_declarations: std::rc::Rc<foliage::VariableDeclarations>,