Re: [isabelle] Isabelle as an interface to Z3

Dear Jasmin,

many thanks for your helpful answer.

Mar 17/11/15, Jasmin Blanchette <jasmin.blanchette at> ha scritto: 

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

The idea is to use Z3 to check whether some finite set-theoretical relation (i.e., a set of pairs) can be completed to a bigger relation satisfying some simple requirement (e.g., being a partial order).
Since Isabelle/HOL already features a bit of (naive) set theory which I could take advantage of in doing that, I thought to give Isabelle a shot as an intermediate layer.

> I get the
> impression that you are using SMT for their model finding
> capabilities, as opposed to proving. Is this correct? 

Yes, this is correct.
However, I have to apologize for not explaining clearly enough that this is all extremely tentative.
Indeed, the legitimate doubts you raise below could make this approach infeasible.

> How do you deal with quantifiers (which normally lead SMT
> solvers to answer "unknown" rather than "sat")?
I think this is the main problem: for some very simple cases, z3 returns a solution, but it hangs for most elementary cases. I found this answer by Leonardo De Moura (Z3 developer), which probably puts a serious no-go to my approach:
> 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?
Thanks for the generous help offer!
However, I wouldn't want to waste your time since, as it appears from the link above, this effort could be sterile.
Anyway, the kind of Isabelle lemma I used to generate the most elementary z3 input file is something like (with the due dependencies imported):

lemma "EX P. (1::nat,2::nat) \<in> P & (2::nat,3::nat) \<in> P & trans P & antisym P & irrefl P" 
sledgehammer [provers=z3, spy=true, overlord=true, debug=true]

The corresponding z3 input file already hangs z3.

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

Currently, I am not sure whether it would be worth doing that, rather than coding directly in Z3.
But it is definitely worth knowing your assessment about the possibility of reusing the SMT module.

> 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?
I meant "model finding".

> 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
Glad to learn about that, I'll keep an eye on it.
Also, I had no idea of CVC4's power. It could be a Z3 contender, then, which adds yet another (welcome) degree of freedom to my choices :)

Again, many thanks for your much appreciated answer.



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