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. 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.

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,7 +239,9 @@ 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_empty_union || expr.id() == ID_if ||
+    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_byte_update_big_endian ||
     expr.id() == ID_byte_update_little_endian)
   {