Thanks for investigating. A number of years back, we had once investigated this issue, and I confirm your observation: The majority of time is spent (wasted?) on equality treatment. There were a few suggestions to change the treatment then.

One plan was to set up a set of left-hand-sides of equations and only check for newly introduced terms if they occur in this set. Trigger a rule application then. For some reason the implementation turned out not to be faster. But I still believe it should have been faster.

I'd be happy if we could revisit this issue.

This is the hash code used for the map:

I think performance can be improved by adding more data to the hash code. For example the term depth must also be equal (I believe):

@Override
public int hashCode() {
    return Objects.hash(term.op(), term.depth());
} 

I don't think that this coarse hash code scheme is the problem.

I replaced it with the hashing function in https://gist.github.com/mattulbrich/28c0f53f5a9f608c8c86f2ab1da39546, and it produced proofs of almost the same runtime (and same number of rule apps).

I am not fully sure how it works, but Richard's compiled taclet matcher may be an efficient alternative to checking all subterms with a hashtable ...

/cc @unp1

I replaced it with the hashing function in gist.github.com/mattulbrich/28c0f53f5a9f608c8c86f2ab1da39546, and it produced proofs of almost the same runtime (and same number of rule apps).

I do think it has a big impact, at least in some situations. Your proposed hash is much slower (mine: 282 seconds for 100% replay, yours: 360 seconds for 19% of the replay).

Ok, that obviously depends on the program to load. I apparently looked at a smaler program. Which example do you use for reference?

While you are at it: The treatment of equalities (applyEq) was found out to be also very slow and inefficient and turned out be the major time waster in many proofs. Feel free to fix it if you stumble across it. :-P

Ok, that obviously depends on the program to load. I apparently looked at a smaler program. Which example do you use for reference?

I use https://gist.github.com/FliegendeWurst/9be15e20e3bfd0722fcdd7f5c4afebcd. It requires some of my changes in https://github.com/FliegendeWurst/key/tree/testing, most notably the support for \dl_seqGet__int (although by now I think it could simply be written as (int) \dl_seqGet).

With some more optimizations it is possible to eliminate this particular slowdown:

Now the other bit of logic in the Simplifier takes approx. 90% of the CPU time. This is actuallly expected because I added some more rules to the OSS for this experiment (selectOfStore, selectOfCreate, selectOfAnon, selectOfMemset, dismissNonSelectedField, selectCreatedOfAnon, castDel, sortsDisjointModuloNull, ifthenelse_negated, elementOfUnion, elementOfArrayRange).

In fact, almost all CPU time is spent in refactorLabelsRecursive.

Regarding selectOfStore etc. Christoph Scheben implemented a set of taclets which pull out common heap terms such that such select-store chains need not be reduced more than once. It may be that adding taclets to the OSS may render these techniques useless.

That's of course even better. I will look into it.

In any case, I have done another profiling session (this time with origin tracking disabled):

It appears CPU time is spent on:

• finding the taclet (~75%)
• rewriting the term (~20%)

I have done some more tests on ShortestPath.java:

I ran the macros Finish Symbolic Execution and Heap Simplification in each configuration (rule app count above is after executing each macro).
The last run did not finish in 9 hours. After stopping the macro the UI became unresponsive, meaning the numbers are a lower bound.