long running time with low steps

[kanigsson]

Hello,

repr.ae.txt

On the attached reproducer, Alt-Ergo runs for a long time, despite specifying a low steps number:

$ alt-ergo repr.ae --steps-bound=200
... runs for several minutes ...

Probably some code doesn't increment the steps counter?

[Halbaroth]

Thanks for reporting this issue.

It seems there are at least two issues here (and maybe three?):

1. We don't increment steps in the reasoner of the Arrays theory.
2. The Arrays theory slows down Alt-Ergo in presence of very long terms, even if the input file doesn't involve terms of this theory, as it's the case for your example.
3. Alt-Ergo produces huge terms for this input file.

• In #1126, I wrote a quick fix for the second point and now Alt-Ergo solves your example immediately. The fix consists in caching the function responsible of the bottleneck in Arrays. The purpose of this function is to register relevant terms for the instantiation engine.. The current implementation explores all the terms of the problem to find select or store calls, which is very slow in presence of long terms.
• To solve the first point, I plan to add a counter for the Arrays theory but I don't plan to increment them in the function update_gets_sets.
• I didn't investigate the last point.

[bclement-ocp]

Fixed by #1126.