Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Run simplifier without arithmetic splitting?

view this post on Zulip Email Gateway (Aug 22 2022 at 20:41):

From: Peter Lammich <lammich@in.tum.de>
Hi,

I have the suspicion that the simplifier gets unbearably slow due to
excessive splitting by the built-in linarith procedure.

Is there any way to switch this off, or to reduce the split-limit, such
that I can test my hypothesis?

Reducing linarith_split_limit will bomb the trace output with messages,
which makes the whole thing even slower.

Thanks in advance for any help,
Peter

view this post on Zulip Email Gateway (Aug 22 2022 at 20:49):

From: Makarius <makarius@sketis.net>
So how about commenting it out for the test? See
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2019/src/HOL/Tools/lin_arith.ML#l432

Makarius

Last updated: Nov 21 2024 at 12:39 UTC