11–20 of 50 posts
Did anyone make a Javascript version of this with emscripten? I am currently using Z3 on the server side but would really like a client side solution to save computational resources.
Though the source is available, it cannot be used for commercial purposes. https://z3.codeplex.com/sourcecontrol/latest#LICENSE.txt You may not redistribute the source on a website intending to teach the use of Z3 for commercial purposes. You also agree that MS can sell any modifications or derivative software that you produce.
Is it even legal to prohibit teaching something due to copyright infringment?
Earlier quoted context omitted.
"...for commercial purposes"
Yeah, I got that first time, thanks. It is not trivial to separate commercial and non-commercial purposes. Creative commons licenses still don't have a clear criteria. So as it goes with copyright, this just has a chilling effect on the education of some compsci fundamentals. I just dont get why MS would do that, is it a competitive advantage?
(In case the sarcasm was a bit too thick, although it was at no less a level than your reply, I think it's plainly obvious what the licence is dictating and hope you will go into a little more detail of your viewpoint that it isn't)
Earlier quoted context omitted.
"...for commercial purposes"
Yeah, I got that first time, thanks. It is not trivial to separate commercial and non-commercial purposes. Creative commons licenses still don't have a clear criteria. So as it goes with copyright, this just has a chilling effect on the education of some compsci fundamentals. I just dont get why MS would do that, is it a competitive advantage?
Even then, if the teacher makes the text available to the students via a public web site, then its availability to non-students puts it outside of fair use.
However, the Z3 license does not prohibit teaching in general. In fact, it says:
"You may use, copy, reproduce, and distribute this Software for any non-commercial purpose, subject to the restrictions in this MSR-LA. Some purposes which can be non-commercial are teaching, academic research, public demonstrations and personal experimentation. You may also distribute this Software with books or other teaching materials, or publish the Software on websites, that are intended to teach the use of the Software for academic or other non-commercial purposes."
How does this have "a chilling effect on the education of some compsci fundamentals"?
If the software is going to be used for commercial purposes, then Microsoft wants some of the action. If you're going to teach how to use the software for commercial purposes, then Microsoft still wants some of the action.
So it seems from the various papers Z3 is oriented around infinite precision real arithmetic. It's that kind of overkill for most practical problems?
How does it compare with iSat or similar approaches in speed? One of the problems with SMT, Satisfiability Modulo Theories, is that it involves a somewhat loose connection between a SAT problem and an underlying theory prover, which can slow down the whole process if the underlying theory prover is not very fast.
If people are using this for interesting projects, I'd love some details.
Weirdly enough, I've studying this kind of thing lately. So it seems from the various papers Z3 is oriented around infinite precision real arithmetic. It's that kind of overkill for most practical problems? How does it compare with iSat or similar approaches in speed? One of the problems with SMT, Satisfiability Modulo Theories, is that it involves a somewhat loose connection between a SAT problem and an underlying t…
Earlier quoted context omitted.
Yeah, I got that first time, thanks. It is not trivial to separate commercial and non-commercial purposes. Creative commons licenses still don't have a clear criteria. So as it goes with copyright, this just has a chilling effect on the education of some compsci fundamentals. I just dont get why MS would do that, is it a competitive advantage?
Commercial = I make money from using this; Non-commercial = NOT commercial (In case the sarcasm was a bit too thick, although it was at no less a level than your reply, I think it's plainly obvious what the licence is dictating and hope you will go into a little more detail of your viewpoint that it isn't)
Non-commercial use for something that is directly involved in the production of something else is fairly easy to determine; it depends on whether that something else is sold for money or not.
But for analytical software like this prover, you could indirectly use it to improve something that is sold for money, but the process of improvement is not necessarily a commercial transaction. It could be performed by students at a university, for example. I have in mind formal verification of program invariants, with potential identification of breaks, as an example.
Earlier quoted context omitted.
Yeah, I got that first time, thanks. It is not trivial to separate commercial and non-commercial purposes. Creative commons licenses still don't have a clear criteria. So as it goes with copyright, this just has a chilling effect on the education of some compsci fundamentals. I just dont get why MS would do that, is it a competitive advantage?
Commercial = I make money from using this; Non-commercial = NOT commercial (In case the sarcasm was a bit too thick, although it was at no less a level than your reply, I think it's plainly obvious what the licence is dictating and hope you will go into a little more detail of your viewpoint that it isn't)
False. There are cases where commercial was held to mean "any use by a for profit company, regardless if the use is research, earns money directly or indirectly", etc.