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

[2] http://rise4fun.com/Z3/bit-count

[3] http://rise4fun.com/Z3Py/nonlinear

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

1. http://security.ece.cmu.edu/aeg/ 2. http://users.ece.cmu.edu/~ejschwar/bib/schwartz_2011_rop-abs...

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.

I suppose it depends on what you mean by flexible. I would say that ASP is more flexible as a modeling language—you can specify all sorts of logic and constraints in it in a fairly expressive logical formalism, with both generative (Prolog-like) and constraint-oriented (CSP-like) language constructs. Particularly with the extensions the Potassco people have been making in their version: http://potassco.sourceforge.net/

However, current ASP solvers ground to variable-free (propositional) programs before solving, which means they blow up on large-ish integer domains, since you end up propositionalizing the whole integer range. I've had some examples where just grounding out the problem takes ages, but then it's nearly instant to solve once the grounding is done. SMT avoids that by providing a way to ground "modulo" a domain theory, rather than fully grounding, with a theory of integers being a common example.

But right, by more flexible I meant the availability of quantifiers in SMT solvers.

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.

The GPL is not the only open source license. It may screw up certain commercial usage, but it never stops users from forking the software. This Microsoft license does.

1. http://opensource.org/

The GPL has a few problems, but non-commercial causes are just noxious.

Who exactly can use a non-commercial piece of software? Presumably, universities can. Can a government research lab use it? How about a military research lab? What about a contractor doing military R&D? If Exon-Mobile uses this to search for oil, is this research (thus non-commercial)?

Any clause which is likely to give your lawyer a headache trying to interpret it is probably a bad license.

The GPL has some ambiguous bits (like its interaction with interpreted code eg Python bindings to MySQL and Javascript libraries in the browser) but it's not as ugly as the term Non-Commercial.

If the JS engine mixes interpreted code with the proprietary DOM, how does that work?

How about LGPL works?

But you're right - it's usually pretty clear if you think about it. There will always be edge-cases, but unlike non-commercial clauses the edge cases aren't that common.

If you distribute GPL code you then become subject to its restrictions and must provide the code.

If they were banned because of the GPL the company was doing its own stupid rules completely unrelated to the restrictions imposed by the GPL. If they weren't then it shows the difference between the GPL and the non-commercial use term of this particular MS license.

For MS and a surprisingly small (in terms of total global economy) number of other businesses selling closed source software (or software dependent on other non-Free software components) the GPL imposes very real restrictions.

I would argue that they are in no way arbitrary but have a clear purpose and objective to further increase the amount of Free software in the world. You may or may not support or want to assist this objective but it certainly doesn't feel arbitrary to me (I've taken the 'capricious; unreasonable; unsupported' definition of arbitrary from Dictionary.com as my interpretation of your meaning).

Edit/reply:

Can't reply to you for some reason. No citation but you have missed my point. I wasn't comparing Open Source Industry to closed source software industry but really the software industry to ALL Other industries (and individuals) in the world. Basically software consumers rather than producers (of which closed source companies like MS form a large part).

If RMS was true to his principles, he would make GPL more viral to cover every deployment and co-deployment. But they leave this huge server hole instead. That is what I mean by arbitrary. Why a hole there and not elsewhere?

Don't want to answer for RMS. I can't think of less arbitrary way of achieving their aims.

There is basically no disagreement about what counts as an open source/free software licence. This licence is not that.

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.

A trademark does not take ownership of general words or phrases from the people.

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

Also, is "open source" really trademarked? Wtf? That's like a beef promo organisation trademarking "well done".

Except when that trademark is "Windows" or "Office" or "Word".

This is a bit of a digression from the original topic, but seems tangentially relevant given that we're talking about Microsoft accidentally misusing or deliberately abusing a term that has an accepted meaning in the marketplace, the very purpose for which trademarks were created.

[Also, I should have added the following disclaimer to the previous comment: Disclaimer: Long ago, in a galaxy far away, I worked for a company that seemed to have a chance at invalidating the Windows trademark, but when Microsoft offered a large settlement, my former employer took the money and ran.]

Likewise, it is reasonable that Microsoft can't call their competing license "open source" when that term already has an established commercial definition and trademark with a specific set of consumer expectations.

Further, until a tradmeark is filed or established by extensive use, competing products can use similar words in their titles. Once upon a time you could have had Microsoft Windows, OpenWindows, the comp.windows.x newsgroup (suggesting that X is a subset of the generic category of "Windows"), etc. Now they will sue if your OS name even rhymes with Windows.

I'll give Leonardo the benefit of the doubt that he's just made an error for now...

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.

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