Encoding and Reasoning about Arrays in Constraint Logic Programming with Sets
This work provides a novel method for integrating array reasoning into constraint logic programming with sets, extending existing decision procedures for set theory.
The paper encodes arrays as functions represented as sets of ordered pairs, enabling array reasoning within a set theory fragment. A decision procedure for this fragment is implemented in the {log} tool, allowing integrated reasoning about sets, functions, and arrays.
We encode arrays as functions which, in turn, are encoded as sets of ordered pairs. The set cardinality of each of these functions coincides with the length of the array it is representing. Then we define a fragment of set theory that is used to give the specifications of a non-trivial class of programs with arrays. In this way, array reasoning becomes set reasoning. Furthermore, a decision procedure for this fragment is also provided and implemented as part of the {log} (read 'setlog') tool. {log} is a constraint logic programming language and satisfiability solver where sets and binary relations are first-class citizens. The tool already implements a few decision procedures for different fragments of set theory. In this way, arrays are seamlessly integrated into {log} thus allowing users to reason about sets, functions and arrays all in the same language and with the same solver. The decision procedure presented in this paper is an extension of decision procedures defined in earlier works not supporting arrays.