Merge pull request #6977 from esteffin/tas/array_functions

Add SMT2 array theory functions

src/solvers/Makefile

@@ -197,6 +197,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/convert_expr_to_smt.cpp \
       smt2_incremental/object_tracking.cpp \
       smt2_incremental/type_size_mapping.cpp \
+      smt2_incremental/smt_array_theory.cpp \
       smt2_incremental/smt_bit_vector_theory.cpp \
       smt2_incremental/smt_commands.cpp \
       smt2_incremental/smt_core_theory.cpp \

src/solvers/smt2_incremental/smt_array_theory.cpp

@@ -0,0 +1,58 @@
+// Author: Diffblue Ltd.
+
+#include "smt_array_theory.h"
+
+const char *smt_array_theoryt::selectt::identifier()
+{
+  return "select";
+}
+
+smt_sortt smt_array_theoryt::selectt::return_sort(
+  const smt_termt &array,
+  const smt_termt &index)
+{
+  return array.get_sort().cast<smt_array_sortt>()->element_sort();
+}
+
+void smt_array_theoryt::selectt::validate(
+  const smt_termt &array,
+  const smt_termt &index)
+{
+  const auto array_sort = array.get_sort().cast<smt_array_sortt>();
+  INVARIANT(array_sort, "\"select\" may only select from an array.");
+  INVARIANT(
+    array_sort->index_sort() == index.get_sort(),
+    "Sort of arrays index must match the sort of the index supplied.");
+}
+
+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

@@ -0,0 +1,35 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_ARRAY_THEORY_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_ARRAY_THEORY_H
+
+#include <solvers/smt2_incremental/smt_terms.h>
+
+class smt_array_theoryt
+{
+public:
+  struct selectt final
+  {
+    static const char *identifier();
+    static smt_sortt
+    return_sort(const smt_termt &array, const smt_termt &index);
+    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/Makefile

@@ -104,6 +104,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/smt2_incremental/convert_expr_to_smt.cpp \
        solvers/smt2_incremental/object_tracking.cpp \
        solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp \
+       solvers/smt2_incremental/smt_array_theory.cpp \
        solvers/smt2_incremental/smt_bit_vector_theory.cpp \
        solvers/smt2_incremental/smt_commands.cpp \
        solvers/smt2_incremental/smt_core_theory.cpp \

unit/solvers/smt2_incremental/smt_array_theory.cpp

@@ -0,0 +1,67 @@
+// Author: Diffblue Ltd.
+
+#include <util/mp_arith.h>
+
+#include <solvers/smt2_incremental/smt_array_theory.h>
+#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
+#include <testing-utils/use_catch.h>
+
+#include "testing-utils/invariant.h"
+
+TEST_CASE("SMT array theory \"select\".", "[core][smt2_incremental]")
+{
+  const smt_identifier_termt index_term("index", smt_bit_vector_sortt(64));
+  const smt_sortt value_sort(smt_bit_vector_sortt(32));
+  const smt_identifier_termt array_term(
+    "array", smt_array_sortt(index_term.get_sort(), value_sort));
+  const smt_function_application_termt select =
+    smt_array_theoryt::select(array_term, index_term);
+  CHECK(select.get_sort() == value_sort);
+  CHECK(select.function_identifier().identifier() == "select");
+  REQUIRE(select.arguments().size() == 2);
+  CHECK(select.arguments()[0].get() == array_term);
+  CHECK(select.arguments()[1].get() == index_term);
+  cbmc_invariants_should_throwt invariants_throw;
+  const smt_bit_vector_constant_termt two{2, 8};
+  REQUIRE_THROWS_MATCHES(
+    smt_array_theoryt::select(two, index_term),
+    invariant_failedt,
+    invariant_failure_containing("\"select\" may only select from an array."));
+  REQUIRE_THROWS_MATCHES(
+    smt_array_theoryt::select(array_term, two),
+    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."));
+}