Unit tests for sparse_arrayt

Author: romainbrenguier

unit/Makefile

@@ -36,6 +36,7 @@ SRC += unit_tests.cpp \
        solvers/refinement/string_refinement/has_subtype.cpp \
        solvers/refinement/string_refinement/substitute_array_list.cpp \
        solvers/refinement/string_refinement/string_symbol_resolution.cpp \
+       solvers/refinement/string_refinement/sparse_array.cpp \
        solvers/refinement/string_refinement/union_find_replace.cpp \
        util/expr_cast/expr_cast.cpp \
        util/expr_iterator.cpp \

unit/solvers/refinement/string_refinement/sparse_array.cpp

@@ -0,0 +1,88 @@
+/*******************************************************************\
+
+ Module: Unit tests for sparse arrays
+   solvers/refinement/string_refinement.cpp
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+
+#include <util/arith_tools.h>
+#include <util/std_types.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+#include <solvers/refinement/string_refinement.h>
+#include <iostream>
+
+SCENARIO("sparse_array", "[core][solvers][refinement][string_refinement]")
+{
+  GIVEN("`ARRAY_OF(0) WITH [4:=x] WITH [1:=y] WITH [100:=z]`")
+  {
+    const typet char_type = unsignedbv_typet(16);
+    const typet int_type = signedbv_typet(32);
+    const exprt index1 = from_integer(1, int_type);
+    const exprt charx = from_integer('x', char_type);
+    const exprt index4 = from_integer(4, int_type);
+    const exprt chary = from_integer('y', char_type);
+    const exprt index100 = from_integer(100, int_type);
+    const exprt char0 = from_integer('0', char_type);
+    const exprt index2 = from_integer(2, int_type);
+    const exprt charz = from_integer('z', char_type);
+    const array_typet array_type(char_type, infinity_exprt(int_type));
+
+    const with_exprt input_expr(
+      with_exprt(
+        with_exprt(
+          array_of_exprt(from_integer(0, char_type), array_type),
+          index4,
+          charx),
+        index1,
+        chary),
+      index100,
+      charz);
+
+    WHEN("It is converted to a sparse array")
+    {
+      const sparse_arrayt sparse_array(input_expr);
+      THEN("The resulting if expression is index=4?x:index=1?y:index=100?z:0")
+      {
+        const symbol_exprt index("index", int_type);
+        const if_exprt expected(
+          equal_exprt(index, index4),
+          charx,
+          if_exprt(
+            equal_exprt(index, index1),
+            chary,
+            if_exprt(
+              equal_exprt(index, index100),
+              charz,
+              from_integer(0, char_type))));
+        REQUIRE(sparse_array.to_if_expression(index) == expected);
+      }
+    }
+
+    WHEN("It is converted to an interval sparse array")
+    {
+      const interval_sparse_arrayt sparse_array(input_expr);
+
+      THEN(
+        "The resulting if expression is index<=1?x:index<=4?y:index<=100?z:0")
+      {
+        const symbol_exprt index("index", int_type);
+        const if_exprt expected(
+          binary_relation_exprt(index, ID_le, index1),
+          chary,
+          if_exprt(
+            binary_relation_exprt(index, ID_le, index4),
+            charx,
+            if_exprt(
+              binary_relation_exprt(index, ID_le, index100),
+              charz,
+              from_integer(0, char_type))));
+        REQUIRE(sparse_array.to_if_expression(index) == expected);
+      }
+    }
+  }
+}