Re: [isabelle] How to invoke Z3 from Isabelle



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


On 21 Jun 2012, at 10:31, Joshua Nwokeji wrote:

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