Add remove_empty_quantifications simplification

potassco · Dec 4, 2024 · 0f5604c · 0f5604c
1 parent 7cbb05c
commit 0f5604c
Showing 1 changed file with 41 additions and 1 deletion.
diff --git 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 [