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
But of course the implication "open source -> I can use it anywhere I want" is broken in this case. The author should have been a little more careful in not abusing that term, even if this was posted on his blog.
I am well aware of that licence, I myself had to use it for some code I wrote while at MSR [1]. I was not happy at all about the non-commercial clause, but it was either that or not releasing the code. I guess the same happened here.
[1] https://github.com/ot/path_decomposed_tries/blob/master/LICE...
It has already been pointed out that they didn't open-source Z3, they just made the source code available under the same license the binary already was. I would add that they have been selling Z3 for a long time:
http://www.microsoftstore.com/store/msstore/en_US/pd/product...
It has been there since 2011 according to my “archives”:
http://blog.frama-c.com/index.php?post/2011/12/23/Z3-in-Micr...
https://github.com/hugomg/hexiom
SMT solvers basically extend SAT solvers to allow you to work directly with other theories (linear inequalities, bit arrays, etc) without being forced to encode this as the booloean formulas that basic SAT understand. The idea is that dealing with the higher level details directly instead of having to convert tihngs to a commo low level makes it simpler to express things and can also allow for custumized optimizations and algorithms?
Satisfiability stuff is interesting because it shows that just because something is NP-complete doesn't mean that it is unapproachable or 'hard' (just as linear programming shows just cause something is in P doesn't mean it is 'easy' - for large values of easy). To ground the concept you can roughly categorize it with logic programming, answer set programming, constraint satisfaction and integer programming. I've made use of answer set programming for certain planning problems as a kind of better prolog but SMT is a 'bit' more flexible.
A particular example would be to take some existing code with holes (just parts left out) and some assertions about the code's behavior, encode both as logic formulas and try to find a satisfying assignment for the holes. When you have a possible assignment, you can verify it with the same encoding. You can then use the satisfying assignment to fill in the holes in the initial program, which are ideally very tedious to code by hand.
Full disclosure, I work for Microsoft.
I'll give Leonardo the benefit of the doubt that he's just made an error for now...
:P
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-Res...
And it means that it can be ported to platforms it's currently not available for.
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.
For me, the greatest value in having the source is to learn from it, not to hijack it.
Resorting to ad-hominems does nothing to strengthen your argument, btw.
> 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.
MSFT claims a non-exclusive right to use your modifications.
