ITE and binary relations are constant when all operands are constants

This expands the definition of is_constantt to cover if-then-else as
well as binary relations and logic or bit operations. In many, but not,
cases the simplifier will have turned these into simpler constants. The
included regression test is derived from Rust code, where the
intermediate representation (together with constant propagation) will
yield such comparisons.

Author: tautschnig

regression/cbmc/constant_folding3/main.c

@@ -0,0 +1,8 @@
+int main(void)
+{
+  int x;
+  int plus_one_is_null = &x + 1 == (int *)0 ? 1 : 0;
+  __CPROVER_assert(plus_one_is_null != 2, "cannot be 2");
+
+  return 0;
+}

regression/cbmc/constant_folding3/test.desc

@@ -0,0 +1,9 @@
+CORE new-smt-backend
+main.c
+
+^Generated 1 VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/util/expr_util.cpp

@@ -239,8 +239,12 @@ bool is_constantt::is_constant(const exprt &expr) const
     expr.id() == ID_typecast || expr.id() == ID_array_of ||
     expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_array ||
     expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union ||
-    expr.id() == ID_empty_union ||
-    expr.id() == ID_byte_update_big_endian ||
+    expr.id() == ID_empty_union || expr.id() == ID_equal ||
+    expr.id() == ID_notequal || expr.id() == ID_lt || expr.id() == ID_le ||
+    expr.id() == ID_gt || expr.id() == ID_ge || expr.id() == ID_if ||
+    expr.id() == ID_not || expr.id() == ID_and || expr.id() == ID_or ||
+    expr.id() == ID_bitnot || expr.id() == ID_bitand || expr.id() == ID_bitor ||
+    expr.id() == ID_bitxor || expr.id() == ID_byte_update_big_endian ||
     expr.id() == ID_byte_update_little_endian)
   {
     return std::all_of(