*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Z3 proof reconstruction - optimizations*From*: Filip Marić <filipmatfbgacrs at gmail.com>*Date*: Fri, 22 Aug 2014 12:40:42 +0200*Reply-to*: filip at matf.bg.ac.rs

Hi! In a recent project I have been extensively using automation provided by the SMT solver interface in Isabelle 2013-2 and it had really been a great experience (many thanks to Sasha, Tjark, Jasmin and other members of the team for making this option available in Isabelle)! However, I have noticed that proof reconstruction of some small and fast z3 proofs goes unexpectedly slow (e.g., z3 produces a proof in under a second and a proof consists only of several thousand steps, but reconstruction goes well beyond 10 seconds) and I have decided to investigate this issue deeper. By using the [[smt_trace = true]] option, I think that I have pinpointed some sources of inefficiency. Although I do not have explicit timings for each proof step (what would be a desirable feature), it seemed pretty obvious that proof reconstruction gets stuck only in a very small number of proof steps, and interestingly, these are all "rewrite" steps - they are all given to fast (logic) method and after a rather long period of time it succeeds (and even worse, in a very small number of cases it seems that it gets stuck). One case of such behavior occurred when proving lemmas whose conclusion contains <-->. At first I solved the problem by using (by (rule iffI, smt+) instead of by smt), but after examining the problematic rewrite steps I have noticed that I do not need to do this and that many such proofs can be made enormously faster by adding the following z3_rule: lemma [z3_rule]: "(\<not> (A \<longleftrightarrow> \<not> B)) \<longleftrightarrow> (A \<longleftrightarrow> B)" by simp Then, the problematic rewrite steps are solved in the first pass and are never even given to the "fast (logic)" method which was very slow on them. In other cases that I noticed that are problematic in my project I have also spotted a pattern, but this happened with much more complicated formulas so I am not sure how to fix this. Here are some examples of problematic proof steps of this kind (all are rewrite steps): (iff (and #72578 (not #72574) #72571 (not #72567) (not (or #134247 #134251 #134255 #134259 #134263 #133898 #133902 #133907)) #72564) (not (or (not #72578) #72574 (not #72571) #72567 #134247 #134251 #134255 #134259 #134263 #133898 #133902 #133907 (not #72564)))) (iff (and (not #75701) #72571 (not #72567) (not (or #134259 #134724 #134263 #134729 #134733 #133911 #134575 #133915)) #76020) (not (or #75701 (not #72571) #72567 #134259 #134724 #134263 #134729 #134733 #133911 #134575 #133915 (not #76020)))) (iff (and (not #96335) #93205 (not #93201) (not (or #140614 #141079 #140618 #141084 #141088 #140266 #140930 #140270)) #96654) (not (or #96335 (not #93205) #93201 #140614 #141079 #140618 #141084 #141088 #140266 #140930 #140270 (not #96654)))) (iff (and (not #93212) (not #93208) #93892 (not #92681) (not (or #140769 #140773 #140602 #140777 #140614 #140436 #140440 #140253)) #93887) (not (or #93212 #93208 (not #93892) #92681 #140769 #140773 #140602 #140777 #140614 #140436 #140440 #140253 (not #93887)))) (iff (and (not #181613) #181578 #206617 #180700 #180691 #181342 #181291 (not (or (not #206438) (not #206236))) #206701) (not (or #181613 (not #181578) (not #206617) (not #180700) (not #180691) (not #181342) (not #181291) (not #206438) (not #206236) (not #206701)))) Hash-numbers in these formulas represent very complex atoms of linear arithmetic (some of them extensively use ite operator). It can be noticed that in all these cases the lhs of iff is a conjuction containing atoms and exactly one negation of a disjunction. (1) Is it possible to add some simple z3_rules that would cover all these proof steps and to prevent to give this large formule to the fast (logic) method as it turns out that it needs much time (several seconds) to discharge them (and in some cases it seems that it gets totally stuck and cannot finish their proof)? (2) Is it possible to set a timeout for each proof step or for the whole proof reconstruction (it seems to me that smt_timeout is only for SMT solver time, and not the reconstruction time, but maybe I am wrong here)? From a users perspective it seems that it would be good to have a timeout for each proof step as it would help detecting the cases were reconstruction gets stuck or is very slow. Otherwise i must either use smt_trace which is slow because of the large output or I must wait very long time and never know if the reconstruction is stuck somewhere. A very nice option would be to give some progress ratio in the trace -- as you know the total number of proof steps that need to be reconstructed, from time to time (e.g., every second) you could print the percent of reconstructed proof steps. Also, is it possible to get some statistics about the number of proof steps of each kind and time spent for their reconstruction in Isabelle? I hope that you have some quick and nice solution to the issue (1), and issue (2) is only a feature request from a user so I know that it cannot be done immediately, but I hope that some of this could be incorporated in some future releases :) Best regards, Filip

- Previous by Date: Re: [isabelle] Isabelle2014-RC4: sledgehammer blocks all other progress
- Next by Date: Re: [isabelle] error mit Pretty.T
- Previous by Thread: Re: [isabelle] error mit Pretty.T
- Next by Thread: [isabelle] Experimental Isabelle/jEdit support for bsup/esup + bsub/esub
- Cl-isabelle-users August 2014 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