Add remove_orphaned_variables simplification

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::<Formula>()
+                    .unwrap()
+                    .apply(&mut remove_orphaned_variables),
+                target.parse().unwrap()
+            )
+        }
+    }
+
     #[test]
     fn test_join_nested_quantifiers() {
         for (src, target) in [