8 ms·

The Z3 theorem prover is now open source

137 points by taocp 14y ago

gojomo 14y ago
The limitation to non-commercial use means it's not quite 'open source' in the common meaning established by the Open Source Initiative. (Discrimination against a 'field of endeavor', such as business use, is not allowable under their definition.)
- fredsanford 14y ago
  The no commercial use thing is Microsoft speak for "We couldn't figure out how to make money with it, but if you do, give it to me." :P
  - sadga 14y ago
    cough http://creativecommons.org/licenses/by-nc/2.0/ http://creativecommons.org/licenses/by-nc/2.0/
- lucian1900 14y ago
  It's not open source by any stretch of the imagination. The Microsoft blog is quite simply lying.
  - frabcus 14y ago
    Thanks both for pointing this out - I've left a comment on the blog post asking him to change "open source" to "shared source" (which is what I thought Microsoft call such visible but not open code). I'll give Leonardo the benefit of the doubt that he's just made an error for now...
  - seanmcdirmid 14y ago
    Or the poster doesn't understand what open source really is, or their definition of open source is different from yours. Honestly, GPL screws up commercial use almost as much as a non commercial use restrictions. But I totally agree that open source are not the right words to use in this situation. Full disclosure, I work for Microsoft.
    - throwaway64 14y ago
      Open Source a term with a single, specific definition. It is damaging to the ideas of FLOSS to allow stuff like "shared source" to be called open source. EDIT: Removed reference to "open source" being trademarked, it is in fact not, apologies for the confusion.
      - hermanhermitage 14y ago
        No. This is a fantasy. A trademark does not take ownership of general words or phrases from the people.
        skrebbel 14y ago
        Correct. A trademark is just that: a mark used in trade. It does not come with the ability to define a standard definition for the mark's meaning, other than "~ is a trademark of $ORGANISATION". Also, is "open source" really trademarked? Wtf? That's like a beef promo organisation trademarking "well done".
        throwaway64 14y ago
        The problem with this idea when applied to this case is the motivations of people wishing to use some alternate definition. There is a real profit motive in being able to call stuff "open source" when it doesn't grant its users the same kind of freedoms the BSD or the GPL license, etc, do. If you allow stuff like "shared source" to be called open source, you reduce the term to a meaningless buzzword, like how the term "open" is frequently abused. citing trademarks is a heavy handed approach, but many parties with a profit motive don't care about anything except strict legality. This is relevant in particular to this blog because Microsoft has a history of attempting to change what the term means http://opensource.org/node/280 http://opensource.org/node/280
        nitrogen 14y ago
        A trademark does not take ownership of general words or phrases from the people. Except when that trademark is "Windows" or "Office" or "Word".
  - andyjohnson0 14y ago
    Why do you think they are "simply lying", rather than (for example) being simply mistaken?
    - lucian1900 14y ago
      Because they've been trying to dilute the term "open source" for quite a while now.
      - tptacek 14y ago
        1997 called and &c &c. Microsoft could give a shit about damaging "open source".
  - tptacek 14y ago
    Those bastards. How dare they publish their source code on terms we don't agree with.
    - dmm 14y ago
      The post you are replying to and its parent are not disagreeing with the terms the source code was published under. Go read them again and find where they disagree with the terms. They do disagree with the way those terms are _described_. "Open source" has a fairly well defined meaning and that meaning excludes a license that restricts use based on "field of endeavour", which the license in question does. This is also completely different from the GPL. The GPL does not restrict commercial use. I can use the GPLed linux kernel to serve up commercial websites all day. Presumably I could not use Z3 to serve a commercial service.
jmartinpetersen 14y ago
It seemed really exciting until I realized that it is only available for non-commercial purposes.
- wladimir 14y ago
  IMO it's still exciting. Sure, you cannot use it directly for commercial purposes, but having the source for something like this is great to learn from. And it means that it can be ported to platforms it's currently not available for.
  - praptak 14y ago
    > Sure, you cannot use it directly for commercial purposes, but having the source for something like this is great to learn from. As long as nobody sees you, otherwise you are vulnerable to a lawsuit. If I had serious plans to make my own implementation I would purposefully avoid even running this program.
    - wladimir 14y ago
      Right, if you intend to make your own implementation and profit from it, it's wise to avoid it. But for the rest of us it isn't that black and white...
      - Jach 14y ago
        Do you think Microsoft will be around in 10-20 years? Do you have a good idea of what you'll be working on (or interested in) in 10-20 years? Do you think laws regarding the forms of IP will be much better in 10-20 years? Do you think you'd get caught now or in the next 10-20 years if you do use this as research (or even rip code directly from it) and get sued for making money off it? Plug in your guestimations and make a decision. I looked at it, myself.
ot 14y ago
This is great news! When I was at MSR I heard the rumor that they wanted to sell Z3, not open-source it! Some context, as not everybody may have heard about it. Z3 is an SMT [1] solver. Since SMT generalizes SAT, it is clearly NP-hard, so a number of heuristics are needed. In particular, Z3 won several SMT speed competitions, so it has been for long the fastest SMT solver. You can play with it online using its Lisp-like native language [2] or using the Python bindings [3] The reason SMT is important is that several static analysis tools work by encoding the program constraints (such as pre/post conditions, invariants, ...) into a big formula. The satisfiability of this formula determines the correctness of the program, and sometimes assignments can be translated back to counterexamples to program correctness. [1] http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories [2] http://rise4fun.com/Z3/bit-count http://rise4fun.com/Z3/bit-count [3] http://rise4fun.com/Z3Py/nonlinear http://rise4fun.com/Z3Py/nonlinear
- wiradikusuma 14y ago
  what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.
  - agravier 14y ago
    Planning problems can be encoded as SAT problems, for instance.
  - raphinou 14y ago
    another example: package dependencies resolution on Linux distributions.
    - wolfgke 14y ago
      This can far more easily be done by topological sorting.
      - gchpaco 14y ago
ajb 14y ago
Non-commercial only. There are several similar projects some of which are really open source: http://smtlib.cs.uiowa.edu/solvers.html http://smtlib.cs.uiowa.edu/solvers.html
- sanxiyn 14y ago
  Sadly, none as good as Z3. I'd want to study Z3, even if I'd rather use something else. The current license is good enough for studying.
derleth 14y ago
From the license text: > Microsoft is granted back, without any restrictions or limitations, a non-exclusive, perpetual, irrevocable, royalty-free, assignable and sub-licensable license, to reproduce, publicly perform or display, install, use, modify, post, distribute, make and have made, sell and transfer your modifications to and/or derivative works of the Software source code or data, for any purpose. The above I can understand. MSFT claims ownership of any modifications you make to its software. Be aware. > [A]ny feedback about the Software provided by you to us is voluntarily given, and Microsoft shall be free to use the feedback as it sees fit without obligation or restriction of any kind, even if the feedback is designated by you as confidential. This I don't get. Why would MSFT want to publish confidential feedback? > That if you breach this MSR-LA or if you sue anyone over patents that you think may apply to or read on the Software or anyone's use of the Software, this MSR-LA (and your license and rights obtained herein) terminate automatically. Upon any such termination, you shall destroy all of your copies of the Software immediately. Sections 3, 4, 5, 6, 7, 8, 11 and 12 of this MSR-LA shall survive any termination of this MSR-LA. This part I certainly understand. "Sue us and you can't use our toys anymore." > That the patent rights, if any, granted to you in this MSR-LA only apply to the Software, not to any derivative works you make. This, again, is unsurprising, but good to keep in mind.
- andrewaylett 14y ago
  The feedback thing is probably along the lines of not wanting to have to have internal controls to deal with confidential information in their feedback processing.
- nwatson 14y ago
  The 'confidential feedback' boilerplate language would especially apply to projects with potential security implications. Your 'confidential feedback' might be disclosure of a security vulnerability and they'd want to choose to patch or not patch and publicly divulge or not divulge the vulnerability your feedback reveals.
- sadga 14y ago
  > The above I can understand. MSFT claims ownership of any modifications you make to its software. Be aware. MSFT claims a non-exclusive right to use your modifications.
elviejo 14y ago
Could this be used to tes ZED models?
jhartmann 14y ago
I think one of the problems with it not being true open source is that they are selling a commercial version @ the microsoft store for 14,950. I suspect this is why they choose this license. I'd be interested if they would provide different terms for the source for the people that bought the commercial version, or if you would just be stuck with the binaries. Here is the link to buy the commercial version: http://www.microsoftstore.com/store/msstore/pd/Microsoft-Research-Z3-Theorem-Prover/productID.242666500 http://www.microsoftstore.com/store/msstore/pd/Microsoft-Res...
tluyben2 14y ago
That's excellent (good to learn from, shame it's only non commercial; it's a step forward though)! I was accidentally checking rise4fun for open source just last week. I hope they open source more; unfortunately the project I'm most curious about at the moment (quickcode) will not be open sourced as it is officially part of Excel now.
timtadh 14y ago
Anyone able to find a link to the code? I have been looking around but I can only seem to find the binaries.
- apawloski 14y ago
  It's on codeplex http://z3.codeplex.com/SourceControl/changeset/view/9823ee3b4481 http://z3.codeplex.com/SourceControl/changeset/view/9823ee3b...
zvrba 14y ago
People bitching about MS misusing the term "open-source" are, IMO, ungrateful SOBs who have never attempted to implement a non-trivial algorithm based on nothing but a stack of academic papers. For me, the greatest value in having the source is to learn from it, not to hijack it.
- algorias 14y ago
  I think a lot of people appreciate the move MS made while simultaneously condemning them for their casual appropriation of a term having a well-established meaning. They've updated the blog post in the meantime, so this is a non-issue. Resorting to ad-hominems does nothing to strengthen your argument, btw.
  - zvrba 14y ago
    Care to show some signs of appreciation by those who complain?
subleq 14y ago
As a plain old programmer, would a tool like this be useful to me? How can I use a theorem prover to improve my code, or make it easier to write my code on a day to day basis? I've heard that Z3 is used for demonstrating security properties, how would I apply this to ensure my own systems are secure?
contextfree 14y ago
Wish someone would update the topic here, since it's not open source as per the generally understood definition ... (as the article's source has updated / corrected on his blog)

137 points by taocp 14y ago

The limitation to non-commercial use means it's not quite 'open source' in the common meaning established by the Open Source Initiative. (Discrimination against a 'field of endeavor', such as business use, is not allowable under their definition.)

fredsanford 14y ago
The no commercial use thing is Microsoft speak for "We couldn't figure out how to make money with it, but if you do, give it to me." :P
- sadga 14y ago
  cough http://creativecommons.org/licenses/by-nc/2.0/ http://creativecommons.org/licenses/by-nc/2.0/
lucian1900 14y ago
It's not open source by any stretch of the imagination. The Microsoft blog is quite simply lying.
- frabcus 14y ago
  Thanks both for pointing this out - I've left a comment on the blog post asking him to change "open source" to "shared source" (which is what I thought Microsoft call such visible but not open code). I'll give Leonardo the benefit of the doubt that he's just made an error for now...
- seanmcdirmid 14y ago
  Or the poster doesn't understand what open source really is, or their definition of open source is different from yours. Honestly, GPL screws up commercial use almost as much as a non commercial use restrictions. But I totally agree that open source are not the right words to use in this situation. Full disclosure, I work for Microsoft.
  - throwaway64 14y ago
    Open Source a term with a single, specific definition. It is damaging to the ideas of FLOSS to allow stuff like "shared source" to be called open source. EDIT: Removed reference to "open source" being trademarked, it is in fact not, apologies for the confusion.
    - hermanhermitage 14y ago
      No. This is a fantasy. A trademark does not take ownership of general words or phrases from the people.
      - skrebbel 14y ago
        Correct. A trademark is just that: a mark used in trade. It does not come with the ability to define a standard definition for the mark's meaning, other than "~ is a trademark of $ORGANISATION". Also, is "open source" really trademarked? Wtf? That's like a beef promo organisation trademarking "well done".
      - throwaway64 14y ago
        The problem with this idea when applied to this case is the motivations of people wishing to use some alternate definition. There is a real profit motive in being able to call stuff "open source" when it doesn't grant its users the same kind of freedoms the BSD or the GPL license, etc, do. If you allow stuff like "shared source" to be called open source, you reduce the term to a meaningless buzzword, like how the term "open" is frequently abused. citing trademarks is a heavy handed approach, but many parties with a profit motive don't care about anything except strict legality. This is relevant in particular to this blog because Microsoft has a history of attempting to change what the term means http://opensource.org/node/280 http://opensource.org/node/280
      - nitrogen 14y ago
        A trademark does not take ownership of general words or phrases from the people. Except when that trademark is "Windows" or "Office" or "Word".
- andyjohnson0 14y ago
  Why do you think they are "simply lying", rather than (for example) being simply mistaken?
  - lucian1900 14y ago
    Because they've been trying to dilute the term "open source" for quite a while now.
    - tptacek 14y ago
      1997 called and &c &c. Microsoft could give a shit about damaging "open source".
- tptacek 14y ago
  Those bastards. How dare they publish their source code on terms we don't agree with.
  - dmm 14y ago
    The post you are replying to and its parent are not disagreeing with the terms the source code was published under. Go read them again and find where they disagree with the terms. They do disagree with the way those terms are _described_. "Open source" has a fairly well defined meaning and that meaning excludes a license that restricts use based on "field of endeavour", which the license in question does. This is also completely different from the GPL. The GPL does not restrict commercial use. I can use the GPLed linux kernel to serve up commercial websites all day. Presumably I could not use Z3 to serve a commercial service.

jmartinpetersen 14y ago

It seemed really exciting until I realized that it is only available for non-commercial purposes.

wladimir 14y ago
IMO it's still exciting. Sure, you cannot use it directly for commercial purposes, but having the source for something like this is great to learn from. And it means that it can be ported to platforms it's currently not available for.
- praptak 14y ago
  > Sure, you cannot use it directly for commercial purposes, but having the source for something like this is great to learn from. As long as nobody sees you, otherwise you are vulnerable to a lawsuit. If I had serious plans to make my own implementation I would purposefully avoid even running this program.
  - wladimir 14y ago
    Right, if you intend to make your own implementation and profit from it, it's wise to avoid it. But for the rest of us it isn't that black and white...
    - Jach 14y ago
      Do you think Microsoft will be around in 10-20 years? Do you have a good idea of what you'll be working on (or interested in) in 10-20 years? Do you think laws regarding the forms of IP will be much better in 10-20 years? Do you think you'd get caught now or in the next 10-20 years if you do use this as research (or even rip code directly from it) and get sued for making money off it? Plug in your guestimations and make a decision. I looked at it, myself.

ot 14y ago

This is great news! When I was at MSR I heard the rumor that they wanted to sell Z3, not open-source it! Some context, as not everybody may have heard about it. Z3 is an SMT [1] solver. Since SMT generalizes SAT, it is clearly NP-hard, so a number of heuristics are needed. In particular, Z3 won several SMT speed competitions, so it has been for long the fastest SMT solver. You can play with it online using its Lisp-like native language [2] or using the Python bindings [3] The reason SMT is important is that several static analysis tools work by encoding the program constraints (such as pre/post conditions, invariants, ...) into a big formula. The satisfiability of this formula determines the correctness of the program, and sometimes assignments can be translated back to counterexamples to program correctness. [1] http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories [2] http://rise4fun.com/Z3/bit-count http://rise4fun.com/Z3/bit-count [3] http://rise4fun.com/Z3Py/nonlinear http://rise4fun.com/Z3Py/nonlinear

wiradikusuma 14y ago
what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.
- agravier 14y ago
  Planning problems can be encoded as SAT problems, for instance.
- raphinou 14y ago
  another example: package dependencies resolution on Linux distributions.
  - wolfgke 14y ago
    This can far more easily be done by topological sorting.
    - gchpaco 14y ago

ajb 14y ago

Non-commercial only. There are several similar projects some of which are really open source: http://smtlib.cs.uiowa.edu/solvers.html http://smtlib.cs.uiowa.edu/solvers.html

sanxiyn 14y ago
Sadly, none as good as Z3. I'd want to study Z3, even if I'd rather use something else. The current license is good enough for studying.

derleth 14y ago

From the license text: > Microsoft is granted back, without any restrictions or limitations, a non-exclusive, perpetual, irrevocable, royalty-free, assignable and sub-licensable license, to reproduce, publicly perform or display, install, use, modify, post, distribute, make and have made, sell and transfer your modifications to and/or derivative works of the Software source code or data, for any purpose. The above I can understand. MSFT claims ownership of any modifications you make to its software. Be aware. > [A]ny feedback about the Software provided by you to us is voluntarily given, and Microsoft shall be free to use the feedback as it sees fit without obligation or restriction of any kind, even if the feedback is designated by you as confidential. This I don't get. Why would MSFT want to publish confidential feedback? > That if you breach this MSR-LA or if you sue anyone over patents that you think may apply to or read on the Software or anyone's use of the Software, this MSR-LA (and your license and rights obtained herein) terminate automatically. Upon any such termination, you shall destroy all of your copies of the Software immediately. Sections 3, 4, 5, 6, 7, 8, 11 and 12 of this MSR-LA shall survive any termination of this MSR-LA. This part I certainly understand. "Sue us and you can't use our toys anymore." > That the patent rights, if any, granted to you in this MSR-LA only apply to the Software, not to any derivative works you make. This, again, is unsurprising, but good to keep in mind.

andrewaylett 14y ago
The feedback thing is probably along the lines of not wanting to have to have internal controls to deal with confidential information in their feedback processing.
nwatson 14y ago
The 'confidential feedback' boilerplate language would especially apply to projects with potential security implications. Your 'confidential feedback' might be disclosure of a security vulnerability and they'd want to choose to patch or not patch and publicly divulge or not divulge the vulnerability your feedback reveals.
sadga 14y ago
> The above I can understand. MSFT claims ownership of any modifications you make to its software. Be aware. MSFT claims a non-exclusive right to use your modifications.

elviejo 14y ago

Could this be used to tes ZED models?

jhartmann 14y ago

I think one of the problems with it not being true open source is that they are selling a commercial version @ the microsoft store for 14,950. I suspect this is why they choose this license. I'd be interested if they would provide different terms for the source for the people that bought the commercial version, or if you would just be stuck with the binaries. Here is the link to buy the commercial version: http://www.microsoftstore.com/store/msstore/pd/Microsoft-Research-Z3-Theorem-Prover/productID.242666500 http://www.microsoftstore.com/store/msstore/pd/Microsoft-Res...

tluyben2 14y ago

That's excellent (good to learn from, shame it's only non commercial; it's a step forward though)! I was accidentally checking rise4fun for open source just last week. I hope they open source more; unfortunately the project I'm most curious about at the moment (quickcode) will not be open sourced as it is officially part of Excel now.

timtadh 14y ago

Anyone able to find a link to the code? I have been looking around but I can only seem to find the binaries.

apawloski 14y ago
It's on codeplex http://z3.codeplex.com/SourceControl/changeset/view/9823ee3b4481 http://z3.codeplex.com/SourceControl/changeset/view/9823ee3b...

zvrba 14y ago

People bitching about MS misusing the term "open-source" are, IMO, ungrateful SOBs who have never attempted to implement a non-trivial algorithm based on nothing but a stack of academic papers. For me, the greatest value in having the source is to learn from it, not to hijack it.

algorias 14y ago
I think a lot of people appreciate the move MS made while simultaneously condemning them for their casual appropriation of a term having a well-established meaning. They've updated the blog post in the meantime, so this is a non-issue. Resorting to ad-hominems does nothing to strengthen your argument, btw.
- zvrba 14y ago
  Care to show some signs of appreciation by those who complain?

subleq 14y ago

As a plain old programmer, would a tool like this be useful to me? How can I use a theorem prover to improve my code, or make it easier to write my code on a day to day basis? I've heard that Z3 is used for demonstrating security properties, how would I apply this to ensure my own systems are secure?

contextfree 14y ago

Wish someone would update the topic here, since it's not open source as per the generally understood definition ... (as the article's source has updated / corrected on his blog)