Skip to content

Commit

Permalink
move check for head mismatches to function
Browse files Browse the repository at this point in the history
  • Loading branch information
janheuer committed Nov 21, 2024
1 parent aa1d743 commit 9239bf9
Showing 1 changed file with 11 additions and 4 deletions.
15 changes: 11 additions & 4 deletions src/translating/completion.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,8 @@ pub fn completion(theory: fol::Theory) -> Option<fol::Theory> {
let (definitions, constraints) = components(theory)?;

// Confirm there are no head mismatches
for (_, heads) in heads(&definitions) {
if !heads.iter().all_equal() {
return None;
}
if has_head_mismatches(&definitions) {
return None;
}

// Complete the definitions
Expand All @@ -42,6 +40,15 @@ pub fn completion(theory: fol::Theory) -> Option<fol::Theory> {
Some(fol::Theory { formulas })
}

pub(crate) fn has_head_mismatches(definitions: &Definitions) -> bool {
for (_, heads) in heads(definitions) {
if !heads.iter().all_equal() {
return true;
}
}
false
}

fn heads(definitions: &Definitions) -> IndexMap<fol::Predicate, Vec<&fol::AtomicFormula>> {
let mut result: IndexMap<_, Vec<_>> = IndexMap::new();
for head in definitions.keys() {
Expand Down

0 comments on commit 9239bf9

Please sign in to comment.