References & Citations
Computer Science > Logic in Computer Science
Title: Integrating Cardinality Constraints into Constraint Logic Programming with Sets
(Submitted on 10 Feb 2021 (v1), last revised 5 Oct 2021 (this version, v2))
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.
Submission history
From: Maximiliano Cristia [view email][v1] Wed, 10 Feb 2021 13:38:49 GMT (54kb)
[v2] Tue, 5 Oct 2021 14:53:16 GMT (58kb)
Link back to: arXiv, form interface, contact.