Conference paper · Book chapter
vZ - An Optimizing SMT Solver
In
Lecture Notes in Computer Science
—
2015, pp. 194-199
Abstract
vZ is a part of the SMT solver Z3. It allows users to pose and solve optimization problems modulo theories. Many SMT applications use models to provide satisfying assignments, and a growing number of these build on top of Z3 to get optimal assignments with respect to objective functions. vZ provides a portfolio of approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations.
Objective functions are combined as either Pareto fronts, lexicographically, or each objective is optimized independently. We describe usage scenarios of vZ, outline the tool architecture that allows dispatching problems to special purpose solvers, and examine use cases.
| Language: | English |
|---|---|
| Publisher: | Springer |
| Year: | 2015 |
| Pages: | 194-199 |
| Proceedings: | 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015)International Conference on Tools and Algorithms for the Construction and Analysis of Systems |
| Series: | Lecture Notes in Computer Science |
| ISBN: | 3662466805 , 3662466813 , 9783662466803 and 9783662466810 |
| ISSN: | 03029743 and 16113349 |
| Types: | Conference paper and Book chapter |
| DOI: | 10.1007/978-3-662-46681-0_14 |
