Re: [isabelle] How to invoke Z3 from Isabelle
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,
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
If that is not what you want to do, you might want to have a look into
JNI  to build an interface between Z3's C-API and Java.
Quoting Joshua Nwokeji <J.Nwokeji at mdx.ac.uk>:
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.
School of Engineering and Information Sciences (EIS),
Middlesex University, London
This archive was generated by a fusion of
Pipermail (Mailman edition) and