Add encode struct_exprt as field concatenation

Author: thomasspriggs

src/solvers/smt2_incremental/struct_encoding.cpp

@@ -2,6 +2,7 @@
 
 #include "struct_encoding.h"
 
+#include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/make_unique.h>
 
@@ -41,6 +42,11 @@ typet struct_encodingt::encode(typet type) const
   return type;
 }
 
+static exprt encode(const struct_exprt &struct_expr)
+{
+  return concatenation_exprt{struct_expr.operands(), struct_expr.type()};
+}
+
 exprt struct_encodingt::encode(exprt expr) const
 {
   std::queue<exprt *> work_queue;
@@ -50,6 +56,8 @@ exprt struct_encodingt::encode(exprt expr) const
     exprt &current = *work_queue.front();
     work_queue.pop();
     current.type() = encode(current.type());
+    if(const auto struct_expr = expr_try_dynamic_cast<struct_exprt>(current))
+      current = ::encode(*struct_expr);
     for(auto &operand : current.operands())
       work_queue.push(&operand);
   }

unit/solvers/smt2_incremental/struct_encoding.cpp

@@ -1,6 +1,7 @@
 // Author: Diffblue Ltd.
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
@@ -71,9 +72,9 @@ TEST_CASE("struct encoding of types", "[core][smt2_incremental]")
 
 TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
 {
-  const struct_union_typet::componentst components{
+  const struct_union_typet::componentst component_types{
     {"green", signedbv_typet{32}}, {"eggs", unsignedbv_typet{16}}};
-  const struct_typet struct_type{components};
+  const struct_typet struct_type{component_types};
   const type_symbolt type_symbol{"my_structt", struct_type, ID_C};
   auto test = struct_encoding_test_environmentt::make();
   test.symbol_table.insert(type_symbol);
@@ -92,4 +93,15 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
     const auto bv_equal = equal_exprt{symbol_expr_as_bv, symbol_expr_as_bv};
     REQUIRE(test.struct_encoding.encode(struct_equal) == bv_equal);
   }
+  SECTION("expression for a struct from list of components")
+  {
+    const symbolt green_ham{"ham", signedbv_typet{32}, ID_C};
+    test.symbol_table.insert(green_ham);
+    const auto forty_two = from_integer(42, unsignedbv_typet{16});
+    const exprt::operandst components{green_ham.symbol_expr(), forty_two};
+    const struct_exprt struct_expr{components, struct_tag};
+    const concatenation_exprt expected_result{
+      {green_ham.symbol_expr(), forty_two}, bv_typet{48}};
+    REQUIRE(test.struct_encoding.encode(struct_expr) == expected_result);
+  }
 }