[isabelle] Isabelle as an interface to Z3

Dear Isabelle users,

I am producing Z3 code to check whether a data structure given in input satisfies certain set-theoretical properties.

I find such properties are much more easily written down in Isabelle than directly in Z3, so I am using sledgehammer with overlord=true, and then I take the generated prob_z3.smt_in and tweak it.

To me, it looks like Isabelle could also be, in addition to its functionalities, a useful way of interfacing to SMT solvers in cases not necessarily related to proof finding, as I am doing in my particular case.

However, I have little control on the z3 file I obtain: the syntax is not so readable, and the list of facts there can be populated with irrelevant asserts.
I played with sledgehammer's options max_facts=smart and fact_thresholds, but I am not sure that they give me enough control.

My questions:

- is there a better approach to use Isabelle this way (as a general-purpose interface to z3)?

- does it make sense at all to use it this way, or are there more convenient interfaces to avoid writing every involved notion at the z3 or SMT-lib level?


Marco Caminati

Marco Caminati, PDRF
School of Computer Science, University of St Andrews 
Jack Cole Building, North Haugh
St Andrews KY16 9SX 
Tel: +44 1334 426399
Fax: +44 1334 463278
mbc8 at st-andrews.ac.uk

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