Implement tightness check

src/ast.rs

@@ -83,11 +83,64 @@ impl foliage::flavor::FunctionDeclaration for FunctionDeclaration
 	}
 }
 
+#[derive(Copy, Clone, Eq, PartialEq)]
+pub enum PredicateDependencySign
+{
+	OnlyPositive,
+	OnlyNegative,
+	PositiveAndNegative,
+}
+
+impl PredicateDependencySign
+{
+	pub fn and_positive(self) -> Self
+	{
+		match self
+		{
+			Self::OnlyPositive => Self::OnlyPositive,
+			Self::OnlyNegative
+			| Self::PositiveAndNegative => Self::PositiveAndNegative,
+		}
+	}
+
+	pub fn and_negative(self) -> Self
+	{
+		match self
+		{
+			Self::OnlyNegative => Self::OnlyNegative,
+			Self::OnlyPositive
+			| Self::PositiveAndNegative => Self::PositiveAndNegative,
+		}
+	}
+
+	pub fn is_positive(&self) -> bool
+	{
+		match self
+		{
+			Self::OnlyPositive
+			| Self::PositiveAndNegative => true,
+			Self::OnlyNegative => false,
+		}
+	}
+
+	pub fn is_negative(&self) -> bool
+	{
+		match self
+		{
+			Self::OnlyPositive => false,
+			Self::OnlyNegative
+			| Self::PositiveAndNegative => true,
+		}
+	}
+}
+
+pub type PredicateDependencies =
+	std::collections::BTreeMap<std::rc::Rc<PredicateDeclaration>, PredicateDependencySign>;
+
 pub struct PredicateDeclaration
 {
 	pub declaration: foliage::PredicateDeclaration,
-	pub dependencies:
-		std::cell::RefCell<Option<std::collections::BTreeSet<std::rc::Rc<PredicateDeclaration>>>>,
+	pub dependencies: std::cell::RefCell<Option<PredicateDependencies>>,
 	pub is_input: std::cell::RefCell<bool>,
 	pub is_output: std::cell::RefCell<bool>,
 }
@@ -109,8 +162,8 @@ impl PredicateDeclaration
 		*self.is_input.borrow() || *self.is_output.borrow()
 	}
 
-	fn collect_transitive_private_dependencies(&self,
-		mut transitive_dependencies: &mut std::collections::BTreeSet<
+	fn collect_positive_dependencies(&self,
+		mut positive_dependencies: &mut std::collections::BTreeSet<
 			std::rc::Rc<crate::PredicateDeclaration>>)
 	{
 		let dependencies = self.dependencies.borrow();
@@ -121,21 +174,61 @@ impl PredicateDeclaration
 			None => return,
 		};
 
-		for dependency in dependencies.iter()
+		for (dependency, sign) in dependencies.iter()
 		{
-			if transitive_dependencies.contains(&*dependency)
+			if positive_dependencies.contains(&*dependency)
+				|| dependency.is_built_in()
+				|| !sign.is_positive()
+			{
+				continue;
+			}
+
+			positive_dependencies.insert(std::rc::Rc::clone(dependency));
+
+			dependency.collect_positive_dependencies(&mut positive_dependencies);
+		}
+	}
+
+	fn collect_private_dependencies(&self,
+		mut private_dependencies: &mut std::collections::BTreeSet<
+			std::rc::Rc<crate::PredicateDeclaration>>)
+	{
+		let dependencies = self.dependencies.borrow();
+		let dependencies = match *dependencies
+		{
+			Some(ref dependencies) => dependencies,
+			// Input predicates don’t have completed definitions and no dependencies, so ignore them
+			None => return,
+		};
+
+		for (dependency, _) in dependencies.iter()
+		{
+			if private_dependencies.contains(&*dependency)
 				|| dependency.is_public()
 				|| dependency.is_built_in()
 			{
 				continue;
 			}
 
-			transitive_dependencies.insert(std::rc::Rc::clone(&dependency));
+			private_dependencies.insert(std::rc::Rc::clone(dependency));
 
-			dependency.collect_transitive_private_dependencies(&mut transitive_dependencies);
+			dependency.collect_private_dependencies(&mut private_dependencies);
 		}
 	}
 
+	pub fn has_positive_dependency_cycle(&self) -> bool
+	{
+		if self.is_built_in()
+		{
+			return false;
+		}
+
+		let mut positive_dependencies = std::collections::BTreeSet::new();
+		self.collect_positive_dependencies(&mut positive_dependencies);
+
+		positive_dependencies.contains(self)
+	}
+
 	pub fn has_private_dependency_cycle(&self) -> bool
 	{
 		if self.is_public() || self.is_built_in()
@@ -143,10 +236,10 @@ impl PredicateDeclaration
 			return false;
 		}
 
-		let mut transitive_dependencies = std::collections::BTreeSet::new();
-		self.collect_transitive_private_dependencies(&mut transitive_dependencies);
+		let mut private_dependencies = std::collections::BTreeSet::new();
+		self.collect_private_dependencies(&mut private_dependencies);
 
-		transitive_dependencies.contains(self)
+		private_dependencies.contains(self)
 	}
 }
 

src/error.rs

@@ -25,6 +25,7 @@ pub enum Kind
 	UnknownColorChoice(String),
 	VariableNameNotAllowed(String),
 	FormulaNotClosed(std::rc::Rc<crate::VariableDeclarations>),
+	ProgramNotTight(std::rc::Rc<crate::PredicateDeclaration>),
 	PrivatePredicateCycle(std::rc::Rc<crate::PredicateDeclaration>),
 	PrivatePredicateInSpecification(std::rc::Rc<crate::PredicateDeclaration>),
 	RunVampire,
@@ -158,6 +159,13 @@ impl Error
 		Self::new(Kind::FormulaNotClosed(free_variables))
 	}
 
+	pub(crate) fn new_program_not_tight(
+		predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>)
+		-> Self
+	{
+		Self::new(Kind::ProgramNotTight(predicate_declaration))
+	}
+
 	pub(crate) fn new_private_predicate_cycle(
 		predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>)
 		-> Self
@@ -248,9 +256,11 @@ impl std::fmt::Debug for Error
 
 				write!(formatter, ")")
 			},
+			Kind::ProgramNotTight(ref predicate_declaration) =>
+				write!(formatter, "program not tight (positive recursion involving {})",
+					predicate_declaration.declaration),
 			Kind::PrivatePredicateCycle(ref predicate_declaration) =>
-				write!(formatter,
-					"program is not supertight (private predicate {} transitively depends on itself)",
+				write!(formatter, "private recursion involving {}",
 					predicate_declaration.declaration),
 			Kind::PrivatePredicateInSpecification(ref predicate_declaration) =>
 				write!(formatter,

src/problem.rs

@@ -66,14 +66,21 @@ impl Problem
 				continue;
 			}
 
-			// If a backward proof is necessary, the program needs to be supertight, that is, no
-			// private predicates may transitively depend on themselves
+			// For a backward proof, the program must be tight and free of negative recursion
 			if proof_direction.requires_backward_proof()
-				&& predicate_declaration.has_private_dependency_cycle()
+			{
+				if predicate_declaration.has_positive_dependency_cycle()
+				{
+					return Err(crate::Error::new_program_not_tight(
+						std::rc::Rc::clone(&predicate_declaration)));
+				}
+
+				if predicate_declaration.has_private_dependency_cycle()
 				{
 					return Err(crate::Error::new_private_predicate_cycle(
 						std::rc::Rc::clone(&predicate_declaration)));
 				}
+			}
 
 			if predicate_declaration.is_public()
 			{

src/translate/verify_properties.rs

@@ -149,9 +149,6 @@ 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());
 
@@ -203,8 +200,20 @@ impl<'p> Translator<'p>
 				let parameters_layer =
 					crate::VariableDeclarationStackLayer::bound(&free_layer, parameters);
 
+				let mut predicate_dependencies =
+					head_atom.predicate_declaration.dependencies.borrow_mut();
+
+				if predicate_dependencies.is_none()
+				{
+					*predicate_dependencies = Some(crate::PredicateDependencies::new());
+				}
+
+				// The conditional assignment above ensures unwrapping to be safe
+				let mut dependencies = predicate_dependencies.as_mut().unwrap();
+
 				let mut definition_arguments =
-					translate_body(rule.body(), self.problem, &parameters_layer)?;
+					translate_body(rule.body(), self.problem, &parameters_layer,
+						&mut Some(&mut dependencies))?;
 
 				// TODO: refactor
 				assert_eq!(predicate_definitions.parameters.len(), head_atom.arguments.len());
@@ -263,7 +272,8 @@ impl<'p> Translator<'p>
 				let free_layer =
 					crate::VariableDeclarationStackLayer::Free(free_variable_declarations);
 
-				let mut arguments = translate_body(rule.body(), self.problem, &free_layer)?;
+				let mut arguments = translate_body(rule.body(), self.problem, &free_layer,
+					&mut None)?;
 
 				// TODO: refactor
 				let free_variable_declarations = match free_layer

src/translate/verify_properties/translate_body.rs

@@ -1,6 +1,7 @@
 // TODO: rename context
 pub(crate) fn translate_body_term<C>(body_term: &clingo::ast::Term, sign: clingo::ast::Sign,
-	context: &C, variable_declaration_stack: &crate::VariableDeclarationStackLayer)
+	context: &C, variable_declaration_stack: &crate::VariableDeclarationStackLayer,
+	head_predicate_dependencies: &mut Option<&mut crate::PredicateDependencies>)
 	-> Result<crate::Formula, crate::Error>
 where
 	C: foliage::FindOrCreateFunctionDeclaration<crate::FoliageFlavor>
@@ -26,6 +27,32 @@ where
 		|parameter| crate::Term::variable(std::rc::Rc::clone(parameter)))
 		.collect::<Vec<_>>();
 
+	if let Some(head_predicate_dependencies) = head_predicate_dependencies
+	{
+		match head_predicate_dependencies.get_mut(&predicate_declaration)
+		{
+			None =>
+			{
+				let predicate_dependency_sign = match sign
+				{
+					clingo::ast::Sign::None
+					| clingo::ast::Sign::DoubleNegation => crate::PredicateDependencySign::OnlyPositive,
+					clingo::ast::Sign::Negation => crate::PredicateDependencySign::OnlyNegative,
+				};
+
+				head_predicate_dependencies.insert(
+					std::rc::Rc::clone(&predicate_declaration), predicate_dependency_sign);
+			},
+			Some(predicate_dependency_sign) =>
+				*predicate_dependency_sign = match sign
+				{
+					clingo::ast::Sign::None
+					| clingo::ast::Sign::DoubleNegation => predicate_dependency_sign.and_positive(),
+					clingo::ast::Sign::Negation => predicate_dependency_sign.and_negative(),
+				},
+		}
+	}
+
 	let predicate = crate::Formula::predicate(predicate_declaration, predicate_arguments);
 
 	let predicate_literal = match sign
@@ -59,7 +86,8 @@ where
 }
 
 pub(crate) fn translate_body_literal<C>(body_literal: &clingo::ast::BodyLiteral,
-	context: &C, variable_declaration_stack: &crate::VariableDeclarationStackLayer)
+	context: &C, variable_declaration_stack: &crate::VariableDeclarationStackLayer,
+	head_predicate_dependencies: &mut Option<&mut crate::PredicateDependencies>)
 	-> Result<crate::Formula, crate::Error>
 where
 	C: foliage::FindOrCreateFunctionDeclaration<crate::FoliageFlavor>
@@ -92,7 +120,7 @@ where
 			Ok(crate::Formula::Boolean(value))
 		},
 		clingo::ast::LiteralType::Symbolic(term) => translate_body_term(term, literal.sign(),
-			context, variable_declaration_stack),
+			context, variable_declaration_stack, head_predicate_dependencies),
 		clingo::ast::LiteralType::Comparison(comparison) =>
 		{
 			let parameters = (0..2).map(
@@ -130,7 +158,9 @@ where
 }
 
 pub(crate) fn translate_body<C>(body_literals: &[clingo::ast::BodyLiteral], context: &C,
-	variable_declaration_stack: &crate::VariableDeclarationStackLayer)
+	variable_declaration_stack: &crate::VariableDeclarationStackLayer,
+	// TODO: refactor
+	mut head_predicate_dependencies: &mut Option<&mut crate::PredicateDependencies>)
 	-> Result<crate::Formulas, crate::Error>
 where
 	C: foliage::FindOrCreateFunctionDeclaration<crate::FoliageFlavor>
@@ -138,6 +168,6 @@ where
 {
 	body_literals.iter()
 		.map(|body_literal| translate_body_literal(body_literal, context,
-			variable_declaration_stack))
+			variable_declaration_stack, &mut head_predicate_dependencies))
 		.collect::<Result<crate::Formulas, crate::Error>>()
 }

src/utils.rs

@@ -1,7 +1,6 @@
 mod arithmetic_terms;
 mod autoname_variables;
 mod closures;
-mod collect_predicate_declarations;
 mod copy_formula;
 mod formula_contains_predicate;
 mod variables_in_terms;
@@ -9,7 +8,6 @@ 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 formula_contains_predicate::*;
 pub(crate) use variables_in_terms::*;

src/utils/collect_predicate_declarations.rs

@@ -1,91 +0,0 @@
-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
-}