Email Gateway (Aug 19 2022 at 17:32): Email Gateway (Aug 19 2022 at 17:32):From: marco caminati <marco.caminati@yahoo.it>
I just learned of that, maybe it's interesting/new information for some on this list.
https://github.com/Z3Prover/z3/commit/40269c8511ca343bc6848cae8c4f2d0f0455b949
Email Gateway (Aug 19 2022 at 17:33):From: Lars Hupel <hupel@in.tum.de>
Well, it used to be "open" for some time already (with source code
available), but only under a "non-commercial" license. Now, it appears
to be truly free (as in: free to use for any purpose).
Anyway, as far as I can tell, there's no official announcement by
Microsoft Research yet. But one of the authors (de Moura) writes it on
his homepage: <https://leodemoura.github.io/>. My uneducated guess is
that it will become official by the next release (4.4) and finally, the
"z3_non_commercial" system option can go away :-)
Cheers
Lars
Email Gateway (Aug 19 2022 at 17:33):From: marco caminati <marco.caminati@yahoo.it>
Sab 28/3/15, Lars Hupel <hupel@in.tum.de> ha scritto:
Well, it used to be "open" for some time already (with source code available), but only under a "non-commercial" license.
I didn't know the source was already available.
Then I'm not sure whether this move makes it more or less open.
Anyway, will this have some effect towards the no-smt policy in afp submissions?
Just for curiosity, since we already removed smt occurrences througout all our Isabelle code :)
Best,
Marco
Email Gateway (Aug 19 2022 at 17:33):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
The Z3 package with Isabelle is actually an unstable version at some point between 4.3.1 and 4.3.2. We could do the same thing again, and just take the latest repository version to get a package with no “z3_non_commercial” option.
Jasmin
Email Gateway (Aug 19 2022 at 17:34):From: Tobias Nipkow <nipkow@in.tum.de>
On 28/03/2015 14:29, marco caminati wrote:
Sab 28/3/15, Lars Hupel <hupel@in.tum.de> ha scritto:
Well, it used to be "open" for some time already (with source code available), but only under a "non-commercial" license.
I didn't know the source was already available.
Then I'm not sure whether this move makes it more or less open.Anyway, will this have some effect towards the no-smt policy in afp submissions?
No. We have no control over Z3 and hence Z3 proofs are inherently brittle.
Tobias
Just for curiosity, since we already removed smt occurrences througout all our Isabelle code :)
Best,
Marco
Email Gateway (Aug 22 2022 at 09:39):From: marco caminati <marco.caminati@yahoo.it>
Lun 30/3/15, Tobias Nipkow <nipkow@in.tum.de> ha scritto:
No. We have no control over Z3 and hence Z3 proofs are inherently brittle.
Tobias
I see.
Thank you for answering.
Best,
Marco
Last updated: Apr 18 2024 at 16:19 UTC