Add SMT bit vector extension operations

Author: thomasspriggs

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -731,3 +731,61 @@ smt_bit_vector_theoryt::repeat(std::size_t i)
   PRECONDITION(i >= 1);
   return smt_function_application_termt::factoryt<repeatt>(i);
 }
+
+const char *smt_bit_vector_theoryt::zero_extendt::identifier()
+{
+  return "zero_extend";
+}
+
+smt_sortt smt_bit_vector_theoryt::zero_extendt::return_sort(
+  const smt_termt &operand) const
+{
+  const std::size_t operand_width =
+    operand.get_sort().cast<smt_bit_vector_sortt>()->bit_width();
+  return smt_bit_vector_sortt{i + operand_width};
+}
+
+std::vector<smt_indext> smt_bit_vector_theoryt::zero_extendt::indices() const
+{
+  return {smt_numeral_indext{i}};
+}
+
+void smt_bit_vector_theoryt::zero_extendt::validate(const smt_termt &operand)
+{
+  PRECONDITION(operand.get_sort().cast<smt_bit_vector_sortt>());
+}
+
+smt_function_application_termt::factoryt<smt_bit_vector_theoryt::zero_extendt>
+smt_bit_vector_theoryt::zero_extend(std::size_t i)
+{
+  return smt_function_application_termt::factoryt<zero_extendt>(i);
+}
+
+const char *smt_bit_vector_theoryt::sign_extendt::identifier()
+{
+  return "sign_extend";
+}
+
+smt_sortt smt_bit_vector_theoryt::sign_extendt::return_sort(
+  const smt_termt &operand) const
+{
+  const std::size_t operand_width =
+    operand.get_sort().cast<smt_bit_vector_sortt>()->bit_width();
+  return smt_bit_vector_sortt{i + operand_width};
+}
+
+std::vector<smt_indext> smt_bit_vector_theoryt::sign_extendt::indices() const
+{
+  return {smt_numeral_indext{i}};
+}
+
+void smt_bit_vector_theoryt::sign_extendt::validate(const smt_termt &operand)
+{
+  PRECONDITION(operand.get_sort().cast<smt_bit_vector_sortt>());
+}
+
+smt_function_application_termt::factoryt<smt_bit_vector_theoryt::sign_extendt>
+smt_bit_vector_theoryt::sign_extend(std::size_t i)
+{
+  return smt_function_application_termt::factoryt<sign_extendt>(i);
+}

src/solvers/smt2_incremental/smt_bit_vector_theory.h

@@ -275,6 +275,28 @@ class smt_bit_vector_theoryt
   };
   static smt_function_application_termt::factoryt<repeatt>
   repeat(std::size_t i);
+
+  struct zero_extendt final
+  {
+    std::size_t i;
+    static const char *identifier();
+    smt_sortt return_sort(const smt_termt &operand) const;
+    std::vector<smt_indext> indices() const;
+    static void validate(const smt_termt &operand);
+  };
+  static smt_function_application_termt::factoryt<zero_extendt>
+  zero_extend(std::size_t i);
+
+  struct sign_extendt final
+  {
+    std::size_t i;
+    static const char *identifier();
+    smt_sortt return_sort(const smt_termt &operand) const;
+    std::vector<smt_indext> indices() const;
+    static void validate(const smt_termt &operand);
+  };
+  static smt_function_application_termt::factoryt<sign_extendt>
+  sign_extend(std::size_t i);
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H

unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -595,3 +595,41 @@ TEST_CASE("SMT bit vector repeat", "[core][smt2_incremental]")
   REQUIRE_THROWS(smt_bit_vector_theoryt::repeat(0));
   REQUIRE_THROWS(smt_bit_vector_theoryt::repeat(1)(true_val));
 }
+
+TEST_CASE("SMT bit vector extend", "[core][smt2_incremental]")
+{
+  const smt_bit_vector_constant_termt two{2, 8};
+  const smt_bool_literal_termt true_val{true};
+  SECTION("Zero extension")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::zero_extend(4)(two);
+    const auto expected_return_sort = smt_bit_vector_sortt{12};
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt(
+        "zero_extend", expected_return_sort, {smt_numeral_indext{4}}));
+    REQUIRE(function_application.get_sort() == expected_return_sort);
+    REQUIRE(function_application.arguments().size() == 1);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_NOTHROW(smt_bit_vector_theoryt::zero_extend(0));
+    REQUIRE_THROWS(smt_bit_vector_theoryt::zero_extend(1)(true_val));
+  }
+  SECTION("Sign extension")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::sign_extend(4)(two);
+    const auto expected_return_sort = smt_bit_vector_sortt{12};
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt(
+        "sign_extend", expected_return_sort, {smt_numeral_indext{4}}));
+    REQUIRE(function_application.get_sort() == expected_return_sort);
+    REQUIRE(function_application.arguments().size() == 1);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_NOTHROW(smt_bit_vector_theoryt::sign_extend(0));
+    REQUIRE_THROWS(smt_bit_vector_theoryt::sign_extend(1)(true_val));
+  }
+}