Amazing!<p>When I was prototyping a programming language with support for <i>contracts</i> (or <i>refined types</i>, e.g. `x : int if x > 0`), I tested a few different SMT solvers, including AltErgo, CVC and Yices (these seemed to be the most used open source solvers).<p>However, none of them were nearly as useful as Z3. In particular, they had no concept of a <i>stack</i> that allows the user to define different assertions <i>locally</i>, and then cancel them later. Without the stack, one would need to restart the solver and re-declare all variables (with all their constraints) for every function call with a constraint, compared to a single SMT script for each function verified in Z3.<p>Also, Z3 supports much more theories, in particular it supports non-linear integer arithmetics (which is an undecidable, incomplete theory), either by using some heuristics, or by translating the statements into the theory of real arithmetics (which is complete and decidable).
For one example of why Z3 is cool, check out this application to "peephole" compiler optimizations: <a href="http://blog.regehr.org/archives/1170" rel="nofollow">http://blog.regehr.org/archives/1170</a><p>Also take a look at the "licensing" section to see why switching to the MIT license is a big deal. Even open source software projects like LLVM have had to worry about whether using Z3 was OK or not. Now they don't any more!
I'm working with Z3 now, and it's been a real joy. One of the biggest advances in programming languages in recent years, perhaps. Glad to see it open-sourced and moved to Github.
I hope they will open source Microsoft.Automata too, it was very useful for a project where I had to generate samples of strings that had to conform to multiple regex :<p><a href="http://research.microsoft.com/en-us/projects/automata/" rel="nofollow">http://research.microsoft.com/en-us/projects/automata/</a>
Great project by MS research: good to see they picked a great license! See <a href="http://rise4fun.com" rel="nofollow">http://rise4fun.com</a> for more great projects like that.
z3 is something I didn't know about until encountering it here. Spent the last few hours playing with the solver, it's quite interesting especially since I've had a fair amount of exposure to Scheme. Felt right at home after getting it up and running.<p>Glitch-free compiling and installing under FreeBSD. The only problem was finding documentation. Rise4fun.com is mentioned in another post, the exact URL for getting started is <a href="http://rise4fun.com/Z3/tutorial/guide" rel="nofollow">http://rise4fun.com/Z3/tutorial/guide</a>. Also, very useful information here-- <a href="http://www.smt-lib.org/" rel="nofollow">http://www.smt-lib.org/</a>
Could please someone informed explain how is this more restricted to only prove theorems, instead of being a more general prolog-like system?<p>From the Microsoft Research page, I read:<p>> <i>Z3 is a high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research.</i><p>And with my current knowledge (which is low on the matter) I can't reconcile arithmetic, arrays, quantifiers, etc. with general program verification...
I've used model checkers before, but never SMT solvers. Looks really cool!<p>Anyway, here's a great post on solving a Project Euler problem using Z3/SMT-lib, which may be inspiring for other novices like myself:<p><a href="http://blogs.teamb.com/craigstuntz/2014/07/07/38818/" rel="nofollow">http://blogs.teamb.com/craigstuntz/2014/07/07/38818/</a>
Could someone who knows about these things, compare Z3 with the Google or-tools? (<a href="https://code.google.com/p/or-tools/" rel="nofollow">https://code.google.com/p/or-tools/</a>)<p>Pro's/Con's of the two?
I heard Microsoft uses provers to check (automated verification) third party kernel mode device drivers. Is that the Z3 proofer? I searched on Google and got several results but the meaning of the term "kernel" is overloaded and means different things in operating systems and proofers/solvers.