Check that only input predicates are used in assumptions

This commit is contained in:
Patrick Lühne 2020-05-29 17:42:05 +02:00
parent 93db8d02b5
commit 9b6632cc94
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
4 changed files with 78 additions and 0 deletions

View File

@ -27,6 +27,7 @@ pub enum Kind
FormulaNotClosed(std::rc::Rc<crate::VariableDeclarations>), FormulaNotClosed(std::rc::Rc<crate::VariableDeclarations>),
ProgramNotTight(std::rc::Rc<crate::PredicateDeclaration>), ProgramNotTight(std::rc::Rc<crate::PredicateDeclaration>),
PrivatePredicateCycle(std::rc::Rc<crate::PredicateDeclaration>), PrivatePredicateCycle(std::rc::Rc<crate::PredicateDeclaration>),
NoninputPredicateInAssumption(std::rc::Rc<crate::PredicateDeclaration>),
PrivatePredicateInSpecification(std::rc::Rc<crate::PredicateDeclaration>), PrivatePredicateInSpecification(std::rc::Rc<crate::PredicateDeclaration>),
RunVampire, RunVampire,
// TODO: rename to something Vampire-specific // TODO: rename to something Vampire-specific
@ -173,6 +174,13 @@ impl Error
Self::new(Kind::PrivatePredicateCycle(predicate_declaration)) Self::new(Kind::PrivatePredicateCycle(predicate_declaration))
} }
pub(crate) fn new_noninput_predicate_in_assumption(
predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>)
-> Self
{
Self::new(Kind::NoninputPredicateInAssumption(predicate_declaration))
}
pub(crate) fn new_private_predicate_in_specification( pub(crate) fn new_private_predicate_in_specification(
predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>) predicate_declaration: std::rc::Rc<crate::PredicateDeclaration>)
-> Self -> Self
@ -262,6 +270,10 @@ impl std::fmt::Debug for Error
Kind::PrivatePredicateCycle(ref predicate_declaration) => Kind::PrivatePredicateCycle(ref predicate_declaration) =>
write!(formatter, "private recursion involving {}", write!(formatter, "private recursion involving {}",
predicate_declaration.declaration), predicate_declaration.declaration),
Kind::NoninputPredicateInAssumption(ref predicate_declaration) =>
write!(formatter,
"assumption includes {}, which is not an input predicate (consider declaring {} an input predicate)",
predicate_declaration.declaration, predicate_declaration.declaration),
Kind::PrivatePredicateInSpecification(ref predicate_declaration) => Kind::PrivatePredicateInSpecification(ref predicate_declaration) =>
write!(formatter, write!(formatter,
"private predicate {} should not occur in specification (consider declaring it an input or output predicate)", "private predicate {} should not occur in specification (consider declaring it an input or output predicate)",

View File

@ -52,6 +52,34 @@ impl Problem
pub(crate) fn check_consistency(&self, proof_direction: ProofDirection) pub(crate) fn check_consistency(&self, proof_direction: ProofDirection)
-> Result<(), crate::Error> -> Result<(), crate::Error>
{ {
for (_, statements) in self.statements.borrow().iter()
{
for statement in statements
{
match statement.kind
{
crate::problem::StatementKind::Assumption => (),
_ => continue,
}
if let Some(predicate_declaration) =
crate::fold_predicates(&statement.formula, None,
&mut |accumulator, predicate: &crate::Predicate|
{
match accumulator
{
None if !*predicate.declaration.is_input.borrow() =>
Some(std::rc::Rc::clone(&predicate.declaration)),
_ => accumulator,
}
})
{
return Err(crate::Error::new_noninput_predicate_in_assumption(
predicate_declaration));
}
}
}
for predicate_declaration in self.predicate_declarations.borrow().iter() for predicate_declaration in self.predicate_declarations.borrow().iter()
{ {
if predicate_declaration.is_built_in() if predicate_declaration.is_built_in()

View File

@ -2,6 +2,7 @@ mod arithmetic_terms;
mod autoname_variables; mod autoname_variables;
mod closures; mod closures;
mod copy_formula; mod copy_formula;
mod fold_predicates;
mod formula_contains_predicate; mod formula_contains_predicate;
mod variables_in_terms; mod variables_in_terms;
@ -9,6 +10,7 @@ pub(crate) use autoname_variables::*;
pub(crate) use arithmetic_terms::*; pub(crate) use arithmetic_terms::*;
pub(crate) use closures::*; pub(crate) use closures::*;
pub(crate) use copy_formula::*; pub(crate) use copy_formula::*;
pub(crate) use fold_predicates::*;
pub(crate) use formula_contains_predicate::*; pub(crate) use formula_contains_predicate::*;
pub(crate) use variables_in_terms::*; pub(crate) use variables_in_terms::*;

View File

@ -0,0 +1,36 @@
pub(crate) fn fold_predicates<B, F>(formula: &crate::Formula, mut accumulator: B, functor: &mut F)
-> B
where
F: FnMut(B, &crate::Predicate) -> B,
{
use crate::Formula;
match formula
{
Formula::And(arguments)
| Formula::IfAndOnlyIf(arguments)
| Formula::Or(arguments) =>
{
for argument in arguments
{
accumulator = fold_predicates(argument, accumulator, functor);
}
accumulator
},
Formula::Boolean(_)
| Formula::Compare(_) => accumulator,
Formula::Exists(quantified_expression)
| Formula::ForAll(quantified_expression) =>
fold_predicates(&quantified_expression.argument, accumulator, functor),
Formula::Implies(implies) =>
{
accumulator = fold_predicates(&implies.antecedent, accumulator, functor);
accumulator = fold_predicates(&implies.implication, accumulator, functor);
accumulator
},
Formula::Not(argument) => fold_predicates(argument, accumulator, functor),
Formula::Predicate(predicate) => functor(accumulator, &predicate),
}
}