Merge pull request #7291 from esteffin/esteffin/smt-array-concat

Add conversion for concatenation of bit vector smt2 terms

Author: Enrico Steffinlongo

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -353,6 +353,11 @@ static smt_termt convert_expr_to_smt(
   const concatenation_exprt &concatenation,
   const sub_expression_mapt &converted)
 {
+  if(operands_are_of_type<bitvector_typet>(concatenation))
+  {
+    return convert_multiary_operator_to_terms(
+      concatenation, converted, smt_bit_vector_theoryt::concat);
+  }
   UNIMPLEMENTED_FEATURE(
     "Generation of SMT formula for concatenation expression: " +
     concatenation.pretty());

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1251,6 +1251,35 @@ TEST_CASE(
   }
 }
 
+TEST_CASE(
+  "expr to smt conversion for concatenation_exprt expressions",
+  "[core][smt2_incremental]")
+{
+  auto test =
+    expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64);
+  SECTION("Bit vector types")
+  {
+    const exprt bit_vector_1 =
+      symbol_exprt{"my_bit_vector_1", signedbv_typet{8}};
+    const exprt bit_vector_2 =
+      symbol_exprt{"my_bit_vector_2", signedbv_typet{9}};
+    const exprt bit_vector_3 =
+      symbol_exprt{"my_bit_vector_3", signedbv_typet{10}};
+    const concatenation_exprt concatenation{
+      {bit_vector_1, bit_vector_2, bit_vector_3}, signedbv_typet{27}};
+    INFO("Expression being converted: " + concatenation.pretty(2, 0));
+    const smt_identifier_termt smt_id_1{
+      "my_bit_vector_1", smt_bit_vector_sortt{8}};
+    const smt_identifier_termt smt_id_2{
+      "my_bit_vector_2", smt_bit_vector_sortt{9}};
+    const smt_identifier_termt smt_id_3{
+      "my_bit_vector_3", smt_bit_vector_sortt{10}};
+    const smt_termt expected = smt_bit_vector_theoryt::concat(
+      smt_bit_vector_theoryt::concat(smt_id_1, smt_id_2), smt_id_3);
+    CHECK(test.convert(concatenation) == expected);
+  }
+}
+
 TEST_CASE(
   "expr to smt conversion for extract bits expressions",
   "[core][smt2_incremental]")