Re: [isabelle] Isabelle as an interface to Z3



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:
> 
> http://stackoverflow.com/a/17711058

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





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