From 58d89b4d0759831da179820c34eda2f6c27ee9ba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Mon, 18 May 2020 01:19:59 +0200 Subject: [PATCH] Detect cyclic dependencies when hiding predicates --- src/error.rs | 15 +++++++-------- src/utils/output_predicates.rs | 31 +++++++++++++++++++++++++------ 2 files changed, 32 insertions(+), 14 deletions(-) diff --git a/src/error.rs b/src/error.rs index ea3e06f..bba0259 100644 --- a/src/error.rs +++ b/src/error.rs @@ -23,8 +23,7 @@ pub enum Kind VariableNameNotAllowed(String), FormulaNotClosed(std::rc::Rc), NoCompletedDefinitionFound(std::rc::Rc), - CannotHidePredicate(std::rc::Rc, - std::rc::Rc), + CannotHidePredicate(std::rc::Rc), WriteTPTPProgram, RunVampire, // TODO: rename to something Vampire-specific @@ -159,11 +158,10 @@ impl Error } pub(crate) fn new_cannot_hide_predicate( - predicate_declaration_1: std::rc::Rc, - predicate_declaration_2: std::rc::Rc) + predicate_declaration: std::rc::Rc) -> Self { - Self::new(Kind::CannotHidePredicate(predicate_declaration_1, predicate_declaration_2)) + Self::new(Kind::CannotHidePredicate(predicate_declaration)) } pub(crate) fn new_write_tptp_program>(source: S) -> Self @@ -239,9 +237,10 @@ impl std::fmt::Debug for Error }, Kind::NoCompletedDefinitionFound(ref predicate_declaration) => write!(formatter, "no completed definition found for {}", predicate_declaration), - Kind::CannotHidePredicate(ref predicate_declaration_1, ref predicate_declaration_2) => - write!(formatter, "cannot hide predicate {} because it depends on {}", - predicate_declaration_1, predicate_declaration_2), + Kind::CannotHidePredicate(ref predicate_declaration) => + write!(formatter, + "cannot hide predicate {} (the completed definition transitively depends on itself)", + predicate_declaration), Kind::RunVampire => write!(formatter, "could not run Vampire"), Kind::ProveProgram(exit_code, ref stdout, ref stderr) => { diff --git a/src/utils/output_predicates.rs b/src/utils/output_predicates.rs index 0ba885e..32aa206 100644 --- a/src/utils/output_predicates.rs +++ b/src/utils/output_predicates.rs @@ -2,7 +2,26 @@ fn formula_contains_predicate(formula: &foliage::Formula, predicate_declaration: &foliage::PredicateDeclaration) -> bool { - unimplemented!() + use foliage::Formula; + + match formula + { + Formula::And(arguments) + | Formula::IfAndOnlyIf(arguments) + | Formula::Or(arguments) => + arguments.iter().any( + |argument| formula_contains_predicate(argument, predicate_declaration)), + Formula::Boolean(_) + | Formula::Compare(_) => false, + Formula::Exists(quantified_expression) + | Formula::ForAll(quantified_expression) => + formula_contains_predicate(&quantified_expression.argument, predicate_declaration), + Formula::Implies(implies) => + formula_contains_predicate(&implies.antecedent, predicate_declaration) + || formula_contains_predicate(&implies.implication, predicate_declaration), + Formula::Not(argument) => formula_contains_predicate(argument, predicate_declaration), + Formula::Predicate(predicate) => &*predicate.declaration == predicate_declaration, + } } fn replace_predicate_in_formula(formula: &mut foliage::Formula, @@ -113,12 +132,12 @@ where // Predicates can only be substituted by their completed definitions if there is no cycle. // For example, if the completed definition of p/1 references q/1 and vice versa, neither can // be replaced with the completed definition of the other - /*if formula_contains_predicate(completed_definition, predicate_declaration) + if formula_contains_predicate(completed_definition, &completed_definition_predicate.declaration) + && formula_contains_predicate(formula, &completed_definition_predicate.declaration) { - return Err(crate::Error::new()) - }*/ - - // TODO: detect cycles and warn accordingly + return Err(crate::Error::new_cannot_hide_predicate( + std::rc::Rc::clone(&completed_definition_predicate.declaration))); + } replace_predicate_in_formula(formula, completed_definition_predicate, completed_definition, declarations);