Require supertight programs for backward proof

src/ast.rs

@@ -86,6 +86,8 @@ impl foliage::flavor::FunctionDeclaration for FunctionDeclaration
 pub struct PredicateDeclaration
 {
 	pub declaration: foliage::PredicateDeclaration,
+	pub dependencies:
+		std::cell::RefCell<Option<std::collections::BTreeSet<std::rc::Rc<PredicateDeclaration>>>>,
 	pub is_input: std::cell::RefCell<bool>,
 	pub is_output: std::cell::RefCell<bool>,
 }
@@ -101,6 +103,45 @@ impl PredicateDeclaration
 	{
 		self.declaration.name.starts_with("p__") && self.declaration.name.ends_with("__")
 	}
+
+	pub fn is_public(&self) -> bool
+	{
+		*self.is_input.borrow() || *self.is_output.borrow()
+	}
+
+	fn collect_transitive_dependencies(&self,
+		mut transitive_dependencies: &mut std::collections::BTreeSet<
+			std::rc::Rc<crate::PredicateDeclaration>>)
+	{
+		let dependencies = self.dependencies.borrow();
+		let dependencies = match *dependencies
+		{
+			Some(ref dependencies) => dependencies,
+			None => unreachable!("all dependencies should have been collected at this point"),
+		};
+
+		for dependency in dependencies.iter()
+		{
+			if transitive_dependencies.contains(&*dependency)
+			{
+				continue;
+			}
+
+			transitive_dependencies.insert(std::rc::Rc::clone(&dependency));
+
+			dependency.collect_transitive_dependencies(&mut transitive_dependencies);
+		}
+	}
+
+	pub fn is_self_referential(&self) -> bool
+	{
+		let mut transitive_dependencies = std::collections::BTreeSet::new();
+		self.collect_transitive_dependencies(&mut transitive_dependencies);
+
+		log::debug!("{} depends on {:?}", self.declaration, transitive_dependencies.iter().map(|x| &x.declaration).collect::<Vec<_>>());
+
+		transitive_dependencies.contains(self)
+	}
 }
 
 impl std::cmp::PartialEq for PredicateDeclaration
@@ -150,6 +191,7 @@ impl foliage::flavor::PredicateDeclaration for PredicateDeclaration
 		Self
 		{
 			declaration: foliage::PredicateDeclaration::new(name, arity),
+			dependencies: std::cell::RefCell::new(None),
 			is_input: std::cell::RefCell::new(false),
 			is_output: std::cell::RefCell::new(false),
 		}

src/commands/verify_program.rs

@@ -45,18 +45,12 @@ where
 		}
 	}
 
-	match problem.check_that_only_input_and_output_predicates_are_used()
-	{
-		Ok(_) => (),
-		Err(error) => log::warn!("{}", error),
-	}
-
-	match problem.restrict_to_output_predicates()
+	match problem.check_consistency(proof_direction)
 	{
 		Ok(_) => (),
 		Err(error) =>
 		{
-			log::error!("could not restrict problem to output predicates: {}", error);
+			log::error!("{}", error);
 			std::process::exit(1)
 		}
 	}

src/error.rs

@@ -26,8 +26,10 @@ pub enum Kind
 	VariableNameNotAllowed(String),
 	FormulaNotClosed(std::rc::Rc<crate::VariableDeclarations>),
 	NoCompletedDefinitionFound(std::rc::Rc<crate::PredicateDeclaration>),
-	CannotHidePredicate(std::rc::Rc<crate::PredicateDeclaration>),
-	PredicateShouldNotOccurInSpecification(std::rc::Rc<crate::PredicateDeclaration>),
+	PrivatePredicateCycle(std::rc::Rc<crate::PredicateDeclaration>),
+	PrivatePredicateInSpecification(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,18 +168,27 @@ impl Error
 		Self::new(Kind::NoCompletedDefinitionFound(predicate_declaration))
 	}
 
-	pub(crate) fn new_cannot_hide_predicate(
+	pub(crate) fn new_private_predicate_cycle(
 		predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>)
 		-> Self
 	{
-		Self::new(Kind::CannotHidePredicate(predicate_declaration))
+		Self::new(Kind::PrivatePredicateCycle(predicate_declaration))
 	}
 
-	pub(crate) fn new_predicate_should_not_occur_in_specification(
+	pub(crate) fn new_private_predicate_in_specification(
 		predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>)
 		-> Self
 	{
-		Self::new(Kind::PredicateShouldNotOccurInSpecification(predicate_declaration))
+		Self::new(Kind::PrivatePredicateInSpecification(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
@@ -258,14 +269,20 @@ impl std::fmt::Debug for Error
 			},
 			Kind::NoCompletedDefinitionFound(ref predicate_declaration) =>
 				write!(formatter, "no completed definition found for {}", predicate_declaration.declaration),
-			Kind::CannotHidePredicate(ref predicate_declaration) =>
+			Kind::PrivatePredicateCycle(ref predicate_declaration) =>
 				write!(formatter,
-					"cannot hide predicate {} (the completed definition transitively depends on itself)",
+					"program is not supertight (private predicate {} transitively depends on itself)",
 					predicate_declaration.declaration),
-			Kind::PredicateShouldNotOccurInSpecification(ref predicate_declaration) =>
+			Kind::PrivatePredicateInSpecification(ref predicate_declaration) =>
 				write!(formatter,
-					"{} should not occur in specification because it’s a private predicate (consider declaring it an input or output predicate)",
+					"private predicate {} should not occur in specification (consider declaring it an input or output predicate)",
 					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) =>
 			{

src/problem.rs

@@ -49,100 +49,60 @@ impl Problem
 		section.push(statement);
 	}
 
-	pub(crate) fn check_that_only_input_and_output_predicates_are_used(&self)
+	pub(crate) fn check_consistency(&self, proof_direction: ProofDirection)
 		-> Result<(), crate::Error>
 	{
 		let predicate_declarations = self.predicate_declarations.borrow();
-
-		if predicate_declarations.iter().find(|x| *x.is_output.borrow()).is_none()
+		let statements = self.statements.borrow();
+		let completed_definitions = match statements.get(&SectionKind::CompletedDefinitions)
 		{
-			return Ok(());
-		}
+			Some(completed_definitions) => completed_definitions,
+			None => return Ok(()),
+		};
 
-		// Check that only input and output predicates are used in the specification
 		for predicate_declaration in predicate_declarations.iter()
 		{
-			if *predicate_declaration.is_input.borrow()
-				|| *predicate_declaration.is_output.borrow()
-				// Auxiliary predicates may occur anywhere
-				|| predicate_declaration.is_built_in()
+			if predicate_declaration.is_built_in()
 			{
+				log::warn!("specification uses built-in predicate {}",
+					predicate_declaration.declaration);
 				continue;
 			}
 
-			for (_, statements) in self.statements.borrow().iter()
-			{
-				for statement in statements
+			let matching_statement = |statement: &&Statement|
+				match statement.kind
 				{
-					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();
-
-		// If no output statements were provided, show all predicates by default
-		if predicate_declarations.iter().find(|x| *x.is_output.borrow()).is_none()
-		{
-			return Ok(());
-		}
-
-		let hidden_predicate_declarations = predicate_declarations.iter()
-			.filter(|x| !*x.is_output.borrow() && !*x.is_input.borrow() && !x.is_built_in());
-
-		let mut statements = self.statements.borrow_mut();
-
-		for hidden_predicate_declaration in hidden_predicate_declarations
-		{
-			let matches_completed_definition =
-				|(_, statement): &(_, &Statement)| match statement.kind
-				{
-					StatementKind::CompletedDefinition(ref predicate_declaration) =>
-						predicate_declaration == hidden_predicate_declaration,
+					StatementKind::CompletedDefinition(ref other_predicate_declaration) =>
+						predicate_declaration == &*other_predicate_declaration,
 					_ => false,
 				};
 
-			let completed_definitions = match statements.get_mut(&SectionKind::CompletedDefinitions)
-			{
-				Some(completed_definitions) => completed_definitions,
-				None => return Ok(()),
-			};
+			let completed_definition = &completed_definitions.iter()
+				.find(matching_statement)
+				.expect("all predicates should have completed definitions at this point")
+				.formula;
 
-			let completed_definition = match completed_definitions.iter().enumerate()
-				.find(matches_completed_definition)
-			{
-				Some((completed_definition_index, _)) =>
-					completed_definitions.remove(completed_definition_index).formula,
-				None => return Err(crate::Error::new_no_completed_definition_found(
-					std::rc::Rc::clone(hidden_predicate_declaration))),
-			};
+			let dependencies = crate::collect_predicate_declarations(&completed_definition);
 
-			drop(completed_definitions);
-
-			for (_, statements) in statements.iter_mut()
+			for dependency in dependencies
 			{
-				for statement in statements.iter_mut()
+				if !predicate_declaration.is_public() && dependency.is_public()
 				{
-					crate::utils::replace_predicate_in_formula_with_completed_definition(
-						&mut statement.formula, &completed_definition)?;
+					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_forward_proof() && !predicate_declaration.is_public()
+				&& predicate_declaration.is_self_referential()
+			{
+				return Err(crate::Error::new_private_predicate_cycle(
+					std::rc::Rc::clone(&predicate_declaration)));
+			}
 		}
 
 		Ok(())
@@ -185,8 +145,7 @@ impl Problem
 
 	pub fn prove(&self, proof_direction: ProofDirection) -> Result<(), crate::Error>
 	{
-		if proof_direction == ProofDirection::Forward
-			|| proof_direction == ProofDirection::Both
+		if proof_direction.requires_forward_proof()
 		{
 			self.print_step_title("Started",
 				termcolor::ColorSpec::new().set_bold(true).set_fg(Some(termcolor::Color::Green)))?;
@@ -238,8 +197,7 @@ impl Problem
 			println!("");
 		}
 
-		if proof_direction == ProofDirection::Backward
-			|| proof_direction == ProofDirection::Both
+		if proof_direction.requires_backward_proof()
 		{
 			self.print_step_title("Started",
 				termcolor::ColorSpec::new().set_bold(true).set_fg(Some(termcolor::Color::Green)))?;

src/problem/proof_direction.rs

@@ -6,6 +6,29 @@ pub enum ProofDirection
 	Both,
 }
 
+impl ProofDirection
+{
+	pub fn requires_forward_proof(&self) -> bool
+	{
+		match self
+		{
+			Self::Forward
+			| Self::Both => true,
+			Self::Backward => false,
+		}
+	}
+
+	pub fn requires_backward_proof(&self) -> bool
+	{
+		match self
+		{
+			Self::Forward => false,
+			Self::Backward
+			| Self::Both => true,
+		}
+	}
+}
+
 impl std::fmt::Debug for ProofDirection
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result

src/translate/verify_properties.rs

@@ -135,7 +135,7 @@ impl<'p> Translator<'p>
 			}
 		};
 
-		for predicate_declaration in self.problem.predicate_declarations.borrow().iter()
+		for predicate_declaration in self.problem.predicate_declarations.borrow_mut().iter()
 		{
 			// Don’t perform completion for input predicates and built-in predicates
 			if *predicate_declaration.is_input.borrow() || predicate_declaration.is_built_in()
@@ -149,6 +149,9 @@ impl<'p> Translator<'p>
 			let completed_definition = completed_definition(predicate_declaration,
 				&mut self.definitions);
 
+			*predicate_declaration.dependencies.borrow_mut() =
+				Some(crate::collect_predicate_declarations(&completed_definition));
+
 			let statement_name =
 				format!("completed_definition_{}", predicate_declaration.tptp_statement_name());
 

src/utils.rs

@@ -1,15 +1,15 @@
 mod arithmetic_terms;
 mod autoname_variables;
 mod closures;
+mod collect_predicate_declarations;
 mod copy_formula;
-mod output_predicates;
 mod variables_in_terms;
 
 pub(crate) use autoname_variables::*;
 pub(crate) use arithmetic_terms::*;
 pub(crate) use closures::*;
+pub(crate) use collect_predicate_declarations::*;
 pub(crate) use copy_formula::*;
-pub(crate) use output_predicates::*;
 pub(crate) use variables_in_terms::*;
 
 #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]

src/utils/collect_predicate_declarations.rs

@@ -0,0 +1,91 @@
+fn collect_predicate_declarations_in_formula(formula: &crate::Formula,
+	mut predicate_declarations:
+		&mut std::collections::BTreeSet<std::rc::Rc<crate::PredicateDeclaration>>)
+{
+	use crate::Formula;
+
+	match formula
+	{
+		Formula::And(ref arguments)
+		| Formula::IfAndOnlyIf(ref arguments)
+		| Formula::Or(ref arguments) =>
+			for argument in arguments
+			{
+				collect_predicate_declarations_in_formula(argument, &mut predicate_declarations);
+			},
+		Formula::Boolean(_)
+		| Formula::Compare(_) => (),
+		Formula::Exists(ref quantified_formula)
+		| Formula::ForAll(ref quantified_formula) =>
+			collect_predicate_declarations_in_formula(&quantified_formula.argument,
+				&mut predicate_declarations),
+		Formula::Implies(ref implies) =>
+		{
+			collect_predicate_declarations_in_formula(&implies.antecedent,
+				&mut predicate_declarations);
+			collect_predicate_declarations_in_formula(&implies.implication,
+				&mut predicate_declarations);
+		},
+		Formula::Not(ref argument) =>
+			collect_predicate_declarations_in_formula(argument, &mut predicate_declarations),
+		Formula::Predicate(ref predicate) =>
+			if !predicate_declarations.contains(&predicate.declaration)
+			{
+				predicate_declarations.insert(std::rc::Rc::clone(&predicate.declaration));
+			},
+	}
+}
+
+pub(crate) fn collect_predicate_declarations(completed_definition: &crate::Formula)
+	-> std::collections::BTreeSet<std::rc::Rc<crate::PredicateDeclaration>>
+{
+	let mut predicate_declarations = std::collections::BTreeSet::new();
+
+	use crate::Formula;
+
+	let false_ = crate::Formula::false_();
+
+	// TODO: refactor
+	let (_completed_definition_predicate, completed_definition) = match completed_definition
+	{
+		Formula::ForAll(quantified_expression) => match *quantified_expression.argument
+		{
+			Formula::IfAndOnlyIf(ref arguments) =>
+			{
+				assert_eq!(arguments.len(), 2, "invalid completed definition");
+
+				match arguments[0]
+				{
+					Formula::Predicate(ref predicate) => (predicate, &arguments[1]),
+					_ => unreachable!("invalid completed definition"),
+				}
+			},
+			Formula::Not(ref argument) => match **argument
+			{
+				Formula::Predicate(ref predicate) => (predicate, &false_),
+				_ => unreachable!("invalid completed definition"),
+			},
+			_ => unreachable!("invalid completed definition"),
+		},
+		Formula::IfAndOnlyIf(ref arguments) =>
+		{
+			assert_eq!(arguments.len(), 2, "invalid completed definition");
+
+			match arguments[0]
+			{
+				Formula::Predicate(ref predicate) => (predicate, &arguments[1]),
+				_ => unreachable!("invalid completed definition"),
+			}
+		},
+		Formula::Not(ref argument) => match **argument
+		{
+			Formula::Predicate(ref predicate) => (predicate, &false_),
+			_ => unreachable!("invalid completed definition"),
+		},
+		_ => unreachable!("invalid completed definition"),
+	};
+
+	collect_predicate_declarations_in_formula(completed_definition, &mut predicate_declarations);
+
+	predicate_declarations
+}