Formal reasoning about finite sets and cardinality is important for many applications, includingsoftware verification, where very often one needs to reason about the size of a given data structure.The Constraint Logic Programming tool {log} provides a decision procedure for decidingthe satisfiability of formulas involving very general forms of finite sets, although it does notprovide cardinality constraints. In this paper we adapt and integrate a decision procedure for atheory of finite sets with cardinality into {log}. The proposed solver is proved to be a decisionprocedure 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 implementationbased on +250 real verification conditions shows that it can be useful in practice.
展开▼
