From 03ed18f42a72d026ae15074d6e1f7b18d3642357 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 24 Mar 2025 15:19:51 +0000
Subject: [PATCH] Simplify quantified expressions over constants

Other simplification rules may turn the where-clause of a quantified
expression into a (Boolean) constant. We can completely remove such
quantified expressions so as not to distract back-ends that may
special-case quantified expressions.

We saw such expressions when working on mlkem-native.
---
 src/util/simplify_expr.cpp         |  4 ++++
 src/util/simplify_expr_boolean.cpp | 22 ++++++++++++++++++++++
 src/util/simplify_expr_class.h     |  4 ++++
 unit/util/simplify_expr.cpp        | 24 ++++++++++++++++++++++++
 4 files changed, 54 insertions(+)

diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 8b14c8cb55e..47b15db05c1 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -3128,6 +3128,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(const exprt &node)
   {
     r = simplify_prophecy_pointer_in_range(*prophecy_pointer_in_range);
   }
+  else if(expr.id() == ID_exists || expr.id() == ID_forall)
+  {
+    r = simplify_quantifier_expr(to_quantifier_expr(expr));
+  }
 
   if(!no_change_join_operands)
     r = changed(r);
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
index 569c91ef837..74a0000748f 100644
--- a/src/util/simplify_expr_boolean.cpp
+++ b/src/util/simplify_expr_boolean.cpp
@@ -377,3 +377,25 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
 
   return unchanged(expr);
 }
+
+simplify_exprt::resultt<>
+simplify_exprt::simplify_quantifier_expr(const quantifier_exprt &expr)
+{
+  const exprt &where = expr.where();
+
+  if(!expr.is_boolean() || !where.is_boolean())
+  {
+    return unchanged(expr);
+  }
+
+  if(where.is_false())
+  {
+    return false_exprt{};
+  }
+  else if(where.is_true())
+  {
+    return true_exprt{};
+  }
+
+  return unchanged(expr);
+}
diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h
index 1a9a1fe2998..8a1a0a3fc7c 100644
--- a/src/util/simplify_expr_class.h
+++ b/src/util/simplify_expr_class.h
@@ -68,6 +68,7 @@ class popcount_exprt;
 class power_exprt;
 class prophecy_pointer_in_range_exprt;
 class prophecy_r_or_w_ok_exprt;
+class quantifier_exprt;
 class refined_string_exprt;
 class shift_exprt;
 class sign_exprt;
@@ -254,6 +255,9 @@ class simplify_exprt
   [[nodiscard]] resultt<>
   simplify_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &);
 
+  /// Try to simplify exists/forall to a constant expression.
+  [[nodiscard]] resultt<> simplify_quantifier_expr(const quantifier_exprt &);
+
   // auxiliary
   bool simplify_if_implies(
     exprt &expr, const exprt &cond, bool truth, bool &new_truth);
diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
index a3a288295f7..4ba152fa694 100644
--- a/unit/util/simplify_expr.cpp
+++ b/unit/util/simplify_expr.cpp
@@ -586,3 +586,27 @@ TEST_CASE("Simplify power", "[core][util]")
       simplify_expr(power_exprt{a, from_integer(1, integer_typet{})}, ns) == a);
   }
 }
+
+TEST_CASE("Simplify quantifier", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  SECTION("Simplification for exists")
+  {
+    symbol_exprt a{"a", integer_typet{}};
+
+    REQUIRE(simplify_expr(exists_exprt{a, false_exprt{}}, ns) == false_exprt{});
+
+    REQUIRE(simplify_expr(exists_exprt{a, true_exprt{}}, ns) == true_exprt{});
+  }
+
+  SECTION("Simplification for forall")
+  {
+    symbol_exprt a{"a", integer_typet{}};
+
+    REQUIRE(simplify_expr(forall_exprt{a, false_exprt{}}, ns) == false_exprt{});
+
+    REQUIRE(simplify_expr(forall_exprt{a, true_exprt{}}, ns) == true_exprt{});
+  }
+}