ArraySolver: Tiny performance optimization #715
Conversation
| for (auto secondIt = selects.begin(); *secondIt != first; ++secondIt) { | ||
| ERef second = *secondIt; | ||
| if (firstRoot == getRoot(second)) { continue; } // The selects are already the same, no lemma needed | ||
| NodeRef arrayFirst = getNodeRef(getRoot(getArrayFromSelect(first))); | ||
| NodeRef arraySecond = getNodeRef(getRoot(getArrayFromSelect(second))); | ||
| if (arrayFirst == arraySecond or getIndexedRepresentative(arrayFirst, index) == getIndexedRepresentative(arraySecond, index)) { |
There was a problem hiding this comment.
getIndexedRepresentative(arrayFirst, index) can also be computed right after arrayFirst
There was a problem hiding this comment.
Yes, but in this case, it is possible that in the original code, it would not be called at all :)
I mean, I don't want to spend time on this now. I think the whole method (at also its usage) needs investigation about how to improve it.
| for (auto secondIt = selects.begin(); *secondIt != first; ++secondIt) { | ||
| ERef second = *secondIt; | ||
| if (firstRoot == getRoot(second)) { continue; } // The selects are already the same, no lemma needed | ||
| NodeRef arrayFirst = getNodeRef(getRoot(getArrayFromSelect(first))); | ||
| NodeRef arraySecond = getNodeRef(getRoot(getArrayFromSelect(second))); | ||
| if (arrayFirst == arraySecond or getIndexedRepresentative(arrayFirst, index) == getIndexedRepresentative(arraySecond, index)) { | ||
| std::unordered_set<PTRef, PTRefHash> undecidedEqualities; |
There was a problem hiding this comment.
What happens if this hash is made to reuse its storage? I.e. move it outside the loops and just call undecidedEqualities.clear() here?
There was a problem hiding this comment.
I mean, it should work, but does it improve performance significantly?
There was a problem hiding this comment.
We cannot do that. The map is currently being moved into LemmaConditions.
There was a problem hiding this comment.
Yes, but after moving and clearing it is again in a valid state. It may potentially reuse previously dynamically allocated storage, it depends on implementation.
blishko
force-pushed
the
array-solver-tiny-opt
branch
from
2fcf805 to
2f72cc0
Compare
This is just a tiny optimization to not repeat the same work inside a loop when we can do it once before the loop.