Add core theory "implies" operation

Author: thomasspriggs

src/solvers/smt2_incremental/smt_core_theory.cpp

@@ -22,6 +22,32 @@ 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::impliest::identifier()
+{
+  return "=>";
+}
+
+smt_sortt
+smt_core_theoryt::impliest::return_sort(const smt_termt &, const smt_termt &)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_core_theoryt::impliest::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  INVARIANT(
+    lhs.get_sort() == smt_bool_sortt{},
+    "Left hand side of \"=>\" must have bool sort.");
+  INVARIANT(
+    rhs.get_sort() == smt_bool_sortt{},
+    "Right hand side of \"=>\" must have bool sort.");
+}
+
+const smt_function_application_termt::factoryt<smt_core_theoryt::impliest>
+  smt_core_theoryt::implies{};
+
 const char *smt_core_theoryt::equalt::identifier()
 {
   return "=";

src/solvers/smt2_incremental/smt_core_theory.h

@@ -16,6 +16,14 @@ class smt_core_theoryt
   };
   static const smt_function_application_termt::factoryt<nott> make_not;
 
+  struct impliest 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<impliest> implies;
+
   struct equalt final
   {
     static const char *identifier();

unit/solvers/smt2_incremental/smt_core_theory.cpp

@@ -22,6 +22,24 @@ TEST_CASE("SMT core theory \"not\".", "[core][smt2_incremental]")
   CHECK_THROWS(smt_core_theoryt::make_not(smt_bit_vector_constant_termt{0, 1}));
 }
 
+TEST_CASE("SMT core theory implies.", "[core][smt2_incremental]")
+{
+  const smt_bool_literal_termt true_term{true};
+  const smt_bool_literal_termt false_term{false};
+  const auto implies = smt_core_theoryt::implies(true_term, false_term);
+  CHECK(implies.get_sort() == smt_bool_sortt{});
+  CHECK(
+    implies.function_identifier() ==
+    smt_identifier_termt{"=>", smt_bool_sortt{}});
+  REQUIRE(implies.arguments().size() == 2);
+  CHECK(implies.arguments()[0].get() == true_term);
+  CHECK(implies.arguments()[1].get() == false_term);
+  cbmc_invariants_should_throwt invariants_throw;
+  const smt_bit_vector_constant_termt two{2, 8};
+  CHECK_THROWS(smt_core_theoryt::implies(two, false_term));
+  CHECK_THROWS(smt_core_theoryt::implies(true_term, two));
+}
+
 TEST_CASE("SMT core theory \"=\".", "[core][smt2_incremental]")
 {
   SECTION("Bool sorted term comparison")