Re: [isabelle] changing smt by automatic reasoning internal to Isabelle




> On 31 Jul 2019, at 16:57, Dominique Unruh <unruh at ut.ee> wrote:
> 
> I noticed that until October 2017, the submission instructions for AFP also contained "No use of the command <code>smt</code>. The result of this command depends on external tools that are not under our control and may stop working in the future."
> 
> This was removed in commit 48c7802 (afp-devel) by Gerwin Klein.
> 
> I am curious why this is no longer a necessity? As I understood, the reason was not the fact that the proof is not replayed (as in the case of smt_oracle), but that the behavior of smt depends on Z3, and thus breaks easily when Z3 changes.
> 
> Is my understanding correct? Has this situation changed? Or has merely the policy changed and the expectation is that smt proofs are just fixed once Z3 changes make them the smt proofs break?

Yes, the latter. The policy has changed, because we were observing very few failures of this kind in other Isabelle code where we did not have the restriction, and this has been played out similarly on the AFP since we changed it. We are also changing Z3 versions less often than we used to. I.e. the benefit of allowing smt outweighs the drawbacks. 

I should probably update my style guide accordingly as well.

Cheers,
Gerwin



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