From d1e15ce8a9d99de5af9189cbf55a0b2252000258 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Wed, 4 Dec 2024 22:23:23 +0100 Subject: [PATCH 1/6] Add evaluate_comparisons simplification --- src/simplifying/fol/ht.rs | 89 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 86 insertions(+), 3 deletions(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 31207bcc..fb0d50d3 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -3,7 +3,9 @@ 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, Relation, Theory, + }, }; pub fn simplify(theory: Theory) -> Theory { @@ -14,6 +16,7 @@ pub fn simplify(theory: Theory) -> Theory { fn simplify_formula(formula: Formula) -> Formula { formula.apply_all(&mut vec![ + Box::new(evaluate_comparisons), Box::new(remove_identities), Box::new(remove_annihilations), Box::new(remove_idempotences), @@ -21,6 +24,56 @@ fn simplify_formula(formula: Formula) -> Formula { ]) } +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 remove_identities(formula: Formula) -> Formula { // Remove identities // e.g. F op E => F @@ -142,8 +195,8 @@ 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_idempotences, remove_identities, simplify_formula, }, crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula}, }; @@ -161,6 +214,36 @@ 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::() + .unwrap() + .apply(&mut evaluate_comparisons), + target.parse().unwrap() + ) + } + } + #[test] fn test_remove_identities() { for (src, target) in [ From 346eb08c431418ef6370e79749b44172fadc120a Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Wed, 4 Dec 2024 22:41:04 +0100 Subject: [PATCH 2/6] Add apply_definitions simplification --- src/simplifying/fol/ht.rs | 76 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 73 insertions(+), 3 deletions(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index fb0d50d3..78959e0a 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -5,6 +5,7 @@ use crate::{ }, syntax_tree::fol::{ AtomicFormula, BinaryConnective, Comparison, Formula, Guard, Relation, Theory, + UnaryConnective, }, }; @@ -17,6 +18,7 @@ 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), @@ -74,6 +76,55 @@ fn evaluate_comparisons(formula: Formula) -> Formula { } } +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 @@ -195,10 +246,13 @@ pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula { mod tests { use { super::{ - evaluate_comparisons, join_nested_quantifiers, - remove_annihilations, remove_idempotences, remove_identities, simplify_formula, + evaluate_comparisons, join_nested_quantifiers, remove_annihilations, + remove_idempotences, remove_identities, 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] @@ -244,6 +298,22 @@ mod tests { } } + #[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::() + .unwrap() + .apply(&mut apply_definitions), + target.parse().unwrap() + ) + } + } + #[test] fn test_remove_identities() { for (src, target) in [ From 1dddd538ee32b300c0ff8bd489f35040655f8677 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Wed, 4 Dec 2024 22:57:10 +0100 Subject: [PATCH 3/6] Amend the remove_identities simplification with rules for implications --- src/simplifying/fol/ht.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 78959e0a..79c7e695 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -158,6 +158,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(), } } @@ -321,6 +328,7 @@ mod tests { ("a and #true", "a"), ("#false or a", "a"), ("a or #false", "a"), + ("#true -> a", "a"), ] { assert_eq!( src.parse::() From b86a15437586a9d77087c5992a2380ceab5c9b70 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Wed, 4 Dec 2024 23:07:13 +0100 Subject: [PATCH 4/6] Amend the remove_annihilations simplification with rules for implications --- src/simplifying/fol/ht.rs | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 79c7e695..5904c032 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -202,6 +202,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(), } } @@ -346,6 +367,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::() From 7cbb05c863b24454d5c098ef1f85d68544f5293c Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Wed, 20 Nov 2024 19:41:23 +0100 Subject: [PATCH 5/6] Add remove_orphaned_variables simplification --- src/simplifying/fol/ht.rs | 59 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 56 insertions(+), 3 deletions(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 5904c032..569d08f3 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -4,8 +4,8 @@ use crate::{ unbox::{fol::UnboxedFormula, Unbox as _}, }, syntax_tree::fol::{ - AtomicFormula, BinaryConnective, Comparison, Formula, Guard, Relation, Theory, - UnaryConnective, + AtomicFormula, BinaryConnective, Comparison, Formula, Guard, Quantification, Relation, + Theory, UnaryConnective, }, }; @@ -22,6 +22,7 @@ fn simplify_formula(formula: Formula) -> Formula { Box::new(remove_identities), Box::new(remove_annihilations), Box::new(remove_idempotences), + Box::new(remove_orphaned_variables), Box::new(join_nested_quantifiers), ]) } @@ -244,6 +245,39 @@ 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, + } +} + 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) @@ -275,7 +309,7 @@ mod tests { use { super::{ evaluate_comparisons, join_nested_quantifiers, remove_annihilations, - remove_idempotences, remove_identities, simplify_formula, + remove_idempotences, remove_identities, remove_orphaned_variables, simplify_formula, }, crate::{ convenience::apply::Apply as _, simplifying::fol::ht::apply_definitions, @@ -288,6 +322,9 @@ mod tests { 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()), @@ -392,6 +429,22 @@ 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::() + .unwrap() + .apply(&mut remove_orphaned_variables), + target.parse().unwrap() + ) + } + } + #[test] fn test_join_nested_quantifiers() { for (src, target) in [ From 0f5604c790b32495517d8fc81fa15b8bd84f5c6f Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Wed, 4 Dec 2024 23:18:22 +0100 Subject: [PATCH 6/6] Add remove_empty_quantifications simplification --- src/simplifying/fol/ht.rs | 42 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 41 insertions(+), 1 deletion(-) diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 569d08f3..8689f498 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -23,6 +23,7 @@ fn simplify_formula(formula: Formula) -> Formula { Box::new(remove_annihilations), Box::new(remove_idempotences), Box::new(remove_orphaned_variables), + Box::new(remove_empty_quantifications), Box::new(join_nested_quantifiers), ]) } @@ -278,6 +279,21 @@ fn remove_orphaned_variables(formula: Formula) -> Formula { } } +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) @@ -309,7 +325,8 @@ mod tests { use { super::{ evaluate_comparisons, join_nested_quantifiers, remove_annihilations, - remove_idempotences, remove_identities, remove_orphaned_variables, simplify_formula, + remove_empty_quantifications, remove_idempotences, remove_identities, + remove_orphaned_variables, simplify_formula, }, crate::{ convenience::apply::Apply as _, simplifying::fol::ht::apply_definitions, @@ -445,6 +462,29 @@ mod tests { } } + #[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 [