Revise the implementation of logical expressions

Issue #48 new
created an issue

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.

Comments (2)

  1. geisserf reporter

    I've already done some research on other implementations of domain-specific languages (DSL). [1] and [2] considers the visitor pattern. Another popular framework is the Boost Proto Library. However, I'm currently investigating Catamorphisms; they have the advantage that they are an algebraic sound tool to evaluate functions and are powerful enough to support arbitrary methods applied on expressions. Eric Niebler (the author of the Proto library) considered them one time for Proto and they are a popular tool in Haskell. I'm currently investigating the C++ approach, how easy it is to implement, and if it suits our requirements.

  2. Log in to comment