We describe a system that integrates the SMT solver Z3 with the Scala
programming language. The system supports the use of the SMT solver for
checking satisfiability, unsatisfiability, as well as solution enumeration. The
embedding of formula trees into Scala uses the host type system of Scala to
prevent the construction of certain ill-typed constraints. The solution
enumeration feature integrates into the iteration constructions of Scala and
supports writing non-deterministic programs. Using Z3's mechanism of theory
extensions, our system also helps users construct custom constraint solvers
where the interpretation of predicates and functions is given as Scala code.
The resulting system preserves the productivity advantages of Scala while
simplifying tasks such as combinatorial search.

### Citation

Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter.
Scala to the power of Z3: Integrating SMT and programming.
In *Computer-Aideded Deduction (CADE) Tool Demo*, 2011.### BibTex Entry

@inproceedings{KoeksalETAL11ScalaZ3,
author = {{Ali Sinan} K{\"o}ksal and Viktor Kuncak and Philippe Suter},
title = {Scala to the Power of {Z3}: Integrating {SMT} and Programming},
booktitle = {Computer-Aideded Deduction (CADE) Tool Demo},
abstract = {
We describe a system that integrates the SMT solver Z3 with the Scala
programming language. The system supports the use of the SMT solver for
checking satisfiability, unsatisfiability, as well as solution enumeration. The
embedding of formula trees into Scala uses the host type system of Scala to
prevent the construction of certain ill-typed constraints. The solution
enumeration feature integrates into the iteration constructions of Scala and
supports writing non-deterministic programs. Using Z3's mechanism of theory
extensions, our system also helps users construct custom constraint solvers
where the interpretation of predicates and functions is given as Scala code.
The resulting system preserves the productivity advantages of Scala while
simplifying tasks such as combinatorial search.
},
year = 2011
}