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.

Author: tautschnig

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);

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);
+}

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);

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{});
+  }
+}