Add implementation of arithmetic operator bvsub.

Also add tests for it, both the conversion of `minus_exprt` to it,
and the node factory constructing the nodes appropriately.

Author: NlightNFotis

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -345,8 +345,10 @@ static smt_termt convert_expr_to_smt(const plus_exprt &plus)
 
 static smt_termt convert_expr_to_smt(const minus_exprt &minus)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for minus expression: " + minus.pretty());
+  PRECONDITION(can_cast_type<bitvector_typet>(minus.lhs().type()));
+  PRECONDITION(can_cast_type<bitvector_typet>(minus.rhs().type()));
+  return smt_bit_vector_theoryt::subtraction(
+    convert_expr_to_smt(minus.lhs()), convert_expr_to_smt(minus.rhs()));
 }
 
 static smt_termt convert_expr_to_smt(const div_exprt &divide)

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -65,3 +65,29 @@ void smt_bit_vector_theoryt::additiont::validate(
 const smt_function_application_termt::factoryt<
   smt_bit_vector_theoryt::additiont>
   smt_bit_vector_theoryt::add{};
+
+const char *smt_bit_vector_theoryt::subtractiont::identifier()
+{
+  return "bvsub";
+}
+
+smt_sortt smt_bit_vector_theoryt::subtractiont::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  // For now, make sure that they have the same bit-width
+  subtractiont::validate(lhs, rhs);
+  const auto width = lhs.get_sort().cast<smt_bit_vector_sortt>()->bit_width();
+  return smt_bit_vector_sortt{width};
+}
+
+void smt_bit_vector_theoryt::subtractiont::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_predicate_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::subtractiont>
+  smt_bit_vector_theoryt::subtraction{};

src/solvers/smt2_incremental/smt_bit_vector_theory.h

@@ -28,6 +28,15 @@ class smt_bit_vector_theoryt
     static void validate(const smt_termt &lhs, const smt_termt &rhs);
   };
   static const smt_function_application_termt::factoryt<additiont> add;
+
+  struct subtractiont 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<subtractiont>
+    subtraction;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -303,4 +303,22 @@ TEST_CASE(
     REQUIRE_THROWS(
       convert_expr_to_smt(plus_exprt{operands, signedbv_typet{8}}));
   }
+
+  SECTION("Subtraction of two constant size bit-vectors")
+  {
+    const auto constructed_term =
+      convert_expr_to_smt(minus_exprt{two_bvint, one_bvint});
+    const auto expected_term =
+      smt_bit_vector_theoryt::subtraction(smt_term_two, smt_term_one);
+    CHECK(constructed_term == expected_term);
+  }
+
+  SECTION(
+    "Ensure that subtraction node conversion fails if the operands are not "
+    "bit-vector based")
+  {
+    const cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(
+      convert_expr_to_smt(minus_exprt{true_exprt{}, false_exprt{}}));
+  }
 }

unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -193,4 +193,17 @@ TEST_CASE(
     // An addition of a bool and a bitvector should hit an invariant violation.
     REQUIRE_THROWS(smt_bit_vector_theoryt::add(three, true_val));
   }
+
+  SECTION("Subtraction")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::subtraction(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvsub", 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);
+  }
 }