Performance overhead in proof_trace_callback_writer

[stevenmeker]

The MPG team have reported a substantial overhead with this class, even when the callback functions are empty. The code in this class does very little but makes use of std::vector<> instantiations for function symbol arguments and substitutions. Putting data in a freshly allocated std::vector<> object implies a heap allocation which much be handled by malloc() and deallocated by free(). One or more malloc()/free() call pairs per rewrite would likely account for the overhead.

One possible resolution is to have a class in the MPG inherit directly from the abstract base class, proof_trace_writer, and cut out proof_trace_callback_writer altogether.

An alternative resolution is to have the needed std::vector<> objects allocated just once inside proof_trace_callback_writer and then resized and reused as needed for each callback. Resizing a vector that already has sufficient memory attached is cheap. Futhermore std::vector<> objects can be moved efficiently with std::move(). However this means that data structures can only be loaned to the MPG in a callback and will not be valid after the callback returns, because they will have be moved or reused.

[stevenmeker]

Actually there are data members in proof_trace_callback_writer that are being reused.

  std::optional<call_event_construction> current_call_event_;

  std::optional<rewrite_event_construction> current_rewrite_event_{
      std::nullopt};

The problem is that the are being reused by calling the optional::reset() method that destroys the contained object and optional::emplace() method that creates a new one. Destroying and creating std::vector<> instances is expensive.