diff --git a/src/commands/verify_program.rs b/src/commands/verify_program.rs
index 3afe935..ae2e482 100644
--- a/src/commands/verify_program.rs
+++ b/src/commands/verify_program.rs
@@ -1,4 +1,4 @@
-pub fn run
(program_path: P, specification_path: P, output_format: crate::output::Format)
+pub fn run
(program_path: P, specification_path: P, proof_direction: crate::ProofDirection)
where
P: AsRef
{
@@ -43,7 +43,7 @@ where
}
}
- match problem.prove(crate::ProofDirection::Both)
+ match problem.prove(proof_direction)
{
Ok(()) => (),
Err(error) =>
diff --git a/src/lib.rs b/src/lib.rs
index 0c0845f..1ab2abf 100644
--- a/src/lib.rs
+++ b/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};
diff --git a/src/main.rs b/src/main.rs
index 0444f09..752128e 100644
--- a/src/main.rs
+++ b/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),
}
}
diff --git a/src/output/tptp.rs b/src/output/tptp.rs
index e678396..ed8e3d2 100644
--- a/src/output/tptp.rs
+++ b/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)) =>
{
diff --git a/src/problem.rs b/src/problem.rs
index f4901ad..75295cd 100644
--- a/src/problem.rs
+++ b/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)
diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs
index c073975..e957ad7 100644
--- a/src/translate/verify_properties.rs
+++ b/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());
diff --git a/src/utils.rs b/src/utils.rs
index b7fed68..fce577b 100644
--- a/src/utils.rs
+++ b/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
+ {
+ 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,