Remove support for vector-typed expressions from back-ends

src/solvers/Makefile

@@ -128,7 +128,6 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/boolbv_unary_minus.cpp \
       flattening/boolbv_union.cpp \
       flattening/boolbv_update.cpp \
-      flattening/boolbv_vector.cpp \
       flattening/boolbv_width.cpp \
       flattening/boolbv_with.cpp \
       flattening/bv_dimacs.cpp \

src/solvers/flattening/boolbv.cpp

@@ -192,8 +192,6 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   }
   else if(expr.id()==ID_array)
     return convert_array(expr);
-  else if(expr.id()==ID_vector)
-    return convert_vector(to_vector_expr(expr));
   else if(expr.id()==ID_complex)
     return convert_complex(to_complex_expr(expr));
   else if(expr.id()==ID_complex_real)

src/solvers/flattening/boolbv.h

@@ -157,7 +157,6 @@ class boolbvt:public arrayst
   virtual bvt convert_if(const if_exprt &expr);
   virtual bvt convert_struct(const struct_exprt &expr);
   virtual bvt convert_array(const exprt &expr);
-  virtual bvt convert_vector(const vector_exprt &expr);
   virtual bvt convert_complex(const complex_exprt &expr);
   virtual bvt convert_complex_real(const complex_real_exprt &expr);
   virtual bvt convert_complex_imag(const complex_imag_exprt &expr);

src/solvers/flattening/boolbv_add_sub.cpp

@@ -21,14 +21,13 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
 
   const typet &type = expr.type();
 
-  if(type.id()!=ID_unsignedbv &&
-     type.id()!=ID_signedbv &&
-     type.id()!=ID_fixedbv &&
-     type.id()!=ID_floatbv &&
-     type.id()!=ID_range &&
-     type.id()!=ID_complex &&
-     type.id()!=ID_vector)
+  if(
+    type.id() != ID_unsignedbv && type.id() != ID_signedbv &&
+    type.id() != ID_fixedbv && type.id() != ID_floatbv &&
+    type.id() != ID_range && type.id() != ID_complex)
+  {
     return conversion_failed(expr);
+  }
 
   std::size_t width=boolbv_width(type);
 
@@ -50,9 +49,8 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
   bool no_overflow=(expr.id()=="no-overflow-plus" ||
                     expr.id()=="no-overflow-minus");
 
-  typet arithmetic_type = (type.id() == ID_vector || type.id() == ID_complex)
-                            ? to_type_with_subtype(type).subtype()
-                            : type;
+  typet arithmetic_type =
+    type.id() == ID_complex ? to_type_with_subtype(type).subtype() : type;
 
   bv_utilst::representationt rep=
     (arithmetic_type.id()==ID_signedbv ||
@@ -68,15 +66,16 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
 
     const bvt &op = convert_bv(*it, width);
 
-    if(type.id()==ID_vector || type.id()==ID_complex)
+    if(type.id() == ID_complex)
     {
       std::size_t sub_width =
         boolbv_width(to_type_with_subtype(type).subtype());
 
-      INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
+      INVARIANT(
+        sub_width != 0, "complex elements shall have nonzero bit width");
       INVARIANT(
         width % sub_width == 0,
-        "total vector bit width shall be a multiple of the element bit width");
+        "total complex bit width shall be a multiple of the element bit width");
 
       std::size_t size=width/sub_width;
       bv.resize(width);
@@ -149,8 +148,7 @@ bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
 
   if(
     type.id() != ID_unsignedbv && type.id() != ID_signedbv &&
-    type.id() != ID_fixedbv && type.id() != ID_complex &&
-    type.id() != ID_vector)
+    type.id() != ID_fixedbv && type.id() != ID_complex)
   {
     return conversion_failed(expr);
   }
@@ -163,9 +161,8 @@ bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
 
   const bool subtract = expr.id() == ID_saturating_minus;
 
-  typet arithmetic_type = (type.id() == ID_vector || type.id() == ID_complex)
-                            ? to_type_with_subtype(type).subtype()
-                            : type;
+  typet arithmetic_type =
+    type.id() == ID_complex ? to_type_with_subtype(type).subtype() : type;
 
   bv_utilst::representationt rep =
     (arithmetic_type.id() == ID_signedbv || arithmetic_type.id() == ID_fixedbv)
@@ -175,15 +172,15 @@ bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
   bvt bv = convert_bv(expr.lhs(), width);
   const bvt &op = convert_bv(expr.rhs(), width);
 
-  if(type.id() != ID_vector && type.id() != ID_complex)
+  if(type.id() != ID_complex)
     return bv_utils.saturating_add_sub(bv, op, subtract, rep);
 
   std::size_t sub_width = boolbv_width(to_type_with_subtype(type).subtype());
 
-  INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
+  INVARIANT(sub_width != 0, "complex elements shall have nonzero bit width");
   INVARIANT(
     width % sub_width == 0,
-    "total vector bit width shall be a multiple of the element bit width");
+    "total complex bit width shall be a multiple of the element bit width");
 
   std::size_t size = width / sub_width;
 

src/solvers/flattening/boolbv_floatbv_op.cpp

@@ -116,7 +116,7 @@ bvt boolbvt::convert_floatbv_op(const ieee_float_op_exprt &expr)
     else
       UNREACHABLE;
   }
-  else if(expr.type().id() == ID_vector || expr.type().id() == ID_complex)
+  else if(expr.type().id() == ID_complex)
   {
     const typet &subtype = to_type_with_subtype(expr.type()).subtype();
 
@@ -129,8 +129,8 @@ bvt boolbvt::convert_floatbv_op(const ieee_float_op_exprt &expr)
 
       DATA_INVARIANT(
         sub_width > 0 && width % sub_width == 0,
-        "width of a vector subtype must be positive and evenly divide the "
-        "width of the vector");
+        "width of a complex subtype must be positive and evenly divide the "
+        "width of the complex expression");
 
       std::size_t size=width/sub_width;
       bvt result_bv;
@@ -160,7 +160,7 @@ bvt boolbvt::convert_floatbv_op(const ieee_float_op_exprt &expr)
 
         INVARIANT(
           sub_result_bv.size() == sub_width,
-          "we constructed a new vector of the right size");
+          "we constructed a new complex of the right size");
         INVARIANT(
           i * sub_width + sub_width - 1 < result_bv.size(),
           "the sub-bitvector fits into the result bitvector");

src/solvers/flattening/boolbv_get.cpp

@@ -153,31 +153,6 @@ exprt boolbvt::bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset)
         bv_get_rec(member, bv, offset),
         type);
     }
-    else if(type.id()==ID_vector)
-    {
-      const std::size_t width = boolbv_width(type);
-
-      const auto &vector_type = to_vector_type(type);
-      const typet &element_type = vector_type.element_type();
-      std::size_t element_width = boolbv_width(element_type);
-      CHECK_RETURN(element_width > 0);
-
-      if(element_width != 0 && width % element_width == 0)
-      {
-        std::size_t size = width / element_width;
-        vector_exprt value({}, vector_type);
-        value.reserve_operands(size);
-
-        for(std::size_t i=0; i<size; i++)
-        {
-          const index_exprt index{expr,
-                                  from_integer(i, vector_type.index_type())};
-          value.operands().push_back(bv_get_rec(index, bv, i * element_width));
-        }
-
-        return std::move(value);
-      }
-    }
     else if(type.id()==ID_complex)
     {
       const std::size_t width = boolbv_width(type);

src/solvers/flattening/boolbv_unary_minus.cpp

@@ -30,8 +30,7 @@ bvt boolbvt::convert_unary_minus(const unary_minus_exprt &expr)
   bvtypet bvtype=get_bvtype(type);
   bvtypet op_bvtype = get_bvtype(op.type());
 
-  if(bvtype==bvtypet::IS_UNKNOWN &&
-     (type.id()==ID_vector || type.id()==ID_complex))
+  if(bvtype == bvtypet::IS_UNKNOWN && type.id() == ID_complex)
   {
     const typet &subtype = to_type_with_subtype(type).subtype();
 

src/solvers/flattening/boolbv_width.cpp

@@ -149,21 +149,6 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     else
       cache_entry = defined_entryt{numeric_cast_v<std::size_t>(total)};
   }
-  else if(type_id==ID_vector)
-  {
-    const vector_typet &vector_type=to_vector_type(type);
-    auto sub_width = get_width_opt(vector_type.element_type());
-    if(!sub_width.has_value())
-      return cache_entry;
-
-    const auto vector_size = numeric_cast_v<mp_integer>(vector_type.size());
-
-    mp_integer total = vector_size * *sub_width;
-    if(total > (1 << 30)) // realistic limit
-      throw analysis_exceptiont("vector too large for flattening");
-    else
-      cache_entry = defined_entryt{numeric_cast_v<std::size_t>(total)};
-  }
   else if(type_id==ID_complex)
   {
     auto sub_width = get_width_opt(to_complex_type(type).subtype());