search

vprover / vampire

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

remove USE_ALLOCATOR where it very likely makes no difference #506

Closed MichaelRawson closed 11 months ago

MichaelRawson commented 11 months ago

In #499 we got rid of quite a few of the old allocator macros. However, it's not possible to remove any more without possibly affecting performance significantly.

This PR removes only those USE_ALLOCATOR instances where in my opinion it's unlikely to make a difference. This could be because:

  1. The code is unused.
  2. The object is only likely to be created a small number of times: inference engines, decision procedures, SAT solvers, main loops, indices, and the like.
  3. The object is used a moderate number of times, but mostly during parsing: symbols, types.
  4. The object is never heap-allocated.

This removes roughly two-thirds of the USE_ALLOCATOR instances, which allows us to focus on the trickier ones. In my view this could go in without performance testing, but of course I don't object if you think it needs it.

quickbeam123 commented 11 months ago

This seems to be actually helping the notorious discount10 from 8746.8 to 8753.4 TPTP FOL probs in 10000 Mi on average.