From 491a255811266e436fd32014f5048273d65bfdb1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 28 May 2020 04:54:42 +0200 Subject: [PATCH] Require supertight programs for backward proof --- src/ast.rs | 42 ++++++++ src/commands/verify_program.rs | 10 +- src/error.rs | 37 +++++-- src/problem.rs | 112 ++++++-------------- src/problem/proof_direction.rs | 23 ++++ src/translate/verify_properties.rs | 5 +- src/utils.rs | 4 +- src/utils/collect_predicate_declarations.rs | 91 ++++++++++++++++ 8 files changed, 226 insertions(+), 98 deletions(-) create mode 100644 src/utils/collect_predicate_declarations.rs diff --git a/src/ast.rs b/src/ast.rs index fb5069d..f12dfb6 100644 --- a/src/ast.rs +++ b/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>>>, pub is_input: std::cell::RefCell, pub is_output: std::cell::RefCell, } @@ -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>) + { + 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::>()); + + 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), } diff --git a/src/commands/verify_program.rs b/src/commands/verify_program.rs index bfc32d8..24eded2 100644 --- a/src/commands/verify_program.rs +++ b/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) } } diff --git a/src/error.rs b/src/error.rs index eae125a..4669f8b 100644 --- a/src/error.rs +++ b/src/error.rs @@ -26,8 +26,10 @@ pub enum Kind VariableNameNotAllowed(String), FormulaNotClosed(std::rc::Rc), NoCompletedDefinitionFound(std::rc::Rc), - CannotHidePredicate(std::rc::Rc), - PredicateShouldNotOccurInSpecification(std::rc::Rc), + PrivatePredicateCycle(std::rc::Rc), + PrivatePredicateInSpecification(std::rc::Rc), + PrivatePredicateDependingOnPublicPredicate(std::rc::Rc, + std::rc::Rc), RunVampire, // TODO: rename to something Vampire-specific ProveProgram(Option, 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) -> 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) -> 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, + public_predicate_declaration: std::rc::Rc) + -> Self + { + Self::new(Kind::PrivatePredicateDependingOnPublicPredicate(private_predicate_declaration, + public_predicate_declaration)) } pub(crate) fn new_run_vampire>(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) => { diff --git a/src/problem.rs b/src/problem.rs index 04df4a7..e482272 100644 --- a/src/problem.rs +++ b/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)))?; diff --git a/src/problem/proof_direction.rs b/src/problem/proof_direction.rs index 0f586a9..35b1315 100644 --- a/src/problem/proof_direction.rs +++ b/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 diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index bd9458c..d596447 100644 --- a/src/translate/verify_properties.rs +++ b/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()); diff --git a/src/utils.rs b/src/utils.rs index dff0305..8ac0c0a 100644 --- a/src/utils.rs +++ b/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)] diff --git a/src/utils/collect_predicate_declarations.rs b/src/utils/collect_predicate_declarations.rs new file mode 100644 index 0000000..437457e --- /dev/null +++ b/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>) +{ + 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 +}