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.

Sign up for GitHub

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

Add more, hopefully rather uncontroversial simplifications #172

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open

Add more, hopefully rather uncontroversial simplifications #172

Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
d1e15ce
Add evaluate_comparisons simplification
teiesti Dec 4, 2024
346eb08
Add apply_definitions simplification
teiesti Dec 4, 2024
1dddd53
Amend the remove_identities simplification with rules for implications
teiesti Dec 4, 2024
b86a154
Amend the remove_annihilations simplification with rules for implicat…
teiesti Dec 4, 2024
7cbb05c
Add remove_orphaned_variables simplification
teiesti Nov 20, 2024
0f5604c
Add remove_empty_quantifications simplification
teiesti Dec 4, 2024
346c0bd
Merge branch 'master' into tobias/simplifications_part1
ZachJHansen Dec 17, 2024
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
286 changes: 282 additions & 4 deletions src/simplifying/fol/ht.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,10 @@ use crate::{
apply::Apply as _,
unbox::{fol::UnboxedFormula, Unbox as _},
},
syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula, Theory},
syntax_tree::fol::{
AtomicFormula, BinaryConnective, Comparison, Formula, Guard, Quantification, Relation,
Theory, UnaryConnective,
},
};

pub fn simplify(theory: Theory) -> Theory {
Expand All @@ -14,13 +17,116 @@ pub fn simplify(theory: Theory) -> Theory {

fn simplify_formula(formula: Formula) -> Formula {
formula.apply_all(&mut vec![
Box::new(evaluate_comparisons),
Box::new(apply_definitions),
Box::new(remove_identities),
Box::new(remove_annihilations),
Box::new(remove_idempotences),
Box::new(remove_orphaned_variables),
Box::new(remove_empty_quantifications),
Box::new(join_nested_quantifiers),
])
}

fn evaluate_comparisons(formula: Formula) -> Formula {
// Evaluate comparisons between structurally equal terms
// e.g. T = T => #true
// e.g. T != T => #false
// e.g. T1 = T2 = T3 => T1 = T2 and T2 = T3 (side effect)

match formula {
Formula::AtomicFormula(AtomicFormula::Comparison(Comparison { term, guards })) => {
let mut formulas = vec![];

let mut lhs = term;
for Guard {
relation,
term: rhs,
} in guards
{
formulas.push(Formula::AtomicFormula(if lhs == rhs {
match relation {
// T = T => #true
// T >= T => #true
// T <= T => #true
Relation::Equal | Relation::GreaterEqual | Relation::LessEqual => {
AtomicFormula::Truth
}
// T != T => #false
// T > T => #false
// T < T => #false
Relation::NotEqual | Relation::Greater | Relation::Less => {
AtomicFormula::Falsity
}
}
} else {
AtomicFormula::Comparison(Comparison {
term: lhs,
guards: vec![Guard {
relation,
term: rhs.clone(),
}],
})
}));

lhs = rhs;
}

Formula::conjoin(formulas)
}
x => x,
}
}

fn apply_definitions(formula: Formula) -> Formula {
// Apply definitions
// e.g. not F => F -> #false
// e.g. F <- G => G -> F
// e.g. F <-> G => (F -> G) and (G -> F)

match formula.unbox() {
// not F => F -> #false
UnboxedFormula::UnaryFormula {
connective: UnaryConnective::Negation,
formula,
} => Formula::BinaryFormula {
connective: BinaryConnective::Implication,
lhs: formula.into(),
rhs: Formula::AtomicFormula(AtomicFormula::Falsity).into(),
},

// F <- G => G -> F
UnboxedFormula::BinaryFormula {
connective: BinaryConnective::ReverseImplication,
lhs,
rhs,
} => Formula::BinaryFormula {
connective: BinaryConnective::Implication,
lhs: rhs.into(),
rhs: lhs.into(),
},

// F <-> G => (F -> G) and (G -> F)
UnboxedFormula::BinaryFormula {
connective: BinaryConnective::Equivalence,
lhs,
rhs,
} => Formula::conjoin([
Formula::BinaryFormula {
connective: BinaryConnective::Implication,
lhs: lhs.clone().into(),
rhs: rhs.clone().into(),
},
Formula::BinaryFormula {
connective: BinaryConnective::Implication,
lhs: rhs.into(),
rhs: lhs.into(),
},
]),
x => x.rebox(),
}
}

fn remove_identities(formula: Formula) -> Formula {
// Remove identities
// e.g. F op E => F
Expand Down Expand Up @@ -54,6 +160,13 @@ fn remove_identities(formula: Formula) -> Formula {
rhs,
} => rhs,

// #true -> F => F
UnboxedFormula::BinaryFormula {
connective: BinaryConnective::Implication,
lhs: Formula::AtomicFormula(AtomicFormula::Truth),
rhs,
} => rhs,

x => x.rebox(),
}
}
Expand Down Expand Up @@ -91,6 +204,27 @@ fn remove_annihilations(formula: Formula) -> Formula {
rhs: _,
} => lhs,

// F -> #true => #true
UnboxedFormula::BinaryFormula {
connective: BinaryConnective::Implication,
lhs: _,
rhs: rhs @ Formula::AtomicFormula(AtomicFormula::Truth),
} => rhs,

// #false -> F => #true
UnboxedFormula::BinaryFormula {
connective: BinaryConnective::Implication,
lhs: Formula::AtomicFormula(AtomicFormula::Falsity),
rhs: _,
} => Formula::AtomicFormula(AtomicFormula::Truth),

// F -> F => #true
UnboxedFormula::BinaryFormula {
connective: BinaryConnective::Implication,
lhs,
rhs,
} if lhs == rhs => Formula::AtomicFormula(AtomicFormula::Truth),

x => x.rebox(),
}
}
Expand All @@ -112,6 +246,54 @@ fn remove_idempotences(formula: Formula) -> Formula {
}
}

fn remove_orphaned_variables(formula: Formula) -> Formula {
// Remove orphaned variables in quantification
// e.g. q X Y F(X) => q X F(X)

match formula {
// forall X Y F(X) => forall X F(X)
// exists X Y F(X) => exists X F(X)
Formula::QuantifiedFormula {
quantification:
Quantification {
quantifier,
variables,
},
formula,
} => {
let free_variables = formula.free_variables();
let variables = variables
.into_iter()
.filter(|v| free_variables.contains(v))
.collect();

Formula::QuantifiedFormula {
quantification: Quantification {
quantifier,
variables,
},
formula,
}
}
x => x,
}
}

fn remove_empty_quantifications(formula: Formula) -> Formula {
// Remove empty quantifiers
// e.g. q F => F

match formula {
// forall F => F
// exists F => F
Formula::QuantifiedFormula {
quantification,
formula,
} if quantification.variables.is_empty() => *formula,
x => x,
}
}

pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula {
// Remove nested quantifiers
// e.g. q X ( q Y F(X,Y) ) => q X Y F(X,Y)
Expand Down Expand Up @@ -142,17 +324,24 @@ pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula {
mod tests {
use {
super::{
join_nested_quantifiers, remove_annihilations, remove_idempotences, remove_identities,
simplify_formula,
evaluate_comparisons, join_nested_quantifiers, remove_annihilations,
remove_empty_quantifications, remove_idempotences, remove_identities,
remove_orphaned_variables, simplify_formula,
},
crate::{
convenience::apply::Apply as _, simplifying::fol::ht::apply_definitions,
syntax_tree::fol::Formula,
},
crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula},
};

#[test]
fn test_simplify() {
for (src, target) in [
("#true and #true and a", "a"),
("#true and (#true and a)", "a"),
("forall X a", "a"),
("X = X and a", "a"),
("forall X (X = X)", "#true"),
] {
assert_eq!(
simplify_formula(src.parse().unwrap()),
Expand All @@ -161,13 +350,60 @@ mod tests {
}
}

#[test]
fn test_evaluate_comparisons() {
for (src, target) in [
("X = X", "#true"),
("X = Y", "X = Y"),
("X != X", "#false"),
("X != Y", "X != Y"),
("X > X", "#false"),
("X > Y", "X > Y"),
("X < X", "#false"),
("X < Y", "X < Y"),
("X >= X", "#true"),
("X >= Y", "X >= Y"),
("X <= X", "#true"),
("X <= Y", "X <= Y"),
("X$i + 1 = X$i + 1", "#true"),
("X$i + 1 + 1 = X$i + 2", "X$i + 1 + 1 = X$i + 2"),
("X = X = Y", "#true and X = Y"),
("X != X = Y", "#false and X = Y"),
("X = Y = Z", "X = Y and Y = Z"),
] {
assert_eq!(
src.parse::<Formula>()
.unwrap()
.apply(&mut evaluate_comparisons),
target.parse().unwrap()
)
}
}

#[test]
fn test_apply_definitions() {
for (src, target) in [
("not f", "f -> #false"),
("f <- g", "g -> f"),
("f <-> g", "(f -> g) and (g -> f)"),
] {
assert_eq!(
src.parse::<Formula>()
.unwrap()
.apply(&mut apply_definitions),
target.parse().unwrap()
)
}
}

#[test]
fn test_remove_identities() {
for (src, target) in [
("#true and a", "a"),
("a and #true", "a"),
("#false or a", "a"),
("a or #false", "a"),
("#true -> a", "a"),
] {
assert_eq!(
src.parse::<Formula>()
Expand All @@ -185,6 +421,9 @@ mod tests {
("a or #true", "#true"),
("#false and a", "#false"),
("a and #false", "#false"),
("a -> #true", "#true"),
("#false -> a", "#true"),
("a -> a", "#true"),
] {
assert_eq!(
src.parse::<Formula>()
Expand All @@ -207,6 +446,45 @@ mod tests {
}
}

#[test]
fn test_remove_orphaned_variables() {
for (src, target) in [
("forall X Y Z (X = X)", "forall X (X = X)"),
("exists X Y (X = Y)", "exists X Y (X = Y)"),
("exists X Y Z (X = Y)", "exists X Y (X = Y)"),
] {
assert_eq!(
src.parse::<Formula>()
.unwrap()
.apply(&mut remove_orphaned_variables),
target.parse().unwrap()
)
}
}

#[test]
fn test_remove_empty_quantifications() {
use crate::syntax_tree::fol::{Atom, AtomicFormula, Quantification, Quantifier};

let src = Formula::QuantifiedFormula {
quantification: Quantification {
quantifier: Quantifier::Forall,
variables: vec![],
},
formula: Box::new(Formula::AtomicFormula(AtomicFormula::Atom(Atom {
predicate_symbol: "a".into(),
terms: vec![],
}))),
};

let target = Formula::AtomicFormula(AtomicFormula::Atom(Atom {
predicate_symbol: "a".into(),
terms: vec![],
}));

assert_eq!(src.apply(&mut remove_empty_quantifications), target);
}

#[test]
fn test_join_nested_quantifiers() {
for (src, target) in [
Expand Down
Loading