Array constraints model how array accesses interact inside a constraint system, especially when the array is large enough that element-wise expansion is impractical.
Motivation
Prior approaches cited in the source handle array manipulations with constructions equivalent to SSA form. In that style, each assignment to an array element is translated into element constraints of the underlying constraint logic programming language. For an array of size n, a single assignment introduces 2n - 1 element constraints. The source notes that this becomes infeasible for memory-like arrays addressed by wide index registers, such as the 24-bit addressed memory used in the ST processor case study. [C1]
Direct array read/write constraints
To avoid full expansion, the source proposes introducing an array type directly in the solver, together with two constraints for element access:
tabReadtabWrite
These constraints maintain consistency between array accesses by propagating between index equalities and value equalities. The source gives the following rules:
i = j => T[i] = T[j]T[i] = T[j] => i = j
The implementation considers propagation in both directions: from relationships on indices to relationships on values, and conversely. [C2]
Order sensitivity
In the example discussed in the source, multiple reads and a write to the same array may alias depending on whether their indices are equal. With tabRead/tabWrite, the required constraints must preserve the order of accesses from the original code. The authors explicitly note that this introduces order dependence, which conflicts with the usual order-independent constraint programming style. They also observe that static dependency analysis is limited because the relevant indices are only known dynamically. [C2]
Two-step alias-based strategy
The paper then presents another strategy for array constraints in two phases:
- choose or fix relationships between access indices;
- add constraints that enforce those chosen relationships.
The key idea is that the complexity of array manipulation depends primarily on whether indices are equal or different. Array accesses may be aliases if they refer to the same location, and the number of possible equality-patterns among n indices is the number of partitions of an n-element set, namely the nth Bell number. [C3]
Bell-number characterization
The source explicitly states that the number of possible relationships among n indices corresponds to the nth Bell number, and gives the recurrence:
b0 = 1
b(n+1) = sum_{k=0..n} C(n,k) * b(k)
This is used to characterize the search space of possible aliasing relationships between array accesses. [C3]
Benefits and drawback of the alias-based approach
According to the source, this second approach has two main advantages:
- variable independence can be analyzed, allowing the constraint store to be split into independent groups of variables;
- graph analysis can then be used to derive variable-ordering heuristics that improve solving performance. [C3]
Its main drawback is that a chosen set of index relationships may be inconsistent with the rest of the constraint store. The authors therefore rely on the solver's backtracking mechanism to recover from such failures, while noting that symbolic solving can often avoid inconsistent choices. [C3]
Relation to STCS
The same paper presents STCS as a dedicated constraint solver created because existing solvers were not a good fit for the combination of typed finite-domain variables, bit-level operations, and array manipulations arising in the target hardware descriptions. The solver is introduced as one of the main contributions of the work. [C4]