  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.
