InfoQ Homepage News LINQ to Z3, The World’s Fasted Theorem Prover

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

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.

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

• ##### Re: Marketing buzz...

by Faisal Waris /

• ##### Re: Marketing buzz...

by Roberto Carlos Gonzalez Flores /

• ##### Re: Marketing buzz...

by Jonathan Allen /

• ##### Re: Marketing buzz...

by Jules Jacobs /

• ##### Z3 is a SMT solver...not a theorem prover

by Francesco Bongiovanni /

• ##### Marketing buzz...

Your message is awaiting moderation. Thank you for participating in the discussion.

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

Your message is awaiting moderation. Thank you for participating in the discussion.

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 /

Your message is awaiting moderation. Thank you for participating in the discussion.

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

Your message is awaiting moderation. Thank you for participating in the discussion.

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

Your message is awaiting moderation. Thank you for participating in the discussion.

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 /

Your message is awaiting moderation. Thank you for participating in the discussion.

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.

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

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

Is your profile up-to-date? Please take a moment to review and update.

Note: If updating/changing your email, a validation request will be sent

Company name:
Company role:
Company size:
Country/Zone:
State/Province/Region:
You will be sent an email to validate the new email address. This pop-up will close itself in a few moments.