Add SMT bit vector repeat operation

Author: thomasspriggs

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -700,3 +700,34 @@ void smt_bit_vector_theoryt::arithmetic_shift_rightt::validate(
 const smt_function_application_termt::factoryt<
   smt_bit_vector_theoryt::arithmetic_shift_rightt>
   smt_bit_vector_theoryt::arithmetic_shift_right{};
+
+const char *smt_bit_vector_theoryt::repeatt::identifier()
+{
+  return "repeat";
+}
+
+smt_sortt
+smt_bit_vector_theoryt::repeatt::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::repeatt::indices() const
+{
+  return {smt_numeral_indext{i}};
+}
+
+void smt_bit_vector_theoryt::repeatt::validate(const smt_termt &operand) const
+{
+  PRECONDITION(i >= 1);
+  PRECONDITION(operand.get_sort().cast<smt_bit_vector_sortt>());
+}
+
+smt_function_application_termt::factoryt<smt_bit_vector_theoryt::repeatt>
+smt_bit_vector_theoryt::repeat(std::size_t i)
+{
+  PRECONDITION(i >= 1);
+  return smt_function_application_termt::factoryt<repeatt>(i);
+}

src/solvers/smt2_incremental/smt_bit_vector_theory.h

@@ -264,6 +264,17 @@ class smt_bit_vector_theoryt
   };
   static const smt_function_application_termt::factoryt<arithmetic_shift_rightt>
     arithmetic_shift_right;
+
+  struct repeatt final
+  {
+    std::size_t i;
+    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<repeatt>
+  repeat(std::size_t i);
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H

unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -577,3 +577,21 @@ TEST_CASE("SMT bit vector shifts", "[core][smt2_incremental]")
       smt_bit_vector_theoryt::arithmetic_shift_right(true_val, three));
   }
 }
+
+TEST_CASE("SMT bit vector repeat", "[core][smt2_incremental]")
+{
+  const smt_bit_vector_constant_termt two{2, 8};
+  const auto expected_return_sort = smt_bit_vector_sortt{32};
+  const smt_bool_literal_termt true_val{true};
+  const auto function_application = smt_bit_vector_theoryt::repeat(4)(two);
+  REQUIRE(
+    function_application.function_identifier() ==
+    smt_identifier_termt(
+      "repeat", 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_THROWS(smt_bit_vector_theoryt::repeat(0));
+  REQUIRE_THROWS(smt_bit_vector_theoryt::repeat(1)(true_val));
+}