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