diff --git a/src/ast.rs b/src/ast.rs index 63a7cf9..f6a18d0 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -109,7 +109,7 @@ impl PredicateDeclaration *self.is_input.borrow() || *self.is_output.borrow() } - fn collect_transitive_dependencies(&self, + fn collect_transitive_private_dependencies(&self, mut transitive_dependencies: &mut std::collections::BTreeSet< std::rc::Rc>) { @@ -124,22 +124,27 @@ impl PredicateDeclaration for dependency in dependencies.iter() { if transitive_dependencies.contains(&*dependency) + || dependency.is_public() + || dependency.is_built_in() { continue; } transitive_dependencies.insert(std::rc::Rc::clone(&dependency)); - dependency.collect_transitive_dependencies(&mut transitive_dependencies); + dependency.collect_transitive_private_dependencies(&mut transitive_dependencies); } } - pub fn is_self_referential(&self) -> bool + pub fn has_private_dependency_cycle(&self) -> bool { - let mut transitive_dependencies = std::collections::BTreeSet::new(); - self.collect_transitive_dependencies(&mut transitive_dependencies); + if self.is_public() || self.is_built_in() + { + return false; + } - log::debug!("{} depends on {:?}", self.declaration, transitive_dependencies.iter().map(|x| &x.declaration).collect::>()); + let mut transitive_dependencies = std::collections::BTreeSet::new(); + self.collect_transitive_private_dependencies(&mut transitive_dependencies); transitive_dependencies.contains(self) } diff --git a/src/problem.rs b/src/problem.rs index 9012e8e..69597cb 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -68,8 +68,8 @@ impl Problem // 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() - && predicate_declaration.is_self_referential() + if proof_direction.requires_backward_proof() + && predicate_declaration.has_private_dependency_cycle() { return Err(crate::Error::new_private_predicate_cycle( std::rc::Rc::clone(&predicate_declaration)));