Skip Ackermann constraints for derived arrays (weak equivalence)

Skip generating Ackermann constraints for arrays that are derived from
other arrays via with (store), if, array_of, array constants,
array_comprehension, typecast, or let expressions.

For a derived array such as x = y with [k := v], the Ackermann
constraint i1 = i2 => x[i1] = x[i2] is already implied by:
  (1) the with constraint: k != j => x[j] = y[j], and
  (2) the Ackermann constraint on the base array y.
This is the read-over-weakeq optimisation from the theory of weakly
equivalent arrays (Christ & Hoenicke, 2014).

The same reasoning applies to if, array_of, and other derived array
expressions, all of which already have constraints connecting them
element-wise to their constituent arrays.

With 5 stores to the same unbounded array the Ackermann constraint
count drops from 110 to 60; with 40 stores it drops from 63180 to
31980 (approximately 50% reduction in all cases).

Co-authored-by: Kiro

Author: tautschnig

regression/cbmc/Array_UF23/main.c

@@ -0,0 +1,21 @@
+/// \file
+/// Test that Ackermann constraints are reduced by the weak equivalence
+/// optimisation: derived arrays (with, if, etc.) do not need Ackermann
+/// constraints because they are implied by the with/if constraints plus
+/// Ackermann on base arrays.
+#include <stdlib.h>
+int main()
+{
+  size_t array_size;
+  int a[array_size];
+  int i0, i1, i2, i3, i4;
+
+  a[i0] = 0;
+  a[i1] = 1;
+  a[i2] = 2;
+  a[i3] = 3;
+  a[i4] = 4;
+
+  __CPROVER_assert(a[i0] >= 0, "a[i0] >= 0");
+  return 0;
+}

regression/cbmc/Array_UF23/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--arrays-uf-always --unwind 1 --show-array-constraints --json-ui
+"arrayAckermann": 60
+^EXIT=10$
+^SIGNAL=0$
+--
+"arrayAckermann": 110
+--
+Checks that the weak equivalence optimisation reduces Ackermann constraints.
+With 5 stores to the same unbounded array, the old code produced 110 Ackermann
+constraints (one per pair of indices per array term). The optimised code skips
+derived arrays (with, if, etc.) and produces only 60.

src/solvers/flattening/arrays.cpp

@@ -335,6 +335,25 @@ void arrayst::add_array_Ackermann_constraints()
   // iterate over arrays
   for(std::size_t i=0; i<arrays.size(); i++)
   {
+    // Skip arrays that are derived from other arrays via with, if, etc.
+    // Their Ackermann constraints are implied by the combination of:
+    // (1) the with/if/array_of/etc. constraints already generated, and
+    // (2) the Ackermann constraints on the underlying base arrays.
+    // This is the "weak equivalence" optimisation: arrays connected by
+    // store chains are weakly equivalent, and read-over-weakeq follows
+    // from the read-over-write constraints plus Ackermann on base arrays.
+    const exprt &arr = arrays[i];
+    if(
+      arr.id() == ID_with || arr.id() == ID_update || arr.id() == ID_if ||
+      arr.id() == ID_array_of || arr.id() == ID_array ||
+      arr.id() == ID_array_comprehension || arr.id() == ID_typecast ||
+      arr.id() == ID_string_constant || arr.is_constant())
+    {
+      continue;
+    }
+    if(expr_try_dynamic_cast<let_exprt>(arr))
+      continue;
+
     const index_sett &index_set=index_map[arrays.find_number(i)];
 
 #ifdef DEBUG