Add translation of array_of_exprt to SMT2

Author: Enrico Steffinlongo

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -906,6 +906,9 @@ static smt_termt convert_expr_to_smt(
   const array_of_exprt &array_of,
   const sub_expression_mapt &converted)
 {
+  // This function is left unimplemented as the `array_of_exprt` nodes are fully
+  // converted by the incremental decision procedure functions
+  // (smt2_incremental_decision_proceduret::define_array_function).
   UNIMPLEMENTED_FEATURE(
     "Generation of SMT formula for array of expression: " + array_of.pretty());
 }
@@ -1353,6 +1356,9 @@ static smt_termt convert_expr_to_smt(
   const array_exprt &array_construction,
   const sub_expression_mapt &converted)
 {
+  // This function is left unimplemented as the `array_exprt` nodes are fully
+  // converted by the incremental decision procedure functions
+  // (smt2_incremental_decision_proceduret::define_array_function).
   UNIMPLEMENTED_FEATURE(
     "Generation of SMT formula for array construction expression: " +
     array_construction.pretty());

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -71,6 +71,7 @@ static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
     if(
       can_cast_expr<symbol_exprt>(expr_node) ||
       can_cast_expr<array_exprt>(expr_node) ||
+      can_cast_expr<array_of_exprt>(expr_node) ||
       can_cast_expr<nondet_symbol_exprt>(expr_node))
     {
       dependent_expressions.push_back(expr_node);
@@ -79,17 +80,10 @@ static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
   return dependent_expressions;
 }
 
-void smt2_incremental_decision_proceduret::define_array_function(
-  const array_exprt &array)
+void smt2_incremental_decision_proceduret::initialize_array_elements(
+  const array_exprt &array,
+  const smt_identifier_termt &array_identifier)
 {
-  const smt_sortt array_sort = convert_type_to_smt_sort(array.type());
-  INVARIANT(
-    array_sort.cast<smt_array_sortt>(),
-    "Converting array typed expression to SMT should result in a term of array "
-    "sort.");
-  const smt_identifier_termt array_identifier = smt_identifier_termt{
-    "array_" + std::to_string(array_sequence()), array_sort};
-  solver_process->send(smt_declare_function_commandt{array_identifier, {}});
   const std::vector<exprt> &elements = array.operands();
   const typet &index_type = array.type().index_type();
   for(std::size_t i = 0; i < elements.size(); ++i)
@@ -100,6 +94,46 @@ void smt2_incremental_decision_proceduret::define_array_function(
       convert_expr_to_smt(elements.at(i)))};
     solver_process->send(element_definition);
   }
+}
+
+void smt2_incremental_decision_proceduret::initialize_array_elements(
+  const array_of_exprt &array,
+  const smt_identifier_termt &array_identifier)
+{
+  const smt_sortt index_type =
+    convert_type_to_smt_sort(array.type().index_type());
+  const smt_identifier_termt array_index_identifier = smt_identifier_termt{
+    id2string(array_identifier.identifier()) + "_index", index_type};
+  const std::vector<exprt> &elements = array.operands();
+  INVARIANT(elements.size() == 1, "array_of_exprt must have only one operand.");
+  const smt_termt element_value = convert_expr_to_smt(elements.front());
+
+  const smt_assert_commandt elements_definition{smt_forall_termt{
+    {array_index_identifier},
+    smt_core_theoryt::equal(
+      smt_array_theoryt::select(array_identifier, array_index_identifier),
+      element_value)}};
+  solver_process->send(elements_definition);
+}
+
+template <typename EXPRT>
+void smt2_incremental_decision_proceduret::define_array_function(
+  const EXPRT &array)
+{
+  static_assert(
+    std::is_same<EXPRT, array_exprt>::value ||
+      std::is_same<EXPRT, array_of_exprt>::value,
+    "smt2_incremental_decision_proceduret::define_array_function can be "
+    "applied only to array_exprt and array_of_exprt arguments.");
+  const smt_sortt array_sort = convert_type_to_smt_sort(array.type());
+  INVARIANT(
+    array_sort.cast<smt_array_sortt>(),
+    "Converting array typed expression to SMT should result in a term of array "
+    "sort.");
+  const smt_identifier_termt array_identifier = smt_identifier_termt{
+    "array_" + std::to_string(array_sequence()), array_sort};
+  solver_process->send(smt_declare_function_commandt{array_identifier, {}});
+  initialize_array_elements(array, array_identifier);
   expression_identifiers.emplace(array, array_identifier);
 }
 
@@ -168,9 +202,14 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
         solver_process->send(function);
       }
     }
-    if(const auto array_expr = expr_try_dynamic_cast<array_exprt>(current))
+    else if(const auto array_expr = expr_try_dynamic_cast<array_exprt>(current))
       define_array_function(*array_expr);
-    if(
+    else if(
+      const auto array_of_expr = expr_try_dynamic_cast<array_of_exprt>(current))
+    {
+      define_array_function(*array_of_expr);
+    }
+    else if(
       const auto nondet_symbol =
         expr_try_dynamic_cast<nondet_symbol_exprt>(current))
     {
@@ -213,8 +252,7 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
 {
   solver_process->send(
     smt_set_option_commandt{smt_option_produce_modelst{true}});
-  solver_process->send(smt_set_logic_commandt{
-    smt_logic_quantifier_free_arrays_uninterpreted_functions_bit_vectorst{}});
+  solver_process->send(smt_set_logic_commandt{smt_logic_allt{}});
   solver_process->send(object_size_function.declaration);
 }
 

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -55,11 +55,27 @@ class smt2_incremental_decision_proceduret final
 protected:
   // Implementation of protected decision_proceduret member function.
   resultt dec_solve() override;
-  /// \brief Defines a function of array sort and asserts the element values.
+  /// \brief Defines a function of array sort and asserts the element values
+  /// from `array_exprt` or `array_of_exprt`.
   /// \details
   ///   The new array function identifier is added to the
   ///   `expression_identifiers` map.
-  void define_array_function(const array_exprt &array);
+  /// \note Statically fails if the template type is not a `array_exprt` or
+  /// `array_of_exprt`.
+  template <typename EXPRT>
+  void define_array_function(const EXPRT &array);
+  /// \brief Sets the state of the array by asserting that each array element is
+  /// correct.
+  void initialize_array_elements(
+    const array_exprt &array,
+    const smt_identifier_termt &array_identifier);
+  /// \brief Sets the state of the array by asserting that each array element is
+  /// correct.
+  /// \note This function uses a forall SMT2 term. This is not in the SMT 2.6
+  /// standard, but it has been tested and works on Z3 and CVC5.
+  void initialize_array_elements(
+    const array_of_exprt &array,
+    const smt_identifier_termt &array_identifier);
   /// \brief Defines any functions which \p expr depends on, which have not yet
   ///   been defined, along with their dependencies in turn.
   void define_dependent_functions(const exprt &expr);

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -171,9 +171,8 @@ TEST_CASE(
       test.sent_commands ==
       std::vector<smt_commandt>{
         smt_set_option_commandt{smt_option_produce_modelst{true}},
-        smt_set_logic_commandt{
-          // NOLINTNEXTLINE(whitespace/line_length)
-          smt_logic_quantifier_free_arrays_uninterpreted_functions_bit_vectorst{}},
+        smt_set_logic_commandt{// NOLINTNEXTLINE(whitespace/line_length)
+                               smt_logic_allt{}},
         test.object_size_function.declaration});
     test.sent_commands.clear();
     SECTION("Set symbol to true.")