Add implementation of negation (unary minus - bvneg) operator.

Along with conversion tests and tests of the factory method integrity.

Author: NlightNFotis

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -154,9 +154,19 @@ static smt_termt convert_expr_to_smt(const bitnot_exprt &bitwise_not)
 
 static smt_termt convert_expr_to_smt(const unary_minus_exprt &unary_minus)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for unary minus expression: " +
-    unary_minus.pretty());
+  const bool operand_is_bitvector =
+    can_cast_type<integer_bitvector_typet>(unary_minus.op().type());
+  if(operand_is_bitvector)
+  {
+    return smt_bit_vector_theoryt::negate(
+      convert_expr_to_smt(unary_minus.op()));
+  }
+  else
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for unary minus expression: " +
+      unary_minus.pretty());
+  }
 }
 
 static smt_termt convert_expr_to_smt(const unary_plus_exprt &unary_plus)

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -365,3 +365,22 @@ void smt_bit_vector_theoryt::signed_remaindert::validate(
 const smt_function_application_termt::factoryt<
   smt_bit_vector_theoryt::signed_remaindert>
   smt_bit_vector_theoryt::signed_remainder{};
+
+const char *smt_bit_vector_theoryt::negatet::identifier()
+{
+  return "bvneg";
+}
+
+smt_sortt smt_bit_vector_theoryt::negatet::return_sort(const smt_termt &operand)
+{
+  return operand.get_sort();
+}
+
+void smt_bit_vector_theoryt::negatet::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::negatet>
+  smt_bit_vector_theoryt::negate{};

src/solvers/smt2_incremental/smt_bit_vector_theory.h

@@ -144,6 +144,14 @@ class smt_bit_vector_theoryt
   };
   static const smt_function_application_termt::factoryt<signed_remaindert>
     signed_remainder;
+
+  struct negatet 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<negatet> negate;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -399,4 +399,20 @@ 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::negate(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

@@ -309,4 +309,19 @@ TEST_CASE(
     // A remainder of a bool and a bitvector should hit an invariant violation.
     REQUIRE_THROWS(smt_bit_vector_theoryt::signed_remainder(true_val, three));
   }
+
+  SECTION("Unary Minus")
+  {
+    const auto function_application = smt_bit_vector_theoryt::negate(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);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    // Negation of a value of bool sort should fail with an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::negate(true_val));
+  }
 }