Add SMT2 core theory "distinct"

Author: thomasspriggs

src/solvers/smt2_incremental/smt_core_theory.cpp

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

src/solvers/smt2_incremental/smt_core_theory.h

@@ -23,6 +23,14 @@ class smt_core_theoryt
     static void validate(const smt_termt &lhs, const smt_termt &rhs);
   };
   static const smt_function_application_termt::factoryt<equalt> equal;
+
+  struct distinctt 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<distinctt> distinct;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H

unit/solvers/smt2_incremental/smt_core_theory.cpp

@@ -62,3 +62,45 @@ TEST_CASE("SMT core theory \"=\".", "[core][smt2_incremental]")
       smt_bit_vector_constant_termt{2, 8}, smt_bool_literal_termt{true}));
   }
 }
+
+TEST_CASE("SMT core theory \"distinct\".", "[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::distinct(true_term, false_term);
+    CHECK(bool_comparison.get_sort() == smt_bool_sortt{});
+    CHECK(
+      bool_comparison.function_identifier() ==
+      smt_identifier_termt{"distinct", 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::distinct(two, three);
+    CHECK(bit_vector_comparison.get_sort() == smt_bool_sortt{});
+    CHECK(
+      bit_vector_comparison.function_identifier() ==
+      smt_identifier_termt{"distinct", 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::distinct(
+      smt_bit_vector_constant_termt{2, 8},
+      smt_bit_vector_constant_termt{2, 16}));
+    CHECK_THROWS(smt_core_theoryt::distinct(
+      smt_bit_vector_constant_termt{2, 8}, smt_bool_literal_termt{true}));
+  }
+}