Skip to content
forked from psuter/bapa-z3

Solving Boolean Algebra with Presburger Arithmetic (BAPA) Constraints in Z3

License

Notifications You must be signed in to change notification settings

saby1101/bapa-z3

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

8 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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.

About

Solving Boolean Algebra with Presburger Arithmetic (BAPA) Constraints in Z3

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Scala 100.0%