search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
302 stars 52 forks source link

remove `STLAllocator<T>` #571

Closed MichaelRawson closed 4 months ago

MichaelRawson commented 5 months ago

With the re-work of Allocator, it's possible that STLAllocator<T> is no longer necessary either. This could have a performance impact as it calls into Vampire's small-object allocator, but I suspect it might be minimal or positive and @quickbeam123 was keen on the idea of no more vstring.

This is just the initial sketch: if it passes the performance question, I will clean up further.

MichaelRawson commented 5 months ago

Tag #157.

quickbeam123 commented 5 months ago

Preliminary run shows this is measurably worse. (Could this be because of vstring though?) Maybe we should figure out which class of those affected is a least a bit hot and keep the special treatment only that one?

MichaelRawson commented 5 months ago

Bleh - it wasn't noticeably bad on the few things I tested here, so I hoped otherwise! I'll dig into it and do exactly that, it'd be nice to have this gone.

quickbeam123 commented 5 months ago

Measurable means "5" problems over the whole TPTP in -i 100000. But still, I'd consider this an opportunity to dig deeper.

MichaelRawson commented 5 months ago

Is it easy to work out which those 5 problems are? perf diff is saying that this Vampire calls memset a lot more from MLMatcher, but I'm not really sure why or what to do with this information.

quickbeam123 commented 5 months ago

The 5 extra was actually 42 gained / 37 lost for the default strategy, i.e., with lrs. Will better come back (in a while) with a discount-based diff.

quickbeam123 commented 5 months ago

No problem in the diff for discount. Sorry for the false alarm. I think this can be promoted to the full extent.

Except maybe for the vstring, maybe we can keep it as a typedef to prevent another giant refactor?

MichaelRawson commented 5 months ago

Great! I'll eliminate most of this properly then. Agreed with vstring. :-)

MichaelRawson commented 5 months ago

Should be ready for re-review. v(i|o)?stringstream and various vcontainers are no more, only vstring remains. vvector was a bit of a pain but is now also dead.

MichaelRawson commented 5 months ago

As discussed, also inline vstring.