A plugin for the Z3 SMT solver. The plugin is written in Scala, and relies on ScalaZ3 to work. It naturally also relies on Z3. Precompiled versions --for 32bit Linux systems-- of both are included in this repository. Please note that Z3 comes with its own license.
The underlying algorithm of the BAPA theory plugin is described in:
- Philippe Suter, Robin Steiger, and Viktor Kuncak. Sets with Cardinality Constraints in Satisfiability Modulo Theories. VMCAI 2011, pp. 403-418.
The paper is available from Springer or from the first author's home page.