Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Zach/simplifications #149

Open
wants to merge 8 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
appeasing clippy
ZachJHansen committed Sep 7, 2024
commit b13f0005483852d76dea981712bc3e90c3f66ed6
16 changes: 9 additions & 7 deletions src/simplifying/fol/ht.rs
Original file line number Diff line number Diff line change
@@ -362,15 +362,16 @@ pub fn restrict_quantifier_domain(formula: Formula) -> Formula {
lhs,
rhs,
},
} => match lhs.unbox() {
UnboxedFormula::QuantifiedFormula {
} => {
if let UnboxedFormula::QuantifiedFormula {
quantification:
Quantification {
quantifier: Quantifier::Exists,
variables: inner_vars,
},
formula: inner_formula,
} => {
} = lhs.unbox()
{
let mut replaced = false;
let conjunctive_terms = Formula::conjoin_invert(inner_formula);
for ct in conjunctive_terms.iter() {
@@ -405,9 +406,7 @@ pub fn restrict_quantifier_domain(formula: Formula) -> Formula {
}
}
}

_ => (),
},
}

_ => (),
}
@@ -422,7 +421,10 @@ mod tests {
remove_idempotences, remove_identities, simplify_empty_quantifiers, simplify_formula,
simplify_variable_lists,
},
crate::{convenience::apply::Apply as _, simplifying::fol::ht::restrict_quantifier_domain, syntax_tree::fol::Formula},
crate::{
convenience::apply::Apply as _, simplifying::fol::ht::restrict_quantifier_domain,
syntax_tree::fol::Formula,
},
};

#[test]