Re: [isabelle] Run simplifier without arithmetic splitting?



On 03/10/2019 20:30, Peter Lammich wrote:
> 
> 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.

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




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