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/solvers/flattening/boolbv_quantifier.cpp

@@ -6,13 +6,14 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include "boolbv.h"
-
 #include <util/arith_tools.h>
+#include <util/bitvector_types.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/simplify_expr.h>
 
+#include "boolbv.h"
+
 /// A method to detect equivalence between experts that can contain typecast
 static bool expr_eq(const exprt &expr1, const exprt &expr2)
 {
@@ -174,7 +175,13 @@ static std::optional<exprt> eager_quantifier_instantiation(
 
   const exprt where_simplified = simplify_expr(expr.where(), ns);
 
-  if(where_simplified.is_true() || where_simplified.is_false())
+  if(
+    (where_simplified.is_true() || where_simplified.is_false()) &&
+    (var_expr.type().id() == ID_integer ||
+     var_expr.type().id() == ID_rational || var_expr.type().id() == ID_real ||
+     var_expr.type().id() == ID_bool ||
+     (can_cast_type<bitvector_typet>(var_expr.type()) &&
+      to_bitvector_type(var_expr.type()).get_width() > 0)))
   {
     return where_simplified;
   }

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,33 @@ 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);
+  }
+
+  // the following simplification only holds when the domain is non-empty
+  if(
+    (where.is_false() || where.is_true()) &&
+    std::all_of(
+      expr.variables().begin(),
+      expr.variables().end(),
+      [](const symbol_exprt &v)
+      {
+        return v.type().id() == ID_integer || v.type().id() == ID_rational ||
+               v.type().id() == ID_real || v.type().id() == ID_bool ||
+               (can_cast_type<bitvector_typet>(v.type()) &&
+                to_bitvector_type(v.type()).get_width() > 0);
+      }))
+  {
+    return where;
+  }
+
+  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{});
+  }
+}