vector_typet::size() is now a constant_exprt

The codebase assumes basically globally that vector_typet::size() is a
constant_exprt.  This is now enforced by the signature.

Author: Daniel Kroening

src/util/std_types.cpp

@@ -283,3 +283,19 @@ bool is_constant_or_has_constant_components(
 
   return false;
 }
+
+vector_typet::vector_typet(const typet &_subtype, const constant_exprt &_size)
+  : type_with_subtypet(ID_vector, _subtype)
+{
+  size() = _size;
+}
+
+const constant_exprt &vector_typet::size() const
+{
+  return static_cast<const constant_exprt &>(find(ID_size));
+}
+
+constant_exprt &vector_typet::size()
+{
+  return static_cast<constant_exprt &>(add(ID_size));
+}

src/util/std_types.h

@@ -1751,28 +1751,18 @@ inline range_typet &to_range_type(typet &type)
 /// Used to represent the short vectors used by CPU instruction sets such as
 /// MMX, SSE and AVX. They all provide registers that are something like
 /// 8 x int32, for example, and corresponding operations that operate
-/// element-wise on their operand vectors. Compared to \ref array_typet
-/// that has no element-wise operators. Note that `remove_vector.h` removes
-/// this data type by compilation into arrays.
+/// element-wise on their operand vectors. Compared to \ref array_typet,
+/// vector_typet has a fixed size whereas array_typet has no element-wise
+/// operators.
+/// Note that `remove_vector.h` removes this data type by compilation into
+/// arrays.
 class vector_typet:public type_with_subtypet
 {
 public:
-  vector_typet(
-    const typet &_subtype,
-    const exprt &_size):type_with_subtypet(ID_vector, _subtype)
-  {
-    size()=_size;
-  }
+  vector_typet(const typet &_subtype, const constant_exprt &_size);
 
-  const exprt &size() const
-  {
-    return static_cast<const exprt &>(find(ID_size));
-  }
-
-  exprt &size()
-  {
-    return static_cast<exprt &>(add(ID_size));
-  }
+  const constant_exprt &size() const;
+  constant_exprt &size();
 };
 
 /// Check whether a reference to a typet is a \ref vector_typet.

unit/solvers/lowering/byte_operators.cpp

@@ -68,7 +68,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
     unsignedbv_typet u32(32);
     unsignedbv_typet u64(64);
 
-    exprt size = from_integer(8, size_type());
+    constant_exprt size = from_integer(8, size_type());
 
     std::vector<typet> types = {
       struct_typet({{"comp1", u32}, {"comp2", u64}}),
@@ -211,7 +211,7 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
     unsignedbv_typet u32(32);
     unsignedbv_typet u64(64);
 
-    exprt size = from_integer(8, size_type());
+    constant_exprt size = from_integer(8, size_type());
 
     std::vector<typet> types = {
     // TODO: only arrays and scalars