Integrating Cardinality Constraints into Constraint Logic Programming with Sets

TL;DR

This paper enhances the {log} constraint logic programming tool by integrating a decision procedure for finite sets with cardinality, enabling more effective reasoning in software verification involving data structure sizes.

Contribution

It introduces a new decision procedure for finite sets with cardinality into {log} and implements it, demonstrating practical utility through empirical evaluation.

Findings

The new solver is a decision procedure for formulas involving finite sets with cardinality.

Implementation in {log} shows practical effectiveness on real verification conditions.

Empirical results indicate usefulness in software verification tasks.

Abstract

Formal reasoning about finite sets and cardinality is an important tool for many applications, including software verification, where very often one needs to reason about the size of a given data structure and not only about what its elements are. The Constraint Logic Programming tool {log} provides a decision procedure for deciding the satisfiability of formulas involving very general forms of finite sets, without cardinality. In this paper we adapt and integrate a decision procedure for a theory of finite sets with cardinality into {log}. The proposed solver is proved to be a decision procedure for its formulas. Besides, the new CLP instance is implemented as part of the {log} tool. In turn, the implementation uses Howe and King's Prolog SAT solver and Prolog's CLP(Q) library, as an integer linear programming solver. The empirical evaluation of this implementation based on +250 real verification conditions shows that it can be useful in practice.