Releasing the Z3 source code

Z3 source code is now available. The source code is available under the MSR-LA license. This is the same license used to distribute the Z3 binaries. The source code can be used for non-commercial purposes. The license allows users to redistribute, copy and modify Z3. For more information see http://z3.codeplex.com/license.

EDIT MSR-LA is not as “open” as GPL, Apache or BSD, but it allows users to read, copy, redistribute, modify, and experiment with Z3 source code. I believe MSR-LA matches academic openness and transparency. The main restriction is that the source code cannot be used for commercial purposes. END EDIT

Nikolaj Bjorner, Christoph Wintersteiger and I wrote several papers describing new algorithms and heuristics for SMT solvers. Some of them are non trivial and hard to reproduce. I believe the source code complements these papers, and may help others to clarify misunderstandings, dispute claims made in our papers, experiment new ideas, reproduce our results, and advance the state-of-the-art. Perhaps, the actual implementation is as important as the abstract procedures described in our papers.

By having the source code available, some features become obsolete. For example, the theory plugin API is not needed anymore. Now, users can directly implement their extensions inside the Z3 code base.

I think the code is quite readable, but it was not originally written for external consumption. We wrote the code for ourselves. Several parts have been rewritten several times, and some duplication exists. Anyway, I will try to cleanup the code in the future. Please, fell free to bug me if you are interested in hacking and/or understanding the source code. All important files are located in the directory lib.

The source code can be compiled in all major platforms. I tried on Windows (using Visual Studio) and Linux (using g++). If you find a problem, please contact me, and I will fix it.