From 9b6632cc9479da6cb753600dd0f1e72ed3f40d6b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Fri, 29 May 2020 17:42:05 +0200
Subject: [PATCH] Check that only input predicates are used in assumptions

---
 src/error.rs                 | 12 ++++++++++++
 src/problem.rs               | 28 ++++++++++++++++++++++++++++
 src/utils.rs                 |  2 ++
 src/utils/fold_predicates.rs | 36 ++++++++++++++++++++++++++++++++++++
 4 files changed, 78 insertions(+)
 create mode 100644 src/utils/fold_predicates.rs

diff --git a/src/error.rs b/src/error.rs
index 61483d9..d7e374f 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -27,6 +27,7 @@ pub enum Kind
 	FormulaNotClosed(std::rc::Rc<crate::VariableDeclarations>),
 	ProgramNotTight(std::rc::Rc<crate::PredicateDeclaration>),
 	PrivatePredicateCycle(std::rc::Rc<crate::PredicateDeclaration>),
+	NoninputPredicateInAssumption(std::rc::Rc<crate::PredicateDeclaration>),
 	PrivatePredicateInSpecification(std::rc::Rc<crate::PredicateDeclaration>),
 	RunVampire,
 	// TODO: rename to something Vampire-specific
@@ -173,6 +174,13 @@ impl Error
 		Self::new(Kind::PrivatePredicateCycle(predicate_declaration))
 	}
 
+	pub(crate) fn new_noninput_predicate_in_assumption(
+		predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>)
+		-> Self
+	{
+		Self::new(Kind::NoninputPredicateInAssumption(predicate_declaration))
+	}
+
 	pub(crate) fn new_private_predicate_in_specification(
 		predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>)
 		-> Self
@@ -262,6 +270,10 @@ impl std::fmt::Debug for Error
 			Kind::PrivatePredicateCycle(ref predicate_declaration) =>
 				write!(formatter, "private recursion involving {}",
 					predicate_declaration.declaration),
+			Kind::NoninputPredicateInAssumption(ref predicate_declaration) =>
+				write!(formatter,
+					"assumption includes {}, which is not an input predicate (consider declaring {} an input predicate)",
+					predicate_declaration.declaration, predicate_declaration.declaration),
 			Kind::PrivatePredicateInSpecification(ref predicate_declaration) =>
 				write!(formatter,
 					"private predicate {} should not occur in specification (consider declaring it an input or output predicate)",
diff --git a/src/problem.rs b/src/problem.rs
index a92d1e5..964160e 100644
--- a/src/problem.rs
+++ b/src/problem.rs
@@ -52,6 +52,34 @@ impl Problem
 	pub(crate) fn check_consistency(&self, proof_direction: ProofDirection)
 		-> Result<(), crate::Error>
 	{
+		for (_, statements) in self.statements.borrow().iter()
+		{
+			for statement in statements
+			{
+				match statement.kind
+				{
+					crate::problem::StatementKind::Assumption => (),
+					_ => continue,
+				}
+
+				if let Some(predicate_declaration) =
+					crate::fold_predicates(&statement.formula, None,
+						&mut |accumulator, predicate: &crate::Predicate|
+						{
+							match accumulator
+							{
+								None if !*predicate.declaration.is_input.borrow() =>
+									Some(std::rc::Rc::clone(&predicate.declaration)),
+								_ => accumulator,
+							}
+						})
+				{
+					return Err(crate::Error::new_noninput_predicate_in_assumption(
+						predicate_declaration));
+				}
+			}
+		}
+
 		for predicate_declaration in self.predicate_declarations.borrow().iter()
 		{
 			if predicate_declaration.is_built_in()
diff --git a/src/utils.rs b/src/utils.rs
index c032dcd..f116136 100644
--- a/src/utils.rs
+++ b/src/utils.rs
@@ -2,6 +2,7 @@ mod arithmetic_terms;
 mod autoname_variables;
 mod closures;
 mod copy_formula;
+mod fold_predicates;
 mod formula_contains_predicate;
 mod variables_in_terms;
 
@@ -9,6 +10,7 @@ pub(crate) use autoname_variables::*;
 pub(crate) use arithmetic_terms::*;
 pub(crate) use closures::*;
 pub(crate) use copy_formula::*;
+pub(crate) use fold_predicates::*;
 pub(crate) use formula_contains_predicate::*;
 pub(crate) use variables_in_terms::*;
 
diff --git a/src/utils/fold_predicates.rs b/src/utils/fold_predicates.rs
new file mode 100644
index 0000000..176f165
--- /dev/null
+++ b/src/utils/fold_predicates.rs
@@ -0,0 +1,36 @@
+pub(crate) fn fold_predicates<B, F>(formula: &crate::Formula, mut accumulator: B, functor: &mut F)
+	-> B
+where
+	F: FnMut(B, &crate::Predicate) -> B,
+{
+	use crate::Formula;
+
+	match formula
+	{
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments)
+		| Formula::Or(arguments) =>
+		{
+			for argument in arguments
+			{
+				accumulator = fold_predicates(argument, accumulator, functor);
+			}
+
+			accumulator
+		},
+		Formula::Boolean(_)
+		| Formula::Compare(_) => accumulator,
+		Formula::Exists(quantified_expression)
+		| Formula::ForAll(quantified_expression) =>
+			fold_predicates(&quantified_expression.argument, accumulator, functor),
+		Formula::Implies(implies) =>
+		{
+			accumulator = fold_predicates(&implies.antecedent, accumulator, functor);
+			accumulator = fold_predicates(&implies.implication, accumulator, functor);
+
+			accumulator
+		},
+		Formula::Not(argument) => fold_predicates(argument, accumulator, functor),
+		Formula::Predicate(predicate) => functor(accumulator, &predicate),
+	}
+}