Re: [isabelle] How to invoke Z3 from Isabelle



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 at 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








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.