From 0538131b87a6fbbfcad63f4d016f3d790950ff3c Mon Sep 17 00:00:00 2001
From: Tobias Stolzmann <tobias.stolzmann@potassco.com>
Date: Fri, 16 Aug 2024 10:49:31 +0200
Subject: [PATCH 1/2] Add join_nested_quantifiers simplification

---
 src/simplifying/fol/ht.rs | 66 ++++++++++++++++++++++++++++++++++++++-
 1 file changed, 65 insertions(+), 1 deletion(-)

diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs
index 8ebaf929..07c425e0 100644
--- a/src/simplifying/fol/ht.rs
+++ b/src/simplifying/fol/ht.rs
@@ -17,6 +17,7 @@ fn simplify_formula(formula: Formula) -> Formula {
         Box::new(remove_identities),
         Box::new(remove_annihilations),
         Box::new(remove_idempotences),
+        Box::new(join_nested_quantifiers),
     ])
 }
 
@@ -111,9 +112,38 @@ fn remove_idempotences(formula: Formula) -> Formula {
     }
 }
 
+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)
+
+    match formula.unbox() {
+        // forall X ( forall Y F(X,Y) ) => forall X Y F(X,Y)
+        // exists X ( exists Y F(X,Y) ) => exists X Y F(X,Y)
+        UnboxedFormula::QuantifiedFormula {
+            quantification: outer_quantification,
+            formula:
+                Formula::QuantifiedFormula {
+                    quantification: mut inner_quantification,
+                    formula: inner_formula,
+                },
+        } if outer_quantification.quantifier == inner_quantification.quantifier => {
+            let mut variables = outer_quantification.variables;
+            variables.append(&mut inner_quantification.variables);
+            variables.sort();
+            variables.dedup();
+
+            inner_formula.quantify(outer_quantification.quantifier, variables)
+        }
+        x => x.rebox(),
+    }
+}
+
 #[cfg(test)]
 mod tests {
-    use super::simplify_formula;
+    use {
+        super::{join_nested_quantifiers, simplify_formula},
+        crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula},
+    };
 
     #[test]
     fn test_simplify_formula() {
@@ -137,4 +167,38 @@ mod tests {
             )
         }
     }
+
+    #[test]
+    fn test_join_nested_quantifiers() {
+        for (src, target) in [
+            ("exists X (exists Y (X = Y))", "exists X Y (X = Y)"),
+            (
+                "exists X Y ( exists Z ( X < Y and Y < Z ))",
+                "exists X Y Z ( X < Y and Y < Z )",
+            ),
+            (
+                "exists X (exists Y (X = Y and q(Y)))",
+                "exists X Y (X = Y and q(Y))",
+            ),
+            (
+                "exists X (exists X$i (p(X) -> X$i < 1))",
+                "exists X X$i (p(X) -> X$i < 1)",
+            ),
+            (
+                "forall X Y (forall Y Z (p(X,Y) and q(Y,Z)))",
+                "forall X Y Z (p(X,Y) and q(Y,Z))",
+            ),
+            (
+                "forall X (forall Y (forall Z (X = Y = Z)))",
+                "forall X Y Z (X = Y = Z)",
+            ),
+        ] {
+            assert_eq!(
+                src.parse::<Formula>()
+                    .unwrap()
+                    .apply(&mut join_nested_quantifiers),
+                target.parse().unwrap()
+            )
+        }
+    }
 }

From 40c8aab95b7cda3871b8c3a262dc9bffa8b2f88d Mon Sep 17 00:00:00 2001
From: Tobias Stolzmann <tobias.stolzmann@potassco.com>
Date: Fri, 16 Aug 2024 19:02:08 +0200
Subject: [PATCH 2/2] Split tests according to the simplification they review

---
 src/simplifying/fol/ht.rs | 53 +++++++++++++++++++++++++++++++++------
 1 file changed, 46 insertions(+), 7 deletions(-)

diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs
index 07c425e0..45a03f3f 100644
--- a/src/simplifying/fol/ht.rs
+++ b/src/simplifying/fol/ht.rs
@@ -141,28 +141,67 @@ fn join_nested_quantifiers(formula: Formula) -> Formula {
 #[cfg(test)]
 mod tests {
     use {
-        super::{join_nested_quantifiers, simplify_formula},
+        super::{
+            join_nested_quantifiers, remove_annihilations, remove_idempotences, remove_identities,
+            simplify_formula,
+        },
         crate::{convenience::apply::Apply as _, syntax_tree::fol::Formula},
     };
 
     #[test]
-    fn test_simplify_formula() {
+    fn test_simplify() {
+        for (src, target) in [
+            ("#true and #true and a", "a"),
+            ("#true and (#true and a)", "a"),
+        ] {
+            assert_eq!(
+                simplify_formula(src.parse().unwrap()),
+                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"),
+        ] {
+            assert_eq!(
+                src.parse::<Formula>()
+                    .unwrap()
+                    .apply(&mut remove_identities),
+                target.parse().unwrap()
+            )
+        }
+    }
+
+    #[test]
+    fn test_remove_annihilations() {
+        for (src, target) in [
             ("#true or a", "#true"),
             ("a or #true", "#true"),
             ("#false and a", "#false"),
             ("a and #false", "#false"),
-            ("a and a", "a"),
-            ("a or a", "a"),
-            ("#true and #true and a", "a"),
-            ("#true and (#true and a)", "a"),
         ] {
             assert_eq!(
-                simplify_formula(src.parse().unwrap()),
+                src.parse::<Formula>()
+                    .unwrap()
+                    .apply(&mut remove_annihilations),
+                target.parse().unwrap()
+            )
+        }
+    }
+
+    #[test]
+    fn test_remove_idempotences() {
+        for (src, target) in [("a and a", "a"), ("a or a", "a")] {
+            assert_eq!(
+                src.parse::<Formula>()
+                    .unwrap()
+                    .apply(&mut remove_idempotences),
                 target.parse().unwrap()
             )
         }