LINQ to Z3, The World’s Fasted Theorem Prover

Posted by Jonathan Allen on Nov 29, 2010

Sections

Development

Topics

.NET ,

Programming ,

Z3 ,

Theorem Prover ,

LINQ

Share |

RELATED Research

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.

1. Back to top

   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.

   Reply

2. Back to top

   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)

   Reply

3. Back to top

   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.

   Reply

4. Back to top

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

   Reply

5. Back to top

   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

   Reply

6. Back to top

   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.

   Reply