Add SMT bit vector rotate operations

Author: thomasspriggs

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -789,3 +789,57 @@ smt_bit_vector_theoryt::sign_extend(std::size_t i)
 {
   return smt_function_application_termt::factoryt<sign_extendt>(i);
 }
+
+const char *smt_bit_vector_theoryt::rotate_leftt::identifier()
+{
+  return "rotate_left";
+}
+
+smt_sortt
+smt_bit_vector_theoryt::rotate_leftt::return_sort(const smt_termt &operand)
+{
+  return operand.get_sort();
+}
+
+std::vector<smt_indext> smt_bit_vector_theoryt::rotate_leftt::indices() const
+{
+  return {smt_numeral_indext{i}};
+}
+
+void smt_bit_vector_theoryt::rotate_leftt::validate(const smt_termt &operand)
+{
+  PRECONDITION(operand.get_sort().cast<smt_bit_vector_sortt>());
+}
+
+smt_function_application_termt::factoryt<smt_bit_vector_theoryt::rotate_leftt>
+smt_bit_vector_theoryt::rotate_left(std::size_t i)
+{
+  return smt_function_application_termt::factoryt<rotate_leftt>(i);
+}
+
+const char *smt_bit_vector_theoryt::rotate_rightt::identifier()
+{
+  return "rotate_right";
+}
+
+smt_sortt
+smt_bit_vector_theoryt::rotate_rightt::return_sort(const smt_termt &operand)
+{
+  return operand.get_sort();
+}
+
+std::vector<smt_indext> smt_bit_vector_theoryt::rotate_rightt::indices() const
+{
+  return {smt_numeral_indext{i}};
+}
+
+void smt_bit_vector_theoryt::rotate_rightt::validate(const smt_termt &operand)
+{
+  PRECONDITION(operand.get_sort().cast<smt_bit_vector_sortt>());
+}
+
+smt_function_application_termt::factoryt<smt_bit_vector_theoryt::rotate_rightt>
+smt_bit_vector_theoryt::rotate_right(std::size_t i)
+{
+  return smt_function_application_termt::factoryt<rotate_rightt>(i);
+}

src/solvers/smt2_incremental/smt_bit_vector_theory.h

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

unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -633,3 +633,40 @@ TEST_CASE("SMT bit vector extend", "[core][smt2_incremental]")
     REQUIRE_THROWS(smt_bit_vector_theoryt::sign_extend(1)(true_val));
   }
 }
+
+TEST_CASE("SMT bit vector rotation", "[core][smt2_incremental]")
+{
+  const smt_bit_vector_constant_termt two{2, 8};
+  const smt_bool_literal_termt true_val{true};
+  const auto expected_return_sort = smt_bit_vector_sortt{8};
+  SECTION("Left rotation")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::rotate_left(4)(two);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt(
+        "rotate_left", 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::rotate_left(0));
+    REQUIRE_THROWS(smt_bit_vector_theoryt::rotate_left(1)(true_val));
+  }
+  SECTION("Right rotation")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::rotate_right(4)(two);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt(
+        "rotate_right", 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::rotate_right(0));
+    REQUIRE_THROWS(smt_bit_vector_theoryt::rotate_right(1)(true_val));
+  }
+}