From c3b149a4739acaf17d232790bab1fedbd69f940b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Thu, 28 May 2020 07:06:01 +0200
Subject: [PATCH] Remove incorrect check

---
 src/error.rs   | 17 -----------------
 src/problem.rs | 36 +-----------------------------------
 2 files changed, 1 insertion(+), 52 deletions(-)

diff --git a/src/error.rs b/src/error.rs
index 35a2ed1..07f863a 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -26,8 +26,6 @@ pub enum Kind
 	VariableNameNotAllowed(String),
 	FormulaNotClosed(std::rc::Rc<crate::VariableDeclarations>),
 	PrivatePredicateCycle(std::rc::Rc<crate::PredicateDeclaration>),
-	PrivatePredicateDependingOnPublicPredicate(std::rc::Rc<crate::PredicateDeclaration>,
-		std::rc::Rc<crate::PredicateDeclaration>),
 	RunVampire,
 	// TODO: rename to something Vampire-specific
 	ProveProgram(Option<i32>, String, String),
@@ -166,15 +164,6 @@ impl Error
 		Self::new(Kind::PrivatePredicateCycle(predicate_declaration))
 	}
 
-	pub(crate) fn new_private_predicate_depending_on_public_predicate(
-		private_predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>,
-		public_predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>)
-		-> Self
-	{
-		Self::new(Kind::PrivatePredicateDependingOnPublicPredicate(private_predicate_declaration,
-			public_predicate_declaration))
-	}
-
 	pub(crate) fn new_run_vampire<S: Into<Source>>(source: S) -> Self
 	{
 		Self::new(Kind::RunVampire).with(source)
@@ -255,12 +244,6 @@ impl std::fmt::Debug for Error
 				write!(formatter,
 					"program is not supertight (private predicate {} transitively depends on itself)",
 					predicate_declaration.declaration),
-			Kind::PrivatePredicateDependingOnPublicPredicate(ref private_predicate_declaration,
-				ref public_predicate_declaration) =>
-				write!(formatter,
-					"private predicate {} transitively depends on public predicate {}",
-					private_predicate_declaration.declaration,
-					public_predicate_declaration.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 e073771..a064462 100644
--- a/src/problem.rs
+++ b/src/problem.rs
@@ -52,15 +52,7 @@ impl Problem
 	pub(crate) fn check_consistency(&self, proof_direction: ProofDirection)
 		-> Result<(), crate::Error>
 	{
-		let predicate_declarations = self.predicate_declarations.borrow();
-		let statements = self.statements.borrow();
-		let completed_definitions = match statements.get(&SectionKind::CompletedDefinitions)
-		{
-			Some(completed_definitions) => completed_definitions,
-			None => return Ok(()),
-		};
-
-		for predicate_declaration in predicate_declarations.iter()
+		for predicate_declaration in self.predicate_declarations.borrow().iter()
 		{
 			if predicate_declaration.is_built_in()
 			{
@@ -74,32 +66,6 @@ impl Problem
 				continue;
 			}
 
-			let matching_statement = |statement: &&Statement|
-				match statement.kind
-				{
-					StatementKind::CompletedDefinition(ref other_predicate_declaration) =>
-						predicate_declaration == &*other_predicate_declaration,
-					_ => false,
-				};
-
-			let completed_definition = &completed_definitions.iter()
-				.find(matching_statement)
-				.expect("all predicates should have completed definitions at this point")
-				.formula;
-
-			let dependencies = crate::collect_predicate_declarations(&completed_definition);
-
-			for dependency in dependencies
-			{
-				if !predicate_declaration.is_public() && dependency.is_public()
-				{
-					return Err(
-						crate::Error::new_private_predicate_depending_on_public_predicate(
-							std::rc::Rc::clone(&predicate_declaration),
-							std::rc::Rc::clone(&dependency)));
-				}
-			}
-
 			// If a backward proof is necessary, the program needs to be supertight, that is, no
 			// private predicates may transitively depend on themselves
 			if proof_direction.requires_backward_proof() && !predicate_declaration.is_public()