Add translation of array_of_exprt to SMT2

Author: Enrico Steffinlongo

regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc

@@ -3,7 +3,7 @@ control_flow.c
 --verbosity 10
 Passing problem to incremental SMT2 solving via
 Sending command to SMT2 solver - \(set-option :produce-models true\)
-Sending command to SMT2 solver - \(set-logic QF_AUFBV\)
+Sending command to SMT2 solver - \(set-logic ALL\)
 Sending command to SMT2 solver - \(declare-fun |goto_symex::&92;guard#1| \(\) Bool\)
 Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool |goto_symex::&92;guard#1|\)
 Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)

regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc

@@ -3,7 +3,7 @@ test.c
 --verbosity 10
 Passing problem to incremental SMT2 solving via
 Sending command to SMT2 solver - \(set-option :produce-models true\)
-Sending command to SMT2 solver - \(set-logic QF_AUFBV\)
+Sending command to SMT2 solver - \(set-logic ALL\)
 Sending command to SMT2 solver - \(define-fun |B0| \(\) Bool true\)
 Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
 Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool \(|=| |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

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

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,39 @@ 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{
+    id2string(array_identifier.identifier()) + "_index", index_type};
+  const smt_termt element_value = convert_expr_to_smt(array.what());
+
+  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 t_exprt>
+void smt2_incremental_decision_proceduret::define_array_function(
+  const t_exprt &array)
+{
+  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{
+    "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 +195,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 +245,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,29 @@ 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 t_exprt>
+  void define_array_function(const t_exprt &array);
+  /// \brief Generate and send to the SMT solver clauses asserting that each
+  /// array element is as specified by \p array.
+  void initialize_array_elements(
+    const array_exprt &array,
+    const smt_identifier_termt &array_identifier);
+  /// \brief Generate and send to the SMT solver clauses asserting that each
+  /// array element is as specified by \p array.
+  /// \note This function uses a forall SMT2 term. Using it in combination with
+  /// arrays, bit vectors and uninterpreted functions requires the `ALL` SMT
+  /// logic that is not in the SMT 2.6 standard, but that it has been tested
+  /// working 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.")