Our current implementation of logical expressions and related functions has three major disadvantages:
no memory management. Whenever a new logical (sub-)expression is created, we have a new raw pointer which never gets deleted, even if the expression is not used anymore. This leads to problems when we implement algorithms with many expression transformations (e.g. EVMDD implementations in our icaps2016 paper).
due to the way logical expressions are implemented, methods transforming logical expressions have to do dynamic casting if their logic requires the knowledge of the specific type. This not only leads to boilerplate code, but has also influence on the runtime of such methods, e.g. state evaluation.
the current implementation is cumbersome to extend. When we want a new method which works on expressions, it has to be implemented in every expression type (logical_expressions.h has already nearly 1000 lines of code).
A new implementation should consider all three points.