flâneur

Z3 Internals (Draft)

z3prover.github.io · 8,478 words · saved by 1 readers

Abstract. We present an overview of Z3 internals to outline the main data-structures and algorithms used in Z3. The overarching aim is to help users gain more insight into formula encodings that have a better chance of being solved, what controls a user has over search behavior, and what information a user can extract from the solver. While we will try to address these questions by providing background on principles and examples of experiences, it is impossible to provide comprehensive answers. The hope is that shedding light into the internal workings of Z3 at a conceptual level offers a bridge towards developing an understanding of how to operate Z3 as well. This document is written from the perspective of a developer of the SMT solver Z3. While it attempts to introduce an audience that includes many users to how to build an SMT solver, the main interest among users is more likely about how to best use an SMT solver. By introducing the internals of Z3 from the point of view of founda

Nikolaj Bjørner Microsoft Research Clemens Eisenhofer TU Wien Arie Gurfinkel U Waterloo Nuno P. Lopes U Lisbon Leonardo de Moura Microsoft Research Lev Nachmanson Microsoft Research Christoph Wintersteiger Microsoft Research Abstract. We present an overview of Z3 internals to outline the main data-structures and algorithms used in Z3. The overarching aim is to help users gain more insight into formula encodings that have a better chance of being solved, what controls a user has over search behavior, and what information a user can extract from the solver. While we will try to…

saved by

related reading