Remove unused make_free_bv_expr

This was previously used for encoding `waitfor`, but this is no longer
supported in this code base. With the removal of make_free_bv_expr,
make_bv_expr became unnecessary, and thereby expressions with id
ID_bv_literals can no longer be generated.

Author: tautschnig

src/solvers/flattening/boolbv.cpp

@@ -121,8 +121,6 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
     return convert_bv_typecast(to_typecast_expr(expr));
   else if(expr.id()==ID_symbol)
     return convert_symbol(to_symbol_expr(expr));
-  else if(expr.id()==ID_bv_literals)
-    return convert_bv_literals(expr);
   else if(expr.id()==ID_plus || expr.id()==ID_minus ||
           expr.id()=="no-overflow-plus" ||
           expr.id()=="no-overflow-minus")
@@ -275,27 +273,6 @@ bvt boolbvt::convert_array_comprehension(const array_comprehension_exprt &expr)
   return bv;
 }
 
-bvt boolbvt::convert_bv_literals(const exprt &expr)
-{
-  std::size_t width=boolbv_width(expr.type());
-
-  if(width==0)
-    return conversion_failed(expr);
-
-  bvt bv;
-  bv.resize(width);
-
-  const irept::subt &bv_sub=expr.find(ID_bv).get_sub();
-
-  if(bv_sub.size()!=width)
-    throw "bv_literals with wrong size";
-
-  for(std::size_t i=0; i<width; i++)
-    bv[i].set(unsafe_string2unsigned(id2string(bv_sub[i].id())));
-
-  return bv;
-}
-
 bvt boolbvt::convert_symbol(const exprt &expr)
 {
   const typet &type=expr.type();
@@ -530,25 +507,6 @@ void boolbvt::set_to(const exprt &expr, bool value)
   SUB::set_to(expr, value);
 }
 
-exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv)
-{
-  exprt dest(ID_bv_literals, type);
-  irept::subt &bv_sub=dest.add(ID_bv).get_sub();
-  bv_sub.resize(bv.size());
-
-  for(std::size_t i=0; i<bv.size(); i++)
-    bv_sub[i].id(std::to_string(bv[i].get()));
-  return dest;
-}
-
-exprt boolbvt::make_free_bv_expr(const typet &type)
-{
-  const std::size_t width = boolbv_width(type);
-  PRECONDITION(width != 0);
-  bvt bv = prop.new_variables(width);
-  return make_bv_expr(type, bv);
-}
-
 bool boolbvt::is_unbounded_array(const typet &type) const
 {
   if(type.id()!=ID_array)

src/solvers/flattening/boolbv.h

@@ -187,7 +187,6 @@ class boolbvt:public arrayst
   virtual bvt convert_abs(const abs_exprt &expr);
   virtual bvt convert_concatenation(const concatenation_exprt &expr);
   virtual bvt convert_replication(const replication_exprt &expr);
-  virtual bvt convert_bv_literals(const exprt &expr);
   virtual bvt convert_constant(const constant_exprt &expr);
   virtual bvt convert_extractbits(const extractbits_exprt &expr);
   virtual bvt convert_symbol(const exprt &expr);
@@ -199,9 +198,6 @@ class boolbvt:public arrayst
   virtual bvt convert_bitreverse(const bitreverse_exprt &expr);
   virtual bvt convert_saturating_add_sub(const binary_exprt &expr);
 
-  virtual exprt make_bv_expr(const typet &type, const bvt &bv);
-  virtual exprt make_free_bv_expr(const typet &type);
-
   void convert_with(
     const typet &type,
     const exprt &op1,

src/util/irep_ids.def

@@ -300,7 +300,6 @@ IREP_ID_ONE(KnR)
 IREP_ID_TWO(C_KnR, #KnR)
 IREP_ID_ONE(constraint_select_one)
 IREP_ID_ONE(cond)
-IREP_ID_ONE(bv_literals)
 IREP_ID_ONE(isfinite)
 IREP_ID_ONE(isinf)
 IREP_ID_ONE(isnormal)