Scala to the Power of Z3: Integrating SMT and Programming

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.


Editor(s):
Bjorner, N.
Sofroniestokkermans, V.
Published in:
Automated Deduction - Cada-23, 6803, 400-406
Presented at:
23rd International Conference on Automated Deduction (CADE 23)
Year:
2011
Publisher:
Berlin, Springer-Verlag Berlin
ISSN:
0302-9743
ISBN:
978-3-642-22437-9
Laboratories:




 Record created 2013-02-28, last modified 2018-09-13


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)