Add equal to smt core theory

Author: thomasspriggs

src/solvers/smt2_incremental/smt_core_theory.cpp

@@ -21,3 +21,26 @@ void smt_core_theoryt::nott::validate(const smt_termt &operand)
 
 const smt_function_application_termt::factoryt<smt_core_theoryt::nott>
   smt_core_theoryt::make_not{};
+
+const char *smt_core_theoryt::equalt::identifier()
+{
+  return "=";
+}
+
+smt_sortt
+smt_core_theoryt::equalt::return_sort(const smt_termt &, const smt_termt &)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_core_theoryt::equalt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  INVARIANT(
+    lhs.get_sort() == rhs.get_sort(),
+    "\"=\" may only be applied to terms which have the same sort.");
+}
+
+const smt_function_application_termt::factoryt<smt_core_theoryt::equalt>
+  smt_core_theoryt::equal{};

src/solvers/smt2_incremental/smt_core_theory.h

@@ -15,6 +15,14 @@ class smt_core_theoryt
     static void validate(const smt_termt &operand);
   };
   static const smt_function_application_termt::factoryt<nott> make_not;
+
+  struct equalt 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<equalt> equal;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H

unit/solvers/smt2_incremental/smt_core_theory.cpp

@@ -0,0 +1,55 @@
+// Author: Diffblue Ltd.
+
+#include <testing-utils/use_catch.h>
+
+#include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/smt_terms.h>
+
+#include <util/mp_arith.h>
+
+TEST_CASE("SMT core theory \"not\".", "[core][smt2_incremental]")
+{
+  const smt_bool_literal_termt operand{true};
+  const auto not_term = smt_core_theoryt::make_not(operand);
+
+  CHECK(not_term.get_sort() == smt_bool_sortt{});
+  REQUIRE(not_term.arguments().size() == 1);
+  REQUIRE(not_term.arguments()[0].get() == operand);
+  cbmc_invariants_should_throwt invariants_throw;
+  CHECK_THROWS(smt_core_theoryt::make_not(smt_bit_vector_constant_termt{0, 1}));
+}
+
+TEST_CASE("SMT core theory \"=\".", "[core][smt2_incremental]")
+{
+  SECTION("Bool sorted term comparison")
+  {
+    const smt_bool_literal_termt true_term{true};
+    const smt_bool_literal_termt false_term{false};
+    const auto bool_comparison = smt_core_theoryt::equal(true_term, false_term);
+    CHECK(bool_comparison.get_sort() == smt_bool_sortt{});
+    REQUIRE(bool_comparison.arguments().size() == 2);
+    REQUIRE(bool_comparison.arguments()[0].get() == true_term);
+    REQUIRE(bool_comparison.arguments()[1].get() == false_term);
+  }
+
+  SECTION("Bit vector sorted term comparison")
+  {
+    const smt_bit_vector_constant_termt two{2, 8};
+    const smt_bit_vector_constant_termt three{3, 8};
+    const auto bit_vector_comparison = smt_core_theoryt::equal(two, three);
+    CHECK(bit_vector_comparison.get_sort() == smt_bool_sortt{});
+    REQUIRE(bit_vector_comparison.arguments().size() == 2);
+    REQUIRE(bit_vector_comparison.arguments()[0].get() == two);
+    REQUIRE(bit_vector_comparison.arguments()[1].get() == three);
+  }
+
+  SECTION("Mismatch sort invariant")
+  {
+    cbmc_invariants_should_throwt invariants_throw;
+    CHECK_THROWS(smt_core_theoryt::equal(
+      smt_bit_vector_constant_termt{2, 8},
+      smt_bit_vector_constant_termt{2, 16}));
+    CHECK_THROWS(smt_core_theoryt::equal(
+      smt_bit_vector_constant_termt{2, 8}, smt_bool_literal_termt{true}));
+  }
+}