Add SMT bit vector theory concatenation

Author: thomasspriggs

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -4,6 +4,34 @@
 
 #include <util/invariant.h>
 
+const char *smt_bit_vector_theoryt::concatt::identifier()
+{
+  return "concat";
+}
+
+smt_sortt smt_bit_vector_theoryt::concatt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  const auto get_width = [](const smt_termt &term) {
+    return term.get_sort().cast<smt_bit_vector_sortt>()->bit_width();
+  };
+  return smt_bit_vector_sortt{get_width(lhs) + get_width(rhs)};
+}
+
+void smt_bit_vector_theoryt::concatt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  const auto lhs_sort = lhs.get_sort().cast<smt_bit_vector_sortt>();
+  INVARIANT(lhs_sort, "Left operand must have bitvector sort.");
+  const auto rhs_sort = rhs.get_sort().cast<smt_bit_vector_sortt>();
+  INVARIANT(rhs_sort, "Right operand must have bitvector sort.");
+}
+
+const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::concatt>
+  smt_bit_vector_theoryt::concat{};
+
 const char *smt_bit_vector_theoryt::extractt::identifier()
 {
   return "extract";

src/solvers/smt2_incremental/smt_bit_vector_theory.h

@@ -8,6 +8,14 @@
 class smt_bit_vector_theoryt
 {
 public:
+  struct concatt final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<concatt> concat;
+
   struct extractt final
   {
     std::size_t i;

unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -7,6 +7,32 @@
 
 #include <util/mp_arith.h>
 
+TEST_CASE("SMT bit vector concatenation", "[core][smt2_incremental]")
+{
+  const smt_bit_vector_constant_termt a_valid{42, 8}, b_valid{42, 16};
+  SECTION("Valid operands")
+  {
+    const auto concat = smt_bit_vector_theoryt::concat(a_valid, b_valid);
+    const auto expected_return_sort = smt_bit_vector_sortt{24};
+    REQUIRE(
+      concat.function_identifier() ==
+      smt_identifier_termt("concat", expected_return_sort));
+    REQUIRE(concat.get_sort() == expected_return_sort);
+    REQUIRE(concat.arguments().size() == 2);
+    REQUIRE(concat.arguments()[0].get() == a_valid);
+    REQUIRE(concat.arguments()[1].get() == b_valid);
+  }
+  SECTION("Invalid operands")
+  {
+    const smt_bool_literal_termt false_term{false};
+    const smt_bool_literal_termt true_term{true};
+    cbmc_invariants_should_throwt invariants_throw;
+    CHECK_THROWS(smt_bit_vector_theoryt::concat(a_valid, false_term));
+    CHECK_THROWS(smt_bit_vector_theoryt::concat(false_term, a_valid));
+    CHECK_THROWS(smt_bit_vector_theoryt::concat(false_term, true_term));
+  }
+}
+
 TEST_CASE("SMT bit vector extract", "[core][smt2_incremental]")
 {
   const smt_bit_vector_constant_termt operand{42, 8};