Email Gateway (Aug 18 2022 at 20:09): Email Gateway (Aug 18 2022 at 20:09):From: Joshua Nwokeji <J.Nwokeji@mdx.ac.uk>
Dear all!
I am currently learning how to use Z3 SMT solver. I program in Java, unfortunately, Z3 does not interface with Java.
Luckily , I read about Isabelle but I don't have an idea on how to use it, nor how to invoke Z3 from Isabelle.
Please I will appreciate any help offered to me in this regard, especially if there is a link I can download detailed and self explanatory tutorial on how to Invoke Z3 from Isabelle.
Regards
Joshua Nwokeji
School of Engineering and Information Sciences (EIS),
Middlesex University, London
Email Gateway (Aug 18 2022 at 20:09):From: Sascha Boehme <boehmes@in.tum.de>
Hi Joshua,
Z3 cannot be invoked directly from Isabelle. It is wrapped into a
layer to ease the interaction for users. You can invoke Z3 from
Isabelle interactively for proving theorems, e.g. as follows:
lemma "P & Q --> P" using [[smt_solver=z3]] by smt
Yet, it is more convenient to use Z3 as a backend prover of
Sledgehammer (see the Sledgehammer tutorial that is distributed with,
e.g., Isabelle-2012).
There is also an API in ML if you want to programmatically interface
with Z3. You can find it in the Isabelle-2011 distribution in file
src/HOL/Tools/SMT/smt_solver.ML.
If that is not what you want to do, you might want to have a look into
JNI [1] to build an interface between Z3's C-API and Java.
Cheers,
Sascha
[1] http://java.sun.com/docs/books/jni/
Quoting Joshua Nwokeji <J.Nwokeji@mdx.ac.uk>:
Email Gateway (Aug 18 2022 at 20:10):From: Lars Hupel <hupel@in.tum.de>
If that is not what you want to do, you might want to have a look into
JNI [1] to build an interface between Z3's C-API and Java.
... which has already been done: <https://github.com/psuter/ScalaZ3/>
(for Scala, though, which is a JVM language). Here are some examples:
<http://lara.epfl.ch/w/jniz3-scala-examples>.
Email Gateway (Aug 18 2022 at 20:10):From: Grant Olney Passmore <grant.passmore@cl.cam.ac.uk>
Hi, Joshua --
If you just want to experiment with Z3 programatically, using Isabelle may be overkill (and I have no idea how Java could fit into the picture).
I don't know of any Java Z3 interfaces, but Z3 4.0 has a very easy to use new Python interface called Z3Py.
See the Z3Py tutorial ( http://rise4fun.com/Z3Py/tutorial/guide ) for more.
Even not knowing any Python, I think it's pretty easy to build upon the tutorial examples and get started experimenting with Z3.
Note also that Z3Py can be used on the web without having to install Z3 locally. The Z3Py tutorial shows you how to do this.
Z3Py exports most of Z3's new LCF-inspired strategy machinery, which can be useful for constructing custom proof procedures.
See the Z3 Strategies tutorial ( http://rise4fun.com/Z3Py/tutorial/strategies ) and this draft article ( http://research.microsoft.com/en-us/um/people/leonardo/strategy.pdf ) for more.
Best wishes,
Grant
Last updated: Apr 18 2024 at 04:17 UTC