*To*: marco caminati <marco.caminati at yahoo.it>*Subject*: Re: [isabelle] Isabelle as an interface to Z3*From*: Jasmin Blanchette <jasmin.blanchette at inria.fr>*Date*: Tue, 17 Nov 2015 16:07:08 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <993768880.9818751.1447768582899.JavaMail.yahoo@mail.yahoo.com>*References*: <993768880.9818751.1447768582899.JavaMail.yahoo.ref@mail.yahoo.com> <993768880.9818751.1447768582899.JavaMail.yahoo@mail.yahoo.com>

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

**References**:**[isabelle] Isabelle as an interface to Z3***From:*marco caminati

- Previous by Date: Re: [isabelle] find_theorems finds private lemmas
- Next by Date: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Previous by Thread: [isabelle] Isabelle as an interface to Z3
- Next by Thread: Re: [isabelle] Isabelle as an interface to Z3
- Cl-isabelle-users November 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list