CIF/BDD: cache results of algebraic variable conversion to prevent exponential blow-ups

Problem

If algebraic variables are used multiple times, we currently convert them again and again each time that we encounter them. In certain cases, this may lead to performance issues. It can even lead to an exponential blow-up in conversion time. We identified this in a research project, where this could happen in real-world models, due to a translation scheme we devised there. To show-case the exponential blow-up, in an artificial context not from that research project, consider the following model:

plant a:
  location:
    initial;
    marked a9;
end

input bool i;

alg bool a1 = i;
alg bool a2 = not i;
alg bool a3 = a1 or a2;

alg bool a4 = a3;
alg bool a5 = not a3;
alg bool a6 = a4 or a5;

alg bool a7 = a6;
alg bool a8 = not a6;
alg bool a9 = a7 or a8;

There are multiple layers of algebraic variables, Each group of lines models one layer. Each layer has a choice between the next layer's algebraic variable and its negation. We get 2 * 2 * 2 * 2 * ... possible choices then. The example above has three layers. The last algebraic variable is used in a marker predicate. The conversion of the predicate unfolds a9, which leads to unfolding a7 and a8. Both lead to unfolding a6, which is thus unfolded twice. Unfolding a6 leads to unfolding a4 and a5, which both lead to unfolding a3, which is thus unfolded twice per unfolding of a6. In total, a3 is thus unfolded four times. Etc.

I made a generator, that generates instances of this problem with varying numbers of layers, and I've synthesized them, to show the exponential blow-up. Here are the results for 15-22 layers:

15: 159 ms
16: 298 ms
17: 533 ms
18: 1,000 ms
19: 1,866 ms
20: 3,754 ms
21: 7,454 ms
22: 14,565 ms

I used the following script: test.tooldef

Note that in the BDDs representation, each algebraic variable is only represented once, due to maximal sharing. However, the conversion to produce those BDDs naively recursively unfolds the CIF expressions, resulting in an exponential blow-up.

Solution

I think the solution is easy. We can just maintain a Map<AlgVariable, BDD> algVarCache to cache the results of converting algebraic variables to BDDs. The first time we convert an algebraic variable, we add the result to the cache. On each use of the algebraic variable, we use only copies of the cached results. After the conversion, we free all cache entries. Each algebraic variable is then only converted once, solving the problem.