Re: [isabelle] SMT integration to Isabelle/HOL



On 16/04/12 22:00, Tobias Nipkow wrote:
> Am 16/04/2012 05:54, schrieb Shuling Wang:
>> Hello,
>>
>>  
>>
>> We are trying to integrate an SMT solver to Isabelle/HOL. It seems that the
>> integration of external procedures is done by defining oracles in Isabelle.
>> I see that the new release of Isabelle supports SMT solvers like Z3, CVC,
>> Yices. I would like to know that, if we implement the SMT solver in the same
>> language as Z3, and also the same input standard, can we avoid defining the
>> oracle and apply the existing oracle for Z3 directly?
> You can share Isabelle's Z3 oracle if your input language is the same as Z3.
> Jasmin already pointed you to the relevant files.
>
> The Z3 link can also reconstruct Z3 proofs in Isabelle (thanks to Sascha), which
> is the safest way to integrate extertnal tools. If your SMT solver outputs
> proofs in the Z3 format, Isabelle could check them, too.
>
> Tobias
A word of warning: the Z3 link can reconstruct Z3 proofs, but Sascha had
to do a lot of guesswork. Z3 breaks large proofs down into component
steps, which is very helpful. Some of these steps are still very large,
however, and all that is given is a name (such as "lemma" or "rewrite").
Sascha guessed what Z3 had done and picked appropriate Isabelle tools,
which might be totally inappropriate for your tool.

In conclusion: Z3's proof output format is far from ideal. You might be
able to come up with a much better one yourself. I can give you some
hints at a later point. Also, the Z3 input language Sascha picked is
just SMTLIB/SMTLIB2.

I would recommend you start by reading some of Sascha's papers on his
work. See http://www4.in.tum.de/~boehmes/ (especially "Fast LCF-style
Proof Reconstruction for Z3").

Yours,
Thomas.





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