Implement extract_bits conversion

This only works so long as the bits to extract are constant values. This
is the same limitation as is present in the old back end. The reason for
this is limitation is due to the way the `extract` operation is defined
in the smtlib version of bitvector theory. It may be possible to work
around this limitation but the work around is unlikely to be trivial.

Author: thomasspriggs

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -733,6 +733,11 @@ static smt_termt convert_expr_to_smt(const extractbit_exprt &extract_bit)
 
 static smt_termt convert_expr_to_smt(const extractbits_exprt &extract_bits)
 {
+  const smt_termt from = convert_expr_to_smt(extract_bits.src());
+  const auto upper_value = numeric_cast<std::size_t>(extract_bits.upper());
+  const auto lower_value = numeric_cast<std::size_t>(extract_bits.lower());
+  if(upper_value && lower_value)
+    return smt_bit_vector_theoryt::extract(*upper_value, *lower_value)(from);
   UNIMPLEMENTED_FEATURE(
     "Generation of SMT formula for extract bits expression: " +
     extract_bits.pretty());

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -819,6 +819,27 @@ SCENARIO(
   }
 }
 
+TEST_CASE(
+  "expr to smt conversion for extract bits expressions",
+  "[core][smt2_incremental]")
+{
+  const typet operand_type = unsignedbv_typet{8};
+  const exprt input = extractbits_exprt{
+    symbol_exprt{"foo", operand_type},
+    from_integer(4, operand_type),
+    from_integer(2, operand_type),
+    unsignedbv_typet{3}};
+  const smt_termt expected_result = smt_bit_vector_theoryt::extract(4, 2)(
+    smt_identifier_termt{"foo", smt_bit_vector_sortt{8}});
+  CHECK(convert_expr_to_smt(input) == expected_result);
+  const cbmc_invariants_should_throwt invariants_throw;
+  CHECK_THROWS(convert_expr_to_smt(extractbits_exprt{
+    symbol_exprt{"foo", operand_type},
+    symbol_exprt{"bar", operand_type},
+    symbol_exprt{"bar", operand_type},
+    unsignedbv_typet{3}}));
+}
+
 TEST_CASE("expr to smt conversion for type casts", "[core][smt2_incremental]")
 {
   const symbol_exprt bool_expr{"foo", bool_typet{}};