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

21–30 of 77 posts

Re: The Z3 theorem prover is now open source

#21

Post by agravier »

wiradikusuma wrote: post #15
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…

what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.

Planning problems can be encoded as SAT problems, for instance.

Re: The Z3 theorem prover is now open source

#22

Post by andyjohnson0 »

lucian1900 wrote: post #8
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.)

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

Why do you think they are "simply lying", rather than (for example) being simply mistaken?

Re: The Z3 theorem prover is now open source

#23

Post by [deleted] »

throwaway64 wrote: post #14
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.

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.

[deleted]

Re: The Z3 theorem prover is now open source

#24

Post by Jach »

wladimir wrote: post #13
praptak wrote: post #9

Earlier quoted context omitted.

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

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

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.

Re: The Z3 theorem prover is now open source

#25

Post by wisty »

seanmcdirmid wrote: post #12
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.

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.

> Honestly, GPL screws up commercial use almost as much as a non commercial use restrictions.

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.

Re: The Z3 theorem prover is now open source

#26

Post by rmc »

seanmcdirmid wrote: post #12
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.

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.

Just about everyone who uses the term "open source" or "free software" would read "the source code can be used for non-commerical purposes" to mean "not open source".

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

Re: The Z3 theorem prover is now open source

#27

Post by raphinou »

wiradikusuma wrote: post #15
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…

what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.

another example: package dependencies resolution on Linux distributions.

Re: The Z3 theorem prover is now open source

#28

Post by olliesaunders »

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…

It seems its only free for non-commercial use, ergo not free.

Re: The Z3 theorem prover is now open source

#29

Post by lucian1900 »

wisty wrote: post #25
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.

> Honestly, GPL screws up commercial use almost as much as a non commercial use restrictions. 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…

Actually, interpreted code or browser code isn't really ambiguous. GPL is based on "derivative works" not necessarily C-style linking.

Re: The Z3 theorem prover is now open source

#30

Post by lucian1900 »

andyjohnson0 wrote: post #22
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.

Why do you think they are "simply lying", rather than (for example) being simply mistaken?

Because they've been trying to dilute the term "open source" for quite a while now.
Post reply on HN