Investigation into a performance issues on some CHC-COMP benchmarks revealed that every access to the steps computed by the CongChainVisitor created a new copy of the steps, which was a performance killer, since this actually happened on access to each step. The easy fix here is to return (and use) just a reference to the stored vector of steps.
Additionally we make use of a C++ std::enable_shared_from_this that allow us to still use the visitor pattern, but turn the raw pointer back to shared pointers without the risk of creating two separate shared_ptr managing the same raw pointer. Since we only create Terms as shared pointers, this is safe, but we should make another step and hide all constructors and only expose a factory method returning shared_ptr.
Investigation into a performance issues on some CHC-COMP benchmarks revealed that every access to the steps computed by the
CongChainVisitorcreated a new copy of the steps, which was a performance killer, since this actually happened on access to each step. The easy fix here is to return (and use) just a reference to the stored vector of steps.Additionally we make use of a C++
std::enable_shared_from_thisthat allow us to still use the visitor pattern, but turn the raw pointer back to shared pointers without the risk of creating two separateshared_ptrmanaging the same raw pointer. Since we only createTerms as shared pointers, this is safe, but we should make another step and hide all constructors and only expose a factory method returningshared_ptr.