Re: [isabelle] Isabelle as an interface to Z3
> 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.
Interesting. Could you explain a little bit more what kind of tweaking you are doing at the SMT-LIB level, and what you are trying to achieve? I get the impression that you are using SMT for their model finding capabilities, as opposed to proving. Is this correct? If so: How do you deal with quantifiers (which normally lead SMT solvers to answer "unknown" rather than "sat")?
If possible, could you send a small example of an Isabelle theory file, the generated SMT-LIB file, and your tweaked SMT-LIB file, so that I get a picture of what you are doing?
> - is there a better approach to use Isabelle this way (as a general-purpose interface to z3)?
From the perspective of a user of Isar, not really. But if you're ready to program some ML, it should be possible to reuse large parts of the current SMT module to achieve what you want.
But again, I'd be curious to know how you define the difference between "general purpose" and "proof finding" -- is it just "model finding" or is it more?
> - 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?
If what you have in mind is model finding, work has recently started at Inria Nancy on an SMT-based successor to Nitpick, called Nunchaku. It will be based primarily on the CVC4 model finder (which is, in my experience, even more powerful than Z3). There's nothing to show yet, but you can always keep an eye on
for some of the science behind Nunchaku.
This archive was generated by a fusion of
Pipermail (Mailman edition) and