>> Today's isatest indicates a significant drop in performance: >> >> http://isabelle.in.tum.de/devel/stats/at-poly/HOL-Metis_Examples.png >> http://isabelle.in.tum.de/devel/stats/mac-poly-M4/HOL-Metis_Examples.png >> http://isabelle.in.tum.de/devel/stats/mac-poly-M8/HOL-Metis_Examples.png > > I added definitional CNF to Metis yesterday, which had a positive effect on > HOL and a neutral effect on the 1600 or so successful goals from the > Judgement Day suite. I'll revert this and reintroduce it if and when it can > be done without harming Metis_Examples (and other apps). (In fact, Larry now > suggested I avoid clausification altogether, which I will investigate in the > coming months.)
From my experience, when the performance of metis examples changes, this
might very well just due to one or two particular metis calls. It might
be worth examining those.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
