From 80d39c8c0a0c4f4e5af22b27cad69d247bf15f8f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Mon, 18 May 2020 02:17:30 +0200
Subject: [PATCH] Check that only input/output predicates are used in
 specification

---
 src/commands/verify_program.rs | 10 +++++++
 src/error.rs                   | 12 +++++++++
 src/problem.rs                 | 48 ++++++++++++++++++++++++++++++++++
 src/utils/output_predicates.rs |  2 +-
 4 files changed, 71 insertions(+), 1 deletion(-)

diff --git a/src/commands/verify_program.rs b/src/commands/verify_program.rs
index aa2a775..f6aece4 100644
--- a/src/commands/verify_program.rs
+++ b/src/commands/verify_program.rs
@@ -44,6 +44,16 @@ where
 		}
 	}
 
+	match problem.check_that_only_input_and_output_predicates_are_used()
+	{
+		Ok(_) => (),
+		Err(error) =>
+		{
+			log::error!("{}", error);
+			std::process::exit(1)
+		}
+	}
+
 	match problem.restrict_to_output_predicates()
 	{
 		Ok(_) => (),
diff --git a/src/error.rs b/src/error.rs
index bba0259..12ae716 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -24,6 +24,7 @@ pub enum Kind
 	FormulaNotClosed(std::rc::Rc<foliage::VariableDeclarations>),
 	NoCompletedDefinitionFound(std::rc::Rc<foliage::PredicateDeclaration>),
 	CannotHidePredicate(std::rc::Rc<foliage::PredicateDeclaration>),
+	PredicateShouldNotOccurInSpecification(std::rc::Rc<foliage::PredicateDeclaration>),
 	WriteTPTPProgram,
 	RunVampire,
 	// TODO: rename to something Vampire-specific
@@ -164,6 +165,13 @@ impl Error
 		Self::new(Kind::CannotHidePredicate(predicate_declaration))
 	}
 
+	pub(crate) fn new_predicate_should_not_occur_in_specification(
+		predicate_declaration: std::rc::Rc<foliage::PredicateDeclaration>)
+		-> Self
+	{
+		Self::new(Kind::PredicateShouldNotOccurInSpecification(predicate_declaration))
+	}
+
 	pub(crate) fn new_write_tptp_program<S: Into<Source>>(source: S) -> Self
 	{
 		Self::new(Kind::WriteTPTPProgram).with(source)
@@ -241,6 +249,10 @@ impl std::fmt::Debug for Error
 				write!(formatter,
 					"cannot hide predicate {} (the completed definition transitively depends on itself)",
 					predicate_declaration),
+			Kind::PredicateShouldNotOccurInSpecification(ref predicate_declaration) =>
+				write!(formatter,
+					"predicate {} should not occur in specification (it is not declared as an input or output predicate)",
+					predicate_declaration),
 			Kind::RunVampire => write!(formatter, "could not run Vampire"),
 			Kind::ProveProgram(exit_code, ref stdout, ref stderr) =>
 			{
diff --git a/src/problem.rs b/src/problem.rs
index 9221709..764e899 100644
--- a/src/problem.rs
+++ b/src/problem.rs
@@ -82,6 +82,54 @@ impl Problem
 		section.push(statement);
 	}
 
+	pub(crate) fn check_that_only_input_and_output_predicates_are_used(&self)
+		-> Result<(), crate::Error>
+	{
+		let predicate_declarations = self.predicate_declarations.borrow();
+		let input_predicate_declarations = self.input_predicate_declarations.borrow();
+		let output_predicate_declarations = self.output_predicate_declarations.borrow();
+
+		if output_predicate_declarations.is_empty()
+		{
+			return Ok(());
+		}
+
+		// Check that only input and output predicates are used in the specification
+		for predicate_declaration in predicate_declarations.iter()
+		{
+			if input_predicate_declarations.contains(predicate_declaration)
+				|| output_predicate_declarations.contains(predicate_declaration)
+				// TODO: refactor
+				// Auxiliary predicates may occur anywhere
+				|| predicate_declaration.name.starts_with("p__")
+					&& predicate_declaration.name.ends_with("__")
+			{
+				continue;
+			}
+
+			for (section_key, statements) in self.statements.borrow().iter()
+			{
+				for statement in statements
+				{
+					match statement.kind
+					{
+						crate::problem::StatementKind::CompletedDefinition(_)
+						| crate::problem::StatementKind::IntegrityConstraint => continue,
+						_ => (),
+					}
+
+					if crate::formula_contains_predicate(&statement.formula, predicate_declaration)
+					{
+						return Err(crate::Error::new_predicate_should_not_occur_in_specification(
+							std::rc::Rc::clone(predicate_declaration)));
+					}
+				}
+			}
+		}
+
+		Ok(())
+	}
+
 	pub(crate) fn restrict_to_output_predicates(&mut self) -> Result<(), crate::Error>
 	{
 		let predicate_declarations = self.predicate_declarations.borrow();
diff --git a/src/utils/output_predicates.rs b/src/utils/output_predicates.rs
index 32aa206..7609458 100644
--- a/src/utils/output_predicates.rs
+++ b/src/utils/output_predicates.rs
@@ -1,4 +1,4 @@
-fn formula_contains_predicate(formula: &foliage::Formula,
+pub(crate) fn formula_contains_predicate(formula: &foliage::Formula,
 	predicate_declaration: &foliage::PredicateDeclaration)
 	-> bool
 {