dec_trivial performance

Stream: general

[Moses Schönfinkel]

I have a computation resolved by dec_trivial that takes about 5 minutes with extreme deterministic timeout lean server setting. How does one diagnose this kind of performance problem - is there a way to inspect what's happening or is the situation similar to #reduce where you're somewhat out of luck in this regard and the best bet is to step through C++ with a debugger? (As a side note, what is being computed is handled by #eval in a few milliseconds.)

[Simon Hudon]

dec_trivial is really a blunt instrument. If your proof involves any natural numbers, that's going to take a long time. As you say, it is analogous to #reduce. If you're working with numbers, consider using norm_num

[Moses Schönfinkel]

Sadly I am not - however, this is a great reply, I'll have to take a look at the kinds of tricks norm_num plays and perhaps tailor a solution for myself. Thanks!