## Philippe Suter, Robin Steiger, and Viktor Kuncak.
Sets with cardinality constraints in satisfiability modulo theories.
In *Verification, Model Checking, and Abstract Interpretation
(VMCAI)*, 2011.

Boolean Algebra with Presburger Arithmetic (BAPA) is a
decidable logic that can express constraints on sets of
elements and their cardinalities. Problems from
verification of complex properties of software
often contain fragments that belong to
quantifier-free BAPA (QFBAPA).
In contrast to many other NP-complete problems (such
as quantifier-free first-order logic or linear arithmetic),
the applications of QFBAPA to a broader set of problems has
so far been hindered by the lack of an efficient
implementation that can be used alongside other efficient
decision procedures.
We overcome these limitations by extending the efficient
SMT solver Z3 with the ability to reason about cardinality (QFBAPA)
constraints. Our implementation uses the DPLL(T) mechanism
of Z3 to reason about the top-level propositional
structure of a QFBAPA formula, improving the efficiency
compared to previous implementations. Moreover, we
present a new algorithm for automatically decomposing
QFBAPA formulas. Our algorithm alleviates the exponential
explosion of considering all Venn regions, significantly
improving the tractability of formulas with many set
variables. Because it is implemented as a theory plugin,
our implementation enables Z3 to prove formulas that use
QFBAPA constructs with constructs from other theories
that Z3 supports,
as well as with quantifiers. We have applied our
implementation to the verification of functional programs; we
show it can automatically prove formulas that no automated
approach was reported to be able to prove before.

[ bib ]
Back