Add bitvector theory bitwise operators

Author: thomasspriggs

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -78,6 +78,71 @@ static void validate_bit_vector_operator_arguments(
     "Left and right operands must have the same bit width.");
 }
 
+// Bitwise operator definitions
+
+const char *smt_bit_vector_theoryt::nott::identifier()
+{
+  return "bvnot";
+}
+
+smt_sortt smt_bit_vector_theoryt::nott::return_sort(const smt_termt &operand)
+{
+  return operand.get_sort();
+}
+
+void smt_bit_vector_theoryt::nott::validate(const smt_termt &operand)
+{
+  const auto operand_sort = operand.get_sort().cast<smt_bit_vector_sortt>();
+  INVARIANT(operand_sort, "The operand is expected to have a bit-vector sort.");
+}
+
+const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::nott>
+  smt_bit_vector_theoryt::make_not{};
+
+const char *smt_bit_vector_theoryt::andt::identifier()
+{
+  return "bvand";
+}
+
+smt_sortt smt_bit_vector_theoryt::andt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::andt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_operator_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::andt>
+  smt_bit_vector_theoryt::make_and{};
+
+const char *smt_bit_vector_theoryt::ort::identifier()
+{
+  return "bvor";
+}
+
+smt_sortt smt_bit_vector_theoryt::ort::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::ort::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_operator_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::ort>
+  smt_bit_vector_theoryt::make_or{};
+
 // Relational operator definitions
 
 const char *smt_bit_vector_theoryt::unsigned_less_thant::identifier()

src/solvers/smt2_incremental/smt_bit_vector_theory.h

@@ -28,6 +28,31 @@ class smt_bit_vector_theoryt
   static smt_function_application_termt::factoryt<extractt>
   extract(std::size_t i, std::size_t j);
 
+  // Bitwise operators
+  struct nott final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &operand);
+    static void validate(const smt_termt &operand);
+  };
+  static const smt_function_application_termt::factoryt<nott> make_not;
+
+  struct andt 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<andt> make_and;
+
+  struct ort 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<ort> make_or;
+
   // Relational operator class declarations
   struct unsigned_less_thant final
   {

unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -60,6 +60,59 @@ TEST_CASE("SMT bit vector extract", "[core][smt2_incremental]")
   }
 }
 
+TEST_CASE("SMT bit vector bitwise operators", "[core][smt2_incremental]")
+{
+  const smt_bit_vector_constant_termt two{2, 8};
+  const smt_bit_vector_constant_termt three{3, 8};
+  const smt_bit_vector_constant_termt wider{4, 16};
+  const smt_bool_literal_termt true_val{true};
+  SECTION("not")
+  {
+    const auto function_application = smt_bit_vector_theoryt::make_not(two);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvnot", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    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::make_not(true_val));
+  }
+  SECTION("or")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::make_or(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvor", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::make_or(three, wider));
+    REQUIRE_THROWS(smt_bit_vector_theoryt::make_or(true_val, three));
+  }
+  SECTION("and")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::make_and(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvand", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::make_and(three, wider));
+    REQUIRE_THROWS(smt_bit_vector_theoryt::make_and(true_val, three));
+  }
+}
+
 TEST_CASE("SMT bit vector predicates", "[core][smt2_incremental]")
 {
   const smt_bit_vector_constant_termt two{2, 8};