diff --git a/src/ast.rs b/src/ast.rs index f6a18d0..2c626fb 100644 --- a/src/ast.rs +++ b/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, PredicateDependencySign>; + pub struct PredicateDeclaration { pub declaration: foliage::PredicateDeclaration, - pub dependencies: - std::cell::RefCell>>>, + pub dependencies: std::cell::RefCell>, pub is_input: std::cell::RefCell, pub is_output: std::cell::RefCell, } @@ -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>) { 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>) + { + 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) } } diff --git a/src/error.rs b/src/error.rs index d35018b..61483d9 100644 --- a/src/error.rs +++ b/src/error.rs @@ -25,6 +25,7 @@ pub enum Kind UnknownColorChoice(String), VariableNameNotAllowed(String), FormulaNotClosed(std::rc::Rc), + ProgramNotTight(std::rc::Rc), PrivatePredicateCycle(std::rc::Rc), PrivatePredicateInSpecification(std::rc::Rc), 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) + -> Self + { + Self::new(Kind::ProgramNotTight(predicate_declaration)) + } + pub(crate) fn new_private_predicate_cycle( predicate_declaration: std::rc::Rc) -> 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, diff --git a/src/problem.rs b/src/problem.rs index 89a370a..a92d1e5 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -66,13 +66,20 @@ 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() { - return Err(crate::Error::new_private_predicate_cycle( - std::rc::Rc::clone(&predicate_declaration))); + 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() diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index d596447..a5e4c30 100644 --- a/src/translate/verify_properties.rs +++ b/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, ¶meters_layer)?; + translate_body(rule.body(), self.problem, ¶meters_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 diff --git a/src/translate/verify_properties/translate_body.rs b/src/translate/verify_properties/translate_body.rs index 03fe584..bb3c5ae 100644 --- a/src/translate/verify_properties/translate_body.rs +++ b/src/translate/verify_properties/translate_body.rs @@ -1,6 +1,7 @@ // TODO: rename context pub(crate) fn translate_body_term(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 where C: foliage::FindOrCreateFunctionDeclaration @@ -26,6 +27,32 @@ where |parameter| crate::Term::variable(std::rc::Rc::clone(parameter))) .collect::>(); + 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(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 where C: foliage::FindOrCreateFunctionDeclaration @@ -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(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 where C: foliage::FindOrCreateFunctionDeclaration @@ -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::>() } diff --git a/src/utils.rs b/src/utils.rs index dfe9a86..c032dcd 100644 --- a/src/utils.rs +++ b/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::*; diff --git a/src/utils/collect_predicate_declarations.rs b/src/utils/collect_predicate_declarations.rs deleted file mode 100644 index 437457e..0000000 --- a/src/utils/collect_predicate_declarations.rs +++ /dev/null @@ -1,91 +0,0 @@ -fn collect_predicate_declarations_in_formula(formula: &crate::Formula, - mut predicate_declarations: - &mut std::collections::BTreeSet>) -{ - 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> -{ - 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 -}