Add SMT bit vector theory extract function

Author: thomasspriggs

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -4,6 +4,37 @@
 
 #include <util/invariant.h>
 
+const char *smt_bit_vector_theoryt::extractt::identifier()
+{
+  return "extract";
+}
+
+smt_sortt
+smt_bit_vector_theoryt::extractt::return_sort(const smt_termt &operand) const
+{
+  return smt_bit_vector_sortt{i - j + 1};
+}
+
+std::vector<smt_indext> smt_bit_vector_theoryt::extractt::indices() const
+{
+  return {smt_numeral_indext{i}, smt_numeral_indext{j}};
+}
+
+void smt_bit_vector_theoryt::extractt::validate(const smt_termt &operand) const
+{
+  PRECONDITION(i >= j);
+  const auto bit_vector_sort = operand.get_sort().cast<smt_bit_vector_sortt>();
+  PRECONDITION(bit_vector_sort);
+  PRECONDITION(i < bit_vector_sort->bit_width());
+}
+
+smt_function_application_termt::factoryt<smt_bit_vector_theoryt::extractt>
+smt_bit_vector_theoryt::extract(std::size_t i, std::size_t j)
+{
+  PRECONDITION(i >= j);
+  return smt_function_application_termt::factoryt<extractt>(i, j);
+}
+
 static void validate_bit_vector_operator_arguments(
   const smt_termt &left,
   const smt_termt &right)

src/solvers/smt2_incremental/smt_bit_vector_theory.h

@@ -8,6 +8,18 @@
 class smt_bit_vector_theoryt
 {
 public:
+  struct extractt final
+  {
+    std::size_t i;
+    std::size_t j;
+    static const char *identifier();
+    smt_sortt return_sort(const smt_termt &operand) const;
+    std::vector<smt_indext> indices() const;
+    void validate(const smt_termt &operand) const;
+  };
+  static smt_function_application_termt::factoryt<extractt>
+  extract(std::size_t i, std::size_t j);
+
   // Relational operator class declarations
   struct unsigned_less_thant final
   {

unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -7,6 +7,33 @@
 
 #include <util/mp_arith.h>
 
+TEST_CASE("SMT bit vector extract", "[core][smt2_incremental]")
+{
+  const smt_bit_vector_constant_termt operand{42, 8};
+  const auto extract_4_3 = smt_bit_vector_theoryt::extract(4, 3);
+  SECTION("Valid construction")
+  {
+    const auto extraction = extract_4_3(operand);
+    const auto expected_return_sort = smt_bit_vector_sortt{2};
+    REQUIRE(
+      extraction.function_identifier() ==
+      smt_identifier_termt(
+        "extract",
+        expected_return_sort,
+        {smt_numeral_indext{4}, smt_numeral_indext{3}}));
+    REQUIRE(extraction.get_sort() == expected_return_sort);
+    REQUIRE(extraction.arguments().size() == 1);
+    REQUIRE(extraction.arguments()[0].get() == operand);
+  }
+  SECTION("Invalid constructions")
+  {
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::extract(3, 4));
+    REQUIRE_THROWS(extract_4_3(smt_bool_literal_termt{true}));
+    REQUIRE_THROWS(extract_4_3(smt_bit_vector_constant_termt{8, 4}));
+  }
+}
+
 TEST_CASE("SMT bit vector predicates", "[core][smt2_incremental]")
 {
   const smt_bit_vector_constant_termt two{2, 8};