# LINQ to Z3, The World’s Fasted Theorem Prover

| by Jonathan Allen 499 Followers on Nov 29, 2010. Estimated reading time: 1 minute |

A note to our readers: You asked so we have developed a set of features that allow you to reduce the noise: you can get email and web notifications for topics you are interested in. Learn more about our new features.

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.

Style

## Hello stranger!

You need to Register an InfoQ account or or login 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

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Marketing buzz...

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

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...

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...

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...

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...

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.
Close

#### by

on

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

6 Discuss

Login to InfoQ to interact with what matters most to you.

Quick overview of most important highlights in the industry and on the site.

#### More signal, less noise

Build your own feed by choosing topics you want to read about and editors you want to hear from.

#### Stay up-to-date

Set up your notifications and don't miss out on content that matters to you