use zero_extend_exprt in SMT2 front-end

This replaces the use of a typecast expression by zero_extend_exprt when
parsing an SMT-LIB2 zero_extend expression.

Author: kroening

src/solvers/smt2/smt2_parser.cpp

@@ -656,7 +656,7 @@ exprt smt2_parsert::function_application()
           if(next_token() != smt2_tokenizert::NUMERAL)
             throw error() << "expected numeral after " << id;
 
-          auto index = std::stoll(smt2_tokenizer.get_buffer());
+          auto index = string2integer(smt2_tokenizer.get_buffer());
 
           if(next_token() != smt2_tokenizert::CLOSE)
             throw error() << "expected ')' after " << id << " index";
@@ -681,9 +681,9 @@ exprt smt2_parsert::function_application()
             // we first convert to a signed type of the original width,
             // then extend to the new width, and then go to unsigned
             const auto width = to_unsignedbv_type(op[0].type()).get_width();
-            const signedbv_typet small_signed_type(width);
-            const signedbv_typet large_signed_type(width + index);
-            const unsignedbv_typet unsigned_type(width + index);
+            const signedbv_typet small_signed_type{width};
+            const signedbv_typet large_signed_type{width + index};
+            const unsignedbv_typet unsigned_type{width + index};
 
             return typecast_exprt(
               typecast_exprt(
@@ -693,9 +693,9 @@ exprt smt2_parsert::function_application()
           else if(id=="zero_extend")
           {
             auto width=to_unsignedbv_type(op[0].type()).get_width();
-            unsignedbv_typet unsigned_type(width+index);
+            unsignedbv_typet unsigned_type{width + index};
 
-            return typecast_exprt(op[0], unsigned_type);
+            return zero_extend_exprt{op[0], unsigned_type};
           }
           else if(id == ID_repeat)
           {

src/util/bitvector_types.h

@@ -107,6 +107,11 @@ class integer_bitvector_typet : public bitvector_typet
   {
   }
 
+  integer_bitvector_typet(const irep_idt &id, const mp_integer &width)
+    : bitvector_typet(id, width)
+  {
+  }
+
   /// Return the smallest value that can be represented using this type.
   mp_integer smallest() const;
   /// Return the largest value that can be represented using this type.
@@ -167,6 +172,11 @@ class unsignedbv_typet : public integer_bitvector_typet
   {
   }
 
+  explicit unsignedbv_typet(const mp_integer width)
+    : integer_bitvector_typet(ID_unsignedbv, width)
+  {
+  }
+
   static void check(
     const typet &type,
     const validation_modet vm = validation_modet::INVARIANT)
@@ -216,6 +226,11 @@ class signedbv_typet : public integer_bitvector_typet
   {
   }
 
+  explicit signedbv_typet(const mp_integer &width)
+    : integer_bitvector_typet(ID_signedbv, width)
+  {
+  }
+
   static void check(
     const typet &type,
     const validation_modet vm = validation_modet::INVARIANT)