Encoding and Reasoning about Arrays in Constraint Logic Programming with Sets

TL;DR

This paper encodes arrays as sets of ordered pairs within a set theory fragment, enabling array reasoning in a constraint logic programming language with a new decision procedure.

Contribution

It introduces a novel encoding of arrays as sets of pairs and extends the {log} solver with a decision procedure for array reasoning.

Findings

Arrays are represented as functions encoded as sets of pairs.

A decision procedure for array reasoning is implemented in {log}.

Arrays are integrated into set reasoning within the {log} language.

Abstract

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.