Email Gateway (Aug 22 2022 at 11:55): Email Gateway (Aug 22 2022 at 11:55):From: marco caminati <marco.caminati@yahoo.it>
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?
Best,
Marco Caminati
Marco Caminati, PDRF
School of Computer Science, University of St Andrews
Jack Cole Building, North Haugh
St Andrews KY16 9SX
Scotland
Tel: +44 1334 426399
Fax: +44 1334 463278
mbc8@st-andrews.ac.uk
http://caminati.co.nr
Email Gateway (Aug 22 2022 at 11:55):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Marco,
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
https://github.com/nunchaku-inria
See also
http://www.loria.fr/~jablanch/smt_frf.pdf
for some of the science behind Nunchaku.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 11:58):From: marco caminati <marco.caminati@yahoo.it>
Dear Jasmin,
many thanks for your helpful answer.
Mar 17/11/15, Jasmin Blanchette <jasmin.blanchette@inria.fr> 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:
http://stackoverflow.com/a/17711058
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.
Best,
Marco
Email Gateway (Aug 22 2022 at 11:58):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Marco,
many thanks for your helpful answer.
My pleasure.
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:
Right. However, if your quantifiers happen to range over uninterpreted sorts (types), finite model techniques can be used. See e.g. Andrew Reynolds's Ph.D. thesis or the SMT Workshop 2015 paper he wrote with Cesare Tinelli and me and which I mentioned in the previous email.
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.
Yes. You might have a little bit more success with Nitpick (and, hopefully one day, Nunchaku):
lemma "EX P. (1::nat,2::nat) \<in> P & (2::nat,3::nat) \<in> P & trans P & antisym P & irrefl P"
nitpick [satisfy, dont_box]
Nitpick found a potentially spurious model:
Skolem constant:
P = {(1, 2), (1, 3), (2, 3)}
("dont_box" is unfortunately necessary here to disable a heuristic.)
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 11:58):From: marco caminati <marco.caminati@yahoo.it>
Dear Jasmin,
many thanks for your helpful answer.
Mar 17/11/15, Jasmin Blanchette <jasmin.blanchette@inria.fr> 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:
http://stackoverflow.com/a/17711058
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.
Best,
Marco
Email Gateway (Aug 22 2022 at 16:06):From: marco caminati via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Mar 17/11/15, Jasmin Blanchette <jasmin.blanchette@inria.fr> ha scritto:
Oggetto: Re: [isabelle] Isabelle as an interface to Z3
A: "marco caminati" <marco.caminati@yahoo.it>
Cc: cl-isabelle-users@lists.cam.ac.uk
Data: Martedì 17 novembre 2015, 15:07
I do a bit of necrothreading to report on some developments on my side.
We found useful application of sledgehammer's SMT generator beyond its intended usage, I think.
In our approach, generated SMT is either directly used to compute, or anyway fed to the solver to show its equivalence with the more efficient SMT code we wrote some other way.
This way, we retain the possibility of proving in Isabelle the stuff we want about the final SMT code, and have therefore a sort of correctness about SMT code (arguably a good thing, given the low level of readability of SMT code one easily gets); moreover, by staying in Isabelle as long as we can, we can integrate our code with other tools (Nitpick, etc...).
This has some similarity with the current functional code generation feature of Isabelle.
Reports are scattered among conference papers, in particular:
http://ieeexplore.ieee.org/document/7890603/?reload=true (sections IV and V)
https://arxiv.org/abs/1707.05383 (section 5, particularly Figure 7)
Hope this can be of interest to somebody.
Thanks again to Jasmin for the useful help he gave on the original message.
Marco
Last updated: Nov 21 2024 at 12:39 UTC