From b52ca236e23ab00e3ef0ad592a9bb67fc27c6c9d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 28 May 2020 07:27:29 +0200 Subject: [PATCH] Handle private predicates in specification --- src/commands/verify_program.rs | 14 ++- src/error.rs | 12 ++ src/problem.rs | 25 +++++ src/utils.rs | 2 + src/utils/formula_contains_predicate.rs | 25 +++++ src/utils/output_predicates.rs | 140 ------------------------ 6 files changed, 76 insertions(+), 142 deletions(-) create mode 100644 src/utils/formula_contains_predicate.rs delete mode 100644 src/utils/output_predicates.rs diff --git a/src/commands/verify_program.rs b/src/commands/verify_program.rs index 58c320e..26244f8 100644 --- a/src/commands/verify_program.rs +++ b/src/commands/verify_program.rs @@ -39,8 +39,18 @@ where if let Err(error) = problem.check_consistency(proof_direction) { - log::error!("{}", error); - std::process::exit(1) + match error.kind + { + // In forward proofs, it’s okay to use private predicates in the specification, but + // issue a warning regardless + crate::error::Kind::PrivatePredicateInSpecification(_) + if !proof_direction.requires_backward_proof() => log::warn!("{}", error), + _ => + { + log::error!("{}", error); + std::process::exit(1) + }, + } } if !no_simplify diff --git a/src/error.rs b/src/error.rs index 07f863a..d35018b 100644 --- a/src/error.rs +++ b/src/error.rs @@ -26,6 +26,7 @@ pub enum Kind VariableNameNotAllowed(String), FormulaNotClosed(std::rc::Rc), PrivatePredicateCycle(std::rc::Rc), + PrivatePredicateInSpecification(std::rc::Rc), RunVampire, // TODO: rename to something Vampire-specific ProveProgram(Option, String, String), @@ -164,6 +165,13 @@ impl Error Self::new(Kind::PrivatePredicateCycle(predicate_declaration)) } + pub(crate) fn new_private_predicate_in_specification( + predicate_declaration: std::rc::Rc) + -> Self + { + Self::new(Kind::PrivatePredicateInSpecification(predicate_declaration)) + } + pub(crate) fn new_run_vampire>(source: S) -> Self { Self::new(Kind::RunVampire).with(source) @@ -244,6 +252,10 @@ impl std::fmt::Debug for Error write!(formatter, "program is not supertight (private predicate {} transitively depends on itself)", predicate_declaration.declaration), + Kind::PrivatePredicateInSpecification(ref predicate_declaration) => + write!(formatter, + "private predicate {} should not occur in specification (consider declaring it an input or output predicate)", + 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 a064462..9012e8e 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -74,6 +74,31 @@ impl Problem return Err(crate::Error::new_private_predicate_cycle( std::rc::Rc::clone(&predicate_declaration))); } + + if predicate_declaration.is_public() + { + continue; + } + + for (_, statements) in self.statements.borrow().iter() + { + for statement in statements + { + match statement.kind + { + crate::problem::StatementKind::CompletedDefinition(_) + | crate::problem::StatementKind::IntegrityConstraint + | crate::problem::StatementKind::Lemma(_) => continue, + _ => (), + } + + if crate::formula_contains_predicate(&statement.formula, predicate_declaration) + { + return Err(crate::Error::new_private_predicate_in_specification( + std::rc::Rc::clone(predicate_declaration))); + } + } + } } Ok(()) diff --git a/src/utils.rs b/src/utils.rs index 8ac0c0a..dfe9a86 100644 --- a/src/utils.rs +++ b/src/utils.rs @@ -3,6 +3,7 @@ mod autoname_variables; mod closures; mod collect_predicate_declarations; mod copy_formula; +mod formula_contains_predicate; mod variables_in_terms; pub(crate) use autoname_variables::*; @@ -10,6 +11,7 @@ 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::*; #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)] diff --git a/src/utils/formula_contains_predicate.rs b/src/utils/formula_contains_predicate.rs new file mode 100644 index 0000000..ec38492 --- /dev/null +++ b/src/utils/formula_contains_predicate.rs @@ -0,0 +1,25 @@ +pub(crate) fn formula_contains_predicate(formula: &crate::Formula, + predicate_declaration: &crate::PredicateDeclaration) + -> bool +{ + use crate::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, + } +} diff --git a/src/utils/output_predicates.rs b/src/utils/output_predicates.rs deleted file mode 100644 index b8f6cd7..0000000 --- a/src/utils/output_predicates.rs +++ /dev/null @@ -1,140 +0,0 @@ -pub(crate) fn formula_contains_predicate(formula: &crate::Formula, - predicate_declaration: &crate::PredicateDeclaration) - -> bool -{ - use crate::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 crate::Formula, - predicate_to_replace: &crate::Predicate, replacement_formula: &crate::Formula) -{ - use crate::{Formula, Term}; - - match formula - { - Formula::And(arguments) - | Formula::IfAndOnlyIf(arguments) - | Formula::Or(arguments) => - for mut argument in arguments - { - replace_predicate_in_formula(&mut argument, predicate_to_replace, - replacement_formula); - }, - Formula::Boolean(_) - | Formula::Compare(_) => (), - Formula::Exists(quantified_expression) - | Formula::ForAll(quantified_expression) => - replace_predicate_in_formula(&mut quantified_expression.argument, predicate_to_replace, - replacement_formula), - Formula::Implies(implies) => - { - replace_predicate_in_formula(&mut implies.antecedent, predicate_to_replace, - replacement_formula); - replace_predicate_in_formula(&mut implies.implication, predicate_to_replace, - replacement_formula); - }, - Formula::Not(argument) => - replace_predicate_in_formula(argument, predicate_to_replace, replacement_formula), - Formula::Predicate(predicate) => - if predicate.declaration == predicate_to_replace.declaration - { - let mut replacement_formula = crate::utils::copy_formula(replacement_formula); - - for (index, argument) in predicate.arguments.iter().enumerate() - { - let variable_declaration = match &predicate_to_replace.arguments[index] - { - Term::Variable(variable) => &variable.declaration, - _ => panic!("invalid completed definition"), - }; - - crate::utils::replace_variable_in_formula_with_term(&mut replacement_formula, - &variable_declaration, argument); - } - - *formula = replacement_formula; - }, - } -} - -pub(crate) fn replace_predicate_in_formula_with_completed_definition( - formula: &mut crate::Formula, completed_definition: &crate::Formula) - -> Result<(), crate::Error> -{ - 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]), - _ => panic!("invalid completed definition"), - } - }, - Formula::Not(ref argument) => match **argument - { - Formula::Predicate(ref predicate) => (predicate, &false_), - _ => panic!("invalid completed definition"), - }, - _ => panic!("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]), - _ => panic!("invalid completed definition"), - } - }, - Formula::Not(ref argument) => match **argument - { - Formula::Predicate(ref predicate) => (predicate, &false_), - _ => panic!("invalid completed definition"), - }, - _ => panic!("invalid completed definition"), - }; - - // 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, &completed_definition_predicate.declaration) - && formula_contains_predicate(formula, &completed_definition_predicate.declaration) - { - 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); - - Ok(()) -}