patrick/anthem-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Detect cyclic dependencies when hiding predicates

Browse Source
This commit is contained in:
Patrick Lühne 2020-05-18 01:19:59 +02:00
parent c0bfbc923c
commit 58d89b4d07
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 32 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/error.rs
View File

@ -23,8 +23,7 @@ pub enum Kind
VariableNameNotAllowed(String),
FormulaNotClosed(std::rc::Rc<foliage::VariableDeclarations>),
NoCompletedDefinitionFound(std::rc::Rc<foliage::PredicateDeclaration>),
CannotHidePredicate(std::rc::Rc<foliage::PredicateDeclaration>,
std::rc::Rc<foliage::PredicateDeclaration>),
CannotHidePredicate(std::rc::Rc<foliage::PredicateDeclaration>),
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<foliage::PredicateDeclaration>,
predicate_declaration_2: std::rc::Rc<foliage::PredicateDeclaration>)
predicate_declaration: std::rc::Rc<foliage::PredicateDeclaration>)
-> Self
{
Self::new(Kind::CannotHidePredicate(predicate_declaration_1, predicate_declaration_2))
Self::new(Kind::CannotHidePredicate(predicate_declaration))
}
pub(crate) fn new_write_tptp_program<S: Into<Source>>(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) =>
{

31
src/utils/output_predicates.rs
View File

@ -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<D>(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);