Add SMT2 array theory store function

Author: Enrico Steffinlongo

src/solvers/smt2_incremental/smt_array_theory.cpp

@@ -27,3 +27,32 @@ void smt_array_theoryt::selectt::validate(
 
 const smt_function_application_termt::factoryt<smt_array_theoryt::selectt>
   smt_array_theoryt::select{};
+
+const char *smt_array_theoryt::storet::identifier()
+{
+  return "store";
+}
+smt_sortt smt_array_theoryt::storet::return_sort(
+  const smt_termt &array,
+  const smt_termt &index,
+  const smt_termt &value)
+{
+  return array.get_sort();
+}
+void smt_array_theoryt::storet::validate(
+  const smt_termt &array,
+  const smt_termt &index,
+  const smt_termt &value)
+{
+  const auto array_sort = array.get_sort().cast<smt_array_sortt>();
+  INVARIANT(array_sort, "\"store\" may only update an array.");
+  INVARIANT(
+    array_sort->index_sort() == index.get_sort(),
+    "Sort of arrays index must match the sort of the index supplied.");
+  INVARIANT(
+    array_sort->element_sort() == value.get_sort(),
+    "Sort of arrays value must match the sort of the value supplied.");
+}
+
+const smt_function_application_termt::factoryt<smt_array_theoryt::storet>
+  smt_array_theoryt::store{};

src/solvers/smt2_incremental/smt_array_theory.h

@@ -16,6 +16,20 @@ class smt_array_theoryt
     static void validate(const smt_termt &array, const smt_termt &index);
   };
   static const smt_function_application_termt::factoryt<selectt> select;
+
+  struct storet final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(
+      const smt_termt &array,
+      const smt_termt &index,
+      const smt_termt &value);
+    static void validate(
+      const smt_termt &array,
+      const smt_termt &index,
+      const smt_termt &value);
+  };
+  static const smt_function_application_termt::factoryt<storet> store;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_ARRAY_THEORY_H

unit/solvers/smt2_incremental/smt_array_theory.cpp

@@ -32,4 +32,36 @@ TEST_CASE("SMT array theory \"select\".", "[core][smt2_incremental]")
     invariant_failedt,
     invariant_failure_containing(
       "Sort of arrays index must match the sort of the index supplied."));
-}
+}
+
+TEST_CASE("SMT array theory \"store\".", "[core][smt2_incremental]")
+{
+  const smt_identifier_termt index_term("index", smt_bit_vector_sortt(64));
+  const smt_identifier_termt value_term("value", smt_bit_vector_sortt(32));
+  const smt_identifier_termt array_term(
+    "array", smt_array_sortt(index_term.get_sort(), value_term.get_sort()));
+  const smt_function_application_termt store =
+    smt_array_theoryt::store(array_term, index_term, value_term);
+  CHECK(store.get_sort() == array_term.get_sort());
+  CHECK(store.function_identifier().identifier() == "store");
+  REQUIRE(store.arguments().size() == 3);
+  CHECK(store.arguments()[0].get() == array_term);
+  CHECK(store.arguments()[1].get() == index_term);
+  CHECK(store.arguments()[2].get() == value_term);
+  cbmc_invariants_should_throwt invariants_throw;
+  const smt_bit_vector_constant_termt two{2, 8};
+  REQUIRE_THROWS_MATCHES(
+    smt_array_theoryt::store(two, index_term, value_term),
+    invariant_failedt,
+    invariant_failure_containing("\"store\" may only update an array."));
+  REQUIRE_THROWS_MATCHES(
+    smt_array_theoryt::store(array_term, two, value_term),
+    invariant_failedt,
+    invariant_failure_containing(
+      "Sort of arrays index must match the sort of the index supplied."));
+  REQUIRE_THROWS_MATCHES(
+    smt_array_theoryt::store(array_term, index_term, two),
+    invariant_failedt,
+    invariant_failure_containing(
+      "Sort of arrays value must match the sort of the value supplied."));
+}