Merge pull request #7294 from thomasspriggs/tas/smt_multi_with

Add conversion of multi where/new_value with_exprt to SMT

Author: thomasspriggs

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1003,26 +1003,25 @@ static smt_termt convert_expr_to_smt(
 }
 
 static smt_termt convert_array_update_to_smt(
-  const exprt &old,
-  const exprt &index,
-  const exprt &new_value,
+  const with_exprt &with,
   const sub_expression_mapt &converted)
 {
-  const smt_termt &old_array_term = converted.at(old);
-  const smt_termt &index_term = converted.at(index);
-  const smt_termt &value_term = converted.at(new_value);
-  return smt_array_theoryt::store(old_array_term, index_term, value_term);
+  smt_termt array = converted.at(with.old());
+  for(auto it = ++with.operands().begin(); it != with.operands().end(); it += 2)
+  {
+    const smt_termt &index_term = converted.at(it[0]);
+    const smt_termt &value_term = converted.at(it[1]);
+    array = smt_array_theoryt::store(array, index_term, value_term);
+  }
+  return array;
 }
 
 static smt_termt convert_expr_to_smt(
   const with_exprt &with,
   const sub_expression_mapt &converted)
 {
-  if(const auto array_type = type_try_dynamic_cast<array_typet>(with.type()))
-  {
-    return convert_array_update_to_smt(
-      with.old(), with.where(), with.new_value(), converted);
-  }
+  if(can_cast_type<array_typet>(with.type()))
+    return convert_array_update_to_smt(with, converted);
   // 'with' expression is also used to update struct fields, but for now we do
   // not support them, so we fail.
   UNIMPLEMENTED_FEATURE(

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1239,15 +1239,30 @@ TEST_CASE(
       array_typet{value_type, from_integer(10, signed_size_type())}};
     const exprt index = from_integer(42, unsignedbv_typet{64});
     const exprt value = from_integer(12, value_type);
-    const with_exprt with{array, index, value};
-    INFO("Expression being converted: " + with.pretty(2, 0));
+    with_exprt with{array, index, value};
     const smt_termt expected = smt_array_theoryt::store(
       smt_identifier_termt{
         "my_array",
         smt_array_sortt{smt_bit_vector_sortt{64}, smt_bit_vector_sortt{8}}},
       smt_bit_vector_constant_termt{42, 64},
       smt_bit_vector_constant_termt{12, 8});
-    CHECK(test.convert(with) == expected);
+    SECTION("Single where/new_value pair update")
+    {
+      INFO("Expression being converted: " + with.pretty(2, 0));
+      CHECK(test.convert(with) == expected);
+    }
+    SECTION("Dual where/new_value pair update")
+    {
+      exprt index2 = from_integer(24, unsignedbv_typet{64});
+      exprt value2 = from_integer(21, value_type);
+      with.add_to_operands(std::move(index2), std::move(value2));
+      const smt_termt expected2 = smt_array_theoryt::store(
+        expected,
+        smt_bit_vector_constant_termt{24, 64},
+        smt_bit_vector_constant_termt{21, 8});
+      INFO("Expression being converted: " + with.pretty(2, 0));
+      CHECK(test.convert(with) == expected2);
+    }
   }
 }