Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Z3 theorem prover is now open source

research.microsoft.com

Post reply on HN
Print view View original

61–70 of 77 posts

Re: The Z3 theorem prover is now open source

#61

Post by Dn_Ab »

mjn wrote: post #53
Dn_Ab wrote: post #51

Earlier quoted context omitted.

I have only made light contact with SMTs in my explorations but SMT solvers have massive applicability. They're used in theorem proving - verification, dependent typing, contracts - scheduling, planning, and for understanding/modelling cell regulatory networks in biology. Satisfiability stuff is interesting because it shows that just because something is NP-complete doesn't mean that it is unapproachable or 'hard' (j…

> 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) langua…

Awesome response thanks. The increased ease of use for modeling is part of why I decided on it rather than an SMT solver. One should prefer ASP wherever the assumptions hold. I use(d) DLV-Complex but will check your link.

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

Re: The Z3 theorem prover is now open source

#62

Post by dmm »

tptacek wrote: post #38
lucian1900 wrote: post #8

Earlier quoted context omitted.

It's not open source by any stretch of the imagination. The Microsoft blog is quite simply lying.

Those bastards. How dare they publish their source code on terms we don't agree with.

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.

Re: The Z3 theorem prover is now open source

#63

Post by sanxiyn »

ajb wrote: post #5

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

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.

Re: The Z3 theorem prover is now open source

#64

Post by throwaway54-762 »

lucian1900 wrote: post #18
seanmcdirmid wrote: post #12

Earlier quoted context omitted.

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.

Microsoft trying to hijack a term with an already fully established meaning is dishonest and screws up everything. This may be an honest mistake by an employee that fell for Microsoft's own marketing, but it's still not right to spread misinformation. Is the license on this list [1]? Then it's almost certainly not open source. Also, this particular license has already been rejected by OSI. The GPL is not the only ope…

Er, technically this license doesn't stop forks -- they are explicitly allowed -- but it definitely propagates the non-commercial clause. I agree, it's definitely not Open Source.

Re: The Z3 theorem prover is now open source

#65

Post by gchpaco »

wolfgke wrote: post #55
raphinou wrote: post #27

Earlier quoted context omitted.

another example: package dependencies resolution on Linux distributions.

This can far more easily be done by topological sorting.

That's not actually sufficient when you consider version requirements; for example requiring a specific range of libc or the like.

Re: The Z3 theorem prover is now open source

#66

Post by pascal_cuoq »

ot wrote: post #4

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-l…

> When I was at MSR I heard the rumor that they wanted to sell Z3, not open-source it!

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

Re: The Z3 theorem prover is now open source

#67

Post by josephlord »

seanmcdirmid wrote: post #49
josephlord wrote: post #43

Earlier quoted context omitted.

You seem to have a VERY narrow definition of commercial use which involves selling software or being a software service provider. There are a vast majority of companies manufacturing/distributing/retailing and providing services for whom the GPL imposes no restriction at all. The MS release seems to prevent all commercial use not just commercial redistribution/binary release making it a FAR broader restriction than t…

Citation needed on how the open source software industry is so much larger (money wise) than the closed source software industry. I'm sure its much more of a mix, plus closed source software is more often sold, meaning more money is involved in say oracle DB vs. MySQL. Also, most of the OSS industry prefers apache/BSD style licenses that aren't viral. If RMS was true to his principles, he would make GPL more viral to…

I don't say anything of the sort. Please read again. I am saying that total global commerce and use of computers is greater than the software industry (not the world's greatest insight I know).

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

Re: The Z3 theorem prover is now open source

#68

Post by lucian1900 »

throwaway54-762 wrote: post #64
lucian1900 wrote: post #18

Earlier quoted context omitted.

Microsoft trying to hijack a term with an already fully established meaning is dishonest and screws up everything. This may be an honest mistake by an employee that fell for Microsoft's own marketing, but it's still not right to spread misinformation. Is the license on this list [1]? Then it's almost certainly not open source. Also, this particular license has already been rejected by OSI. The GPL is not the only ope…

Er, technically this license doesn't stop forks -- they are explicitly allowed -- but it definitely propagates the non-commercial clause. I agree, it's definitely not Open Source.

I meant that it doesn't allow arbitrary forking. There are cases in which it's illegal to keep using it, whereas with the GPL at most you'd have to release the derivative source to your (paying) users.

Re: The Z3 theorem prover is now open source

#69

Post by sedachv »

seanmcdirmid wrote: post #49
josephlord wrote: post #43

Earlier quoted context omitted.

You seem to have a VERY narrow definition of commercial use which involves selling software or being a software service provider. There are a vast majority of companies manufacturing/distributing/retailing and providing services for whom the GPL imposes no restriction at all. The MS release seems to prevent all commercial use not just commercial redistribution/binary release making it a FAR broader restriction than t…

Citation needed on how the open source software industry is so much larger (money wise) than the closed source software industry. I'm sure its much more of a mix, plus closed source software is more often sold, meaning more money is involved in say oracle DB vs. MySQL. Also, most of the OSS industry prefers apache/BSD style licenses that aren't viral. If RMS was true to his principles, he would make GPL more viral to…

RMS didn't foresee the server hole. That's why GNU came out with the Affero GPL in 2007: http://www.gnu.org/licenses/agpl-3.0.html

Re: The Z3 theorem prover is now open source

#70

Post by sadga »

fredsanford wrote: post #7
gojomo wrote: post #2

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

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

cough http://creativecommons.org/licenses/by-nc/2.0/
Post reply on HN