Add remainder (modulus) arithmetic operator bvurem.

Along with tests of its conversion and the function application factory
integrity.

Author: NlightNFotis

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -172,22 +172,3 @@ void smt_bit_vector_theoryt::remaindert::validate(
 const smt_function_application_termt::factoryt<
   smt_bit_vector_theoryt::remaindert>
   smt_bit_vector_theoryt::remainder{};
-
-const char *smt_bit_vector_theoryt::negationt::identifier()
-{
-  return "bvneg";
-}
-
-smt_sortt
-smt_bit_vector_theoryt::negationt::return_sort(const smt_termt &operand)
-{
-  return operand.get_sort();
-}
-
-void smt_bit_vector_theoryt::negationt::validate(const smt_termt &operand)
-{
-}
-
-const smt_function_application_termt::factoryt<
-  smt_bit_vector_theoryt::negationt>
-  smt_bit_vector_theoryt::negation{};

src/solvers/smt2_incremental/smt_bit_vector_theory.h

@@ -63,13 +63,13 @@ class smt_bit_vector_theoryt
   };
   static const smt_function_application_termt::factoryt<remaindert> remainder;
 
-  struct negationt final
+  struct remaindert final
   {
     static const char *identifier();
-    static smt_sortt return_sort(const smt_termt &operand);
-    static void validate(const smt_termt &operand);
+    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<negationt> negation;
+  static const smt_function_application_termt::factoryt<remaindert> remainder;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -366,20 +366,4 @@ TEST_CASE(
     const cbmc_invariants_should_throwt invariants_throw;
     REQUIRE_THROWS(convert_expr_to_smt(mod_exprt{one_bvint, false_exprt{}}));
   }
-
-  SECTION("Unary minus of constant size bit-vector")
-  {
-    const auto constructed_term =
-      convert_expr_to_smt(unary_minus_exprt{one_bvint});
-    const auto expected_term = smt_bit_vector_theoryt::negation(smt_term_one);
-    CHECK(constructed_term == expected_term);
-  }
-
-  SECTION(
-    "Ensure that unary minus node conversion fails if the operand is not a "
-    "bit-vector")
-  {
-    const cbmc_invariants_should_throwt invariants_throw;
-    REQUIRE_THROWS(convert_expr_to_smt(unary_minus_exprt{true_exprt{}}));
-  }
 }

unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -238,15 +238,4 @@ TEST_CASE(
     REQUIRE(function_application.arguments()[0].get() == two);
     REQUIRE(function_application.arguments()[1].get() == three);
   }
-
-  SECTION("Unary Minus")
-  {
-    const auto function_application = smt_bit_vector_theoryt::negation(two);
-    REQUIRE(
-      function_application.function_identifier() ==
-      smt_identifier_termt("bvneg", 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);
-  }
 }