Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] AFP submission and smt2

Email Gateway (Aug 19 2022 at 16:34):

From: marco caminati <marco.caminati@yahoo.it>
In AFP submission guidelines (http://afp.sourceforge.net/submitting.shtml), I read "No use of the command smt."

But what about smt2? Does the same exclusion hold?

(I should say I have no idea about the difference between them)

TIA,
Marco

Email Gateway (Aug 19 2022 at 16:34):

From: Tobias Nipkow <nipkow@in.tum.de>
On 04/11/2014 21:03, marco caminati wrote:

In AFP submission guidelines (http://afp.sourceforge.net/submitting.shtml), I read "No use of the command smt."

But what about smt2? Does the same exclusion hold?

Yes.

Tobias

(I should say I have no idea about the difference between them)

TIA,
Marco

smime.p7s

Email Gateway (Aug 19 2022 at 16:34):

From: Makarius <makarius@sketis.net>
This is explained in NEWS:

• SMT module: A new version of the SMT module, temporarily called "SMT2",
  uses SMT-LIB 2 and supports recent versions of Z3 (e.g., 4.3). The new
  proof method is called "smt2". CVC3 and CVC4 are also supported as
  oracles. Yices is no longer supported, because no version of the solver
  can handle both SMT-LIB 2 and quantifiers.

In the next release, there will be only the new version of the SMT module
and Z3, and the proof method will be just called "smt" again.

Back to the AFP question. The official text from
http://afp.sourceforge.net/submitting.shtml says:

No use of the command smt. The result of this command depends on
external tools that are not under our control and may stop working in
the future.

I am not an AFP editor, but my interpretation of it: since Z3 is non-free,
having AFP entries depend on it would render them unusable for people who
don't have a valid Z3 license. Z3 is only free as in beer for
non-commercial users. It is a friendly move of MSR that we can easily
bundle it according to its non-free license, but it is not a proper
open-source component.

Makarius

http://stop-ttip.org 797,770 people so far

Email Gateway (Aug 19 2022 at 16:35):

From: marco caminati <marco.caminati@yahoo.it>

Mar 4/11/14, Tobias Nipkow <nipkow@in.tum.de> ha scritto:

But what about smt2?
Does the same exclusion hold?
Yes.
Tobias

Mar 4/11/14, Makarius <makarius@sketis.net> ha scritto:

I am not an AFP editor, but my interpretation of it: [...]

Good to know, thanks to both Tobias and Makarius.

Best,
Marco

Last updated: Nov 21 2024 at 12:39 UTC