Add core theory "if then else" operation

Author: thomasspriggs

src/solvers/smt2_incremental/smt_core_theory.cpp

@@ -67,3 +67,32 @@ void smt_core_theoryt::distinctt::validate(
 
 const smt_function_application_termt::factoryt<smt_core_theoryt::distinctt>
   smt_core_theoryt::distinct{};
+
+const char *smt_core_theoryt::if_then_elset::identifier()
+{
+  return "ite";
+}
+
+smt_sortt smt_core_theoryt::if_then_elset::return_sort(
+  const smt_termt &,
+  const smt_termt &then_term,
+  const smt_termt &)
+{
+  return then_term.get_sort();
+}
+
+void smt_core_theoryt::if_then_elset::validate(
+  const smt_termt &condition,
+  const smt_termt &then_term,
+  const smt_termt &else_term)
+{
+  INVARIANT(
+    condition.get_sort() == smt_bool_sortt{},
+    "Condition term must have bool sort.");
+  INVARIANT(
+    then_term.get_sort() == else_term.get_sort(),
+    "\"ite\" must have \"then\" and \"else\" terms of the same sort.");
+}
+
+const smt_function_application_termt::factoryt<smt_core_theoryt::if_then_elset>
+  smt_core_theoryt::if_then_else;

src/solvers/smt2_incremental/smt_core_theory.h

@@ -31,6 +31,21 @@ class smt_core_theoryt
     static void validate(const smt_termt &lhs, const smt_termt &rhs);
   };
   static const smt_function_application_termt::factoryt<distinctt> distinct;
+
+  struct if_then_elset final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(
+      const smt_termt &condition,
+      const smt_termt &then_term,
+      const smt_termt &else_term);
+    static void validate(
+      const smt_termt &condition,
+      const smt_termt &then_term,
+      const smt_termt &else_term);
+  };
+  static const smt_function_application_termt::factoryt<if_then_elset>
+    if_then_else;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H

unit/solvers/smt2_incremental/smt_core_theory.cpp

@@ -104,3 +104,23 @@ TEST_CASE("SMT core theory \"distinct\".", "[core][smt2_incremental]")
       smt_bit_vector_constant_termt{2, 8}, smt_bool_literal_termt{true}));
   }
 }
+
+TEST_CASE("SMT core theory if then else.", "[core][smt2_incremental]")
+{
+  const smt_bool_literal_termt false_term{false};
+  const smt_bit_vector_constant_termt two{2, 8};
+  const smt_bit_vector_constant_termt three{2, 8};
+  const auto if_then_else =
+    smt_core_theoryt::if_then_else(false_term, two, three);
+  CHECK(if_then_else.get_sort() == smt_bit_vector_sortt{8});
+  CHECK(
+    if_then_else.function_identifier() ==
+    smt_identifier_termt{"ite", smt_bit_vector_sortt{8}});
+  REQUIRE(if_then_else.arguments().size() == 3);
+  CHECK(if_then_else.arguments()[0].get() == false_term);
+  CHECK(if_then_else.arguments()[1].get() == two);
+  CHECK(if_then_else.arguments()[2].get() == three);
+  cbmc_invariants_should_throwt invariants_throw;
+  CHECK_THROWS(smt_core_theoryt::if_then_else(two, two, three));
+  CHECK_THROWS(smt_core_theoryt::if_then_else(false_term, false_term, three));
+}