Make constant_exprt a nullary_exprt

It should always have been one, and the introduction of
annotated_pointer_constant_exprt makes it possible to implement this.

This highlighted to pieces of dead code: there are not `constant_exprt`
of type `ID_array` for such constant are `array_exprt`;
`goto_trace_constant_pointer_exprt` was never used (though meant to be
what annotated_pointer_constant_exprt now actually is).

Author: tautschnig

src/goto-programs/goto_trace.h

@@ -296,32 +296,4 @@ void show_goto_trace(
   if(cmdline.isset("stack-trace"))                                             \
     options.set_option("stack-trace", true);
 
-/// Variety of constant expression only used in the context of a GOTO trace, to
-/// give both the numeric value and the symbolic value of a pointer,
-/// e.g. numeric value "0xabcd0004" but symbolic value "&some_object + 4". The
-/// numeric value is stored in the `constant_exprt`'s usual value slot (see
-/// \ref constant_exprt::get_value) and the symbolic value is accessed using the
-/// `symbolic_pointer` method introduced by this class.
-class goto_trace_constant_pointer_exprt : public constant_exprt
-{
-public:
-  const exprt &symbolic_pointer() const
-  {
-    return static_cast<const exprt &>(operands()[0]);
-  }
-};
-
-template <>
-inline bool can_cast_expr<goto_trace_constant_pointer_exprt>(const exprt &base)
-{
-  return can_cast_expr<constant_exprt>(base) && base.operands().size() == 1;
-}
-
-inline const goto_trace_constant_pointer_exprt &
-to_goto_trace_constant_pointer_expr(const exprt &expr)
-{
-  PRECONDITION(can_cast_expr<goto_trace_constant_pointer_exprt>(expr));
-  return static_cast<const goto_trace_constant_pointer_exprt &>(expr);
-}
-
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H

src/solvers/flattening/boolbv_constant.cpp

@@ -22,29 +22,7 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
 
   const typet &expr_type=expr.type();
 
-  if(expr_type.id()==ID_array)
-  {
-    std::size_t op_width=width/expr.operands().size();
-    std::size_t offset=0;
-
-    forall_operands(it, expr)
-    {
-      const bvt &tmp=convert_bv(*it);
-
-      DATA_INVARIANT_WITH_DIAGNOSTICS(
-        tmp.size() == op_width,
-        "convert_constant: unexpected operand width",
-        irep_pretty_diagnosticst{expr});
-
-      for(std::size_t j=0; j<op_width; j++)
-        bv[offset+j]=tmp[j];
-
-      offset+=op_width;
-    }
-
-    return bv;
-  }
-  else if(expr_type.id()==ID_string)
+  if(expr_type.id() == ID_string)
   {
     // we use the numbering for strings
     std::size_t number = string_numbering.number(expr.get_value());

src/util/std_expr.h

@@ -2799,11 +2799,11 @@ inline type_exprt &to_type_expr(exprt &expr)
 }
 
 /// \brief A constant literal expression
-class constant_exprt : public expr_protectedt
+class constant_exprt : public nullary_exprt
 {
 public:
   constant_exprt(const irep_idt &_value, typet _type)
-    : expr_protectedt(ID_constant, std::move(_type))
+    : nullary_exprt(ID_constant, std::move(_type))
   {
     set_value(_value);
   }
@@ -2827,6 +2827,11 @@ inline bool can_cast_expr<constant_exprt>(const exprt &base)
   return base.id() == ID_constant;
 }
 
+inline void validate_expr(const constant_exprt &value)
+{
+  validate_operands(value, 0, "Constants must not have operands");
+}
+
 /// \brief Cast an exprt to a \ref constant_exprt
 ///
 /// \a expr must be known to be \ref constant_exprt.