Abstract
Array constraints are essential for handling data
structures in automated reasoning and software verification. Unfortunately, the use of a typical finite
domain (FD) solver based on local consistencybased filtering has strong limitations when constraints on indexes are combined with constraints
on array elements and size. This paper proposes
an efficient and complete FD-solving technique for
extended constraints over (possibly unbounded) arrays. We describe a simple but particularly powerful transformation for building an equisatisfiable
formula that can be efficiently solved using standard FD reasoning over arrays, even in the unbounded case. Experiments show that the proposed
solver significantly outperforms FD solvers, and
successfully competes with the best SMT-solvers