Do not use vectors indexed by Pterms' ids in LASolver #500
Conversation
|
Did you try it with qf_lra or qf_Lia already? I have some (probably outdated but still) evidence that hash maps might be a lot slower than an array. |
|
No, I wanted to try, but the cluster was not working today. I'll try later. I have a benchmark for Golem where this change meant more than 10% improvement. |
|
OK let's wait for the results. One option is to run them in mantella, there are some scripts to do that and it might be faster than waiting for the cluster to come up. |
When LAVarMapper is storing mapping from PTerms to LATerms as vectors with TermId as index, this creates possibly huge vectors with just a small number of entries filled. This is not a problem for single-use instances, but in applications where number of terms in Logic is growing constantly are a solver is queries repeatedly, the initialization of LASolver due to allocation of large vectors starts to be noticeable. For now we use standard hashmap as a replacement. It seems that some kind of flat map, which additioanlly does not need to support deletion could be even better.
|
It seems there is some slowdown associated with this. |
This PR suggests to replace the inner representation of how LASolver maintains mappings from Pterms to its inner representations (LVRefs and bounds).
Instead of vectors indexed by PTId, I suggest to use just normal HashMap.
The disadvantage of current representation is its memory inefficiency, because the size of the vectors possibly depends on the number of terms in Logic. But Logic may contain a huge number of terms compared to a few atoms that need to be represented in LASolver.
For OpenSMT itself this does not make much difference, but for Golem, it can have noticeable impact, as
LASolveris re-initialized on every check-sat call, and Golem makes quite a lot of them.