LINQ to Z3, The World’s Fasted Theorem Prover

by Jonathan Allen on Nov 29, 2010 |

Microsoft Research claims that Z3 is the world’s fastest theorem prover. Z3 is designed to be a low-level tool for other applications, it is not meant to stand-alone. With its host of theorem provers, it is used by numerous projects including Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, SAGE, VS3, FORMULA, and HAVOC.

Using Z3’s .NET API, one can encode theorems using an object-orientated style. However the example in the Z3 Tutorial demonstrates that even small problems can be quite tedious to code. Bart De Smet greatly simplified this by wrapping the OO-style API with a query-style API called LINQ to Z3. Below is an example that accompanied Bart De Smet’s Channel 9 interview.

  var theorem = from t in ctx.NewTheorem<Symbols<int, int, int, int, int>>()
    where t.X1 - t.X2 >= 1
    where t.X1 - t.X2 <= 3
    where t.X1 == (2 * t.X3) + t.X5
    where t.X3 == t.X5
    where t.X2 == 6 * t.X4
    select t; 
  var solution = theorem.Solve();
  Console.WriteLine("X1 = {0}, X2 = {1}, X3 = {2}, X4 = {3}, X5 = {4}",

Support for Z3 primarily available on Windows, but there is a Linux version of Z3. Z3 is released for non-commercial use under the “Microsoft Research License Agreement”. You can play with an on-line version of Z3 on RiSE4fun.

Related Editorial

How do you estimate on an Agile project?

Getting Ahead in the Cloud: The Need for Better Identity and Access Controls

Impact of Java EE Frameworks on the Structural Quality of Applications

Speed Matters: See why Nike, Groupon, and Comcast are using New Relic

Betfair Chooses not to Gamble with Database Performance: An AppDyanmics Case Study

Hello stranger!

You need to Register an InfoQ account or to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Tell us what you think

Community comments

Marketing buzz... by Jérôme Radix Posted

Re: Marketing buzz... by Faisal Waris Posted

Re: Marketing buzz... by Roberto Carlos Gonzalez Flores Posted

Re: Marketing buzz... by Jonathan Allen Posted

Re: Marketing buzz... by Jules Jacobs Posted

Z3 is a SMT solver...not a theorem prover by Francesco Bongiovanni Posted

Marketing buzz... by Jérôme Radix

The denomination "Theorem prover" seems too large for what it is exactly : a constraint processor in the integer domain. A Theorem is a thing a lot more complex than a list of inequalities.

Z3 is a SMT solver...not a theorem prover by Francesco Bongiovanni

I concur with previous comments...a SMT solver is a 'bit' different than pure theorem provers such as Isabelle or Coq. So the title is misleading :P (check the tutorial, its even written in it on page 12 that its not a theorem prover)

Re: Marketing buzz... by Faisal Waris

Z3 is an SMT (Satisfiability Modulo Theory) tool that seems to get pretty decent ratings among similar tools. Although I am not sure about the "world's fastest" claim.

See: www.smtexec.org/exec/?jobs=311,684

I don't know much about Z3 or SMT but I am using Microsoft Solver Foundation which is a constraint programming and linear/quadratic programming tool.

Constraint programming problems can become large and intractable. Perhaps Z3 can handle some of these types of problems better. It will be good to know that.

Additionally, I think it will be useful to be able to express such problems in LINQ so we can substitute for Z3 or Solver Foundation (or any other such tool) without impacting application code much.

Re: Marketing buzz... by Roberto Carlos Gonzalez Flores

I think that you are at the same level, or do you have tested all the API?, because it seems not to be only in the integer domain, if you look the introduction you will see: " supports real,..." whatever Real means in computer world... :

"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. These include: Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, SAGE, VS3, FORMULA, and HAVOC. It can read problems in SMT-LIB and Simplify formats."...

I haven't test this API, and I knew that a theorem is a lot more complex or it seems, because a theorem is a single solution to a problem under certain "controlled" circumnstances so it could be infered by an algorithm, I'm not saying that like it, I'm only saying "lets give it a try", and then we can talk, discuss, qualify, etc...

:)

Re: Marketing buzz... by Jonathan Allen

I admit I'm not an expert in this area and thus had to relie on the marketing buzz far more than I normally would. If any of you are and want to write an article setting the record straight, feel free to contact me at the below address. In addition to part-time staff positions, we do pay for one-time articles in our Educational Content section.

Jonathan Allen
jonathan@infoq.com

Re: Marketing buzz... by Jules Jacobs

Z3 is an SMT solver, which is not a general theorem prover, but it is definitely more powerful than solving inequalities over the integers. It can also reason about data types, arrays, functions, quantifiers, and any domain that you implement a module for.