Performance overhead in proof_trace_callback_writer

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.

Locate proof_trace_callback_writer and its relationship to the proof_trace_writer base class and MPG callbacks. Compare the allocation behavior of the callback path, including empty callbacks, then determine which proposed design preserves callback data semantics while removing the overhead. Done means the overhead is reduced and callback behavior remains correct.