Solving Boolean Algebra with Presburger Arithmetic (BAPA) Constraints in Z3
Scala
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
src/main/scala/bapa
unmanaged
z3
.gitignore
LICENSE
README.md
build.sbt

README.md

BAPA Z3 integration

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.